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

Class Simulator<STATE,TRANSITION>

java.lang.Object
dev.civl.gmc.Simulator<STATE,TRANSITION>
Type Parameters:
STATE - the type for the states in the transition system
TRANSITION - the type for the transitions in the transition system
public class Simulator<STATE,TRANSITION> extends Object
A Simulator is used to execute a transition system using a TransitionChooser to determine which transition to execute from each state. E.g., this could be used to replay an execution trace of a transition system, for which the trace was stored in a file created by method
invalid reference 
DfsSearcher#writeStack(File)
. Or, it could be used to perform a random execution.

  • Constructor Details

    • Simulator

      public Simulator(StateManager<STATE,TRANSITION> manager, PrintStream out)
      Parameters:
      manager - state manager; used to compute the next state given a state and transition
      out - stream to which the trace should be written in human-readable form
      enabler - enabler used to determine the set of enabled transitions at a given state

  • Method Details

    • setPredicate

      public void setPredicate(StatePredicateIF<STATE> predicate)

    • getPredicate

      public StatePredicateIF<STATE> getPredicate()

    • setPrintAllStates

      public void setPrintAllStates(boolean value)

    • getPrintAllStates

      public boolean getPrintAllStates()

    • setLog

      public void setLog(ErrorLog log)

    • getLog

      public ErrorLog getLog()

    • isQuiet

      public boolean isQuiet()

    • setQuiet

      public void setQuiet(boolean quiet)

    • play

      public Trace<TRANSITION,STATE>[] play(STATE initialState, TransitionChooser<STATE,TRANSITION> chooser, boolean verbose) throws MisguidedExecutionException
      Throws:
      MisguidedExecutionException

    • play

      public Trace<TRANSITION,STATE>[] play(STATE[] states, boolean[] print, String[] names, TransitionChooser<STATE,TRANSITION> chooser, boolean verbose) throws MisguidedExecutionException
      Plays the trace. This method accepts an array of initial states, and will create executions in parallel, one for each initial state. All of the executions will use the same sequence of transitions, but may start from different initial states. The common use case has two initial states, the first one a symbolic state and the second a concrete state obtained by solving the path condition.
      Parameters:
      states - the states from which the execution should start. The first state in the initial state (index 0) will be the one assumed to execute according to the guide. This method will modify this array so that upon returning the array will hold the final states.
      print - which states should be printed at a point when states will be printed. Array of length states.length.
      names - the names to use for the different executions. Array of length states.length
      chooser - the object used to decide which transition to choose when more than one is enabled at a state
      verbose - print verbose output about what's going on?
      Returns:
      An array of traces after executing the trace with different initial states. See also Trace.
      Throws:
      MisguidedExecutionException

    • play

      public Trace<TRANSITION,STATE>[] play(STATE initialSymbolicState, STATE initialConcreteState, boolean printSymbolicStates, TransitionChooser<STATE,TRANSITION> chooser, boolean verbose) throws MisguidedExecutionException
      Throws:
      MisguidedExecutionException