State sequences

[ns]

hello, I was wondering if there was a convenient way to specify a required sequence of states in TLA+. As an example, suppose the code 3 2 1 unlocks something, we would like to say 

Next ==

       ...

\/    num = 3 /\ num'=2 /\ num''=1 /\ unlock'''

      ...

and the usual [] [Next]_{vars}. I would like for this to mean

  [] (Next \/ (num'=num /\ unlock'=unlock) \/ (num''=num' /\ unlock''=unlock') \/ (num'''=num'' /\ unlock'''=unlock'') 

but I don't know if there's a way to write this easily in TLA"

thanks!

[Stephan Merz]

You cannot nest primes in TLA+ formulas, for good reasons related to stuttering invariance. You want to specify a state machine that monitors the progress of unlocking. Perhaps something along the following lines:

Digit == 0 .. 9

CONSTANT Code  \* can be instantiated to <<3,2,1>>, for example

ASSUME Code \in Seq(Digit)

VARIABLES 

  locked,   \* status of the lock

  idx       \* monitor progression in input of the code

Init ==

  /\ locked = TRUE

  /\ idx = 1

Input(x) ==

  \/ \* user input correct digit

     /\ idx <= Len(Code) /\ x = Code[idx]

     /\ idx' = idx+1

     /\ locked' = (idx < Len(Code))  \* unlock when last digit has been input

  \/ \* user input incorrect digit

     /\ idx <= Len(Code) /\ x # Code[idx]

     /\ idx' = Len(Code)+1  \* make further inputs useless

     /\ locked' = locked

  \/ \* ignore input when beyond the length of the code

     /\ idx > Len(Code)

     /\ UNCHANGED <<locked, idx>>

Spec == Init /\ [][\E x \in Digit : Input(x)]_<<locked,idx>>

The last disjunct of the Input action is in fact useless here, since stuttering is always allowed, but it may be useful when interaction with the user is modeled through an explicit interface. Also, you may choose to have a different strategy of handling input errors such as tolerating a certain number of wrong inputs before blocking.

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/c9a1dbdf-33f5-4b1e-a3cf-4c42202ce33d%40googlegroups.com.

[ss.ne...@gmail.com]

hi Stephan, thanks for the suggestion. I was doing something similar using variables checking1, checking2, etc, although I prefer your approach as its more compact. Nevertheless even this approach still seems long-winded compared to what I would like to have written. I know its not possible to write it that way in TLA+, but would my solution work in principle - I thought I'd taken  care of the stuttering issue.

thanks

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

[Stephan Merz]

I thought I'd taken  care of the stuttering issue.

Not really: as far as I understand, your specification requires that either three stuttering steps happen in a row or the three non-stuttering steps occur without interruption. It does not accommodate the step num = 3 /\ num'=2 being followed by a stuttering step, for example.

Stephan

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/80d2e6d4-2a17-4319-8a9e-d900f8f77be1%40googlegroups.com.