作者热门文章
- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我已经编写了汉诺塔问题的 TLA+ 规范:
TEX
ASCII
------------------------------- MODULE Hanoi -------------------------------
EXTENDS Sequences, Integers
VARIABLE A, B, C
CanMove(x,y) == /\ Len(x) > 0
/\ IF Len(y) > 0 THEN Head(y) > Head(x) ELSE TRUE
Move(x,y,z) == /\ CanMove(x,y)
/\ x' = Tail(x)
/\ y' = <<Head(x)>> \o y
/\ z' = z
Invariant == C /= <<1,2,3>> \* When we win!
Init == /\ A = <<1,2,3>>
/\ B = <<>>
/\ C = <<>>
Next == \/ Move(A,B,C) \* Move A to B
\/ Move(A,C,B) \* Move A to C
\/ Move(B,A,C) \* Move B to A
\/ Move(B,C,A) \* Move B to C
\/ Move(C,A,B) \* Move C to A
\/ Move(C,B,A) \* Move C to B
=============================================================================
当我将 Invariant
公式指定为 Invariant 时,TLA 模型检查器将为我解决这个难题。
我想让它变得不那么冗长,理想情况下我不想将未更改的变量传递给 Move()
,但我不知道如何做。我想做的是写
Move(x,y) == /\ CanMove(x,y)
/\ x' = Tail(x)
/\ y' = <<Head(x)>> \o y
/\ UNCHANGED (Difference of and {A,B,C} and {y,x})
如何用 TLA 语言表达这一点?
最佳答案
您应该有一个序列,towers
,而不是变量 A、B、C,其中塔是索引。这还有一个优点是塔的数量是通用的。您的 Next
公式也会更短:
CanMove(i,j) == /\ Len(towers[i]) > 0
/\ Len(towers[j]) = 0 \/ Head(towers[j]) > Head(towers[i])
Move(i, j) == /\ CanMove(i, j)
/\ towers' = [towers EXCEPT ![i] = Tail(@),
![j] = <<Head(towers[i])>> \o @]
Init == towers = << <<1,2,3>>, <<>>, <<>> >> \* Or something more generic
Next == \E i, j \in DOMAIN towers: i /= j /\ Move(i, j)
或者,如果您想继续使用字母,您可以使用记录而不是塔的序列,并且您需要在我建议的规范中更改的是:
Init == towers = [a |-> <<1, 2, 3>>, b |-> <<>>, c |-> <<>>]
关于tla+ - 如何将公式转换为TLA+代码,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36392389/
我是一名优秀的程序员,十分优秀!