tla+pluscal

process local invariant in PlusCal

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

I want to have an invariant of x > 0 for all processes. Is there any way other than making x global?

I tried

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

But in translated TLA+ code, Inv is defined before variable x

Solution

  • Place the invariant after the \* END TRANSLATION line and it won't get clobbered by the PlusCal translator.