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.


Last updated on 2009/01/30 14h:53