3Module behavior/petri-net🔗 i

This module provides the ability to model, and execute, Petri nets. From Wikipedia):

A Petri net consists of places, transitions, and arcs. Arcs run from a place to a transition or vice versa, never between places or between transitions. The places from which an arc runs to a transition are called the input places of the transition; the places to which arcs run from a transition are called the output places of the transition.

According to the same definition "...the execution of Petri nets is nondeterministic: when multiple transitions are enabled at the same time, they will fire in any order". To achieve this, at each step in the execution a single random enabled transition is chosen to fire.

The model follows the usual mathematical model for an elementary net, as described below, with the relevant validations.

• A net is a triple N=(P,T,F) where P and T are disjoint finite sets of places and transitions, respectively.

• F\subset(P \times T) \cup (T \times P) is a set of arcs (or flow relations).

• • An arc may not connect a place to a place, or a transition to a transition.

• An elementary net is a net of the form EN=(N,C) where N is a net and C is a configuration.

• • A configuration, C, is such that C \subseteq P.

• A Petri net PN=(N,M,W) extends the elementary net with M markings and W weights, or multiplicities.

• • Each arc also has a multiplicity value that indicates the number of tokens required from a source place, or the number of tokens provided to a target place.

• The structure petri-net and the function make-petri-net correspond to the pair NM=(N,W) or network model.

• • Both places, and transitions, are represented as a set? of symbol? .

  • No symbol may appear in both sets.

• The structure net-execution corresponds to the pair (NM,M_i) where M_i is the current set of markings across the network described by NM.

• The function make-net-execution creates the pair (NM,M_0) where an initial; marking M_0 is associated with the network model.

Initial, but incomplete, support is also provided for Colored Petri nets.