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

Module products

Products between automata and transition systems

Classes
  OnTheFlyProductAutomaton
Dynamically extends itself by adding successors.
Functions
ts_ba_sync_prod(transition_system, buchi_automaton)
Construct transition system for the synchronous product TS * BA.
 
find_ba_succ(prev_q, next_s, fts, ba)
 
find_prod_succ(prev_sq, next_s, enabled_ba_trans, product, ba, fts)
 
ba_ts_sync_prod(buchi_automaton, transition_system)
Construct Buchi Automaton equal to synchronous product TS x NBA.
Variables
  logger = logging.getLogger(__name__)
  __package__ = None
hash(x)
Function Details

ts_ba_sync_prod(transition_system, buchi_automaton)

 

Construct transition system for the synchronous product TS * BA.

Def. 4.62, p.200 [BK08]

Erratum

note the erratum: P_{pers}(A) is ^_{q\in F} !q, verified from: http://www-i2.informatik.rwth-aachen.de/~katoen/errata.pdf

See Also

ba_ts_sync_prod, sync_prod

Returns:
(product_ts, persistent_states), where:
  • product_ts is the synchronous product TS * BA
  • persistent_states are those in TS * BA which project on accepting states of BA.

ba_ts_sync_prod(buchi_automaton, transition_system)

 

Construct Buchi Automaton equal to synchronous product TS x NBA.

See Also

ts_ba_sync_prod, sync_prod

Returns:
prod_ba, the product BuchiAutomaton.

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