------------------- MODULE petri8 -----------------
EXTENDS Naturals,TLC
CONSTANTS Places
VARIABLES  M

LesPlaces == {"p12"}

t1 == 
	/\ M["p11"] \geq 1  /\  M["p12"]  \geq 1 
	/\ M'=  [[[[M EXCEPT!["p11"]=M["p11"]-1] EXCEPT!["p12"]=M["p12"]-1] EXCEPT!["p21"]=M["p21"]+1] EXCEPT!["p31"]=M["p31"]+1]



t21 == 
	/\ M["p21"] \geq 1 
	/\ M'=[[[M EXCEPT!["p22"]=M["p22"]+2] EXCEPT!["p11"]=M["p11"]+1] EXCEPT!["p21"]=M["p21"]-1]



t31 == 
	/\ M["p31"] \geq 1 
	/\ M'=[[[M EXCEPT!["p33"]=M["p33"]+1] EXCEPT!["p12"]=M["p12"]+1] EXCEPT!["p31"]=M["p31"]-1]



Init1 ==  M = [p \in Places |-> IF p \in {"p11","p12"} THEN 1 ELSE 0 ]

Init == Init1

Next == t1 \/ t21 \/ t31
NONO == t1 \/ t21 \/ t31

safety1 == M["p11"]+M["p12"]\leq 2
safety2 ==  2*M["p33"]=M["p22"]  \* wrong *\
safety3 ==  M["p21"] = 0 /\ M["p31"]=0 => 2*M["p33"]=M["p22"]  

Petri  == Init /\ [][Next]_<<M>>

 
TypeInvariant ==  \A p \in Places :  M[p] \geq 0

Inv1 ==  M["p11"] + M["p12"] + M["p21"] +   M["p22"] + M["p31"] + M["p33"] \geq  2

Inv2 ==   M["p11"] + M["p12"] + M["p21"]  + M["p31"]  =   2

Inv3 ==  M["p11"] + M["p12"] + M["p21"] +   M["p22"] + M["p31"] + M["p33"] \geq  2

Inv4 ==     (M["p22"] = 2*  M["p33"])

Inv5 ==     (M["p22"] # 0  /\ M["p31"] =  0  ) => (M["p22"] = 2*  M["p33"])

Inv6 ==     (M["p22"] # 0  /\ M["p31"] =  0  /\ M["p21"] =  0  ) => (M["p22"] = 2*  M["p33"])

Inv7 ==  M["p22"] = 0

Inv8 == M["p33"] # 10

InvTest == TypeInvariant  /\ M["p22"] # 23490

Q1 == M["p31"] = 0

Q2 == M["p33"] # 18












=============================================