Class SmartSucc<S>

  • public class SmartSucc<S>
    extends Object
    This class acts like a "smart cache" for the states produced during NBA determinization. When called for a (state,sym) pair the first time, it checks whether "suitable" successors already exists and returns one of them if possible, instead of returning a new state. This uses perations to transform between ranked slices and a certain different encoding. If not useSmartSucc is enabled, this class just passes through successor calculation.
    • Constructor Detail

    • Method Detail

      • successor

        public Edge<NbaDetState<S>> successor​(NbaDetState<S> cur,
                                              BitSet sym)
        Wraps successor calculation. Performs smart successor choice, if enabled in config. If enabled, first checks for existing suitable successors. Returns existing if possible and otherwise computes new one using default policy.
      • unprune

        public static List<Pair<BitSet,​Integer>> unprune​(List<Pair<BitSet,​Integer>> pruned)
        Takes content of a ranked slice, returns a "unpruned" version, i.e., labels contain states of whole subtree unpruned nodes in rank order uniquely determine a rank slice and are useful for storing ranked slices in k-equiv-aware lookup table (trieMap)
      • toTrieEncoding

        public static List<BitSet> toTrieEncoding​(RankedSlice rs)
        Notice that this is only for a single slice. For the optimization the corresponding method for NbaDetState is used.
      • fromTrieEncoding

        public static RankedSlice fromTrieEncoding​(List<BitSet> word)
        Reverses the trieMap encoding. But this works correctly only for individually encoded RankedSlices.
      • finerOrEqual

        public static boolean finerOrEqual​(RankedSlice rs1,
                                           RankedSlice rs2)
        Returns true if second slice is a neighbor-merged version of the first, ignoring ranks.
      • kEquiv

        public static boolean kEquiv​(List<BitSet> th1,
                                     List<BitSet> th2,
                                     int k)
        Two trieMap-encoded slices are k-equiv. if have same k prefix in trieMap branch.
      • notWorse

        public static boolean notWorse​(List<BitSet> th1,
                                       List<BitSet> th2,
                                       int k)
        Returns whether k-cut not worse in t1 compared to t2. This means: if in trieMap nodes >= k never appear states of t2 that never appear >= k in t2 and all states in t1 appear in nodes >= k not later than in t2