Package org.svvrl.goal.core.tran
Class QPTL2NGBWByLTL2NGBW
java.lang.Object
- All Implemented Interfaces:
java.util.EventListener
,Algorithm
,AlgorithmListener
,ControllableAlgorithm
,EditableAlgorithm
,Translator<QPTL,FSA>
- Direct Known Subclasses:
ExtendedGPVWPlusTranslators.QPTL2LOSNGBW
,ExtendedGPVWPlusTranslators.QPTL2NGBW
,ExtendedGPVWTranslators.QPTL2LOSNGBW
,ExtendedGPVWTranslators.QPTL2NGBW
,ExtendedLTL2AUTPlusTranslators.QPTL2LOSNGBW
,ExtendedLTL2AUTPlusTranslators.QPTL2NGBW
,ExtendedLTL2AUTTranslators.QPTL2LOSNGBW
,ExtendedLTL2AUTTranslators.QPTL2NGBW
,ExtendedModellaTranslators.QPTL2LOSNGBW
,ExtendedModellaTranslators.QPTL2NGBW
,IncTableauPlusTranslators.QPTL2LOSNGBW
,IncTableauPlusTranslators.QPTL2NGBW
,IncTableauTranslators.QPTL2LOSNGBW
,IncTableauTranslators.QPTL2NGBW
,ModellaTranslators.QPTL2LOSNGBW
,ModellaTranslators.QPTL2NGBW
,TableauTranslators.QPTL2LOSNGBW
,TableauTranslators.QPTL2NGBW
,TemporalTesterTranslators.QPTL2LOSNGBW
,TemporalTesterTranslators.QPTL2NGBW
public class QPTL2NGBWByLTL2NGBW extends AbstractTranslator<QPTL,FSA>
This is a translator from a QPTL formula that can be converted to prenex
normal form and has no universal quantification to an NGBW by utilizing a LTL
translator. This translator first converts the QPTL formula to prenex normal
form, then translate the un-quantified sub-formula by the LTL translator, and
eliminates the quantification by projection, and finally simplifies the
projected NBW if the simplification option is on.
- Author:
- Ming-Hsien Tsai
-
Constructor Summary
Constructors Constructor Description QPTL2NGBWByLTL2NGBW(Translator<LTL,FSA> t)
Constructs this translator to translate a QPTL formula to an equivalent NGBW with the help of a translator from LTL to NGBW. -
Method Summary
Modifier and Type Method Description Editable
getIntermediateResult()
Returns the intermediate result of this translator.Translator<QPTL,FSA>
newInstance()
Creates a new translator instance same as this one.FSA
translate(QPTL f)
Translates a logic formula to an automaton.Methods inherited from class org.svvrl.goal.core.AbstractControllableAlgorithm
addControllableListener, addSubAlgorithm, doPause, doStage, doStart, doStep, fireReferenceChangedEvent, getInterval, getStages, getStatus, pause, pause, removeControllableListener, removeSubAlgorithm, setInterval, setStages, setStatus, setSynchronizationObject, stagePause, stagePause
Methods inherited from class org.svvrl.goal.core.AbstractAlgorithm
addAlgorithmListener, addProgress, appendStageMessage, appendStepMessage, getAlgorithmListeners, getCurrentProgress, getMaximalProgress, getMinimalProgress, getName, getOptions, getSubAlgorithms, isDeterministicProgress, removeAlgorithmListener, setCurrentProgress, setDeterministicProgress, setMaximalProgress, setMinimalProgress
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
Methods inherited from interface org.svvrl.goal.core.Algorithm
addAlgorithmListener, getAlgorithmListeners, getOptions, removeAlgorithmListener
Methods inherited from interface org.svvrl.goal.core.AlgorithmListener
appendStageMessage, appendStepMessage, getCurrentProgress, getMaximalProgress, getMinimalProgress, setCurrentProgress, setDeterministicProgress, setMaximalProgress, setMinimalProgress
Methods inherited from interface org.svvrl.goal.core.ControllableAlgorithm
addControllableListener, doPause, doStage, doStart, doStep, getInterval, getStages, getStatus, removeControllableListener, setInterval, setStages, setStatus, setSynchronizationObject
-
Constructor Details
-
QPTL2NGBWByLTL2NGBW
Constructs this translator to translate a QPTL formula to an equivalent NGBW with the help of a translator from LTL to NGBW.- Parameters:
t
- a translator from a LTL formula to an equivalent NGBW
-
-
Method Details
-
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
Description copied from interface:Translator
Translates a logic formula to an automaton.- Parameters:
f
- a logic formula to be translate- Returns:
- the automaton translated from
formula
- Throws:
UnsupportedException
- ifformula
is not supported by this translator
-
newInstance
Description copied from interface:Translator
Creates a new translator instance same as this one.- Returns:
- a new translator instance same as this one
-