如何使用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。将值更改为a可能一直持续到a = 2为止。对a的进一步更改是不可能的。一旦a变为等于2，它就永远等于2。这是a可能发生的变化，这是由连词[][Next]_a所指定的，意思是[](Next \/ UNCHANGED a)，即[](Next \/ (a' = a))，符号[]的意思是“总是”。

联合Init和[][Next]_a指定一个安全属性。安全是关乎可能发生的事，而不是一定要发生的事。活性(必须发生的事情)由连词WF_a(Next)指定，它描述弱公平性。公式WF_a(Next)要求，如果不间断地启用满足公式Next并更改变量a值的步骤，则最终必须执行此步骤。

换句话说，如果可以通过采取满足Next (a <<Next>>_a-step)的步骤来更改变量<<Next>>_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; *)

=====================

必须将其转换为TLA+，然后才能由TLC运行。使用

• CTRL+T在VS代码extension
• java pcal.trans Steps.tla中的TLA+ toolbox
• Parse module命令中使用CLI