Uses of Interface
dev.civl.gmc.StatePredicateIF

Packages that use StatePredicateIF

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.smc	A simple implementation of General Model Checker (GMC) is used by a set of code coverage test cases.

Uses of StatePredicateIF in dev.civl.gmc

Classes in dev.civl.gmc that implement StatePredicateIF

Modifier and Type	Class	Description
class	FalsePredicate<S>	The state predicate which simply returns "false" at every state.

Methods in dev.civl.gmc that return StatePredicateIF

Modifier and Type	Method	Description
StatePredicateIF<STATE>	Simulator.getPredicate()

Methods in dev.civl.gmc with parameters of type StatePredicateIF

Modifier and Type	Method	Description
void	Simulator.setPredicate(StatePredicateIF<STATE> predicate)

Uses of StatePredicateIF in dev.civl.gmc.concurrent

Methods in dev.civl.gmc.concurrent that return StatePredicateIF

Modifier and Type	Method	Description
StatePredicateIF<STATE>	ConcurrentDfsSearcher.predicate()

Constructors in dev.civl.gmc.concurrent with parameters of type StatePredicateIF

Modifier	Constructor	Description
	ConcurrentDfsSearcher(EnablerIF<STATE,TRANSITION> enabler, ConcurrentStateManagerIF<STATE,TRANSITION> manager, StatePredicateIF<STATE> predicate, int N)

Uses of StatePredicateIF in dev.civl.gmc.dpor

Methods in dev.civl.gmc.dpor that return StatePredicateIF

Modifier and Type	Method	Description
StatePredicateIF<STATE>	DporDfsSearcher.predicate()

Constructors in dev.civl.gmc.dpor with parameters of type StatePredicateIF

Modifier	Constructor	Description
	DporDfsSearcher(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.

Uses of StatePredicateIF in dev.civl.gmc.seq

Methods in dev.civl.gmc.seq that return StatePredicateIF

Modifier and Type	Method	Description
StatePredicateIF<STATE>	DfsSearcher.predicate()

Constructors in dev.civl.gmc.seq with parameters of type StatePredicateIF

Modifier	Constructor	Description
	DfsSearcher(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.

Uses of StatePredicateIF in dev.civl.gmc.smc

Classes in dev.civl.gmc.smc that implement StatePredicateIF

Modifier and Type	Class	Description
class	Predicate	The predicate used for detecting violation state defined in the given list states.

Methods in dev.civl.gmc.smc with parameters of type StatePredicateIF

Modifier and Type	Method	Description
boolean	SMC.run(MatrixDirectedGraph graph, StatePredicateIF<Integer> predicate, GMCConfiguration config)	For a given MatrixDirectedGraph graph and a predicate implementing StatePredicateIF, If the predicate is hold, true will be returned, else false. Note that the default starting state is the state with id of 0
boolean	SMC.run(MatrixDirectedGraph graph, StatePredicateIF<Integer> predicate, Integer initialState, GMCConfiguration config)	For a given MatrixDirectedGraph graph, a predicate implementing StatePredicateIF and a starting state initialState, If the predicate is hold, true will be returned, else false.
Trace<String,Integer>	SMCSimulator.run(MatrixDirectedGraph graph, StatePredicateIF<Integer> predicate)
Trace<String,Integer>	SMCSimulator.run(MatrixDirectedGraph graph, StatePredicateIF<Integer> predicate, Integer initialState)