Package org.svvrl.goal.core.tran

Class QPTL2NBWByLTL2NBW

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

All Implemented Interfaces:

java.util.EventListener, Algorithm, AlgorithmListener, ControllableAlgorithm, EditableAlgorithm, Translator<QPTL,FSA>

Direct Known Subclasses:

CCJ09Translators.QPTL2NBW, CouvreurTranslators.QPTL2NBW, CouvreurTranslators.QPTL2NTGBW, ExtendedCouvreurTranslators.QPTL2NBW, ExtendedCouvreurTranslators.QPTL2NTGBW, ExtendedGPVWPlusTranslators.QPTL2LOSNBW, ExtendedGPVWPlusTranslators.QPTL2NBW, ExtendedGPVWTranslators.QPTL2LOSNBW, ExtendedGPVWTranslators.QPTL2NBW, ExtendedLTL2AUTPlusTranslators.QPTL2LOSNBW, ExtendedLTL2AUTPlusTranslators.QPTL2NBW, ExtendedLTL2AUTTranslators.QPTL2LOSNBW, ExtendedLTL2AUTTranslators.QPTL2NBW, ExtendedLTL2BuchiTranslators.QPTL2NBW, ExtendedLTL2BuchiTranslators.QPTL2NTGBW, ExtendedModellaTranslators.QPTL2LOSNBW, ExtendedModellaTranslators.QPTL2NBW, IncTableauPlusTranslators.QPTL2LOSNBW, IncTableauPlusTranslators.QPTL2NBW, IncTableauTranslators.QPTL2LOSNBW, IncTableauTranslators.QPTL2NBW, LTL2BATranslators.QPTL2NBW, LTL2BuchiTranslators.QPTL2NBW, LTL2BuchiTranslators.QPTL2NTGBW, ModellaTranslators.QPTL2LOSNBW, ModellaTranslators.QPTL2NBW, PLTL2BATranslators.QPTL2NBW, TableauTranslators.QPTL2LOSNBW, TableauTranslators.QPTL2NBW, TemporalTesterTranslators.QPTL2LOSNBW, TemporalTesterTranslators.QPTL2NBW

public class QPTL2NBWByLTL2NBW
extends AbstractTranslator<QPTL,FSA>

This is a translator from a QPTL formula that can be converted to prenex normal form to an NBW 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, eliminates the quantification by projection and complementation, and finally simplifies the projected NBW if the simplification option is on. If the divide-and-conquer option in the preference is on, this translator will translate sub-formulae connected by boolean operators and then compose the results by automata operations.

Author:

Ming-Hsien Tsai

Constructor Summary

Constructors

Constructor	Description
QPTL2NBWByLTL2NBW(Translator<LTL,FSA> t)	Constructs this translator to translate a QPTL formula to an equivalent NBW with the help of a translator from LTL to NBW.

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.tran.AbstractTranslator

translate

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

Methods inherited from interface org.svvrl.goal.core.tran.Translator

getName

Constructor Details

QPTL2NBWByLTL2NBW

public QPTL2NBWByLTL2NBW(Translator<LTL,FSA> t)

Constructs this translator to translate a QPTL formula to an equivalent NBW with the help of a translator from LTL to NBW.

Parameters:

t - a translator from a LTL formula to an equivalent NBW

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 f) throws UnsupportedException

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