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

*From*: david streader <davidistreader@xxxxxxxxx>*Date*: Tue, 26 Mar 2019 19:00:49 -0700 (PDT)*References*: <7e9a7d4b-e2fc-4fe4-b7cb-9778d5b02c2b@googlegroups.com>

Hi A partial answer only.

On Thursday, 21 March 2019 21:58:01 UTC+13, Shiyao MA wrote:

-- 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, FiniteSets

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

(* --algorithm simple

variables

flags = [f \in Flags |-> FALSE];

begin

with f \in Flags do

flags[f] := TRUE;

end with;

end algorithm; *)

\* BEGIN TRANSLATION

VARIABLES flags, pc

vars == << 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]_vars

Termination == <>(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.

Visit this group at https://groups.google.com/group/tlaplus.

For more options, visit https://groups.google.com/d/optout.

**Follow-Ups**:**[tlaplus] Re: Understanding relation between pluscal and tla***From:*Shiyao MA

- Prev by Date:
**[tlaplus] Re: Proving false with fairness** - Next by Date:
**Re: [tlaplus] Re: Why is this temporal property violated?** - Previous by thread:
**[tlaplus] Re: Proving false with fairness** - Next by thread:
**[tlaplus] Re: Understanding relation between pluscal and tla** - Index(es):