Module dev.civl.gmc
Package dev.civl.gmc.dpor

Class DporStackEntry<STATE,TRANSITION>

java.lang.Object
dev.civl.gmc.dpor.DporStackEntry<STATE,TRANSITION>
public class DporStackEntry<STATE,TRANSITION> extends Object
An element of the DporSearchStack. Wraps a DporNode with transient data used in the DPOR search.

  • Method Details

    • currentTransition

      public TRANSITION currentTransition()
      Returns:
      the transition which is either being explored (if this an "interior" entry) or is about to be explored (if this is the top entry of the stack)

    • getTid

      public int getTid()
      Returns:
      the transition id used for replaying traces

    • getNode

      public DporNode<STATE,TRANSITION> getNode()
      Returns:
      The DporNode held by this entry

    • getState

      public STATE getState()
      Returns:
      The state held by this entry's node

    • getPid

      public int getPid()
      Precondition: !isDone()
      Returns:
      the id of the process currently being explored.

    • getStackPosition

      public int getStackPosition()
      Returns:
      the index this entry has on the stack

    • isDone

      public boolean isDone()
      Returns:
      whether every enabled transition from every process in this entry's backtrack set has been explored

    • inBacktrack

      public boolean inBacktrack(int pid)
      Returns:
      whether pid is in this entry's backtrack set

    • addToBacktrack

      public void addToBacktrack(int pid)
      Add process pid into this entry's backtrack set

      Preconditions:

      • pid is not in already backtrack set
      • pid is enabled at this entry's state

    • addAllToBacktrack

      public int addAllToBacktrack(Collection<Integer> procs)
      Adds all of the processes in procs which are not already in the backtrack set Precondition: All processes in procs are enabled at this entry's state
      Returns:
      the number of new processes added to the backtrack

    • nextTransition

      public boolean nextTransition(StateManager<STATE,TRANSITION> manager)
      Increments to the next outgoing transition to be explored from the current state, moving to the next process in the backtrack set if necessary.
      Parameters:
      manager - Used to obtain the transitions of a process
      Returns:
      true iff a next transition exists

    • getPrevStackPosition

      public int getPrevStackPosition()
      Precondition: This entry is not the top of the stack.
      Returns:
      The stack position of the last entry with a transition from the same process as this entry's transition.

    • getHbSet

      public DporHbSet getHbSet()
      Precondition: This entry is not on the top of the stack.
      Returns:
      The DporHbSet representing the set of stack entries with transitions that happen before this entry's transition