# [tlaplus] Re: Understanding relation between pluscal and tla

• Date: Tue, 26 Mar 2019 19:00:49 -0700 (PDT)

Q1. not sure what you mean as the State Graph (Q2) shows the states in all the detail I can think of.
Q2. the Next loops are caused by the  TLA+  (pc = "Done" /\ UNCHANGED vars) clause as can be seen by commenting them out. Not sure though what you have to do the PlusCal to prevent  this clause being formed.
Q3. the clause /\ \E f \in Flags: flags' = [flags EXCEPT ![f] = TRUE] is satisfied both when f = "f1" and when f = "f2" hence the step generates the two transitions of the State Graph.

regards david

On Thursday, 21 March 2019 21:58:01 UTC+13, Shiyao MA wrote:
Hi.  This post contains three *correlated* questions from the same code snippet attached below.

Q1. Model checking the program gives 5 states and 3 distinct ones. What are the exact states?

Q2. The checker's state graph output is here: https://imgur.com/a/p81e77M           .  Why is there a loop (the green arrow)?

Q3. The tla translated code for the with statement is:

with f \in Flags do
flags
[f] := TRUE;

end with;

Lbl_1 == /\ pc = "Lbl_1"
/
\ \E f \in Flags:
flags
' = [flags EXCEPT ![f] = TRUE]
/\ pc'
= "Done"

The pcal with clause branches each possible Flags value. But the tla one, which seems to me, only works on one possible new state because of the \E (as long as there exists one) logical operator.

I must be understanding something wrong about the \E here.

Thanks.

`---- MODULE simple ----EXTENDS Integers, TLC, Sequences, FiniteSetsFlags == {"f1", "f2"}(* --algorithm simplevariables    flags = [f \in Flags |-> FALSE];begin    with f \in Flags do         flags[f] := TRUE;    end with;end algorithm; *)\* BEGIN TRANSLATIONVARIABLES flags, pcvars == << flags, pc >>Init == (* Global variables *)        /\ flags = [f \in Flags |-> FALSE]        /\ pc = "Lbl_1"Lbl_1 == /\ pc = "Lbl_1"         /\ \E f \in Flags:              flags' = [flags EXCEPT ![f] = TRUE]         /\ pc' = "Done"Next == Lbl_1           \/ (* Disjunct to prevent deadlock on termination *)              (pc = "Done" /\ UNCHANGED vars)Spec == Init /\ [][Next]_varsTermination == <>(pc = "Done")\* END TRANSLATION====`

--
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 post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.