The identifier is undefined or not an operator

[Amine BOUFTILZ]

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 

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

[Stephan Merz]

You certainly mean to write "\/" (disjunction) instead of "\union" (set union).

Hope this helps,

Stephan

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/4d46a9f0-b93a-4956-9c5a-693577922f8en%40googlegroups.com.

[Amine BOUFTILZ]

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