java.lang.Object
- owl.translations.nbadet.NbaDet

```
public final class NbaDet
extends Object
```
This class provides the entry-point for the translation from non-deterministic Büchi automata to deterministic parity automata described in Bibliography.ICALP_19_1 with optimisations from Bibliography.ATVA_19.

Method Summary

All Methods Static Methods Concrete Methods
Modifier and Type	Method	Description
`static <S> Automaton<BitSet,AllAcceptance>`	`createPowerSetAutomaton(NbaAdjMat<S> adjMat)`	Create a powerset automaton of NBA where state sets are represented by BitSets.
`static <S> Automaton<?,ParityAcceptance>`	`determinize(Automaton<S,? extends BuchiAcceptance> aut, AutomatonConversionCommands.Nba2DpaCommand args)`	Main method of module.
`static <S> Automaton<NbaDetState<S>,ParityAcceptance>`	`determinizeNba(NbaDetConf<S> conf)`
`static <S> Pair<Automaton<NbaDetState<S>,ParityAcceptance>,Map<BitSet,NbaDetState<S>>>`	`determinizeNbaAlongScc(Automaton<BitSet,?> refScc, NbaDetConf<S> conf)`	Determinize provided NBA partially, while not leaving some automaton refScc.
`static <S> Automaton<Pair<Integer,NbaDetState<S>>,ParityAcceptance>`	`determinizeNbaTopo(NbaDetConf<S> conf)`	Determinize automaton, utilizing "topological" optimization, i.e.
`static Map<Handler,Level>`	`overrideLogLevel(Level verbosity)`
`static <S> Pair<Automaton<Set<S>,BuchiAcceptance>,Set<Pair<Set<S>,Set<S>>>>`	`preprocess(Automaton<S,BuchiAcceptance> aut, AutomatonConversionCommands.Nba2DpaCommand args)`	Compute selected simulations.
`static void`	`restoreLogLevel(Map<Handler,Level> oldLogLevels)`

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

overrideLogLevel

public static Map<Handler,Level> overrideLogLevel(Level verbosity)

restoreLogLevel

public static void restoreLogLevel(Map<Handler,Level> oldLogLevels)

preprocess

public static <S> Pair<Automaton<Set<S>,BuchiAcceptance>,Set<Pair<Set<S>,Set<S>>>> preprocess(Automaton<S,BuchiAcceptance> aut,
                                                                                                                AutomatonConversionCommands.Nba2DpaCommand args)

Compute selected simulations. if possible, shrink automaton using computed equivalences. Returns (possibly quotiented) automaton and known language inclusions.

determinize

public static <S> Automaton<?,ParityAcceptance> determinize(Automaton<S,? extends BuchiAcceptance> aut,
                                                                  AutomatonConversionCommands.Nba2DpaCommand args)

Main method of module.

determinizeNba

public static <S> Automaton<NbaDetState<S>,ParityAcceptance> determinizeNba(NbaDetConf<S> conf)

determinizeNbaTopo
```
public static <S> Automaton<Pair<Integer,NbaDetState<S>>,ParityAcceptance> determinizeNbaTopo(NbaDetConf<S> conf)
```
Determinize automaton, utilizing "topological" optimization, i.e. determinize each SCC of the powerset structure of the NBA separately and prune the partial DPAs (keep one bottom SCC of the partial DPAs).

Parameters:

conf - prepared determinization config (which includes the input NBA)

Returns:

resulting DPA

determinizeNbaAlongScc

public static <S> Pair<Automaton<NbaDetState<S>,ParityAcceptance>,Map<BitSet,NbaDetState<S>>> determinizeNbaAlongScc(Automaton<BitSet,?> refScc,
                                                                                                                                       NbaDetConf<S> conf)

Determinize provided NBA partially, while not leaving some automaton refScc. Returns partial DPA and a mapping from all reference states to some representative DPA state. refScc should be some kind of powerset SCC (i.e. deterministic structure) of the NBA. The exploration starts from the unique initial state of that powerset SCC automaton.

createPowerSetAutomaton
```
public static <S> Automaton<BitSet,AllAcceptance> createPowerSetAutomaton(NbaAdjMat<S> adjMat)
```
Create a powerset automaton of NBA where state sets are represented by BitSets.

Type Parameters:

S - state type of underlying NBA

Parameters:

adjMat - BitSet-based transitions for underlying NBA

Returns:

the resulting powerset automaton

Class NbaDet