Package org.svvrl.goal.core.comp.schewe

  • Class Summary 
    Class Description
    HistoryTree
    This class implements the history tree with labels and LIR in [Sven Schewe: Tighter Bounds for the Determinisation of Büchi Automata.
    Node
    A Node is a tree node in a history tree.
    ScheweConstruction
    This class provides a complementation of an NBW through DRW and DSW based on [Sven Schewe: Tighter Bounds for the Determinisation of Büchi Automata.
    ScheweConverter
    This class provides two determinization constructions, one from NBW to DRW and the other from NBW to DPW, based on [Sven Schewe: Tighter Bounds for the Determinisation of Büchi Automata.
    ScheweConverter.NBW2DPWConverter
    This class is the real implementation of the determinization algorithm of Safra-Schewe construction.
    ScheweConverter.NBW2DRWConverter
    This class is the real implementation of the determinization algorithm of Safra-Schewe construction.
    ScheweState
    This class provides states in the DRW created by Schewe-Piterman construction.
    ScheweStateInfoDrawer
    This is a drawer that can display the information of a state with a history tree.