Module dev.civl.gmc
Package dev.civl.gmc.seq

Class DfsSearcher<STATE,TRANSITION>

java.lang.Object
dev.civl.gmc.seq.DfsSearcher<STATE,TRANSITION>
public class DfsSearcher<STATE,TRANSITION> extends Object

A DfsSearcher performs a depth-first search of the state space of a transition system, stopping immediately if it finds a state satisfying the given predicate. A DfsSearcher is instantiated with a given enabler (an object which tells what transitions to explore from a given state), a state manager, a predicate, and a state from which to start the search.

Note that the STATE that this searcher use MUST override Object.hashCode() and #equals(Object) methods and STATEs that are canonically the same should return have the same hash code and they should be equal. Also the transition that is used by this searcher also needs to implement Object.equals(Object).

  • Constructor Details

    • DfsSearcher

      public DfsSearcher(EnablerIF<STATE,TRANSITION> enabler, StateManager<STATE,TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig, PrintStream debugOut)
      Constructs a new depth first search searcher.
      Parameters:
      enabler - the enabler used to determine the set of enabled transitions at each state in the course of this search
      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

    • DfsSearcher

      public DfsSearcher(EnablerIF<STATE,TRANSITION> enabler, StateManager<STATE,TRANSITION> manager, StatePredicateIF<STATE> predicate, GMCConfiguration gmcConfig)

  • Method Details

    • predicate

      public StatePredicateIF<STATE> predicate()

    • setName

      public void setName(String name)

    • name

      public String name()

    • isDepthBounded

      public boolean isDepthBounded()

    • unboundDepth

      public void unboundDepth()

    • boundDepth

      public void boundDepth(int value)

    • restrictDepth

      public void restrictDepth()
      Sets the depth bound to one less than the current stack size. Also sets the "stackIsBounded" bit to true.

    • setMinimize

      public void setMinimize(boolean value)

    • getMinimize

      public boolean getMinimize()

    • reportCycleAsViolation

      public boolean reportCycleAsViolation()

    • setPreemptionBound

      public void setPreemptionBound(int value)

    • setFairCycleCheck

      public void setFairCycleCheck(boolean value)
      Set the fairCycleCheck bit. If reporting cycles as violations, only report a cycle as a violation if it is a fair cycle. The cycle is not fair iff there is a process that is enabled at every state in the cycle but never executes in the cycle.

    • fairCycleCheck

      public boolean fairCycleCheck()
      Gets the fairCycleCheck bit. If reporting cycles as violations, only report a cycle as a violation if it is a fair cycle. The cycle is not fair iff there is a process that is enabled at every state in the cycle but never executes in the cycle.

    • setReportCycleAsViolation

      public void setReportCycleAsViolation(boolean value)
      If you want to check for cycles in the state space, and report the existence of a cycle as a violation, this flag should be set to true. Else set it to false. By default, it is false.

    • cycleFound

      public boolean cycleFound()
      If reportCycleAsViolation is true, and the search terminates with a "true" value, then this method can be called to determine whether the predicate holds (indicating a standard property violation) or a cycle has been found.

    • currentState

      public STATE currentState()
      Returns the state at the top of the stack, without modifying the stack.

    • stack

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

    • search

      public boolean search(STATE initialState) throws StateSpaceCycleException
      Performs a depth-first search starting from the given state. Essentially, this pushes the given state onto the stack, making it the current state, and then invokes search().
      Returns:
      true if a state is found that satisfies the predicate, in which case method currentState() can be used to get the state. If false is returned, the search has completed without finding a state satisfying the predicate.
      Throws:
      StateSpaceCycleException

    • search

      public boolean search() throws StateSpaceCycleException

      Resumes a depth-first search of the state space starting from the current state. The set of seen states and the stack may be non-empty, as this method is typically used to resume a search that has been "paused". It can also be used to start a search, as long as the current state has been set.

      Returns true iff predicate holds at some state reachable from the current state, including the current state. If this is the case, this will return true when the first state satisfying predicate is found in search. Once true is returned you may print the stack or look at the current state before resuming the search again. If false is returned, the search has completed without finding a state satisfying the predicate.

      If reportCycleAsViolation is true, this will also terminate and return true if a cycle in the state space has been found. The final state in the trace will also be the one which occurs earlier in the trace, forming a cycle.

      Returns:
      true if state is found which satisfies predicate. false if search completes without finding such a state.
      Throws:
      StateSpaceCycleException

    • proceedToNewState

      public boolean proceedToNewState() throws StateSpaceCycleException

      Proceeds with the search until we arrive at a state that has not been seen before (assuming there is one). In this case it marks the new state as seen, pushes it on the stack, and marks it as on the stack, and then returns true. If it finishes searching without finding a new state, it returns false.

      The search proceeds in the depth-first manner. The last transition sequence is obtained from the stack; these are the enabled transitions departing from the current state. The first transition in this sequence is applied to the current state. If the resulting state has not been seen before, we are done. Otherwise, the next transition is tried, and so on. If all these transitions are exhausted we proceed as follows: if the stack is empty, the search has completed and false is returned. Otherwise, the stack is popped, and the list of remaining transitions to be explored for the new current state is used, and we proceed as before. If this is again exhausted, we pop and repeat.

      Returns:
      true if there is a new state; false if the search is over so there is no new state
      Throws:
      StateSpaceCycleException

    • checkStackTrace

      public boolean checkStackTrace(StackEntry<STATE,TRANSITION> stackEntry)
      Returns:
      false iff there exist a state on the trace that has already been fully expanded.

    • 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

    • numTransitions

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

    • 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