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

Interface TraceStep

All Superinterfaces:
dev.civl.gmc.TraceStepIF<State>
public interface TraceStep extends dev.civl.gmc.TraceStepIF<State>
TraceStep extends TraceStepIF for CIVL models. A CIVL trace step is composed of a sequence of atomic steps executed by a single process.
See Also:

  • Method Details

    • addAtomicStep

      void addAtomicStep(AtomicStep step)
      Adds an atomic step to the trace step.
      Parameters:
      step - The atomic step to be added.

    • getNumAtomicSteps

      int getNumAtomicSteps()
      Returns the number of atomic steps contained in this trace step.
      Returns:
      the number of atomic steps contained in this trace step.

    • processIdentifier

      int processIdentifier()
      Returns the identifier of the process that this trace step belongs to.
      Returns:
      the identifier of the process that this trace step belongs to.

    • getAtomicSteps

      Iterable<AtomicStep> getAtomicSteps()
      Returns the list of atomic steps of this trace step.
      Returns:
      the list of atomic steps of this trace step.

    • setFinalState

      void setFinalState(State finalState)

      Set final state to the trace step.

      Parameters:
      finalState - The state to be used as the final state of the trace step.

    • getFinalState

      State getFinalState()
      Specified by:
      getFinalState in interface dev.civl.gmc.TraceStepIF<State>