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

Interface EnablerIF<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
All Known Implementing Classes:
SMCEnabler
public interface EnablerIF<STATE,TRANSITION>

An EnablerIF tells you which transitions should be explored from a given state. It might need to know things about the state of the search (such as what states are currently on the DFS stack). Such information can be provided at creation.

A transition is an edge in the state space which means that two transitions emanating from different states are different even if they originated from the same statement.

  • Method Summary

    Modifier and Type
    Method
    Description
    Collection<TRANSITION>
    ampleSet(STATE source)
    Return the candidate ampleSet of transitions departing from a given state by satisfying the following three conditions:
    boolean
    debugging()
    Returns the current value of the debugging flag.
    Collection<TRANSITION>
    fullSet(STATE state)
    Computes the set of transitions which are enabled at state.
    PrintStream
    getDebugOut()
    Returns the debugging output stream.
    boolean
    inAtomic(STATE state)
    Is the given state in the middle of an atomic action? Such intermediate states should be ignored by some algorithms.
    void
    setDebugging(boolean value)
    Set the debugging flag to the given value.
    void
    setDebugOut(PrintStream out)
    Set the debugging output stream to the given stream.

  • Method Details

    • ampleSet

      Collection<TRANSITION> ampleSet(STATE 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.

      Parameters:
      source - The target state.
      Returns:
      The candidate ampleSet of transitions of the target state.

    • fullSet

      Collection<TRANSITION> fullSet(STATE state)
      Computes the set of transitions which are enabled at state.
      Parameters:
      state - The source state.
      Returns:
      the collection of transitions that are enabled at state.

    • inAtomic

      boolean inAtomic(STATE state)
      Is the given state in the middle of an atomic action? Such intermediate states should be ignored by some algorithms.
      Parameters:
      state - a state
      Returns:
      true iff the state is in the midst of an atomic action

    • setDebugging

      void setDebugging(boolean value)
      Set the debugging flag to the given value. When true, debugging output will be printed to the debugging output stream.
      Parameters:
      value - true if you want to print debugging info, false otherwise

    • debugging

      boolean debugging()
      Returns the current value of the debugging flag. When true, debugging output will be be printed to the debugging output stream.
      Returns:
      current value of debugging flag.

    • setDebugOut

      void setDebugOut(PrintStream out)
      Set the debugging output stream to the given stream.
      Parameters:
      out - the stream to which you want the debugging output to be sent

    • getDebugOut

      PrintStream getDebugOut()
      Returns the debugging output stream. This is the stream to which debuging output will be printed when the debugging flag is on.
      Returns:
      the debugging output stream