Re: [tlaplus] PlusCal issue

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

Stephan

On Mar 10, 2024, at 14:54, Andrew Samokish <asam.mail@xxxxxxxxx> wrote:

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.