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

[tlaplus] State sequences

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"


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.