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
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
.