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

Class StateManager<STATE,TRANSITION>

java.lang.Object
dev.civl.gmc.seq.StateManager<STATE,TRANSITION>
Type Parameters:
STATE - the type used to represent states in the state-transition system being analyzed
TRANSITION - the type used to represent transitions in the state-transition system being analyzed
Direct Known Subclasses:
ConcurrentStateManagerIF, SimpleStateManager
public abstract class StateManager<STATE,TRANSITION> extends Object
A StateManagerIF provides part of a generic interface to a state-transition system. The primary method is nextState(STATE, TRANSITION), which, given a state and a transition, returns the "next state", i.e., the state which results from executing the transition from the given state. Other methods are provided that are needed specifically for depth-first search, including methods to mark a state as "seen before", and to make a state as "currently on (or off) the stack". Still other methods are provided for printing information about states.

  • Constructor Details

    • StateManager

      public StateManager()

  • Method Details

    • nextState

      public abstract TraceStepIF<STATE> nextState(STATE state, TRANSITION transition)
      Given a state and a transition, returns the trace step after executing the transition at the given state. See TraceStepIF.
      Parameters:
      state - a state in the state transition system
      transition - a transition which is enabled at the given state
      Returns:
      the trace step after executing the transition at the given state.

    • tryNextState

      public abstract TraceStepIF<STATE> tryNextState(STATE state, TRANSITION transition)
      Same as nextState(STATE,TRANSITION) except if an error is encountered then it is not reported and null is returned
      Parameters:
      state - a state in the state transition system
      transition - an transition which is enabled at the given state
      Returns:
      the trace step after executing the transition at the given state.

    • getPid

      public abstract int getPid(TRANSITION transition)
      Gets the ID number of the process that is responsible for executing transition. This is used for the preemption-bounding search. If not doing preemption-bounded search, this method is not used. The preemption-bounded search determines if the given transition is a preemption if the PID is different from the PID of the previous transition but there is a transition in the enabled (or ample) set with the PID of the previous transition.
      Parameters:
      transition - a non-null transition
      Returns:
      a PID of the given transition

    • getEnabledProcesses

      public abstract Set<Integer> getEnabledProcesses(STATE state)

    • getLiveProcesses

      public abstract Set<Integer> getLiveProcesses(STATE state)

    • getTransitions

      public abstract Collection<TRANSITION> getTransitions(STATE state, int pid)

    • normalize

      public abstract void normalize(TraceStepIF<STATE> traceStep)

      Normalize/simplify a state. It takes a TraceStepIF as input since normalize always happens after nextState(Object, Object) which will return a TraceStepIF and normalize may need information from TraceStepIF.

      Note that each distinct state (not equal with each other) will only normalized once. Since when a unnormalized state is seen again, you can get its normalized state through its associated SequentialNode.

      Parameters:
      state - The state that is being normalized/simplified.

    • printTraceStep

      public abstract void printTraceStep(STATE sourceState, TraceStepIF<STATE> traceStep)
      This method should print the source state id and transitions within this traceStep. Note that this method should not print the final state in the traceStep.
      Parameters:
      traceStep - The traceStep you want to print

    • printTraceStepFinalState

      public abstract void printTraceStepFinalState(STATE finalState, int normalizedID)

      This method should print the final state of a trace step. So a complete print of a trace step consists of a call to printTraceStep(Object, TraceStepIF) and a call to this method.

      When this method is called, the final state of the traceStep is already normalized if (-saveStates option is enabled).

      Parameters:
      finalState - The final state of a trace step
      normalizedID - The ID of a normalized state (-1, if -saveStates option is diabled). see also getId(Object)

    • printStateShort

      public abstract void printStateShort(PrintStream out, STATE state)
      Prints out a short human-readable representation of the state. This is intended to be something like "State 13", or something similar.
      Parameters:
      out - the stream to which to send the output
      state - any state in the state transition system

    • printStateLong

      public abstract void printStateLong(PrintStream out, STATE state)
      Prints out a long human-readable representation of the state. This is intended to show all the details of the state, e.g., the values of all variables, etc.
      Parameters:
      out - the stream to which to send the output
      state - any state in the state transition system

    • printTransitionShort

      public abstract void printTransitionShort(PrintStream out, TRANSITION transition)
      Prints out a short human-readable representation of the transition.
      Parameters:
      out - the stream to which to send the output
      transition - any transition in the state transition system

    • printTransitionLong

      public abstract void printTransitionLong(PrintStream out, TRANSITION transition)
      Prints out a long human-readable representation of the transition. This is intended to show all details of the transition.
      Parameters:
      out - the stream to which to send the output
      transition - any transition in the state transition system

    • printAllStatesShort

      public abstract void printAllStatesShort(PrintStream out)
      Prints out all the states, in short form, currently "held" by this manager. It is up to each implementation to decide what states are "held".
      Parameters:
      out - the stream to which to send the output

    • printAllStatesLong

      public abstract void printAllStatesLong(PrintStream out)
      Prints out all the states, in long form, currently "held" by this manager. It is up to each implementation to decide what states are "held".
      Parameters:
      out - the stream to which to send the output

    • debug

      public abstract void debug(STATE state, List<Integer> backtrack)

    • getId

      public int getId(STATE normalizedState)
      Get the id of a normalizedState.
      Parameters:
      normalizedState - The State of which you want the id.
      Returns:
      the id of the normalizedState.

    • setGetIdFunction

      public void setGetIdFunction(GetIdFunction<STATE> getIdFunc)