java.lang.Object

org.svvrl.goal.core.aut.OmegaUtil

public class OmegaUtil
extends java.lang.Object

This class provides several utility methods for ω-automata.

Author:: Ming-Hsien Tsai

Nested Class Summary

Nested Classes
Modifier and Type	Class	Description
`static class`	`OmegaUtil.AcceptanceAction`	Actions applied in acceptance imitation.
`(package private) static class`	`OmegaUtil.CycleFinder`	A `CycleFinder` is able to find all elementary cycles of an automaton.

Constructor Summary

Constructors

Constructor Description

OmegaUtil()

Method Summary

Modifier and Type	Method	Description
`static void`	`checkInputSequenceValidity(FSA aut, InputSequence seq)`	Checks if an input sequence is valid for an finite state automaton.
`static void`	`contractEmptyAlphabet(Automaton aut)`	Removes the inserted proposition by the method `#expandEmptyAlphabet(Automaton)`.
`static void`	`copyInTransitions(State si, State sj, OmegaUtil.AcceptanceAction action)`	Copies incoming transitions of a specified state to another specified state.
`static void`	`copyOutTransitions(State si, State sj, OmegaUtil.AcceptanceAction action)`	Copies outgoing transitions of a specified state to another specified state.
`static void`	`eliminateEpsilonTransitions(FSA aut)`	Eliminates ε-transitions of a classic finite state automaton with a classical alphabet.
`static void`	`empty(Automaton aut)`	Makes an automaton accept an empty language by removing all states and transitions except only one non-accepting initial state.
`static void`	`equalizeAlphabet(Automaton aut1, Automaton aut2)`	Makes two automaton have the same alphabet.
`static boolean`	`expandEmptyAlphabet(Automaton aut)`	Expands the alphabet of an automaton by adding a new proposition if the alphabet is empty.
`static void`	`expandWithEpsilon(FSA aut, java.util.List<StateRun> runs)`	Expands a specified list of state runs with ε-transitions.
`static java.util.List<StateRun>`	`expandWithEpsilon(FSA aut, StateRun run)`	Returns a list of state runs obtained by expanding a specified state run with ε-transitions.
`static boolean[][]`	`getAdjacentMatrix(Automaton aut)`	Returns the adjacent matrix `m` for the states of an automaton.
`static java.util.Set<StateList>`	`getCycles(java.util.Collection<StateList> cycles)`	Returns all cycles that can be formed by a specified collection of cycles.
`static java.util.Set<StateList>`	`getCycles(Automaton aut)`	Returns all cycles in a specified automaton.
`static java.util.Set<StateList>`	`getCycles(Automaton aut, StateSet area)`	Returns all cycles restricted in a specified area of an automaton.
`static java.util.List<StateList>`	`getElementaryCycles(Automaton aut)`	Deprecated. use `ElementaryCycleFinder`
`static java.util.List<StateList>`	`getElementaryCycles(Automaton aut, AlgorithmListener listener)`	Deprecated. use `ElementaryCycleFinder`
`static java.util.List<StateList>`	`getElementaryCycles(Automaton aut, StateSet area)`	Deprecated. use `ElementaryCycleFinder`
`static int`	`getMaxNonemptyParity(ParityAcc acc)`	Returns the maximum non-empty parity.
`static int`	`getMaxParity(ParityAcc acc, StateSet states)`	Returns the maximum parity among a set of states.
`static int`	`getMinParity(ParityAcc acc, StateSet states)`	Returns the minimum parity among a set of states.
`static java.util.Collection<StateSet>`	`getMSCCs(Automaton aut)`	Returns the maximal strongly connected components (MSCCs) of an automaton.
`static StateList`	`getPath(Automaton aut, StateSet set, State p, State q)`	Returns a non-empty path in an automaton from a state `p` to another state `q` through states in a specified set.
`static java.util.Set<StateList>`	`getStateCycles(java.util.Collection<StateList> cycles)`	Returns cycles that can be formed by a specified collection of cycles.
`static java.util.Set<StateList>`	`getStateCycles(Automaton aut)`	Returns cycles in a specified automaton.
`static java.util.Set<StateList>`	`getStateCycles(Automaton aut, StateSet area)`	Returns cycles restricted in a specified area of an automaton.
`static java.util.SortedMap<java.lang.Integer,StateSet>`	`getStateParityMap(ParityAcc acc, StateSet states)`	Returns a map from a parity to states, among a specified set of states, that have the parity.
`static <T extends Automaton> T`	`getSubgraph(T aut, StateSet set)`	Returns a subgraph of an automaton.
`static java.awt.Point`	`getTransitionControlPoint(Transition t)`	Deprecated. use `Transition#getControlPoint()` instead
`static TransitionSet`	`getTransitionsInArea(Automaton aut, java.util.Collection<State> area)`	Returns the transitions in an area of an automaton.
`static TransitionSet`	`getTransitionsInCycle(Automaton aut, StateList cycle)`	Returns the transitions in a cycle of an automaton.
`static boolean`	`hasEpsilonTransition(Automaton aut)`	Returns `true` if a specified automaton has ε-transitions.
`static boolean`	`hasPath(Automaton aut, StateSet set, State p, State q)`	Checks if there is a non-empty path in an automaton from a specified state to another specified state through states in a specified set.
`static boolean`	`hasPath(Automaton aut, TransitionSet set, State p, State q)`	Checks if there is a non-empty path in an automaton from a specified state to another specified state through transitions in a specified set.
`static boolean`	`hasSameAccepting(Automaton aut, State s1, State s2)`	Returns `true` if two states behave the same in the acceptance condition of an automaton.
`static boolean`	`hasSameAccepting(Automaton aut, Transition t1, Transition t2)`	Returns `true` if two transitions behave the same in the acceptance condition of an automaton.
`static boolean`	`hasSameAlphabet(Automaton aut1, Automaton aut2)`	Returns `true` if two automata have the same alphabet type and the same alphabet.
`static boolean`	`hasSameAlphaPredecessors(State si, State sj)`	Returns `true` if there is a transition (sk, a, si) if and only if there is a transition (sk, a, sj) for all symbol a and state sk.
`static boolean`	`hasSameAlphaSuccessors(Automaton aut, State s, State t)`	Returns `true` if the two specified states have the same α-successors.
`static boolean`	`hasSameAlphaSuccessors(State si, State sj)`	Returns `true` if there is a transition (si, a, sk) if and only if there is a transition (sj, a, sk) for all symbol a and state sk.
`static boolean`	`hasSameAtomicPropositions(Automaton aut1, Automaton aut2)`	Returns `true` if two specified automata have the same set of atomic propositions.
`static void`	`imitateAcceptance(Acc<?> acc1, State s1, Acc<?> acc2, State s2, OmegaUtil.AcceptanceAction action)`	Makes a state imitate another state in an acceptance condition.
`static void`	`imitateAcceptance(Acc<?> acc1, Transition t1, Acc<?> acc2, Transition t2, OmegaUtil.AcceptanceAction action)`	Makes a transition imitate another transition in an acceptance condition.
`static boolean`	`isABW(java.lang.Object obj)`	Returns `true` if an object is an alternating Büchi word automaton.
`static boolean`	`isAccOnState(Acc<?> acc)`	Checks if the acceptance condition is on states.
`static boolean`	`isAccOnTransition(Acc<?> acc)`	Checks if the acceptance condition is on transitions.
`static boolean`	`isACW(java.lang.Object obj)`	Returns `true` if an object is an alternating co-Büchi word automaton.
`static boolean`	`isAGBW(java.lang.Object obj)`	Returns `true` if an object is an alternating generalized Büchi word automaton.
`static boolean`	`isAMW(java.lang.Object obj)`	Returns `true` if an object is an alternating Muller word automaton.
`static boolean`	`isAPW(java.lang.Object obj)`	Returns `true` if an object is an alternating parity word automaton.
`static boolean`	`isARW(java.lang.Object obj)`	Returns `true` if an object is an alternating Rabin word automaton.
`static boolean`	`isASW(java.lang.Object obj)`	Returns `true` if an object is an alternating Streett word automaton.
`static boolean`	`isClassicalAlphabet(java.lang.Object obj)`	Returns `true` if a specified object is an automaton with a classical alphabet.
`static boolean`	`isCNFAltAutomaton(java.lang.Object obj)`	Checks if an object is an automaton with alternation in CNF form.
`static boolean`	`isConfiguarionLoopAccepting(FSA aut, java.util.Collection<Configuration> cfgs)`	Returns `true` if a sequence of configurations forming a loop satisfy the acceptance condition of the automaton.
`static boolean`	`isCycle(Automaton aut, StateSet states)`	Returns `true` if the states in a specified set form a cycle in a specified automaton, that is, for every two states in the set, there is a path from one state to the other state in the automaton through only states in the set.
`static boolean`	`isCycle(Automaton aut, TransitionSet trans)`	Returns `true` if a specified set of transitions form a cycle in a specified automaton.
`static boolean`	`isDBG(java.lang.Object obj)`	Returns `true` an object is a deterministic Büchi game.
`static boolean`	`isDBW(java.lang.Object obj)`	Returns `true` if the specified object is a deterministic Büchi word automaton.
`static boolean`	`isDCG(java.lang.Object obj)`	Returns `true` an object is a deterministic co-Büchi game.
`static boolean`	`isDCW(java.lang.Object obj)`	Returns `true` if the specified object is a deterministic co-Büchi word automaton.
`static boolean`	`isDeterministic(Automaton aut)`	Checks if an automaton is deterministic.
`static boolean`	`isDFG(java.lang.Object obj)`	Returns `true` an object is a deterministic game with a classic acceptance condition.
`static boolean`	`isDFW(java.lang.Object obj)`	Returns `true` if the specified object is a deterministic finite word automaton.
`static boolean`	`isDGBG(java.lang.Object obj)`	Returns `true` an object is a deterministic generalized Büchi game.
`static boolean`	`isDGBW(java.lang.Object obj)`	Returns `true` if the specified object is a deterministic generalized Büchi word automaton.
`static boolean`	`isDMG(java.lang.Object obj)`	Returns `true` an object is a deterministic Muller game.
`static boolean`	`isDMW(java.lang.Object obj)`	Returns `true` if the specified object is a deterministic Muller word automaton.
`static boolean`	`isDNFAltAutomaton(java.lang.Object obj)`	Checks if an object is an automaton with alternation in DNF form.
`static boolean`	`isDPG(java.lang.Object obj)`	Returns `true` an object is a deterministic parity game.
`static boolean`	`isDPW(java.lang.Object obj)`	Returns `true` if the specified object is a deterministic parity word automaton.
`static boolean`	`isDREG(java.lang.Object obj)`	Returns `true` an object is a deterministic reachability game.
`static boolean`	`isDREW(java.lang.Object obj)`	Checks if an object is a deterministic reachability automaton.
`static boolean`	`isDRG(java.lang.Object obj)`	Returns `true` an object is a deterministic Rabin game.
`static boolean`	`isDRW(java.lang.Object obj)`	Returns `true` if the specified object is a deterministic Rabin word automaton.
`static boolean`	`isDSG(java.lang.Object obj)`	Returns `true` an object is a deterministic Streett game.
`static boolean`	`isDSW(java.lang.Object obj)`	Returns `true` if the specified object is a deterministic Streett word automaton.
`static boolean`	`isDTBW(java.lang.Object obj)`	Returns `true` if a specified object is a DTBW.
`static boolean`	`isDTCW(java.lang.Object obj)`	Returns `true` if a specified object is a DTCW.
`static boolean`	`isDTGBW(java.lang.Object obj)`	Returns `true` if a specified object is a DTGBW.
`static boolean`	`isDTMW(java.lang.Object obj)`	Returns `true` if a specified object is a DTMW.
`static boolean`	`isDTPW(java.lang.Object obj)`	Returns `true` if a specified object is a DTPW.
`static boolean`	`isDTRW(java.lang.Object obj)`	Returns `true` if a specified object is a DTRW.
`static boolean`	`isDTSW(java.lang.Object obj)`	Returns `true` if a specified object is a DTSW.
`static boolean`	`isHOA(java.lang.Object obj)`	Returns `true` if a specified object is a Hanoi automaton.
`static boolean`	`isLittleWeak(TwoWayAltAutomaton aut)`	Returns `true` if a specified two-way alternating co-Büchi automaton is little weak, that is, there is a partial order ≤ on the states such that for all state s, s is trapped in a sub-graph which contains no accepting states, or for all backward or forward successor t of s, t < s.
`static boolean`	`isLOS(Automaton aut)`	Checks if the labels of an automaton are on states.
`static boolean`	`isLOSNBW(java.lang.Object obj)`	Checks if an object is a label-on-state nondeterministic Büchi word automaton.
`static boolean`	`isLOSNCW(java.lang.Object obj)`	Checks if an object is a label-on-state nondeterministic co-Büchi word automaton.
`static boolean`	`isLOSNFW(java.lang.Object obj)`	Checks if an object is a label-on-state nondeterministic finite word automaton.
`static boolean`	`isLOSNGBW(java.lang.Object obj)`	Checks if an object is a label-on-state nondeterministic generalized Büchi word automaton.
`static boolean`	`isLOSNMW(java.lang.Object obj)`	Checks if an object is a label-on-state nondeterministic Muller word automaton.
`static boolean`	`isLOSNPW(java.lang.Object obj)`	Checks if an object is a label-on-state nondeterministic parity word automaton.
`static boolean`	`isLOSNREW(java.lang.Object obj)`	Checks if an object is a label-on-state nondeterministic reachability automaton.
`static boolean`	`isLOSNRW(java.lang.Object obj)`	Checks if an object is a label-on-state nondeterministic Rabin word automaton.
`static boolean`	`isLOSNSW(java.lang.Object obj)`	Checks if an object is a label-on-state nondeterministic Streett word automaton.
`static boolean`	`isLOT(Automaton aut)`	Checks if the labels of an automaton are on transitions.
`static boolean`	`isMSCCAccepting(Automaton aut, StateSet mscc)`	Returns `true` if a maximal strongly connected component (MSCC) is accepting.
`static boolean`	`isNBG(java.lang.Object obj)`	Returns `true` an object is a nondeterministic Büchi game.
`static boolean`	`isNBW(java.lang.Object obj)`	Checks if an object is a nondeterministic Büchi word automaton.
`static boolean`	`isNCG(java.lang.Object obj)`	Returns `true` an object is a nondeterministic co-Büchi game.
`static boolean`	`isNCW(java.lang.Object obj)`	Checks if an object is a nondeterministic co-Büchi word automaton.
`static boolean`	`isNFG(java.lang.Object obj)`	Returns `true` an object is a nondeterministic game with a classic accentance condition.
`static boolean`	`isNFW(java.lang.Object obj)`	Checks if an object is a nondeterministic finite word automaton.
`static boolean`	`isNGBG(java.lang.Object obj)`	Returns `true` an object is a nondeterministic generalized Büchi game.
`static boolean`	`isNGBW(java.lang.Object obj)`	Checks if an object is a nondeterministic generalized Büchi word automaton.
`static boolean`	`isNMG(java.lang.Object obj)`	Returns `true` an object is a nondeterministic Muller game.
`static boolean`	`isNMW(java.lang.Object obj)`	Checks if an object is a nondeterministic Muller word automaton.
`static boolean`	`isNPG(java.lang.Object obj)`	Returns `true` an object is a nondeterministic parity game.
`static boolean`	`isNPW(java.lang.Object obj)`	Checks if an object is a nondeterministic parity word automaton.
`static boolean`	`isNREG(java.lang.Object obj)`	Returns `true` an object is a nondeterministic reachability game.
`static boolean`	`isNREW(java.lang.Object obj)`	Checks if an object is a nondeterministic reachability automaton.
`static boolean`	`isNRG(java.lang.Object obj)`	Returns `true` an object is a nondeterministic Rabin game.
`static boolean`	`isNRW(java.lang.Object obj)`	Checks if an object is a nondeterministic Rabin word automaton.
`static boolean`	`isNSG(java.lang.Object obj)`	Returns `true` an object is a nondeterministic Streett game.
`static boolean`	`isNSW(java.lang.Object obj)`	Checks if an object is a nondeterministic Streett word automaton.
`static boolean`	`isNTBW(java.lang.Object obj)`	Returns `true` if a specified object is an NTBW.
`static boolean`	`isNTCW(java.lang.Object obj)`	Returns `true` if a specified object is an NTCW.
`static boolean`	`isNTGBW(java.lang.Object obj)`	Returns `true` if a specified object is an NTGBW.
`static boolean`	`isNTMW(java.lang.Object obj)`	Returns `true` if a specified object is an NTMW.
`static boolean`	`isNTPW(java.lang.Object obj)`	Returns `true` if a specified object is an NTPW.
`static boolean`	`isNTRW(java.lang.Object obj)`	Returns `true` if a specified object is an NTRW.
`static boolean`	`isNTSW(java.lang.Object obj)`	Returns `true` if a specified object is an NTSW.
`static boolean`	`isOmegaAutomaton(java.lang.Object obj)`	Returns `true` if a specified object is an ω-automaton.
`static boolean`	`isPropositionalAlphabet(java.lang.Object obj)`	Returns `true` if a specified object is an automaton with a propositional alphabet.
`static boolean`	`isSDBW(java.lang.Object obj)`	Returns `true` if the specified object is a semi-deterministic Büchi word automaton.
`static boolean`	`isTriviallyEmpty(FSA aut)`	Returns `true` if an automaton is trivally empty, that is, the automaton has at most one state, and the automaton has no transition.
`static boolean`	`isTriviallyUniversal(FSA aut)`	Returns `true` if an automaton is trivally universal.
`static boolean`	`isTWABW(java.lang.Object obj)`	Returns `true` if an object is a two-way alternating Büchi word automaton.
`static boolean`	`isTWACW(java.lang.Object obj)`	Returns `true` if an object is a two-way alternating co-Büchi word automaton.
`static boolean`	`isTWAGBW(java.lang.Object obj)`	Returns `true` if an object is a two-way alternating generalized Büchi word automaton.
`static boolean`	`isTWAMW(java.lang.Object obj)`	Returns `true` if an object is a two-way alternating Muller word automaton.
`static boolean`	`isTWAPW(java.lang.Object obj)`	Returns `true` if an object is a two-way alternating parity word automaton.
`static boolean`	`isTWARW(java.lang.Object obj)`	Returns `true` if an object is a two-way alternating Rabin word automaton.
`static boolean`	`isTWASW(java.lang.Object obj)`	Returns `true` if an object is a two-way alternating Streett word automaton.
`static boolean`	`isTWLWAA(java.lang.Object obj)`	Returns `true` if a specified object is a co-Büchi two-way little weak alternating automaton in DNF.
`static boolean`	`isTWVWAA(java.lang.Object obj)`	Returns `true` if a specified object is a co-Büchi two-way very weak alternating automaton in DNF.
`static boolean`	`isUCW(java.lang.Object obj)`	Checks if an object is a universal co-Büchi word automaton, that is, a CNF alternating automaton with co-Büchi acceptance condition.
`static boolean`	`isValidNPW(java.lang.Object obj)`	Returns `true` if an object is a valid parity automaton.
`static boolean`	`isValidNTPW(java.lang.Object obj)`	Returns `true` if an object is a valid transition parity automaton.
`static boolean`	`isValidParityAcc(ParityAcc acc)`	Checks if a parity condition is valid, that is, it contains all states and every state has only one parity.
`static boolean`	`isValidParityAcc(TParityAcc acc)`	Checks if a parity condition is valid, that is, it contains all states and every state has only one parity.
`static boolean`	`isVeryWeak(AbstractAltAutomaton aut)`	Returns `true` if a specified alternating automaton is very weak.
`static boolean`	`isVeryWeak(Automaton aut)`	Returns `true` if a specified object is a very weak automata.
`static boolean`	`isVWAA(java.lang.Object obj)`	Returns `true` if a specified object is a co-Büchi very weak alternating automaton in DNF.
`static boolean`	`isWAA(java.lang.Object obj)`	Returns `true` if a specified object is a weak alternating Büchi automaton in CNF.
`static boolean`	`isWAPA(java.lang.Object obj)`	Returns `true` if a specified object is a weak alternating parity automaton in CNF.
`static boolean`	`isWeak(Automaton aut)`	Returns `true` if a specified object is a weak automaton.
`static boolean`	`isWeaklyDeterministic(Automaton aut)`	Returns `true` if an automaton with labels on transitions is weakly deterministic.
`static void`	`makeTransitionComplete(Automaton aut)`	Makes the transition relation complete by adding a sink state.
`static StateSet`	`maximizeAcceptingSet(AlgorithmListener listener, Automaton aut)`	Maximizes the Büchi acceptance condition of an automaton without changing the language of the automaton by finding all strongly connected components.
`static StateSet`	`maximizeAcceptingSet(Automaton aut)`	Maximizes the Büchi acceptance condition of an automaton without changing the language of the automaton.
`static StateSet`	`maximizeAcceptingSet2(AlgorithmListener listener, Automaton aut)`	Maximizes the Büchi acceptance condition of an automaton without changing the language of the automaton by finding cycles.
`static <T extends Automaton> T`	`merge(T aut1, T aut2)`	Merges two automata with the same alphabet type, label position, and type of acceptance condition.
`static void`	`mergeEquivalentStates(Automaton aut, State s1, State s2)`	Merges a specified state `s2` into another specified state `s1`.
`static void`	`mergeInitialStates(Automaton aut)`	Merges the initial states of a label-on-transition automaton by creating a new initial state to simulate the old initial states.
`static void`	`mergeStates(State[] states)`	Merge specified states.
`static void`	`mergeStates(State s1, State s2)`	Merges two states s1 and s2 in the same automaton by copying all incoming transitions and outgoing transitions of s2 to s1, adding s1 to an acceptance set if s2 is in the set, making s1 initial if s2 is initial, and finally removing s2.
`static StateSet`	`minimizeAcceptingSet(AlgorithmListener listener, Automaton aut)`	Simplifies the Büchi acceptance condition of an automaton without changing the language of the automaton by finding all strongly connected components.
`static StateSet`	`minimizeAcceptingSet(Automaton aut)`	Simplifies the Büchi acceptance condition of an automaton without changing the language of the automaton.
`static FSA`	`omega(FSA aut)`	Returns an NBW that accepts L^ω where L is the language accepted by a specified NFW.
`static <T extends Automaton> java.util.Map<State,State>`	`paste(T aut1, StateSet states, T aut2, boolean keep_init, boolean keep_acc)`	Paste states of an automaton onto another automaton.
`static <T extends Automaton> java.util.Map<State,State>`	`paste(T aut1, T aut2, boolean keep_init, boolean keep_acc)`	Paste an automaton onto another automaton.
`static void`	`reduceNotLeadTo(Automaton aut, State s)`	Removes all states that cannot reach a specified state.
`static void`	`reduceNotReachedFrom(Automaton aut, State s)`	Removes all states that cannot be reached by a specified state.
`static void`	`setTransitionControlPoint(Transition t, java.awt.Point p)`	Deprecated. use `Transition#setControlPoint(Point)` instead
`static TransitionSet`	`simulate(Automaton aut, State s, State t)`	Make a specified state s simulate another specified state t by adding transitions with symbol sym from s to u if there is a transition with the same symbol from t to u.
`static FSA`	`star(FSA aut)`	Returns an NFW that accepts L* where L is the language of a specified NFW.

