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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Wed, 6 Feb 2019 18:06:41 -0800 (PST)*References*: <7530440e-0b79-45ee-af76-8a0537a1fd30@googlegroups.com>

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.

It is pointless to ask what corresponds to someone's intuition of what

fairness means. We are concerned with specifying systems, not reading

people's minds. The concept of fairness in this context has been

discussed since the 70s. In 1986 Nissim Francez published a book

titled "Fairness". One of the strengths of TLA is that it is the only

formalism I know of capable of simply and elegantly expressing what

computer scientists have meant by fairness.

So how can I explain intuitively where their intuitions have led them

astray or at least are different to the notion of fairness embedded in

PlusCal / TLA+?

People have difficulty understanding fairness and, more generally,

liveness. I suspect that this stems from not having a good

understanding of quantification, so they can't immediately "feel in

their gut" the difference between \A x : \E y and \E y : \A x. But

for whatever reason, you should expect that you and your students will

have difficulty with fairness. The only thing to do is to patiently

explain the WF and SF operators to your students in terms of

assertions about behaviors. Since teaching something is a great way

to learn it, at least you'll come to understand it fairly quickly.

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.

Your students shouldn't be surprised that there are things they can

express in PlusCal that they can't express in C++. It won't surprise

them to learn that there are things they can express in TLA+ that

aren't easily expressed in PlusCal. The farther away you get from

the math that describes what's really going on, the less expressive

the language is. PlusCal looks more familiar to your students

than TLA+, and can be more convenient to use for some things--mainly

for multithreaded algorithms because it handles the pc variable for

you. But that comes at a cost. It's always possible to modify

the fairness property produced by the PlusCal translator. Remember

that if the PlusCal code is

A : either x' = x+1 or y' = y+1 ;

you can express fairness of an A action that increments x by writing

WF_vars(A /\ x'#x).

Leslie

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.

It is pointless to ask what corresponds to someone's intuition of what

fairness means. We are concerned with specifying systems, not reading

people's minds. The concept of fairness in this context has been

discussed since the 70s. In 1986 Nissim Francez published a book

titled "Fairness". One of the strengths of TLA is that it is the only

formalism I know of capable of simply and elegantly expressing what

computer scientists have meant by fairness.

So how can I explain intuitively where their intuitions have led them

astray or at least are different to the notion of fairness embedded in

PlusCal / TLA+?

People have difficulty understanding fairness and, more generally,

liveness. I suspect that this stems from not having a good

understanding of quantification, so they can't immediately "feel in

their gut" the difference between \A x : \E y and \E y : \A x. But

for whatever reason, you should expect that you and your students will

have difficulty with fairness. The only thing to do is to patiently

explain the WF and SF operators to your students in terms of

assertions about behaviors. Since teaching something is a great way

to learn it, at least you'll come to understand it fairly quickly.

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.

Your students shouldn't be surprised that there are things they can

express in PlusCal that they can't express in C++. It won't surprise

them to learn that there are things they can express in TLA+ that

aren't easily expressed in PlusCal. The farther away you get from

the math that describes what's really going on, the less expressive

the language is. PlusCal looks more familiar to your students

than TLA+, and can be more convenient to use for some things--mainly

for multithreaded algorithms because it handles the pc variable for

you. But that comes at a cost. It's always possible to modify

the fairness property produced by the PlusCal translator. Remember

that if the PlusCal code is

A : either x' = x+1 or y' = y+1 ;

you can express fairness of an A action that increments x by writing

WF_vars(A /\ x'#x).

Leslie

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

- Prev by Date:
**Re: How does Fairness relate to the State Graph** - Next by Date:
**Re: Practical TLA+ now out** - Previous by thread:
**Re: [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):