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

[tlaplus] Re: Understanding relation between pluscal and tla

Hi A partial answer only.
  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
[f] := TRUE;
end with;

Lbl_1 == /\ pc = "Lbl_1"
\ \E f \in 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.


---- MODULE simple ----
Integers, TLC, Sequences, FiniteSets

Flags == {"f1", "f2"}

(* --algorithm simple
= [f \in Flags |-> FALSE];
with f \in Flags do
[f] := TRUE;
end with;
end algorithm; *)

, pc

== << flags, pc >>

Init == (* Global variables *)
/\ flags = [f \in Flags |-> FALSE]
/\ pc = "Lbl_1"

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

Next == Lbl_1
\/ (* Disjunct to prevent deadlock on termination *)
(pc = "Done" /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(pc = "Done")



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.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.