A |
active [ReachabilityTree.Make] |
active t u returns true iff the vertex u is active in the tree t .
|
add_covering [ReachabilityTree.Make] |
add_covering t v w adds the covering pair v ◅ w to the tree t .
|
add_vertex [ReachabilityTree.Make] |
add_vertex t loc reg m e creates a new vertex u with location loc ,
region reg and mark m , and adds u to the tree t , with inbound edge
e .
|
ancestor [ReachabilityTree.Make] |
ancestor t u v is true iff u is an ancestor of v in the tree t .
|
arg_spec [Option.Miscellaneous] |
|
arg_spec [Option.Logging] |
|
arg_spec [Option.APInv] |
|
arg_spec [Option.LazyAbstraction] |
|
arg_spec [Option.Cegar] |
|
arg_spec [Option.Control] |
|
arg_spec [Option.StaticAnalyzer] |
|
arg_spec [Option.ScmWrapper] |
|
arg_spec_of_integer [Option] |
|
arg_spec_of_symbols [Option] |
|
atom_strong_post [TraceCheckerUtil.Common] |
|
atom_strong_pre [TraceCheckerUtil.Common] |
|
atom_weak_post [TraceCheckerUtil.Common] |
|
atom_weak_pre [TraceCheckerUtil.Common] |
|
B |
bot [Model.REGION] |
|
C |
channel_policy [Option.ScmWrapper] |
|
channel_policy_names [Option.ScmWrapper] |
|
channel_policy_opt [Option.ScmWrapper] |
|
check_global [ScmWrapper] |
|
clo [Model.CLOSURE] |
|
clr_coverees [ReachabilityTree.Make] |
clr_coverees t w removes all covering pairs · ◅ w from the tree t .
|
clr_coverers [ReachabilityTree.Make] |
clr_coverers t v removes all covering pairs v ◅ · from the tree t .
|
command [Model.AUTOMATON.Transition] |
|
compare [ReachabilityTree.Make.Vertex] |
Total ordering over vertices (creation order).
|
compare [Model.AUTOMATON.Location] |
|
compare [Model.AUTOMATON.Owner] |
|
compl [Model.REGION] |
|
control [Control.Make] |
|
control_arg_spec [Option.Main] |
|
control_arg_spec [Option] |
|
create [ReachabilityTree.Make] |
create () creates a new, empty reachability tree.
|
D |
del_covering [ReachabilityTree.Make] |
del_covering t v w removes the covering pair v ◅ w from the tree t .
|
del_vertex [ReachabilityTree.Make] |
del_vertex t u removes the vertex u , as well as its subtree, from the
tree t .
|
depth [ReachabilityTree.Make] |
depth t u returns the depth of u in the tree t .
|
direction [Option.StaticAnalyzer] |
|
direction_opt [Option.StaticAnalyzer] |
|
dump [Model.REGION] |
|
E |
edge [ReachabilityTree.Make] |
edge t u returns the inbound edge of the vertex u in the tree t .
|
eq [Model.REGION] |
|
equal [ReachabilityTree.Make.Vertex] |
Equality predicate on vertices.
|
equal [Model.AUTOMATON.Location] |
|
equal [Model.AUTOMATON.Owner] |
|
extrapol_coloring [Option.ScmWrapper] |
|
extrapol_coloring_names [Option.ScmWrapper] |
|
extrapol_coloring_opt [Option.ScmWrapper] |
|
extrapolation [Option.ScmWrapper] |
|
extrapolation_names [Option.ScmWrapper] |
|
extrapolation_opt [Option.ScmWrapper] |
|
F |
fold_children [ReachabilityTree.Make] |
fold_children f t u a returns (f vN ... (f v2 (f v1 a))...) , where v1,
..., vN are the children of u in t , in increasing order.
|
fold_coverees [ReachabilityTree.Make] |
fold_coverees f t u a returns (f vN ... (f v2 (f v1 a))...) , where v1,
..., vN are the coverees of u in t , in increasing order.
|
fold_coverers [ReachabilityTree.Make] |
fold_coverers f t u a returns (f vN ... (f v2 (f v1 a))...) , where v1,
..., vN are the coverers of u in t , in increasing order.
|
fold_error [Model.S] |
|
fold_in_transitions [Model.AUTOMATON] |
|
fold_init [Model.S] |
|
fold_location [ReachabilityTree.Make] |
fold_location f t loc a returns (f uN ... (f u2 (f u1 a))...) , where
u1, ..., uN are the vertices of t with location loc , in increasing
order.
|
fold_locations [Model.AUTOMATON] |
|
fold_out_transitions [Model.AUTOMATON] |
|
fold_owners [Model.AUTOMATON] |
|
fold_transitions [Model.AUTOMATON] |
|
fold_vertices [ReachabilityTree.Make] |
fold_vertices pre post t u a is similar to iter_vertices pre post t u ,
but returns a value.
|
forward_backward_names [Option.StaticAnalyzer] |
|
G |
give_message [Model.COMMAND] |
|
give_queue [Model.COMMAND] |
|
give_type [Model.COMMAND] |
|
graph_exploration [Option.Cegar] |
|
graph_exploration_names [Option.Cegar] |
|
graph_exploration_opt [Option.Cegar] |
|
graph_refinement [Option.Cegar] |
|
graph_refinement_names [Option.Cegar] |
|
graph_refinement_opt [Option.Cegar] |
|
H |
has_children [ReachabilityTree.Make] |
has_children t u returns true iff the vertex u has at least one child
in the tree t .
|
has_coverees [ReachabilityTree.Make] |
has_coverees t w returns true iff there exists a covering pair · ◅ w
in the tree t .
|
has_coverers [ReachabilityTree.Make] |
has_coverers t v returns true iff there exists a covering pair v ◅ ·
in the tree t .
|
hash [ReachabilityTree.Make.Vertex] |
Hashing function on vertices.
|
hash [Model.AUTOMATON.Location] |
|
hash [Model.AUTOMATON.Owner] |
|
I |
initialize [Option] |
|
inter [Model.REGION] |
|
is_controllable [Model.AUTOMATON.Transition] |
|
is_empty_path_feasible [Validator.Make] |
is_empty_path_feasible () returns true if there is a non empty
intersection between initial and error symbolic states of the model.
|
is_non_empty_path_bwd_feasible [Validator.Make] |
is_non_empty_path_bwd_feasible p returns true if p is a non empty path
that is feasible.
|
is_non_empty_path_fwd_feasible [Validator.Make] |
is_non_empty_path_fwd_feasible p returns true if p is a non empty path
that is feasible.
|
is_safe_bwd_invariant [Validator.Make] |
is_safe_bwd_invariant l returns true if l is a safe backward inductive
invariant:
l contains all error symbolic states of the model, and, l is a post-fixpoint of the model's pre image operator, and, l is disjoint from all initial symbolic states of the model.
|
is_safe_fwd_invariant [Validator.Make] |
is_safe_fwd_invariant l returns true if l is a safe forward inductive
invariant:
l contains all initial symbolic states of the model, and, l is a post-fixpoint of the model's post image operator, and, l is disjoint from all error symbolic states of the model.
|
iter_children [ReachabilityTree.Make] |
iter_children f t u applies f in turn to all children of u in t , in
increasing order.
|
iter_coverees [ReachabilityTree.Make] |
iter_coverees f t u applies f in turn to all coverees of u in t , in
increasing order.
|
iter_coverers [ReachabilityTree.Make] |
iter_coverers f t u applies f in turn to all coverers of u in t , in
increasing order.
|
iter_error [Model.S] |
|
iter_in_transitions [Model.AUTOMATON] |
|
iter_init [Model.S] |
|
iter_location [ReachabilityTree.Make] |
iter_location f t loc applies f in turn to all vertices of t with
location loc , in increasing order.
|
iter_locations [Model.AUTOMATON] |
|
iter_out_transitions [Model.AUTOMATON] |
|
iter_owners [Model.AUTOMATON] |
|
iter_transitions [Model.AUTOMATON] |
|
iter_vertices [ReachabilityTree.Make] |
iter_vertices pre post t u traverses the subtree of t rooted in u ,
applying the pre-order operation pre and the post-order operation post
to all visited vertices.
|
K |
k [Option.Main] |
|
k_max [Option.Main] |
|
k_max_opt [Option.Main] |
|
k_min [Option.Main] |
|
k_min_opt [Option.Main] |
|
k_opt [Option.Main] |
|
key_of_value [Option] |
|
L |
leq [Model.REGION] |
|
limit [Option.Main] |
|
limit_opt [Option.Main] |
|
location [ReachabilityTree.Make.Vertex] |
location u returns the location of the vertex u .
|
M |
make_global [ScmWrapper] |
|
mark [ReachabilityTree.Make.Vertex] |
mark u returns the mark of the vertex u .
|
mc_engine [Option.Main] |
|
mc_engine_names [Option.Main] |
|
mc_engine_opt [Option.Main] |
|
mem_vertex [ReachabilityTree.Make] |
mem_vertex t u tests whether the tree t contains the vertex u .
|
minus [Model.REGION] |
|
model_check [ModelChecker.S] |
The model-checking function.
|
N |
nb_error [Model.S] |
|
nb_init [Model.S] |
|
nb_locations [Model.AUTOMATON] |
|
nb_owners [Model.AUTOMATON] |
|
nb_transitions [Model.AUTOMATON] |
|
nb_vertices [ReachabilityTree.Make] |
nb_vertices t returns the number of vertices in the tree t .
|
num_state_atoms [TraceCheckerUtil.Common] |
num_state_atoms a m n returns the number of `State atoms in the array
a , between the indexes m and n (inclusive).
|
O |
owner [Model.AUTOMATON.Transition] |
|
P |
parent [ReachabilityTree.Make] |
parent t u returns the parent of the vertex u in the tree t (if any).
|
parse [ScmWrapper] |
|
post [Model.SEMANTICS] |
|
pre [Model.SEMANTICS] |
|
print [TraceChecker.T.Result] |
|
print [TraceChecker.T.Trace] |
|
print [TraceChecker.T.Atom] |
|
print_automaton [Model.AUTOMATON] |
|
print_model [Model.S] |
|
R |
reduce_bwd_invariant [TraceCheckerUtil.Common] |
reduce_bwd_invariant inv takes a backward trace invariant (that might be
reducible), reduces it and returns the resulting irreducible backward
trace invariant.
|
reduce_fwd_invariant [TraceCheckerUtil.Common] |
reduce_fwd_invariant inv takes a forward trace invariant (that might be
reducible), reduces it and returns the resulting irreducible forward
trace invariant.
|
refine [ReachabilityTree.Make.Vertex] |
refine u reg replaces the region of u by reg .
|
region [ReachabilityTree.Make.Vertex] |
region u returns the region of the vertex u .
|
rel [Model.SEMANTICS] |
|
rel_cmd_impl [Option.ScmWrapper] |
|
rel_cmd_impl_names [Option.ScmWrapper] |
|
rel_cmd_impl_opt [Option.ScmWrapper] |
|
result_validation [Option.Main] |
|
result_validation_opt [Option.Main] |
|
S |
safe_approximation [Option.APInv] |
|
safe_approximation_names [Option.APInv] |
|
safe_approximation_opt [Option.APInv] |
|
scm_consistency_check [Option.Main] |
|
scm_consistency_check_opt [Option.Main] |
|
scm_source_file [Option.Main] |
|
scm_source_file_opt [Option.Main] |
|
show_estimate [Option.Control] |
|
show_estimate_opt [Option.Control] |
|
show_statistics [Option.Main] |
|
show_statistics_opt [Option.Main] |
|
simplify [Model.REGION] |
|
simulation_mode [Option.Control] |
|
simulation_mode_names [Option.Control] |
|
simulation_mode_opt [Option.Control] |
|
simulation_only [Option.Control] |
|
simulation_only_opt [Option.Control] |
|
size [Model.REGION] |
|
source [Model.AUTOMATON.Transition] |
|
T |
target [Model.AUTOMATON.Transition] |
|
tc_discard_states [Option.Main] |
|
tc_discard_states_opt [Option.Main] |
|
tc_engine [Option.Main] |
|
tc_engine_names [Option.Main] |
|
tc_engine_opt [Option.Main] |
|
tc_validate [Option.Main] |
|
tc_validate_opt [Option.Main] |
|
top [Model.REGION] |
|
trace_check [TraceChecker.S] |
The trace-checking function.
|
tree_exploration [Option.LazyAbstraction] |
|
tree_exploration_names [Option.LazyAbstraction] |
|
tree_exploration_opt [Option.LazyAbstraction] |
|
tree_pruning [Option.LazyAbstraction] |
|
tree_pruning_opt [Option.LazyAbstraction] |
|
U |
union [Model.REGION] |
|
usage_msg [Option] |
|
V |
value_of_key [Option] |
|
verify_arg_spec [Option.Main] |
|
verify_arg_spec [Option] |
|