| CompactSafraTree |
This class implements the compact Safra tree in [Piterman.
|
| Node |
A Node is a tree node in a compact Safra tree.
|
| PitermanConstruction |
A PitermanComplement object complements an NBW A in
stages:
Determinizes the input NBW as a DPW P by the
Safra-Piterman construction.
Complements P as another DPW P' by increasing the
parity of every state by 1.
Converts P' to an NBW A'. |
| PitermanContainment |
Test if an NBW A is contained in another NBW B by constructing the
intersection of A and the complement of B incrementally.
|
| PitermanContainmentOptions |
This class contains several options for the containment with Safra-Piterman
construction.
|
| PitermanContainmentState |
PitermanContainmentState is used in the on-the-fly containment
testing with the Safra-Piterman construction.
|
| PitermanConverter |
This class provides an implementation of the determinization algorithm of
Safra-Piterman construction [Piterman.
|
| PitermanConverter.NBW2DPWConverter |
This class is the real implementation of the determinization algorithm of
Safra-Piterman construction.
|
| PitermanState |
A PitermanState is a state in the DPW created by Safra-Piterman
construction.
|
| PitermanStateInfoDrawer |
This is a drawer that can display the information of a state with a compact
Safra tree.
|