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_And_Symbols(
  Prop_ptr  prop, 
  Check_Strategy  strategy, 
  Trace_ptr* output_trace, 
  boolean  silent, 
  NodeList_ptr  symbols 
)
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. A trace is created for variables and defines in 'symbols'. If trace is not required 'symbols' can be NULL. The result of model checking is stored in the given property.

See Also check_spec check_ltlspec Mc_CheckInvar

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. The built trace is non-volatile. For more control over the built trace, please see Mc_fill_trace_from_bdd_state_input_list

Side Effects none

See Also Trace_create Bmc_create_trace_from_cnf_model Mc_fill_trace_from_bdd_state_input_list

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))))


Trace_ptr 
Mc_fill_trace_from_bdd_state_input_list(
  const BddEnc_ptr  bdd_enc, 
  Trace_ptr  trace, 
  node_ptr  path 
)
Fills the given trace out of a < S (i, S)* > bdd list. The returned trace is the given one, filled with all steps. The given trace MUST be empty. Path must be non-Nil

Side Effects none

See Also Trace_create Bmc_fill_trace_from_cnf_model

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_eu_explain_restrict_state_input_to_minterms(
  BddFsm_ptr  fsm, 
  BddEnc_ptr  enc, 
  node_ptr  path, 
  node_ptr  initial_node 
)
'path' is a list of ((state, input)+, state). States and inputs are BDDs. The list has to be reversed i.e. state car(path) can be reached from state car(cdr(cdr(path))) through input car(cdr(path)). The first element of the path, i.e. car(path) has to be already minterm. The function restricts every state and input to single state/input, resp, i.e. to minterm. initial_node is the last state node of path to be restricted.


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


Last updated on 2012/11/18 14h:37