Module dev.civl.mc
Package dev.civl.mc.kripke.IF

Interface Enabler

All Superinterfaces:
dev.civl.gmc.seq.EnablerIF<State,Transition>
public interface Enabler extends dev.civl.gmc.seq.EnablerIF<State,Transition>
Enabler extends EnablerIF for CIVL models.

  • Method Summary

    Modifier and Type
    Method
    Description
    dev.civl.sarl.IF.expr.BooleanExpression
    getGuard(Statement statement, int pid, State state)
    Computes the guard of a statement.

    Methods inherited from interface dev.civl.gmc.seq.EnablerIF

    ampleSet, debugging, fullSet, getDebugOut, inAtomic, setDebugging, setDebugOut

  • Method Details

    • getGuard

      dev.civl.sarl.IF.expr.BooleanExpression getGuard(Statement statement, int pid, State state)
      Computes the guard of a statement. Since we have SystemGuardExpression and WaitGuardExpression, we don't need to compute the guard for system function calls and wait statements explicitly, which are now handled by the evaluator.
      Parameters:
      statement - The statement whose guard is to computed.
      pid - The ID of the process that the statement belongs to.
      state - The current state that the computation happens.
      Returns:
      The value of the guard of the given statement.