Specifying non-invariant safety properties in TLC

[ns]

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

[Stephan Merz]

Hello,

the standard way to check such properties is to express them as a state machine and then verify that your system specification refines that state machine. For your example, we could create the following module

-------------------------- MODULE NoCashBeforePin --------------------------

VARIABLES pin, cash

Init ==

  /\ pin \in BOOLEAN

  /\ cash \in BOOLEAN

  /\ ~ pin => ~ cash

  

Next == pin' = TRUE /\ cash' \in BOOLEAN

Spec == Init /\ [][Next]_<<pin,cash>> 

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

then add the following line to your main ATM specification

Prop == INSTANCE NoCashBeforePin

and use TLC to verify the temporal property Prop!Spec. Of course, you don't have to place the property state machine in a separate module, and you may tweak the way you formulate the property state machine if you find it too obscure. (The above assumes that pin entry and dispensing of cash happens only once, you may want to reset the state machine if you want to reuse the ATM. The point is to rule out that pin is set to TRUE before cash is.)

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