Protocols encoded in REFAL-5

Contents:

On the encoding of the cache coherence protocols: Parameterized protocols
for multithreaded Java programs: 		More parameterized protocols:

Specifications of the protocols.

It is not a good idea to see this Web-page in a small window.

On the encoding of the cache coherence protocols: We consider the protocols as discrete dynamic systems. Given an initial state d of such a system and a finite sequence p of the actions evaluating the system, the p determines the system state reached as the result of the last action. Thus, inherently, the p(d) is a call for a program transforming the states of the system and the result of the program p is the last state. We encode a protocol as an interpreter fint of the programming language defined by the protocols rules: each program is a finite sequence of the actions. Notice that not all actions are applicable to all protocol states; an attempt of execution of non-applicable action leads to an abnormal stop of the program. The post-condition Test encodes the safety property of the corresponding protocol.

Now the call Test(fint(p0,d0)) tests the protocol evaluated by a given sequence p0 on a given initial configuration d0.

Let us assume that the interpreter int(p,d) = Test(fint(p,d)) terminates for all possible values of its arguments, but for some values it may terminate with abnormal stop. The abnormal stop indicates the input values of the arguments are outside of the domain. Let us have a robust specializer generating a residual program q(p) = int(p,d0) defining an extension of the partial predicate defined by the problem int(p,d0) to be specialized. Assume that q is a partial constant function True or False and this property is expressed explicitly in syntax of q. For example, q does not contain any syntactic construction with the semantics return False (in the case of the True partial constant). In such a case, the result of specialization can be considered as a proof of the (partial) constant property. The termination property of int mentioned above guarantees that the domain of the original partial predicate is not empty.

Now the True-constant property of the residual program q means all source programs p satisfy the post-condition Test (in the given context of specialization). In such a case we conclude the specializer solved a verification problem. See references for an additional information about. We use REFAL-5 language for encoding of the interpreter and the SCP4 supercompiler as a specializer. Here we just notice that, as usually, /* and */ embrace multi-lines comments, while a line starting with * is a single-line comment. A line starting with *$ is a single-line comment for REFAL-5 and a switch for the SCP4 supercompiler, which indicates a strategy of specialization process.

Top Bottom On the encoding Specification Result of supercompilation

Example #1 (Synapse N+1):

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go { e.time (e.i) = <Loop (e.time) (Invalid I e.i)(Dirty )(Valid ) >; }

Loop {
  () (Invalid e.1)(Dirty e.2)(Valid e.3) =
         <Test (Invalid e.1)(Dirty e.2)(Valid e.3)>;
  (s.t e.time) (Invalid e.1)(Dirty e.2)(Valid e.3) = 
         <Loop (e.time) 
               <RandomAction s.t (Invalid e.1)(Dirty e.2)(Valid e.3)>>;
}


RandomAction {
* rh Trivial 
* rm
rm (Invalid I e.1) (Dirty e.2) (Valid e.3)
   = (Invalid e.1 e.2)  (Dirty ) (Valid I e.3);
* wh1 Trivial 
* wh2
wh2 (Invalid e.1) (Dirty e.2) (Valid I e.3)
   = (Invalid e.1 e.2 e.3)  (Dirty I) (Valid );
* wm 
wm (Invalid I e.1) (Dirty e.2) (Valid e.3)
   = (Invalid e.1 e.2 e.3)  (Dirty I) (Valid );
}


