Uses of Interface
dev.civl.mc.model.IF.ModelFactory

Packages that use ModelFactory

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.model.IF	Module model defines a static model, i.e., the control flow graph, representation of a CIVL-C program.
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 ModelFactory in dev.civl.mc.dynamic.IF

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

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 ModelFactory in dev.civl.mc.kripke.IF

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

Modifier and Type	Method	Description
LibraryEnabler	LibraryEnablerLoader.getLibraryEnabler(String name, Enabler primaryEnabler, Evaluator evaluator, ModelFactory modelFacotry, SymbolicUtility symbolicUtil, SymbolicAnalyzer symbolicAnalyzer)	Obtains the library executor of the given name.

Uses of ModelFactory in dev.civl.mc.model.IF

Methods in dev.civl.mc.model.IF that return ModelFactory

Modifier and Type	Method	Description
ModelFactory	Model.factory()
ModelFactory	ModelBuilder.factory()

Methods in dev.civl.mc.model.IF with parameters of type ModelFactory

Modifier and Type	Method	Description
void	Fragment.addGuardToStartLocation(Expression guard, ModelFactory factory)	Add a specified guard to the all statements of the start location.
void	CIVLFunction.computePathconditionOfLocations(ModelFactory modelFactory)
static ModelBuilder	Models.newModelBuilder(ModelFactory factory)	Creates a new instance of model builder.

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

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

Modifier and Type	Method	Description
static PotentialDeadlock	Predicates.newPotentialDeadlock(dev.civl.sarl.IF.SymbolicUniverse universe, Enabler enabler, LibraryEnablerLoader loader, Evaluator evaluator, ModelFactory modelFactory, SymbolicUtility symbolicUtil, SymbolicAnalyzer symbolicAnalyzer)

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

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

Modifier and Type	Method	Description
ModelFactory	Evaluator.modelFactory()	The model factory should be the unique one used in the system.

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

Modifier and Type	Method	Description
LibraryEvaluator	LibraryEvaluatorLoader.getLibraryEvaluator(String name, Evaluator primaryEvaluator, ModelFactory modelFacotry, SymbolicUtility symbolicUtil, SymbolicAnalyzer symbolicAnalyzer)	Obtains the library evaluator of the given name.
LibraryExecutor	LibraryExecutorLoader.getLibraryExecutor(String name, Executor primaryExecutor, ModelFactory modelFacotry, SymbolicUtility symbolicUtil, SymbolicAnalyzer symbolicAnalyzer)	Obtains the library executor of the given name.
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.
static SymbolicAnalyzer	Semantics.newSymbolicAnalyzer(CIVLConfiguration civlConfig, CIVLErrorLogger errorLogger, dev.civl.sarl.IF.SymbolicUniverse universe, ModelFactory modelFactory, SymbolicUtility symbolicUtil)	Creates a new instance of symbolic analyzer.

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

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

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.