All Classes and Interfaces
Class
Description
An exception that is thrown if the command line arguments are not formatted
correctly.
A tool for parsing a command line and generating a
GMCConfiguration.
This ConcurrentDfsSearcher is implemented based on Alfons Laarman's algorithm
in paper "Partial-Order Reduction for Multi-Core LTL Model Checking", but
there are improvements being made.
A ConcurrentStateManager is used by a
ConcurrentDfsSearcher which
encapsulates all methods that are needed by ConcurrentDfsSearcher on
STATE.
A DfsSearcher performs a depth-first search of the state space of a
transition system, stopping immediately if it finds a state satisfying the
given predicate.
An EnablerIF tells you which transitions should be explored from a given
state.
A log for recording errors and corresponding traces encountered during a
model checking run.
An exception thrown when the number of errors encountered in the course of a
search of a state-transition system exceeds some specified bound.
The state predicate which simply returns "false" at every state.
A GMCConfiguration is composed of a number of GMCSection's, each of which
encapsulates a set of key-value pairs, where the keys correspond to
commandline parameters and the value is the value assigned to that parameter.
A GMCSection has a unique name and it encapsulates a set of key-value pairs,
where the keys correspond to commandline parameters and the value is the
value assigned to that parameter.
Transition Chooser which makes its choice using an explicit "guide".
An entry in an error log.
A simple directed graph implemented with a square matrix.
The threadPool That is used to manage the threads used in the algorithm.
An instance of this class represents a command-line parameter for a model
checker.
The types of option.
The predicate used for detecting violation state defined in the given list
states.This enumeration stores the result of checking "stack proviso" of a STATE in
the STATE-TRANSITION system.
An implementation of
TransitionChooser in which a transition is
chosen randomly from the full set of the enabled transitions enabled at a
state.A Node in the state graph for the sequential depth first search.
The factory to get a GMC search
SequentialNode, if the
SequentialNode has been seen before, the seen SequentialNode
will be returned, otherwise, a new SequentialNode will be created and
returned.The implementation of the interface
StateManager used by SMC.A
Simulator is used to execute a transition system using a
TransitionChooser to determine which transition to execute from each
state.This is a simple sequential model checker (SMC) implementing general model
checker (GMC).
The implementation of
EnablerIF used by SMC.The stack entry that is going to be pushed onto the stack during the search.
The stack entry that is going to be pushed onto the stack during the search.
A StateManagerIF provides part of a generic interface to a state-transition
system.
A state predicate is basically a function which returns either true or false
at any state in the transition system.
This is the Exception that will be thrown by the
DfsSearcher if and
only if 1) a cycle in state space detected; and 2) cycle violation is set to
be reported.This represents a trace of an execution of a given model.
The implementation of the interface
TraceStepIF used by SMC.A TraceStepIF represents the execution result of nextState of StateManagerIF.
General interface for an object which can select one enabled transition from
the set of enabled transitions at any state.