Test {
(Invalid e.1) (Dirty I e.2) (Valid I e.3) = False;
(Invalid e.1) (Dirty I I e.2) (Valid e.3) = False;

(Invalid e.1) (Dirty e.2) (Valid e.3) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • invalid ≥ 1, dirty = 0, valid = 0
  • The potentially unsafe states:
    • (1) invalid ≥ 0, dirty ≥ 1, valid ≥ 1
    (2) invalid ≥ 0, dirty ≥ 2, valid ≥ 0
Top Bottom On the encoding Specification Result of supercompilation

Example #2 (MSI):

/*
  The parameterized MSI protocol is taken from the paper
  "Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols" 
  by E.A. Emerson and V. Kahlon. 
*/

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go { e.time (e.i) = <Loop (e.time) (Invalid I e.i)(Modified )(Shared )>; }

Loop {
  () (Invalid e.1)(Modified e.2)(Shared e.3) 
       = <Test (Invalid e.1)(Modified e.2)(Shared e.3)>;
  (s.t e.time) (Invalid e.1)(Modified e.2)(Shared e.3) 
       = <Loop (e.time) <RandomAction s.t  (Invalid e.1)(Modified e.2)(Shared e.3)>>;
}


RandomAction {
* PrWr1
PrWr1 (Invalid I e.1) (Modified e.2) (Shared e.3)
                 = (Invalid e.1 e.2 e.3)  (Modified I)  (Shared );

* PrWr2 
PrWr2 (Invalid e.1)(Modified e.2)(Shared I e.3) 
                 = (Invalid e.1 e.2 e.3)(Modified I)(Shared);

* PrRd 
PrRd (Invalid I e.1)(Modified e.2)(Shared e.3) 
                 = (Invalid e.1)(Modified )(Shared I e.2 e.3);
* PrT Trivial.
}


Test {
(Invalid e.1)(Modified I e.2)(Shared I e.3) = False;
(Invalid e.1)(Modified I I e.2)(Shared e.3) = False;

(Invalid e.1)(Modified e.2)(Shared e.3) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • invalid ≥ 1, modified = 0, shared = 0
  • The potentially unsafe states:
    • (1) invalid ≥ 0, modified ≥ 1, shared ≥ 1
    (2) invalid ≥ 0, modified ≥ 2, shared ≥ 0
Top Bottom On the encoding Specification Result of supercompilation

Example #3 (MOSI):

/*
  The parameterized MOSI protocol is taken from the Ph.D. dissertation
  "Token Coherence", Page 19, University of Wisconsin, 2003.
  by M.M.K. Martin. 
*/


*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go {e.time (e.i) = <Loop (e.time) (Invalid I e.i)(Modified )(Shared )(Owned ) >;}

Loop {
  () (Invalid e.1)(Modified e.2)(Shared e.3)(Owned e.4) =
             <Test (Invalid e.1)(Modified e.2)(Shared e.3)(Owned e.4)>;
  (s.t e.time) (Invalid e.1)(Modified e.2)(Shared e.3)(Owned e.4) = 
         <Loop (e.time) 
             <RandomAction s.t
               (Invalid e.1)(Modified e.2)(Shared e.3)(Owned e.4)>>;
}


RandomAction {
* rh Trivial 
* rm
rm (Invalid I e.1) (Modified e.2) (Shared e.3) (Owned e.4)
   = (Invalid e.1) (Modified ) (Shared I e.3)(Owned e.2 e.4);
* write
wO (Invalid e.1)(Modified e.2)(Shared e.3)(Owned I e.4) =
   (Invalid e.4 e.3 e.2 e.1)(Modified  I)(Shared )(Owned );

wI (Invalid I e.1)(Modified e.2)(Shared e.3)(Owned e.4) =
   (Invalid e.4 e.3 e.2 e.1)(Modified  I)(Shared )(Owned );

wS (Invalid e.1)(Modified e.2)(Shared I e.3)(Owned e.4) =
   (Invalid e.4 e.3 e.2 e.1)(Modified  I)(Shared )(Owned );

* silent_evict
se (Invalid e.1)(Modified e.2)(Shared I e.3)(Owned e.4) =
   (Invalid I e.1)(Modified  e.2)(Shared e.3)(Owned e.4);
* write_back
wbM (Invalid e.1)(Modified I e.2)(Shared e.3)(Owned e.4) =
    (Invalid I e.1)(Modified  e.2)(Shared e.3)(Owned e.4);

wbO (Invalid e.1)(Modified e.2)(Shared e.3)(Owned I e.4) =
    (Invalid I e.1)(Modified  e.2)(Shared e.3)(Owned e.4);
}


Test {
(Invalid e.1)(Modified I I e.2)(Shared e.3)(Owned e.4) = False;

(Invalid e.1)(Modified e.2)(Shared e.3)(Owned I I e.4) = False;

(Invalid e.1)(Modified I e.2)(Shared I e.3)(Owned e.4) = False;

(Invalid e.1)(Modified e.2)(Shared e.3)(Owned e.4) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • invalid ≥ 1, owned = 0, shared = 0, modified = 0
  • The potentially unsafe states:
    • (1) invalid ≥ 0, shared ≥ 0, owned ≥ 2, modified ≥ 0
    (2) invalid ≥ 0, shared ≥ 0, owned ≥ 0, modified ≥ 2
    (3) invalid ≥ 0, shared ≥ 1, owned ≥ 0, modified ≥ 1
Top Bottom On the encoding Specification Result of supercompilation

Example #4 (MESI):

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go {e.time (e.i) = <Loop (e.time) (Invalid I e.i)(Modified )(Shared )(Exclusive ) >;}

Loop {
  () (Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive e.4) =
             <Test (Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive e.4)>;
  (s.t e.time) (Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive e.4) = 
         <Loop (e.time) 
             <RandomAction s.t
               (Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive e.4)>>;
}


RandomAction {
* rh Trivial 
* rm
rm (Invalid I e.1) (Modified e.2) (Shared e.3) (Exclusive e.4)
   = (Invalid e.1)  (Modified )  (Shared I e.2 e.3 e.4 ) (Exclusive );
* wh1 Trivial
*wh2
wh2 (Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive I e.4) =
  (Invalid e.1)(Modified I e.2)(Shared e.3)(Exclusive e.4);
* wh3 
wh3 (Invalid e.1)(Modified e.2)(Shared I e.3)(Exclusive e.4) =
  (Invalid e.1 e.2 e.3 e.4)(Modified  )(Shared )(Exclusive I);
* wm  
wm (Invalid I e.1)(Modified e.2)(Shared e.3)(Exclusive e.4) =
  (Invalid e.1 e.2 e.3 e.4)(Modified  )(Shared )(Exclusive I);
}


Test {
(Invalid e.1)(Modified I e.2)(Shared I e.3)(Exclusive e.4) = False;
(Invalid e.1)(Modified I I e.2)(Shared e.3)(Exclusive e.4) = False;

(Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive e.4) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • invalid ≥ 1, exclusive = 0, shared = 0, modified = 0
  • The potentially unsafe states:
    • (1) invalid ≥ 0, exclusive ≥ 0, shared ≥ 1, modified ≥ 1
    (2) invalid ≥ 0, exclusive ≥ 0, shared ≥ 0, modified ≥ 2
Top Bottom On the encoding Specification Result of supercompilation

Example #5 (MOESI):

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go {
  e.time (e.i) 
     = <Loop (e.time) (Invalid I e.i)(Modified )(Shared )(Exclusive )(Owned ) >;
}

Loop {
  () (Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive e.4)(Owned e.5)=
             <Test (Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive e.4)(Owned e.5)>;
  (s.t e.time) (Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive e.4)(Owned e.5) = 
         <Loop (e.time) 
               <RandomAction s.t
                   (Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive e.4)(Owned e.5)>>;
}


RandomAction {
* rh Trivial 
* rm
rm (Invalid I e.1) (Modified e.2) (Shared e.3) (Exclusive e.4)(Owned e.5)
       = (Invalid e.1) (Modified ) (Shared I e.3 e.4 )(Exclusive )(Owned e.2 e.5);
* wh1 Trivial
* wh2
wh2 (Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive I e.4)(Owned e.5) 
       = (Invalid e.1)(Modified I e.2)(Shared e.3)(Exclusive e.4)(Owned e.5);
* wh3 
wh3A (Invalid e.1)(Modified e.2)(Shared I e.3)(Exclusive e.4)(Owned e.5)
       = (Invalid e.5 e.4 e.3 e.2 e.1)(Modified  )(Shared )(Exclusive I)(Owned );
wh3B (Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive e.4)(Owned I e.5) 
       = (Invalid e.5 e.4 e.3 e.2 e.1)(Modified  )(Shared )(Exclusive I)(Owned );

* wm  
wm (Invalid I e.1)(Modified e.2)(Shared e.3)(Exclusive e.4)(Owned e.5) 
       = (Invalid e.5 e.4 e.3 e.2 e.1)(Modified  )(Shared )(Exclusive I)(Owned );
}


Test {
* (1)
(Invalid e.1)(Modified I e.2)(Shared I e.3)(Exclusive e.4)(Owned e.5) = False;
(Invalid e.1)(Modified I e.2)(Shared e.3)(Exclusive I e.4)(Owned e.5) = False;
(Invalid e.1)(Modified I e.2)(Shared e.3)(Exclusive e.4)(Owned I e.5) = False;

* (2)
(Invalid e.1)(Modified e.2)(Shared I e.3)(Exclusive I e.4)(Owned e.5) = False;
(Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive I e.4)(Owned I e.5) = False;

* (3)
(Invalid e.1)(Modified I I e.2)(Shared e.3)(Exclusive e.4)(Owned e.5) = False;

* (4)
(Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive I I e.4)(Owned e.5) = False;

(Invalid e.1)(Modified e.2)(Shared e.3)(Exclusive e.4)(Owned e.5) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • invalid ≥ 1, exclusive = 0, shared = 0, modified = 0, owned = 0
  • The potentially unsafe states:
    • (1) exclusive + shared + owned ≥ 1, modified ≥ 1
    (2) exclusive ≥ 1, shared + owned ≥ 1
    (3) modified ≥ 2
    (4) exclusive ≥ 2
Top Bottom On the encoding Specification Result of supercompilation

Example #6 (The University of Illinois):

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;

$ENTRY Go {e.time (e.i) = <Loop (e.time) (Invalid I e.i)(Dirty )(Shared )(Exclusive )>; }

Loop {
  () (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) =
             <Test (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4)>;
  (s.t e.time) (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) = 
         <Loop (e.time) 
               <RandomAction s.t
                    (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4)>>;
}

RandomAction {
* r1 Trivial 
* r2
r2 (Invalid I e.1) (Dirty ) (Shared ) (Exclusive)
       = (Invalid e.1)  (Dirty )  (Shared ) (Exclusive I);
* r3
r3 (Invalid I e.1)(Dirty I e.2)(Shared e.3)(Exclusive e.4) 
       = (Invalid e.1)(Dirty e.2)(Shared I I e.3)(Exclusive e.4);
* r4 
r4A (Invalid I e.1)(Dirty e.2)(Shared I e.3)(Exclusive e.4) 
       = (Invalid e.1)(Dirty e.2)(Shared I e.4 I e.3)(Exclusive);
r4B (Invalid I e.1)(Dirty e.2)(Shared e.3)(Exclusive I e.4) 
       = (Invalid e.1)(Dirty e.2)(Shared I I e.4 e.3)(Exclusive);

* r5 Trivial 
* r6 
r6 (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive I e.4) 
       = (Invalid e.1)(Dirty I e.2)(Shared e.3)(Exclusive e.4);
* r7
r7 (Invalid e.1)(Dirty e.2)(Shared I e.3)(Exclusive e.4)  
       = (Invalid e.1 e.3)(Dirty I e.2)(Shared )(Exclusive e.4);
* r8 
r8 (Invalid I e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4)
       = (Invalid  e.4 e.3 e.2 e.1)(Dirty I)(Shared )(Exclusive );
* r9 
r9 (Invalid e.1)(Dirty I e.2)(Shared e.3)(Exclusive e.4) 
       = (Invalid I e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4);
* r10
r10 (Invalid e.1)(Dirty e.2)(Shared I e.3)(Exclusive e.4)
       = (Invalid I e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4);
* r11 
r11 (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive I e.4) 
       = (Invalid I e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4); 
}

Test {
(Invalid e.1)(Dirty I e.2)(Shared I e.3)(Exclusive e.4) = False;
(Invalid e.1)(Dirty I I e.2)(Shared e.3)(Exclusive e.4) = False;

(Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • invalid ≥ 1, exclusive = 0, dirty = 0, shared = 0
  • The potentially unsafe states:
    • (1) invalid ≥ 0, exclusive ≥ 0, dirty ≥ 1, shared ≥ 1
    (2) invalid ≥ 0, exclusive ≥ 0, dirty ≥ 2, shared ≥ 0
Top Bottom On the encoding Specification Result of supercompilation

Example #7 (Berkley):

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;

$ENTRY Go {
 e.time (e.i) = <Loop (e.time) (Invalid I e.i)(Non-exclusive )(Exclusive )(Unowned )>;
}

Loop {
  () (Invalid e.1)(Non-exclusive e.2)(Exclusive e.3)(Unowned e.4) =
             <Test (Invalid e.1)(Non-exclusive e.2)(Exclusive e.3)(Unowned e.4)>;
  (s.t e.time) (Invalid e.1)(Non-exclusive e.2)(Exclusive e.3)(Unowned e.4) = 
         <Loop (e.time) 
               <RandomAction s.t
                         (Invalid e.1)(Non-exclusive e.2)(Exclusive e.3)(Unowned e.4)>>;
}


RandomAction {

* rm
rm (Invalid I e.1) (Non-exclusive e.2) (Exclusive e.3) (Unowned e.4)
       = (Invalid e.1) (Non-exclusive e.3 e.2) (Exclusive )(Unowned I e.4);
* rh Trivial
* wm
wm (Invalid I e.1)(Non-exclusive e.2)(Exclusive e.3)(Unowned e.4) 
       = (Invalid e.4 e.3 e.2 e.1)(Non-exclusive )(Exclusive I)(Unowned );
* wh1
wh1A (Invalid e.1)(Non-exclusive I e.2)(Exclusive e.3)(Unowned e.4) 
       = (Invalid e.4 e.2 e.1)(Non-exclusive )(Exclusive I e.3)(Unowned );
wh1B (Invalid e.1)(Non-exclusive e.2)(Exclusive e.3)(Unowned I e.4) 
       = (Invalid e.4 e.2 e.1 )(Non-exclusive )(Exclusive I e.3)(Unowned );

* wh2 Trivial
}


Test {
* (1)
(Invalid e.1)(Non-exclusive e.2)(Exclusive I  e.3)(Unowned I e.4) = False;
(Invalid e.1)(Non-exclusive I e.2 )(Exclusive I e.3)(Unowned e.4) = False;
* (2)
(Invalid e.1)(Non-exclusive e.2 )(Exclusive I I e.3)(Unowned e.4) = False;

(Invalid e.1)(Non-exclusive e.2)(Exclusive e.3)(Unowned e.4) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • invalid ≥ 1, non_exclusive = 0, unowned = 0, exclusive = 0
  • The potentially unsafe states:
    • (1) exclusive ≥ 1, unowned + non_exclusive ≥ 1
    (2) exclusive ≥ 2
Top Bottom On the encoding Specification Result of supercompilation

Example #8 (DEC Firefly):

* DEC firefly cache coherence protocol
*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;

$ENTRY Go {
  e.time (e.i) = <Loop (e.time) (Invalid I e.i)(Dirty )(Shared )(Exclusive )>;
}

Loop {
  () (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) =
             <Test (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4)>;
  (s.t e.time) (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) = 
         <Loop (e.time) 
               <RandomAction s.t
                   (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4)>>;
}


RandomAction {
* rh Trivial 
* rm_1
rm_1 (Invalid I e.1) (Dirty ) (Shared ) (Exclusive )
     = (Invalid e.1)  (Dirty )  (Shared ) (Exclusive I);
* 
* rm_2
rm_2 (Invalid I e.1)(Dirty I e.2)(Shared e.3)(Exclusive e.4) 
     = (Invalid e.1)(Dirty e.2)(Shared I I e.3)(Exclusive e.4);
* rm_3 
rm_3A (Invalid I e.1)(Dirty e.2)(Shared I e.3)(Exclusive e.4) 
     = (Invalid e.1)(Dirty e.2)(Shared I e.4 I e.3)(Exclusive );
rm_3B (Invalid I e.1)(Dirty e.2)(Shared e.3)(Exclusive I e.4) 
     = (Invalid e.1)(Dirty e.2)(Shared I I e.4 e.3)(Exclusive );

* wh_1 Trivial

* wh_2 
wh_2 (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive I e.4) 
     = (Invalid e.1)(Dirty I e.2)(Shared e.3)(Exclusive e.4);

* wh_3 
wh_3 (Invalid e.1)(Dirty e.2)(Shared I)(Exclusive e.4) 
     = (Invalid e.1)(Dirty e.2)(Shared )(Exclusive I e.4);

* wh_4 Trivial
* wm 
wm (Invalid I e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) 
     = (Invalid e.4 e.3 e.2 e.1)(Dirty I)(Shared )(Exclusive );
}


Test {
* (1)
(Invalid e.1)(Dirty I e.2)(Shared I e.3)(Exclusive e.4) = False;
(Invalid e.1)(Dirty I e.2)(Shared e.3)(Exclusive I e.4) = False;
* (2)
(Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive I I e.4) = False;
* (3)
(Invalid e.1)(Dirty I I e.2)(Shared e.3)(Exclusive e.4) = False;

(Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • invalid ≥ 1, exclusive = 0, shared = 0, dirty = 0
  • The potentially unsafe states:
    • (1) dirty ≥ 1, shared + exclusive ≥ 1
    (2) exclusive ≥ 2
    (3) dirty ≥ 2
Top Bottom On the encoding Specification Result of supercompilation

Example #9 (IEEE Futurebus+):

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go {
  e.time (e.p) = 
     <Loop (e.time) (invalid I e.p)(sharedU )(exclusiveU )(exclusiveM )
                    (pendingR )(pendingW )(pendingEMR )(pendingEMW )(pendingSU )>;
}

Loop {
  () (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
     (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9) =
         <Test (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
               (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9)>;

  (s.t e.time) (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
               (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9) = 
         <Loop (e.time) 
               <RandomAction s.t
                     (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
                     (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9)>>;
}


RandomAction {
* r1 Trivial
* r2
r2 (invalid I e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
                  (pendingW )(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9)
     = (invalid e.1)(sharedU )(exclusiveU )(exclusiveM )(pendingR I e.5)
       (pendingW )(pendingEMR e.7 e.4)(pendingEMW e.8)(pendingSU e.2 e.3 e.9);

* r3 
r3 (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
                (pendingW e.6)(pendingEMR I e.7)(pendingEMW e.8)(pendingSU e.9)
     = (invalid e.1)(sharedU I e.2 e.5)(exclusiveU e.3)(exclusiveM e.4)(pendingR )
       (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9);

* r4
r4 (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
                (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU I e.9)
     = (invalid e.1)(sharedU e.2 e.5 I e.9)(exclusiveU e.3)(exclusiveM e.4)(pendingR )
       (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU );

* r5
r5 (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR I I e.5)
                (pendingW e.6)(pendingEMR )(pendingEMW e.8)(pendingSU ) 
     = (invalid e.1)(sharedU I I e.5 e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR )
       (pendingW e.6)(pendingEMR )(pendingEMW e.8)(pendingSU );

* r6 
r6 (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR I)
                (pendingW e.6)(pendingEMR )(pendingEMW e.8)(pendingSU ) 
     = (invalid e.1)(sharedU e.2)(exclusiveU I e.3)(exclusiveM e.4)(pendingR )
       (pendingW e.6)(pendingEMR )(pendingEMW e.8)(pendingSU );

* wm1 
wm1 (invalid I e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
                   (pendingW )(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9)
     = (invalid e.1 e.3 e.2 e.9 e.5 e.7)(sharedU )(exclusiveU )(exclusiveM )(pendingR )
       (pendingW I)(pendingEMR )(pendingEMW e.4 e.8)(pendingSU );

* wm2
wm2 (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
                 (pendingW e.6)(pendingEMR e.7)(pendingEMW I e.8)(pendingSU e.9) 
     = (invalid I e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.6 e.4)(pendingR e.5)
       (pendingW )(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9); 

* wm3
wm3 (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
                 (pendingW e.6)(pendingEMR e.7)(pendingEMW )(pendingSU e.9) 
       = (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.6 e.4)(pendingR e.5)
         (pendingW )(pendingEMR e.7)(pendingEMW )(pendingSU e.9);  

* wh1 Trivial
* wh2
wh2 (invalid e.1)(sharedU e.2)(exclusiveU I e.3)(exclusiveM e.4)(pendingR e.5)
                 (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9) 
       = (invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM I e.4)(pendingR e.5)
         (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9);

* wh3
wh3 (invalid e.1)(sharedU I e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
                 (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9)
       = (invalid e.2 e.1)(sharedU )(exclusiveU e.3)(exclusiveM I e.4)(pendingR e.5)
         (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9);
}


Test {
* (1)
(invalid e.1)(sharedU I e.2)(exclusiveU I e.3)(exclusiveM e.4)(pendingR e.5)
             (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9) = False;
(invalid e.1)(sharedU I e.2)(exclusiveU e.3)(exclusiveM I e.4)(pendingR e.5)
             (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9) = False; 
* (2)
(invalid e.1)(sharedU e.2)(exclusiveU I I e.3)(exclusiveM e.4)(pendingR e.5)
             (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9) = False;
(invalid e.1)(sharedU e.2)(exclusiveU I e.3)(exclusiveM I e.4)(pendingR e.5)
             (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9) = False;
(invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM I I e.4)(pendingR e.5)
             (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9) = False;
* (3)
(invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR I e.5)
             (pendingW I e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9) = False;
* (4)
(invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
             (pendingW I I e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9) = False;

(invalid e.1)(sharedU e.2)(exclusiveU e.3)(exclusiveM e.4)(pendingR e.5)
             (pendingW e.6)(pendingEMR e.7)(pendingEMW e.8)(pendingSU e.9) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • invalid ≥ 1, sharedU = 0, exclusiveU = 0, exclusiveM = 0,
    pendingR = 0, pendingW = 0, pendingEMR = 0, pendingEMW = 0, pendingSU = 0
  • The potentially unsafe states:
    • (1) sharedU ≥ 1, exclusiveU + exclusiveM ≥ 1
    (2) exclusiveU + exclusiveM ≥ 2
    (3) pendingR ≥ 1, pendingW ≥ 1
    (4) pendingW ≥ 2

Example #10 (Xerox PARC Dragon):

(A) An incorrect specification given by G. Delzanno in [2].

Top Bottom On the encoding Specification Result of supercompilation 
* Xerox PARC Dragon protocol.
*** "Automatic Verification of Parametrized Cache Coherence Protocols."
***  by Georgio Delzanno, DISI - University of Genova.
**!!! 
**!!! The specification of the protocol given by G. Delzanno is invalid!.
**!!! The fact was established on the base of analyzing of the residual program 
**!!! constructed by SCP4. (We supercompiled the invalid version of the protocol.)
**!!! It is easy to recognize an unsafed test in the residual program 
**!!! constructed by SCP4. The test is given below (see the comment - "The unsafed test").

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;

/* 
* A usafed test for the variant of the Xerox PARC Dragon protocol given by G. Delzanno.
* Just 1) uncomment the following entry point;
*      2) comment the second entry point;
*      3) compile the program and launch it.
* The usafed test is 
*   time = wm1 wm2C wh3
*   invalid = I I I
* All other variables are zero.
$ENTRY Go {
  = <Prout <Loop (wm1 wm2C wh3) (invalid I I I)(shared_clean )(shared_dirty )(dirty )(exclusive )>>;
}
*/

*/*
$ENTRY Go { e.time (e.i) 
  = <Loop (e.time) (invalid I e.i)(shared_clean )(shared_dirty )(dirty )(exclusive )>;
}
*/

Loop {
  () (invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5)
      = <Test (invalid e.1)(shared_clean e.2)
                (shared_dirty e.3)(dirty e.4)(exclusive e.5)>;
  (s.t e.time) 
     (invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5) 
      =  <Loop (e.time) 
           <RandomAction s.t
             (invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5)
         >>;
}


RandomAction {
* rh Trivial 
* rm1
 rm1 (invalid I e.1)(shared_clean )(shared_dirty )(dirty )(exclusive )
       = (invalid e.1)(shared_clean )(shared_dirty )(dirty )(exclusive I);

* rm2
 rm2A (invalid I e.1)(shared_clean I e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean I e.5 I e.2)
         (shared_dirty e.4 e.3)(dirty )(exclusive );
 rm2B (invalid I e.1)(shared_clean e.2)(shared_dirty I e.3)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean I e.5 e.2)
         (shared_dirty e.4 I e.3)(dirty )(exclusive );
 rm2C (invalid I e.1)(shared_clean e.2)(shared_dirty e.3)(dirty I e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean I e.5 e.2)
         (shared_dirty I e.4 e.3)(dirty )(exclusive );
 rm2D (invalid I e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive I e.5)
       = (invalid e.1)(shared_clean I I e.5 e.2)
         (shared_dirty e.4 e.3)(dirty )(exclusive );

* wm1 
 wm1 (invalid I e.1)(shared_clean )(shared_dirty )(dirty )(exclusive )
       = (invalid e.1)(shared_clean )(shared_dirty )(dirty I)(exclusive );

* wm2 
* shared_clean + shared_dirty + dirty + exclusive >= 1
 wm2A (invalid I e.1)(shared_clean I e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean e.3 e.5 I e.2)
         (shared_dirty I)(dirty e.4)(exclusive );
 wm2B (invalid I e.1)(shared_clean e.2)(shared_dirty I e.3)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean I e.3 e.5 e.2)
         (shared_dirty I)(dirty e.4)(exclusive );
 wm2C (invalid I e.1)(shared_clean e.2)(shared_dirty e.3)(dirty I e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean e.3 e.5 e.2)
         (shared_dirty I)(dirty I e.4)(exclusive );
 wm2D (invalid I e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive I e.5)
       = (invalid e.1)(shared_clean e.3 I e.5 e.2)
         (shared_dirty I)(dirty e.4)(exclusive );

* wh1 Trivial 
* wh2 
 wh2 (invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive I e.5)
       = (invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty I e.4)(exclusive e.5);

* wh3 
 wh3 (invalid e.1)(shared_clean )(shared_dirty I)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean )(shared_dirty )(dirty I e.4)(exclusive e.5);

* wh4 
 wh4 (invalid e.1)(shared_clean I)(shared_dirty )(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean )(shared_dirty )(dirty I e.4)(exclusive e.5);

* wh5 
 wh5A (invalid e.1)(shared_clean I I e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean e.3 I e.2)(shared_dirty I)
         (dirty e.4)(exclusive e.5);

 wh5B (invalid e.1)(shared_clean I e.2)(shared_dirty I e.3)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean e.3 I e.2)(shared_dirty I)
         (dirty e.4)(exclusive e.5);

 wh5C (invalid e.1)(shared_clean e.2)(shared_dirty I I e.3)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean I e.3 e.2)(shared_dirty I)
         (dirty e.4)(exclusive e.5);
}


/* 
 We paint the False cases with the numbers. 
 The aim is to keep (in the residual program) the possible traces of the cases.
*/
Test {
* (3)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)
             (dirty I I e.4)(exclusive e.5) = False3 I I e.4;

* (1)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)
            (dirty I e.4)(exclusive e.5), e.2 e.3 e.5: I e.y = False1;
                                               
* (4)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)
             (dirty e.4)(exclusive I I e.5) = False4;

* (2)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)
             (dirty e.4)(exclusive I e.5), e.2 e.3: I e.y = False2;
                                               
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5) = True;
}                            

/*
* Here is just another variant of the Test definition.
Test {
* (3)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)
             (dirty I I e.4)(exclusive e.5) = False;

* (1)
(invalid e.1)(shared_clean )(shared_dirty )(dirty I e.4)(exclusive ) = True;
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty I e.4)(exclusive e.5) = False;
                                               
* (4)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)
             (dirty e.4)(exclusive I I e.5) = False;

* (2)
(invalid e.1)(shared_clean )(shared_dirty )(dirty e.4)(exclusive I e.5) = True;
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive I e.5) = False;
                                               
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5) = True;
}                            
*/
  • The parameterized  initial  configuration  is  expressed  as:   
    • invalid ≥ 1, shared_clean = 0, shared_dirty = 0, dirty = 0, exclusive = 0
  • The potentially unsafe states:
    • (1) dirty ≥ 1, exclusive + shared_clean + shared_dirty ≥ 1
    (2) exclusive ≥ 1, shared_clean + shared_dirty ≥ 1
    (3) dirty ≥ 2
    (4) exclusive ≥ 2

(B) The correct specification given by G. Delzanno [3].

Top Bottom On the encoding Specification Result of supercompilation Structure of the automatic proof 
* Xerox PARC Dragon protocol.
*** "Automatic Verification of Parametrized Cache Coherence Protocols."
*** Georgio Delzanno, DISI - University of Genova.
**!!!
**!!! The cases wm2_j and wh_i were corrected according to the HyTech code of the protocol.
**!!! A reference to the code is given by G. Delzanno in his paper, 
**!!! where the specification of the protocol is invalid.
**!!! The reference to the following address:
**!!!  http://www.disi.unige.it/person/DelzannoG/protocols.html


*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go { e.time (e.i) 
  = <Loop (e.time) (invalid I e.i)(shared_clean )(shared_dirty )(dirty )(exclusive )>;
}


Loop {
  () (invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5)
      = <Test (invalid e.1)(shared_clean e.2)
                (shared_dirty e.3)(dirty e.4)(exclusive e.5)>;
  (s.t e.time) 
     (invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5) 
      =  <Loop (e.time) 
           <RandomAction s.t
             (invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5)
         >>;
}


RandomAction {
* rh Trivial 
* rm1
 rm1 (invalid I e.1)(shared_clean )(shared_dirty )(dirty )(exclusive )
       = (invalid e.1)(shared_clean )(shared_dirty )(dirty )(exclusive I);

* rm2
 rm2A (invalid I e.1)(shared_clean I e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean I e.5 I e.2)
         (shared_dirty e.4 e.3)(dirty )(exclusive );
 rm2B (invalid I e.1)(shared_clean e.2)(shared_dirty I e.3)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean I e.5 e.2)
         (shared_dirty e.4 I e.3)(dirty )(exclusive );
 rm2C (invalid I e.1)(shared_clean e.2)(shared_dirty e.3)(dirty I e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean I e.5 e.2)
         (shared_dirty I e.4 e.3)(dirty )(exclusive );
 rm2D (invalid I e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive I e.5)
       = (invalid e.1)(shared_clean I I e.5 e.2)
         (shared_dirty e.4 e.3)(dirty )(exclusive );

* wm1 
 wm1 (invalid I e.1)(shared_clean )(shared_dirty )(dirty )(exclusive )
       = (invalid e.1)(shared_clean )(shared_dirty )(dirty I)(exclusive );

* wm2 corrected. 
* shared_clean + shared_dirty + dirty + exclusive >= 1
 wm2A (invalid s.1 e.1)(shared_clean s.2 e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean e.3 e.4 e.5 s.2 e.2)
         (shared_dirty s.1)(dirty )(exclusive );
 wm2B (invalid s.1 e.1)(shared_clean e.2)(shared_dirty s.3 e.3)(dirty e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean s.3 e.3 e.4 e.5 e.2)
         (shared_dirty s.1)(dirty )(exclusive );
 wm2C (invalid s.1 e.1)(shared_clean e.2)(shared_dirty e.3)(dirty s.4 e.4)(exclusive e.5)
       = (invalid e.1)(shared_clean e.3 s.4 e.4 e.5 e.2)
         (shared_dirty s.1)(dirty )(exclusive );
 wm2D (invalid s.1 e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive s.5 e.5)
       = (invalid e.1)(shared_clean e.3 e.4 s.5 e.5 e.2)
         (shared_dirty s.1)(dirty )(exclusive );

* wh-s corrected. 
* wh1 
 wh1 (invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty I e.4)(exclusive e.5)
       = (invalid I e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5);

* wh2 
 wh2 (invalid e.1)(shared_clean I e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5)
       = (invalid I e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5);

* wh3 
 wh3 (invalid e.1)(shared_clean e.2)(shared_dirty I e.3)(dirty e.4)(exclusive e.5)
       = (invalid I e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5);

* wh4 
 wh4 (invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive I e.5)
       = (invalid I e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5);
}

Test {
* (3)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)
             (dirty I I e.4)(exclusive e.5) = False;

* (1)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)
             (dirty I e.4)(exclusive e.5), e.2 e.3 e.5: I e.y = False;
                                               
* (4)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)
             (dirty e.4)(exclusive I I e.5) = False;

* (2)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive I e.5),
        e.2 e.3: I e.y = False;
                                               
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)(sirty e.4)(exclusive e.5) = True;
} 


/*
* Here is just another variant of the Test definition.
Test {
* (3)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)
             (dirty I I e.4)(exclusive e.5) = False;

* (1)
(invalid e.1)(shared_clean )(shared_dirty )(dirty I e.4)(exclusive ) = True;
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty I e.4)(exclusive e.5) = False;
                                               
* (4)
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)
             (dirty e.4)(exclusive I I e.5) = False;

* (2)
(invalid e.1)(shared_clean )(shared_dirty )(dirty e.4)(exclusive I e.5) = True;
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive I e.5) = False;
                                               
(invalid e.1)(shared_clean e.2)(shared_dirty e.3)(dirty e.4)(exclusive e.5) = True;
}                            
*/
  • The parameterized  initial  configuration  is  expressed  as:   
    • invalid ≥ 1, shared_clean = 0, shared_dirty = 0, dirty = 0, exclusive = 0
  • The potentially unsafe states:
    • (1) dirty ≥ 1, exclusive + shared_clean + shared_dirty ≥ 1
    (2) exclusive ≥ 1, shared_clean + shared_dirty ≥ 1
    (3) dirty ≥ 2
    (4) exclusive ≥ 2
Top Bottom On the encoding Specification Result of supercompilation

Example #11 (Java Meta-Locking Algorithm):

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;

trans {
* get_fast
get_fast (obj_trans not_busy) t.race
         (idle I e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait)
     =   (obj_trans (busy)) t.race 
         (idle e.idle) (owner I e.owner) (handin e.handin) (handout e.handout) (wait e.wait);
* put_fast
put_fast (obj_trans (busy)) t.race
         (idle e.idle) (owner I e.owner) (handin e.handin) (handout e.handout) (wait e.wait)
     =   (obj_trans not_busy) t.race
         (idle I e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait);
* get_slow
get_slow (obj_trans (busy e.busy)) t.race
         (idle I e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait)
     =   (obj_trans (busy I e.busy)) t.race
         (idle e.idle) (owner e.owner) (handin I e.handin) (handout e.handout) (wait e.wait);
* put_slow
put_slow (obj_trans (busy I e.busy)) t.race
         (idle e.idle) (owner I e.owner) (handin e.handin) (handout e.handout) (wait e.wait)
     =   (obj_trans (busy e.busy)) t.race
         (idle e.idle) (owner e.owner) (handin e.handin) (handout I e.handout) (wait e.wait);

* request
request  t.obj_trans (race h0)
         (idle e.idle) (owner e.owner) (handin I e.handin) (handout e.handout) (wait e.wait)
      =  t.obj_trans (race h1)
         (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait I e.wait);
request  t.obj_trans (race h2)
         (idle e.idle) (owner e.owner) (handin I e.handin) (handout e.handout) (wait e.wait)
      =  t.obj_trans (race h3)
         (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait I e.wait);

release  t.obj_trans (race h0)
         (idle e.idle) (owner e.owner) (handin e.handin) (handout I e.handout) (wait e.wait)
      =  t.obj_trans (race h2)
         (idle I e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait);
release  t.obj_trans (race h1)
         (idle e.idle) (owner e.owner) (handin e.handin) (handout I e.handout) (wait e.wait)
      =  t.obj_trans (race h3)
         (idle I e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait);

* go
go  t.obj_trans (race h3)
         (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait I e.wait)
      =  t.obj_trans (race h3)
         (idle e.idle) (owner I e.owner) (handin e.handin) (handout e.handout) (wait e.wait);

/* 
  Here we encode unchangable states of the protocol in another way than in the other protocols.
  The reason is: just to make the things more interesting.
*/
s.act  t.obj_trans t.race
         t.idle t.owner t.handin t.handout t.wait
      =  t.obj_trans t.race
         t.idle t.owner t.handin t.handout t.wait;
}

$ENTRY Go {
 e.time (e.threads) 
    = <Loop (e.time) (obj_trans not_busy) (race h0)
                      (idle e.threads) (owner) (handin) (handout) (wait) 
      >;
}

Loop {
  () (obj_trans e.busy) t.race
     (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait)
        =  <Test (obj_trans e.busy) t.race
                    (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait)>;

  (s.t e.time) (obj_trans e.busy) t.race
            (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait) = 
         <Loop (e.time) 
         <trans s.time (obj_trans e.busy) t.race
         (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait)>>;
}

Test {
 (obj_trans e.busy) t.race
 (idle e.idle) (owner s.1 s.2 e.owner) (handin e.handin) (handout e.handout) (wait e.wait) = False; 
 (obj_trans e.busy) t.race
 (idle e.idle) (owner e.owner) (handin e.handin) (handout s.1 s.2 e.handout) (wait e.wait) = False; 
 (obj_trans e.busy) t.race
 (idle e.idle) (owner s.1 e.owner) (handin e.handin) (handout s.2 e.handout) (wait e.wait) = False; 

 (obj_trans e.busy) t.race
 (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait) = True; 
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • obj_trans_not_busy = TRUE, race = H0,
    idle ≥ 0, owner = 0, handin = 0, handout = 0, wait = 0
  • The potentially unsafe states:
    • (1) owner + handout ≥ 2
Top Bottom On the encoding Specification Result of supercompilation

Example #12 (Reader-Writer protocol):

* Reader-Writer mutual exclusion protocol from the paper 
* "Petri Nets, Flat Languages and Linear Arithmetic", by Laurent Fribourg
* 
*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go { e.time (e.q) = <Loop (e.time) (x2 I)(x3)(x4)(x5 e.q)(x6)(x7)>; }

Loop {
  () (x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7) =
         <Test (x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7)>;
  (s.t e.time) (x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7) =
         <Loop (e.time) 
           <RandomAction s.t
                 (x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7)>>;
}


RandomAction {
*r1
r1 (x2 I e.2)(x3 e.3)(x4)(x5 e.5)(x6 e.6)(x7 I e.7)
   = (x2 e.2)(x3 I e.3)(x4)(x5 e.5)(x6 e.6)(x7 e.7);

*r2
r2 (x2 I e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 I e.6)(x7 e.7)
   = (x2 I e.2)(x3 e.3)(x4 I e.4)(x5 e.5)(x6 e.6)(x7 e.7);
   
*r3
r3 (x2 e.2)(x3 I e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7)
   = (x2 I e.2)(x3 e.3)(x4 e.4)(x5 I e.5)(x6 e.6)(x7 e.7);
*r4
r4 (x2 e.2)(x3 e.3)(x4 I e.4)(x5 e.5)(x6 e.6)(x7 e.7)
   = (x2 e.2)(x3 e.3)(x4 e.4)(x5 I e.5)(x6 e.6)(x7 e.7);

*r5
r5 (x2 e.2)(x3 e.3)(x4 e.4)(x5 I e.5)(x6 e.6)(x7 e.7)
   = (x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 I e.6)(x7 e.7);

*r6
r6 (x2 e.2)(x3 e.3)(x4 e.4)(x5 I e.5)(x6 e.6)(x7 e.7)
   = (x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 I e.7);
}


Test {
(x2 e.2)(x3 I e.3)(x4 I e.4)(x5 e.5)(x6 e.6)(x7 e.7) = False;

(x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7)= True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • x2 = 1, x3 = 0, x4 = 0, x5 ≥ 0, x6 = 0, x7 = 0
  • The potentially unsafe states:
    • (1) x3 ≥ 1, x4 ≥ 1

Example #13 (Steve German's directory-based consistency protocol):

Model I

Top Bottom On the encoding Specification Result of supercompilation 
/*
 Encoding a client-server protocol after 
"Constraint-based Verification of Client-Server Protocols"
 by G. Delzanno and T. Bultan

 Model I
*/

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go { 
 e.time (e.n) 
    = <Loop (e.time) (Server Idle No) 
                  (Null I e.n) (WaitS ) (Shared ) (WaitE ) (Exclusive )
      >;
}

Loop {
  () (Server e.serv)
     (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5) =
             <Test (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)>;

  (s.t e.time) (Server e.serv)
     (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5) =
         <Loop (e.time) 
                <RandomAction s.t (Server e.serv)
                       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)>>;
}



RandomAction {
*1. reqS
reqS (Server Idle s.bool) 
     (Null I e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server ServS s.bool) 
               (Null e.1) (WaitS I e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);
*2. reqE1
reqE1 (Server Idle s.bool) 
      (Null I e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server ServE s.bool) 
               (Null e.1) (WaitS e.2) (Shared e.3) (WaitE I e.4) (Exclusive e.5);

*3. reqE2
reqE2 (Server Idle s.bool) 
      (Null e.1) (WaitS e.2) (Shared I e.3) (WaitE e.4) (Exclusive e.5)
             = (Server ServE s.bool) 
               (Null e.1) (WaitS e.2) (Shared e.3) (WaitE I e.4) (Exclusive e.5);

*4. inv
inv   (Server ServS Yes) 
      (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive I e.5)
             = (Server GrantS No) 
               (Null I e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);

*5. nonex1
nonex1 (Server ServS No) 
       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server GrantS No) 
               (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);

*6. invS
invS   (Server ServE s.bool) 
       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server InvE s.bool) 
               (Null e.1 e.3) (WaitS e.2) (Shared ) (WaitE e.4) (Exclusive e.5);

*7. invE
invE   (Server InvE Yes) 
       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive I e.5)
             = (Server GrantE No) 
               (Null I e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);

*8. nonex2
nonex2 (Server InvE No) 
       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server GrantE No) 
               (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);

*9. grantS
grantS (Server GrantS s.bool) 
       (Null e.1) (WaitS I e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server Idle s.bool) 
               (Null e.1) (WaitS e.2) (Shared I e.3) (WaitE e.4) (Exclusive e.5);

*10. grantE
grantE (Server GrantE s.bool) 
       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE I e.4) (Exclusive e.5)
             = (Server Idle Yes) 
               (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive I e.5);

*11. servG
servG   (Server ServE s.bool) 
       (Null e.1) (WaitS e.2) (Shared ) (WaitE e.4) (Exclusive )
             = (Server GrantE s.bool) 
               (Null e.1) (WaitS e.2) (Shared ) (WaitE e.4) (Exclusive );

*12. ee1
ee1   (Server ServE s.bool) 
       (Null e.1) (WaitS e.2) (Shared I e.3) (WaitE e.4) (Exclusive e.5)
             = (Server ServE s.bool) 
               (Null I e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);

*13. ee2
ee2   (Server ServE s.bool) 
       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive I e.5)
             = (Server ServE No) 
               (Null I e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);
}


Test {
(Null e.1) (WaitS e.2) (Shared I e.3) (WaitE e.4) (Exclusive I e.5) = False;
(Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive I I e.5) = False;

(Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • server = IDLE, bool = NO,
    null ≥ 1, wait_s = 0, shared = 0, wait_e = 0, exclusive = 0
  • The potentially unsafe states:
    • (1) shared ≥ 1, exclusive ≥ 1
    (2) exclusive ≥ 2

Model B

Top Bottom On the encoding Specification Result of supercompilation 
/*
 Encoding a client-server protocol after 
"Constraint-based Verification of Client-Server Protocols"
 by G. Delzanno and T. Bultan

 Model B
*/

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go { 
 e.time (e.n) 
    = <Loop (e.time) (Server Idle No) 
                     (Null I e.n) (WaitS ) (Shared ) (WaitE ) (Exclusive )
      >;
}

Loop {
  () (Server e.serv)
     (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5) =
             <Test (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)>;

  (s.t e.time) (Server e.serv)
     (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5) =
         <Loop (e.time) 
               <RandomAction s.t (Server e.serv)
                       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)>>;
}



RandomAction {
*1. reqS
reqS (Server Idle s.bool) 
     (Null I e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server ServS s.bool) 
               (Null e.1) (WaitS I e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);
*2. reqE1
reqE1 (Server Idle s.bool) 
      (Null I e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server ServE s.bool) 
               (Null e.1) (WaitS e.2) (Shared e.3) (WaitE I e.4) (Exclusive e.5);

*3. reqE2
reqE2 (Server Idle s.bool) 
      (Null e.1) (WaitS e.2) (Shared I e.3) (WaitE e.4) (Exclusive e.5)
             = (Server ServE s.bool) 
               (Null e.1) (WaitS e.2) (Shared e.3) (WaitE I e.4) (Exclusive e.5);

*4. inv
inv   (Server ServS Yes) 
      (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive I e.5)
             = (Server GrantS No) 
               (Null I e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);

*5. nonex1
nonex1 (Server ServS No) 
       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server GrantS No) 
               (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);

*6. invS
invS   (Server ServE s.bool) 
       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server InvE s.bool) 
               (Null e.1 e.3) (WaitS e.2) (Shared ) (WaitE e.4) (Exclusive e.5);

*7. invE
invE   (Server InvE Yes) 
       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive I e.5)
             = (Server GrantE No) 
               (Null I e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);

*8. nonex2
nonex2 (Server InvE No) 
       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server GrantE No) 
               (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5);

