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 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:
My questions about these options are as follows:
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/7372981851c946adb7381ddf6b1cb3e5%40thalesgroup.com. |