#define N 100
byte x=0;
proctype P1(){	
	x=x+1;
	x=x+1
}
proctype P2(){
	x=2
}

proctype ueberlauf() {
	byte y = 0;

	x = 0;
	x = x-1;
	
	x = 254;
	x = x+1;
	x = x+1;
}	

active proctype zufall() {
	do
	:: x % 10 != 9 -> x = x + 1;
	:: x % 10 == 9 && x != 99 ->  x = x +2;
	:: break;
	od

}	


/* Aufgabe 1a: Werte 2 und 4 sind möglich */
/* Aufgabe 1b: Es wird eine Fehlermeldung ausgegeben:
	  1:	proc  0 (ueberlauf) aufg1.pml:13 (state 1)	[x = 0]
	  spin: aufg1.pml:14, Error: value (-1->255 (8)) truncated in assignment
	  2:	proc  0 (ueberlauf) aufg1.pml:14 (state 2)	[x = (x-1)]
	  3:	proc  0 (ueberlauf) aufg1.pml:16 (state 3)	[x = 254]
	  4:	proc  0 (ueberlauf) aufg1.pml:17 (state 4)	[x = (x+1)]
	  spin: aufg1.pml:18, Error: value (256->0 (8)) truncated in assignment
	  5:	proc  0 (ueberlauf) aufg1.pml:18 (state 5)	[x = (x+1)]
*/
/* Aufgabe 1c: */