-
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 2011/04/06 21h:13