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

Re: Fairness for interruptable process

A is always enabled regardless of D. It is 3b that I need. 

I am in the process of learning TLA+ and I am finding getting fairness right a little bit tricky so many thanks for the help.


On Friday, January 18, 2019 at 7:52:43 PM UTC+1, Leslie Lamport wrote:
You seem to have stated the following conditions:

 1a. A is always enabled.

  b. B is enabled only after an A step.
  c. C is enabled only after a B step.
  d. D is enabled only after a C step.

 2. A D step eventually occurs after every A step.

What you don't make clear is whether 

 3a. Only a finite number of A,B,C, and D steps may occur.

  b. A finite or infinite number of those steps may occur.
  c. An infinite number of those steps must occur.

Conditions 1a-d are safety conditions and should be a consequence

of the definition of the next-state action.

Conditions 1a-d imply that Condition 2 is equivalent to strong

fairness of the B, C, and D actions.

That's all you need for 3b.  For 3c, you just need to add weak

fairness of A. For 3a, you need to modify 1a to allow D to disable A,
and have strong fairness on such a D action that does disable A.

All of this assumes that in 3, zero is a finite number.  You'll have

to modify the solutions for 3a and 3b  if you want to ensure that at 
least one A step occurs.