Home       Trees       Indices       Help   
TuLiP
Package tulip :: Package transys :: Module automata
[frames] | no frames]

Module automata

Automata Module

Classes
  FiniteStateAutomaton
Set of sequences described with a graph and a condition.
  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.
  ParityGame
GameGraph equipped with coloring.
Functions
 
dfa2nfa(dfa)
Copy DFA to an NFA, so remove determinism restriction.
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

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 ?)

See Also

tuple2fts

Parameters:
  • S - set of states
  • S0 - set of initial states, must be \subset S
  • Sa - set of accepting states
  • Sigma_or_AP - Sigma = alphabet
  • trans - transition relation, represented by list of triples: 
           [(from_state, to_state, guard), ...]

    where guard \in \Sigma.

  • name (str) - used for file export
Returns: BuchiAutomaton

   Home       Trees       Indices       Help   
TuLiP
Generated by Epydoc 3.0.1 on Sat Nov 19 00:11:17 2016 http://epydoc.sourceforge.net