Module dev.civl.gmc

Package dev.civl.gmc.smc

package dev.civl.gmc.smc

A simple implementation of General Model Checker (GMC) is used by a set of code coverage test cases. And it can be regarded as a simple example of the implementation of client part of GMC.

Related Packages

Package	Description
dev.civl.gmc	The root package of generic model checking is used to construct model checking applications, either sequential or concurrent.
dev.civl.gmc.concurrent	This package provides concurrent generic model checking functionality.
dev.civl.gmc.dpor
dev.civl.gmc.seq	This package provides sequential generic model checking functionality.
dev.civl.gmc.util	The utility package for GMC, providing a set of utility classes and functions used by GMC.

Classes

Class	Description
MatrixDirectedGraph	A simple directed graph implemented with a square matrix.
Predicate	The predicate used for detecting violation state defined in the given list states.
SimpleStateManager	The implementation of the interface StateManager used by SMC.
SMC	This is a simple sequential model checker (SMC) implementing general model checker (GMC).
SMCConstants
SMCEnabler	The implementation of EnablerIF used by SMC.
SMCSimulator
TraceStep	The implementation of the interface TraceStepIF used by SMC.