Methods inherited from class java.lang.Object

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

Constructor Details
- OmegaUtil
  
  public OmegaUtil()
Method Details
- getTransitionControlPoint
  
  public static java.awt.Point getTransitionControlPoint(Transition t)
  
  Deprecated.
  use Transition#getControlPoint() instead
  
  Returns the control point of a transition. The control point, the location of the source state, and the location of the destination state are used to draw the transition as a curve.
  
  Parameters:
  
  t - a transition
  
  Returns:
  
  the control point of the transition
- setTransitionControlPoint
  
  public static void setTransitionControlPoint(Transition t, java.awt.Point p)
  
  Deprecated.
  use Transition#setControlPoint(Point) instead
  
  Sets the control point of a transition.
  
  Parameters:
  
  t - a transition
  
  p - a new location for the control point
  
  See Also:
  
  getTransitionControlPoint(Transition)
- isClassicalAlphabet
  
  public static boolean isClassicalAlphabet(java.lang.Object obj)
  
  Returns true if a specified object is an automaton with a classical alphabet.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is an automaton with a classical alphabet
- isPropositionalAlphabet
  
  public static boolean isPropositionalAlphabet(java.lang.Object obj)
  
  Returns true if a specified object is an automaton with a propositional alphabet.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is an automaton with a propositional alphabet
