//Fast File Modified for ranking stuff - 2009, Dec 10,11:16:36 model easy2{ //parameters x__o, y__o, z__o; var x, y, z, x__o, y__o, z__o; states stop, start, lbl_7_1, ____start; transition t_13 :={ from := start ; to := stop ; guard := z<=0; action := ; }; transition t_14 :={ from := start ; to := lbl_7_1 ; guard := z>=1; action := z' = z - 1,y' = y - 1,x' = 1 + x; }; transition t_11 :={ from := lbl_7_1 ; to := stop ; guard := z<=0; action := ; }; transition t_12 :={ from := lbl_7_1 ; to := lbl_7_1 ; guard := z>=1; action := z' = z - 1,y' = y - 1,x' = 1 + x; }; transition ____inittransition :={ from := ____start ; to := start ; guard := true; action := x' = x__o,y' = y__o,z' = z__o; }; } strategy xx { Region init:={ state = ____start && true}; } // Result of Analysis //invariant stop := z<=z__o && z<=0 && y+z__o=z+y__o && x+z=x__o+z__o ; //invariant start := z=z__o && y=y__o && x=x__o ; //invariant ____start := true ; //invariant lbl_7_1 := x>=x__o+1 && z>=0 && x+z=x__o+z__o && x+y=x__o+y__o ;