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