[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] PlusCal issue

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"
        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.