Package owl.translations.nbadet
Class NbaDet
- java.lang.Object
-
- owl.translations.nbadet.NbaDet
-
public final class NbaDet extends Object
This class provides a conversion from non-deterministic Büchi automata into deterministic parity automata. It is based on the following two papers: https://doi.org/10.4230/LIPIcs.ICALP.2019.120 https://doi.org/10.1007/978-3-030-31784-3_18
-
-
Field Summary
Fields Modifier and Type Field Description static OwlModule<OwlModule.Transformer>
MODULE
-
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,BuchiAcceptance> aut, NbaDetArgs 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 void
main(String... args)
Entry point for nbadet tool.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, NbaDetArgs args)
Compute selected simulations.static void
restoreLogLevel(Map<Handler,Level> oldLogLevels)
-
-
-
Field Detail
-
MODULE
public static final OwlModule<OwlModule.Transformer> MODULE
-
-
Method Detail
-
main
public static void main(String... args) throws IOException
Entry point for nbadet tool.- Parameters:
args
- arguments from environment- Throws:
IOException
- on failure to parse the input file
-
preprocess
public static <S> Pair<Automaton<Set<S>,BuchiAcceptance>,Set<Pair<Set<S>,Set<S>>>> preprocess(Automaton<S,BuchiAcceptance> aut, NbaDetArgs 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,BuchiAcceptance> aut, NbaDetArgs 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
-
-