Uses of Class
dev.civl.gmc.seq.StateManager
Packages that use StateManager
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.
-
Uses of StateManager in dev.civl.gmc
Constructors in dev.civl.gmc with parameters of type StateManager -
Uses of StateManager in dev.civl.gmc.concurrent
Subclasses of StateManager in dev.civl.gmc.concurrentModifier and TypeClassDescriptionclassConcurrentStateManagerIF<STATE,TRANSITION> A ConcurrentStateManager is used by aConcurrentDfsSearcherwhich encapsulates all methods that are needed byConcurrentDfsSearcheron STATE. -
Uses of StateManager in dev.civl.gmc.dpor
Methods in dev.civl.gmc.dpor with parameters of type StateManagerModifier and TypeMethodDescriptionbooleanDporStackEntry.nextTransition(StateManager<STATE, TRANSITION> manager) Increments to the next outgoing transition to be explored from the current state, moving to the next process in the backtrack set if necessary.Constructors in dev.civl.gmc.dpor with parameters of type StateManagerModifierConstructorDescriptionDporDfsSearcher(DependencyAnalyzer<STATE, TRANSITION> analyzer, StateManager<STATE, TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig) DporDfsSearcher(DependencyAnalyzer<STATE, TRANSITION> analyzer, StateManager<STATE, TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig, PrintStream debugOut) Constructs a new depth first search searcher.DporNodeFactory(StateManager<STATE, TRANSITION> stateManager, boolean saveStates) -
Uses of StateManager in dev.civl.gmc.seq
Constructors in dev.civl.gmc.seq with parameters of type StateManagerModifierConstructorDescriptionDfsSearcher(EnablerIF<STATE, TRANSITION> enabler, StateManager<STATE, TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig) DfsSearcher(EnablerIF<STATE, TRANSITION> enabler, StateManager<STATE, TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig, PrintStream debugOut) Constructs a new depth first search searcher.SequentialNodeFactory(StateManager<STATE, TRANSITION> stateManager, boolean saveStates) -
Uses of StateManager in dev.civl.gmc.smc
Subclasses of StateManager in dev.civl.gmc.smcModifier and TypeClassDescriptionclassThe implementation of the interfaceStateManagerused by SMC.