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