RE: [tlaplus] Using VIEW to check temporal properties of monotonic systems

Hello Andrew,

We faced the same problem. Maybe our approach with wrap around and checking that the comparison for the sequence numbers is only performed between values where the relation is certain can be an inspiration for your solution:

https://github.com/stresch/pingpong/blob/master/seqnr.tla

Kind regards,

Stefan

From: tlaplus@xxxxxxxxxxxxxxxx <tlaplus@xxxxxxxxxxxxxxxx> On Behalf Of Andrew Helwer
Sent: Wednesday, February 17, 2021 8:58 PM
To: tlaplus <tlaplus@xxxxxxxxxxxxxxxx>
Subject: [tlaplus] Using VIEW to check temporal properties of monotonic systems

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/74870f61-4b86-455f-9d8f-b90f9769b3dcn%40googlegroups.com.