PlusCal issue

[Andrew Samokish]

Hello, 

Can you please clarify this issue for me?

i have a small test code:

(*--algorithm test
variables   x = FALSE,  i1 = 0, i2 = 0;
           
process clock = "clock"
begin
    ActionClock:
        i1 := i1+1;
        x:= ~x;
    goto ActionClock;    
end process; 

...

Basically, it is alternating variable x and counts iterations.

I have a similar process for i2.

That is, what I have as a translation to TLA:

ActionClock == /\ pc["clock"] = "ActionClock"
               /\ i1' = i1+1
               /\ x' = ~x
               /\ pc' = [pc EXCEPT !["clock"] = "ActionClock"]
               /\ i2' = i2

why i2 is not listed as UNCHANGED << x, i2 >> ?

if I would remove x:= ~x;  from pluscal code - i2 appears in 'unchanged' section.

Does it somehow impact other code able to perform in parallel and impact i2?

thank you very much in advance

Sincerely yours, Andrew

[Stephan Merz]

A basic tenet of PlusCal is to consider all statements that appear between two consecutive labels as happening atomically. In your example, both assignments to i1 and to x, as well as the `goto’ happen in a single step. And since x is being assigned to in the step, it is not listed as `UNCHANGED’.

Also, parallelism is represented as interleaving between actions. In your example, you’ll have arbitrary interleaving between steps of the two processes.

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5992abf5-56dd-452a-8175-8bdaa66f48e8n%40googlegroups.com.

[Andrew Samokish]

Stephan, thank you very much for the answer,  the behavior about 'x' variable is clear to me 

but I would precise my question:

for me, the i2 variable is supposed to be listed in the 'UNCHANGED' block, but instead, it is described as "/\ i2' = i2'".

i2 appears in UNCHANGED, if "x:= ~x;" is removed from the text

lets compare those two examples:

1. 

process clock = "clock"
begin
    ActionClock:
        i1 := i1+1;
        x:= ~x;
    goto ActionClock;

end process;

>>

ActionClock == /\ pc["clock"] = "ActionClock"
               /\ i1' = i1+1
               /\ x' = ~x
               /\ pc' = [pc EXCEPT !["clock"] = "ActionClock"]

               /\ i2' = i2

2. 

process clock = "clock"
begin
    ActionClock:
        i1 := i1+1;

    goto ActionClock;
end process;

>>

ActionClock == /\ pc["clock"] = "ActionClock"
               /\ i1' = i1+1

               /\ pc' = [pc EXCEPT !["clock"] = "ActionClock"]

               /\ UNCHANGED << x, i2 >> 

it happens, when I do use 'translate pluscal algorithm' in TLA+ toolbox, v 1.7.1

Practically, both examples are equivalent about i2 variable behavior,

Just the translator don`t want to define 'UNCHANGED' block for the single variable

воскресенье, 10 марта 2024 г. в 16:01:00 UTC+1, Stephan Merz:

[Stephan Merz]

Oh, I see. The two are equivalent since UNCHANGED e is just different syntax for e’ = e. For a single variable, the PlusCal translator prefers the latter over the former and does not produce an UNCHANGED block.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4d3b9da5-b4b2-4979-88b0-b0842aa44e3en%40googlegroups.com.

[Andrew Samokish]

yes, thank you. just was surprised a little bit by the PlusCal translator

Andrew

понедельник, 11 марта 2024 г. в 08:40:26 UTC+1, Stephan Merz: