-
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.
-
mcTrace.c
- This module contains functions to build traces from bdd lists
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.
-
explain_and()
- Generates a witness path for car(formula) AND cdr(formula)
-
explain_eval()
- required
-
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
-
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_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.
-
compute_path_fb()
- Generates a counterexample from a path forward and a
path backward
-
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
-
check_invariant_forward_backward_with_break()
- Performs on the fly verification of the
invariant during reachability analysis.
-
print_invar()
- Print an invariant specification
-
print_result()
- Prints the result of the check if the check was performed,
does nothing otherwise
-
mc_rewrite_invar()
- Rewrites an invariant specification containing input
variables or next with an observer state variable
-
mc_rewrite_cleanup()
- Crean up the memory after the rewritten property check
-
check_invariant()
- Check the given invariant with the specified technology
-
forward_heuristic()
- Constant function to perform forward analysis
-
backward_heuristic()
- Constant function to perform backward analysis
-
never_stopping_heuristic()
- Constant function to perform backward, forward and
FB analysis
-
forward_backward_heuristic()
- Heuristic function used to decide the sept to perform
in forward-backward analysis
-
stopping_heuristic()
- Heuristic function used to decide whether to stop BDD
analysis to pass to BMC.
-
complete_bmc_trace_with_bdd()
- Completes a partial BMC tace in BDD-BMC analysis
mcLE.c
Language Emptiness
By: Marco Roveri
Check for language emptiness
See Alsooptional
-
Mc_CheckLanguageEmptiness()
- Checks whether the language is empty
-
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
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()
-
mcTrace.c
This module contains functions to build traces from bdd lists
By: Marco Pensallorto
-
Mc_create_trace_from_bdd_state_input_list()
- Creates a trace out of a < S (i, S)* > bdd list
-
Mc_trace_step_put_state_from_bdd()
- Populates a trace step with state assignments
-
Mc_trace_step_put_input_from_bdd()
- Populates a trace step with input assignments
Last updated on 2010/05/19 15h:56