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
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 <email@example.com> writes:
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
This archive was generated by hypermail 2b30 : Thu May 24 2001 - 13:14:23 MDT