/*
 Let us consider the following program code modeling some protocol.

 1 int main() {
 2 unsigned int x1 = 0, x2 = 0; int s = 1;
 3
 4 while (nondet()) {
 5 if (s == 1) x1++;
 6 else if (s == 2) x2++;
 7
 8 s++;
 9 if (s == 5) s = 1;
10
11 if ((s == 1) && (x1 != x2)) {
12 // Valid safety property
13 ERROR: return 1;
14 }
15 }
16 }

 In the input program below, the function while models the actions done in the lines 4-15. 
 The loop is modeled to be not deterministic by introducing the additional argument of the function while, e.p.
 The parameter determines the number of the loop iterations. 

 The test given in the line 11 is modeled by the function TestCorrect.

 The resulting program does not contain functions returning 'F', 
 hence the protocol is proven to be correct in respect to the given condition.
*/

/***********************************************/
/*           the input program                 */
/***********************************************/

$ENTRY Go {
	e.p = <while (e.p) (x1 )(x2 )(s 'I')>;
}

while {
 () (x1 e.x1)(x2 e.x2)(s e.s) = <TestCorrect (x1 e.x1)(x2 e.x2)(s e.s)>;

 ('T' e.p) (x1 e.x1)(x2 e.x2)(s 'I')                                       
	= <while (e.p) (x1 'I'e.x1)(x2 e.x2)(s 'II')>;
 ('T' e.p) (x1 e.x1)(x2 e.x2)(s 'II') 
	= <while (e.p) (x1 e.x1)(x2 'I'e.x2)(s 'III')>;
 ('T' e.p) (x1 e.x1)(x2 e.x2)(s 'IIII') 
	= <while (e.p) (x1 e.x1)(x2 e.x2)(s 'I')>;
 ('T' e.p) (x1 e.x1)(x2 e.x2)(s e.s) 
	= <while (e.p) (x1 e.x1)(x2 e.x2)(s 'I'e.s)>;       
}


TestCorrect {
 (x1 e.x1)(x2 e.x1)(s 'I') = 'T';   
 (x1 e.x1)(x2 e.x2)(s 'I') = 'F';
 (x1 e.x1)(x2 e.x2)(s e.s) = 'T';
}

/***********************************************/
/*          the residual program               */
/***********************************************/

/*
$ENTRY Go {
 e.x1 =  <while_12_0 (e.x1) ()>;
}


while_12_0 {
 () (e.x1) =  'T';
 ('T') (e.x1) =  'T';
 ('TT') (e.x1) =  'T';
 ('TTT') (e.x1) =  'T';
 ('TTTT' e.x1) (e.x2) =  <while_12_0 (e.x1) ('I' e.x2)>;
}

*/