Package org.svvrl.goal.core.tran.ltl2ba

  • Class Summary 
    Class Description
    LTL2BA
    This class provides an implementation of the LTL2BA translation algorithm [Paul Gastin and Denis Oddoux.
    LTL2BAOptions
    This class contains several options for the LTL2BA translation algorithm.
    LTL2BATranslators
    This class provides several translators based on the LTL2BA translation algorithm.
    LTL2BATranslators.LTL2NBW
    This class provides a translator from a LTL formula to an NBW.
    LTL2BATranslators.LTL2NTGBW
    This class provides a translator from a LTL formula into an NTGBW.
    LTL2BATranslators.LTL2VWAA
    This class provides a translator from a LTL formula into a co-Büchi VWAA.
    LTL2BATranslators.QPTL2NBW
    This class provides a translator from a QPTL formula to an NBW.
    LTL2BATranslators.QPTL2NTGBW
    This class provides a translator from a QPTL formula to an NTGBW.
    LTL2BATranslators.QPTL2VWAA
    This class provides a translator from a QPTL formula to a co-Büchi VWAA.
    LTL2VWAA
    This class provides an implementation of the translation from LTL formulae to co-Büchi very weak alternating automata in [Paul Gastin and Denis Oddoux.
    NTGBW2NBW
    This class provides an implementation of the conversion from an NTGBW to an equivalent NBW proposed in LTL2BA.
    NTGBWStateReducer
    This class implements the state simplification of NTGBW applied in LTL2BA.
    VWAA2NTGBW
    This class provides an implementation of the conversion in LTL2BA from co-Büchi VWAA to an equivalent NTGBW.