[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Specifying non-invariant safety properties in TLC

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)


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 on the web visit https://groups.google.com/d/msgid/tlaplus/ebf0f6ed-40e1-4135-89d7-5e5b051faa5f%40googlegroups.com.