Package owl.automaton.symbolic

Class SymbolicAutomaton<A extends EmersonLeiAcceptance>

java.lang.Object

owl.automaton.symbolic.SymbolicAutomaton<A>

Type Parameters:

A - the acceptance class

public abstract class SymbolicAutomaton<A extends EmersonLeiAcceptance>
extends Object

An automaton over infinite words.

This class provides a symbolic automaton representation.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static interface	SymbolicAutomaton.StateEncoder<S>
static interface	SymbolicAutomaton.StateEncoderFactory
static interface	SymbolicAutomaton.VariableAllocation
static interface	SymbolicAutomaton.VariableAllocator

Constructor Summary

Constructors

Constructor	Description
SymbolicAutomaton()

Method Summary

Modifier and Type	Method	Description
abstract A	acceptance()
abstract List<String>	atomicPropositions()
abstract int	colourOffset()
BddSetFactory	factory()
abstract BddSet	initialStates()
boolean	is(Automaton.Property property)
static <S,A extends EmersonLeiAcceptance> SymbolicAutomaton<A>	of(Automaton<S,? extends A> automaton)
static <S,A extends EmersonLeiAcceptance> SymbolicAutomaton<A>	of(Automaton<S,? extends A> automaton, BddSetFactory factory, List<String> atomicPropositions)
BddSet	predecessors(BddSet statesAndValuation)
abstract Set<Automaton.Property>	properties()
BddSet	reachableStates()
BddSet	successors(BddSet statesAndValuation)
Automaton<ImmutableBitSet,A>	toAutomaton()
abstract BddSet	transitionRelation()
abstract SymbolicAutomaton.VariableAllocation	variableAllocation()

Methods inherited from class java.lang.Object

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

Constructor Detail

SymbolicAutomaton

public SymbolicAutomaton()

Method Detail

atomicPropositions

public abstract List<String> atomicPropositions()

initialStates

public abstract BddSet initialStates()

transitionRelation

public abstract BddSet transitionRelation()

acceptance

public abstract A acceptance()

variableAllocation

public abstract SymbolicAutomaton.VariableAllocation variableAllocation()

properties

public abstract Set<Automaton.Property> properties()

colourOffset

public abstract int colourOffset()

successors

public BddSet successors(BddSet statesAndValuation)

predecessors

public BddSet predecessors(BddSet statesAndValuation)

reachableStates

@Memoized
public BddSet reachableStates()

is

public boolean is(Automaton.Property property)

factory

public BddSetFactory factory()

of

public static <S,A extends EmersonLeiAcceptance> SymbolicAutomaton<A> of(Automaton<S,? extends A> automaton)

of

public static <S,A extends EmersonLeiAcceptance> SymbolicAutomaton<A> of(Automaton<S,? extends A> automaton,
                                                                               BddSetFactory factory,
                                                                               List<String> atomicPropositions)

toAutomaton

@Memoized
public Automaton<ImmutableBitSet,A> toAutomaton()