Infinite Traces and Fairness Constraints

Infinite Traces and Fairness Constraints

• A trace is a sequence of states.
• Infinite traces are useful for reasoning about eventualities and arbitration.

Examples:

• “If Have_Token then eventually No Req.”
  . . ., Have_Token, Have_Token, NoReq, NoReq, . . . 4. . ., Have_Token, Have_Token, Have_Token, . . . 8
  • An environment model that randomly generates input patterns A, B, and C.“It is always the case that sometime in the future an A is generated. ” Similarly for B and C.
    A, B, C, A, B, C, A, B, C, ...A, B, C, B, A, B, C, B, A, ... both satisfy constraints.A, B, C, A, B, A, B, A, B, ... does not.

    Previous slide

    Next slide

    Back to the first slide

    View Graphic Version