- isAccOnState
  
  public static boolean isAccOnState(Acc<?> acc)
  
  Checks if the acceptance condition is on states.
  
  Parameters:
  
  acc - the acceptance condition to be checked
  
  Returns:
  
  true if the acceptance condition is on states
- isAccOnTransition
  
  public static boolean isAccOnTransition(Acc<?> acc)
  
  Checks if the acceptance condition is on transitions.
  
  Parameters:
  
  acc - the acceptance condition to be checked
  
  Returns:
  
  true if the acceptance condition is on transitions
- isLOT
  
  public static boolean isLOT(Automaton aut)
  
  Checks if the labels of an automaton are on transitions.
  
  Parameters:
  
  aut - the automaton to be checked
  
  Returns:
  
  true if the labels of the automaton are on transitions
- isLOS
  
  public static boolean isLOS(Automaton aut)
  
  Checks if the labels of an automaton are on states.
  
  Parameters:
  
  aut - the automaton to be checked
  
  Returns:
  
  true if the labels of the automaton are on states
- isLOSNFW
  
  public static boolean isLOSNFW(java.lang.Object obj)
  
  Checks if an object is a label-on-state nondeterministic finite word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a label-on-state nondeterministic finite word automaton
- isLOSNREW
  
  public static boolean isLOSNREW(java.lang.Object obj)
  
  Checks if an object is a label-on-state nondeterministic reachability automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a label-on-state nondeterministic reachability automaton
- isLOSNBW
  
  public static boolean isLOSNBW(java.lang.Object obj)
  
  Checks if an object is a label-on-state nondeterministic Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a label-on-state nondeterministic Büchi word automaton
