Transcript Document

Haskell-Coloured
Petri Nets
Implementation and Applications
(work-in-progress)
IFL'04, Lübeck, Germany, 10 September 2004
Claus Reinke
what to take home
1. Petri nets are well worth looking into
•
many programming language folks are not aware of the huge
and varied developments, in both applications and theory,
since 1960, http://www.daimi.au.dk/PetriNets/
2. high-level Petri nets: a great modelling formalism
•
•
combine nicely with functional inscription languages
are not costly to implement
3. Haskellers can start using them (HCPN)
•
HCPN graphical editor/simulator snapshots available now
http://www.cs.kent.ac.uk/~cr3/HCPN/
4. would be great to see similar support for
•
Clean, Erlang, Curry, ..
Background
Petri nets, basic actions, and composition
(high-level) Petri nets
• Petri nets are a generalisation of finite automata for concurrent
and distributed systems:
– distributed local state
– local state transitions
• places hold multisets of resources,
– marked by anonymous ("black") tokens
• transitions operate on places/tokens (token game, firing rule)
– consume resources from input places
– produce resources on output places
• high-level nets annotate ("colour") tokens with data objects of
some programming language, manipulated by transition
inscriptions in the same language
building net models (building blocks)
• basic actions:
– consumer
– producer
building net models (building blocks)
• basic actions:
– consumer
– producer
• composition: no sharing
– concurrency
building net models (building blocks)
• basic actions:
– consumer
– producer
• composition: no sharing
– concurrency
• composition: sharing resources
– asynchronous/buffered communication/causal dependency
– conflict (sharing)
building net models (building blocks)
• basic actions:
– consumer
– producer
• composition: no sharing
– concurrency
• composition: sharing resources
– asynchronous/buffered communication/causal dependency
– conflict (sharing)
• composition: sharing transitions
– guarded transitions
– synchronisation;
synchronous/unbuffered communication
a trivial example
mutual exlusive access to shared resource,
as a plain Petri net
critical region – stage 1
(mutually exclusive access to shared resource)
critical region – stage 2
(mutually exclusive access to shared resource)
example: critical region
(mutually exclusive access to shared resource)
high-level nets
here: Haskell-Coloured Petri nets (HCPN)
towards HCPN models
– places have Haskell types, tokens are Haskell data objects
– consumer arcs can be labelled with patterns, transitions with
boolean guards (pattern match failure or false guards disable)
Just a
(a>0)
– producer arcs can be labelled with expressions
1+2
– synchronised actions share input variable environments
Just x
y
"done"
(y/=0) x/y
token game for HCPN
• firing rule for an HCPN transition:
– transition is enabled iff on each input place there is a token
matching the label on the corresponding input arc and the
guard evaluates to True under the bindings introduced by the
pattern matches
– enabled transition fires by consuming the enabling tokens
from its input places and producing tokens on its output
places; the values of the latter tokens are determined by the
expression labels on the corresponding output arcs under the
bindings introduced via the enabling pattern matches
• the transition firing rule is tightly interwoven with
evaluation of Haskell patterns and guards
a slightly less trivial example
starving philosophers,
with plain and coloured nets
philosophers – stage 1
philosophers – stage 2
philosophers – stage 3
example: starving philosophers
philosophers – stage 4
(adding colour)
philosophers – stage 5
(folding structure into colour)
example: folded philosophers
we could fold further, until we're left with one transition/place;
the trick is to find the right balance between structure and colour
implementation
embedding HCPN into Haskell,
graphical editing and simulation
embedding HCPN in Haskell (0)
• implementing a HCPN toolchain requires at least
– graphical editor
– net "token game" simulator
– functional inscription language evaluator
• but we're lazy and have limited resources
– that is too much work (about 3 years?)!
– idea [ifl99]: generate Haskell code from HCPN
– need eval/runtime compilation, loading, and linking, to
integrate generated code into running editing session, but:
Haskell doesn't offer runtime reflection 
embedding HCPN in Haskell (I)
places and markings
• the places of a net form a heterogeneous collection
– maps to a record, with a field for each place
– (may need to revisit this when nets get modular)
• each place marking is a homogeneous multiset
– use lists for now
– (probably inefficient for large markings; revisit then)
• so the places of a net map to a record type, and net
markings map to records of this type, nice and simple:
data Mark = Mark { place_n :: [type_of_place_n] }
mark = Mark { place_n = [initial_marking_of_place_n]}
embedding HCPN in Haskell (II)
transitions, arc labels, guards
a
Just x
b
y
t "done"
(y/=0) x/y
t :: Mark -> [Mark]
t m = do
(Just x,a_rest) <- select (a m)
(y,b_rest) <- select (b m)
if (y/=0)
then return m{a = a_rest
,b = b_rest
,c = ("done"):(c m)
,d = (x/y):(d m) }
else fail "guard failed"
c
d
embedding HCPN in Haskell (III)
whole net and simulation loop
net_declarations
data Mark = Mark { place_n :: [type_of_place_n] }
mark = Mark { place_n = [initial_marking_of_place_n]}
t_n :: Mark -> [Mark]
net = Net{ Trans{name="t_n",action=t_n} }
main = run net mark
run net marking = print marking >>
if null enabledTs
then putStrLn "no more enabled transitions!"
else do trans <- choose enabledTs
putStrLn (fst $ fst trans)
run net (snd trans)
where
enabledTs = enabled net marking
embedding HCPN in Haskell (IV)
graphics
• nowadays, Haskell has (once again..) GUI libs [chose wxHaskell]
• build graphical net editor and Haskell code exporter [done]
• invert simulation loop (drive it by timer events so it can be
slowed down to a visible 2 steps/sec) [done]
• interface simulation loop to graphics [done]
– load and display net graphics
– map transition and place names to node ids in loaded net
– generate showMarking function that updates marking
• compilation&loading of generated code from editor
[in progress; "works" now, but we're hoping for improved lib/comp support]
– interpret error messages in terms of source net!
poor man's runtime reflection
NEd.hs
compile
NEd
generate
Net.hs
NSim
load
compile
Net
poor man's runtime reflection
NEd.hs
compile
NEd
save
Net.hcpn
generate
Net.hs
start&control
compile&load
GHCI
run
load
NSim
Net
experience so far..
• Petri nets and Haskell combine nicely
– (Haskell is good for abstract languages/machines and Petri nets are great
for concurrency concepts) could now use Haskell, e.g., in OS lectures
instead of just compiler lectures, or in concurrent system design!
• HCPN now have initial tool support
– graphical editing, code export, graphical simulation – you can use them!
– original estimate was 2 weeks for editor and simulator; textual simulation
was only a day, but fiddling with graphics issues and overall design took
longer (lack of recent GUI experience; GUI lib still in development); now
slightly over a month of work;
– lots remains to be done (continued GUI fiddling and bug fixing, but also
support for hierarchical nets & other arc types, state space
generation/exploration, ..)
• programming
– doing practical stuff in Haskell (with GUI) is fun!
– lots of by-hand refactoring (mostly to grow or change design, i.e., for
experimentation and development, not for cleanup!)
– runtime reflection API would be great (in the works)
related work
• Haskell-Coloured Petri Nets [Reinke 1999] are highlevel Petri nets using Haskell as the inscription language
• some related tools (and inscription languages):
–
–
–
–
Design/CPN [Jensen et.al. 1989-2003]: Standard ML
CPN Tools [Jensen et.al. 2003-]: Standard ML
Graph [Schepers et.al. 1988-1992]: Kiel Reduction Language
Genomic Object Net [Matsuno et.al. 2003] : unspecified
functional language (HFPN are a hybrid functional Petri net
formalism, used for representing and simulating bio-pathways)
– Cell Illustrator [Gene Networks Inc. 2003]: commercial
version of GON
embedding a Pi-calculus in HCPN
embedding a Turing machine