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

Class DporSearchStack<STATE,TRANSITION>

java.lang.Object
dev.civl.gmc.dpor.DporSearchStack<STATE,TRANSITION>
public class DporSearchStack<STATE,TRANSITION> extends Object
This class represents the search stack used in the DPOR algorithm. It maintains a stack of entries each of which represents a state in the state space. If an entry in the stack is not the top entry, then it also represents the transition from its own state to the next state on the stack. Such entries are referred to as "interior" entries.

  • Method Details

    • numStatesSeen

      public int numStatesSeen()
      Returns:
      the number of unique states explored

    • numStatesMatched

      public int numStatesMatched()
      Returns:
      the number of times a state was re-explored

    • numTraceSteps

      public int numTraceSteps()
      Returns:
      the number of unique trace steps executed

    • numTraceStepsMatched

      public int numTraceStepsMatched()
      Returns:
      the number of times a trace step was re-explored using the cache to avoid a repeat execution

    • isEmpty

      public boolean isEmpty()
      Returns:
      whether the stack is empty

    • size

      public int size()
      Returns:
      the number of entries on the stack

    • top

      public DporStackEntry<STATE,TRANSITION> top()
      Returns:
      the most recent entry on the stack. It is the only entry that has no transition.

    • get

      public DporStackEntry<STATE,TRANSITION> get(int index)
      Parameters:
      index -
      Returns:
      the entry on the stack with the specified index

    • currentState

      public STATE currentState()
      Returns:
      the state held by the top entry of our stack.

    • currentTransition

      public TRANSITION currentTransition()
      Returns:
      the next transition to be executed. null if the top entry is done exploring transitions.

    • searchForTransition

      public boolean searchForTransition()
      Traverses to the next available transition to explore, popping from the stack as necessary.

      Precondition: currentTransition() == null

      Returns:
      whether a next transition was found. Will be false iff the stack is empty after searching

    • pushTransition

      public boolean pushTransition()
      Explores the current transition and pushes resulting state as a DporStackEntry onto the stack

      Precondition:

      Returns:
      whether the new stack entry contains a node that has been seen before

    • popTransition

      public void popTransition()
      Pops the top entry from the stack.

      This action also implicitly pops the last transition of the execution if one existed: the new top entry will no longer be "interior" and will thus no longer represent a transition.

      Precondition: The stack is not empty.

    • getHbSet

      public DporHbSet getHbSet(int pid)
      Parameters:
      pid - A process id
      Returns:
      the DporHbSet for the next transitions of the process pid

    • addRace

      public void addRace(DporStackEntry<STATE,TRANSITION> entry, int pid)
      Marks a race between the transition of entry and one of the next transitions at the current state from the process pid.
      Parameters:
      entry - An interior entry
      pid - a process id

    • makeStackTraversal

      public DporSearchStack<STATE,TRANSITION>.StackTraversal makeStackTraversal(int proc)
      Constructs a new DporSearchStack<STATE,TRANSITION>.StackTraversal object for traversing the interior entries of this stack in reverse order, skipping entries whose transition happens before some next transition of proc at the stack's current state.

      Adding races to this stack while traversing with this returned object is allowed and such additions are reflected in the traversal

      Parameters:
      proc -
      Returns:
      a new DporSearchStack<STATE,TRANSITION>.StackTraversal object