*9. grantS
grantS (Server GrantS s.bool) 
       (Null e.1) (WaitS I e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5)
             = (Server Idle s.bool) 
               (Null e.1) (WaitS e.2) (Shared I e.3) (WaitE e.4) (Exclusive e.5);

*10. grantE
grantE (Server GrantE s.bool) 
       (Null e.1) (WaitS e.2) (Shared e.3) (WaitE I e.4) (Exclusive e.5)
             = (Server Idle Yes) 
               (Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive I e.5);
}


Test {
(Null e.1) (WaitS e.2) (Shared I e.3) (WaitE e.4) (Exclusive I e.5) = False;
(Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive I I e.5) = False;

(Null e.1) (WaitS e.2) (Shared e.3) (WaitE e.4) (Exclusive e.5) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • server = IDLE, bool = NO,
    null ≥ 1, wait_s = 0, shared = 0, wait_e = 0, exclusive = 0
  • The potentially unsafe states:
    • (1) shared ≥ 1, exclusive ≥ 1
    (2) exclusive ≥ 2
Top Bottom On the encoding Specification Result of supercompilation

Example #14 (Load Balancing Monitor protocol):

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go {
 e.time (e.req) = <Loop (e.time) (idle I)(busy )(req e.req)(use )(high )(low )>;
}

Loop {
  () (idle e.1)(busy e.2)(req e.3)(use e.4)(high e.5)(low e.6) =
         <Test (idle e.1)(busy e.2)(req e.3)(use e.4)(high e.5)(low e.6)>;
  (t.t e.time) (idle e.1)(busy e.2)(req e.3)(use e.4)(high e.5)(low e.6) = 
         <Loop (e.time) 
            <RandomAction t.t (idle e.1)(busy e.2)(req e.3)(use e.4)(high e.5)(low e.6)>>;
}


RandomAction {
* r1
(r1) (idle I e.1)(busy e.2)(req I e.3)(use e.4)(high e.5)(low e.6)
   = (idle I e.1)(busy e.2)(req e.3)(use I e.4)(high e.5)(low e.6);
* r2
(r2) (idle I e.1)(busy e.2)(req e.3)(use I e.4)(high e.5)(low e.6)
   = (idle I e.1)(busy e.2)(req I e.3)(use e.4)(high e.5)(low e.6);
* r3 
(r3  e.r3) 
     (idle I e.1)(busy e.2)(req e.3)(use e.4)(high e.5)(low e.6)
   = (idle e.1)(busy I e.2) 
     <RandomDistribution (r3  (low_use e.4 e.6) e.r3) 
                         (req e.3)(use )(high e.5)(low e.6)>;
* r4 
(r4) (idle e.1)(busy I e.2)(req e.3)(use e.4)(high e.5)(low e.6)
   = (idle I e.1)(busy e.2)(req e.3 e.6)(use e.4 e.5)(high )(low );
}

RandomDistribution {
* r3 
(r3  (low_use I e.lu) (high_low I e.hl)) 
     (req e.3)(use e.4)(high e.5)(low e.6)
   = <RandomDistribution (r3  (low_use e.lu) (high_low e.hl))
                         (req e.3)(use e.4)(high I e.5)(low e.6)>;

(r3  (low_use e.lu) (high_low )) 
     (req e.3)(use e.4)(high e.5)(low e.6)
   = (req e.3)(use e.4)(high e.5)(low e.lu e.6);

(r3  (low_use ) (high_low e.hl)) 
     (req e.3)(use e.4)(high e.5)(low e.6)
   = (req e.3)(use e.4)(high e.5)(low e.6);
}


Test {
(idle e.1)(busy I e.2)(req e.3)(use I e.4)(high e.5)(low e.6) = False;

(idle e.1)(busy e.2)(req e.3)(use e.4)(high e.5)(low e.6) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • idle = 1, busy = 0, req ≥ 0, use = 0, high = 0, low = 0
  • The potentially unsafe states:
    • (1) busy ≥ 1, use ≥ 1
Top Bottom On the encoding Specification Result of supercompilation

Example #15 (Data Race Free Synchronization Model):

/*
  Data Race Free Synchronization Model.
  http://www.disi.unige.it/person/DelzannoG/ParameterizedSystems/drf.html
  after F.Pong and M. Dubois
  "Formal Verification of Delayed Consistency Protocols", IPPS96.
*/

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go {
 e.time (e.out) = <Loop (e.time) (out I e.out)(cs )(scs )>;
}

Loop {
  () (out e.1)(cs e.2)(scs e.3) =
         <Test (out e.1)(cs e.2)(scs e.3)>;
  (s.t e.time) (out e.1)(cs e.2)(scs e.3) = 
         <Loop (e.time) <RandomAction s.t (out e.1)(cs e.2)(scs e.3)>>;
}


RandomAction {
* r1
r1 (out I e.1)(cs )(scs ) = (out e.1)(cs I)(scs );
* r2
r2 (out I e.1)(cs )(scs e.3) = (out e.1)(cs )(scs I e.3);
* r3 
r3 (out e.1)(cs I e.2)(scs e.3) = (out I e.1)(cs e.2)(scs e.3);
* r4 
r4 (out e.1)(cs e.2)(scs I e.3) = (out I e.1)(cs e.2)(scs e.3);
}


Test {
(out e.1)(cs I e.2)(scs I e.3) = False;

(out e.1)(cs e.2)(scs e.3) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • out ≥ 0, cs = 0, scs = 0
  • The potentially unsafe states:
    • (1) cs ≥ 1, scs ≥ 1
Top Bottom On the encoding Specification Result of supercompilation

Example #16 (Control Server Monitor protocol):

/*
  Consitency Protocols with Atomic Syncronization Actions. 
  Control Server Monitor.
  After Laurent van Begin: 
  http://www.ulb.ac.be/di/ssd/lvbegin/CST/#examples
*/

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go { e.time (e.think) 
  = <Loop (Time e.time) 
              (Think I e.think)(WaitC )(UseC )(Stopped )
              (WaitD )(UseD )(IdleD I)(BusyD )
              (IdleC I)(BusyC )
              (Pbusy )(Noint I)(Int )
    >;
}

Loop {
  (Time ) 
     (Think e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13)
      = <Test 
             (Think e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
             (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
             (IdleC e.9)(BusyC e.10)
             (Pbusy e.11)(Noint e.12)(Int e.13)
        >;

  (Time s.t e.time) 
     (Think e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13)
      =  <Loop (Time e.time) 
           <RandomAction s.t
             (Think e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
             (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
             (IdleC e.9)(BusyC e.10)
             (Pbusy e.11)(Noint e.12)(Int e.13)
         >>;
}

RandomAction {
*--- REQ
 REQ (Think I e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13)
   =
     (Think e.1)(WaitC I e.2)(UseC e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13);


* --- USE_C
USE_C (Think e.1)(WaitC I e.2)(UseC e.3)(Stopped e.4)
      (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
      (IdleC I e.9)(BusyC e.10)
      (Pbusy e.11)(Noint e.12)(Int e.13)
   =
     (Think e.1)(WaitC e.2)(UseC I e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9)(BusyC I e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13);

*--- RELEASE_C
 RELEASE_C1
     (Think e.1)(WaitC e.2)(UseC I e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9)(BusyC I e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13)
   =
     (Think I e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC I e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13);

 RELEASE_C2
     (Think e.1)(WaitC e.2)(UseC I e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9)(BusyC I e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13)
   =
     (Think e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
     (WaitD I e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC I e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13);

*--- USE_D
USE_D (Think e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
      (WaitD I e.5)(UseD e.6)(IdleD I e.7)(BusyD e.8)
      (IdleC e.9)(BusyC e.10)
      (Pbusy e.11)(Noint e.12)(Int e.13)
   =
     (Think e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
     (WaitD e.5)(UseD I e.6)(IdleD e.7)(BusyD I e.8)
     (IdleC e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13);

*--- RELEASE_D
 RELEASE_D
     (Think e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
     (WaitD e.5)(UseD I e.6)(IdleD e.7)(BusyD I e.8)
     (IdleC e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13)
   =
     (Think e.1)(WaitC I e.2)(UseC e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD I e.7)(BusyD e.8)
     (IdleC e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13);

*--- STOP
 STOP
     (Think e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9)(BusyC e.10)
     (Pbusy e.11)(Noint I e.12)(Int e.13)
   =
     (Think e.1)(WaitC e.2)(UseC )(Stopped e.3 e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9 e.11)(BusyC e.10)
     (Pbusy )(Noint e.12)(Int I e.13);

*---RETURN
RETURN
     (Think e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int I e.13)
   =
     (Think e.1)(WaitC e.2)(UseC e.3 e.4)(Stopped )
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC )(BusyC e.10)
     (Pbusy e.9 e.11)(Noint I e.12)(Int e.13);
}

Test {
     (Think e.1)(WaitC e.2)(UseC I I e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13)
     = False;

     (Think e.1)(WaitC e.2)(UseC e.3)(Stopped e.4)
     (WaitD e.5)(UseD e.6)(IdleD e.7)(BusyD e.8)
     (IdleC e.9)(BusyC e.10)
     (Pbusy e.11)(Noint e.12)(Int e.13)
     = True;
};
  • The parameterized  initial  configuration  is  expressed  as:   
    • Think ≥ 1, WaitC = 0, UseC = 0, Stopped = 0, WaitD = 0, UseD = 0, IdleD = 1,
    BusyD = 0, IdleC = 1, BusyC = 0, Pbusy = 0, Noint = 1, Int = 0
  • The potentially unsafe states:
    • (1) UseC ≥ 2
Top Bottom On the encoding Specification Result of supercompilation

Example #17 (Inc/Dec):

This incorrect model of the parameterized "Atomic Increments and decrements on a Point object" protocol is taken from the web-page by Laurent van Begin. 

/*
Atomic Increments and decrements on a Point object.
 
An incorrect abstract model for inc/dec threads
given by Laurent van Begin: 
http://www.ulb.ac.be/di/ssd/lvbegin/CST/#examples
*/

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;

*$MATCHING ForRepeatedSpecialization;


/* 
* A usafed test for the incorrect abstract model for inc/dec threads given by Laurent van Begin. 
* Just 1) uncomment the following entry point;
*      2) comment the second entry point;
*      3) compile the program and launch it.
* The usafed test is 
*   time = r1 r1 r2 r3 r4 r5 r2 r3 r4 r5
*   whileinc = I I
*   whiledec = I
*   notxpos  = I
*   notypos  = I 
*   unlock   = I
* All other variables are assigned zero.

$ENTRY Go { 
  = <Prout 
    <Loop (Time r1 r1 r2 r3 r4 r5 r2 r3 r4 r5) 
                   (whileinc I I)(incx )(xi )(notifyincx )(endincx ) 
                   (incy )(yi )(notifyincy )(endincy )(endinc ) 

                   (whiledec I)(decx )(while1 )(wait1 )(afterwait1 ) 
                   (xd )(enddecx1 )(enddecx2 )(decy )(while2 ) 
                   (wait2 )(afterwait2 )(yd )(enddecy1 )(enddecy2 )(enddec )

                   (xpos )(notxpos I)(ypos )(notypos I) 
                   (lock )(unlock I)
    >>;
}
*/

*/*
$ENTRY Go { 
 e.time (e.wh_inc)(e.wh_dec) 
  = <Loop (Time e.time) 
                   (whileinc I e.wh_inc)(incx )(xi )(notifyincx )(endincx ) 
                   (incy )(yi )(notifyincy )(endincy )(endinc ) 

                   (whiledec I e.wh_dec)(decx )(while1 )(wait1 )(afterwait1 ) 
                   (xd )(enddecx1 )(enddecx2 )(decy )(while2 ) 
                   (wait2 )(afterwait2 )(yd )(enddecy1 )(enddecy2 )(enddec )

                   (xpos )(notxpos I)(ypos )(notypos I) 
                   (lock )(unlock I)
    >;
}
*/

Loop {
  (Time ) 
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
      = <Test 
              (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
              (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10)
 
              (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
              (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
              (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

              (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
              (lock e.31)(unlock e.32)
        >;

  (Time s.t e.time) 
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 
     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25) 
     (enddec e.26)(xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
      =  <Loop (Time e.time) 
           <RandomAction s.t
               (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
               (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 
               (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
               (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
               (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25) 
               (enddec e.26)(xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
               (lock e.31)(unlock e.32)
         >>;
}

RandomAction {
* r1
/*
--1---
	when
	  whileinc >= 1
	do {
  	     whileinc' = whileinc - 1,
             incx' = incx + 1
           } goto LOC;
*/
  r1 (whileinc I e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25) 
     (enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx I e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32);

* r2
/*
--2---
	when
	  incx >= 1 & unlock >= 1 
	do {
	     incx' = incx - 1,
	     xi' = xi + 1,
	     unlock' = unlock - 1,
	     lock' = lock + 1
           } goto LOC;
*/
  r2 (whileinc e.1)(incx I e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32)
     =
     (whileinc e.1)(incx e.2)(xi I e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32);

* r3
/*
--3---
	when
	  xi >= 1 
	do {
	     xi' = xi - 1,
	     notifyincx' = notifyincx + 1,
	     xpos' = xpos + notxpos + 0,
	     notxpos' = 0
           } goto LOC;
*/
  r3 (whileinc e.1)(incx e.2)(xi I e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx I e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27 e.28)(notxpos )(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32);

**************************************************************
* r4
/*
--4---
	when
	  notifyincx >= 1 
	do {
	     notifyincx' = notifyincx - 1,
	     endincx' = endincx + 1,
	     afterwait1' = afterwait1 + wait1 + 0,
	     wait1' = 0,
	     afterwait2' = afterwait2 + wait2 + 0,
  	     wait2' = 0
           } goto LOC;
*/
  r4 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx I e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx I e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 )(afterwait1 e.14 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 )(afterwait2 e.21 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32);

* r5
/*
--5---
	when
	  endincx >= 1 & lock >= 1 
	do {
	     endincx' = endincx - 1,
	     incy' = incy + 1,
	     lock' = lock - 1,
	     unlock' = unlock + 1
           } goto LOC;
*/
  r5 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx I e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy I e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32);

/********************************************************************
* The specification part given above is incorrect.  
* The following test
*   time = r1 r1 r2 r3 r4 r5 r2 r3 r4 r5
*   demonstrates that.
*  We commented the other part of the specification, which is irrelevant to the test.
*/
* r6
/*
--6---
	when
	  incy >= 1 & unlock >= 1 
	do {
	     incy' = incy - 1,
	     yi' = yi + 1,
	     unlock' = unlock - 1,
	     lock' = lock + 1
           } goto LOC;
*+/
  r6 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy I e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi I e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32);

* r7
/*
--7---
	when
  	  yi >= 1 
	do {
	    yi' = yi - 1,
	    notifyincy' = notifyincy + 1,
	    ypos' = ypos + notypos + 0,
	    notypos' = 0
           } goto LOC;
*+/
  r7 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi I e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy I e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29 e.30)(notypos )
     (lock e.31)(unlock e.32);

* r8
/*
--8---
	when
	  notifyincy >= 1 
	do {
	     notifyincy' = notifyincy - 1,
	     endincy' = endincy + 1,
	     afterwait1' = afterwait1 + wait1 + 0,
             wait1' = 0,
             afterwait2' = afterwait2 + wait2 + 0,
             wait2' = 0
           } goto LOC;
*+/
  r8 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy I e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy I e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 )(afterwait1 e.14 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 )(afterwait2 e.21 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32);

* r9
/*
--9---
	when
	 endincy >= 1 & lock >= 1 
	do {
	     endincy' = endincy - 1,
	     endinc' = endinc + 1, 
	     lock' = lock - 1,
	     unlock' = unlock + 1
           } goto LOC;
*+/
  r9 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy I e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc I e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32);

* r10
/*
--10---
	when
	  endinc >= 1 
	do {
	     endinc' = endinc - 1,
	     whileinc' = whileinc + 1
           } goto LOC;
*+/
 r10 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc I e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc I e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32);

* r11
/*
--11---
	when
	  whiledec >= 1 
	do {
	     whiledec' = whiledec - 1,
	     decx' = decx + 1
           } goto LOC;
*+/
 r11 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec I e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx I e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32);

* r12
/*
--12---
	when
	  decx >= 1 & unlock >= 1 
	do {
	     decx' = decx - 1,
	     while1' = while1 + 1,
	     unlock' = unlock - 1,
	     lock' = lock + 1
           } goto LOC;
*+/
 r12 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx I e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 I e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32);

* r13
/*
--13---
	when
	  while1 >= 1 & lock >= 1 & notxpos >= 1 
	do {
	     while1' = while1 - 1,
	     wait1' = wait1 + 1,
	     lock' = lock - 1,
	     unlock' = unlock + 1
           } goto LOC;
*+/
 r13 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 I e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos I e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 I e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos I e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32);

* r14
/*
--14---
	when
	  afterwait1 >= 1 & unlock >= 1 
	do {
	    afterwait1' = afterwait1 - 1,
	    while1' = while1 + 1,
	    unlock' = unlock - 1,
	    lock' = lock + 1
          } goto LOC;
*+/
 r14 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 I e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 I e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32);

* r15
/*
--15---
	when
	  while1 >= 1 & xpos >= 1 
	do {
	     while1' = while1 - 1,
	     xd' = xd + 1
           } goto LOC;
*+/
 r15 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 I e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos I e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd I e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos I e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32);

* r16
/*
--16---
	when
	  xd >=1 
	do {
	     xd' = xd - 1,
	     enddecx1' = enddecx1 + 1,
	     xpos' = xpos + notxpos + 0,
	     notxpos' = 0
           } goto LOC;
*+/
 r16 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd I e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 I e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27 e.28)(notxpos )(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32);

* r17
/*
--17---
	when
	  xd >=1 
	do {
             xd' = xd - 1,
             enddecx2' = enddecx2 + 1,
             notxpos' = xpos + notxpos + 0,
             xpos' = 0
           } goto LOC;
*+/
 r17 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd I e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 I e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos )(notxpos e.27 e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32);

* r18
/*
--18---
	when
	  enddecx1 >= 1 & lock >= 1 
	do {
	     enddecx1' = enddecx1 - 1,	
	     decy' = decy + 1,
	     lock' = lock - 1,
	     unlock' = unlock + 1
           } goto LOC;
*+/
 r18 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 I e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy I e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32);

* r19
/*
--19---
	when
	  enddecx2 >= 1 & lock >= 1 
	do {
             enddecx2' = enddecx2 - 1,
             decy' = decy + 1,
             lock' = lock - 1,
             unlock' = unlock + 1
           } goto LOC;
*+/
 r19 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 I e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy I e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32);

* r20
/*
--20---
	when
	  decy >= 1 & unlock >= 1 
	do {
	     decy' = decy - 1,
	     while2' = while2 + 1,
	     unlock' = unlock - 1,
	     lock' = lock + 1
           } goto LOC;
*+/
 r20 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy I e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 I e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32);

* r21
/*
--21---
	when
	  while2 >= 1 & notypos >= 1 & lock >= 1 
	do {
	     while2' = while2 - 1,
	     wait2' = wait2 + 1,
	     lock' = lock - 1,
	     unlock' = unlock + 1
           } goto LOC;
*+/
 r21 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 I e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos I e.30)
     (lock I e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 I e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos I e.30)
     (lock e.31)(unlock I e.32);

* r22
/*
--22---
	when
	  afterwait2 >= 1 & unlock >= 1 
	do {
	     afterwait2' = afterwait2 - 1,
	     while2' = while2 + 1,
	     unlock' = unlock - 1,
	     lock' = lock + 1
           } goto LOC;
*+/
 r22 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 I e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 I e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32);

* r23
/*
--23---
	when
	  while2 >= 1 & ypos >= 1 
	do {
	     while2' = while2 - 1,
	     yd' = yd + 1
           } goto LOC;
*+/
 r23 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 I e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos I e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd I e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos I e.29)(notypos e.30)
     (lock e.31)(unlock e.32);

* r24
/*
--24---
	when
	  yd >= 1 
	do {
	     yd' = yd - 1,
	     enddecy1' = enddecy1 + 1,
	     ypos' = ypos + notypos + 0,
	     notypos' = 0
           } goto LOC; 
*+/
 r24 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd I e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 I e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29 e.30)(notypos )
     (lock e.31)(unlock e.32);

* r25
/*
--25---
	when
	  yd >= 1 
	do {
             yd' = yd - 1,
             enddecy2' = enddecy2 + 1,
             notypos' = ypos + notypos + 0,
             ypos' = 0
           } goto LOC; 
*+/
 r25 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd I e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 I e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos )(notypos e.29 e.30)
     (lock e.31)(unlock e.32);

* r26
/*
--26---
	when
	  enddecy1 >= 1 & lock >= 1 
	do {
	     enddecy1' =enddecy1 - 1,
	     enddec' = enddec + 1,
	     lock' = lock - 1,
	     unlock' = unlock + 1
           } goto LOC;
*+/
 r26 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 I e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec I e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32);

* r27
/*
--27---
	when
	  enddecy2 >= 1 & lock >= 1 
	do {
             enddecy2' =enddecy2 - 1,
             enddec' = enddec + 1,
             lock' = lock - 1,
             unlock' = unlock + 1
           } goto LOC;
*+/
 r27 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 I e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock I e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec I e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock I e.32);

* r28
/*
--28---
	when
	  enddec >= 1 
	do {
	     enddec' = enddec - 1,
	     whiledec' = whiledec + 1
           } goto LOC;
*+/
 r28 (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec I e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32)
     =
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec I e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32);
}


/* 
 We paint the False cases with the numbers. 
 The aim is to keep (in the residual program) the possible traces of the cases.
*/
Test {
* (1)
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy I I e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32) 
     = False1;

* (2)
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy I e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy I e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32) 
     = False2;

* (3)
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy I I e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32) 
     = False3;

******
     (whileinc e.1)(incx e.2)(xi e.3)(notifyincx e.4)(endincx e.5) 
     (incy e.6)(yi e.7)(notifyincy e.8)(endincy e.9)(endinc e.10) 

     (whiledec e.11)(decx e.12)(while1 e.13)(wait1 e.14)(afterwait1 e.15) 
     (xd e.16)(enddecx1 e.17)(enddecx2 e.18)(decy e.19)(while2 e.20) 
     (wait2 e.21)(afterwait2 e.22)(yd e.23)(enddecy1 e.24)(enddecy2 e.25)(enddec e.26)

     (xpos e.27)(notxpos e.28)(ypos e.29)(notypos e.30)
     (lock e.31)(unlock e.32) 
     = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • whileinc ≥ 1, incx = 0, xi = 0, notifyincx = 0, endincx = 0, incy = 0, yi = 0,
    notifyincy = 0, endincy = 0, endinc = 0, whiledec ≥ 1, decx = 0, while1 = 0,
    wait1 = 0, afterwait1 = 0, xd = 0, enddecx1 = 0, enddecx2 = 0, decy = 0, while2 = 0,
    wait2 = 0, afterwait2 = 0, yd = 0, enddecy1 = 0, enddecy2 = 0, enddec = 0, xpos = 0,
    notxpos = 1, ypos = 0, notypos = 1, lock = 0, unlock = 1
  • The potentially unsafe states:
    • (1) decy ≥ 2
    (2) decy ≥ 1, incy ≥ 1
    (3) incy ≥ 2
Top Bottom On the encoding Specification Result of supercompilation

Example #18 (P/C):

The description of the parameterized Consumer Producer protocol is taken from the web-page by Laurent van Begin. 

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go { e.time  (e.c)(e.p)
  = <Loop (Time e.time) 
            (initc I e.c) 
            (whilec ) (whileget ) (waitget ) 
            (competec )(notifyc ) (endc )
            (initp I e.p) 
            (whilep )(whileput )(waitput )(competep ) 
            (notifyp )(returnp )(available )(notavailable I) 
            (lock )(notlock I)
    >;
}

Loop {
  (Time ) 
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18)
      = <Test 
             (initc e.1) 
             (whilec e.2) (whileget e.3) (waitget e.4) 
             (competec e.5)(notifyc e.6) (endc e.7)
             (initp e.8) 
             (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
             (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
             (lock e.17)(notlock e.18)
        >;

  (Time s.t e.time) 
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18)
      =  <Loop (Time e.time) 
           <RandomAction s.t
             (initc e.1) 
             (whilec e.2) (whileget e.3) (waitget e.4) 
             (competec e.5)(notifyc e.6) (endc e.7)
             (initp e.8) 
             (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
             (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
             (lock e.17)(notlock e.18)
         >>;
}

RandomAction {
*--- consumer
* c1
/*
when
initc >= 1
do {
	initc' = initc - 1
	,
	whilec' = whilec + 1} goto LOC;
*/
c1  (initc I e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18)
    =
    (initc e.1) 
    (whilec I e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18);

* c2
/*
when
whilec >= 1 & notlock >= 1 
do {
	whilec' = whilec - 1
	,
	whileget' = whileget + 1
	,
	notlock' = notlock - 1
	,
	lock' = lock + 1} goto LOC;
*/
c2  (initc e.1) 
    (whilec I e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock I e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget I e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock I e.17)(notlock e.18);

* c3
/*
when
whileget >= 1 & notavailable >= 1 & lock >= 1 
do {
	whileget' = whileget - 1
	,
	waitget' = waitget + 1
	,
	lock' = lock - 1
	,
	notlock' = notlock + 1} goto LOC;
*/
c3  (initc e.1) 
    (whilec e.2) (whileget I e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable I e.16) 
    (lock I e.17)(notlock e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget I e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable I e.16) 
    (lock e.17)(notlock I e.18);

* c4
/*
when
competec >= 1 & notlock >= 1 
do {
	competec' = competec - 1
	,
	whileget' = whileget + 1
	,
	notlock' = notlock - 1
	,
	lock' = lock + 1} goto LOC;
*/
c4  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec I e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock I e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget I e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock I e.17)(notlock e.18);

* c5
/*
when
whileget >= 1 & available >= 1 
do {
	whileget' = whileget - 1
	,
	notifyc' = notifyc + 1
	,
	notavailable' = notavailable + 1 
	,
	available' = available - 1} goto LOC;
*/
c5  (initc e.1) 
    (whilec e.2) (whileget I e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available I e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc I e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable I e.16) 
    (lock e.17)(notlock e.18);

* c6
/*
when
notifyc >= 1 
do {
	notifyc' = notifyc - 1
	,
	endc' = endc + 1
	,
	competec' = competec + waitget 
	,
	waitget' = 0
	,
	competep' = competep + waitput 
	,
	waitput' = 0 } goto LOC;
*/
c6  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc I e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget ) 
    (competec e.4 e.5)(notifyc e.6) (endc I e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput )(competep e.11 e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18);

* c7
/*
when
endc >= 1 & lock >= 1 
do {
	endc' = endc - 1
	,
	whilec' = whilec + 1
	,
	lock' = lock - 1
	,
	notlock' = notlock + 1} goto LOC;
*/
c7  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc I e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock I e.17)(notlock e.18)
    =
    (initc e.1) 
    (whilec I e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock I e.18);

***--- producer
* p1
/*
when
initp >= 1
do {
	initp' =initp - 1
	,
	whilep' = whilep + 1} goto LOC;
*/
p1  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp I e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep I e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18);

* p2
/*
when
whilep >= 1 & notlock >= 1 
do {
	whilep' = whilep - 1
	,
	whileput' = whileput + 1
	,
	notlock' = notlock - 1
	,
	lock' = lock + 1} goto LOC;
*/
p2  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep I e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock I e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput I e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock I e.17)(notlock e.18);

* p3
/*
when
whileput >= 1 & lock >= 1 & available >= 1 
do {
	whileput' = whileput - 1
	,
	waitput' = waitput + 1
	,
	lock' = lock - 1
	,
	notlock' = notlock + 1} goto LOC;
*/
p3  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput I e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available I e.15)(notavailable e.16) 
    (lock I e.17)(notlock e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput I e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available I e.15)(notavailable e.16) 
    (lock e.17)(notlock I e.18);
	
* p4
/*
when
competep >= 1 & notlock >= 1 
do {
	competep' = competep - 1
	,
	whileput' = whileput + 1
	,
	notlock' = notlock - 1
	,
	lock' = lock + 1} goto LOC;
*/
p4  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep I e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock I e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput I e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock I e.17)(notlock e.18);
	
* p5
/*
when
whileput >= 1 & notavailable >= 1 
do {
	whileput' = whileput - 1
	,
	notifyp' = notifyp + 1
	,
	available' = available + 1 
	,
	notavailable' = notavailable - 1} goto LOC;
*/
p5  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput I e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable I e.16) 
    (lock e.17)(notlock e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp I e.13)(returnp e.14)(available I e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18);

* p6
/*
when
notifyp >= 1 
do {
	notifyp' = notifyp - 1
	,
	returnp' = returnp + 1
	,
	competec' = competec + waitget 
	,
	waitget' = 0
	,
	competep' = competep + waitput 
	,
	waitput' = 0} goto LOC;
*/
p6  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp I e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget ) 
    (competec e.4 e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput )(competep e.11 e.12) 
    (notifyp e.13)(returnp I e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18);

* p7
/*
when
returnp >= 1 & lock >= 1 
do {
	returnp' = returnp - 1
	,
	whilep' = whilep + 1
	,
	lock' = lock - 1
	,
	notlock' = notlock + 1} goto LOC;
*/
p7  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp I e.14)(available e.15)(notavailable e.16) 
    (lock I e.17)(notlock e.18)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep I e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock I e.18);

}


Test {
* (1)
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget I I e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput I I e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18)
     = False;

    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (endc e.7)
    (initp e.8) 
    (whilep e.9)(whileput e.10)(waitput e.11)(competep e.12) 
    (notifyp e.13)(returnp e.14)(available e.15)(notavailable e.16) 
    (lock e.17)(notlock e.18)
     = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • initc ≥ 1, whilec = 0, whileget = 0, waitget = 0, competec = 0, notifyc = 0,
    endc = 0, initp ≥ 1, whilep = 0, whileput = 0, waitput = 0, competep = 0,
    notifyp = 0, returnp = 0, available = 0, notavailable = 1, lock = 0, notlock = 1
  • The potentially unsafe states:
    • (1) waitget ≥ 2, waitput ≥ 2
Top Bottom On the encoding Specification Result of supercompilation

Example #19 (P/C2sansinv):

The description of the parameterized broadcast Consumer-producer protocol is taken from the web-page by Laurent van Begin. The property is that a consumer can consume a resource only when one is available. 

/*
Broadcast Protocols 
Abstract Multithreaded Java Programs:
P/C: The "classical" producer consumer with Java threads 
Java description (from the Sun Java tutorial)_ 
http://java.sun.com/docs/books/tutorial/networking/index.html

--Consumer-producer example
--The property is that a consumer can consume a resource only when one is 
--available
*/

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;
*$TRANSIENT Yes;


$ENTRY Go { e.time  (e.c)(e.p)
  = <Loop (Time e.time) 
            (initc I e.c) 
            (whilec ) (whileget ) (waitget ) 
            (competec )(notifyc ) (consume ) (endc )
            (initp I e.p) 
            (whilep )(whileput )(waitput )(competep )
            (notifyp )(produce )(returnp )(available )(notavailable I) 
            (lock )(notlock I)
    >;
}

Loop {
  (Time ) 
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20)
      = <Test 
             (initc e.1) 
             (whilec e.2) (whileget e.3) (waitget e.4) 
             (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
             (initp e.9) 
             (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
             (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
             (lock e.19)(notlock e.20)
        >;

  (Time s.t e.time) 
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20)
      =  <Loop (Time e.time) 
           <RandomAction s.t
             (initc e.1) 
             (whilec e.2) (whileget e.3) (waitget e.4) 
             (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
             (initp e.9) 
             (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
             (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
             (lock e.19)(notlock e.20)
         >>;
}

RandomAction {
*--- consumer
* c1
/*
	when
		initc >= 1 
	do {
	initc' = initc - 1,
	whilec' = whilec + 1 } goto LOC;
*/
c1  (initc I e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec I e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20);

* c2
/*
	when
		whilec >= 1 & notlock >= 1 
	do {
	whilec' = whilec - 1,
	whileget' = whileget + 1,
	notlock' = notlock - 1,
	lock' = lock + 1 } goto LOC;
*/
c2  (initc e.1) 
    (whilec I e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock I e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget I e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock I e.19)(notlock e.20);

* c3
/*
	when
		whileget >= 1 & notavailable >= 1 & lock >= 1 
	do {
	whileget' = whileget - 1,
	waitget' = waitget + 1,
	lock' = lock - 1,
	notlock' = notlock + 1 } goto LOC;
*/
c3  (initc e.1) 
    (whilec e.2) (whileget I e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable I e.18) 
    (lock I e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget I e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable I e.18) 
    (lock e.19)(notlock I e.20);

* c4
/*
	when
		competec >= 1 & notlock >= 1 
	do {
	competec' = competec - 1,
	whileget' = whileget + 1,
	notlock' = notlock - 1,
	lock' = lock + 1 } goto LOC;
*/
c4  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec I e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock I e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget I e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock I e.19)(notlock e.20);


* c5
/*
	when
		whileget >= 1 & available >= 1 
	do {
	whileget' = whileget - 1,
	consume' = consume + 1 } goto LOC;
*/
c5  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget I e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available I e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume I e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available I e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20);


* c6
/*
	when
		consume >= 1 
	do {	
        consume' = consume - 1,
	notifyc' = notifyc + 1,
	notavailable' = notavailable + 1,
	available' = available - 1 } goto LOC;
*/
c6  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume I e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available I e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc I e.5) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable I e.18) 
    (lock e.19)(notlock e.20);

* c7
/*
	when	
		notifyc >= 1 
	do {
	notifyc' = notifyc - 1,
	endc' = endc + 1,
	competec' = competec + waitget,
	waitget' = 0,
	competep' = competep + waitput,
	waitput' = 0 } goto LOC;
*/
c7  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc I e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget ) 
    (competec e.4 e.5)(notifyc e.5) (consume e.7) (endc I e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput )(competep e.12 e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20);

* c8
/*
	when
		endc >= 1 & lock >= 1 
	do {
	endc' = endc - 1,
	whilec' = whilec + 1,
	lock' = lock - 1,
	notlock' = notlock + 1 } goto LOC;
*/
c8  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc I e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock I e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec I e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock I e.20);

** --producer
* p1
/*
	when
		initp >= 1 
	do {
	initp' =initp - 1,
	whilep' = whilep + 1 } goto LOC;
*/
p1  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp I e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep I e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20);

* p2
/*
	when
		whilep >= 1 & notlock >= 1 
	do {
	whilep' = whilep - 1,
	whileput' = whileput + 1,
	notlock' = notlock - 1,
	lock' = lock + 1 } goto LOC;
*/
p2  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep I e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock I e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput I e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock I e.19)(notlock e.20);

* p3
/*
	when
		whileput >= 1 & lock >= 1 & available >= 1 
	do {
	whileput' = whileput - 1,
	waitput' = waitput + 1,
	lock' = lock - 1,
	notlock' = notlock + 1} goto LOC;
*/
p3  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput I e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available I e.17)(notavailable e.18) 
    (lock I e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput I e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available I e.17)(notavailable e.18) 
    (lock e.19)(notlock I e.20);
	

* p4
/*
	when
		competep >= 1 & notlock >= 1 
	do {
	competep' = competep - 1,
	whileput' = whileput + 1,
	notlock' = notlock - 1,
	lock' = lock + 1 } goto LOC;
*/
p4  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep I e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock I e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput I e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock I e.19)(notlock e.20);
	
* p5
/*
	when
		whileput >= 1 & notavailable >= 1 
	do {
	whileput' = whileput - 1,
	produce' = produce + 1 } goto LOC;
*/
p5  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput I e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable I e.18) 
    (lock e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce I e.15)(returnp e.16)(available e.17)(notavailable I e.18) 
    (lock e.19)(notlock e.20);

* p6
/*
	when
		produce >= 1 
	do {
	produce' = produce - 1,
	notifyp' = notifyp + 1,
	available' = available + 1,
	notavailable' = notavailable - 1} goto LOC;
*/
p6  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce I e.15)(returnp e.16)(available e.17)(notavailable I e.18) 
    (lock e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp I e.14)(produce e.15)(returnp e.16)(available I e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20);

* p7
/*
	when
		notifyp >= 1 
	do {
	notifyp' = notifyp - 1,
	returnp' = returnp + 1,
	competec' = competec + waitget,
	waitget' = 0,
	competep' = competep + waitput,
	waitput' = 0 } goto LOC;
*/
p7  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp I e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget ) 
    (competec e.4 e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput )(competep e.12 e.13)
    (notifyp e.14)(produce e.15)(returnp I e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20);

* p8
/*
	when
		returnp >= 1 & lock >= 1 
	do {
	returnp' = returnp - 1,
	whilep' = whilep + 1,
	lock' = lock - 1,
	notlock' = notlock + 1 } goto LOC;
*/
p8  (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp I e.16)(available e.17)(notavailable e.18) 
    (lock I e.19)(notlock e.20)
    =
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep I e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock I e.20);

}

