Thanks, I see that my first attempt was not math, but an thinly veiled instruction to what TLC ought to do. I evidently have a lot of programmer quirks to iron out.
Another thing I realized was that my usage of helpers hid the fact that I tried to set the next state of locks twice per action.
The following rewrite works as intended:
OpenWorkspace(u, w) == /\ locks[w] <= 0
/\ openWorkspaces' = [openWorkspaces EXCEPT ![u] = openWorkspaces[u] \cup {w}]
/\ locks' = [c \in Workspaces |-> IF c = w THEN 10 ELSE locks[c] - 1]
EditWorkspace(u, w) == /\ locks[w] > 0
/\ w \in openWorkspaces[u]
/\ locks' = [c \in Workspaces |-> IF c = w THEN 10 ELSE locks[c] - 1]
/\ UNCHANGED openWorkspaces
CloseWorkspace(u, w) == /\ locks[w] > 0
/\ openWorkspaces' = [openWorkspaces EXCEPT ![u] = openWorkspaces[u] \cap {w}]
/\ locks' = [c \in Workspaces |-> IF c = w THEN 0 ELSE locks[c] - 1]
Next == \/ \E u \in Users, w \in Workspaces : OpenWorkspace(u, w)
\/ \E u \in Users, w \in Workspaces : EditWorkspace(u, w)
\/ \E u \in Users, w \in Workspaces : CloseWorkspace(u, w)
It's a silly and naïve specification, but I'm having a lot of fun playing around with it. :)
On Sunday, February 2, 2020 at 2:35:36 AM UTC+1, Leslie Lamport wrote:
Please look up CHOOSE and see what
CHOOSE u \in Users : ...
means. Then look up \E and see what
\E u \in Users : ...
means.