Convert LTL formula to Buchi Automaton using ltl2ba.

Parameters:

• formula (`str(formula)` must be admissible ltl2ba input)

Returns: [`Automaton`]

Buchi automaton whose edges are annotated with Boolean formulas as `str`

Return strong product with given graph.

Reference

http://en.wikipedia.org/wiki/Strong_product_of_graphs nx.algorithms.operators.product.strong_product

Return Cartesian product with given graph.

If u,v are nodes in self and z,w nodes in other, then ((u,v), (z,w) ) is an edge in the Cartesian product of self with other if and only if:

• (u == v) and (z,w) is an edge of other OR
• (u,v) is an edge in self and (z == w)

In system-theoretic terms, the Cartesian product is the interleaving where at each step, only one system/process/player makes a move/executes.

So it is a type of parallel system.

This is an important distinction with the strong_product, because that includes "diagonal" transitions, i.e., two processes executing truly concurrently.

Note that a Cartesian interleaving is different from a strong interleaving, because the latter can skip states and transition directly along the diagonal.

For a model of computation, strong interleaving would accurately model the existence of multiple cores, not just multiple processes executing on a single core.

References

• http://en.wikipedia.org/wiki/Cartesian_product_of_graphs
• networkx.algorithms.operators.product.cartesian_product

Synchronous product between (BA, TS), or (BA1, BA2).

The result is always a L{BuchiAutomaton}:

    - If C{ts_or_ba} is a L{FiniteTransitionSystem} TS,
        then return the synchronous product BA * TS.

        The accepting states of BA * TS are those which
        project on accepting states of BA.

    - If C{ts_or_ba} is a L{BuchiAutomaton} BA2,
        then return the synchronous product BA * BA2.

        The accepting states of BA * BA2 are those which
        project on accepting states of both BA and BA2.

        This definition of accepting set extends
        Def.4.8, p.156 U{[BK08]
        <http://tulip-control.sourceforge.net/doc/bibliography.html#bk08>}
        to NBA.

Synchronous product TS * BA or TS1 * TS2.

Returns a Finite Transition System, because TS is
the first term in the product.

Changing term order, i.e., BA * TS, returns the
synchronous product as a BA.

Caution
=======
This method includes semantics for true\in\Sigma (p.916, U{[BK08]
<http://tulip-control.sourceforge.net/doc/bibliography.html#bk08>}),
so there is a slight overlap with logic grammar.  In other
words, not completely isolated from logics.

See Also
========
L{_ts_ba_sync_prod}

@param ts_or_ba: other with which to take synchronous product
@type ts_or_ba: L{FiniteTransitionSystem} or L{BuchiAutomaton}

@return: self * ts_or_ba
@rtype: L{BuchiAutomaton}

See Also
========
__mul__, async_prod, BuchiAutomaton.sync_prod, tensor_product
Def. 2.42, pp. 75--76 U{[BK08]
<http://tulip-control.sourceforge.net/doc/bibliography.html#bk08>}
Def. 4.62, p.200 U{[BK08]
<http://tulip-control.sourceforge.net/doc/bibliography.html#bk08>}

@param ts_or_ba: system with which to take synchronous product
@type ts_or_ba: L{FiniteTransitionSystem} or L{BuchiAutomaton}

@return: synchronous product C{self} x C{ts_or_ba}
@rtype: L{FiniteTransitionSystem}

Merge two Finite Transition Systems.

States, Initial States, Actions, Atomic Propositions and State labels and Transitions of the second Transition System are merged into the first and take precedence, overwriting existing labeling.

Example

This can be useful to construct systems quickly by creating standard "pieces" using the functions: line_labeled_with, cycle_labeled_with

>>> n = 4
>>> L = n*['p'] # state labeling
>>> ts1 = line_labeled_with(L, n-1)
>>> ts1.plot()
>>>
>>> L = n*['p']
>>> ts2 = cycle_labeled_with(L)
>>> ts2.states.add('s3', ap={'!p'})
>>> ts2.plot()
>>>
>>> ts3 = ts1 +ts2
>>> ts3.transitions.add('s'+str(n-1), 's'+str(n) )
>>> ts3.default_layout = 'circo'
>>> ts3.plot()

See Also

line_labeled_with, cycle_labeled_with

Parameters:

• other (FiniteTransitionSystem) - system to merge with

Returns: FiniteTransitionSystem

merge of self with other, union of states, initial states, atomic propositions, actions, edges and labelings, those of other taking precedence over self.

Asynchronous product TS1 x TS2 between FT Systems.

See Also

__or__, sync_prod, cartesian_product Def. 2.18, p.38 [BK08]