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