[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] The identifier is undefined or not an operator
You're absolutely right. Thank you for pointing that out!
I’ve corrected it, and I was able to finish solving the problem :
---------------------- MODULE Indy ------------------------------------------
EXTENDS Naturals, TLC
tau == [ I |-> 1, G |-> 2, W |-> 4, K |-> 8, L |-> 0 ]
maxt == 15
A == DOMAIN tau
L == "L"
max(S) == CHOOSE x \in S : \A y \in S : y <= x
Max(S) == max({tau[a] : a \in S})
ASSUME
/\ \A x \in A : tau[x] \in Nat
/\ maxt \in Nat
/\ L \in A
VARIABLES left, time
Type ==
/\ left \subseteq A
/\ time \in 0..maxt
Init ==
/\ left = A
/\ time = 0
DeuxActeursTraversent ==
\E a, b \in left \ {L} :
/\ L \in left
/\ left' = left \ {a, b, L}
/\ time' = time + Max({a, b})
UnActeurRevientAvecLampe ==
\E a, b \in A \ (left \union {L}) :
/\ L \in A \ left
/\ left' = left \union {a,b, L}
/\ time' = time + Max({a, b})
Next ==
/\ \/ DeuxActeursTraversent
\/ UnActeurRevientAvecLampe
/\ time' <= maxt
Target ==
/\ left = {}
/\ time <= maxt
=============================================================================
Best regards,
Amine
Le mercredi 19 mars 2025 à 08:26:16 UTC+1, Stephan Merz a écrit :
You certainly mean to write "\/" (disjunction) instead of "\union" (set union).
Hope this helps,
Hello everyone,
I'm working on a project where Indiana Jones and his team need to cross a bridge. I wrote some code, but I ran into this error:
The identifier left is undefined or not an operator: at line 24 in the method DeuxActeursTraversent.
I even tried simplifying Next to something like left' = left, but it still doesn’t work.
Any ideas?
---------------------- 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
=============================================================================
Le mercredi 19 mars 2025 à 08:26:16 UTC+1, Stephan Merz a écrit :
You certainly mean to write "\/" (disjunction) instead of "\union" (set union).
Hope this helps,
Hello everyone,
I'm working on a project where Indiana Jones and his team need to cross a bridge. I wrote some code, but I ran into this error:
The identifier left is undefined or not an operator: at line 24 in the method DeuxActeursTraversent.
I even tried simplifying Next to something like left' = left, but it still doesn’t work.
Any ideas?
---------------------- 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
=============================================================================
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/19851e58-bcf1-4e20-b9df-8c498dc6397cn%40googlegroups.com.