Hello, I'm interested in safety properties that aren't state invariants. For example the book
Principles of Model Checking has an example of such a safety property in the context of an ATM example: "No cash is dispensed unless the correct PIN was previously entered". I'm wondering how to express such a requirement in TLA+?
Below is my attempt at formalizing a very trivial ATM in TLA that waits for a correct PIN, displays a brief message, and then dispenses the cash:(this deadlocks, that's fine)
VARIABLES msg, pin, cash
vars == <<msg,pin,cash>>
Init == pin=FALSE /\ cash=FALSE /\ msg=FALSE
Pin == pin \in BOOLEAN /\ pin' \in BOOLEAN
Msg == msg \in BOOLEAN /\ msg' \in BOOLEAN
ATM ==
\/ (~pin /\ pin'=TRUE /\
msg'=TRUE /\ UNCHANGED cash)
\/ (msg /\
cash'=TRUE /\ msg'=FALSE /\ UNCHANGED pin)
Next == Pin /\ Msg /\ ATM
Spec == Init /\ [][Next]_vars
I would like to say something like ~(~pin U cash)
Thanks