Uses of Interface
dev.civl.mc.kripke.IF.Enabler

Packages that use Enabler

Package	Description
dev.civl.mc.kripke.IF	Module kripke provides the definition of various transitions and the enabler and state manager of CIVL.
dev.civl.mc.predicate.IF	Module predicate defines predicates that are required to hold for any CIVL-C programs.

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

Methods in dev.civl.mc.kripke.IF that return Enabler

Modifier and Type	Method	Description
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.

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

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.
static CIVLStateManager	Kripkes.newStateManager(Enabler enabler, Executor executor, SymbolicAnalyzer symbolicAnalyzer, CIVLErrorLogger errorLogger, CIVLConfiguration config)	Creates a new instance of state manager.

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

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

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