I am learning TLA+ now, and I want to write a testing spec to exercise as below:
-------------------------------- MODULE Sum --------------------------------
EXTENDS Naturals, TLC
CONSTANT sum
VARIABLE x,y
vars == <<x,y>>
Init == /\ x \in 1..10
/\ y \in 1..10
Next == IF (x+y#sum) THEN /\ x' = RandomElement(1..10)
/\ y' = RandomElement(1..10)
/\ PrintT(<<x,y>>)
ELSE /\ PrintT(<<x,y>>)
/\ UNCHANGED <<x,y>>
Liveness == WF_vars(Next)
Property1 == <>(x+y=10)
Spec == Init /\ [][Next]_<<vars>>
=============================================================================
\* Modification History
\* Last modified Tue Jan 30 18:25:46 CST 2018 by stephen
\* Created Tue Jan 30 17:53:14 CST 2018 by stephen
The purpose of this spec is make summation of two variables equal 10, and keeping the values unchanged when the summation is 10. The following picture is the Model Checking Results:
1. why Temporal properties were violated at State(num=1) rather than other states?
2. Can I use Property1 == <>(x+y=10) to verify that x+y eventually equlas to 10? or at some time x+y equals to 10? or what is the right temporal property to verify this?
3. Can anybody point out as much as possible errors in this spec and tell me the reason?
I appreciate,
Yong