TLA+模型检查器无法生成状态

Question

我一直在学习这个课程，https://learntla.com/introduction/example/，但是我在运行这个模型时遇到了困难。它根本不会生成任何状态

版本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 

以下是控制台输出

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)

这是模型

​

我不明白为什么它会选择“无行为规范”。选项列表中没有任何其他内容。然而，该课程选择了一个“时间公式”。我在哪里可以找到这个选项？

Answer 1

TLC会忽略====行以下的所有内容。将其移动到"End Translation“行之后，然后在模型中的What is the Behavior Spec下，将其设置为Temporal Formula，并将公式设置为Spec。那么它应该是有效的。