This plugin provides an implementation of the action-based synchronisation from algebras of Petri nets. With respect to the usual definition of synchronisation, the plugin is slightly more general in that it does not impose a fixed arity for action. The extensions are as follows:

Example

Let's start with an example: we build a Petri net with two transitions in parallel that will be synchronised later on.

>>> import snakes.plugins
>>> snakes.plugins.load('synchro', 'snakes.nets', 'nets')
<module ...>
>>> from nets import *
>>> n = PetriNet('N')
>>> n.add_place(Place('e1'))
>>> n.add_place(Place('x1'))
>>> m1 = [Action('a', True, [Variable('x'), Value(2)]),
...       Action('b', True, [Value(3), Variable('y')]),
...       Action('c', False, [Variable('x'), Variable('y')])]
>>> print(', '.join(str(action) for action in m1))
a!(x,2), b!(3,y), c?(x,y)
>>> n.add_transition(Transition('t1', guard=Expression('x!=y'), actions=m1))
>>> n.add_input('e1', 't1', Variable('x'))
>>> n.add_output('x1', 't1', Variable('z'))
>>> n.add_place(Place('e2'))
>>> n.add_place(Place('x2'))
>>> m2 = [Action('a', False, [Variable('w'), Variable('y')]),
...       Action('d', False, [Variable('z')])]
>>> print(', '.join(str(action) for action in m2))
a?(w,y), d?(z)
>>> n.add_transition(Transition('t2', guard=Expression('z>0'), actions=m2))
>>> n.add_input('e2', 't2', Variable('w'))
>>> n.add_output('x2', 't2', Variable('z'))
>>> n.transition('t1').vars() == set(['x', 'y', 'z'])
True

On transition t1, we have put a multiaction that can be abbreviated as a!(x,2), a!(3,y), b?(x,y) and can be interpreted as three synchronous communication performed atomically and simultaneously when t1 fires:

And similarly for transition t2 that has two actions:

Thus, t1 and t2 hold conjugated actions, which are matching emitting and receiving actions a!(x,2) and a?(x,y). So we can synchronise the net on a which builds a new transition whose firing is exactly equivalent to the simultaneous firing of t1 and t2 performing the communications over channel a.

>>> n.synchronise('a')
>>> t = [t for t in n.transition() if t.name not in ('t1', 't2')][0]
>>> print(t.name)
a(w,2)@(t1[x=w,y=e,z=f]+t2[y=2])
>>> print(t.guard)
((w != e)) and ((z > 0))
>>> print(', '.join(sorted(str(action) for action in t.actions)))
b!(3,e), c?(w,e), d?(z)

The second statement t = ... retrieves the new transition then we print its name and guard. The names can be read as: this is the result of execution action a(w,2) on t1 substituted by {x->w, y->e, z->f} and t2 substituted by {y->2}. Indeed, both transitions have variables y and zin common, so they are replaced in t1 to avoid names clashes, then, actions a can be a!(x,2) and a?(w,y) can be matched by considering x=w and y=2 which yields the rest of the substitutions for the transitions. The resulting transition results from the merging of the unified transitions, its guard is the and of the guards of the merged transitions and its multiaction is the union of the multiactions of the merged transitions minus the actions that did synchronise.

The net now has three transitions: t1, t2 and the new one resulting from the synchronisation. This allows both synchronous and asynchronous behaviour:

>>> for t in sorted(t.name for t in n.transition()) :
...     print(t)
a(w,2)@(t1[x=w,y=e,z=f]+t2[y=2])
t1
t2

If we want to force the synchronous behaviour, we have to restrict over 'a' which removes any transition that hold an action a?(...) or a!(...). In practice, this is what we want and so we may have used method n.scope('a') to apply directly the synchronisation followed by the restriction.

>>> n.restrict('a')
>>> for t in sorted(t.name for t in n.transition()) :
...     print(t)
a(w,2)@(t1[x=w,y=e,z=f]+t2[y=2])

Class Action

class Action (object) :

Models one action with a name, a direction (send or receive) and parameters.

Method Action.__init__

def __init__ (self, name, send, params) :

Constructor. The direction is passed as a Boolean: True for a send action, False for a receive.

Call API

Class MultiAction

class MultiAction (object) :

Models a multiset of actions.

Method MultiAction.__init__

def __init__ (self, actions) :

The only restriction when building a multiaction is to avoid putting two conjugated actions in it. Indeed, this may lead to infinite Petri nets upon synchronisation. For example, consider two transitions t1 and t2 with both a?() and a!() in their multiactions. We can synchronise say a?() from t1 with a!() from t2 yielding a transition whose multiaction has a!() from t1 and a?() fromt2and thus can be synchronised witht1ort2, yielding a new transition witha?()anda!()`, etc. Fortunately, it makes little sense to let a transition synchronise with itself, so this situation is simply forbidden.

>>> try : MultiAction([Action('a', True, [Variable('x')]),
...                    Action('a', False, [Value(2)])])
... except ConstraintError : print(sys.exc_info()[1])
conjugated actions in the same multiaction
Call API

Extensions

Class Transition

class Transition (module.Transition) :

Class Transition is extended to allow a keyword argument actions in several of its methods __init__ and copy (to replace a multiaction upon copy).

Class PetriNet

class PetriNet (module.PetriNet) :

Method PetriNet.synchronise

def synchronise (self, name) :

Synchronise the net wrt name.

Call API

Method PetriNet.restrict

def restrict (self, name) :

Restrict the net wrt name.

Call API

Method PetriNet.scope

def scope (self,  name) :

Scope the net wrt name, this is equivalent to apply synchronisation followed by restriction on the same name.

Call API

Method PetriNet.merge_transitions

def merge_transitions (self, target, sources, **args) :

Accepts a keyword parameter actions to change the multiaction of the resulting transition. If actions is not given, the multiaction of the new transition is the sum of the multiactions of the merged transition.

Call API

Method PetriNet.copy_transition

def copy_transition (self, source, targets, **args) :

Accepts a keyword parameter actions to change the multiaction of the resulting transition. If actions is not given, the multiaction of the new transition is the the same multiaction as the copied transition.

Call API