- isLOSNCW
  
  public static boolean isLOSNCW(java.lang.Object obj)
  
  Checks if an object is a label-on-state nondeterministic co-Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a label-on-state nondeterministic co-Büchi word automaton
- isLOSNGBW
  
  public static boolean isLOSNGBW(java.lang.Object obj)
  
  Checks if an object is a label-on-state nondeterministic generalized Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a label-on-state nondeterministic generalized Büchi word automaton
- isLOSNMW
  
  public static boolean isLOSNMW(java.lang.Object obj)
  
  Checks if an object is a label-on-state nondeterministic Muller word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a label-on-state nondeterministic Muller word automaton
- isLOSNRW
  
  public static boolean isLOSNRW(java.lang.Object obj)
  
  Checks if an object is a label-on-state nondeterministic Rabin word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a label-on-state nondeterministic Rabin word automaton
- isLOSNSW
  
  public static boolean isLOSNSW(java.lang.Object obj)
  
  Checks if an object is a label-on-state nondeterministic Streett word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a label-on-state nondeterministic Streett word automaton
- isLOSNPW
  
  public static boolean isLOSNPW(java.lang.Object obj)
  
  Checks if an object is a label-on-state nondeterministic parity word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a label-on-state nondeterministic parity word automaton
- isNFW
  
  public static boolean isNFW(java.lang.Object obj)
  
  Checks if an object is a nondeterministic finite word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic finite word automaton
- isDFW
  
  public static boolean isDFW(java.lang.Object obj)
  
  Returns true if the specified object is a deterministic finite word automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if obj is a deterministic finite word automaton
- isNREW
  
  public static boolean isNREW(java.lang.Object obj)
  
  Checks if an object is a nondeterministic reachability automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic reachability automaton
- isDREW
  
  public static boolean isDREW(java.lang.Object obj)
  
  Checks if an object is a deterministic reachability automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a deterministic reachability automaton
- isNBW
  
  public static boolean isNBW(java.lang.Object obj)
  
  Checks if an object is a nondeterministic Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic Büchi word automaton
- isDBW
  
  public static boolean isDBW(java.lang.Object obj)
  
  Returns true if the specified object is a deterministic Büchi word automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if obj is a deterministic Büchi word automaton
- isNGBW
  
  public static boolean isNGBW(java.lang.Object obj)
  
  Checks if an object is a nondeterministic generalized Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic generalized Büchi word automaton
- isDGBW
  
  public static boolean isDGBW(java.lang.Object obj)
  
  Returns true if the specified object is a deterministic generalized Büchi word automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if obj is a deterministic generalized Büchi word automaton
- isNCW
  
  public static boolean isNCW(java.lang.Object obj)
  
  Checks if an object is a nondeterministic co-Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic co-Büchi word automaton
- isDCW
  
  public static boolean isDCW(java.lang.Object obj)
  
  Returns true if the specified object is a deterministic co-Büchi word automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if obj is a deterministic co-Büchi word automaton
- isNMW
  
  public static boolean isNMW(java.lang.Object obj)
  
  Checks if an object is a nondeterministic Muller word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic Muller word automaton
- isDMW
  
  public static boolean isDMW(java.lang.Object obj)
  
  Returns true if the specified object is a deterministic Muller word automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if obj is a deterministic Muller word automaton
- isNRW
  
  public static boolean isNRW(java.lang.Object obj)
  
  Checks if an object is a nondeterministic Rabin word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic Rabin word automaton
- isDRW
  
  public static boolean isDRW(java.lang.Object obj)
  
  Returns true if the specified object is a deterministic Rabin word automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if obj is a deterministic Rabin word automaton
- isNSW
  
  public static boolean isNSW(java.lang.Object obj)
  
  Checks if an object is a nondeterministic Streett word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic Streett word automaton
- isDSW
  
  public static boolean isDSW(java.lang.Object obj)
  
  Returns true if the specified object is a deterministic Streett word automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if obj is a deterministic Streett word automaton
- isNPW
  
  public static boolean isNPW(java.lang.Object obj)
  
  Checks if an object is a nondeterministic parity word automaton. Note that this method only checks the type of the object and the type of the acceptance condition. The parity condition of the object may still be invalid.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic parity word automaton
- isDPW
  
  public static boolean isDPW(java.lang.Object obj)
  
  Returns true if the specified object is a deterministic parity word automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if obj is a deterministic parity word automaton
  
  See Also:
  
  isNPW(Object)
- isSDBW
  
  public static boolean isSDBW(java.lang.Object obj)
  
  Returns true if the specified object is a semi-deterministic Büchi word automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if obj is a semi-deterministic Büchi word automaton
- isNTBW
  
  public static boolean isNTBW(java.lang.Object obj)
  
  Returns true if a specified object is an NTBW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is an NTBW
- isDTBW
  
  public static boolean isDTBW(java.lang.Object obj)
  
  Returns true if a specified object is a DTBW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a DTBW
- isNTCW
  
  public static boolean isNTCW(java.lang.Object obj)
  
  Returns true if a specified object is an NTCW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is an NTCW
- isDTCW
  
  public static boolean isDTCW(java.lang.Object obj)
  
  Returns true if a specified object is a DTCW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a DTCW
- isNTGBW
  
  public static boolean isNTGBW(java.lang.Object obj)
  
  Returns true if a specified object is an NTGBW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is an NTGBW
- isDTGBW
  
  public static boolean isDTGBW(java.lang.Object obj)
  
  Returns true if a specified object is a DTGBW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a DTGBW
- isNTMW
  
  public static boolean isNTMW(java.lang.Object obj)
  
  Returns true if a specified object is an NTMW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is an NTMW
- isDTMW
  
  public static boolean isDTMW(java.lang.Object obj)
  
  Returns true if a specified object is a DTMW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a DTMW
- isNTRW
  
  public static boolean isNTRW(java.lang.Object obj)
  
  Returns true if a specified object is an NTRW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is an NTRW
- isDTRW
  
  public static boolean isDTRW(java.lang.Object obj)
  
  Returns true if a specified object is a DTRW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a DTRW
- isNTSW
  
  public static boolean isNTSW(java.lang.Object obj)
  
  Returns true if a specified object is an NTSW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is an NTSW
- isDTSW
  
  public static boolean isDTSW(java.lang.Object obj)
  
  Returns true if a specified object is a DTSW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a DTSW
- isNTPW
  
  public static boolean isNTPW(java.lang.Object obj)
  
  Returns true if a specified object is an NTPW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is an NTPW
- isDTPW
  
  public static boolean isDTPW(java.lang.Object obj)
  
  Returns true if a specified object is a DTPW.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a DTPW
- isCNFAltAutomaton
  
  public static boolean isCNFAltAutomaton(java.lang.Object obj)
  
  Checks if an object is an automaton with alternation in CNF form.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is an automaton with alternation in CNF form
- isDNFAltAutomaton
  
  public static boolean isDNFAltAutomaton(java.lang.Object obj)
  
  Checks if an object is an automaton with alternation in DNF form.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is an automaton with alternation in DNF form
- isABW
  
  public static boolean isABW(java.lang.Object obj)
  
  Returns true if an object is an alternating Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is an alternating Büchi word automaton
- isACW
  
  public static boolean isACW(java.lang.Object obj)
  
  Returns true if an object is an alternating co-Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is an alternating co-Büchi word automaton
- isAGBW
  
  public static boolean isAGBW(java.lang.Object obj)
  
  Returns true if an object is an alternating generalized Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is an alternating generalized Büchi word automaton
- isAMW
  
  public static boolean isAMW(java.lang.Object obj)
  
  Returns true if an object is an alternating Muller word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is an alternating Muller word automaton
- isARW
  
  public static boolean isARW(java.lang.Object obj)
  
  Returns true if an object is an alternating Rabin word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is an alternating Rabin word automaton
- isASW
  
  public static boolean isASW(java.lang.Object obj)
  
  Returns true if an object is an alternating Streett word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is an alternating Streett word automaton
- isAPW
  
  public static boolean isAPW(java.lang.Object obj)
  
  Returns true if an object is an alternating parity word automaton. Note that this method only checks the type of the object and the type of the acceptance condition. The parity condition of the object may still be invalid.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is an alternating parity word automaton
- isTWABW
  
  public static boolean isTWABW(java.lang.Object obj)
  
  Returns true if an object is a two-way alternating Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a two-way alternating Büchi word automaton
- isTWACW
  
  public static boolean isTWACW(java.lang.Object obj)
  
  Returns true if an object is a two-way alternating co-Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a two-way alternating co-Büchi word automaton
- isTWAGBW
  
  public static boolean isTWAGBW(java.lang.Object obj)
  
  Returns true if an object is a two-way alternating generalized Büchi word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a two-way alternating generalized Büchi word automaton
- isTWAMW
  
  public static boolean isTWAMW(java.lang.Object obj)
  
  Returns true if an object is a two-way alternating Muller word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a two-way alternating Muller word automaton
