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
--
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...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/74870f61-4b86-455f-9d8f-b90f9769b3dcn%40googlegroups.com.
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
--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7684095c-caaf-49e7-adf4-cbc360b7714dn%40googlegroups.com.
On 1 Mar 2021, at 02:28, Andrew Helwer <andrew...@gmail.com> wrote:Is VIEW documented anywhere? As in, how to write a VIEW function and what is valid/invalid VIEW function syntax?
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ed776f20-b23d-48ce-a4aa-1a5cb37398cbn%40googlegroups.com.