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

Class DporDfsSearcher<STATE,TRANSITION>

java.lang.Object
dev.civl.gmc.dpor.DporDfsSearcher<STATE,TRANSITION>
public class DporDfsSearcher<STATE,TRANSITION> extends Object

  • Constructor Details

    • DporDfsSearcher

      public DporDfsSearcher(DependencyAnalyzer<STATE,TRANSITION> analyzer, StateManager<STATE,TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig, PrintStream debugOut)
      Constructs a new depth first search searcher.
      Parameters:
      manager - the object used to manage states, compute the next state from a current state and transition, and so, during this search
      predicate - the state predicate -- this will be checked at each state encountered in the search, and if it is found to hold, the search method will return; hence it is usually a predicate about something "bad" happening, like a deadlock
      gmcConfig - GMC configuration object
      debugOut - if null, debugging output is not printed, otherwise debugging output will be printing to this stream
      enabler - the enabler used to determine the set of enabled transitions at each state in the course of this search

    • DporDfsSearcher

      public DporDfsSearcher(DependencyAnalyzer<STATE,TRANSITION> analyzer, StateManager<STATE,TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig)

  • Method Details

    • predicate

      public StatePredicateIF<STATE> predicate()

    • stack

      public DporSearchStack<STATE,TRANSITION> stack()
      Returns the stack used to perform the depth first search

    • explore

      public boolean explore(STATE initialState) throws StateSpaceCycleException
      Explore the state space starting at initialState using DPOR.
      Parameters:
      initialState -
      Returns:
      Throws:
      StateSpaceCycleException

    • setDebugging

      public void setDebugging(boolean value)
      Set the debugging flag to the given value. If true, debugging output will be printed to the debug stream. Otherwise debugging output will not be printed.
      Parameters:
      value - if true, start showing the debugging output, otherwise don't show it

    • setDebugOut

      public void setDebugOut(PrintStream out)
      Sets the debugging output stream to the given stream. This is the stream used to print debugging information if the debugging flag is on.
      Parameters:
      out - the output stream to which debugging information should be sent

    • getDebugOut

      public PrintStream getDebugOut()
      Returns the stream used to print debugging output when the debugging flag is on.
      Returns:
      the debugging output stream

    • printStack

      public void printStack(PrintStream out, boolean longFormat, boolean summarize)
      Prints the current stack in a human-readable format.
      Parameters:
      out - the stream to which to print the stack
      longFormat - if true, provide detailed information about each state
      summarize - if true, don't print out more than some fixed bound number of entries from the top of the stack; otherwise print the whole stack

    • printStack

      public void printStack(PrintStream out)
      Prints the whole stack in a human readable form to the given stream. Prints first a summary, then the stack in full detail (with detailed state information).
      Parameters:
      out - output stream to which this information should be sent

    • numStatesSeen

      public int numStatesSeen()
      The number of states seen in this search.
      Returns:
      the number of states seen so far

    • numTraceSteps

      public int numTraceSteps()
      The number of transitions executed in the course of this search so far.
      Returns:
      the number of transitions executed.

    • numTraceStepsMatched

      public int numTraceStepsMatched()

    • numStatesMatched

      public int numStatesMatched()
      The number of states matched so far. A state is "matched" when the search determines the state has been seen before, earlier in the search. If the state has been seen before, it is not explored.
      Returns:
      the number of states matched

    • numOfSearchNodeSaved

      public int numOfSearchNodeSaved()
      Returns:
      the number of search nodes saved which is also the number of non-equal states.

    • printSummary

      public void printSummary(PrintStream out)
      Summarizes the current state of the search in a human-readable form printed to the given stream.
      Parameters:
      out - the stream to which to print the information

    • writeStack

      public void writeStack(PrintStream stream)
      Write the state of the current stack in a condensed form that can be used to replay the trace later.
      Parameters:
      stream - stream to which to write the current state of the DFS stack