have uploaded the questions
Simple Protocol Simple Protocol Abstract This is a small toy example describing a simple protocol by which a sender can transfer a number of packets to a receiver. The communication medium may loose packets and packets may overtake each other. Hence, it may be necessary to retransmit packets and to ignore doublets and packets that are out of order. The example illustrates how the results of a lengthy simulation can be recorded for later inspection and analysis. One way is to add “reporting places” and another is to use an output file. The example is a modified version of a timed CP-net presented in Sect. 5.5 of Vol. 2 of the CPN book. Developed and Maintained by: Kurt Jensen, Aarhus University, Denmark (
[email protected]). 2 CPN Model This example describes a simple protocol where a sequence of packets is sent from one site to another via a network where packets may be delayed or lost. We do not claim that the described protocol is optimal (it is not). However, the protocol is interesting enough to deserve a closer investigation, and it is also complex enough for such an investigation to be valuable. The CPN model of the protocol system is shown below. It consists of three parts. The Sender part has two transitions which can Send Packets and (n,p) Send Packet nn k n n Receive Acknow. A INTxDATA (n,p) (n,p) if Ok(s,r) then 1‘(n,p) else empty Transmit Packet SP Ten0 8 D INT Transmit Acknow. n s if Ok(s,r) then 1‘n else empty s B INTxDATA (n,p) k if n=k then k+1 else k if n=k then k+1 else k Receive Packet str if n=k andalso p<>stop then str^p else str NextSend INT 1 Send INTxDATA 1‘(1,"Modellin")++ 1‘(2,"g and An")++ 1‘(3,"alysis b")++ 1‘(4,"y Means")++ 1‘(5,"of Colou")++ 1‘(6,"red Petr")++ 1‘(7,"i Nets##")++ 1‘(8,"########") Received DATA "" NextRec INT 1 C INT SA Ten0 8 NetworkSender Receiver color INT = int; color DATA = string; color INTxDATA= product INT*DATA; var n,k: INT; var p, str: DATA; val stop = ”########”; color Ten0 = int with 0..10; color Ten1 = int with 1..10; var s: Ten0; var r: Ten1; fun Ok(s:Ten0, r:Ten1) = (r<=s); 3="" receive="" acknowledgments.="" the="" network="" part="" has="" two="" transitions="" which="" can="" transmit="" packets="" and="" transmit="" acknowledgments.="" finally,="" the="" receiver="" part="" has="" a="" single="" transition="" which="" can="" receive="" packets="" (and="" send="" acknowledgments).="" the="" interface="" between="" the="" sender="" and="" the="" network="" consists="" of="" the="" places="" a="" and="" d,="" while="" the="" interface="" between="" the="" network="" and="" the="" receiver="" consists="" of="" the="" places="" b="" and="" c.="" the="" packets="" to="" be="" sent="" are="" positioned="" at="" the="" place="" send="" (in="" the="" upper="" left="" corner).="" each="" token="" on="" this="" place="" contains="" a="" packet="" number="" and="" the="" data="" contents="" of="" the="" packet="" (represented="" as="" a="" text="" string).="" the="" place="" next="" send="" contains="" the="" number="" of="" the="" next="" packet="" to="" be="" sent.="" initially="" this="" number="" is="" 1,="" and="" it="" is="" updated="" each="" time="" an="" acknowledgment="" is="" received.="" the="" content="" of="" the="" received="" message="" is="" kept="" at="" the="" place="" received="" (in="" the="" upper="" right="" corner).="" this="" place="" contains="" a="" single="" token="" with="" a="" text="" string="" which="" is="" the="" concatenation="" of="" the="" text="" strings="" contained="" in="" the="" received="" packets="" (ignoring="" the="" contents="" of="" duplicates="" and="" packets="" received="" out="" of="" order).="" initially="" the="" text="" string="" at="" received="" is="" empty,="" i.e.,="" "".="" at="" the="" end="" of="" the="" transmission="" we="" expect="" received="" to="" contain="" the="" text="" string="" "modelling="" and="" analysis="" by="" means="" of="" coloured="" petri="" nets".="" the="" place="" next="" rec="" contains="" the="" number="" of="" the="" next="" packet="" to="" be="" received.="" initially="" this="" number="" is="" 1,="" and="" it="" is="" updated="" each="" time="" a="" packet="" is="" successfully="" received.="" we="" do="" not="" model="" how="" the="" sender="" splits="" a="" message="" into="" a="" sequence="" of="" packets="" or="" how="" the="" receiver="" reassembles="" the="" packets="" into="" a="" message.="" neither="" do="" we="" model="" how="" the="" tokens="" at="" send="" and="" received="" are="" removed="" at="" the="" end="" of="" the="" transmission="" or="" how="" the="" packet="" numbers="" in="" next="" send="" and="" next="" rec="" are="" reset="" to="" 1.="" now="" let="" us="" take="" a="" closer="" look="" at="" the="" five="" different="" transitions="" in="" the="" protocol="" system.="" send="" packet="" sends="" a="" packet="" to="" the="" network="" by="" creating="" a="" copy="" of="" the="" packet="" on="" place="" a.="" the="" number="" in="" next="" send="" specifies="" which="" packet="" to="" send.="" it="" should="" be="" noted="" that="" the="" packet="" is="" not="" removed="" from="" send.="" neither="" is="" the="" counter="" at="" next="" send="" increased.="" the="" reason="" is="" that="" the="" packet="" may="" be="" lost="" and="" hence="" need="" to="" be="" retransmitted.="" our="" protocol="" is="" pessimistic,="" in="" the="" sense="" that="" it="" continues="" to="" repeat="" the="" same="" packet="" –="" until="" it="" gets="" an="" acknowledgment="" telling="" that="" the="" packet="" has="" been="" successfully="" received.="" transmit="" packet="" transmits="" a="" packet="" from="" the="" sender="" site="" of="" the="" network="" to="" the="" receiver="" site="" by="" moving="" the="" corresponding="" token="" from="" a="" to="" b.="" the="" boolean="" expression="" ok(s,r)="" determines="" whether="" the="" packet="" is="" successfully="" transmitted="" or="" lost.="" the="" variable="" r="" will="" be="" bound="" to="" an="" arbitrary="" value="" in="" its="" colour="" set="" (i.e.,="" to="" any="" integer="" between="" 1="" and="" 10).="" cpn="" tools="" makes="" a="" fair="" choice="" between="" the="" 10="" values.="" the="" ok="" function="" returns="" true="" if="" the="" value="" of="" r="" is="" less="" than="" or="" equal="" to="" the="" value="" of="" s.="" this="" means="" that="" the="" probability="" of="" successful="" transmission="" is="" determined="" by="" the="" token="" at="" place="" sp.="" we="" have="" given="" sp="" a="" token="" with="" value="" 8.="" hence="" we="" have="" 80="" %="" chance="" for="" successful="" transmission.="" however,="" it="" is="" easy="" to="" modify="" the="" success="" rate,="" simply="" by="" changing="" the="" token="" value="" at="" sp.="" 4="" receive="" packet="" receives="" a="" packet="" and="" checks="" whether="" the="" packet="" number="" n="" is="" identical="" to="" the="" number="" k="" in="" next="" rec.="" when="" the="" two="" numbers="" match,="" the="" number="" in="" next="" rec="" is="" increased="" by="" 1="" and="" the="" text="" string="" in="" the="" packet="" is="" concatenated="" to="" the="" text="" string="" in="" received="" –="" unless="" it="" is="" stop="########" ,="" which="" by="" convention="" indicates="" end-of-message.="" otherwise,="" the="" packet="" is="" ignored="" and="" the="" number="" in="" next="" rec="" is="" left="" unchanged.="" in="" both="" cases="" an="" acknowledgment="" is="" sent="" containing="" the="" number="" of="" the="" next="" packet="" which="" the="" sender="" should="" send.="" transmit="" acknowledgment="" transmits="" an="" acknowledgment="" from="" the="" receiver="" site="" of="" the="" network="" to="" the="" sender="" site="" by="" moving="" the="" corresponding="" token="" from="" c="" to="" d.="" the="" transition="" works="" in="" a="" similar="" way="" as="" transmit="" packet.="" this="" means="" that="" the="" acknowledgment="" may="" be="" lost,="" with="" a="" probability="" determined="" by="" the="" token="" at="" place="" sa.="" receive="" acknowledgment="" receives="" an="" acknowledgment="" and="" updates="" the="" number="" in="" next="" send="" by="" replacing="" the="" old="" value="" with="" the="" one="" contained="" in="" the="" acknowledgment.="" after="" a="" number="" of="" steps="" the="" cp-net="" may="" have="" reached="" the="" intermediate="" marking="" shown="" below.="" from="" the="" left-hand="" part="" of="" the="" net,="" we="" see="" that="" the="" sender="" is="" sending="" packet="" number="" three.="" we="" also="" see="" that="" three="" copies="" of="" this="" packet="" are="" present="" at="" places="" a="" and="" b.="" from="" the="" right-hand="" part="" of="" the="" net="" we="" see="" that="" the="" intermediate="" marking="" (n,p)="" send="" packet="" nn="" k="" n="" n="" receive="" acknow.="" a="" 2="" 2‘(3,"alysis="" b")="" intxdata="" (n,p)="" (n,p)="" if="" ok(s,r)="" then="" 1‘(n,p)="" else="" empty="" transmit="" packet="" sp="" 1="" 1‘8="" ten0="" 8="" d="" 2="" 2‘4="" int="" transmit="" acknow.="" n="" s="" if="" ok(s,r)="" then="" 1‘n="" else="" empty="" s="" b="" 1="" 1‘(3,"alysis="" b")="" intxdata="" (n,p)="" k="" if="" n="k" then="" k+1="" else="" k="" if="" n="k" then="" k+1="" else="" k="" receive="" packet="" str="" if="" n="k" andalso=""><>stop then str^p else str NextSend 1 1‘3 INT 1 Send 8 1‘(1,"Modellin")++1‘(2,"g and An")++1‘(3,"alysis b")++1‘(4,"y Means")++1‘(5,"of Colou")++1‘(6,"red Petr")++ INTxDATA 1‘(1,"Modellin")++ 1‘(2,"g and An")++ 1‘(3,"alysis b")++ 1‘(4,"y Means")++ 1‘(5,"of Colou")++ 1‘(6,"red Petr")++ 1‘(7,"i Nets##")++ 1‘(8,"########") Received 1 1‘"Modelling and Analysis b" DATA "" NextRec 1 1‘4INT 1 C INT SA 1 1‘8 Ten0 8 NetworkSender Receiver 5 string "Modelling and Analysis b" has been Received. This is the contents of the first three packets and the receiver is now waiting for packet number four. Hence the packets on A and B will be ignored when they reach the receiver. We can also see that two acknowledgments are present at place D. When Receive Acknowledgment occurs, Next Send will be updated to four, and then the sender will start sending packet number four. When the last packet (with "########") is successfully received by the receiver, Next Rec gets the value nine (one larger than the number of packets). This value will (via an acknowledgment) be communicated to the sender, Next Send will be updated to nine, and the sending will stop – because no packet with this number exists. After a few more steps, where the places A, B, C and D are cleared for packets/acknowledgments, the CP-net will reach a dead final marking, which looks as shown below. Even though this protocol is rather simple, it is not that easy to see that it actually works correctly. What happens, for instance, if the “last” acknowledgment gets lost? By making a number of simulations – interactive and automatic – the user can greatly increase his confidence in the protocol. He may also make a proof of correctness by using the occurrence graph tool. For more information about this, see the example: “Simple Protocol for Occurrence Graph”. It is often convenient to be able to record the things that happen during a Final Marking (n,p) Send Packet nn k n n Receive Acknow. A INTxDATA (n,p) (n,p) if Ok(s,r) then 1‘(n,p) else empty Transmit Packet SP 1 1‘8 Ten0 8 D INT Transmit Acknow. n s if Ok(s,r) then 1‘n else empty s B INTxDATA (n,p) k if n=k then k+1 else k if n=k then k+1 else k Receive Packet str if n=k andalso p<>stop then str^p else str NextSend 1 1‘9 INT 1 Send 8 1‘(1,"Modellin")++1‘(2,"g and An")++1‘(3,"alysis b")++1‘(4,"y Means")++1‘(5,"of Colou")++1‘(6,"red Petr")++1‘( INTxDATA 1‘(1,"Modellin")++ 1‘(2,"g and An")++ 1‘(3,"alysis b")++ 1‘(4,"y Means")++ 1‘(5,"of Colou")++ 1‘(6,"red Petr")++ 1‘(7,"i Nets##")++ 1‘(8,"########") Received 1 1‘"Modelling and Analysis by Means of Coloured Petri Nets##" DATA "" NextRec 1 1‘9 INT 1 C INT SA 1 1‘8 Ten0 8 NetworkSender Receiver 6 simulation. This is in particular the case when we perform a fast-forward simulation where we have no chance