|
Fairness Constraints in VIS
Fairness Constraints in VIS
- VIS allows fairness constraints of the form
Finf S1 & Finf S2 & ... & Finf Sn
- Si: A set of states represented by a CTL formula.
- The fairness constraint is satisfied if some state in each Si is visited infinitely often.
- Example: Let S1 be given by !(client_state = Have_Token)
S1 = {NoReq, Req}
- Finf S1 means {NoReq, Req} is visited infinitely often, i.e., Have_Token does not remain asserted forever.
- Usage: vis> read_fairness file.fair
- Restricts attention to traces that satisfy the fairness constraints.
- Like listing a set of false paths.
|
