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

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

Realized over night, if my understanding of what has been said is correct then: In order for the small program to be terminating, when restricting to fair behaviors, you would not need to change how temporal logic was calculated only how either... or ....  was translated.  
       With the extra label "oneMore" the state graph (attached)  always branches with two arrows in the same step 
                                         s--oneMore-->h--upx-->n and s--oneMore-->g--upy-->m 
but if the translation made the branch occur between different steps 
                                             s--upx-->h  and s--upy-->m  
then I think the tool would give the desired result. How easy it would be to change the translation I do not know.

But all of this is only relevant if other peoples  intuition is that a fair execution of the small program would indeed terminate.

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.

Attachment: Fair5.tla
Description: Binary data

Attachment: lastGasp.pdf
Description: Adobe PDF document