Package org.mpi_sws.jmc.strategies.trust

Class ExplorationStack.Item

java.lang.Object
org.mpi_sws.jmc.strategies.trust.ExplorationStack.Item
Enclosing class:
ExplorationStack
public static class ExplorationStack.Item extends Object
Represents an item in the exploration stack.

  • Method Details

    • addAdditionalEvent

      public void addAdditionalEvent(Event event)

    • getAdditionalEventsToProcess

      public List<Event> getAdditionalEventsToProcess()

    • forwardRW

      public static ExplorationStack.Item forwardRW(ExecutionGraphNode read, ExecutionGraphNode write, ExecutionGraph graph)
      Creates a forward revisit item for a read revisiting an alternative write.
      Parameters:
      read - The read event
      write - The write event
      graph - The graph to be used in the case of a backward revisit
      Returns:
      The created item

    • forwardWW

      public static ExplorationStack.Item forwardWW(ExecutionGraphNode one, ExecutionGraphNode two, ExecutionGraph graph)
      Creates a forward revisit item for a write revisiting an alternative concurrent write.
      Parameters:
      one - The first write event
      two - The second write event
      graph - The graph to be used in the case of a backward revisit
      Returns:
      The created item

    • forwardLW

      public static ExplorationStack.Item forwardLW(ExecutionGraphNode one, ExecutionGraph graph)

    • backwardRevisit

      public static ExplorationStack.Item backwardRevisit(ExecutionGraphNode one, ExecutionGraph graph)
      Creates a backward revisit item for a write revisiting a read.
      Parameters:
      one - The write event
      graph - The graph to be used in the case of a backward revisit
      Returns:
      The created item

    • lockBackwardRevisit

      public static ExplorationStack.Item lockBackwardRevisit(ExecutionGraphNode one, ExecutionGraphNode two, ExecutionGraph graph)
      Creates a backward revisit item for a lock read revisiting another lock read.
      Parameters:
      one - The read event
      two - The revisited read
      graph - The graph to be used in the case of a backward revisit
      Returns:
      The created item

    • setInnerStackIndex

      public void setInnerStackIndex(int index)
      Sets the inner stack index of the item.
      Parameters:
      index - The inner stack index

    • getInnerStackIndex

      public int getInnerStackIndex()
      Gets the inner stack index of the item.
      Returns:
      The inner stack index

    • getType

      public ExplorationStack.ItemType getType()
      Gets the type of the item.
      Returns:
      The type of the item

    • getEvent1

      public ExecutionGraphNode getEvent1()
      Gets the first event of the item.
      Returns:
      The first event of the item

    • getEvent2

      public ExecutionGraphNode getEvent2()
      Gets the second event of the item.
      Returns:
      The second event of the item

    • getGraph

      public ExecutionGraph getGraph()
      Gets the graph associated with the item.
      Returns:
      The graph associated with the item

    • isBackwardRevisit

      public boolean isBackwardRevisit()
      Checks if the item is a forward revisit.
      Returns:
      True if the item is a forward revisit, false otherwise

    • toString

      public String toString()
      Overrides:
      toString in class Object