Class RewriteGraph

java.lang.Object
es.ucm.maude.bindings.RewriteGraph
public class RewriteGraph extends Object
Complete rewriting graph from an initial state.

  • Constructor Details

    • RewriteGraph

      public RewriteGraph(Term term)
      Construct a state transition graph.

      Parameters:
      term - Initial state term (it will be reduced).

  • Method Details

    • delete

      public void delete()

    • getStateTerm

      public Term getStateTerm(int stateNr)
      Get the term of the given state.

      Parameters:
      stateNr - A state number.

    • getRule

      public Rule getRule(int origin, int dest)
      Get a rule that connects two states.

      Parameters:
      origin - Origin state number.
      dest - Destination state number.

      Returns:
      A rule that connects the two states or null if none.

    • getNrRewrites

      public int getNrRewrites()
      Get the number of rewrites used to generate this graph,
      including the evaluation of atomic propositions.

    • modelCheck

      public ModelCheckResult modelCheck(Term formula)
      Model check a given LTL formula.

      Parameters:
      formula - Term of the Formula sort.

      Returns:
      The result of model checking.

    • getNrStates

      public int getNrStates()
      Get the number of states in the graph.

    • getNextState

      public int getNextState(int stateNr, int index)
      List the successors of a state in the graph.

      Parameters:
      stateNr - A state number.
      index - A child index (from zero).

      Returns:
      The state number of a successor or -1.

    • getStateParent

      public int getStateParent(int stateNr)
      Get the (one) parent of a given state.

      Parameters:
      stateNr - A state number.

      Returns:
      The state number of the parent or -1.