/*
 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 >= 4) {
12 // Invalid 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 TestIncorrect.

 The resulting program points out to the counterexample for the protocol.
*/

/***********************************************/
/*           the input program                 */
/***********************************************/
*$MST_FROM_ENTRY;
$ENTRY Go {
	e.p = <while (e.p) (x1 )(x2 )(s 'I')>;
}

while {
 () (x1 e.x1)(x2 e.x2)(s e.s) = <TestIncorrect (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)>;       
}


TestIncorrect {
 (x1 e.x1)(x2 e.x2)(s 'IIII'e.s) = '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) =  'F';
 ('TTTT' e.x1) (e.x2) =  <while_12_0 (e.x1) ('I' e.x2)>;
}

*/