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

*From*: Leslie Lamport <tlaplus.ll@xxxxxxxxx>*Date*: Thu, 7 Feb 2019 15:15:28 -0800 (PST)*References*: <7530440e-0b79-45ee-af76-8a0537a1fd30@googlegroups.com>

A more straightforward translation might be:

...

b == \* /\ pc = "b" The definitions of b_BRANCH* make this conjunct redundant.

/\ \/ b__BRANCH1

\/ b__BRANCH2

...

b == \* /\ pc = "b" The definitions of b_BRANCH* make this conjunct redundant.

/\ \/ b__BRANCH1

\/ b__BRANCH2

But this doesn't solve the problem. The desired fairness condition is

fairness of both b_BRANCH1 and b_BRANCH2, and how is that supposed to

be indicated in the PlusCal code?

Before we waste any more time discussing this, everyone should realize

that it is just one of many kinds of fairness conditions one might

want that aren't expressible in PlusCal. For example in

that it is just one of many kinds of fairness conditions one might

want that aren't expressible in PlusCal. For example in

w : with (n \in 1..42) { x := n }

one might want the fairness condition

\A n \in 1..42 : SF_...(pc = "w" /\ x' = n)

Other specification methods that have been proposed write a spec with

a next-state relation as the disjunction of a particular set of

(named) actions. Some of them can specify liveness with fairness

conditions on those particular actions. But TLA+ is more expressive

than any other formalism I know of because it isn't limited to

fairness of those particular named actions. I know no way to get that

expressiveness when using PlusCal other than by defining a spec that

is the conjunction of the formula Spec generated by the PlusCal

translation with additional fairness formulas.

a next-state relation as the disjunction of a particular set of

(named) actions. Some of them can specify liveness with fairness

conditions on those particular actions. But TLA+ is more expressive

than any other formalism I know of because it isn't limited to

fairness of those particular named actions. I know no way to get that

expressiveness when using PlusCal other than by defining a spec that

is the conjunction of the formula Spec generated by the PlusCal

translation with additional fairness formulas.

Perhaps someone else can find a way to do this that I haven't been

able to think of in the last 14 years. But please realize the scope

and difficulty of the problem and let's not clutter the group with ad

hoc proposals that may or may not work in one particular example.

able to think of in the last 14 years. But please realize the scope

and difficulty of the problem and let's not clutter the group with ad

hoc proposals that may or may not work in one particular example.

Leslie

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.

**References**:**How does Fairness relate to the State Graph***From:*david streader

- Prev by Date:
**[tlaplus] Re: How does Fairness relate to the State Graph** - Next by Date:
**[tlaplus] Re: How does Fairness relate to the State Graph** - Previous by thread:
**[tlaplus] Re: How does Fairness relate to the State Graph** - Next by thread:
**[tlaplus] Re: How does Fairness relate to the State Graph** - Index(es):