*1.  final_reg :=  consume >= 1 & notavailable >= 1;
Test {
* (1)
    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume I e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable I e.18) 
    (lock e.19)(notlock e.20)
     = False;

    (initc e.1) 
    (whilec e.2) (whileget e.3) (waitget e.4) 
    (competec e.5)(notifyc e.6) (consume e.7) (endc e.8)
    (initp e.9) 
    (whilep e.10)(whileput e.11)(waitput e.12)(competep e.13)
    (notifyp e.14)(produce e.15)(returnp e.16)(available e.17)(notavailable e.18) 
    (lock e.19)(notlock e.20)
     = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • initc ≥ 1, initp ≥ 1, whilec = 0, whileget = 0, waitget = 0, competec = 0,
    notifyc = 0, consume = 0, endc = 0, whilep = 0, whileput = 0, waitput = 0,
    competep = 0, notifyp = 0, produce = 0, returnp = 0, available = 0,
    notavailable = 1, lock = 0, notlock = 1
  • The potentially unsafe states:
    • (1) consume ≥ 1, notavailable ≥ 1
Top Bottom On the encoding Specification Result of supercompilation

Example #20 (2P/2C):

The description of the parameterized Two Consumers - Two Producers protocol is taken from the web-page by Laurent van Begin.

The Refal program encoding this protocol is too large and may be downloaded.

