Mc_CheckAGOnlySpec()
This function checks for SPEC of the form AG alpha in "context".
Mc_CheckCTLSpec()
Verifies that M,s0 |= alpha
Mc_CheckCompute()
Compute quantitative characteristics on the model.
Mc_CheckInvarSilently()
Verifies that M,s0 |= AG alpha WITHOUT print results or counterexamples
Mc_CheckInvar_With_Strategy()
Verifies that M,s0 |= AG alpha with the specified strategy
Mc_CheckInvar()
Verifies that M,s0 |= AG alpha
Mc_CheckLanguageEmptiness()
Checks whether the language is empty
Mc_End()
Quit the mc package
Mc_Init()
Initializes the mc package.
Mc_check_psl_property()
Top-level function for mc of PSL properties
Mc_create_trace_from_bdd_state_input_list()
Creates a trace out of a < S (i, S)* > bdd list
Mc_fair_si_iteration()
Mc_get_fair_si_subset()
Mc_rewrite_invar_get_sexp_fsm()
Prepares the rewriting generating a new sexp fsm containing the needed observer variable and its transition relation as well as its initial state.
Mc_trace_step_put_input_from_bdd()
Populates a trace step with input assignments
Mc_trace_step_put_state_from_bdd()
Populates a trace step with state assignments
mc_check_language_emptiness_el_bwd()
Checks whether the language is empty using the backward Emerson-Lei algorithm
mc_check_language_emptiness_el_fwd()
Checks whether the language is empty using the forward Emerson-Lei algorithm
mc_rewrite_cleanup()
Crean up the memory after the rewritten property check
mc_rewrite_invar()
Rewrites an invariant specification containing input variables or next with an observer state variable

Last updated on 2010/05/19 22h:26