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 忽略 ==== 行以下的所有内容。将其移到“结束翻译”行之后，然后在模型中的 What is the Behavior Spec 下，将其设置为 Temporal Formula 并将公式设置为 Spec。然后它应该工作。

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

TLA+ model checker fails to generate states

proof

tla+