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

Interface Transition

public interface Transition
This represents a CIVL transition, which is deterministic and enabled at a certain state. It is composed of a path condition, an atomic statement, a PID, and a process identifier.

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Interface
    Description
    static enum 
    Transition.TransitionKind
     

  • Method Summary

    Modifier and Type
    Method
    Description
    dev.civl.sarl.IF.expr.BooleanExpression
    clause()
     
    int
    pid()
    The PID of the process that this transition belongs to.
    boolean
    simpifyState()
    Shall the state be simplified after the transition is done?
    Statement
    statement()
    The statement that this transition is to execute, which should be atomic, deterministic, and enabled in the context of the path condition.
    Transition.TransitionKind
    transitionKind()
    returns the kind of this transition.

  • Method Details

    • clause

      dev.civl.sarl.IF.expr.BooleanExpression clause()
      Returns:
      a boolean-value clause. Execution of this transition will start from a new state, which is obtained via conjunction of this clause and the path condition of the source state.

    • statement

      Statement statement()
      The statement that this transition is to execute, which should be atomic, deterministic, and enabled in the context of the path condition.
      Returns:
      The statement that this transition is to execute

    • pid

      int pid()
      The PID of the process that this transition belongs to.
      Returns:
      The PID of the process that this transition belongs to.

    • transitionKind

      Transition.TransitionKind transitionKind()
      returns the kind of this transition.
      Returns:

    • simpifyState

      boolean simpifyState()
      Shall the state be simplified after the transition is done?
      Returns: