Package owl.translations.nbadet
Contains the translation from non-deterministic Büchi automata to deterministic parity automata
described in "LP19b" (
Bibliography.ICALP_19_1)
with optimisations from "LP19a"
(Bibliography.ATVA_19).-
Interface Summary Interface Description NbaSimAlgorithm<S,T> Interface that all pluggable language inclusion / simulation algorithms should implement. -
Class Summary Class Description NbaAdjMat<S> NbaDet This class provides the entry-point for the translation from non-deterministic Büchi automata to deterministic parity automata described inBibliography.ICALP_19_1with optimisations fromBibliography.ATVA_19.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.NbaDetConfSets these 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.NbaLangInclusions This class glues available algorithms that can underapprox.RankedSlice type/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.SimType Register new simulation algorithms here.