logic - 使用 TLA+(动作的时间逻辑)指定多个步骤
问题描述
浏览此处主要显示了操作规范的简单示例,您可以在其中使用 引用下一个状态'
,如下所示:
UponV1(self) ==
/\ pc[self] = "V1"
/\ pc' = [pc EXCEPT ![self] = "AC"]
/\ sent' = sent \cup { <<self, "ECHO">> }
/\ nCrashed' = nCrashed
/\ Corr' = Corr
例如,/\ nCrashed' = nCrashed
是一个逻辑语句“...AND next(nCrashed) == this(nCrashed)`。所以基本上,上述函数将一些变量设置为“处于下一个状态”。但这一切基本上都是一步完成的(至少在逻辑上)。
我想知道的是如何定义在多个步骤中发生的事情。说 10 步。
UpdateWithTenSteps(self) ==
/\ foo' = foo + 1
/\ bar'' = foo' + 1
/\ baz''' = bar'' + 1
/\ ...
....
所以“在第三个状态之前,baz 会被设置为 bar 在第二个状态加一”。类似的东西。但这没有任何意义。在命令式语言中,您只需执行以下操作:
function updateInTenSteps() {
incFoo()
incBar()
incBaz()
}
但这是有道理的,因为每个函数调用都发生在前一个函数调用之后。但我不知道如何在 TLA+ 中表示这一点。
想知道你应该如何完成在动作的时间逻辑+中需要不止一步的事情。另一个例子是while循环。
解决方案
TLA 被设计成只考虑当前状态和后继状态(或整个行为)。您总是可以通过引入一个显式变量来拆分多个相互依赖的步骤,该变量告诉您哪些分配已经完成:
EXTENDS Naturals
Labels == { "foo", "bar", "baz", "fin" } (* just for documentation purposes *)
VARIABLE currstate, foo, baz, bar
Init == /\ currstate = "foo"
/\ foo = 0
/\ bar = 0
/\ baz = 0
Next == \/ (currstate = "foo" /\ currstate' = "bar" /\ foo' = foo +1 /\ UNCHANGED <<bar,baz>>)
\/ (currstate = "bar" /\ currstate' = "baz" /\ bar' = foo +1 /\ UNCHANGED <<foo,baz>>)
\/ (currstate = "baz" /\ currstate' = "fin" /\ baz' = bar +1 /\ UNCHANGED <<foo,bar>>)
\/ (currstate = "fin" /\ UNCHANGED <<foo,bar,baz,currstate>>
如果为此创建一个模型,设置由Init
and 定义的行为Next
,然后检查不变量baz = 0
,您将获得一个跟踪,显示导致 baz 更改的状态(您的最后一个任务)。循环只是将后继标签分配为已经发生的标签(例如,而不是定义baz' = "foo"
)。
Pluscal 转换为 TLA 的工作方式类似:每个标记的行对应一个 id,从第 l 行到第 m 行的每个转换都会将下一个状态的程序计数器从 l 更改为 m。
推荐阅读
- node.js - 如何在 docker 文件中使用 DEBUG 命令运行节点服务器?
- ios - Flutter iOS pod未安装
- javascript - 更新 React Native Android 后 OneSignal 无法正常工作
- vb.net - 如何更改比较多个文本框
- tabs - 在 Materialise 1.0.0 中切换选项卡的问题
- python - 如何遍历每 10 秒刷新一次的 Web 元素列表?
- java - 在 Apache JsonToStringStyle 中格式化日期
- python - 为什么“浏览”方法使用不存在的 id 返回错误的记录集?
- javascript - react-native 的水平滑块插件
- json - 如何从文件中获取所有 JSON 名称并将其存储到字符串中