function - 如何使用 TLA+ 定义顺序动作？

Question

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

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

也就是说，我们有一个棋子a并在 position 开始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步骤不间断地启用，那么这个步骤必须最终发生。

换句话说，如果可以a通过采取满足Next（a <<Next>>_a-step）的步骤来改变变量，那么a就不能永远保持不变，而最终必须以 描述的方式改变Next。事实上，whilea不是 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 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在 TLA+ 工具箱中
• Parse moduleVS Code 扩展中的命令
• java pcal.trans Steps.tla使用 CLI