java.lang.Object

org.svvrl.goal.core.tran.qptl2ba.QPTL2TWACWCanonical

All Implemented Interfaces:: java.util.EventListener, Algorithm, AlgorithmListener, ControllableAlgorithm, EditableAlgorithm, Translator<QPTL,TwoWayAltAutomaton>

public class QPTL2TWACWCanonical
extends AbstractTranslator<QPTL,TwoWayAltAutomaton>

This class provides a translation from a QPTL formula in canonical forms to an equivalent two-way alternating co-Büchi automaton. Past sub-formulae are required to be convertible to prenex normal form.

Author:: Ming-Hsien Tsai

Constructor Summary

Constructors
Constructor	Description
`QPTL2TWACWCanonical()`	Constructs this translation algorithm with default options.
`QPTL2TWACWCanonical(Properties options)`	Constructs this translation algorithm with custom options.

Method Summary

Modifier and Type	Method	Description
`static TwoWayAltAutomaton`	`applyConjunction(TwoWayAltAutomaton aut1, TwoWayAltAutomaton aut2)`	Returns a conjunction of two TWACW.
`static TwoWayAltAutomaton`	`applyDisjunction(TwoWayAltAutomaton aut1, TwoWayAltAutomaton aut2)`	Returns a disjunction of two TWACW.
`static void`	`applyNext(TwoWayAltAutomaton aut)`	Applies a next temporal operator to a TWACW.
`Editable`	`getIntermediateResult()`	Returns the intermediate result of this translator.
`static boolean`	`isApplicable(QPTL formula)`	Returns `true` if a specified QPTL formula is supported by this translator.
`Translator<QPTL,TwoWayAltAutomaton>`	`newInstance()`	Creates a new translator instance same as this one.
`TwoWayAltAutomaton`	`translate(QPTL formula)`	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
- QPTL2TWACWCanonical
  
  public QPTL2TWACWCanonical()
  
  Constructs this translation algorithm with default options.
- QPTL2TWACWCanonical
  
  public QPTL2TWACWCanonical(Properties options)
  
  Constructs this translation algorithm with custom options.
  
  Parameters:
  
  options - custom options
Method Details
- isApplicable
  
  public static boolean isApplicable(QPTL formula)
  
  Returns true if a specified QPTL formula is supported by this translator.
  
  Parameters:
  
  formula - a QPTL formula
  
  Returns:
  
  true if the specified QPTL formula is supported by this translator
- 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
- applyNext
  
  public static void applyNext(TwoWayAltAutomaton aut)
  
  Applies a next temporal operator to a TWACW.
  
  Parameters:
  
  aut - a TWACW
- applyConjunction
  
  public static TwoWayAltAutomaton applyConjunction(TwoWayAltAutomaton aut1, TwoWayAltAutomaton aut2)
  
  Returns a conjunction of two TWACW.
  
  Parameters:
  
  aut1 - an TWACW
  
  aut2 - an TWACW
  
  Returns:
  
  a conjunction of the two TWACW
- applyDisjunction
  
  public static TwoWayAltAutomaton applyDisjunction(TwoWayAltAutomaton aut1, TwoWayAltAutomaton aut2)
  
  Returns a disjunction of two TWACW.
  
  Parameters:
  
  aut1 - an TWACW
  
  aut2 - an TWACW
  
  Returns:
  
  a disjunction of the two TWACW
- translate
  
  public TwoWayAltAutomaton 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,TwoWayAltAutomaton> newInstance()
  
  Description copied from interface: Translator
  
  Creates a new translator instance same as this one.
  
  Returns:
  
  a new translator instance same as this one

Class QPTL2TWACWCanonical