[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: than...@xxxxxxxxx*Date*: Tue, 22 May 2018 18:57:57 -0700 (PDT)

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

**Follow-Ups**:**Re: How to end an increacing number TLA+ specification?***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] No detailed information from TLA+ Parser Error** - Next by Date:
**Re: How to end an increacing number TLA+ specification?** - Previous by thread:
**Re: [tlaplus] No detailed information from TLA+ Parser Error** - Next by thread:
**Re: How to end an increacing number TLA+ specification?** - Index(es):