than...@gmail.com
unread,May 22, 2018, 10:19:38 PM5/22/18Sign in to reply to author
Sign in to forward
You do not have permission to delete messages in this group
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to tlaplus
Hi all,
I have meet a problem in TLA+. Some algorithm use an increasing number to ensure it correntness. A simple specification like bellow, as the TLC model checking process of the exapmle specification never ends, so we can not conclude the result of the specification.
My question is how to modify the specification the let it end gracefully? Is it a typical case and have a known solution?
Thanks.
VARIABLES a, b
vars == << a, b >>
Init == (* Global variables *)
/\ a = 1
/\ b = 2
Next == \/ /\ a' = a + 2
/\ b' = b
\/ /\ b' = b + 2
/\ a' = a
Spec == Init /\ [][Next]_vars
Invariant == a /= b