- isTWARW
  
  public static boolean isTWARW(java.lang.Object obj)
  
  Returns true if an object is a two-way alternating Rabin word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a two-way alternating Rabin word automaton
- isTWASW
  
  public static boolean isTWASW(java.lang.Object obj)
  
  Returns true if an object is a two-way alternating Streett word automaton.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a two-way alternating Streett word automaton
- isTWAPW
  
  public static boolean isTWAPW(java.lang.Object obj)
  
  Returns true if an object is a two-way alternating parity word automaton. Note that this method only checks the type of the object and the type of the acceptance condition. The parity condition of the object may still be invalid.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a two-way alternating parity word automaton
- isValidParityAcc
  
  public static boolean isValidParityAcc(ParityAcc acc)
  
  Checks if a parity condition is valid, that is, it contains all states and every state has only one parity.
  
  Parameters:
  
  acc - the parity condition to be checked
  
  Returns:
  
  true if the parity condition is valid
- isValidNPW
  
  public static boolean isValidNPW(java.lang.Object obj)
  
  Returns true if an object is a valid parity automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if an object is a valid parity automaton
- isValidParityAcc
  
  public static boolean isValidParityAcc(TParityAcc acc)
  
  Checks if a parity condition is valid, that is, it contains all states and every state has only one parity.
  
  Parameters:
  
  acc - the parity condition to be checked
  
  Returns:
  
  true if the parity condition is valid
- isValidNTPW
  
  public static boolean isValidNTPW(java.lang.Object obj)
  
  Returns true if an object is a valid transition parity automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if an object is a valid transition parity automaton
- isWAA
  
  public static boolean isWAA(java.lang.Object obj)
  
  Returns true if a specified object is a weak alternating Büchi automaton in CNF.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a weak alternating Büchi automaton in CNF
- isWAPA
  
  public static boolean isWAPA(java.lang.Object obj)
  
  Returns true if a specified object is a weak alternating parity automaton in CNF.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a weak alternating parity automaton in CNF
- isVWAA
  
  public static boolean isVWAA(java.lang.Object obj)
  
  Returns true if a specified object is a co-Büchi very weak alternating automaton in DNF.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a co-Büchi very weak alternating automaton in DNF
- isTWVWAA
  
  public static boolean isTWVWAA(java.lang.Object obj)
  
  Returns true if a specified object is a co-Büchi two-way very weak alternating automaton in DNF.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a co-Büchi two-way very weak alternating automaton in DNF
  
  See Also:
  
  isVeryWeak(AbstractAltAutomaton)
- isTWLWAA
  
  public static boolean isTWLWAA(java.lang.Object obj)
  
  Returns true if a specified object is a co-Büchi two-way little weak alternating automaton in DNF.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a co-Büchi two-way little weak alternating automaton in DNF
  
  See Also:
  
  isLittleWeak(TwoWayAltAutomaton)
- isHOA
  
  public static boolean isHOA(java.lang.Object obj)
  
  Returns true if a specified object is a Hanoi automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is a Hanoi automaton
- isUCW
  
  public static boolean isUCW(java.lang.Object obj)
  
  Checks if an object is a universal co-Büchi word automaton, that is, a CNF alternating automaton with co-Büchi acceptance condition.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a universal co-Büchi word automaton
- isDFG
  
  public static boolean isDFG(java.lang.Object obj)
  
  Returns true an object is a deterministic game with a classic acceptance condition.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a deterministic game with a classic acceptance condition
- isDREG
  
  public static boolean isDREG(java.lang.Object obj)
  
  Returns true an object is a deterministic reachability game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a deterministic reachability game
- isDBG
  
  public static boolean isDBG(java.lang.Object obj)
  
  Returns true an object is a deterministic Büchi game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a deterministic Büchi game
- isDCG
  
  public static boolean isDCG(java.lang.Object obj)
  
  Returns true an object is a deterministic co-Büchi game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a deterministic co-Büchi game
- isDGBG
  
  public static boolean isDGBG(java.lang.Object obj)
  
  Returns true an object is a deterministic generalized Büchi game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a deterministic generalized Büchi game
- isDMG
  
  public static boolean isDMG(java.lang.Object obj)
  
  Returns true an object is a deterministic Muller game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a deterministic Muller game
- isDRG
  
  public static boolean isDRG(java.lang.Object obj)
  
  Returns true an object is a deterministic Rabin game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a deterministic Rabin game
- isDSG
  
  public static boolean isDSG(java.lang.Object obj)
  
  Returns true an object is a deterministic Streett game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a deterministic Streett game
- isDPG
  
  public static boolean isDPG(java.lang.Object obj)
  
  Returns true an object is a deterministic parity game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a deterministic parity game
- isNFG
  
  public static boolean isNFG(java.lang.Object obj)
  
  Returns true an object is a nondeterministic game with a classic accentance condition.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic game with a classic accentance condition
- isNREG
  
  public static boolean isNREG(java.lang.Object obj)
  
  Returns true an object is a nondeterministic reachability game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic reachability game
- isNBG
  
  public static boolean isNBG(java.lang.Object obj)
  
  Returns true an object is a nondeterministic Büchi game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic Büchi game
- isNCG
  
  public static boolean isNCG(java.lang.Object obj)
  
  Returns true an object is a nondeterministic co-Büchi game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic co-Büchi game
- isNGBG
  
  public static boolean isNGBG(java.lang.Object obj)
  
  Returns true an object is a nondeterministic generalized Büchi game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic generalized Büchi game
- isNMG
  
  public static boolean isNMG(java.lang.Object obj)
  
  Returns true an object is a nondeterministic Muller game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic Muller game
- isNRG
  
  public static boolean isNRG(java.lang.Object obj)
  
  Returns true an object is a nondeterministic Rabin game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic Rabin game
- isNSG
  
  public static boolean isNSG(java.lang.Object obj)
  
  Returns true an object is a nondeterministic Streett game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic Streett game
- isNPG
  
  public static boolean isNPG(java.lang.Object obj)
  
  Returns true an object is a nondeterministic parity game.
  
  Parameters:
  
  obj - the object to be checked
  
  Returns:
  
  true if the object is a nondeterministic parity game
- isVeryWeak
  
  public static boolean isVeryWeak(Automaton aut)
  
  Returns true if a specified object is a very weak automata.
  
  Parameters:
  
  aut - an automaton
  
  Returns:
  
  true if the specified object is a very weak automata
- isVeryWeak
  
  public static boolean isVeryWeak(AbstractAltAutomaton aut)
  
  Returns true if a specified alternating automaton is very weak.
  
  Parameters:
  
  aut - an alternating automaton
  
  Returns:
  
  true if the specified alternating automaton is very weak
- isLittleWeak
  
  public static boolean isLittleWeak(TwoWayAltAutomaton aut)
  Returns true if a specified two-way alternating co-Büchi automaton is little weak, that is, there is a partial order ≤ on the states such that for all state s,
  
  s is trapped in a sub-graph which contains no accepting states, or
  
  for all backward or forward successor t of s, t < s.
  Parameters:
  
  aut - an alternating automaton
  
  Returns:
  
  true if the specified two-way alternating co-Büchi automaton is futurely very weak
- isWeak
  
  public static boolean isWeak(Automaton aut) throws java.lang.IllegalArgumentException
  Returns true if a specified object is a weak automaton. An automaton is weak if it satisfies one of the following conditions.
  
  its acceptance condition F is Büchi,
  
  its states can be partitioned into disjoint subsets Q1, Q2, ..., Qn such that for each Qi, Qi ⊆ F or Qi ∩ F = ∅, and
  
  there is a partial order < on the subsets such that Qi cannot have transitions to Qj if Qi < Qj.
  
  its acceptance condition F is parity, and
  
  if there is a transition from some state si to some state sj, then F(si) ≥ F(sj).
  Parameters:
  
  aut - an automaton
  
  Returns:
  
  true if the specified object is a weak automaton
  
  Throws:
  
  java.lang.IllegalArgumentException - if the input cannot be tested
- isOmegaAutomaton
  
  public static boolean isOmegaAutomaton(java.lang.Object obj)
  
  Returns true if a specified object is an ω-automaton.
  
  Parameters:
  
  obj - an object
  
  Returns:
  
  true if the specified object is an ω-automaton
- isDeterministic
  
  public static boolean isDeterministic(Automaton aut)
  
  Checks if an automaton is deterministic.
  
  Parameters:
  
  aut - an automaton to be checked
  
  Returns:
  
  true if the automaton is deterministic
- isWeaklyDeterministic
  
  public static boolean isWeaklyDeterministic(Automaton aut)
  
  Returns true if an automaton with labels on transitions is weakly deterministic. An automaton is weakly deterministic if for every state in the automaton, every outgoing transition of the state has a distinct label. If an automaton is weakly deterministic, it can become deterministic by calling makeTransitionComplete(Automaton).
  
  Parameters:
  
  aut - an automaton to be checked
  
  Returns:
  
  true if the automaton is weakly deterministic
