-
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/01/30 14h:53