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_CheckInvarSilently(
Prop_ptr prop,
Trace_ptr* trace
)
- Verifies that M,s0 |= AG alpha, with alpha propositional.
Uses strategy read from the option variable.
If opt_counter_examples is setted and trace is not null, then a
trace is stored (and must be released by caller) in trace
parameter location.
The result of model checking is stored in the given property.
- See Also
check_spec
check_ltlspec
Mc_CheckInvar_With_Strategy
void
Mc_CheckInvar_With_Strategy(
Prop_ptr prop,
Check_Strategy strategy,
Trace_ptr* output_trace,
boolean silent
)
- Verifies that M,s0 |= AG alpha, with alpha propositional.
Uses strategy given in input
If opt_counter_examples is setted and trace is not null, then a
trace is stored (and must be released by caller) in trace
parameter location.
The result of model checking is stored in the given property.
- See Also
check_spec
check_ltlspec
Mc_CheckInvar
void
Mc_CheckInvar(
Prop_ptr prop
)
- Verifies that M,s0 |= AG alpha, with alpha propositional.
Uses strategy read from the option variable.
- See Also
check_spec
check_ltlspec
Mc_CheckInvar_With_Strategy
void
Mc_CheckLanguageEmptiness(
const BddFsm_ptr fsm,
boolean allinit,
boolean verbose
)
- Checks whether the language is empty. Basically just a
wrapper function that calls the language emptiness algorithm given
by the value of the oreg_justice_emptiness_bdd_algorithm option.
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. allinit is
not supported for forward Emerson-Lei.
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. Forward Emerson-Lei
requires forward_search and use_reachable_states to be enabled.
If verbose is true, then some information on the set of
initial states is printed out too. verbose is ignored for
forward Emerson-Lei.
- Side Effects None
- See Also
mc_check_language_emptiness_el_bwd
mc_check_language_emptiness_el_fwd
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
Trace_ptr
Mc_create_trace_from_bdd_state_input_list(
const BddEnc_ptr bdd_enc,
const NodeList_ptr symbols,
const char* desc,
const TraceType type,
node_ptr path
)
- Creates a trace out of a < S (i, S)* > bdd list
- Side Effects none
- See Also
Trace_create
Bmc_create_trace_from_cnf_model
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.
SexpFsm_ptr
Mc_rewrite_invar_get_sexp_fsm(
const Prop_ptr prop,
SymbLayer_ptr layer,
node_ptr* created_var
)
- Returns the scalar fsm and the third argument will
be filled with the name of the monitor variable
void
Mc_trace_step_put_input_from_bdd(
Trace_ptr trace,
TraceIter step,
BddEnc_ptr bdd_enc,
bdd_ptr bdd
)
- Populates a trace step with input assignments
- Side Effects none
void
Mc_trace_step_put_state_from_bdd(
Trace_ptr trace,
TraceIter step,
BddEnc_ptr bdd_enc,
bdd_ptr bdd
)
- Populates a trace step with state assignments
- Side Effects none
void
mc_check_language_emptiness_el_bwd(
const BddFsm_ptr fsm,
boolean allinit,
boolean verbose
)
- See Mc_CheckLanguageEmptiness.
- See Also
BddFsm_get_fair_states
void
mc_check_language_emptiness_el_fwd(
const BddFsm_ptr fsm,
boolean allinit,
boolean verbose
)
- See Mc_CheckLanguageEmptiness.
- See Also
BddFsm_get_revfair_states
void
mc_rewrite_cleanup(
Prop_ptr rewritten_prop,
SymbLayer_ptr layer
)
- Crean up the memory after the rewritten property check
Prop_ptr
mc_rewrite_invar(
const Prop_ptr prop,
SymbLayer_ptr layer
)
- Returns a rewrited property