Uses of Package
dev.civl.gmc
Packages that use dev.civl.gmc
Package
Description
The root package of generic model checking is used to construct model
checking applications, either sequential or concurrent.
This package provides concurrent generic model checking functionality.
This package provides sequential generic model checking functionality.
A simple implementation of General Model Checker (GMC) is used by a set of
code coverage test cases.
-
Classes in dev.civl.gmc used by dev.civl.gmcClassDescriptionAn exception that is thrown if the command line arguments are not formatted correctly.A log for recording errors and corresponding traces encountered during a model checking run.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.An entry in an error log.An instance of this class represents a command-line parameter for a model checker.The types of option.A state predicate is basically a function which returns either true or false at any state in the transition system.This represents a trace of an execution of a given model.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.
-
Classes in dev.civl.gmc used by dev.civl.gmc.concurrentClassDescriptionA state predicate is basically a function which returns either true or false at any state in the transition system.
-
Classes in dev.civl.gmc used by dev.civl.gmc.dporClassDescriptionA 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 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.A TraceStepIF represents the execution result of nextState of StateManagerIF. -
Classes in dev.civl.gmc used by dev.civl.gmc.seqClassDescriptionA 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 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.A TraceStepIF represents the execution result of nextState of StateManagerIF. -
Classes in dev.civl.gmc used by dev.civl.gmc.smcClassDescriptionA 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.An instance of this class represents a command-line parameter for a model checker.A state predicate is basically a function which returns either true or false at any state in the transition system.This represents a trace of an execution of a given model.A TraceStepIF represents the execution result of nextState of StateManagerIF.