Go to the first, previous, next, last section, table of contents.
FAIRNESS declarationsA fairness constraint is a CTL formula which is assumed to be true infinitely often in all fair execution paths. When evaluating specifications, the model checker considers path quantifiers to apply only to fair paths. Fairness constraints are declared using the following syntax:
fairness_declaration :: "FAIRNESS" fair_expr
fair_expr :: ctl_expr
A path is considered fair if and only if all constraints declared in this manner are true infinitely often.