[tlaplus] PlusCal issue

[Andrew Samokish <asam.mail@xxxxxxxxx>]

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

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