- equalizeAlphabet
  
  public static void equalizeAlphabet(Automaton aut1, Automaton aut2)
  
  Makes two automaton have the same alphabet. The proposition (or classical symbol) of one automaton that is missing in the other automaton will be added to the other automaton.
  
  Parameters:
  
  aut1 - an automaton
  
  aut2 - an automaton
- hasSameAtomicPropositions
  
  public static boolean hasSameAtomicPropositions(Automaton aut1, Automaton aut2)
  
  Returns true if two specified automata have the same set of atomic propositions.
  
  Parameters:
  
  aut1 - an automaton
  
  aut2 - an automaton
  
  Returns:
  
  true if the two specified automata have the same set of atomic propositions
- hasSameAccepting
  
  public static boolean hasSameAccepting(Automaton aut, State s1, State s2)
  
  Returns true if two states behave the same in the acceptance condition of an automaton.
  
  Parameters:
  
  aut - an automaton
  
  s1 - a state in the automaton
  
  s2 - a state in the automaton
  
  Returns:
  
  true if the two states behave the same in the acceptance condition of the automaton
- hasSameAccepting
  
  public static boolean hasSameAccepting(Automaton aut, Transition t1, Transition t2)
  
  Returns true if two transitions behave the same in the acceptance condition of an automaton.
  
  Parameters:
  
  aut - an automaton
  
  t1 - a transition in the automaton
  
  t2 - a transition in the automaton
  
  Returns:
  
  true if the two transitions behave the same in the acceptance condition of the automaton
- mergeInitialStates
  
  public static void mergeInitialStates(Automaton aut) throws java.lang.IllegalArgumentException
  
  Merges the initial states of a label-on-transition automaton by creating a new initial state to simulate the old initial states. Note that the new initial state will not be in the acceptance condition if the automaton is an ω-automaton. If the automaton is a classic finite state automaton and some of its initial state is accepting, then the merged initial state will also be accepting.
  
  Parameters:
  
  aut - the automaton with initial states to be merged
  
  Throws:
  
  java.lang.IllegalArgumentException - if aut is not a label-on-transition automaton
- mergeEquivalentStates
  
  public static void mergeEquivalentStates(Automaton aut, State s1, State s2)
  
  Merges a specified state s2 into another specified state s1. If s2 is in an acceptance set, then s1 will be added to the same acceptance set. If s2 is an initial state, s1 will become an initial state. For all self-looped transitions of s2, self-loop transitions of s1 with the same symbols will be created. For transitions from s2 to another state t, transitions with the same symbols from s1 to t will be created. For transitions from t to s2, transitions with the same symbols from t to s1 will be created. Finally, s2 will be removed from the automaton.
  
  Parameters:
  
  aut - an automaton
  
  s1 - a state in the automaton
  
  s2 - a state in the automaton
- mergeStates
  
  public static void mergeStates(State s1, State s2)
  
  Merges two states s1 and s2 in the same automaton by copying all incoming transitions and outgoing transitions of s2 to s1, adding s1 to an acceptance set if s2 is in the set, making s1 initial if s2 is initial, and finally removing s2.
  
  Parameters:
  
  s1 - a state
  
  s2 - a state
- mergeStates
  
  public static void mergeStates(State[] states)
  
  Merge specified states.
  
  Parameters:
  
  states - states in the same automaton
  
  See Also:
  
  mergeStates(State, State)
- getElementaryCycles
  
  public static java.util.List<StateList> getElementaryCycles(Automaton aut, AlgorithmListener listener)
  
  Deprecated.
  use ElementaryCycleFinder
  
  Returns all elementary cycles of an automaton.
  
  Parameters:
  
  aut - an automaton
  
  listener - an algorithm listener that is interested in the progress of this operation, null if no one is interested
  
  Returns:
  
  all elementary cycles of the automaton
- getElementaryCycles
  
  public static java.util.List<StateList> getElementaryCycles(Automaton aut)
  
  Deprecated.
  use ElementaryCycleFinder
  
  Returns all elementary cycles of an automaton.
  
  Parameters:
  
  aut - an automaton
  
  Returns:
  
  all elementary cycles of the automaton
- getElementaryCycles
  
  public static java.util.List<StateList> getElementaryCycles(Automaton aut, StateSet area)
  
  Deprecated.
  use ElementaryCycleFinder
  
  Returns elementary cycles restricted in a specified area of an automaton.
  
  Parameters:
  
  aut - an automaton
  
  area - an area in the automaton
  
  Returns:
  
  elementary cycles in the specified area of the automaton
- getStateCycles
  
  public static java.util.Set<StateList> getStateCycles(Automaton aut)
  
  Returns cycles in a specified automaton. Note that in this method, if more than one cycle is composed of the same set of states, only one of them will be returned.
  
  Parameters:
  
  aut - an automaton
  
  Returns:
  
  cycles in aut
- getStateCycles
  
  public static java.util.Set<StateList> getStateCycles(Automaton aut, StateSet area)
  
  Returns cycles restricted in a specified area of an automaton. Note that in this method, if more than one cycle is composed of the same set of states, only one of them will be returned.
  
  Parameters:
  
  aut - an automaton
  
  area - an area in the automaton
  
  Returns:
  
  cycles in the specified area of the automaton
- getStateCycles
  
  public static java.util.Set<StateList> getStateCycles(java.util.Collection<StateList> cycles)
  
  Returns cycles that can be formed by a specified collection of cycles. Note that in this method, if more than one cycle is composed of the same set of states, only one of them will be returned.
  
  Parameters:
  
  cycles - cycles
  
  Returns:
  
  cycles that can be formed by the specified collection of cycles
- getCycles
  
  public static java.util.Set<StateList> getCycles(Automaton aut)
  
  Returns all cycles in a specified automaton.
  
  Parameters:
  
  aut - an automaton
  
  Returns:
  
  all cycles in aut
- getCycles
  
  public static java.util.Set<StateList> getCycles(Automaton aut, StateSet area)
  
  Returns all cycles restricted in a specified area of an automaton.
  
  Parameters:
  
  aut - an automaton
  
  area - an area in the automaton
  
  Returns:
  
  all cycles in the specified area of the automaton
- getCycles
  
  public static java.util.Set<StateList> getCycles(java.util.Collection<StateList> cycles)
  
  Returns all cycles that can be formed by a specified collection of cycles.
  
  Parameters:
  
  cycles - cycles
  
  Returns:
  
  cycles that can be formed by the specified collection of cycles
- getMSCCs
  
  public static java.util.Collection<StateSet> getMSCCs(Automaton aut)
  
  Returns the maximal strongly connected components (MSCCs) of an automaton.
  
  Parameters:
  
  aut - the source automaton where the MSCCs are going to be found
  
  Returns:
  
  the set of MSCCs
- getPath
  
  public static StateList getPath(Automaton aut, StateSet set, State p, State q)
  Returns a non-empty path in an automaton from a state p to another state q through states in a specified set. There is a non-empty path from (p to q) if either
  
  there is a transition from p to q, or
  
  there is some other state r such that there are a non-empty path from p to r and a non-empty path from r to q.
  Parameters:
  
  aut - an automaton to be checked
  
  set - a state set restricting the path
  
  p - the source state of the path
  
  q - the destination state of the path
  
  Returns:
  
  a path from state p (inclusive) to state q (inclusive) through states in set, or null if there is no such path
- hasPath
  
  public static boolean hasPath(Automaton aut, StateSet set, State p, State q)
  
  Checks if there is a non-empty path in an automaton from a specified state to another specified state through states in a specified set.
  
  Parameters:
  
  aut - an automaton to be checked
  
  set - a state set restricting the path
  
  p - the source state of the path
  
  q - the destination state of the path
  
  Returns:
  
  true if there is a path in aut from p to q through states in set
- hasPath
  
  public static boolean hasPath(Automaton aut, TransitionSet set, State p, State q)
  
  Checks if there is a non-empty path in an automaton from a specified state to another specified state through transitions in a specified set.
  
  Parameters:
  
  aut - an automaton to be checked
  
  set - a transition set restricting the path
  
  p - the source state of the path
  
  q - the destination state of the path
  
  Returns:
  
  true if there is a path in aut from p to q through transitions in set
- isCycle
  
  public static boolean isCycle(Automaton aut, StateSet states)
  
  Returns true if the states in a specified set form a cycle in a specified automaton, that is, for every two states in the set, there is a path from one state to the other state in the automaton through only states in the set.
  
  Parameters:
  
  aut - an automaton
  
  states - a set of states of aut
  
  Returns:
  
  true if the states in the specified set form a cycle in the specified automaton
- isCycle
  
  public static boolean isCycle(Automaton aut, TransitionSet trans)
  
  Returns true if a specified set of transitions form a cycle in a specified automaton. Note that if some transition in the set is not needed to form a cycle, false will be returned.
  
  Parameters:
  
  aut - an automaton
  
  trans - a set of transitions of aut
  
  Returns:
  
  true if the transitions in the specified set form a cycle in the specified automaton
