Re: [tlaplus] Re: How does Fairness relate to the State Graph

Hi David,

It appears that either... or... is inherently unfair

exactly: either ... or ... is just non-deterministic choice, without any fairness condition attached. You can see this effect when you uncomment the labels upx and upy in your original algorithm and inspect the TLA+ specification that is generated by the PlusCal translator: the Count action includes a non-deterministic choice between moving to either of these labels whereas the actions upx and upy simply increment the variables x or y respectively. The fairness annotations do not correspond to what you have in mind. It might be tempting to add a construct "either+" to PlusCal that models nondeterministic choice while ensuring fairness between the different branches, but the interaction with the rules for placing labels – in order to ensure branching is visible – are going to be intricate, and PlusCal aims at being simple. A similar "with+" construct that nondeterministically but fairly chooses between the elements of a set would be even more intricate, unless the set is a constant.

As Leslie and Ron say, it is easy to express the desired effect in TLA+, and you can just add a fairness condition to that effect to the TLA+ spec that the PlusCal translator generates. See the module below. TLC will now confirm termination (remember to change "Spec" to "FairSpec" in "What is the behavior spec"). In fact, just adding WF_x(counter) to the default fairness condition is enough for this to hold.

Regards,

Stephan

------------------------------ MODULE Counter ------------------------------

EXTENDS TLC, Integers

CONSTANT Size

(* --algorithm counter

variable x = 0, y = 0;

fair process counter = "counter"

begin Count:

  while (x<Size) do

  either 

  await (x<Size);

\*   upx:+

    x := x + 1;

or

\*   upy:+

    y := (y + 1)%Size;

  end either;    

 end while;

end process;

end algorithm; *)

\* BEGIN TRANSLATION

VARIABLES x, y, pc

vars == << x, y, pc >>

ProcSet == {"counter"}

Init == (* Global variables *)

        /\ x = 0

        /\ y = 0

        /\ pc = [self \in ProcSet |-> "Count"]

Count == /\ pc["counter"] = "Count"

         /\ IF (x<Size)

               THEN /\ \/ /\ (x<Size)

                          /\ x' = x + 1

                          /\ y' = y

                       \/ /\ y' = (y + 1)%Size

                          /\ x' = x

                    /\ pc' = [pc EXCEPT !["counter"] = "Count"]

               ELSE /\ pc' = [pc EXCEPT !["counter"] = "Done"]

                    /\ UNCHANGED << x, y >>

counter == Count

Next == counter

           \/ (* Disjunct to prevent deadlock on termination *)

              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

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

        /\ WF_vars(counter)

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

(***************************************************************************)

(* The following condition states that control should not remain at label  *)

(* "Count" while leaving either x or y unchanged forever.                  *)

(***************************************************************************) 

XYFair == WF_x(counter) /\ WF_y(counter)

FairSpec == Spec /\ XYFair

=============================================================================

On 7 Feb 2019, at 01:47, david streader <davidistreader@xxxxxxxxx> wrote:

Hi Ron
Unfortunately I do not understand TLA+ as well as I understand operational semantics. My problem is trying to understand the relation between PlusCal and the State Graphs. You may well be correct that there is no easy way to use Temporal Logic to define fairness the way I think is natural from the perspective of the operational semantics. When using TLC to model check the finite state approximations of the potentially infinite state State Machines it would seem helpful to provide fairness analysis on these approximations and it is easy enough to check such fairness on the State Graph even if it is hard to formulate in temporal logic.

One question remains would it be reasonable for an engineer (say one of my students) to expect my simple algorithm to terminate given fair behavior. If so that would mean the technical definition of fairness in TLA+ is at odds with this engineer's intuitions. So how can I explain intuitively where their intuitions have lead them astray or at least are different to the notion of fairness embedded in PlusCal / TLA+? I could say fairness is only understandable at the TLA+ code level and not at the PlusCal level but this would not be very helpful to the student.

As it stands, and with the limit of my understanding, It appears that either... or... is inherently unfair (because of the way steps are built by the translation) but this is a little unfortunate and before I tell my students this I would like to know if I have made some mistake.

p.s. many thanks for the help with this.

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

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