Skip to content

Commit

Permalink
Finished documentation for Petri nets (including math definitions)
Browse files Browse the repository at this point in the history
  • Loading branch information
Simon Johnston committed Aug 29, 2018
1 parent 5cf1195 commit 0ed657f
Show file tree
Hide file tree
Showing 3 changed files with 166 additions and 37 deletions.
73 changes: 50 additions & 23 deletions behavior/petri-net.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,13 @@
; [make-colored-arc
; (-> symbol? symbol? exact-nonnegative-integer?
; (-> arc? (set/c arc?) (values boolean? (listof symbol?))) arc?)]


[petri-net-place-set
(-> petri-net? (set/c symbol?))]

[petri-net-transition-set
(-> petri-net? (set/c symbol?))]

[make-net-execution
(->* (petri-net? (hash/c symbol? (or/c exact-nonnegative-integer? (listof symbol?))))
((-> net-history-event? void?)) net-execution?)]
Expand All @@ -36,7 +42,12 @@
(-> net-execution? net-execution?)]

[net-execution-complete?
(-> net-execution? boolean?)])
(-> net-execution? boolean?)]

[token symbol?]

[tokens
(-> exact-positive-integer? (listof symbol?))])

(except-out
(struct-out petri-net)
Expand Down Expand Up @@ -69,16 +80,17 @@
(struct petri-net
(name
colored?
places ; (or/c (set/c symbol?) (hash/c symbol? symbol?))
transitions ; (set/c symbol?)
places ; (or/c (listof symbol?) (hash/c symbol? symbol?))
transitions ; (listof symbol?)
arc-set ; (set/c arc)
arcs-from ; (hash/c symbol? arc)
arcs-to) ; (hash/c symbol? arc)
#:constructor-name private-petri-net)

(struct arc
(from
to
threshold ; 0 = inhibitor
(source
target
multiplicity ; 0 = inhibitor
expression)
#:constructor-name private-arc)

Expand All @@ -98,6 +110,9 @@

(define token (gensym))

(define (tokens count)
(make-list count token))

;; ---------- Implementation - Definition

(define (make-petri-net name places transitions arcs #:inhibitors? [inhibitors? #f])
Expand All @@ -112,6 +127,14 @@
(define (make-colored-arc from to threshold expression)
(private-arc from to threshold expression))

(define (petri-net-place-set net)
(if (petri-net-colored? net)
(hash-keys (petri-net-places net))
(list->set (petri-net-places net))))

(define (petri-net-transition-set net)
(list->set (petri-net-transitions)))

;; ---------- Implementation - Execution

(define (make-net-execution net configuration [reporter #f])
Expand All @@ -134,7 +157,7 @@
[(exact-nonnegative-integer? value)
(hash-set! initial-configuration place (make-list value token))])
(raise-argument-error 'make-net-execution
"Specified place is not a valid place in this net"
"Specified place name is not a valid place in this net"
place)))
(private-net-execution net
initial-configuration
Expand Down Expand Up @@ -166,8 +189,11 @@

(define (enabled? exec transition)
(for/and ([arc (hash-ref (petri-net-arcs-to (net-execution-model exec)) transition)])
(define token-count (length (hash-ref (net-execution-place-tokens exec) (arc-from arc))))
(>= token-count (arc-threshold arc))))
(if (= (arc-multiplicity arc) 0)
#f ; inhibitor
(let ([token-count (length (hash-ref (net-execution-place-tokens exec)
(arc-source arc)))])
(>= token-count (arc-multiplicity arc))))))

(define (enabled-transitions exec)
(shuffle (filter (λ (t) (enabled? exec t))
Expand All @@ -176,18 +202,18 @@
(define (fire-transition exec transition)
(for ([arc (hash-ref (petri-net-arcs-to (net-execution-model exec))
transition)])
(define tokens (hash-ref (net-execution-place-tokens exec) (arc-from arc)))
(define tokens (hash-ref (net-execution-place-tokens exec) (arc-source arc)))
(hash-set! (net-execution-place-tokens exec)
(arc-from arc)
(list-tail tokens (arc-threshold arc)))
(report-place-emits exec (arc-from arc) (take tokens (arc-threshold arc))))
(arc-source arc)
(list-tail tokens (arc-multiplicity arc)))
(report-place-emits exec (arc-source arc) (take tokens (arc-multiplicity arc))))
(report-transition-firing exec transition)
(for ([arc (hash-ref (petri-net-arcs-from (net-execution-model exec)) transition)])
(define tokens (hash-ref (net-execution-place-tokens exec) (arc-to arc)))
(define tokens (hash-ref (net-execution-place-tokens exec) (arc-target arc)))
(hash-set! (net-execution-place-tokens exec)
(arc-to arc)
(append tokens (make-list (arc-threshold arc) token)))
(report-place-consumes exec (arc-to arc) (make-list (arc-threshold arc) token))))
(arc-target arc)
(append tokens (make-list (arc-multiplicity arc) token)))
(report-place-consumes exec (arc-target arc) (make-list (arc-multiplicity arc) token))))


(define (evaluate-colored-transition exec transition arc)
Expand All @@ -203,14 +229,14 @@
(define arc-list (set->list arcs))
(when (false? inhibitors?)
(begin
(define inhibited (filter (λ (arc) (= (arc-threshold arc) 0)) arc-list))
(define inhibited (filter (λ (arc) (= (arc-multiplicity arc) 0)) arc-list))
(when (> (length inhibited) 0)
(raise-argument-error who
"Inhibited arcs not allowed without #:inhibitors #t"
(set-intersect places transitions)))))
(define place-names (if colored? (hash-keys places) places))
(define bad-arcs (filter (λ (arc) (not (xor (set-member? place-names (arc-from arc))
(set-member? place-names (arc-to arc)))))
(define bad-arcs (filter (λ (arc) (not (xor (set-member? place-names (arc-source arc))
(set-member? place-names (arc-target arc)))))
arc-list))
(when (> (length bad-arcs) 0)
(raise-argument-error who
Expand All @@ -221,9 +247,10 @@
;; ignores colored? hash
(set->list places)
(set->list transitions)
arcs
;; TODO: below is incomplete, ignores multiple arcs to/from same place
(for/hash ([arc arcs]) (values (arc-from arc) (list arc)))
(for/hash ([arc arcs]) (values (arc-to arc) (list arc)))))
(for/hash ([arc arcs]) (values (arc-source arc) (list arc)))
(for/hash ([arc arcs]) (values (arc-target arc) (list arc)))))

(define (report-place-emits exec place tokens)
(when (net-execution-reporter exec)
Expand Down
129 changes: 115 additions & 14 deletions behavior/scribblings/behavior.scrbl
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,17 @@
#lang scribble/manual

@(require racket/sandbox
scribble/core
scribble/eval
scribble-math
behavior/fsm
behavior/markov-chain
behavior/petri-net
behavior/reporter
(for-label racket/contract
(for-label racket/base
racket/contract
racket/logging
racket/set
behavior/fsm
behavior/markov-chain
behavior/petri-net
Expand Down Expand Up @@ -583,7 +587,21 @@ Return a Graphviz representation of the provided chain as a string.
@section[]{Module behavior/petri-net}
@defmodule[behavior/petri-net]

TBD
This module provides the ability to model, and execute, Petri nets. From
@hyperlink["https://en.wikipedia.org/wiki/Petri_net" "Wikipedia"]):

@italic{A Petri net consists of @elem[#:style plain]{places},
@elem[#:style plain]{transitions}, and @elem[#:style plain]{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
@elem[#:style plain]{input places} of the transition; the places to which arcs
run from a transition are called the @elem[#:style plain]{output places} of the
transition.}

According to the same definition "@italic{...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[ #:eval example-eval
(define net (make-petri-net 'first-net
Expand All @@ -601,51 +619,110 @@ TBD
(execute-net exec)
]

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

@(use-mathjax)

@itemlist[
@item{A @italic{net} is a triple @${N=(P,T,F)} where @${P} and @${T}
are disjoint finite sets of @italic{places} and @italic{transitions},
respectively.}
@item{@${F\subset(P \times T) \cup (T \times P)} is a set of @italic{arcs}
(or flow relations).}
@itemlist[
@item{An @racket[arc] @italic{may not} connect a place to a place, or a
transition to a transition.}]
@item{An elementary net is a net of the form @${EN=(N,C)} where @${N}
is a @italic{net} and @${C} is a @italic{configuration}.}
@itemlist[
@item{A @italic{configuration}, @${C}, is such that @${C \subseteq P}.}]
@item{A @italic{Petri net} @${PN=(N,M,W)} extends the elementary net with @${M}
@italic{markings} and @${W} @italic{weights}, or multiplicities.}
@itemlist[
@item{Each @racket[arc] also has a @racket[multiplicity] value that indicates
the number of tokens required from a @racket[source] place, or the
number of tokens provided to a @racket[target] place.}]
@item{The structure @racket[petri-net] and the function
@racket[make-petri-net] correspond to the pair @${NM=(N,W)} or
@italic{network model}.}
@itemlist[
@item{Both places, and transitions, are represented as a @racket[set?]
of @racket[symbol?].}
@item{No symbol may appear in both sets.}]
@item{The structure @racket[net-execution] corresponds to the pair
@${(NM,M_i)} where @${M_i} is the current set of markings across the
network described by @${NM}.}
@item{The function @racket[make-net-execution] creates the pair
@${(NM,M_0)} where an initial; marking @${M_0} is associated with the
network model.}
]


@;{============================================================================}
@subsection[#:tag "petri:types"]{Types and Predicates}

@defstruct*[petri-net
([name symbol?]
[colored? boolean?])]{
[colored? boolean?]
[place-set (set/c symbol?)]
[transition-set (set/c symbol?)]
[arc-set (listof arc?)])]{
The implementation of the Petri net model where @racket[place-set] corresponds to
@${P}, @racket[transition-set] corresponds to @${T}, and @racket[acr-set]
corresponds to @${F}.
}

@defstruct*[arc
([from symbol?]
[to symbol?]
[threshold exact-nonnegative-integer?])]{
([source symbol?]
[target symbol?]
[multiplicity exact-nonnegative-integer?])]{
An arc within the @racket[petri-net] model, note we include the weights from
@${W} as individual @racket[multiplicity] values on each @racket[arc].
}

@defstruct*[net-execution
([model petri-net?]
[place-tokens (hash/c symbol (listof symbol?))])]{
This structure pairs the @racket[model] itself with a hash (from place to a list
of tokens) that represents the current @italic{marking}, @${M_i}, of the execution.
}

@defstruct*[(net-history-event history-event)
([current-execution net-execution?]
[kind symbol?]
[place-or-transition symbol?]
[tokens list?])]{
An event sent to a reporter function (see @secref["Module_behavior_reporter"
#:doc '(lib "behavior/scribblings/behavior.scrbl")]) with details of state changes
in the execution. The value of @racket[kind] will determine the valid values of
the other fields. Currently these values include @racket['emits], @racket['firing],
@racket['consumes], and @racket['completed].
}


@;{============================================================================}
@subsection[#:tag "petri:construction"]{Construction}


@defproc[(make-petri-net
[name symbol?]
[places (set/c symbol?)]
[transitions (set/c symbol?)]
[arcs (set/c arc?)]
[place-set (set/c symbol?)]
[transition-set (set/c symbol?)]
[arc-set (set/c arc?)]
[#:inhibitors? inhibitors? boolean? #f])
petri-net?]{
Construct a new @racket[petri] net using the places, transitions, and arcs
specified. The value of the keyword parameter @racket[inhibitors?] determines
whether the multiplicity of an @racket[arc] may be 0.
}

@defproc[(make-arc
[from symbol?]
[to symbol?]
[threshold exact-nonnegative-integer?])
[source symbol?]
[target symbol?]
[multiplicity exact-nonnegative-integer?])
arc?]{
Construct a new @racket[arc] from @racket[source] to @racket[target] with the
provided @racket[mutiplicity].
}

@;{============================================================================}
Expand All @@ -654,24 +731,48 @@ TBD

@defproc[(make-net-execution
[model petri-net?]
[configuration (hash/c symbol? (or/c exact-nonnegative-integer? (listof symbol?)))]
[configuration (hash/c symbol?
(or/c exact-nonnegative-integer?
(listof symbol?)))]
[reporter (-> net-history-event? void?) #f])
net-execution?]{
Construct a new execution from the provided @racket[petri-net] @italic{model}. The
@racket[configuration] represents the initial, @italic{marking} @${M_0}, marking
of the execution. A @racket[reporter] function can be provided to receive
history events.
}

@defproc[(execute-net
[exec net-execution?])
net-execution?]{
Execute the net (repeating @racket[execute-net-step]) until
@racket[net-execution-complete?].
}

@defproc[(execute-net-step
[exec net-execution?])
net-execution?]{
Select and @italic{fire} an enabled transition, mapping from marking @${M_i}
into mapping @${M_{i+1}}.
}

@defproc[(net-execution-complete?
[exec net-execution?])
boolean?]{
A network is complete if there are no @italic{enabled} transitions.

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

@defthing[token symbol?]{
The default symbol used as a token when constructing a marking.
}

@defproc[(tokens
[count exact-positive-integer?])
(listof symbol?)]{
Construct a list of @racket[count] copies of @racket[token]. This is used
in the construction of initial configurations.
}

@;{============================================================================}
Expand Down
1 change: 1 addition & 0 deletions info.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@
"racket-index"))
(define build-deps '(
"scribble-lib"
"scribble-math"
"racket-doc"
"sandbox-lib"
"cover-coveralls"))

0 comments on commit 0ed657f

Please sign in to comment.