Class NbaSccInfo<S>


  • public abstract class NbaSccInfo<S>
    extends Object
    This class wraps SccDecomposition, assigns each SCC an integer ID (in topological order) and provides additional lookup tables to check various SCC properties and the SCC ID of states.
    • Constructor Detail

      • NbaSccInfo

        public NbaSccInfo()
    • Method Detail

      • sccDecomposition

        public abstract SccDecomposition<S> sccDecomposition()
        the state sets, numbered in some topological order (bottom SCCs last).
      • trvSccs

        public abstract Set<Integer> trvSccs()
        trivial SCCs.
      • botSccs

        public abstract Set<Integer> botSccs()
        bottom SCCs.
      • detSccs

        public abstract Set<Integer> detSccs()
        deterministic SCCs.
      • rejSccs

        public abstract Set<Integer> rejSccs()
        Weak rejecting SCCs (trivial or only rejecting cycles).
      • accSccs

        public abstract Set<Integer> accSccs()
        Weak accepting SCCs (non-trivial and only good cycles).
      • ids

        public IntStream ids()
        SCC IDs in some reverse topological order (bottom SCCs first, initial last).
      • isSccReachable

        public boolean isSccReachable​(int s,
                                      int t)
        reachability relation on SCCs. An SCC is reachable from itself iff it is not transient.
      • isStateReachable

        public boolean isStateReachable​(S p,
                                        S q)
        reachability relation on states.