Search code examples
prooftla+

TLA+ model checker fails to generate states

I've been following this course https://learntla.com/introduction/example/ however I'm having difficulty running the model. It does not generates any states at all

Version TLA+ = 1.8

------------------------------ MODULE Example ------------------------------


=============================================================================
\* Modification History
\* Last modified Fri Sep 03 17:43:29 IST 2021 by faish
\* Created Fri Sep 03 17:15:54 IST 2021 by faish

EXTENDS Naturals, TLC
(* --algorithm transfer
variables alice_account = 10, bob_account = 10, money \in 1..20

begin
A: alice_account := alice_account - money;
B: bob_account := bob_account + money;
C: assert alice_account >= 0;

end algorithm*)
\* BEGIN TRANSLATION (chksum(pcal) = "4f516040" /\ chksum(tla) = "66759d32")
VARIABLES alice_account, bob_account, money, pc

vars == << alice_account, bob_account, money, pc >>

Init == (* Global variables *)
        /\ alice_account = 10
        /\ bob_account = 10
        /\ money \in 1..20
        /\ pc = "A"

A == /\ pc = "A"
     /\ alice_account' = alice_account - money
     /\ pc' = "B"
     /\ UNCHANGED << bob_account, money >>

B == /\ pc = "B"
     /\ bob_account' = bob_account + money
     /\ pc' = "C"
     /\ UNCHANGED << alice_account, money >>

C == /\ pc = "C"
     /\ Assert(alice_account >= 0, 
               "Failure of assertion at line 16, column 4.")
     /\ pc' = "Done"
     /\ UNCHANGED << alice_account, bob_account, money >>

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == pc = "Done" /\ UNCHANGED vars

Next == A \/ B \/ C
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")

\* END TRANSLATION

Here is the console output

Starting... (2021-09-03 18:07:58)
Computing initial states...
Finished computing initial states: 0 distinct states generated at 2021-09-03 18:08:03.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 0.0
Progress(1) at 2021-09-03 18:08:03: 0 states generated (0 s/min), 0 distinct states found (0 ds/min), 0 states left on queue.
0 states generated, 0 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 1.
Finished in 6116ms at (2021-09-03 18:08:03)

Here is the model enter image description here

I don't understand why it's choosing "No Behaviour Spec". The option list doesn't have anything else in it. The course however selects a "Temporal Formula". Where do I find that option?

Solution

  • TLC ignores everything below the ==== line. Move that after the "End Translation" line, and then in the model, under What is the Behavior Spec, set it to Temporal Formula and set the formula to Spec. Then it should work.