如何使用TLA+定义顺序操作

Question

假设我有一组简单的顺序操作(我将首先强制定义(：

start(a, 1)
move(a, 3)
move(a, 5)
move(a, 4)
move(a, 2)

也就是说，我们有一个游戏棋子a，并在位置1开始它。然后我们依次将其移动到3，然后移动到5，然后移动4，然后移动2。每一步一次。

您将如何使用TLA+来定义这一点？试图将我的思想集中在如何在TLA+中指定复杂的命令式操作序列上。

Answer 1

问题中描绘的行为可以在TLA+中描述如下：

---- MODULE Steps ----
VARIABLE a

Init == a = 1
Next == / / a = 1
/ a' = 3
/ / a = 3
/ a' = 5
/ / a = 5
/ a' = 4
/ / a = 4
/ a' = 2
Spec == Init / [][Next]_a / WF_a(Next)
=====================

变量a的行为由时间公式Spec指定(其他变量可以以任意方式表现(。

变量a开始等于1(通过连词Init(，时间步长要么保持a不变，要么将其从1变为3。如果发生这种变化，则以下时间步骤要么保持a不变，要么将其从3更改为5。对CCD_ 9的值的改变可以持续到CCD_。无法对a进行进一步更改。一旦a等于2，它就永远等于2。这些是a的可能变化，如连词[][Next]_a所指定的，其表示[](Next / UNCHANGED a)，即[](Next / (a' = a))，符号[]表示"；总是"；。

连词Init和[][Next]_a指定了一个安全属性。安全是指可能发生的事情，而不是必须发生的事情。Liveness(必须发生的事情(是用连词WF_a(Next)指定的，它描述了弱公平性。公式WF_a(Next)要求，如果满足公式Next和的步骤不间断地改变变量a的值，则最终必须发生这样的步骤。

换句话说，如果可以通过采取满足Next的步骤(<<Next>>_a-步骤(来改变变量a，则a不能永远保持不变，而是必须最终以Next所描述的方式改变。实际上，当a不是2，而是1、3、5或4时，动作<<Next>>_a(这意味着Next / (a' # a)，即Next和a改变值(被启用，因此a将保持改变，直到它达到值2。当a为2时，<<Next>>_a变为禁用状态。

Answer 2

有很多方法可以做到这一点，但脑海中浮现出两个简单的解决方案；第一个使用宏：

---- MODULE Steps ----
VARIABLE a
move(start, end) ==
/ a = start
/ a' = end
Init ==
/ a = 1
Next == 
/ move(1, 3)
/ move(3, 5)
/ move(5, 4)
/ move(4, 2)
Spec ==
/ Init
/ [][Next]_a
=====================

请注意，只有当你的动作序列没有恢复到相同的状态时，上述操作才会起作用。如果是这样，您将不得不添加类似pc"的内容；程序计数器"；变量和序列和yada yada。。。在这一点上，你可能会更好地使用PlusCal，这是一种TLA+变体，通常更适合于编写顺序操作：

---- MODULE Steps ----
(* --algorithm Steps
variables a = 1;
begin
a := 3;
a := 5;
a := 4;
a := 2;
end algorithm; *)
=====================

在TLC运行之前，必须将其转换为TLA+。使用

TLA+工具箱中的CTRL+T

VS代码扩展中的Parse module命令

带CLI的java pcal.trans Steps.tla