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_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_fair_si_iteration()
Mc_get_fair_si_subset()
abu()
Set of states satisfying A[f U^{inf..sup} g].
au()
Set of states satisfying A[f U g].
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()
Performs on the fly verification of the invariant during reachability analysis.
check_invariant_forward()
Performs on the fly verification of the invariant during reachability analysis.
compute_and_print_path_fb()
compute_and_print_path()
Extracts and prints a counterexample for AG alpha.
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_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.
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.
minu()
Computes the minimum length of the shortest path from f to g.
print_compute()
Prints out a COMPUTE specification
print_invar()
Print an invariant specification
print_spec()
Prints out a CTL specification
quad_mod_bdd_op()
Applies quaternary operation.
ternary_mod_bdd_op()
Applies ternary operation.
unary_bdd_op()
Applies unary operation.
unary_mod_bdd_op()
Applies unary operation.

Last updated on 2009/03/04 13h:34