# [tlaplus] Re: Approaching repeated assignment in PlusCal

• From: Srikumar Subramanian <srikumar.subramanian@xxxxxxxxxxxx>
• Date: Wed, 9 Dec 2020 19:43:13 -0800 (PST)
• References: <CAJs285kRCQAH6JRsNGk5=tSOd==hcxqWELz1czii66CNgYPNZQ@mail.gmail.com>

(Newbie here so I may be wrong)

To me,, the following looks like a specification error -
section1:
x := x + 1;
x := x + 1;

This is (I think) when the mental model of "assignment"" for "state update" gets shaky. "x := x + 1" is really saying "x' = x + 1" in TLA+. So Saying it twice, would be redundant if you want to treat them as being made atomically. So you're really saying "x1' = x + 1 /\ x' = x1' + 1" in TLA+ notation. I suppose then you want to change the mental model in your PlusCal generator ...which I'm not sure is a good idea as it moves away from thinking about it as "specification" versus "program". (I guess more experienced folks ought to comment on that)

However, if you do want to do that atomically, I don't see a way out of introducing more temporary state variables to handle this. You will have to pretty much treat every "assignment" as introducing a new variable, generate update expressions for each of them and finally update the original state. Meaning you need to treat "x := x + 1; x := x + 1; .. <n times>"  as " x1' = x + 1 /\ x2' = x1' + 1 /\ ... <n times> /\ x' = xn' ".

-Srikumar

On Thursday, December 10, 2020 at 5:43:11 AM UTC+5:30 fhack...@xxxxxxxxx wrote:

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

This mail contains confidential information intended only for the individual(s) named. If you’re not the named addressee, don’t disseminate, distribute or copy this e-mail. Please notify the sender immediately and delete it from your system.If you wish not to receive such e-mails you may reply with text “Unsubscribe”.

--
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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.