TLA+1.8模型检查器运行示例无状态生成且无行为规范可选问题

问题描述 #

我正在学习教程 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)

模型配置截图 #

问题疑问 #

我不理解为何配置默认选中“No Behaviour Spec”，选项列表中没有其他可选内容，但教程中选择的是“Temporal Formula”选项，请问该选项在哪里可以找到？

解决方案 #

你遇到的问题是TLC未加载模块定义的行为规范，所以无法识别初始状态，按以下步骤操作即可解决：

• 首先确认PlusCal代码已经完成翻译，你贴出的代码里已经自动生成了Spec时序公式，满足运行要求。
• 打开模型配置页找到「What is the behaviour spec?」板块，点击「Temporal formula」单选框，在下方输入框填写Spec，就是模块翻译生成的时序公式名称。
• 如果看不到「Temporal formula」选项，先检查当前模型是否绑定了正确的.tla模块，确认模块无语法错误、翻译过程无报错，只要模块内有合法的时序公式定义，该选项就会自动出现在配置页。
• 保存配置后重新运行模型即可正常生成状态，同时会触发你编写的断言报错（因为money取值范围是1~20，当取值大于10时Alice账户余额会变为负数，不符合断言要求）。

内容的提问来源于stack exchange，提问作者ffff