//Fast File Modified for ranking stuff - 2009, Dec 10,11:17:09 model relation1{ //parameters x__o, y__o; var x, y, x__o, y__o; states stop, start, lbl_4_1, ____start; transition t_22 :={ from := start ; to := lbl_4_1 ; guard := true; action := x' = ?; }; transition t_18 :={ from := lbl_4_1 ; to := stop ; guard := true; action := y' = x; }; transition ____inittransition :={ from := ____start ; to := start ; guard := true; action := x' = x__o,y' = y__o; }; } strategy xx { Region init:={ state = ____start && true}; } // Result of Analysis //invariant stop := x=y ; //invariant start := x=x__o && y=y__o ; //invariant lbl_4_1 := y=y__o ; //invariant ____start := true ;