行为

到目前为止，我们已经了解了PlusCal的基本知识以及如何运行模型。我们还看到，如果我们的起始变量被指定为一个集合，它将扩展TLC可以搜索的状态空间。这需要我们编写有用的specifications。最后一步是添加不同的行为：允许系统在给定的步骤中做不同的事情。在单一的进程PlusCal算法中，有两种简单的方式来引入并发性：with语句和either语句。

Either

either看起来都很像一个基本的if语句。其语法如下：

either
  skip;
or
  skip;
or
  skip;
end either;

需要注意的是TLC将运行每个分支。当它遇到任意一个时，它创建一个单独的行为并为每个行为执行一个不同的分支。例如：

variables x = 3, i = 2;
begin
while i > 0 do
  either 
    x := x + 2;
  or 
    x := x * 2;
  end either;
  i := i - 1;
end while

内循环将发生两次。每次模型可以添加两个或两个x，这意味着有四个可能的最终结果:

With

with的作用的是一样的，除了为每个可能的分支创建一个新的行为之外，它还为集合中的每个元素创建一个行为。在下面的情况下，我们有三个可能的行为:

with a \in {1, 2, 3} do
  x := x + a
end with;

这将为集合中的每个元素创建一个单独的时间线。

例子

描述一个系统，该系统有三个标志，打开和关闭，还有一个更改标志的状态。

现在我们在实际操作上有一些限制，但是我们已经可以开始构建简单的模式了。这里有一种写法：

---- MODULE flags ----
EXTENDS TLC, Integers
(* --algorithm flags
variables f1 \in BOOLEAN, f2 \in BOOLEAN, f3 \in BOOLEAN
begin
  while TRUE do
    with f \in {1, 2, 3} do
      if f = 1 then
        either
          f1 := TRUE;
        or
          f1 := FALSE;
        end either;
      elsif f = 2 then
        either
          f2 := TRUE;
        or
          f2 := FALSE;
        end either;
      else
        either
          f3 := TRUE;
        or
          f3 := FALSE;
        end either;
      end if;
    end with;
  end while;
end algorithm; *)

====

这并不是最理想的写法，但我想在这里同时展示with和either。你可以用这两种方法。BOOLEAN是一个TLA+内建，它等于集合{TRUE, FALSE}。如你所见，每一步都选择一个标志，并将其设置为true或false。如果觉得麻烦，我们可以这样写:

---- MODULE flags ----
EXTENDS TLC, Integers
(* --algorithm flags
variables flags \in [1..3 -> BOOLEAN], next = TRUE;
begin
  while next do
    with f \in DOMAIN flags, n \in BOOLEAN do
      flags[f] := ~flags[f];
      next := n;
    end with;
  end while;
end algorithm; *)

====

The flags \in [1..3 -> BOOLEAN] 叫做一个函数式集合，后面的内容会涉及。