多进程

之前使用的例子都是单进程的，现在用多进程来描述多个逻辑同时发生，TLA+中的多进程可以理解为其他高级语言中的多线程。为了方便理解，使用Pluscal语言来描述，TLA+ Toolbox可以将pluscal语言转化为TLA+，基本格式如下：

---- MODULE module_name ----
\* TLA+ code

(* --algorithm algorithm_name   \* 固定格式，algorithm_name根据需要填写
variables global_variables      \* 全局变量，在process之外声明的都是全局变量

process p_name = foo             \* 使用process关键字定义一个进程
variables local_variables		 \* 局部变量
begin                            \* 当前进程的处理逻辑用begin和end process作为开始和结束标志。
  \* pluscal code 			     \* 主要的处理逻辑需要用label标识出来
end process

process p_group \in bar        \* 定义多个进程，进程的逻辑相同，其中bar是一个集合
variables local_variables        
begin
  \* pluscal code 
end process

end algorithm; *)
=================      

所有的进程都需要一个值，可以采用两种方式，一种是上述例子中的process p_name=foo,一种是上述例子中的process p_group \in bar，其中bar是集合。 进程名用来区分进程，因此进程名最好是同一类型，且赋予不同的值。

在进程之外声明的变量是全局变量，可以被多个进程共享使用。在进程内声明的变量是局部变量。

上述的例子可以看出，在pluscal中也可以使用 \in 这样的逻辑符号。TLC在多进程运行时，会选择可能的步骤运行，每个步骤对应于进程中一个label中的所有代码。TLC在选择的运行路径中如果任何一条破坏了不变量规则，就会正常终止，并在Error-trace中打印出错误路径。以下是一个多进程用例

variables x = 0;
process one = 1
begin
  A:
    x := x - 1;
  B:
    x := x * 3;
end process

process two = 2
begin
  C:
    x := x + 1;
  D:
    assert x /= 0;
end process

上述代码存在bug，因为当TLC选择C -> A -> B -> D的运行路径时，将会出现 0 + 1 -> 1 - 1 -> 0 * 3 -> 0 /= 0的情况。对于同一流程的多个进程，TLC的运行路径是类似的，例如

(* --algorithm foo
variables x = 0;
process cycle \in 1..3
begin
  A:
    x := x + 1;
  B:
    x := 0;
  C:
    assert x /= 2;
end process
end algorithm; *)

上述逻辑在运行路径A[1] -> B[1] -> A[2] -> A[3] -> C[1]上会失败。

await

可以使用await关键字来暂时阻止TLC的运行，await用来等待条件被满足后，才能继续执行。回到上述例子，添加await后，进程2在开始执行C时，会一直等待x<-1才会往下执行。初始状态x=0,进程1执行A后x=-1，进程1执行B后x=-3，因此TLC运行路径只能是A->B->C->D。

process one = 1
begin
  A:
    x := x - 1;
  B:
    x := x * 3;
end process

process two = 2
begin
  C:
    await x < -1;
    x := x + 1;
  D:
    assert x /= 0;
end process

但是很明显的问题，如果 x<-1不为真的情况，进程2会一直处于阻塞状态，成为死锁。TLC可以检测死锁，当检测死锁时，如果遇到死锁就会报错。当不检测死锁时，即使出现死锁也不会报错。所以，如果死锁不是系统中的错误，应该在TLC Model中禁用死锁检查。