- 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/
我正在为 TLA+ 中的主-备份协议(protocol)建模,并在元组中进行复制配置。一些设置 TLA+: NNodes == 3 Nodes == 1..NNodes 然后,在 Pluscal 算法
我正在使用 VS Code 和 vscode-tlaplus 插件而不是 TLA+ 工具箱来学习 TLA+。现在我有了这个 TLA 文件,我在其中定义了一些常量: ---- MODULE test -
变量state代表系统的状态,例如state\in {"ready", "prepare", "do", "cleanup", "done"}。如何表达 state 最终应通过所有五个状态(以任何顺序
我是一个新的TLA+用户。 我读到TLA工具箱允许我们在完成模型检查后可视化状态图。 为了这样做,需要安装我所做的dot。 但是我不知道如何启动可视化。 我可以使用GUI进行购买吗?还是需要使用专用的
请给我一些关于 TLA+ 中的项目主题的建议语。我正在学习语言类(class),这是我学习规范和验证的第一年,我不知道在两周内选择实现什么。有任何想法吗? 最佳答案 使用 TLA+ 的常见玩具项目如下
我已经编写了汉诺塔问题的 TLA+ 规范: TEX ASCII ------------------------------- MODULE Hanoi -----------------------
我有两套: X = {a, b} Y = {1, 2, 3} 我想生成以下一组对: {>, >, >} {>, >, >} {>, >, >} {>, >, >} ... {>, >, >} 在每个集
我有一个规范,我试图定义一个 LRU 缓存系统,我遇到的一个问题是如何从结构键/值对(基本上是字典或哈希映射)中删除值其他语言)。 到目前为止,这是规范本身(不完整): EXTENDS Integer
我正在使用正则表达式 System.Text.RegularExpressions.Regex.Replace(stringToSplit, "([A-Z])", " $1").Trim() 按大写字
实际上,我想从 1..N 构建一个 {"1", "2", "3", ..., "N"} 集> 设置。如何将数字转换为字符串? 最佳答案 TLC 模块提供了一个ToString 运算符。 关于forma
我有一系列看起来像这样的字符值。我希望它们看起来像这样。 然而,我有一组词,当完全匹配时,它们应该保持原样。在此列表中将包含 ABC 之类的内容。 对于输入 六六十个测试对象 不包括“六” 所需的输出
正如我读到的: http://docs.oracle.com/cd/E13150_01/jrockit_jvm/jrockit/geninfo/diagnos/tune_app_thruput.htm
我目前正在撰写硕士论文,面临着在时间逻辑中指定和验证我的方法。 在我的情况下,哪种时序逻辑最适合使用?我真的很想得到一些关于我的方法以及如何继续的反馈 我的模型由参与者组成,这些参与者将同时执行。对于
我是一名优秀的程序员,十分优秀!