Package org.svvrl.goal.core.tran

Interface Translator<T extends Logic,​A extends Automaton>

Type Parameters:
T - the type of the logic
A - the type of the automaton
All Superinterfaces:
Algorithm, AlgorithmListener, java.util.EventListener
All Known Implementing Classes:
AbstractTranslator, CCJ09, CCJ09Translators.LTL2NBW, CCJ09Translators.QPTL2NBW, Couvreur, CouvreurTranslators.LTL2NBW, CouvreurTranslators.LTL2NTGBW, CouvreurTranslators.QPTL2NBW, CouvreurTranslators.QPTL2NTGBW, ExtendedCouvreur, ExtendedCouvreurTranslators.LTL2NBW, ExtendedCouvreurTranslators.LTL2NTGBW, ExtendedCouvreurTranslators.QPTL2NBW, ExtendedCouvreurTranslators.QPTL2NTGBW, ExtendedGPVWPlusTranslators.LTL2LOSNBW, ExtendedGPVWPlusTranslators.LTL2LOSNGBW, ExtendedGPVWPlusTranslators.LTL2NBW, ExtendedGPVWPlusTranslators.LTL2NGBW, ExtendedGPVWPlusTranslators.QPTL2LOSNBW, ExtendedGPVWPlusTranslators.QPTL2LOSNGBW, ExtendedGPVWPlusTranslators.QPTL2NBW, ExtendedGPVWPlusTranslators.QPTL2NGBW, ExtendedGPVWTranslators.LTL2LOSNBW, ExtendedGPVWTranslators.LTL2LOSNGBW, ExtendedGPVWTranslators.LTL2NBW, ExtendedGPVWTranslators.LTL2NGBW, ExtendedGPVWTranslators.QPTL2LOSNBW, ExtendedGPVWTranslators.QPTL2LOSNGBW, ExtendedGPVWTranslators.QPTL2NBW, ExtendedGPVWTranslators.QPTL2NGBW, ExtendedLTL2AUTPlusTranslators.LTL2LOSNBW, ExtendedLTL2AUTPlusTranslators.LTL2LOSNGBW, ExtendedLTL2AUTPlusTranslators.LTL2NBW, ExtendedLTL2AUTPlusTranslators.LTL2NGBW, ExtendedLTL2AUTPlusTranslators.QPTL2LOSNBW, ExtendedLTL2AUTPlusTranslators.QPTL2LOSNGBW, ExtendedLTL2AUTPlusTranslators.QPTL2NBW, ExtendedLTL2AUTPlusTranslators.QPTL2NGBW, ExtendedLTL2AUTTranslators.LTL2LOSNBW, ExtendedLTL2AUTTranslators.LTL2LOSNGBW, ExtendedLTL2AUTTranslators.LTL2NBW, ExtendedLTL2AUTTranslators.LTL2NGBW, ExtendedLTL2AUTTranslators.QPTL2LOSNBW, ExtendedLTL2AUTTranslators.QPTL2LOSNGBW, ExtendedLTL2AUTTranslators.QPTL2NBW, ExtendedLTL2AUTTranslators.QPTL2NGBW, ExtendedLTL2Buchi, ExtendedLTL2BuchiTranslators.LTL2NBW, ExtendedLTL2BuchiTranslators.LTL2NTGBW, ExtendedLTL2BuchiTranslators.QPTL2NBW, ExtendedLTL2BuchiTranslators.QPTL2NTGBW, ExtendedModella, ExtendedModellaTranslators.LTL2LOSNBW, ExtendedModellaTranslators.LTL2LOSNGBW, ExtendedModellaTranslators.LTL2NBW, ExtendedModellaTranslators.LTL2NGBW, ExtendedModellaTranslators.QPTL2LOSNBW, ExtendedModellaTranslators.QPTL2LOSNGBW, ExtendedModellaTranslators.QPTL2NBW, ExtendedModellaTranslators.QPTL2NGBW, ExtendedOnTheFlyNGBWBuilder, IncTableauPlusTranslators.LTL2LOSNBW, IncTableauPlusTranslators.LTL2LOSNGBW, IncTableauPlusTranslators.LTL2NBW, IncTableauPlusTranslators.LTL2NGBW, IncTableauPlusTranslators.QPTL2LOSNBW, IncTableauPlusTranslators.QPTL2LOSNGBW, IncTableauPlusTranslators.QPTL2NBW, IncTableauPlusTranslators.QPTL2NGBW, IncTableauTranslators.LTL2LOSNBW, IncTableauTranslators.LTL2LOSNGBW, IncTableauTranslators.LTL2NBW, IncTableauTranslators.LTL2NGBW, IncTableauTranslators.QPTL2LOSNBW, IncTableauTranslators.QPTL2LOSNGBW, IncTableauTranslators.QPTL2NBW, IncTableauTranslators.QPTL2NGBW, KP02, KP02Translators.QPTL2NBW, LTL2BA, LTL2BATranslators.LTL2NBW, LTL2BATranslators.LTL2NTGBW, LTL2BATranslators.LTL2VWAA, LTL2BATranslators.QPTL2NBW, LTL2BATranslators.QPTL2NTGBW, LTL2BATranslators.QPTL2VWAA, LTL2Buchi, LTL2BuchiTranslators.LTL2NBW, LTL2BuchiTranslators.LTL2NTGBW, LTL2BuchiTranslators.QPTL2NBW, LTL2BuchiTranslators.QPTL2NTGBW, LTL2LOSNGBWAdapter, LTL2TWVWAA, LTL2VWAA, Modella, ModellaTranslators.LTL2LOSNBW, ModellaTranslators.LTL2LOSNGBW, ModellaTranslators.LTL2NBW, ModellaTranslators.LTL2NGBW, ModellaTranslators.QPTL2LOSNBW, ModellaTranslators.QPTL2LOSNGBW, ModellaTranslators.QPTL2NBW, ModellaTranslators.QPTL2NGBW, ORETranslator, PLTL2BA, PLTL2BATranslators.LTL2NBW, PLTL2BATranslators.LTL2NTGBW, PLTL2BATranslators.LTL2TWVWAA, PLTL2BATranslators.QPTL2NBW, PLTL2BATranslators.QPTL2NTGBW, PLTL2BATranslators.QPTL2TWVWAA, PMT02, PMT02Translators.ACTL2LOSNBW, PMT02Translators.ACTL2LOSNGBW, PMT02Translators.ACTL2NBW, PMT02Translators.ACTL2NGBW, QPTL2ABWFuture, QPTL2BA, QPTL2BACanonical, QPTL2BAFuture, QPTL2BATranslators.CanonicalQPTL2TWACW, QPTL2BATranslators.FutureQPTL2ABW, QPTL2BATranslators.QPTL2NBW, QPTL2NBWByLTL2NBW, QPTL2NGBWByLTL2NGBW, QPTL2TWACWCanonical, RETranslator, Tableau, TableauTranslators.LTL2LOSNBW, TableauTranslators.LTL2LOSNGBW, TableauTranslators.LTL2NBW, TableauTranslators.LTL2NGBW, TableauTranslators.QPTL2LOSNBW, TableauTranslators.QPTL2LOSNGBW, TableauTranslators.QPTL2NBW, TableauTranslators.QPTL2NGBW, TemporalTesterTranslators.LTL2LOSNBW, TemporalTesterTranslators.LTL2LOSNGBW, TemporalTesterTranslators.LTL2NBW, TemporalTesterTranslators.LTL2NGBW, TemporalTesterTranslators.QPTL2LOSNBW, TemporalTesterTranslators.QPTL2LOSNGBW, TemporalTesterTranslators.QPTL2NBW, TemporalTesterTranslators.QPTL2NGBW, TranslateByDivideAndConquer, TranslateToNBWByNGBW, TranslateToNGBWByLOSNGBW
public interface Translator<T extends Logic,​A extends Automaton>
extends Algorithm
This is an interface for translators from a logic formula to an automaton. An instance of a translator object is expected to be used only once.
Author:
Ming-Hsien Tsai

  • Method Details

    • getName

      java.lang.String getName()
      Returns the name of this translator.
      Returns:
      the name of this translator.

    • getIntermediateResult

      Editable getIntermediateResult()
      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

      A translate​(T formula) throws UnsupportedException
      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

      Translator<T,​A> newInstance()
      Creates a new translator instance same as this one.
      Returns:
      a new translator instance same as this one