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

Class SMCEnabler

java.lang.Object
dev.civl.gmc.smc.SMCEnabler
All Implemented Interfaces:
EnablerIF<Integer,String>
public class SMCEnabler extends Object implements EnablerIF<Integer,String>
The implementation of EnablerIF used by SMC.

  • Constructor Details

  • Method Details

    • ampleSet

      public Collection<String> ampleSet(Integer source)

      Return the candidate ampleSet of transitions departing from a given state by satisfying the following three conditions:

      • C0: ampleSet is not empty if the full enabled set is not empty.
      • C1: Along every path in the full state graph that starts at source state, the following condition holds: a transition that is dependent on a transition in ample(s) can not be executed without a transition in ample(s) occurring first
      • C2: If source state is not fully expanded, then every transition in ample(s) is invisible.

      For detail information about how to compute the ample set of a state, please refer to the book "Model Checking" by Edmund M. Clarke Jr.


      Note that, all transitions in a same Collection should share a same source state. (Because the SMC uses the fly-weight)

      Specified by:
      ampleSet in interface EnablerIF<Integer,String>
      Parameters:
      source - The target state.
      Returns:
      The candidate ampleSet of transitions of the target state.

    • fullSet

      public Collection<String> fullSet(Integer state)
      Description copied from interface: EnablerIF
      Computes the set of transitions which are enabled at state.
      Specified by:
      fullSet in interface EnablerIF<Integer,String>
      Parameters:
      state - The source state.
      Returns:
      the collection of transitions that are enabled at state.

    • setDebugging

      public void setDebugging(boolean value)
      Description copied from interface: EnablerIF
      Set the debugging flag to the given value. When true, debugging output will be printed to the debugging output stream.
      Specified by:
      setDebugging in interface EnablerIF<Integer,String>
      Parameters:
      value - true if you want to print debugging info, false otherwise

    • debugging

      public boolean debugging()
      Description copied from interface: EnablerIF
      Returns the current value of the debugging flag. When true, debugging output will be be printed to the debugging output stream.
      Specified by:
      debugging in interface EnablerIF<Integer,String>
      Returns:
      current value of debugging flag.

    • setDebugOut

      public void setDebugOut(PrintStream out)
      Description copied from interface: EnablerIF
      Set the debugging output stream to the given stream.
      Specified by:
      setDebugOut in interface EnablerIF<Integer,String>
      Parameters:
      out - the stream to which you want the debugging output to be sent

    • getDebugOut

      public PrintStream getDebugOut()
      Description copied from interface: EnablerIF
      Returns the debugging output stream. This is the stream to which debuging output will be printed when the debugging flag is on.
      Specified by:
      getDebugOut in interface EnablerIF<Integer,String>
      Returns:
      the debugging output stream

    • inAtomic

      public boolean inAtomic(Integer state)
      Description copied from interface: EnablerIF
      Is the given state in the middle of an atomic action? Such intermediate states should be ignored by some algorithms.
      Specified by:
      inAtomic in interface EnablerIF<Integer,String>
      Parameters:
      state - a state
      Returns:
      true iff the state is in the midst of an atomic action