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.