Uses of Interface
dev.civl.mc.state.IF.StateFactory

Packages that use StateFactory

Package	Description
dev.civl.mc.dynamic.IF	Module dynamic provides general computations of symbolic expressions, including the pretty printing method.
dev.civl.mc.kripke.IF	Module kripke provides the definition of various transitions and the enabler and state manager of CIVL.
dev.civl.mc.log.IF	Module log provides the data structure for logging errors during verification.
dev.civl.mc.predicate.IF	Module predicate defines predicates that are required to hold for any CIVL-C programs.
dev.civl.mc.semantics.IF	Module semantics implements the semantics of CIVL-C.
dev.civl.mc.state.IF	Module state is responsible for the creation and manipulation of states of a CIVL model.

Uses of StateFactory in dev.civl.mc.dynamic.IF

Methods in dev.civl.mc.dynamic.IF with parameters of type StateFactory

Modifier and Type	Method	Description
static SymbolicUtility	Dynamics.newSymbolicUtility(dev.civl.sarl.IF.SymbolicUniverse universe, ModelFactory modelFactory, StateFactory stateFactory)	Creates a new instance of symbolic utility.

Uses of StateFactory in dev.civl.mc.kripke.IF

Methods in dev.civl.mc.kripke.IF with parameters of type StateFactory

Modifier and Type	Method	Description
static dev.civl.gmc.dpor.DependencyAnalyzer<State,Transition>	Kripkes.newDependencyAnalyzer(dev.civl.gmc.seq.StateManager<State,Transition> manager, StateFactory stateFactory, dev.civl.mc.kripke.common.SimpleEnabler enabler)
static Enabler	Kripkes.newEnabler(StateFactory stateFactory, Evaluator evaluator, Executor executor, SymbolicAnalyzer symbolicAnalyzer, MemoryUnitFactory memUnitFactory, LibraryEnablerLoader libLoader, CIVLErrorLogger errorLogger, CIVLConfiguration civlConfig, dev.civl.gmc.GMCConfiguration gmcConfig)	Creates a new instance of enabler.

Uses of StateFactory in dev.civl.mc.log.IF

Constructors in dev.civl.mc.log.IF with parameters of type StateFactory

Modifier	Constructor	Description
	CIVLErrorLogger(File directory, String sessionName, PrintStream out, CIVLConfiguration civlConfig, dev.civl.gmc.GMCConfiguration gmcConfig, StateFactory stateFactory, dev.civl.sarl.IF.SymbolicUniverse universe, boolean solve)	creates a new instance of error logger.

Uses of StateFactory in dev.civl.mc.predicate.IF

Methods in dev.civl.mc.predicate.IF with parameters of type StateFactory

Modifier and Type	Method	Description
static Deadlock	Predicates.newDeadlock(dev.civl.sarl.IF.SymbolicUniverse universe, Enabler enabler, StateFactory stateFactory, SymbolicAnalyzer symbolicAnalyzer)

Uses of StateFactory in dev.civl.mc.semantics.IF

Methods in dev.civl.mc.semantics.IF that return StateFactory

Modifier and Type	Method	Description
StateFactory	Evaluator.stateFactory()	The state factory should be the unique one used in the system.
StateFactory	Executor.stateFactory()

Methods in dev.civl.mc.semantics.IF with parameters of type StateFactory

Modifier and Type	Method	Description
static Evaluator	Semantics.newErrorSideEffectFreeEvaluator(ModelFactory modelFactory, StateFactory stateFactory, LibraryEvaluatorLoader loader, LibraryExecutorLoader loaderExec, SymbolicUtility symbolicUtil, SymbolicAnalyzer symbolicAnalyzer, MemoryUnitFactory memUnitFactory, CIVLErrorLogger errLogger, CIVLConfiguration config)	Creates a new instance of ErrorSideEffectFreeEvaluator.
static Evaluator	Semantics.newEvaluator(ModelFactory modelFactory, StateFactory stateFactory, LibraryEvaluatorLoader loader, LibraryExecutorLoader loaderExec, SymbolicUtility symbolicUtil, SymbolicAnalyzer symbolicAnalyzer, MemoryUnitFactory memUnitFactory, CIVLErrorLogger errLogger, CIVLConfiguration config)	Creates a new instance of CIVL evaluator.
static Executor	Semantics.newExecutor(ModelFactory modelFactory, StateFactory stateFactory, LibraryExecutorLoader loader, Evaluator evaluator, SymbolicAnalyzer symbolicAnalyzer, CIVLErrorLogger errLogger, CIVLConfiguration civlConfig)	Creates a new instance of CIVL executor.

Uses of StateFactory in dev.civl.mc.state.IF

Methods in dev.civl.mc.state.IF that return StateFactory

Modifier and Type	Method	Description
static StateFactory	States.newImmutableStateFactory(ModelFactory modelFactory, MemoryUnitFactory memFactory, CIVLConfiguration config)	Returns a new immutable state factory based on the given model factory.

Methods in dev.civl.mc.state.IF with parameters of type StateFactory

Modifier and Type	Method	Description
void	MemoryUnitFactory.add(MemoryUnitSet muSet, dev.civl.sarl.IF.expr.SymbolicExpression pointer, StateFactory stateFactory)