> For option (2), is such a thing even possible with VIEW?Yes! The VIEW can be any TLA+ _expression_. (Er, excluding temporal operators and primed variables.) It is not restricted to being a sequence of variables.One way to achieve what you want---the best way I think---is to write a VIEW that strips out or transforms the sequence values in messages.> For option (2), it kind of seems like if I could define such a VIEW, I would be sort of assuming that the sequence counter just doesn't matterYou're absolutely right. Most likely you will need to transform (rather than strip) the sequence values, and you will need to be extremely careful about how you do it, so that you do not change the meaning of your spec. How are the sequence values used? Are they recorded timestamps that capture moments in the past, or are they deadlines that indicate moments in the future, or are they something more complicated?An interesting question you should ask yourself is what property of the counter value lends correctness to the algorithm? Is it that the new value is greater than all previous values over the history of the program, greater than all values that are currently "used" somewhere in the system, or merely unique among all values that currently exist in the system?
If, say, it is the last, you could declare a CONSTANT set, CounterValue and an operator, Unique(c), that is true iff the value c is currently unused in the system (even though you wouldn't be able to implement such an operator in the real system), and then, instead of, say, counter' = counter' + 1 ∧ ..., do something like ∃ c ∈ CounterValue : (Unique(c) ∧ counter’ = c ∧ …). You could then check with CounterValue being a small symmetry set. Establishing that an incrementing natural number is a refinement would then be a simple matter.
Even if correctness stems from the second option, you could do something a little more elaborate, that defines an order relation on CounterValue that changes with each step (imagine an order relation based on the position of the set’s elements in some sequence, and when elements are no longer used in the system, they are removed from the head and added at the tail).
— Ron
On Wednesday, February 17, 2021 at 7:58:25 PM UTC andrew...@xxxxxxxxx wrote:In Leslie's 2005 paper Real Time is Really Simple, he describes a system with a clock variable now which increases monotonically. Ordinarily to model check such a system you'd have to add a state restriction on now to ensure the state space is finite. Of course, this approach only works for safety properties: section 14.3.5 of Specifying Systems describes how state restrictions interfere with more general temporal properties, usually by invalidating fairness assumptions. The Real Time paper works around this problem with the use of VIEW, which is a statement in the CFG file that directs TLC to only use a subset of the specification's variables when determining whether a state has been visited before. Ignoring the now variable ensures the state space is finite and makes possible the checking of general temporal properties, when combined with clever spec-writing that avoids embedding absolute timestamps in other variables.I am writing a spec with both a now variable and also a monotonically-increasing message sequence counter, seq. Unfortunately the nature of message sequence counters means that the counter value is attached to each message as it is sent, which "contaminates" other variables with monotonically-increasing values and means I can't just use VIEW to ignore both now and seq. It seems I am faced with two options if I want to verify temporal properties:
- Rewrite the spec to quarantine (or even remove) references to the monotonically-increasing sequence counter
- Somehow write a more advanced state function than VIEW seems to provide, more similar to ALIAS, with which I could strip out embedded sequence counter values
My questions about these options are as follows:
- For option (1), does anyone else have experience writing a spec of a system using a monotonically-increasing message counter, with wisdom they could provide?
- For option (1), is it likely I could establish a refinement relationship between the old & new spec (or vice-versa), or will this unavoidably run afoul of the infinite state space problem?
- For option (2), is such a thing even possible with VIEW?
- For option (2), it kind of seems like if I could define such a VIEW, I would be sort of assuming that the sequence counter just doesn't matter, which seems a fairly large assumption requiring more examination (and I probably end up back in option 1 establishing refinement relationships anyway). Leslie is quite careful in his Real Time paper while establishing that the system is symmetric under a VIEW ignoring now.
Thanks for any help or guidance y'all can provide!Andrew--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...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7684095c-caaf-49e7-adf4-cbc360b7714dn%40googlegroups.com.