Package org.svvrl.goal.core.tran.qptl2ba

Class QPTL2BAFuture

java.lang.Object
org.svvrl.goal.core.AbstractAlgorithm
org.svvrl.goal.core.AbstractControllableAlgorithm
org.svvrl.goal.core.AbstractEditableAlgorithm
org.svvrl.goal.core.tran.AbstractTranslator<QPTL,​FSA>
org.svvrl.goal.core.tran.qptl2ba.QPTL2BAFuture
All Implemented Interfaces:
java.util.EventListener, Algorithm, AlgorithmListener, ControllableAlgorithm, EditableAlgorithm, Translator<QPTL,​FSA>
public class QPTL2BAFuture
extends AbstractTranslator<QPTL,​FSA>
This class provides a translation from a QPTL formula without past operators to an equivalent NBW. The formula to be translated is not required to be convertible to an equivalent formula in prenex normal form. This translation requires an underlying LTL translation algorithm and an NBW complementation construction. While the underlying LTL translation algorithm can be specified in the constructor, the complementation construction will always be the default complementation construction set in the preference.
Author:
Ming-Hsien Tsai

  • Constructor Details

    • QPTL2BAFuture

      public QPTL2BAFuture()
      Constructs this translation algorithm with default options.

    • QPTL2BAFuture

      public QPTL2BAFuture​(Properties options)
      Constructs this translation algorithm with custom options.
      Parameters:
      options - custom options

    • QPTL2BAFuture

      public QPTL2BAFuture​(Properties options, Translator<LTL,​FSA> tran)
      Constructs this translation with custom options and an underlying LTL translation algorithm.
      Parameters:
      options - custom options
      tran - an LTL translation algorithm

  • Method Details

    • getIntermediateResult

      public Editable getIntermediateResult()
      Description copied from interface: Translator
      Returns the intermediate result of this translator. This method can be used for displaying the intermediate result during the step-by-step translation.
      Returns:
      the intermediate result of this translator

    • translate

      public FSA translate​(QPTL formula) throws UnsupportedException
      Description copied from interface: Translator
      Translates a logic formula to an automaton.
      Parameters:
      formula - a logic formula to be translate
      Returns:
      the automaton translated from formula
      Throws:
      UnsupportedException - if formula is not supported by this translator

    • newInstance

      public Translator<QPTL,​FSA> newInstance()
      Description copied from interface: Translator
      Creates a new translator instance same as this one.
      Returns:
      a new translator instance same as this one