Class StrategyRewriteGraph

java.lang.Object
es.ucm.maude.bindings.StrategyRewriteGraph
public class StrategyRewriteGraph extends Object
Complete rewriting graph under the control of a strategy from an initial state.

  • Constructor Details

    • StrategyRewriteGraph

      public StrategyRewriteGraph(Term initial, StrategyExpression strat, StringVector opaques, boolean biased)
      Construct a strategy transition graph.

      Parameters:
      initial - Initial state term (it will be reduced).
      strat - A strategy expression.
      opaques - A list of strategy names to be considered opaque.
      biased - Whether the matchrews should be biased.

    • StrategyRewriteGraph

      public StrategyRewriteGraph(Term initial, StrategyExpression strat, StringVector opaques)
      Construct a strategy transition graph.

      Parameters:
      initial - Initial state term (it will be reduced).
      strat - A strategy expression.
      opaques - A list of strategy names to be considered opaque.

    • StrategyRewriteGraph

      public StrategyRewriteGraph(Term initial, StrategyExpression strat)
      Construct a strategy transition graph.

      Parameters:
      initial - Initial state term (it will be reduced).
      strat - A strategy expression.

  • Method Details

    • delete

      public void delete()

    • getStateTerm

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

      Parameters:
      stateNr - A state number.

    • getStateStrategy

      public StrategyExpression getStateStrategy(int stateNr)
      Get the strategy that will be executed next
      from the given state.

      Parameters:
      stateNr - A state number.

      Returns:
      That strategy expression or null if there is
      no pending strategy in the current call or subsearch frame.

    • getTransition

      public StrategyGraphTransition getTransition(int origin, int dest)
      Get the transition that connects two states (if any).

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

      Returns:
      That transition if exists or a null pointer.

    • 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.

    • getNrRealStates

      public int getNrRealStates()
      Get the number of real (not merged) states in the graph (in linear time).

    • 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.

    • isSolutionState

      public boolean isSolutionState(int stateNr)
      Whether the state is a solution for the strategy.

      Parameters:
      stateNr - A state number.