|
Why fairness constraints?
Why fairness constraints?
- Non-determinism is used to hide irrelevant detail.
- May introduce behavior that is not part of actual system. Example: Client module
- Non-det. model allows No Req, Req, Req, Have_Token, Have_Token ... but actual client eventually gives up token.
- Want to refine the non-det. description to model the client more closely.
- Must remove traces that stay in Have_Token forever.
|
