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_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.