Module dev.civl.mc

Package dev.civl.mc.kripke.IF

Class Kripkes

java.lang.Object

dev.civl.mc.kripke.IF.Kripkes

public class Kripkes
extends Object

This is the entry point of the module kripke.

Constructor Summary

Constructors

Constructor	Description
Kripkes()

Method Summary

Modifier and Type	Method	Description
static dev.civl.gmc.dpor.DependencyAnalyzer<State,Transition>	newDependencyAnalyzer(dev.civl.gmc.seq.StateManager<State,Transition> manager, StateFactory stateFactory, dev.civl.mc.kripke.common.SimpleEnabler enabler)
static Enabler	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.
static LibraryEnablerLoader	newLibraryEnablerLoader(LibraryEvaluatorLoader libEvaluatorLoader, CIVLConfiguration civlConfig)	Creates a new instance of library enabler loader.
static CIVLStateManager	newStateManager(Enabler enabler, Executor executor, SymbolicAnalyzer symbolicAnalyzer, CIVLErrorLogger errorLogger, CIVLConfiguration config)	Creates a new instance of state manager.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

Kripkes

public Kripkes()

Method Details

newEnabler

public static Enabler 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.

Parameters:

stateFactory - The state factory to be used.

evaluator - The evaluator to be used.

symbolicAnalyzer - The symbolic analyzer used in the system.

memUnitFactory - The memory unit factory for memory analysis.

libLoader - The library enabler loader to be used.

errorLogger - The error logger to be used.

civlConfig - The configuration of the CIVL model.

Returns:

The new enabler created.

newDependencyAnalyzer

public static dev.civl.gmc.dpor.DependencyAnalyzer<State,Transition> newDependencyAnalyzer(dev.civl.gmc.seq.StateManager<State,Transition> manager,
 StateFactory stateFactory,
 dev.civl.mc.kripke.common.SimpleEnabler enabler)

newLibraryEnablerLoader

public static LibraryEnablerLoader newLibraryEnablerLoader(LibraryEvaluatorLoader libEvaluatorLoader,
 CIVLConfiguration civlConfig)

Creates a new instance of library enabler loader.

Parameters:

libEvaluatorLoader - the library evaluator loader

civlConfig - the CIVL configuration

Returns:

The new library enabler loader created.

newStateManager

public static CIVLStateManager newStateManager(Enabler enabler,
 Executor executor,
 SymbolicAnalyzer symbolicAnalyzer,
 CIVLErrorLogger errorLogger,
 CIVLConfiguration config)

Creates a new instance of state manager.

Parameters:

enabler - The enabler to be used.

executor - The executor to be used.

symbolicAnalyzer - The symbolic analyzer to be used.

errorLogger - The error logger to be used.

config - The configuration of the CIVL model.

Returns:

The new state manager created.