Top Bottom On the encoding Specification Result of supercompilation

Example #21 (SPS2):

The incorrect specification of the parameterized SPS2 protocol is taken from the paper by X. Zhao, K. Sammut, F. He, Sh. Qin and made more precise (but still incorrect) by Xuemei Zhao in an e-mail message. 

/*
  The parameterized SPS2 Snooping Cache Coherence Protocol for CMP
  is taken from the paper
  "Formal Verification of a Novel Snooping Cache Coherence Protocol for CMP" 
  by Xuemei Zhao, Karl Sammut and Fangpo He. 
  There exists an error in the protocol's state graph given in the paper.
  The error was "corrected" by the authors of the protocol 
   in an e-mail message by Xuemei Zhao (SPS2_states.pdf was attached by him),
  but nevertheless the protocol violates one of the safety properies.
*/

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;

* A usafed test for the incorrect abstract model for inc/dec threads given by Laurent van Begin. 
* Just 1) uncomment the following entry point;
*      2) comment the second entry point;
*      3) compile the program and launch it.
* The usafed test is 
*   time = r2 wm12 r3 rp1-r16 repS-r20
*   III = I I I
* All other variables are assigned zero.

/*
$ENTRY Go { 
* The test: r2 wm12 r3 rp1-r16 repS-r20

      = <Prout <Loop (Time r2 wm12 r3 rp1-r16 repS-r20) 
               (III I I I)(IIS )(SIS )(MII )(IMI )(OIS )(IOS )>>; 
}
*/


