Contains the translation from non-deterministic Büchi automata to deterministic parity automata described in "LP19b" (
Bibliography.ICALP_19_1) with optimisations from "LP19a" (
Interface Summary Interface Description NbaSimAlgorithm<S,T>Interface that all pluggable language inclusion / simulation algorithms should implement.
Class Summary Class Description NbaAdjMat<S> NbaDetThis class provides the entry-point for the translation from non-deterministic Büchi automata to deterministic parity automata described in
Bibliography.ICALP_19_1with optimisations from
NbaDetConf<S>This is the structure containing all required information that is used in the determinization process and is obtained based on an NbaDetArgs instance. NbaDetConfSetsthese sets reflect the different determinisation components to be used in the DetState i.e. NbaDetState<S>This is the state type of the deterministic parity automaton produced by nbadet. NbaLangInclusionsThis class glues available algorithms that can underapprox. RankedSlicetype/wrapper of ranked slices, which are just tuples of disjoint sets, with entries that are additionally to the index order also ranked by some extra total order (i.e. SmartSucc<S>This class acts like a "smart cache" for the states produced during NBA determinization.
Enum Summary Enum Description NbaDetConf.UpdateMode NbaLangInclusions.SimTypeRegister new simulation algorithms here.