A fairness constraint "a=1" instructs the model checker to disregard
computations (paths) along which "a=1" does not happen infinitely
often. It is not necessary for "a=1" to always hold along the path
for it to be fair.
Hence, it is quite possible for a counterexample to contain states
with "a=0" even if the fairness constraint "a=1" is in effect.
>From a practical standpoint, it's worth noting that in Vis, fairness
constraints are honored by "model_check," and ignored by
"check_invariant."
It is unusual to check invariants under fairness constraints, which
are most often specified for liveness properties. However, should one
want to check whether an invariant holds in all states reachable along
a fair path (as opposed to the states reachable via any path), the
invariant should be written as an AG property, and checked with "mc."
>>>>> "vg" == vanessa goyal <vanessa_goyal@rediffmail.com> writes:
vg> sir
vg> If a=1(one of the input to FSM) is fairness constraint,then
vg> reachability analysis will get restricted to paths for which a=1.
vg> So,i expect, on failure of any property,counter example generated
vg> should contain only those states for which a=1,but its showing
vg> states having a=0 also.
vg> Is it my misconception.
vg> thanking you
vg> vanessa
Fabio
This archive was generated by hypermail 2b30 : Thu May 24 2001 - 13:14:23 MDT