UNCHANGED vars disjunct

[lemmy]

---- MODULE lockserver_nodefs ----
EXTENDS TLC, Naturals

Server == {"s1", "s2"}
Client == {"c1", "c2"}

VARIABLE semaphore
VARIABLE clientlocks
vars==<<semaphore, clientlocks>>

TypeOK ==
    /\ semaphore \in [Server -> {TRUE, FALSE}]
    /\ clientlocks \in [Client -> SUBSET Server]

\* Initially each server holds its lock, and all clients hold no locks.
Init == 
    /\ semaphore = [i \in Server |-> TRUE]
    /\ clientlocks = [i \in Client |-> {}]

Next == 
    \/ \E c \in Client, s \in Server : 
        /\ semaphore[s] = TRUE
        /\ clientlocks' = [clientlocks EXCEPT ![c] = clientlocks[c] \cup {s}]
        /\ semaphore' = [semaphore EXCEPT ![s] = FALSE]
    \/ \E c \in Client, s \in Server : 
        /\ s \in clientlocks[c]
        /\ clientlocks' = [clientlocks EXCEPT ![c] = clientlocks[c] \ {s}]
        /\ semaphore' = [semaphore EXCEPT ![s] = TRUE]
    \/ UNCHANGED vars

====

TypeError: Cannot read properties of null (reading 'fingerprint')
    at eval.js:412:45
    at Array.map (<anonymous>)
    at FcnRcdValue.fingerprint (eval.js:412:34)
    at TupleValue.fingerprint (eval.js:279:20)
    at evalEq (eval.js:1217:32)
    at evalBoundInfix (eval.js:1338:16)
    at evalBoundInfix (eval.js:2530:15)
    at evalExpr (eval.js:2075:16)
    at evalExpr (eval.js:2517:15)
    at evalExpr (eval.js:2066:16)

The problem appears to be UNCHANGED vars, whereas the equivalent formula UNCHANGED <<semaphore, clientlocks>> works fine.

[will62794]

The UNCHANGED vars construct should now be handled in the spec posted above, but there may still be some cases where UNCHANGED doesn't work correctly. I need to think on some of the details more to be clear whether the interpreter will handle all cases properly. Adding an upfront pre-processing step that expands all constants/definitions may help make some of this evaluation logic simpler.

[will62794]

Working spec.