在PlusCal中处理进程局部不变量：非全局化实现x>0的方法问询

你不需要将x改为全局变量，有两种可靠的方法实现所有进程局部x > 0的不变量验证：

方法1：在PlusCal转换后的TLA+代码区域后定义不变量 #

PlusCal转换为TLA+时，进程的局部变量会被自动转换为以进程ID为索引的函数（比如x[s]对应Server为s的进程的局部变量）。你之前的方法失效，是因为define块在转换时会被置于所有变量声明之前，导致引用未定义的x。

解决步骤：

1. 保留原PlusCal进程的局部变量定义：

---- MODULE ServerModule ----
EXTENDS TLC, Integers

Servers == {"s1", "s2", "s3"}

(*--algorithm ServerLogic
process(Server \in Servers)
variable x;
{
    \* 你的进程逻辑，比如初始化x为正整数
    x := 2;
    ...
}
end algorithm; *)

2. 在PlusCal注释块之后添加不变量定义（转换后的TLA+变量声明会自动生成在注释块内部展开的位置，后续定义可以合法引用x）：

\* 不变量定义，此时x已被转换为进程索引的函数
Inv == \A s \in Servers: x[s] > 0

\* 可选：用TLA+定理声明不变量，让TLC验证
THEOREM Spec => []Inv

之后运行TLC时，将Inv加入不变量检查列表即可。

方法2：进程内添加断言（运行时检查） #

如果需要在算法执行的每一步确保x > 0，可以在进程逻辑中每次修改x后添加assert语句：

process(Server \in Servers)
variable x;
{
    x := 1;
    assert x > 0; \* 初始化后检查
    ...
    x := x + 5;
    assert x > 0; \* 修改后检查
    ...
}

注意：这种方法仅检查实际执行路径中的状态，无法像全局不变量那样遍历所有可能状态，适合补充验证而非替代全局不变量。

内容的提问来源于stack exchange，提问作者Tauta