[tlaplus] State sequences

[ns <nedsri1988@xxxxxxxxx>]

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!

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