-
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:13