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

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

Hi Leslie
       Many people are well aware of what fairness means. Unfortunately they how they interpret the details of this depends upon their formal background.  Personally I have more of a background in operational semantics than in temporal logic. Although TLA+  rests on Classical and Temporal Logic there is a State Graph that I had been applying by operational semantics understanding to.  
    Let us take fairness to mean "if an event is offered infinitely often then it must be taken in a finite number of steps".  On the State Graph what is fair behavior depends upon how you interpret "an event is offered"  this, in operational semantic, is often thought to mean that the loops in the operational semantics  that can be exited will eventually be exited.  
    Clearly this is not the interpretation in the PlusCal TLA+ translation where  it is not the individual transitions of the State Graph that are offered but the labeled steps.

 Certainly I had not picked up on the inherent non determinism of either.. or..  and  my intention was to build an algorithm that any fair behavior of would terminate.
I am not trying to say there is anything wrong with the interpretation "an event is offered"  as being a labeled step it simply was not my original understanding.  Given that this is how TLA+ works you can say I was trying to encode an PlusCal algorithm that performed either of two steps that had different labels. I am still not sure if this is possible in plusCal. 

I agree completely with Leslie
     "The translation doesn't make anything happen. "
and had certainly not meant to give the translation with any agency. All that I intended was that : the State Graph is a formal representation of the State Machine that  gives  meaning to the PlusCal/TLA+ syntax. As, I assume, TLA+ is rich enough to define either any State Machine, or at least the state machines we are considering, then the State Graph that I outlined could be defined  as a TLA+ translation of either.. or... (or some new command  either+ .. or ..) 

This would allow exactly the same definition  and implementation of fairness but  to give an alternative result by virtue of the state graph branching with different named steps.

kind regards david

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.