-
mc.h
- External header file
-
mcInt.h
- Internal header file
-
mcAGonly.c
- This file contains the code to deal with AG formulas in a
special way.
-
mcCmd.c
- Model checking commands.
-
mcEval.c
- CTL to BDD compiler
-
mcExplain.c
- Witness and Debug generator for Fair CTL models.
-
mcInvar.c
- Dedicated algorithms for the verification of
invariants on-the-fly wrt reachability analysis.
-
mcLE.c
- Language Emptiness
-
mcMc.c
- Fair CTL model checking routines.
mc.h
External header file
By: Marco Roveri, Roberto Cavada
mcInt.h
Internal header file
By: Marco Roveri
See AlsomcMc.c
mcExplain.c
mcAGonly.c
This file contains the code to deal with AG formulas in a
special way.
By: Marco Roveri
This file contains the code to deal with AG formulas
only, using special purpose algorithms. This functionality is invoked
with the -AG option and works only in conjunction with the -f
(forward search) option.
See AlsomcMc.c
mcEval.c
mcExplain.c
-
Mc_CheckAGOnlySpec()
- This function checks for SPEC of the form AG
alpha in "context".
-
check_AG_only()
- This function checks for SPEC of the form AG
alpha in "context".
-
make_AG_counterexample()
- This function constructs a counterexample
starting from state target_state
-
is_AG_only_formula()
- Checks if the formulas is of type AGOnly.
-
is_AG_only_formula_recur()
- Recursive function that helps is_AG_only_formula.
mcCmd.c
Model checking commands.
By: Marco Roveri
This file contains all the shell command to deal with
model checking and for counterexample navigation.
See AlsocmdCmd.c
-
Mc_Init()
- Initializes the mc package.
-
Mc_End()
- Quit the mc package
-
Mc_check_psl_property()
- Top-level function for mc of PSL properties
-
CommandCheckCtlSpec()
- Performs fair CTL model checking.
-
CommandCheckInvar()
- Performs model checking of invariants
-
CommandCheckCompute()
- Performs computation of quantitative characteristics
-
CommandCheckPslSpec()
- Performs fair PSL model checking.
-
CommandLanguageEmptiness()
- Checks for language emptiness.
-
CommandCheckSpec()
- Deprecated version of CommandCheckCtlSpec
mcEval.c
CTL to BDD compiler
By: Marco Roveri
In this file there is the code to compile CTL formulas
into BDD and the code to call the model checking algorithms.
See AlsomcMc.c
mcExplain.c
mcACTL.c
-
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.
-
eval_compute()
- Computes shortest and longest length of the path
between two set of states.
-
free_formula_list()
- Frees a list of BDD as generated by eval_formula_list
-
eval_ctl_spec_recur()
- Recursive step of
eval_ctl_spec
.
-
eval_compute_recur()
- Recursive step of
eval_compute
.
-
unary_bdd_op()
- Applies unary operation.
-
binary_bdd_op()
- Applies binary operation.
-
unary_mod_bdd_op()
- Applies unary operation.
-
binary_mod_bdd_op()
- Applies binary operation.
-
binary_mod_bdd_op_ns()
- Applies binary operation.
-
ternary_mod_bdd_op()
- Applies ternary operation.
-
quad_mod_bdd_op()
- Applies quaternary operation.
mcExplain.c
Witness and Debug generator for Fair CTL models.
By: Marco Roveri
This file contains the code to find counterexamples
execution trace that shows a cause of the problem. Here are
implemented the techniques described in the CMU-CS-94-204 Technical
Report by E. Clarke, O. Grumberg, K. McMillan and X. Zhao.
See AlsomcMc.c
-
explain()
- Counterexamples and witnesses generator.
-
ex_explain()
- This function computes a path that is a witness
for EX(f).
-
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_explain()
- This function finds a path that is a witness
for E[f U g]
-
eg_explain()
- This function finds a path that is an example
for EG(g).
-
ebu_explain()
- This function finds a path that is a witness
for E[f U g]^{sup}_{inf}.
-
ebg_explain()
- This function finds a path of length
(sup-inf) that is an example for
EG(g)^{sup}_{inf}.
-
explain_recur()
- Recursively traverse the formula CTL and rewrite
it in order to use the base witnesses generator functions.
-
fairness_explain()
- Auxiliary function to the computation of a
witness of the formula EG f.
-
Extend_trace_with_state_input_pair()
-
-
Extend_trace_with_states_inputs_pair()
-
-
Check_TraceList_Sanity()
-
mcInvar.c
Dedicated algorithms for the verification of
invariants on-the-fly wrt reachability analysis.
By: Marco Roveri
Dedicated algorithms for the verification of
invariants on-the-fly wrt reachability analysis.
See AlsomcMc.c
-
Mc_CheckInvar()
- Verifies that M,s0 |= AG alpha
-
compute_and_print_path()
- Extracts and prints a counterexample for AG alpha.
-
check_invariant_forward()
- Performs on the fly verification of the
invariant during reachability analysis.
-
compute_and_print_path_fb()
-
-
check_invariant_forward_backward()
- Performs on the fly verification of the
invariant during reachability analysis.
-
print_invar()
- Print an invariant specification
mcLE.c
Language Emptiness
By: Marco Roveri
Check for language emptiness
See Alsooptional
-
Mc_CheckLanguageEmptiness()
- Checks whether the language is empty
mcMc.c
Fair CTL model checking routines.
By: Marco Roveri
Fair CTL model checking routines.
See AlsomcExplain.c
-
Mc_CheckCTLSpec()
- Verifies that M,s0 |= alpha
-
Mc_CheckCompute()
- Compute quantitative characteristics on the model.
-
ex()
- Set of states satisfying EX(g).
-
eu()
- Set of states satisfying E[ f U g ].
-
eg()
- Set of states satisfying EF(g).
-
ef()
- Set of states satisfying EF(g).
-
au()
- Set of states satisfying A[f U g].
-
ex_si()
- Set of states satisfying EG(g).
-
eu_si()
- Computes the set of state-input pairs that satisfy
E(f U g), with f and g sets of state-input pairs.
-
eg_si()
- Set of states-inputs satisfying EG(g).
-
ebu()
- Set of states satisfying E[f U^{inf..sup} g].
-
ebf()
- Set of states satisfying EF^{inf..sup}(g).
-
ebg()
- Set of states satisfying EG^{inf..sup}(g).
-
abu()
- Set of states satisfying A[f U^{inf..sup} g].
-
minu()
- Computes the minimum length of the shortest path
from f to g.
-
maxu()
- This function computes the maximum length of the
shortest path from f to g.
-
print_spec()
- Prints out a CTL specification
-
print_compute()
- Prints out a COMPUTE specification
-
Mc_fair_si_iteration()
-
-
Mc_get_fair_si_subset()
-
Last updated on 2009/03/04 13h:34