Hello,
I'm working on PGo (link: https://github.com/UBC-NSS/pgo), a tool that, among other things, does some macro-like expansion over PlusCal.
I'd like to discuss some tricky edge cases we're running into, namely: specifications which are written as-if multiple assignments happen to the same variable within the same action, in PlusCal. I am aware that PlusCal assignments correspond to TLA+ primed constraints, and therefore that under the PlusCal translation it really makes no sense to actually reassign the same variable in the same action, in any literal sense.
The trouble is that there are situations where code that has that kind of effect needs to be written, and it would be convenient if it could be generated in a way that works, like PlusCal itself, via macro expansion.
Consider some example critical sections, assuming a single-process specification, with a state variable x that is some integer.
section1:
x := x + 1;
x := x + 1;
Clearly, a human would just rewrite the body to say "x := x + 2" and be done.
Mechanically, this can also be handled by inserting a with:
section1:
with (x0 = x + 1) {
x := x0 + 1;
}
This works for many simpler cases, but becomes troublesome when certain types of control flow become involved:
section2:
if (x = 2) {
x := x + 1;
}
x := x + 1;
Here, we can't bind any x0 locally that "fixes" the situation, because there is no syntactically general way to bind something inside a branch that is also visible outside that branch. The best we can do syntactically is to perform a little inlining, duplicating any statements after the if:
section2:
if (x = 2) {
with (x0 = x + 1) {
x := x0 + 1;
}
} else {
x := x + 1;
}
If we want to avoid code duplication, the only other way we can think of is to add a dummy state variable, also called x0 (this is similar to what PGo currently generates):
section2:
if (x = 2) {
x0 := x + 1;
} else {
x0 := x;
}
x := x0 + 1;
This has a significant detrimental effect on state space in
practice, though, so it is not a very good approach.
My question, then: can anyone think of better (automatable) ways
to simulate multiple intra-action assignments to the same
variable? Would there be a TLC/toolbox feature that could help
with this kind of thing? For instance, in the dummy state variable version, it would make a big difference if we had
a way to selectively drop some state variable from the state
space, preventing space blow-up.
Any thoughts or comments are appreciated,
A. Finn Hackett