Package tulip :: Package transys :: Module automata

Module automata

Automata Module

Classes
	FiniteStateAutomaton Generic automaton.
	FiniteWordAutomaton Finite-word finite-state automaton.
	OmegaAutomaton
	BuchiAutomaton
	BA Alias to BuchiAutomaton.
	RabinPairs Acceptance pairs for Rabin automaton.
	RabinAutomaton Rabin automaton.
	DRA Deterministic Rabin Automaton.
	StreettAutomaton Omega-automaton with Streett acceptance condition.
	MullerAutomaton Omega-automaton with Muller acceptance condition.
	ParityAutomaton Omega-automaton with Parity acceptance condition.
	ParityGame GameGraph equipped with coloring.

Functions

nfa2dfa()
Determinize NFA using Rabin-Scott subset construction.

dfa2nfa(dfa)
Copy DFA to an NFA, so remove determinism restriction.

ba2dra()
Buchi to Deterministic Rabin Automaton converter.

ba2ltl()
Buchi Automaton to Linear Temporal Logic formula converter.

BuchiAutomaton

tuple2ba(S, S0, Sa, Sigma_or_AP, trans, name='ba', prepend_str=None, atomic_proposition_based=True)
Create a Buchi Automaton from a tuple of fields.

Variables
	logger = `logging.getLogger(__name__)`
	__package__ = `None` hash(x)

Function Details

nfa2dfa()

Determinize NFA using Rabin-Scott subset construction.

UNDER DEVELOPMENT; function signature may change without notice. Calling will result in NotImplementedError.

ba2dra()

Buchi to Deterministic Rabin Automaton converter.

UNDER DEVELOPMENT; function signature may change without notice. Calling will result in NotImplementedError.

ba2ltl()

Buchi Automaton to Linear Temporal Logic formula converter.

UNDER DEVELOPMENT; function signature may change without notice. Calling will result in NotImplementedError.

tuple2ba(S, S0, Sa, Sigma_or_AP, trans, name=`'ba'`, prepend_str=None, atomic_proposition_based=True)

Create a Buchi Automaton from a tuple of fields.

defines Buchi Automaton by a tuple (S, S0, Sa, \Sigma, trans) (maybe replacing \Sigma by AP since it is an AP-based BA ?)

Module automata

nfa2dfa()

ba2dra()

ba2ltl()

tuple2ba(S, S0, Sa, Sigma_or_AP, trans, name='ba', prepend_str=None, atomic_proposition_based=True)

See Also

tuple2ba(S, S0, Sa, Sigma_or_AP, trans, name=`'ba'`, prepend_str=None, atomic_proposition_based=True)