*/*
$ENTRY Go { 
 e.time (e.i) = <Loop (Time e.time) (III I e.i)(IIS )(SIS )(MII )(IMI )(OIS )(IOS )>; 
}
*/

Loop {
  (Time ) (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7)
       = <Test (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7)>;
  (Time s.t e.time) (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7)
       = <Loop (Time e.time) <RandomAction s.t  
               (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7)>>;
}


RandomAction {
* (r1) SIS+OIS+MII >= 1 .
* Trivial

* r2
* (r2) III >= 1, MII=0, IMI=0 -> III'=0, SIS'=SIS+1, IIS'=IIS+III-1
r2 (III I e.1)(IIS e.2)(SIS e.3)(MII )(IMI )(OIS e.6)(IOS e.7)
                 = (III )(IIS e.2 e.1)(SIS I e.3)(MII )(IMI )(OIS e.6)(IOS e.7);

* r3 
* (r3) III >= 1, MII >= 1 -> III'=0, SIS'=SIS+1, MII'=MII-1,OIS'=OIS+1, IIS'=IIS+III-1
r3 (III I e.1)(IIS e.2)(SIS e.3)(MII I e.4)(IMI e.5)(OIS e.6)(IOS e.7)
                 = (III )(IIS e.2 e.1)(SIS I e.3)(MII e.4)(IMI e.5)(OIS I e.6)(IOS e.7);

* r4 
* (r4) III >= 1, IMI >= 1 -> III'=0, SIS'=SIS+1, IMI'=IMI-1,IOS'=IOS+1, IIS'=IIS+III-1
r4 (III I e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI I e.5)(OIS e.6)(IOS e.7)
                 = (III )(IIS e.2 e.1)(SIS I e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS I e.7);

* r5
* (r5) IIS >= 1 -> IIS'=IIS-1, SIS'=SIS+1
r5 (III e.1)(IIS I e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7)
                 = (III e.1)(IIS e.2)(SIS I e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7);

* r6
* (r6) IMI >= 1 -> MII'=MII+1, IMI'=IMI-1
r6 (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI I e.5)(OIS e.6)(IOS e.7)
                 = (III e.1)(IIS e.2)(SIS e.3)(MII I e.4)(IMI e.5)(OIS e.6)(IOS e.7);

* r7
* (r7) IOS >= 1 -> OIS'=OIS+1, IOS'=IOS-1
r7 (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS I e.7)
                 = (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS I e.6)(IOS e.7);


* wh8 - hit
* (wh8) MII >= 1 -> .
* trivial

* wh9 - hit
* (wh9) IMI >= 1 -> IMI' = IMI-1, MII' = MII+1
wh9 (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI I e.5)(OIS e.6)(IOS e.7)
                 = (III e.1)(IIS e.2)(SIS e.3)(MII I e.4)(IMI e.5)(OIS e.6)(IOS e.7);

* wm10 - miss
* (wm10) OIS >= 1 -> MII' = 1, OIS' = 0, 
*                    IIS' = 0, IMI' = 0, IOS' = 0, SIS' = 0,
*                    III' = III + IIS + (OIS-1) + MII + IMI + IOS + SIS
wm10 (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS I e.6)(IOS e.7)
                 = (III e.1 e.2 e.6 e.4 e.5 e.7 e.3)(IIS )(SIS )(MII I)(IMI )(OIS )(IOS );
* wm11 - miss
* (wm11) IOS >= 1 -> MII' = 1, IOS' = 0, 
*                    IIS' = 0, IMI' = 0, OIS' = 0, SIS' = 0,
*                    III' = III + IIS + OIS + MII + IMI + (IOS-1) + SIS
wm11 (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS I e.7)
                 = (III e.1 e.2 e.6 e.4 e.5 e.7 e.3)(IIS )(SIS )(MII I)(IMI )(OIS )(IOS );

* wm12 - miss
* (wm12) SIS >= 1 -> MII' = 1, SIS' = 0, 
*                    IIS' = 0, IMI' = 0, IOS' = 0, OIS' = 0,
*                    III' = III + IIS + OIS + MII + IMI + IOS + (SIS-1)
wm12 (III e.1)(IIS e.2)(SIS I e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7)
                 = (III e.1 e.2 e.6 e.4 e.5 e.7 e.3)(IIS )(SIS )(MII I)(IMI )(OIS )(IOS );

* wm13 - miss
* (wm13) III >= 1 -> MII' = 1,  
*                    IIS' = 0, IMI' = 0, IOS' = 0, SIS' = 0, OIS' = 0,
*                    III' = (III-1) + IIS + OIS + MII + IMI + IOS + SIS
wm13 (III I e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7)
                 = (III e.1 e.2 e.6 e.4 e.5 e.7 e.3)(IIS )(SIS )(MII I)(IMI )(OIS )(IOS );

* wm14 - miss
* (wm14) IIS >= 1 -> MII' = 1, IIS' = 0, 
*                    IIS' = 0, IMI' = 0, IOS' = 0, SIS' = 0,
*                    III' = III + IIS + (OIS-1) + MII + IMI + IOS + SIS
wm14 (III e.1)(IIS I e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7)
                 = (III e.1 e.2 e.6 e.4 e.5 e.7 e.3)(IIS )(SIS )(MII I)(IMI )(OIS )(IOS );

* rp1-r15 - replacement
* (rp1-r15) MII >= 1 -> MII' = MII-1, IMI' = IMI+1 
rp1-r15 (III e.1)(IIS e.2)(SIS e.3)(MII I e.4)(IMI e.5)(OIS e.6)(IOS e.7)
                 = (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI I e.5)(OIS e.6)(IOS e.7);

* rp1-r16 - replacement
* (rp1-r16) OIS >= 1 -> OIS' = OIS-1, IOS' = IOS+1 
rp1-r16 (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS I e.6)(IOS e.7)
                 = (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS I e.7);

* rp1-r17 - replacement
* (rp1-r17) SIS >= 1 -> SIS' = SIS-1, IIS' = IIS+1 
rp1-r17 (III e.1)(IIS e.2)(SIS I e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7)
                 = (III e.1)(IIS I e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7);

* rp2-r18 - replacement
* (rp2-r18) IOS >= 1 -> IOS' = IOS-1, IIS' = IIS+1 
rp2-r18 (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS I e.7)
                 = (III e.1)(IIS I e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7);

* rp2-r19 - replacement
* (rp2-r19) IMI >= 1 -> IMI' = IMI-1, III' = III+1 
rp2-r19 (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI I e.5)(OIS e.6)(IOS e.7)
                 = (III I e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7);

* repS-r20 - replacement
* (repS-r20) IOS >= 1 -> IOS' = IOS-1, IMI' = IMI+1 
repS-r20 (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS I e.7)
                 = (III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI I e.5)(OIS e.6)(IOS e.7);

* repS-r21 - replacement
* (repS-r21) IIS >= 1 -> IIS' = IIS-1, III' = III+1 
repS-r21 (III e.1)(IIS I e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7)
                 = (III I e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7);

* repS-r22 - replacement
* (repS-r22) SIS >= 1 -> SIS' = SIS-1, III' = III+1 
repS-r22 (III e.1)(IIS e.2)(SIS I e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7)
                 = (III I e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7);

}


