The root package of generic model checking is used to construct model checking applications, either sequential or concurrent.
Some of the services provided include:
- Command line parser to parse GMC configurations.
- Error Log to for recording errors and corresponding traces encountered during a model checking run.
- TransitionChooser to replay the trace file or conduct a simulation run.
- Trace represents a trace of an execution of a given model.
ClassDescriptionAn exception that is thrown if the command line arguments are not formatted correctly.A tool for parsing a command line and generating a
GMCConfiguration.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.GuidedTransitionChooser<STATE,
TRANSITION>Transition Chooser which makes its choice using an explicit "guide".An entry in an error log.An instance of this class represents a command-line parameter for a model checker.The types of option.RandomTransitionChooser<STATE, TRANSITION>An implementation of
TransitionChooserin which a transition is chosen randomly from the full set of the enabled transitions enabled at a state.Simulator<STATE,
TRANSITION>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
DfsSearcherif and only if 1) a cycle in state space detected; and 2) cycle violation is set to be reported.Trace<TRANSITION,
STATE>This represents a trace of an execution of a given model.TraceStepIF<STATE>A TraceStepIF represents the execution result of nextState of StateManagerIF.TransitionChooser<STATE, TRANSITION>General interface for an object which can select one enabled transition from the set of enabled transitions at any state.