| ModifiedSafraConstruction |
This class can complement an NBW by the modified Safra's construction.
|
| ModifiedSafraContainment |
Test if an NBW A is contained in another NBW B by constructing the
intersection of A and the complement of B incrementally.
|
| ModifiedSafraContainmentOptions |
This class contains several options for the containment with the modified
Safra's construction.
|
| Node |
A Node is a tree node in a Safra tree.
|
| SafraConstruction |
A SafraComplement object complements an NBW A in stages:
Determinizes the input NBW A as a DRW R by the
Safra's construction.
Complements R as a DSW S by interpreting the
acceptance condition of R as a Streett condition.
Converts S to an NBW A'. |
| SafraContainment |
Test if an NBW A is contained in another NBW B by constructing the
intersection of A and the complement of B incrementally.
|
| SafraContainmentOptions |
This class contains several options for the containment with the Safra's
construction.
|
| SafraContainmentState |
SafraContainmentState is used in the on-the-fly containment testing
with the Safra's construction.
|
| SafraConverter |
This class provides an implementation of the Safra's determinization
algorithm [S.
|
| SafraConverter.NBW2DRWConverter |
This is the real implementation of the Safra's determinization.
|
| SafraState |
A SafraState is a state in the DRW created by Safra's construction.
|
| SafraStateInfoDrawer |
This is a drawer that can display the information of a state with a Safra
tree.
|
| SafraTree |
This class provides an implementation of the Safra tree [S.
|