1‘(i+1) 1‘i
1‘i
1‘i updi i
Fig.15.N -Countingtransitionrings.
This particularmodulecontainsonesub-module, which isaninstance ofC,themodulein Fig.14.The
moduleshouldthusbetranslatedintoaSMLstructurewithonesub-structure,correspondingtothemodule
C. By implementing C asa functor, weget a parameterisedstructure in SML, and instantiating the
sub-module ofN isamatterof instantiating theSMLfunctorwith theappropriateparameters,asspecied in
theNET region.
5.1 Translating PCPN modulesinto SML structures
Beforewecandecidehowto translateanetmoduleintoanSML structure,wewill havetodecidehowthe
structure isgoingto interact with thetool usingthemodule. Inthefollowingwewill assumethemodules
aregoingtobeusedinasimulator.Usingthemodulesinothertools,likesayastatespacetool,shouldwork
inasimilarfashion.
Wewillassumethat wehaveasimulatorwhichis responsiblefor schedulingtransitionrings, andone
globalstate.Eachmodulewillhavefunctionsresponsibleforupdatingtheglobalstatewhenaringoccurs,
andforaddingtransitionstotheschedulingqueuewhen needed.
Ingeneralthiswillworkasfollows:Initiallyalltransitionswillbeexamined,andtheenabledtransitions
will beadded totheschedulingqueue.Whenatransitionis scheduled,anenabledbindingelementwill be
chosenrandomly(if suchabindingexists), andthetransition willre andupdatethe state.Changingthe
statewillpossiblyresultinanumberoftransitionsbecomingenabled.Eachcandidateforthiswillbeadded
totheschedulingqueue.Wewilldenotethecombinationoftheselectionofbindingelement,updatingstate,
and schedulingnewcandidates, asanevent. Wewill henceforthreferto theschedulingqueue astheevent
queue.
All the actions associated with an event, can be encapsulated in a function ora record of functions,
storedintheeventqueue.Oncetheinitialeventsareinstalledintheeventqueue,theschedulerwillonlybe
requiredtoselectandexecutethenextevent,ifany.Nofurtherknowledgeofthemodules isrequired.
initialisingthemodule,i.e.,addingallinitialeventstotheeventqueue.Theinitfunctionisalsoresponsible
forinitialisinganysub-modules, bycalling theirinitfunction.
signature PCPN MODULE =
sig
val init:unit >unit
end
Fig.16.SignatureforPCPNmodule
A generalPCPNmoduleasdescribedabovecanthenbetranslatedtoanSMLfunctor oftheformseen
inFig.17.
functor M((*Parameters *)): PCPN MODULE =
structure
(* |Declarations | *)
(* |Code forHandling Events| *)
(* |Sub-modules | *)
(* |Module Initialisation | *)
fun init ()=((* Initialisation code *))
end
Fig.17.TemplateforPCPNmodulefunctor
Thefunctor generated for the module C (in Fig. 14) is shown in Fig. 18. In the gure, only thecode
relatedtoparameterisedmodulesisshown,andthecodeforinteractingwiththesimulatorisomitted.The
interesting part in the gure is the parameter part of the functor. The parameters consists of the type
parameterT,andthetwoportplacesAandB. T isanSMLtypeparameter,whileAandBarestructures
implementingplaces.
WeconstructtheparameterpartofthefunctorfromthePARAMETERS boxofthenet,andwedothisin
averystraightforwardmanner.WetranslatecertainPCPNkeywordsintoSMLkeywords,andinserttherest
verbatimintotheSMLfunctor.Thekeywordsaretranslatedasfollows:port istranslatedto structure,expr
istranslatedtoval,andnet istranslatedtofunctor.Wewillreturntothelattershortly.Thispreprocessingis
donesolelyforallowingPCPNkeywordsindeclarations.WecoulddowithoutitbyusingtheSMLkeywords.
Placesmarkedasportsarealsoinsertedintheparameterpart.Thesearestructureparameterswithsignature
PLACE.
ThelastlineintheparameterpartofthefunctorinFig.18speciesthatthecoloursetoftheportplaces
AandBisthesameastheparametertypeT.Thisisimplicitlyassumedfrom thecoloursetspeciedinthe
netinscriptions.Thelineisneededbecauseweimplementplacesasstructures,eachwithacolourset(type)
C.
Figure19showsthefunctorgeneratedforthemoduleN inFig.15.Ascanbeseen,N takesnoparameters.
InthenetthereisnoPARAMETERSbox,andinthefunctor,theparameterpartisempty.Thereis,however,
aDECLARATIONS boxin the net.The declarations there havebeeninsertedverbatiminto the functor.
The declarations are put at the beginning of the functor, before any code that could possibly need it. In
somecasesit mightbe necessaryto pre-process aDECLARATIONS boxbefore insertingthedeclarations
147
structureB: PLACE
structureA : PLACE
sharing type T =B.C =A.C): PCPN MODULE =
struct
(* <<snippedopen of needed structures>> *)
(* <<snippedcode for handlingevents>> *)
fun init ()=
((*<<snippedcode>> *))
end
Fig.18.FunctorformoduleC.
functor N((* none *)): PCPN MODULE =
struct
(* <<snippedopen ofneeded structures>> *)
(* DECLARATIONS *)
fun updii =1`(i+1)
(* <<snippedcode for handlingevents>> *)
structure Y =C(type T=int structureA=Astructure B=B)
fun init ()=
((*<<snippedcode>> *))
end
Fig.19.FunctorformoduleN.
forthesimulatorweareconsidering.
Noticethesub-modulein Fig.19.ThisissimplyimplementedasanSML structure,createdbyacallto
the appropriatefunctor. In this casethe functor C from Fig.18. The parametersused in the functorcall
arecreatedfromtheNET boxin thesamewayastheparametersforthefunctorC werecreatedfromthe
PARAMETERS box.
InFig.19thefunctorusedtocreatethesub-modulemustbegloballyknown,sinceitisreferredtosimply
byaname.Wewanttobeabletohandlenetparametersinmuchthesameway,butwhereweletthefunctor
used tocreate themodule beaparameterofthefunctor thatcontainsthesub-module. Toimplementthis
wecanusehigherorderfunctorsasimplementedinSML/NJ[1].
Considerthe netin Fig.20, anddenote itM. The functorcreatedforthis netis seenin Fig.21. Here
M takesasargumentafunctorN andcreatesthesub-module Y with thisfunctor.ThefunctorN istyped
withthefunctorsignatureC 0
SIG.ThissignatureiscreatedautomaticallyfromthenetCwesawinFig.14.
ThedenitionofC 0
SIGisshowninFig.22.
Y NET:N
type T=int port A=A port B=B X
B
int A
int
1‘0 PARAMETERS net N:C’SIG
1‘i
1‘i
1‘i 1‘(i+1)
Fig.20.M-Netwithnetparameter.
6 Future work
CPN has powerfuland general methods forboth validation and verication. Validation is concerned with
convincingourselvesthatanetbehavesasintended,whilevericationisconcernedwithproofthatanethas
aformallystatedproperty.TheobviousnextstepforPCPNistoextendthesemethodstohandleparameters.
Thisisnecessaryto beabletoexaminemodulesindependently,and toexploittheunderlyingmodularity.
6.1 Validation
Validation is usually done through simulation.In Sect. 5 we examined how to implement a simulator for
PCPN. The discussion, however, was only concerned with how to translate PCPN into SML code, and
was notconcerned with howto actually simulate the nets. With ourprototype simulator [7] we canonly
simulateinstantiatednets,andwehaveonlydened thebehaviourofnetswithoutfreetypeandexpression
parameters.
Modules, however, are usually self-contained units, and we must expect that modules are primarily
developed independently, thus we should be able to validate modules independently. At least, to as high
a degree as possible. To do this we have to come up with a meaningful denition of the behaviour of a
parameterisednet,andtoolsupportforthis.
6.2 Verication
The primary verication techniques for CPN are state spaces and invariants [6]. Work has been done on
exploitingmodularityin vericationwithbothtechniquesin [3]and[4].
149
toimaginevericationindependentofinstantiation.Symbolicstatespaces,however,couldturnouttomake
thispossiblein somecases.
Invariantsrelyonthestructureofnetsratherthantheinitialmarking,andoersperhapsmorepromise
asavericationtechniquefor PCPN.Type parameterswill notinuence invariantproperties directly,but
willdeterminetheweightfunctions.Expressionandnetparameterswillin generalaectproperties,butby
puttingrestrictionsonthepossiblenetsandexpressionsassigned to parameterswemight beableto prove
certainproperties.
7 Conclusion
In this paper we have formally dened PCPN as CPN with type, expression, and net parameters. We
haveseen how net parameterslead to amodule systemfor PCPN and examined how asimulator can be
implementedsuchthatcodeforseparatemodulescanbegeneratedindependently,andsuchthatinstantiated
netscanbesimulated.
Now, the next stepis to create validation and verication techniques for handling parameterisednets
individually.
Acknowledgements
Thanksto SrenChristensen,BoLindstrm,RegnarB.Lyngs,KjeldH.Mortensen,andLisaWellswhose
discussionandcommentshelpedimprovethispaper.
References
1. Special Features of SML/NJ. WWW online documentation <URL:http://cm.bell-labs.com/cm/cs/wha t/
smlnj/doc/features.html>.
2. SrenChristensenandKjeldH.Mortensen. Parametrisation ofColouredPetriNets. TechnicalReportDAIMI
PB-521,DepartmentofComputerScience,UniversityofAarhus,March1997.
3. SrenChristensenandL.Petrucci. Modularstatespaceanalysisofcolouredpetrinets. InProceedingofthe16th
InternationalConferenceonApplicationandTheory ofPetriNets,Turin,pages201{217,June1995.
4. Sren Christensen and Laure Petrucci. Towards a modularanalysis of coloured petri nets. In Proceeding of
the 13th InternationalConference on Application and Theory of Petri Nets, SheÆeld, UK,volume 616, pages
113{133.Springer-Verlag,June1992.
5. Kurt Jensen. Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use. -Volume 1: Basic
Concepts. Monographsintheoreticalcomputerscience,Springer-Verlag,Berlin,1992.
6. KurtJensen. ColouredPetri Nets-BasicConcepts, AnalysisMethodsandPracticalUse. -Volume2: Analysis
Methods. Monographsintheoreticalcomputerscience,Springer-Verlag,Berlin,1994.
7. Thomas Mailund. A Simulatorfor ParameterizedCPNModules. <URL:http://www.daimi.au.dk/~mailund/
pcpn.html>.
8. Thomas Mailund. FormalDenition ofParameterized CPN. Technical report, Department ofComputer
Sci-ence,UniversityofAarhus,1999.InternalTechnicalReport,<URL:http://www.daimi.au.dk/~mailund/p aper s/
definitions.ps>.
9. R.Milner,M.Tofte,andR.Harper. TheDenitionofStandard ML. MITPress,1990.
10. L.C.Paulson. MLforthe WorkingProgrammer. CambridgeUniversityPress,2ndedition,1996.
struct
(* <<snippedcode>> *)
structure Y =N(type T=int structureA=A structureB=B)
fun init ()=
((*<<snippedcode>> *))
end
Fig.21.FunctorformoduleM.
funsig C'SIG (type T
structure B: PLACE
structure A :PLACE
sharing type T =B.C = A.C)=PCPN MODULE
Fig.22.FunctorsignaturefornetC.