CPNTOOLS举例

1、简单协议 Simple Protocol协议系统的CPN模型如下所示。它包括三个部分。Sender部分有两个变迁，它们能Send Packets （发包） 和 Receive Acknowledgments （收到确认）。Network 部分有两个变迁：Transmit Packets （传送包）和 Transmit Acknowledgments （传送收到确认）。最后，Receiver部分有一个单独的变迁，它能Receive Packets （收到 包）（和发送确认）。Sender和Network之间的接口包括库所A和D, Network和Receiver之间的接口包 括库所B和CoT(1

2、.MModellinH)+ T(Z”g and AnM)+INTxDATA+1(4. y Means )+T(5.n0f Coloif)* r(6.Hred Petr+1,(7/,i Nets?w*I Ft rTTF vTTTTTrT ；Send(n,P)INTxDATA0P)(n?pjINTxDATATransmit f PacketextSenReceive- Ack now.Send PacketTenOTenCSendernINTif Qkfs.r) then 1 *n else emplysmit Ack now.Network。贬).a then r(n?pT_7 else emp

3、tyINT1NextRecf n=k then k else kINTReceivedDATA(UP)Receive Packetif an dalso ptop then strAp else strif n=k then k+1 else kReceivercolor INT = ini;color DATA = string;color INTxDATA= product INT*DATA; var n,k: INT;var p5 str: DATA; val stop = ”料出曲七 color TenO = ini with 0. 10; color Tenl = int with

4、L. 10; var s: TenO; var r: Ten 1;fun Ok(s:Ten09 r:Tenl) = (r1,(2；,gand Ant1X3；,alysisbt1,(4；y MeansttTfS/ofColoul/red Petr)trf(1J，Modellin+ T(2.”g and An”)卄 嗖聖;:区:器獵:+ T(5.MofColou+ 7f(6.Hred PetrM)卄 T(7.Mi Ne 出MIf Sdelling and Analysis by Means of Coloured Petri Nets#O：INTxDATASend Packet(2(n.p；n 1

5、1 QTenO(n.p)回Tra nsriit Packet8INTxDATA ifOkis.r)tf)en (n.pTK/-else emptyNTReceive Acknow. extSenTenOif Okfs.r； then |NT else enpkTra nsmitAckno?v. if n=k then k+1 else kQ回NextRecDATA(n.p)Receive Packetif n=k andalso postop then strp else strceiveStrINTif n=k then k+1 else kSenderNetworkReceiver尽管这个

6、协议是非常简单的，但能明白它在实际中是如何正确地丄作却是不容易的。例如，如果最后 一个确认丢失了，会发生什么？通过大量的仿真一一交互式的和自动化的一一用户可以在通讯中极大 地增强自信。通过使用发生图occurrence graph T具，用户还可以检验正确性。更多信息请见例子“简 单协议的 occurrence graph”。通常，能够记录仿真中发生的事情是非常方便的。特别是我们执行的是一个快进的仿真，没有机会观 察单独步的发生。通过增加大量的“报告库所(reporting places)99,可以实现记录，如：手机有关仿真 运行历史信息的库所一一不影响仿真的运行。报告库所的使用如下所示。为了

7、了解CPN Tools中的报 告库所，我们不得不使用叫做SimpleProtocoLRP的CPN模型。首先，我们增加一些额外的声明：color BOOL = bool;color INTxINT = product INT*INT; color PackSeq = list INTxDATA; vari: INT;var plist: PackSeq;然后，我们给每个变迁增加一个或两个额外的库所。库所SentPack告诉我们已经发送了多少次单独的 包。在本例中，号码1的包被发送了 4次，号码2的包发送了 6次，号码3的包发送了 2次。库所RecAck 告诉我们发送者收到了哪个确认。每个确认被记

8、录为一个对pair,第一个元素是顺序编号，第二个元 素是确认的内容。顺序号从库所Count中获得。本例中，我们首先收到了四个值为2的确认，然后收 到了值为3的确认。Reporting Facilities for the SenderT(t%bdellirT)+T2”g snd AnJ+YPJalysis bj+十(4”y Me3ny)+T(5of Colo)+*(6&ed PetT)+Reporting Facilities for the Networkif Ok(s?r) then empty else Vn INTxDATAT ran smit PacketINTxDATA1l(3:,

9、alysibnifOk(s.r) then 1 *Cn,p else emptyTenOTenO回if Ok(s?r) then VnI NTT ransmit Acknow. else empty-if Ok(s.r) then true eke false回INT1*false8*lrueBOOL库所LostPack告诉我们有关丢失的包。本例中，我们只丢失了一个号码为2的包的拷贝。库所LostAck 告诉我们，我们已经发送/丢失了多少个确认。本例中，我们丢失了一个确认，成功地发送了 8个确认。Reporting Facilities for the Receiver库所RecPack告诉我

10、们有关成功收到的包（从ReceivePacket到RecPack的操作符“连接了两个列表）。 本例中，我们收到了三个包。首先，收到了编号为1的包，有数据Modelling然后收到了编号2的包迄 and AnS最后收到了编号3的包，数据是”alysis bS记录仿真结果的第二个方法是使用代码片段，把选择好的结果写入输出文件中。稍侯，人或另一个计 算机程序（如：电子数据表程序）可以读该文件。为了了解CPN Tools中输出文件（输入文件）的使 用，可以使用叫做“SimpleProtocolJO的CPN模型。我们首先增加一些额外的声明：color INTxDATA = product I NT *

11、DATA; color E = with e;globref packets = empty: INTxDATA ms; globref outfile = TextlO.stdOut;ftjn getPackets()二(Ipackets);预先定义的函数INTxDAT.out把具体表达式的值写入到具体的文件中。表达式必须是INTxDATA类型 （如果表达式是INTxDATA多重集，必须要使用函数INTxDATA.output_ms）o类似地，预先定义的函 数INTxDATA.inpuCms把INTxDATA的多重集从具体的文件中读入（如果想要读出类型INTxDATA 的一个单独的值，必须使

12、用函数INTxDATA.input）o 应该注意的是，叫做packets的变量是一个全局引用变量，它的类型是INTxDATA ms 这说明，必须绑 定INTxDATA的多重集（而不是INTxDATA的单独的值）。变量初始化为空的多重集。全局引用变量 outfile给我们的输出文件提供了操作的句柄。引用变量初始化为TextIO.stdOut （标准的输出），但这随 后被覆盖。接下来，我们给变迁Receive Packet增加一个代码片段：input (n,p,k);actionif n=k then(if n=1 thenoutfile :二 TextlO.openOut(,lSimplePro

13、tocol.SimRes:,) else ();INTxDATA.output(!outfile, (n.p):if p=stop then TextlO.closeOut(loutfile) else ()else ();第一行说明了代码片段的action部分，它用来引用变量n.p和k的值。Action部分检验了收到的包是否 成功（n二k）或失败（nHk）。如果失败，则什么都不做，如果成功，就说明了下面在输出文件上的操作： 当收到了第一个包（n=l）时，打开了输出文件SimpleProtocol.SimRes对每一个成功收到的包，我们使用函数INTxDATA.output,在输出文件上写入值

14、（n,p）（值后面自动 追加一个空格）。当收到最后一个包时（p=stop）,关闭输出文件。仿真后（有8个包），输出文件有下列内容:(lz MMoaellinr/)(2, and An,f)(3, alysis br/)(4,、y Means )(5Z of Colou/r)(6， red Petrr/)(7, viNets#) (8,呻 #)下面要说明如何使用一个输入文件来初始化一个仿真。为此，我们增加一个额外的变迁，叫做Initialise Packets.当仿真开始时，这个变迁从一个具体的文件中读入多重集，给库所S纫增加多重集指定的托 肯，库所的初始值为空。INTxDATA(lr ,T4o

15、dellinH ) + 1 ( 2r ,fg and 尘n )+ +( 3r Lysis bH ) + ( 4 Jy P4eans 11) + + ( 5r lfof Colou11) + red Petr11) + 1 (7f i Nets# ) + +#”)% first oacket% second packet% third packet% fourth uacket% fifth packet% sixth packet% seventh packet % eighth packetactionletval infilesTfextlO.openlnfSimpleP rotoeolJ

16、O.TXT);val message = INTxDATA.i nput_ms(i nfil 前； inpackets := message：T extIO.closel n (infe);()end handl&_ = ();我们使用一个固定的文件名字（和我们对输出文件的操作一样）。首先，读入INTXDATA,将其绑定 到全局引用变量packetso然后，关闭输入文件input file。当计算了弧的注释getPackets（）9将返回packets 的当前值，如，将返回从文件中读入的多重集。如果当读入文件时，输入文件不在或发生了一个错误, 将会提出一个异常。该异常在代码片段的最后一行处理（在本例中，packets的值没有变化，函数 getPacketsQ返回空的多重集）。文件”SimpleProtocol_IO.TXT”（和该例子一起给出的）具体说明了带有8个包的多重集，如下:%Th.is flie is used by to initialise %tlie uackets on Send4很容易对Simple Protocol”的CPN模型进行修改，如：获得一个损坏的协议其中，马上一个接一 个地发送所有的包一一而没有等到单独包的确认。鼓励读者进行多个修改，来使用CPN Tools仿真器 验