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

Re: Fairness for interruptable process



I would specify this by adding an id parameter to my actions, and maintain history of execution as a (ghost) variable

A1, B1, C1, D1, A2, B2, C2, D2
A1, B1, A2, B2, C2, D2
A1, B1, A2, B2, A3, B3, A4, B4, C4, D4
A1, A2, B2, A3, A4, A5
A1, A2, A3, A4, A5, A6

And now, since I'm maintaining history, I can specify something like:
    \A i \in Nat: Di \in History => Ai \in History

Now your History is a (monotonic) set and you can choose to implement Di, Ai, etc in whatever manner you like - string, record, etc.

Thanks,
Saksham

On Friday, January 18, 2019 at 12:55:35 PM UTC-5, Jack Vanlightly wrote:
Hi,

I have a series of actions A, B, C and D which fire sequentially, each in a different step. As long as A doesn't fire again before D, then every firing of action A must always lead to D. However, it is possible A will fire again before D, starting the series of actions again.

So for example, all of the below sequences of steps are valid:
A, B, C, D, A, B, C, D
A, B, A, B, C, D
A, B, A, B, A, B, A, B, C, D
A, A, B, A, A, A
A, A, A, A, A, A

So my question is: How can I state some fairness property that describes that A will eventually lead to D, but only if A doesn't fire again before D.

Many thanks
Jack