------------------------------ MODULE serie3_1 ------------------------------
EXTENDS Naturals,TLC
CONSTANT T0,Nmax
VARIABLES T,V_P1,V_P2,Mutex_READ_P1,Mutex_READ_P2,S

f == [i \in Nat |-> i+3 ]

MyNat == 0..Nmax

READ_P1 == 
    /\ \E w \in MyNat : <<"data",w>> \in T
    /\ Mutex_READ_P1 = "ko"
    /\ UNCHANGED <<Mutex_READ_P2,V_P2,S,V_P2>>
   \* soit v une valeur choisie dans l'ensemble T de la forme <<"data",val>>
    /\ LET val_p1 == CHOOSE v \in MyNat :  (<<"data",v>> \in T)
        IN
            /\ V_P1'=val_p1
            /\ Mutex_READ_P1' = "ok"
            \* on supprime l'element de notre ensemble T
            \* attention on cr�e un ensemble  avec les {} que on intersect avec T
            /\ T' = T \ {<<"data",val_p1>>}
    
COMP_P1 == 
    /\ Mutex_READ_P1 = "ok"
    /\ UNCHANGED <<Mutex_READ_P2,V_P1,V_P2,S>>
    /\ Mutex_READ_P1'= "ko"
    \* () op�rateur [] fonction
    /\ T'=T \union {<<"out",f[V_P1]>>}

READ_P2 == 
    /\ \E w \in MyNat : <<"out",w>> \in T
    /\ Mutex_READ_P2 = "ko"
    /\ UNCHANGED <<Mutex_READ_P1,V_P1,S,V_P1>>
   \* soit v une valeur choisie dans l'ensemble T de la forme <<"data",val>>
    /\ LET val_p2 == CHOOSE v \in MyNat :  /\ (v \in MyNat) /\ (<<"out",v>> \in T)
        IN
            /\ V_P2'=val_p2
            /\ Mutex_READ_P2' = "ok"
            \* on supprime l'element de notre ensemble T
            \* attention on cr�e un ensemble  avec les {} que on intersect avec T
            /\ T' = T \ {<<"out",val_p2>>}

COMP_P2 == 
    /\ Mutex_READ_P2 = "ok"
    /\ UNCHANGED <<Mutex_READ_P1,V_P1,V_P2>>
    /\ Mutex_READ_P2'= "ko"
    /\ S' = S + V_P2
    /\ T'=(T \ {<<"somme",S>>}) \union {<<"somme",S'>>}  
 

Init == Mutex_READ_P1 = "ko" /\ Mutex_READ_P2 = "ko" /\ T = T0 /\ V_P1 = 0 /\ V_P2 = 0 /\ S = 0

Next == COMP_P1 \/ COMP_P2 \/ READ_P2 \/ READ_P1




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

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

=============================================================================
\* Modification History
\* Last modified Mon Jan 25 14:55:30 CET 2016 by arthur
\* Created Mon Jan 25 14:29:37 CET 2016 by arthur