- maximizeAcceptingSet
  
  public static StateSet maximizeAcceptingSet(Automaton aut)
  
  Maximizes the Büchi acceptance condition of an automaton without changing the language of the automaton.
  
  Parameters:
  
  aut - the automaton with a Büchi acceptance condition to be maximized
  
  Returns:
  
  a set of states inserted to the Büchi acceptance condition by this method
- maximizeAcceptingSet2
  
  public static StateSet maximizeAcceptingSet2(AlgorithmListener listener, Automaton aut)
  
  Maximizes the Büchi acceptance condition of an automaton without changing the language of the automaton by finding cycles.
  
  Parameters:
  
  listener - a possibly null algorithm listener that is interested in the progress
  
  aut - an automaton with Büchi acceptance condition to be maximized
  
  Returns:
  
  a set of states inserted to the Büchi acceptance condition by this method
  
  See Also:
  
  ElementaryCycleGenerator
- maximizeAcceptingSet
  
  public static StateSet maximizeAcceptingSet(AlgorithmListener listener, Automaton aut)
  
  Maximizes the Büchi acceptance condition of an automaton without changing the language of the automaton by finding all strongly connected components.
  
  Parameters:
  
  listener - a possibly null algorithm listener that is interested in the progress
  
  aut - an automaton with Büchi acceptance condition to be maximized
  
  Returns:
  
  a set of states inserted to the Büchi acceptance condition by this method
- minimizeAcceptingSet
  
  public static StateSet minimizeAcceptingSet(Automaton aut)
  
  Simplifies the Büchi acceptance condition of an automaton without changing the language of the automaton.
  
  Parameters:
  
  aut - the automaton with a Büchi acceptance condition to be simplified
  
  Returns:
  
  a set of states removed from the Büchi acceptance condition by this method
- minimizeAcceptingSet
  
  public static StateSet minimizeAcceptingSet(AlgorithmListener listener, Automaton aut)
  
  Simplifies the Büchi acceptance condition of an automaton without changing the language of the automaton by finding all strongly connected components.
  
  Parameters:
  
  listener - a possibly null algorithm listener that is interested in the progress
  
  aut - an automaton with Büchi acceptance condition to be simplified
  
  Returns:
  
  a set of states removed from the Büchi acceptance condition by this method
- getAdjacentMatrix
  
  public static boolean[][] getAdjacentMatrix(Automaton aut)
  
  Returns the adjacent matrix m for the states of an automaton. If m[i][j] is true and states are the states returned by aut.getStates(), then states[j] is a successor of states[i] in aut.
  
  Parameters:
  
  aut - an automaton to compute the adjacent matrix
  
  Returns:
  
  the adjacent matrix of the automaton
- empty
  
  public static void empty(Automaton aut)
  
  Makes an automaton accept an empty language by removing all states and transitions except only one non-accepting initial state.
  
  Parameters:
  
  aut - the automaton that wants to accept an empty language
- isConfiguarionLoopAccepting
  
  public static boolean isConfiguarionLoopAccepting(FSA aut, java.util.Collection<Configuration> cfgs)
  
  Returns true if a sequence of configurations forming a loop satisfy the acceptance condition of the automaton.
  
  Parameters:
  
  aut - an automaton
  
  cfgs - a sequence of configurations forming a loop
  
  Returns:
  
  true if the set of configurations forming a loop satisfy the acceptance condition of the automaton
- checkInputSequenceValidity
  
  public static void checkInputSequenceValidity(FSA aut, InputSequence seq) throws java.lang.IllegalArgumentException
  
  Checks if an input sequence is valid for an finite state automaton. Throws an exception with explanation if the input sequence is not valid.
  
  Parameters:
  
  aut - an automaton
  
  seq - an input sequence
  
  Throws:
  
  java.lang.IllegalArgumentException - if the input sequence is invalid for the automaton
- imitateAcceptance
  
  public static void imitateAcceptance(Acc<?> acc1, State s1, Acc<?> acc2, State s2, OmegaUtil.AcceptanceAction action)
  
  Makes a state imitate another state in an acceptance condition.
  
  Parameters:
  
  acc1 - an acceptance condition containing s1
  
  s1 - a state that wants to imitate s2
  
  acc2 - an acceptance condition containing s2
  
  s2 - a state to be imitated
  
  action - action applied in this imitation
  
  Throws:
  
  java.lang.IllegalArgumentException - if the types of the two acceptance conditions are not the same
- imitateAcceptance
  
  public static void imitateAcceptance(Acc<?> acc1, Transition t1, Acc<?> acc2, Transition t2, OmegaUtil.AcceptanceAction action)
  
  Makes a transition imitate another transition in an acceptance condition. For HanoiAcc, only acceptance sets are affected while the Boolean expression on the acceptance sets is unchanged.
  
  Parameters:
  
  acc1 - an acceptance condition containing t1
  
  t1 - a transition that wants to imitate t2
  
  acc2 - an acceptance condition containing t2
  
  t2 - a transition to be imitated
  
  action - action applied in this imitation
  
  Throws:
  
  java.lang.IllegalArgumentException - if the types of the two acceptance conditions are not the same
- hasSameAlphaSuccessors
  
  public static boolean hasSameAlphaSuccessors(Automaton aut, State s, State t)
  
  Returns true if the two specified states have the same α-successors.
  
  Parameters:
  
  aut - an automaton containing the two specified states
  
  s - a state in aut
  
  t - a state in aut
  
  Returns:
  
  true if the two specified states have the same α-successors
- simulate
  
  public static TransitionSet simulate(Automaton aut, State s, State t)
  
  Make a specified state s simulate another specified state t by adding transitions with symbol sym from s to u if there is a transition with the same symbol from t to u. If the automaton is a classic finite state automaton and t is accepting, then s will be made accepting.
  
  Parameters:
  
  aut - an automaton containing the specified states
  
  s - a state that simulates t
  
  t - a state simulated by s
  
  Returns:
  
  the transitions created by this method
- omega
  
  public static FSA omega(FSA aut)
  
  Returns an NBW that accepts L^ω where L is the language accepted by a specified NFW.
  
  Parameters:
  
  aut - an NFW
  
  Returns:
  
  an NBW that accepts L^ω where L is the language accepted by aut
  
  Throws:
  
  java.lang.IllegalArgumentException - if aut is not an NFW
- star
  
  public static FSA star(FSA aut)
  
  Returns an NFW that accepts L* where L is the language of a specified NFW. The input automaton will not be modified. Unlike Closure.closure(org.svvrl.goal.core.aut.fsa.FSA), this method will not introduce ε-transitions.
  
  Parameters:
  
  aut - an NFW
  
  Returns:
  
  an NFW that accepts L* where L is the language of aut
  
  Throws:
  
  java.lang.IllegalArgumentException - if aut is not an NFW
- reduceNotReachedFrom
  
  public static void reduceNotReachedFrom(Automaton aut, State s)
  
  Removes all states that cannot be reached by a specified state.
  
  Parameters:
  
  aut - an automaton
  
  s - a state of the automaton
- reduceNotLeadTo
  
  public static void reduceNotLeadTo(Automaton aut, State s)
  
  Removes all states that cannot reach a specified state.
  
  Parameters:
  
  aut - an automaton
  
  s - a state of the automaton
- eliminateEpsilonTransitions
  
  public static void eliminateEpsilonTransitions(FSA aut)
  
  Eliminates ε-transitions of a classic finite state automaton with a classical alphabet. Do nothing if the input automaton is not a classic finite state automaton or its alphabet is not classical.
  
  Parameters:
  
  aut - a classic finite state automaton with a classical alphabet
- hasEpsilonTransition
  
  public static boolean hasEpsilonTransition(Automaton aut)
  
  Returns true if a specified automaton has ε-transitions.
  
  Parameters:
  
  aut - an automaton
  
  Returns:
  
  true if the specified automaton has ε-transitions
- expandWithEpsilon
  
  public static java.util.List<StateRun> expandWithEpsilon(FSA aut, StateRun run)
  
  Returns a list of state runs obtained by expanding a specified state run with ε-transitions.
  
  Parameters:
  
  aut - the automaton containing the state run run
  
  run - a state run
  
  Returns:
  
  a list of state runs obtained by expanding run with ε-transitions
- expandWithEpsilon
  
  public static void expandWithEpsilon(FSA aut, java.util.List<StateRun> runs)
  
  Expands a specified list of state runs with ε-transitions.
  
  Parameters:
  
  aut - an automaton containing the specified state runs
  
  runs - a list of state runs to be expanded
- hasSameAlphabet
  
  public static boolean hasSameAlphabet(Automaton aut1, Automaton aut2)
  
  Returns true if two automata have the same alphabet type and the same alphabet.
  
  Parameters:
  
  aut1 - an automaton
  
  aut2 - an automaton
  
  Returns:
  
  true if the two automata have the same alphabet type and the same alphabet
