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/11/04 13h:34