Test {
* (C1) OIS >= 1 & MII >= 1
(III e.1)(IIS e.2)(SIS e.3)(MII I e.4)(IMI e.5)(OIS I e.6)(IOS e.7) = False1;

* (C2) OIS >= 2
(III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS I I e.6)(IOS e.7) = False2;

* (C3) IIS >= 1 & IMI >= 1
(III e.1)(IIS I e.2)(SIS e.3)(MII e.4)(IMI I e.5)(OIS e.6)(IOS e.7) = False3;

* (C4) MII >= 2 
(III e.1)(IIS e.2)(SIS e.3)(MII I I e.4)(IMI e.5)(OIS e.6)(IOS e.7) = False4;

(III e.1)(IIS e.2)(SIS e.3)(MII e.4)(IMI e.5)(OIS e.6)(IOS e.7) = True;
}
  • The parameterized  initial  configuration  is  expressed  as:   
    • initc ≥ 1, whilec = 0, whileget = 0, waitget = 0, competec = 0, notifyc = 0,
    endc = 0, initp ≥ 1, whilep = 0, whileput = 0, waitput = 0, competep = 0,
    notifyp = 0, returnp = 0, available = 0, notavailable = 1, lock = 0, notlock = 1
  • The potentially unsafe states:
    • (1) waitget ≥ 2, waitput ≥ 2
