|
Let's say we have three "blinkers", which flip between TRUE and FALSE: EXTENDS Integers, TLC Next == ??? Spec == Init /\ [][Next]_vars If I want to change one of the blinkers per step, I can do it the usual way: Next == But what if I want to change any number of them? EXCEPT syntax doesn't support that. I've usually seen it done as: Next == So why can't we just do this? Because it doesn't fully specify f'. For all
we know, f' has the domain Int instead of 1..3, and it
doesn't specify what happens to the elements not in the
set. We also can't write DOMAIN f' = 1..3
because TLC can't check that, even though it's a valid TLA+
_expression_. But there's a trick we can use: the first time TLC encounters encounters a primed variable, it uses that the generate the potential next-states for that variable. We need to write either f' = ... or f' \in ... . But after that, TLC can use f to determine whether or a given action is enabled or not. We can use f' as an action constraint! Next == This works, as it fully defines f' in a way that's checkable by TLC. Practically speaking, this style is probably worse than the other two solutions. For one, it doesn't work on non-enumerable ranges. Nonetheless it's pretty neat. H 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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/1178a27b-9a02-56a7-4708-5079c9eaec24%40gmail.com. For more options, visit https://groups.google.com/d/optout. |