Package owl.translations.nbadet

Class NbaDetState<S>

  • public abstract class NbaDetState<S>
extends Object
    This is the state type of the deterministic parity automaton produced by nbadet. It provides an implementation of the modular determinization construction as described in: https://doi.org/10.1007/978-3-030-31784-3_18 If you for some reason need to convert the bit-encoded states back to the actual NBA states, you can use the states field which gives you the mapping.

    • Constructor Detail

      • NbaDetState

        public NbaDetState()

    • Method Detail

      • powerSet

        public abstract BitSet powerSet()
        all states present in this macro-state (states with same powerSet are lang-equiv.).

      • rSccs

        public abstract BitSet rSccs()
        stores states in rej. SCCs (if sepRej enabled).

      • aSccsBuffer

        public abstract BitSet aSccsBuffer()
        stores inactive states for acc. SCC state breakpoint construction (if sepAcc enabled).

      • aSccs

        public abstract Optional<Pair<BitSet,​Integer>> aSccs()
        stores active states + rank for acc. SCC state breakpoint construction (if sepAcc enabled).

      • dSccs

        public abstract ArrayList<RankedSlice> dSccs()
        deterministic mixed SCC(s) that are handled separately (if sepDet enabled).

      • mSccs

        public abstract ArrayList<RankedSlice> mSccs()
        (remaining, unhandled) mixed SCC(s) - simple ranked slices / Safra tree(s).

      • of

        public static <S> NbaDetState<S> of​(NbaDetConf<S> conf,
                                    Set<S> initialSet)
        Given a set and a configuration, create a DetState to be used as an initial state. The states are distributed in the set into the right components according to the config.

      • toTrieEncoding

        public List<BitSet> toTrieEncoding()
        Combined trieMap encoding (the det. components are ignored here and are fully determined by configuration)

      • finerOrEqual

        public boolean finerOrEqual​(NbaDetState<S> o)
        Check finerOrEqual component-wise, assuming same configuration.

      • toString

        public final String toString()
        Prints the sets of the determinization components, where each bitset is expanded into the states of the underlying NBA, i.e., usually integers numbering the states of the input NBA (more complicated objects would work, but make this rather unreadable).
        Overrides:
        toString in class Object

      • rankToPriority

        public static int rankToPriority​(int rank,
                                 boolean isGood)
        Transform a good/bad event for a rank into a min-even priority.

      • priorityToRank

        public static Pair<Integer,​Boolean> priorityToRank​(int prio)
        Inverse of rankToPriority.

      • rankUpperBound

        public static <S> int rankUpperBound​(NbaDetConf<S> c)
        There are at most as many non-empty ranked sets as states.

      • weakestBadPrio

        public static <S> int weakestBadPrio​(NbaDetConf<S> c)
        Some weakly bad event that can not be caused by any real set with rank.

      • getAcceptance

        public static <S> ParityAcceptance getAcceptance​(NbaDetConf<S> c)
        Naive unoptimized parity acceptance (just uses upper bound of possible priorities).