- hasSameAlphaSuccessors
  
  public static boolean hasSameAlphaSuccessors(State si, State sj)
  
  Returns true if there is a transition (si, a, sk) if and only if there is a transition (sj, a, sk) for all symbol a and state sk.
  
  Parameters:
  
  si - a state
  
  sj - a state
  
  Returns:
  
  true if the two states have the same α-successors.
- hasSameAlphaPredecessors
  
  public static boolean hasSameAlphaPredecessors(State si, State sj)
  
  Returns true if there is a transition (sk, a, si) if and only if there is a transition (sk, a, sj) for all symbol a and state sk.
  
  Parameters:
  
  si - a state
  
  sj - a state
  
  Returns:
  
  true if the two states have the same α-predecessors.
- copyInTransitions
  
  public static void copyInTransitions(State si, State sj, OmegaUtil.AcceptanceAction action)
  
  Copies incoming transitions of a specified state to another specified state.
  
  Parameters:
  
  si - the destination state of transitions to be copied
  
  sj - the destination state of copied transitions
  
  action - action applied in acceptance imitation
- copyOutTransitions
  
  public static void copyOutTransitions(State si, State sj, OmegaUtil.AcceptanceAction action)
  
  Copies outgoing transitions of a specified state to another specified state.
  
  Parameters:
  
  si - the source state of transitions to be copied
  
  sj - the source state of copied transitions
  
  action - action applied in acceptance imitation
- makeTransitionComplete
  
  public static void makeTransitionComplete(Automaton aut)
  
  Makes the transition relation complete by adding a sink state.
  
  Parameters:
  
  aut - an automaton with transition relation to be made complete
- getTransitionsInArea
  
  public static TransitionSet getTransitionsInArea(Automaton aut, java.util.Collection<State> area)
  
  Returns the transitions in an area of an automaton.
  
  Parameters:
  
  aut - an automaton
  
  area - an area of the automaton
  
  Returns:
  
  the transitions in the area of the automaton.
- getTransitionsInCycle
  
  public static TransitionSet getTransitionsInCycle(Automaton aut, StateList cycle)
  
  Returns the transitions in a cycle of an automaton.
  
  Parameters:
  
  aut - an automaton
  
  cycle - a cycle of the automaton
  
  Returns:
  
  the transitions in the cycle of the automaton.
- getMaxParity
  
  public static int getMaxParity(ParityAcc acc, StateSet states)
  
  Returns the maximum parity among a set of states.
  
  Parameters:
  
  acc - a parity condition
  
  states - a set of states
  
  Returns:
  
  the maximum parity among a set of states, or 0 if the set is empty
- getMinParity
  
  public static int getMinParity(ParityAcc acc, StateSet states)
  
  Returns the minimum parity among a set of states.
  
  Parameters:
  
  acc - a parity condition
  
  states - a set of states
  
  Returns:
  
  the minimum parity among a set of states, or 0 if the set is empty
- getStateParityMap
  
  public static java.util.SortedMap<java.lang.Integer,StateSet> getStateParityMap(ParityAcc acc, StateSet states)
  
  Returns a map from a parity to states, among a specified set of states, that have the parity.
  
  Parameters:
  
  acc - a parity condition
  
  states - a set of states
  
  Returns:
  
  a map from a parity to states that have the parity
- isMSCCAccepting
  
  public static boolean isMSCCAccepting(Automaton aut, StateSet mscc)
  
  Returns true if a maximal strongly connected component (MSCC) is accepting. For a classic finite state automaton, a MSCC is accepting if it contains some accepting state. For an ω-automaton, a MSCC is accepting if it contains some accepting cycle. If the input MSCC contains only one state and the state does not have a self-loop, false will be returned.
  
  Parameters:
  
  aut - an automaton
  
  mscc - a maximal strongly connected component in the automaton
  
  Returns:
  
  true if the maximal strongly connected component (MSCC) is accepting
- merge
  
  public static <T extends Automaton> T merge(T aut1, T aut2)
  
  Merges two automata with the same alphabet type, label position, and type of acceptance condition. The state IDs of the two input automata will be reordered such that the state ID of the first automaton starts from 0 and the state ID of the second automaton starts from the state size of the first automaton. The initial states and the accepting states will also be merged.
  
  Type Parameters:
  
  T - the type of the automata
  
  Parameters:
  
  aut1 - the first automaton
  
  aut2 - the second automaton
  
  Returns:
  
  the automaton obtained by merging aut1 and aut2
  
  Throws:
  
  java.lang.IllegalArgumentException - if the two input automata have difference alphabet types, label positions, or types of acceptance condition
- paste
  
  public static <T extends Automaton> java.util.Map<State,State> paste(T aut1, T aut2, boolean keep_init, boolean keep_acc)
  
  Paste an automaton onto another automaton. The initial and accepting states of the automaton to be pasted may be kept.
  
  Type Parameters:
  
  T - the type of the automata
  
  Parameters:
  
  aut1 - the automaton to be pasted
  
  aut2 - the target automaton
  
  keep_init - true such that initial states of aut1 remain initial in aut2
  
  keep_acc - true such that accepting states of aut1 remain accepting in aut2
  
  Returns:
  
  a map from a state in aut1 to its corresponding state in aut2
  
  Throws:
  
  java.lang.IllegalArgumentException - if the two input automata have difference alphabet types or label positions
- paste
  
  public static <T extends Automaton> java.util.Map<State,State> paste(T aut1, StateSet states, T aut2, boolean keep_init, boolean keep_acc)
  
  Paste states of an automaton onto another automaton.
  
  Type Parameters:
  
  T - the type of the automata
  
  Parameters:
  
  aut1 - the automaton containing the state to be pasted
  
  states - the states to be pasted
  
  aut2 - the target automaton
  
  keep_init - true such that initial states of aut1 remain initial in aut2
  
  keep_acc - true such that accepting states of aut1 remain accepting in aut2
  
  Returns:
  
  a map from a state in aut1 to its corresponding state in aut2
  
  Throws:
  
  java.lang.IllegalArgumentException - if the two input automata have difference alphabet types or label positions
- expandEmptyAlphabet
  
  public static boolean expandEmptyAlphabet(Automaton aut)
  
  Expands the alphabet of an automaton by adding a new proposition if the alphabet is empty.
  
  Parameters:
  
  aut - an automaton
  
  Returns:
  
  true if the original alphabet of the automaton is empty
- contractEmptyAlphabet
  
  public static void contractEmptyAlphabet(Automaton aut)
  
  Removes the inserted proposition by the method #expandEmptyAlphabet(Automaton).
  
  Parameters:
  
  aut - an automaton with alphabet expaneded by the method #expandEmptyAlphabet(Automaton)
- getMaxNonemptyParity
  
  public static int getMaxNonemptyParity(ParityAcc acc)
  
  Returns the maximum non-empty parity.
  
  Parameters:
  
  acc - a parity condition
  
  Returns:
  
  the maximum non-empty parity in the parity condition, or 0 if the parity condition is empty
- getSubgraph
  
  public static <T extends Automaton> T getSubgraph(T aut, StateSet set)
  
  Returns a subgraph of an automaton.
  
  Type Parameters:
  
  T - the type of the automaton
  
  Parameters:
  
  aut - an automaton
  
  set - a set of states in the automaton
  
  Returns:
  
  the subgraph of the automaton constructed from the set of states
- isTriviallyUniversal
  
  public static boolean isTriviallyUniversal(FSA aut)
  Returns true if an automaton is trivally universal. If the automaton has labels on transitions, it is trivally universal if
  
  the automaton has only one state s,
  
  s is an initial state,
  
  s has transitions with all the symbols in the alphabet back to itself, and
  
  the run s^ω is an accepting run.
  
  If the automaton has labels on states and a propositional alphabet, it is trivally universal if
  
  the automaton has only one state s,
  
  s is an initial state,
  
  the label of s is True,
  
  s has a transition back to itself, and
  
  the run s^ω is an accepting run.
  
  If the automaton has labels on states and a classic alphabet, it is trivally universal if
  
  the automaton has only one state s,
  
  s is an initial state,
  
  the label of s is True,
  
  s has a transition back to itself, and
  
  the run s^ω is an accepting run.
  
  Currently, only automata with acceptance conditions on states are supported.
  Parameters:
  
  aut - an automaton with an acceptance condition on states
  
  Returns:
  
  true if the automaton is trivally universal
- isTriviallyEmpty
  
  public static boolean isTriviallyEmpty(FSA aut)
  Returns true if an automaton is trivally empty, that is,
  
  the automaton has at most one state, and
  
  the automaton has no transition.
  Parameters:
  
  aut - an automaton
  
  Returns:
  
  true if the automaton is trivally empty

Class OmegaUtil

Nested Class Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Constructor Details

Method Details