英文:
TLC passes property but the state is not existed
问题
我是TLA+的新用户。以下的代码可能有点傻。这是我私有代码的精简版本。在下面的代码中没有将END赋值给s，但Prop在TLC模型检查中通过而没有错误。
我无法弄清楚为什么它会通过。我的代码可能存在问题。有人可以解释一下吗？TLA+版本是1.7.1。操作系统是Ubuntu 20.04。谢谢。
英文:
I'm a new user of TLA+. The following code might be silly. It's a narrowed-down version of my private code.
There are no lines assigning END to s on the following code but the Prop passes without error on TLC model check.
----------------------------- MODULE notExisted -----------------------------
EXTENDS Sequences
VARIABLES s, q
Init == /\ s = "S0"
/\ q = <<>>
sub_nxt == /\ q' = Append(q, "wow")
/\ UNCHANGED<<s>>
Next == \/ /\ s = "S0"
/\ s' = "S1"
/\ UNCHANGED<<q>>
Spec == /\ Init
/\ [][Next]_<<s,q>>
/\ SF_<<s,q>>(sub_nxt)
Prop == []<>(s = "END")
=============================================================================
I can't figure out why it passes. There might be bad pattern on my code.
Can anyone explain?
The TLA+ version is 1.7.1.
The OS is Ubuntu 20.04.
Thanks.
答案1
得分: 0
这是一个自问自答。
我查阅了指定系统的"14.3.5 有限性检查的限制"，最终弄清楚了问题所在。我认为...
因为规范是有限的，而sub_nxt始终为真，所以SF为假。
在这种情况下，SF_<<s, q>>(sub_nxt) => []<>(s = "END")是真的。
当A为假时，A => B是真的。
我还尝试了以下内容，也通过了。
EXTENDS Integers
VARIABLE x
Spec == (x=0) /\ [][x' = x + 2 /\ x < 10]_x /\ WF_x(x' = x + 2)
Prop == []<>(x=1)
=============================================================================
英文:
It is a self-answer.
I checked Specifying Systems "14.3.5 Limitations of Liveness Checking" and finally figured out what was wrong. I think...
The SF is False since the Spec is finite and sub_nxt always true.
In that case, the SF_<<s,q>>(sub_nxt) => []<>(s = "END") is true.
The A => B is true when A is false.
I've also tried following and it also passes.
--------------------------- MODULE LimOfLivCheck ---------------------------
EXTENDS Integers
VARIABLE x
Spec == (x=0) /\ [][x' = x + 2 /\ x < 10]_x /\ WF_x(x' = x + 2)
Prop == []<>(x=1)
=============================================================================
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论