------------------------------ MODULE serie7_4 ------------------------------
EXTENDS Naturals, Integers, TLC, Reals
VARIABLES x,t1,t2,pc1, pc2
CONSTANTS U




Init == x=3 /\ pc1 ="l1" /\ pc2 = "m1" /\ t1 = U /\ t2 = U

(* Next 1 *)
al1l2 == pc1 ="l1" /\ pc1'="l2" /\ t1' = x /\ x'=x+1 /\ UNCHANGED <<pc2,t2>>

al2l3 == pc1 ="l2" /\ pc1'="l3" /\ x' = t1+1 /\ UNCHANGED <<pc2,t2,t1>>

Next1 == al1l2 \/ al2l3

(* Next 2 *)
am1m2 == pc2 ="m1" /\ pc2'="m2" /\ t2' = x /\ x'=x+1 /\ UNCHANGED <<pc1,t1>>

am2m3 == pc2 ="m2" /\ pc2'="m3" /\ x' = t2+1 /\ UNCHANGED <<pc1,t1,t2>>

Next2 == am1m2 \/ am2m3

Next == Next1 \/ Next2 \/ UNCHANGED <<pc1,t1,pc2,t2,x>>

Q1 == pc1 = "l3" /\ pc2="m3" => x # 4
Qpc == pc1 = "l3" /\ pc2="m3" => x \in {4,5}

=============================================================================
\* Modification History
\* Last modified Thu Nov 26 09:10:50 CET 2015 by garnier34u
\* Created Thu Nov 26 08:20:39 CET 2015 by garnier34u