Index of values


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 vw 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 vw 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]