Index of modules
A | |
| APInv | |
| APInv [Option] | |
| Armc | |
| Atom [TraceChecker.T] |
Union type for the possible basic elements composing a trace.
|
| Automaton [Model.S] | |
C | |
| Cegar | |
| Cegar [Option] | |
| Closure [Model.S] | |
| Command [Model.S] | |
| Command [Model.SEMANTICS] | |
| Command [Model.AUTOMATON] | |
| Common [TraceCheckerUtil] |
Common utility functor for trace-checking engines.
|
| Control | |
| Control [Option] | |
D | |
| DiscardStates [TraceCheckerUtil] |
Functor transforming a given trace-checking engine by discarding
`State
regions and then reducing the obtained trace invariant.
|
E | |
| Edge [ReachabilityTree.Make] |
The printable type of possible inbound edges for a vertex.
|
L | |
| LazyAbstraction |
Lazy Abstraction Refinement Tree.
|
| LazyAbstraction [Option] | |
| Location [Model.AUTOMATON] | |
| Logging [Option] | |
M | |
| Main [Option] | |
| Make [Control] | |
| Make [Validator] |
Functor providing inductive invariant checking and path feasibility checking
functions for a given model.
|
| Make [ReachabilityTree] | |
| Make [StaticAnalyzer] | |
| Make [LazyAbstraction] | |
| Make [Cegar] | |
| Make [Armc] | |
| Make [ScmWrapper] |
Functor providing an implementation of the
Model.S interface for a given
global SCM.
|
| MakeBwd [UPInv] | |
| MakeBwd [APInv] | |
| MakeFwd [UPInv] | |
| MakeFwd [APInv] | |
| Miscellaneous [Option] | |
| Model |
This module defines the input interface of the model-checking engine,
which is given by the signature S below.
|
| ModelChecker |
Model Checker.
|
O | |
| Option |
This module manages global options and performs command-line processing.
|
| Owner [Model.AUTOMATON] | |
R | |
| ReachabilityTree |
Reachability Trees.
|
| Region [Model.CLOSURE] | |
| Region [Model.SEMANTICS] | |
| Result [TraceChecker.T] |
Type of possible results for the trace-checking function.
|
| Reverse [TraceCheckerUtil] |
Functor reversing a given trace-checking engine.
|
S | |
| ScmWrapper |
SCM Model Wrapper.
|
| ScmWrapper [Option] | |
| Semantics [Model.S] | |
| State [Model.S] | |
| StaticAnalyzer | |
| StaticAnalyzer [Option] | |
T | |
| T [TraceChecker] |
Common interface to all trace-checking engines.
|
| Trace [TraceChecker.T] |
A trace is a finite sequence of atoms.
|
| TraceChecker |
Trace Checker.
|
| TraceCheckerUtil |
Common utility functor for trace-checking engines.
|
| Transition [Model.AUTOMATON] | |
U | |
| UPInv | |
V | |
| Validate [TraceCheckerUtil] |
Functor wrapping a given trace-checking engine with result validation.
|
| Validator |
Inductive invariant checking and path feasibility.
|
| Vertex [ReachabilityTree.Make] |
Module to manage vertices.
|