Check_TraceList_Sanity()
CommandCheckCompute()
Performs computation of quantitative characteristics
CommandCheckCtlSpec()
Performs fair CTL model checking.
CommandCheckInvar()
Performs model checking of invariants
CommandCheckPslSpec()
Performs fair PSL model checking.
CommandCheckSpec()
Deprecated version of CommandCheckCtlSpec
CommandLanguageEmptiness()
Checks for language emptiness.
Extend_trace_with_state_input_pair()
Extend_trace_with_states_inputs_pair()
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
abu()
Set of states satisfying A[f U^{inf..sup} g].
au()
Set of states satisfying A[f U g].
backward_heuristic()
Constant function to perform backward analysis
binary_bdd_op()
Applies binary operation.
binary_mod_bdd_op_ns()
Applies binary operation.
binary_mod_bdd_op()
Applies binary operation.
check_AG_only()
This function checks for SPEC of the form AG alpha in "context".
check_invariant_forward_backward_with_break()
Performs on the fly verification of the invariant during reachability analysis.
check_invariant()
Check the given invariant with the specified technology
complete_bmc_trace_with_bdd()
Completes a partial BMC tace in BDD-BMC analysis
compute_and_complete_path()
Generates a counterexample from a path forward and a path backward completing the two parts with the specified middle trace if needed
compute_path_fb()
Generates a counterexample from a path forward and a path backward
ebf()
Set of states satisfying EF^{inf..sup}(g).
ebg_explain()
This function finds a path of length (sup-inf) that is an example for EG(g)^{sup}_{inf}.
ebg()
Set of states satisfying EG^{inf..sup}(g).
ebu_explain()
This function finds a path that is a witness for E[f U g]^{sup}_{inf}.
ebu()
Set of states satisfying E[f U^{inf..sup} g].
ef()
Set of states satisfying EF(g).
eg_explain()
This function finds a path that is an example for EG(g).
eg_si()
Set of states-inputs satisfying EG(g).
eg()
Set of states satisfying EF(g).
eu_explain()
This function finds a path that is a witness for E[f U g]
eu_si_explain()
This function finds a path that is a witness for E[f U g] when g is a set of state-inputs
eu_si()
Computes the set of state-input pairs that satisfy E(f U g), with f and g sets of state-input pairs.
eu()
Set of states satisfying E[ f U g ].
eval_compute_recur()
Recursive step of eval_compute.
eval_compute()
Computes shortest and longest length of the path between two set of states.
eval_ctl_spec_recur()
Recursive step of eval_ctl_spec.
eval_ctl_spec()
Compile a CTL formula into BDD and performs Model Checking.
eval_formula_list()
This function takes a list of formulas, and returns the list of their BDDs.
ex_explain()
This function computes a path that is a witness for EX(f).
ex_si()
Set of states satisfying EG(g).
explain_and()
Generates a witness path for car(formula) AND cdr(formula)
explain_eval()
required
explain_recur()
Recursively traverse the formula CTL and rewrite it in order to use the base witnesses generator functions.
explain()
Counterexamples and witnesses generator.
ex()
Set of states satisfying EX(g).
fairness_explain()
Auxiliary function to the computation of a witness of the formula EG f.
forward_backward_heuristic()
Heuristic function used to decide the sept to perform in forward-backward analysis
forward_heuristic()
Constant function to perform forward analysis
free_formula_list()
Frees a list of BDD as generated by eval_formula_list
is_AG_only_formula_recur()
Recursive function that helps is_AG_only_formula.
is_AG_only_formula()
Checks if the formulas is of type AGOnly.
make_AG_counterexample()
This function constructs a counterexample starting from state target_state
maxu()
This function computes the maximum length of the shortest path from f to g.
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
minu()
Computes the minimum length of the shortest path from f to g.
never_stopping_heuristic()
Constant function to perform backward, forward and FB analysis
print_compute()
Prints out a COMPUTE specification
print_invar()
Print an invariant specification
print_result()
Prints the result of the check if the check was performed, does nothing otherwise
print_spec()
Prints out a CTL specification
quad_mod_bdd_op()
Applies quaternary operation.
stopping_heuristic()
Heuristic function used to decide whether to stop BDD analysis to pass to BMC.
ternary_mod_bdd_op()
Applies ternary operation.
unary_bdd_op()
Applies unary operation.
unary_mod_bdd_op()
Applies unary operation.

Last updated on 2011/04/06 21h:12