void
Mc_CheckAGOnlySpec(
Prop_ptr prop
)
- The implicit assumption is that "spec" must be an AG
formula (i.e. it must contain only conjunctions and AG's). No attempt
is done to normalize the formula (e.g. push negations). The AG mode
relies on the previous computation and storage of the reachable
state space (reachable_states_layers), they are used in
counterexample computation.
- See Also
check_spec
void
Mc_CheckCTLSpec(
Prop_ptr prop
)
- Verifies that M,s0 |= alpha using the fair CTL model checking.
void
Mc_CheckCompute(
Prop_ptr prop
)
- Compute the given quantitative characteristics on the model.
void
Mc_CheckInvar(
Prop_ptr prop
)
- Verifies that M,s0 |= AG alpha, with alpha propositional.
- See Also
check_spec
check_ltlspec
void
Mc_CheckLanguageEmptiness(
const BddFsm_ptr fsm,
boolean allinit,
boolean verbose
)
- Checks whether the language is empty. If
allinit is true the check is performed by
verifying whether all initial states are included in the set of fair
states. If it is the case from all initial states there exists a
fair path and thus the language is not empty. On the other hand, if
allinit is false, the check is performed by verifying
whether there exists at least one initial state that is also a fair
state. In this case there is an initial state from which it starts a
fair path and thus the lnaguage is not empty.
Depending on the global option use_reachable_states the set of fair
states computed can be restricted to reachable states only. In this
latter case the check can be further simplified.
if verbose is true, then some information on the set of
initial states is printed out too.
- Side Effects None
- See Also
BddFsm_get_fair_states
void
Mc_End(
)
- Quit the mc package
void
Mc_Init(
)
- Initializes the mc package.
int
Mc_check_psl_property(
Prop_ptr prop
)
- The parameters are:
- prop is the PSL property to be checked
- Side Effects None
bdd_ptr
Mc_fair_si_iteration(
BddFsm_ptr fsm,
BddStatesInputs states,
BddStatesInputs subspace
)
- Perform one iteration over the list of fairness
conditions (order is statically determined). Compute states that are
backward reachable from each of the fairness conditions.
MAP( ApplicableStatesInputs ) over Fairness constraints
(Q / ex_si ( Z / AND_i eu_si(Z, (Z/ StatesInputFC_i))))
BddStatesInputs
Mc_get_fair_si_subset(
BddFsm_ptr fsm,
BddStatesInputs si
)
- Returns the set of state-input pairs in si that are
fair, i.e. beginning of a fair path.