Top Specification Result of supercompilation

References

  1. A. Lisitsa and A.P. Nemytykh. Verification of parameterized systems using supercompilation. A case study. Proceedings of the Third Workshop on Applied Semantics (APPSEM05), Fraunchiemsee, Germany, 12-15 September 2005. Editors: Martin Hofmann, Hans-Wolfgang Loidl - Ludwig Maximillians Universitat Munchen, 2005. appsem_verification2005.ps
  2. A. Lisitsa and A.P. Nemytykh. A number of experiments on verification via supercompilation. , 2005.
  3. A. Lisitsa and A.P. Nemytykh. Work on errors. (in Russian), In: Program Systems: Theory and Applications (Programmnye systemy: teoriya i prilozheniya) , Fizmatlit, Moscow, vol. 1, pp: 195-232, 2006. psta_errors2006.pdf
  4. A. Lisitsa and A.P. Nemytykh. Verification as a Parameterized Testing (Experiments with the SCP4 Supercompiler) , In: J. Programming and Computer Software , Vol. 33, No.1, pp: 14-23, 2007.
    • The paper is translation of the Russian version: Verifikatciya kak parametrizovannoe testirovanie (experimenty s superkompilyatorom SCP4). In: J. Programmirovanie, No. 1, pp: 22-34, 2007. abstract
  5. A. Lisitsa and A.P. Nemytykh. Reachability Analysis in Verification via Supercompilation,

 

nemytykh@math.botik.ru