Module dev.civl.gmc
Package dev.civl.gmc.smc

Class SimpleStateManager

java.lang.Object
dev.civl.gmc.seq.StateManager<Integer,String>
dev.civl.gmc.smc.SimpleStateManager
public class SimpleStateManager extends StateManager<Integer,String>
The implementation of the interface StateManager used by SMC.

  • Constructor Details

  • Method Details

    • nextState

      public TraceStepIF<Integer> nextState(Integer state, String transition)
      Description copied from class: StateManager
      Given a state and a transition, returns the trace step after executing the transition at the given state. See TraceStepIF.
      Specified by:
      nextState in class StateManager<Integer,String>
      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 TraceStepIF<Integer> tryNextState(Integer state, String transition)
      Description copied from class: StateManager
      Same as StateManager.nextState(STATE,TRANSITION) except if an error is encountered then it is not reported and null is returned
      Specified by:
      tryNextState in class StateManager<Integer,String>
      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.

    • getId

      public int getId(Integer normalizedState)
      Description copied from class: StateManager
      Get the id of a normalizedState.
      Overrides:
      getId in class StateManager<Integer,String>
      Parameters:
      normalizedState - The State of which you want the id.
      Returns:
      the id of the normalizedState.

    • normalize

      public void normalize(TraceStepIF<Integer> traceStep)
      Description copied from class: StateManager

      Normalize/simplify a state. It takes a TraceStepIF as input since normalize always happens after StateManager.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.

      Specified by:
      normalize in class StateManager<Integer,String>

    • printStateShort

      public void printStateShort(PrintStream out, Integer state)
      Description copied from class: StateManager
      Prints out a short human-readable representation of the state. This is intended to be something like "State 13", or something similar.
      Specified by:
      printStateShort in class StateManager<Integer,String>
      Parameters:
      out - the stream to which to send the output
      state - any state in the state transition system

    • printStateLong

      public void printStateLong(PrintStream out, Integer state)
      Description copied from class: StateManager
      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.
      Specified by:
      printStateLong in class StateManager<Integer,String>
      Parameters:
      out - the stream to which to send the output
      state - any state in the state transition system

    • printTransitionShort

      public void printTransitionShort(PrintStream out, String transition)
      Description copied from class: StateManager
      Prints out a short human-readable representation of the transition.
      Specified by:
      printTransitionShort in class StateManager<Integer,String>
      Parameters:
      out - the stream to which to send the output
      transition - any transition in the state transition system

    • printTransitionLong

      public void printTransitionLong(PrintStream out, String transition)
      Description copied from class: StateManager
      Prints out a long human-readable representation of the transition. This is intended to show all details of the transition.
      Specified by:
      printTransitionLong in class StateManager<Integer,String>
      Parameters:
      out - the stream to which to send the output
      transition - any transition in the state transition system

    • printAllStatesShort

      public void printAllStatesShort(PrintStream out)
      Description copied from class: StateManager
      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".
      Specified by:
      printAllStatesShort in class StateManager<Integer,String>
      Parameters:
      out - the stream to which to send the output

    • printAllStatesLong

      public void printAllStatesLong(PrintStream out)
      Description copied from class: StateManager
      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".
      Specified by:
      printAllStatesLong in class StateManager<Integer,String>
      Parameters:
      out - the stream to which to send the output

    • printTraceStep

      public void printTraceStep(Integer sourceState, TraceStepIF<Integer> traceStep)
      Description copied from class: StateManager
      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.
      Specified by:
      printTraceStep in class StateManager<Integer,String>
      Parameters:
      traceStep - The traceStep you want to print

    • printTraceStepFinalState

      public void printTraceStepFinalState(Integer finalState, int normalizedID)
      Description copied from class: StateManager

      This method should print the final state of a trace step. So a complete print of a trace step consists of a call to StateManager.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).

      Specified by:
      printTraceStepFinalState in class StateManager<Integer,String>
      Parameters:
      finalState - The final state of a trace step
      normalizedID - The ID of a normalized state (-1, if -saveStates option is diabled). see also StateManager.getId(Object)

    • getPid

      public int getPid(String transition)
      Description copied from class: StateManager
      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.
      Specified by:
      getPid in class StateManager<Integer,String>
      Parameters:
      transition - a non-null transition
      Returns:
      a PID of the given transition

    • debug

      public void debug(Integer state, List<Integer> backtrack)
      Specified by:
      debug in class StateManager<Integer,String>

    • getEnabledProcesses

      public Set<Integer> getEnabledProcesses(Integer state)
      Specified by:
      getEnabledProcesses in class StateManager<Integer,String>

    • getLiveProcesses

      public Set<Integer> getLiveProcesses(Integer state)
      Specified by:
      getLiveProcesses in class StateManager<Integer,String>

    • getTransitions

      public Collection<String> getTransitions(Integer state, int pid)
      Specified by:
      getTransitions in class StateManager<Integer,String>