3 Module behavior/petri-net

3 Module behavior/petri-net🔗ℹ

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.

Examples:

> (define net (make-petri-net 'first-net
                              (set 'a 'b)
                              (set 't)
                              (set (make-arc 'a 't 1)
                                   (make-arc 't 'b 1))))
> (define reporter (λ (ev)
                     (displayln
                      (format "~a ~a ~a"
                              (net-history-event-place-or-transition ev)
                              (net-history-event-kind ev)
                              (net-history-event-tokens ev)))))
> (define exec (make-net-execution net (hash 'a 1) reporter))
> (execute-net exec)
a emits (g12089)
t firing ()
b consumes (g12089)
#<net-execution>

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.

3.1 Types and Predicates🔗ℹ

struct
(struct petri-net (name colored? place-set transition-set arc-set))
  name : symbol?
  colored? : boolean?
  place-set : (set/c symbol?)
  transition-set : (set/c symbol?)
  arc-set : (listof arc?)

The implementation of the Petri net model where place-set corresponds to P, transition-set corresponds to T, and acr-set corresponds to F.

struct
(struct arc (source target multiplicity))
  source : symbol?
  target : symbol?
  multiplicity : exact-nonnegative-integer?

An arc within the petri-net model, note we include the weights from W as individual multiplicity values on each arc.

struct
(struct net-execution (model place-tokens))
model : petri-net?
place-tokens : (hash/c symbol (listof symbol?))

This structure pairs the model itself with a hash (from place to a list of tokens) that represents the current marking, M_i, of the execution.

struct
(struct net-history-event history-event ( current-execution
kind
place-or-transition
tokens))
  current-execution : net-execution?
  kind : symbol?
  place-or-transition : symbol?
  tokens : list?

An event sent to a reporter function (see Module behavior/reporter) with details of state changes in the execution. The value of kind will determine the valid values of the other fields. Currently these values include 'emits, 'firing, 'consumes, and 'completed.

3.2 Construction🔗ℹ

procedure
(make-petri-net name
place-set
transition-set
arc-set
[ #:inhibitors? inhibitors?]) → petri-net?
  name : symbol?
  place-set : (set/c symbol?)
  transition-set : (set/c symbol?)
  arc-set : (set/c arc?)
  inhibitors? : boolean? = #f

Construct a new petri net using the places, transitions, and arcs specified. The value of the keyword parameter inhibitors? determines whether the multiplicity of an arc may be 0.

procedure
(make-arc source target multiplicity) → arc?
  source : symbol?
  target : symbol?
  multiplicity : exact-nonnegative-integer?

Construct a new arc from source to target with the provided mutiplicity.

3.3 Execution🔗ℹ

procedure
(make-net-execution model
configuration
[ reporter]) → net-execution?
  model : petri-net?
   configuration :
(hash/c symbol?
        (or/c exact-nonnegative-integer?
              (listof symbol?)))
  reporter : (-> net-history-event? void?) = #f

Construct a new execution from the provided petri-net model. The configuration represents the initial, marking M_0, marking of the execution. A reporter function can be provided to receive history events.

procedure
(execute-net exec) → net-execution?
exec : net-execution?

Execute the net (repeating execute-net-step) until net-execution-complete?.

procedure
(execute-net-step exec) → net-execution?
exec : net-execution?

Select and fire an enabled transition, mapping from marking M_i into mapping M_{i+1}.

procedure
(net-execution-complete? exec) → boolean?
exec : net-execution?

A network is complete if there are no enabled transitions.

\neg \exists t \in T : (\forall p : M_p \geq W_{p,t})

value
token : symbol?

The default symbol used as a token when constructing a marking.

procedure
(tokens count) → (listof symbol?)
count : exact-positive-integer?

Construct a list of count copies of token. This is used in the construction of initial configurations.

1	Module behavior/ fsm
2	Module behavior/ markov-chain
3	Module behavior/ petri-net
4	Module behavior/ reporter