Type(I(p))=C(p)
MS
^ Var(I(p))=;
9. PortsP isasubsetof the places.
10. TS is a substitutionmappingTS : T *NVPow(PPN)TASSEASSNASSisapartial
mapping from the transitions of N to pairs of net variables and relations of places and port names.
For transition t 2 T let S(t) = t[t. S(t) is called the sockets of t. TS should satisfy, that for all
t 2dom(TS)with TS(t)=(net;R ; ;;), RS(t)PN,that isthe relation isarelation between
the socketsof t andportnames.dom(TS)iscalledthe substitutiontransitions ofN.
u t
Thedenition of TS looks alittleghastly, butwill hopefullybemoreclearafter wehavediscussedthe
threekindsofassignmentsrelatedtoPCPN.
Intuitively,TS relatestoeachsubstitutiontransitionanetvariableandanamingofsockets,andatriple
ofatype,expression,andnetassignment.Givenanetassignment,whichrelatesthenetvariabletoanactual
net,theassignmentsareapplied tothisnetandtherelationisused to\glue"thetwonetstogether.
IntheexamplesweusedtheNET regionstodeneTS(seeFig.12).Thename(afterthecolon)isthenet
variable,andreferstothenetparameterinthePARAMETERSbox.Therelationandthethreeassignments
aredened in the box. Weusetypeto dene typeassignments,expr todene expression assignmentsand
net todene netassignments.Therelationisdened bytheport assignments.Wheneverwereferto anet
variablewhichisnotaparameter,weassumethatthevariablerefersuniquelytoaspecicnet.Wecanthen
thinkof thenetasalreadybeingassigned.
Y NET:N
type T=int expr E=fn x=>x+5 net M=N’
port A=A port B=B B
int A
int
1‘0 PARAMETERS net N:N’SIG net N’:N’’SIG 1‘i
1‘i
Fig.12.ExampleofNET region.
IfweignorePorts and TS foramoment,wecanseethat PCPN looks alot likenonhierarchicalCPN
asdened in[5](Def. 2.5).Wedonothavethesetofcoloursets . InsteadwehavethetypelanguagesT.
Furthermore,CPNasdened in[5]doesnotallowfortypenorexpressionvariables.
variableshavebeenassigned(seeDef.16andDef.12).ThisbehaviouristhesameasforCPN.
Fortransitiont let Var(t) denotethe (binding) variablesof t i.e.,the unionofthe bindingvariables in
theguardof t andthearc expressionsonthe arcswithsource ordestinationin t.Var(t)doesnot include
anyexpressionvariables.
8t2T:Var(t)=fvjv2Var(G(t))_9a2A(t):v2Var( E(a))g
whereA(t) denotesthesetof arcswithsourceordestination int.
ForexpressionE2E andmappingb : Var(E)!E denotebyEhbitheexpressionobtainedbyreplacing
allvariablesinthedomainof b,appearinginE withb(v).This closelymatchesthedenition ofexpression
variablesubstitution,howeverthedierentset ofbrackets[ ]vs.h idistinguishthetwo.
Denition7 (Binding,[5] Def. 2.6).A bindingofatransitiont isafunction b denedonVar(t),such
that
1. 8v2Var(t):b(v)2Type(v)
2. G(t)hbi=true
ByB(t) wedenotethe setof all bindingsfor t. ut
Denition8 ([5] Def. 2.7).A tokenelement isa pair (p;c) where p2P and c2C(p),whilea binding
element isapair (t;b)wheret2T andb2B(t). The setof alltokenelements isdenotedTE whilethe set
of allbinding elementsisdenotedbyBE.
A markingisamulti-setoverTE whilea stepisanon-empty andnitemultisetoverBE. ut
LetE(x;y)denotethe(multi-set)sumofexpressionsonarcsbetweenxandy.Thiswillbewelldened
sincetheseexpressionswillrangeoverthesamemulti-set.Eitherxorymustbeaplace,andtheexpressions
willrangeovertheassociatedcolourset.
8(x;y)2(P T[T P):E(x;y)= X
a2A(x;y) E(a)
whereA(x;y)isthesetofarcsfromx toy.
Denition9 (Enable, [5] Def. 2.8).AstepY is enabledinamarkingM if
8p2P: X
(t;b)2Y
E(p;t)hbiM(p)
Denition10 (Occur, [5] Def. 2.9).WhenastepY isenabledinamarkingM itmay occur, changing
the markingtoanother markingM 0
,denedby
8p2P:M 0
(p)= 0
@
M(p) X
(t;b)2Y
E(p;t)hbi 1
A
+ X
(t;b)2Y
E(t;p)hbi
u t
3.5 Assignments
Wecannowdenehowtoassignvaluesto parameters.
141
T
(P;T;A;N;C 0
;G;E;I;Ports;TS 0
)denotethenetobtainedbyreplacinginN allappearancesoftypevariables
v2dom( )with (v). Then
Substitutingtypesinanetchangesthecolourfunctionandpropagatesthesubstitutiontosubnetsthrough
thetransition substitution function.Typesubstitutionis likelyto change thetypeofvariables. Wedonot
considerthismoreformallysinceitdependsheavilyonthewayType(v)isgiven.
Denition12. For PCPN N = (P;T;A;N;C ;G;E;I;Ports;TS) and expression assignment , we let
) denote the net obtained by replacing in N all appearances of
expressionvariables v2dom() with(v), where
1. G
Expressionsubstitutionchangesthedierentinscriptionfunctions.Again,thesubstitutionispropagated
tosubnetsviatheTS function.
Wemightneedtoputsomerestrictionsontheexpressionsweallowagivenvariabletobesubstitutedfor.
IntheexamplesinSect.2weexplicitlytypedtheexpressionparametersused.Thisisnotexplicitlyrequired
from thedenition,but is used toensurethat all expressionassignmentsusedare legal. Otherrestrictions
might be needed for other inscription languages or for other purposes. We will not consider this further
however.
Beforewedenehowtoapplyanetassignment(Def.17),weneedtodenehowwesubstitutetransitions
withnets(Def. 16),butrstweneedtodene howtofuseplaces:
Denition13 (Place fusion).AplacefusionsetF of aPCPNN =(P;T;A;N;C ;G;E;I;Ports;TS)is
anequivalenceclass partitionof P suchthat
8p
denotes the class ofF containingp. ut
Denition14. ForPCPNN =(P;T;A;N;C ;G;E;I;Ports;TS),andaplacefusionsetF overP,wecan
fuse the placesandgetanet
A placefusioncreatesaplace foreachfusionclassand connectsa(class-)placeandatransitionifthere
isanoriginalplaceintheclass,connectedtothetransition.
Noticethat anyclasscontainingaportitselfbecomesaport.
PCPN N andN
iscalleda port/socketrelation(between N 0
andt). ut
A port/socket relation is a relation between the ports of a net and the sockets of a transition. The
restrictionsto thecolourset andinitialmarkingensuresthatwecanfuseportsandsockets.
Inthefollowingweuse U
i=1;:::;n A
i
tomeanthedisjointunionof sets
Wedeneforeachiafunction in
i
Usingdisjointunionensures,amongotherthings,that wecanhavemorethanoneinstance ofthesame
nets.
Denition16 (Transitionsubstitution).LetN =(P
1
PCPNsuchthatfor allt
i
isaport/socket relationbetween N
i
constructedinthefollowingway:LetN
where A( dom()) denotes the set of arcs connected to any
transition indom()
PN)TASSEASSNASSdenedbyin
i
the relation F asthesmallestequivalence relation satisfyingF(in
i
Thus dened, F will relate all portsrelated toat leastone common socket, andall sockets relatedtoat
leastonecommonport, andthe closureof this.F willbeanequivalencesatisfyingthe propertiesneededfor
afusion set.Thuswecancreatethe net
Inshort, a transition substitution creates copies for each instance of nets, and fuse ports and sockets
relatedbysomeport/socketrelation.
Werelatethe substitutionmapping TS to net assignments in thefollowingway. Wheneverwehave
PCPNN andnetassignmentwecan dene
HereN []
N
isnetN after netassignmentasdenedinDef.17.
Pleasealsonoticetheorderofassignmentsin
.Expressionsubstitutionmustalways
occurafter type substitution, to beable to specify valuesof specic types, andstill obeytype-rulesupon
substitution. Placingnet substitution last ensures that type and expression substitution only takes place
throughthesubstitutionmappings inSub.
Noticethat themapping
denedin thiswaymatchesthemappingfromDef.16.
Intuitively, TS maps substitution transitions to variables while maps variables to nets.
is the
composition thatlinkssubstitution transitionstonets.
Intuitively TS relateseachsubstitution transition to asignature consisting ofthenet variable andthe
namingofthesockets.Thenetassignmentthenrelatesasignaturetoaspecicnet,byassociatingthenet
variablewithanetandnamingtheports.ThisisillustratedinFigure13.Ontheleftweseeasubstitution
transitionwith twosocketspandq.TS mapsthistransition tothevariableN,andrelatesthesocketpto
thenameAandsocket qtothenameB. Thesignatureisdrawnonthedashedline. Ontherightweseea
netwithtwoports.Inthegure mapsvariableN to thisnet,andrelatestheupperport tonameAand
thelowerport tonameB.
canbethoughtofasthecompositionofthearrowsinthegure.