Package org.svvrl.goal.core.comp

  • Interface Summary 
    Interface Description
    ComplementConstruction<I extends Automaton,​O extends Automaton>
    A ComplementConstruction object is an implementation of a complementation construction that can complement an automaton into another automaton which accepts the complement language.
  • Class Summary 
    Class Description
    AbstractComplementConstruction<I extends Automaton,​O extends Automaton>
    A ComplementConstruction object is an implementation of a complementation construction that can complement an automaton into another automaton which accepts the complement language.
    AbstractOnTheFlyContainment<T>
    Test if the first NBW A is contained in the second NBW B by constructing the intersection of A and the complement of B incrementally.
    ComplementRepository
    This class provides methods to extend and access the repository of complementation constructions.
    DeterministicComplementConstruction
    This class provides a complementation construction that can complement a deterministic automaton simply by taking the dual of the acceptance condition.
    ProductState<T1,​T2>
    A ProductState is a tuple <s1, s2, i> where s1 is a state in an automaton, s2 is a state in another automaton, and i is an index indicating which acceptance condition should be satisfied next.
  • Exception Summary 
    Exception Description
    NotContainedException
    This exception is thrown if a counterexample in an on-the-fly containment testing is found during a double DFS.