PlusCal中的过程局部不变

Question

process(Server \in Servers)
variable x;
{
    ...
}

对于所有的过程，我想要一个x>0的不变量。除了使x成为全球之外，还有其他的方法吗？

我试过了

define {
  Inv == \A s \in Servers: x[s] > 0
}

但是在翻译的TLA+代码中，Inv是在变量x之前定义的。

Answer 1

将不变量放在\* END TRANSLATION行之后，它不会被PlusCal翻译器破坏。