---------------------- MODULE Indy ------------------------------------------
EXTENDS Naturals, TLC
tau == [ I |-> 1, G |-> 2, W |-> 4, K |-> 8, L |-> 0 ]
maxt == 15
A == DOMAIN tau
L == "L"
N == Nat
max(S) == CHOOSE x \in S : \A y \in S: y \leq x
Max(S) == max( {tau[a] : a \in S} )
ASSUME
/\ \A x \in A : tau[x] \in N
/\ maxt \in N
/\ L \in A
VARIABLES left, time
Init ==
/\ left = A
/\ time = 0
DeuxActeursTraversent ==
\E a, b \in left : (left' = left \ {a,b,L}) /\ (time' = time + Max({tau[a], tau[b]}))
UnActeurRevientAvecLampe ==
/\ \E a \in A \ left : (left' = left \union {a,L}) /\ (time' = time + tau[a])
Next == DeuxActeursTraversent \union UnActeurRevientAvecLampe
Inv ==
/\ left \subseteq A
/\ time <= maxt
Target ==
left = {}
/\ time <= maxt
=============================================================================