Package owl.translations.nbadet

Class NbaAdjMat<S>

java.lang.Object

owl.translations.nbadet.NbaAdjMat<S>

public final class NbaAdjMat<S>
extends Object

Constructor Summary

Constructors

Constructor	Description
NbaAdjMat(Automaton<S,? extends BuchiAcceptance> automaton, com.google.common.collect.ImmutableBiMap<S,Integer> sMap, Set<S> aSinks, owl.translations.nbadet.SubsumedStatesMap extIncl)

Method Summary

Modifier and Type	Method	Description
Automaton<S,? extends BuchiAcceptance>	original()
Pair<BitSet,BitSet>	powerSucc(BitSet state, BitSet valuation)	Optimized successor function for a fixed valuation.
com.google.common.collect.ImmutableBiMap<S,Integer>	stateMap()
BitSet	states()
Pair<BitSet,BitSet>	succ(int st, int sym)
String	toString()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

NbaAdjMat

public NbaAdjMat(Automaton<S,? extends BuchiAcceptance> automaton,
                 com.google.common.collect.ImmutableBiMap<S,Integer> sMap,
                 Set<S> aSinks,
                 owl.translations.nbadet.SubsumedStatesMap extIncl)

Method Detail

original

public Automaton<S,? extends BuchiAcceptance> original()

stateMap

public com.google.common.collect.ImmutableBiMap<S,Integer> stateMap()

states

public BitSet states()

succ

public Pair<BitSet,BitSet> succ(int st,
                                      int sym)

powerSucc

public Pair<BitSet,BitSet> powerSucc(BitSet state,
                                           BitSet valuation)

Optimized successor function for a fixed valuation. It uses the provided accepting sinks and language inclusions to modify/shrink the result.

Parameters:

state - current set of states

valuation - active transition

Returns:

all successors + successors reached by at least one accepting edge

toString

public String toString()

Overrides:

toString in class Object