#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: */