A plugin to compose nets a la Petri Box Calculus.

Note: this plugin depends on plugins clusters and status that are automatically loaded

Control-flow and buffers places

When this module is used, places are equipped with statuses (see also plugin status that provides this service). We distinguish in particular:

Plugin ops exports these statuses as Python objects:1 entry, internal and exit are instances of class Status while buffer is a function that returns an instance of Buffer (a subclass of Status) when called with a name as its parameter.

Let's define a net with one entry place, one exit place and two buffer places. Note how we use keyword argument status to the place constructor to define the status of the created place:

>>> import snakes.plugins
>>> snakes.plugins.load('ops', 'snakes.nets', 'nets')
<module ...>
>>> from nets import *
>>> basic = PetriNet('basic')
>>> basic.add_place(Place('e', status=entry))
>>> basic.add_place(Place('x', status=exit))
>>> basic.add_transition(Transition('t'))
>>> basic.add_input('e', 't', Value(dot))
>>> basic.add_output('x', 't', Value(dot))
>>> basic.add_place(Place('b1', [1], status=buffer('egg')))
>>> basic.add_place(Place('b2', [2], status=buffer('spam')))
>>> basic.add_input('b1', 't', Variable('x'))
>>> basic.add_output('b2', 't', Expression('x+1'))

The simplest operation is to change buffer names, let's do it on a copy of our net. This operation is called hide because it is basically used to hide a buffer:

>>> n = basic.copy()
>>> n.node('b1').status
Buffer('buffer','egg')
>>> n.hide(buffer('egg'))
>>> n.node('b1').status
Status(None)

As we can see, place b1 now has a dummy status. But hide can accept a second argument and allows to rename a buffer:

>>> n.node('b2').status
Buffer('buffer','spam')
>>> n.hide(buffer('spam'), buffer('ham'))
>>> n.node('b2').status
Buffer('buffer','ham')

A slighlty different way for hiding buffers is to use operator /, which actually constructs a new net, changing the names of every node in the original net to '[.../egg]':

>>> n = basic / 'egg'
>>> n.node('[b1/egg]').status
Buffer('buffer')

As we can see, a buffer hidden using / still has a buffer status but with no name associated. Such an anonymous buffer is treated in a special way as we'll see later on.

The systematic renaming of nodes is something we should get used to before to continue. When one or two nets are constructed through an operation, the nodes of the operand nets are combined in one way or another. For an arbitrary operation A % B, the resulting net will be called '[A.name%B.name]' (if A and B are nets). Whenever a node a from A is combined with a node b from B, the resulting node will be called '[a%b]'. If only one node is copied in the resulting net, it will be called '[a%]' or '[%b]' depending on wher it comes from. This systematic renaming allows to ensure that even if A and B have nodes with the same names, there will be no name clash in the result, while, at the same time allowing users to predict the new name of a node.

Control-flow compositions

Using control-flow places, it becomes possible to build nets by composing smaller nets through control flow operations. Let's start with the sequential composition A & B, basically, its combines the exit places of net A with the entry places of net B, ensuring thus that the resulting net behaves like if we execute A followed by B. In the example below, we use method status of a net to get the places with a given status:

>>> n = basic & basic
>>> n.status(internal)
('[x&e]',)
>>> n.place('[x&e]').pre
{'[t&]': Value(dot)}
>>> n.place('[x&e]').post
{'[&t]': Value(dot)}
>>> n.status(buffer('egg'))
('[b1&b1]',)
>>> n.status(buffer('spam'))
('[b2&b2]',)

We can see that n now has one internal place that is the combination of the exit place of the left copy of basic with the entry place of the right copy of basic. (Hence its name: '[x&e]'.) We can see also how it is connected to the left/right copy of t as its input/output. Last, we can see that buffer places from the two copies of basic have been merged when they have had the same name. This merging won't occur for anonymous buffers. For example, hiding 'spam' in the right net of the sequential composition will result in two buffer places, one still named 'spam' that is the copy of 'b2' from the left operand of &, another that is anonymous and is the copy of '[b2/spam]' (ie, 'b2'after its status was hidden) from the right operand of &.

>>> n = basic & (basic / 'spam')
>>> n.status(buffer('spam'))
('[b2&]',)
>>> n.status(buffer(None))
('[&[b2/spam]]',)

The next operation is the _choice A + B that behave either as A or as B. This is obtained by comining the entry places of both nets one the one hand, and by combining their exit places on the other hand.

>>> n = basic + basic
>>> n.status(entry)
('[e+e]',)
>>> list(sorted(n.place('[e+e]').post.items()))
[('[+t]', Value(dot)), ('[t+]', Value(dot))]
>>> n.status(exit)
('[x+x]',)
>>> list(sorted(n.place('[x+x]').pre.items()))
[('[+t]', Value(dot)), ('[t+]', Value(dot))]

Another operation is the iteration A * B that behaves by executing A repeatedly (including no repetition) followed by one execution of B. This is obtained by combining the entry and exit places of A with the entry place of B.

>>> n = basic * basic
>>> n.status(entry)
('[e,x*e]',)
>>> n.place('[e,x*e]').post
{'[t*]': Value(dot), '[*t]': Value(dot)}
>>> n.place('[e,x*e]').pre
{'[t*]': Value(dot)}

Finally, there is the parallel composition A | B that just executes both nets in parallel. But because of the merging of buffer places, they are able to communicate.

>>> n = basic | basic
>>> n.status(buffer('egg'))
('[b1|b1]',)
>>> n.status(buffer('spam'))
('[b2|b2]',)

Extensions

Essentially, class PetriNet is extended to support the binary operations discussed above.

Class PetriNet

class PetriNet (module.PetriNet) :

Method PetriNet.__or__

def __or__ (self, other) :

Parallel composition

Method PetriNet.__and__

def __and__ (self, other) :

Sequential composition

Method PetriNet.__add__

def __add__ (self, other) :

Choice

Method PetriNet.__mul__

def __mul__ (self, other) :

Iteration

Method PetriNet.hide

def hide (self, old, new=None) :

Status hiding and renaming

Method PetriNet.__div__

def __div__ (self, name) :

Buffer hiding

  1. All these objects are actually defined in plugin status ↩