Module dev.civl.mc
Package dev.civl.mc.semantics.IF

Class Semantics

java.lang.Object
dev.civl.mc.semantics.IF.Semantics
public class Semantics extends Object
Entry point of the module civl.semantics.

  • Constructor Details

    • Semantics

      public Semantics()

  • Method Details

    • newLibraryExecutorLoader

      public static LibraryExecutorLoader newLibraryExecutorLoader(LibraryEvaluatorLoader libEvaluatorLoader, CIVLConfiguration civlConfig)
      Creates a new instance of library executor loader.
      Returns:
      The new library executor loader.

    • newLibraryEvaluatorLoader

      public static LibraryEvaluatorLoader newLibraryEvaluatorLoader(CIVLConfiguration civlConfig)
      Creates a new instance of library evaluator loader.
      Returns:
      The new library evaluator loader.

    • newExecutor

      public static Executor newExecutor(ModelFactory modelFactory, StateFactory stateFactory, LibraryExecutorLoader loader, Evaluator evaluator, SymbolicAnalyzer symbolicAnalyzer, CIVLErrorLogger errLogger, CIVLConfiguration civlConfig)
      Creates a new instance of CIVL executor.
      Parameters:
      modelFactory - The model factory of the system.
      stateFactory - The state factory of the system.
      loader - The library executor loader for executing system functions.
      evaluator - The CIVL evaluator for evaluating expressions.
      symbolicAnalyzer - The symbolic analyzer used in the system.
      errLogger - The error logger for reporting execution errors.
      civlConfig - The CIVL configuration.
      log - The error logger of the system.
      Returns:
      The new CIVL executor.

    • newEvaluator

      public static Evaluator 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.
      Parameters:
      modelFactory - The model factory of the system.
      stateFactory - The state factory of the system.
      loader - The library evaluator loader for evaluating the guards of system functions.
      symbolicUtil - The symbolic utility for manipulations of symbolic expressions.
      symbolicAnalyzer - The symbolic analyzer used in the system.
      errLogger - The error logger for reporting execution errors.
      Returns:
      The new CIVL evaluator.

    • newErrorSideEffectFreeEvaluator

      public static Evaluator 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.
      Parameters:
      modelFactory - The model factory of the system.
      stateFactory - The state factory of the system.
      loader - The library evaluator loader for evaluating the guards of system functions.
      symbolicUtil - The symbolic utility for manipulations of symbolic expressions.
      symbolicAnalyzer - The symbolic analyzer used in the system.
      errLogger - The error logger for reporting execution errors.
      Returns:
      The new CIVL evaluator.

    • newSymbolicAnalyzer

      public static SymbolicAnalyzer newSymbolicAnalyzer(CIVLConfiguration civlConfig, CIVLErrorLogger errorLogger, dev.civl.sarl.IF.SymbolicUniverse universe, ModelFactory modelFactory, SymbolicUtility symbolicUtil)
      Creates a new instance of symbolic analyzer.
      Parameters:
      universe - The symbolic universe to be used.
      modelFactory - The model factory to be used.
      symbolicUtil - The symbolic utility to be used.
      Returns:
      The new symbolic analyzer.

    • newTransition

      public static Transition newTransition(int pid, dev.civl.sarl.IF.expr.BooleanExpression clause, Statement statement)
      Creates a new regular Transition whose statement will be executed by executor.
      Parameters:
      pid - The PID of the process associated with this transition.
      clause - The boolean value clause that will be conjuncted to the path condition of the source state to form a new state immediately before the execution.
      statement - The statement associated with this transition, it will be executed by the executor.
      Returns:
      A new instance of regular CommonTransition

    • newTransition

      public static Transition newTransition(int pid, dev.civl.sarl.IF.expr.BooleanExpression clause, Statement statement, boolean simplifyState)
      Creates a new regular Transition whose statement will be executed by executor.
      Parameters:
      pid - The PID of the process associated with this transition.
      clause - The boolean value clause that will be conjuncted to the path condition of the source state to form a new state immediately before the execution.
      statement - The statement associated with this transition, it will be executed by the executor.
      simplifyState - A flag, set to true if and only if the target state of this transition must be simplified.
      atomicLockAction - An instance of
      invalid reference 
      AtomicLockAction
      Returns:
      A new instance of regular CommonTransition

    • newNoopTransition

      public static dev.civl.mc.semantics.common.NoopTransition newNoopTransition(int pid, dev.civl.sarl.IF.expr.BooleanExpression assumption, Statement statement, boolean symplifyState)
      Create a new NoopTransition whose statement will not be executed.
      Parameters:
      pid - The process id of the process executing this transition.
      statement - The statement associated with this transition, it will NOT be executed by the executor.
      clause - The boolean value clause that will be conjuncted to the path condition of the source state to form a new state immediately before the execution.
      simplifyState - A flag, set to true if and only if the target state of this transition must be simplified.
      Returns:
      A new instance of NoopTransition

    • newMemoryUnitEvaluator

      public static MemoryUnitExpressionEvaluator newMemoryUnitEvaluator(Evaluator evaluator, MemoryUnitFactory memUnitFactory)