Add statuses to nodes: a status is a special kind of label that is
used to define Petri nets compositions a la Petri Box Calculus. See
plugin ops to read more about how statuses are used in practice.
Several status are defined by default: entry, internal, exit,
buffer, safebuffer for places and tick for transitions.
Internally, a status is an instance of class Status or one of its
subclasses that is identified by a name and an optional value. For
instance the plugin defines:
entry = Status('entry')
exit = Status('exit')
internal = Status('internal')
The second parameter is omitted which means that there is no value for
these status. Buffer places have both a name and a value for their
status: the name is 'buffer' and the value is used as the name of
the buffer.
Status can be added to nodes either when they are created or when they are added to the net:
>>> import snakes.plugins
>>> snakes.plugins.load('status', 'snakes.nets', 'nets')
<module ...>
>>> from nets import *
>>> n = PetriNet('N')
>>> n.add_place(Place('p1'), status=entry)
>>> n.place('p1')
Place('p1', MultiSet([]), tAll, status=Status('entry'))
>>> n.add_place(Place('p2', status=exit))
>>> n.place('p2')
Place('p2', MultiSet([]), tAll, status=Status('exit'))
Class Status
class Status (object) :
The status of a node
Method Status.__init__
def __init__ (self, name, value=None) :
Initialize with a status name and an optional value
Call API
str name: the name of the statushashable value: an optional additional value to make a difference between status with te same name
Class Buffer
class Buffer (Status) :
Status for buffer places, it can be used to merge all the nodes with the same buffer name. For example:
>>> import snakes.plugins
>>> snakes.plugins.load('status', 'snakes.nets', 'nets')
<module ...>
>>> from nets import *
>>> n = PetriNet('N')
>>> n.add_place(Place('p3', range(2), status=buffer('buf')))
>>> n.add_place(Place('p4', range(3), status=buffer('buf')))
>>> n.status.merge(buffer('buf'), 'b')
>>> p = n.place('b')
>>> p
Place('b', MultiSet([...]), tAll, status=Buffer('buffer','buf'))
>>> p.tokens == MultiSet([0, 0, 1, 1, 2])
True
Function buffer
def buffer (name) :
Generate a buffer status called name
>>> buffer('foo')
Buffer('buffer','foo')
Call API
str name: the name of the bufferreturn Buffer:Buffer('buffer', name)
Class Safebuffer
class Safebuffer (Buffer) :
A status for safe buffers (ie, variables) places. The only
difference with Buffer status is that when buffer places with
SafeBuffer status are merged, they must have all the same
marking which also becomes the marking of the resulting place
(instead of adding the markings of the merged places).
>>> import snakes.plugins
>>> snakes.plugins.load('status', 'snakes.nets', 'nets')
<module ...>
>>> from nets import *
>>> n = PetriNet('N')
>>> var = safebuffer('var')
>>> n.add_place(Place('p5', [1], status=var))
>>> n.add_place(Place('p6', [1], status=var))
>>> n.add_place(Place('p7', [1], status=var))
>>> n.status.merge(var, 'v')
>>> n.place('v')
Place('v', MultiSet([1]), tAll, status=Safebuffer('safebuffer','var'))
>>> n.add_place(Place('p8', [3], status=var))
>>> n.status.merge(var, 'vv')
Traceback (most recent call last):
...
ConstraintError: incompatible markings
Function safebuffer
def safebuffer (name) :
Generate a safebuffer status called name
>>> safebuffer('foo')
Safebuffer('safebuffer','foo')
Call API
str name: the name of the safebufferreturn Safebuffer:Safebuffer('safebuffer', name)
Class Tick
class Tick (Status) :
A status for tick transition. Ticks are to transitions what
buffers are to places: they allow automatic merging of transitions
with the same tick status when nets are composed. This is used to
implement variants of the Petri Box Calculus with causal time.
When transitions are merged, their guards are and-ed.
Function tick
def tick (name) :
Generate a tick status called name
>>> tick('spam')
Tick('tick','spam')
Call API
str name: the name of the tickreturn Tick:Tick('tick', name)
Extensions
Class Place
class Place (module.Place) :
Place is extended to allow status keyword argument in
its constructor, which is later available as status
attribute.
Class Transition
class Transition (module.Transition) :
Transition is extended to allow status keyword argument
in its constructor, which is later available as status
attribute.
Class PetriNet
class PetriNet (module.PetriNet) :
PetriNet is extended to allow status keyword argument
in several of its methods. An attributes status is also
available to allow retreiving nodes (actually their names) by
status or merge all the nodes with a given status.
The exact way how merging is performed depends on the exact
status: for exemple, as seen above, using Buffer or
Safebuffer does not lead to merge place the same way.
>>> import snakes.plugins
>>> snakes.plugins.load('status', 'snakes.nets', 'nets')
<module ...>
>>> from nets import *
>>> n = PetriNet('N')
>>> n.add_place(Place('a', range(2), status=buffer('buf')))
>>> n.add_place(Place('b', range(3), status=buffer('buf')))
>>> n.add_place(Place('c', range(3), status=buffer('spam')))
>>> list(sorted(n.status(buffer('buf'))))
['a', 'b']
>>> n.status.merge(buffer('buf'), 'd')
>>> list(sorted(n.status(buffer('buf'))))
['d']
Note in this example how nodes merged by status are removed
after being merge. This differs from the standard methods
PetriNet.merge_places and PetriNet.merge_transitions that
preserve the merged nodes and only add the new one.
Method PetriNet.add_place
def add_place (self, place, **args) :
Extended with status keyword argument.
Call API
object placeobject args- keyword
status: a status that is given to the node
Method PetriNet.add_transition
def add_transition (self, trans, **args) :
Extended with status keyword argument.
Call API
object transobject args- keyword
status: a status that is given to the node
Method PetriNet.set_status
def set_status (self, node, status) :
Assign a new status to a node.
Call API
str node: the name of the nodeStatus status: a status that is given to the node
Method PetriNet.copy_place
def copy_place (self, source, targets, **args) :
Extended with status keyword argument.
Call API
object sourceobject targetsobject args- keyword
status: a status that is given to the new node
Method PetriNet.copy_transition
def copy_transition (self, source, targets, **args) :
Extended with status keyword argument.
Call API
object sourceobject targetsobject args- keyword
status: a status that is given to the new node
Method PetriNet.merge_places
def merge_places (self, target, sources, **args) :
Extended with status keyword argument.
Call API
object targetobject sourcesobject args- keyword
status: a status that is given to the new node
Method PetriNet.merge_transitions
def merge_transitions (self, target, sources, **args) :
Extended with status keyword argument.
Call API
object targetobject sourcesobject args- keyword
status: a status that is given to the new node