Re: [tlaplus] Specifying non-invariant safety properties in TLC

-------------------------- 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

On 9 Jan 2020, at 19:46, ns <nedsri1988@xxxxxxxxx> wrote:

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

--
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.