{"id":527,"date":"2007-10-10T09:03:27","date_gmt":"2007-10-10T09:03:27","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/2007\/10\/10\/colored-petri-nets\/"},"modified":"2007-10-10T09:03:27","modified_gmt":"2007-10-10T09:03:27","slug":"colored-petri-nets","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2007\/10\/10\/colored-petri-nets\/","title":{"rendered":"Colored Petri Nets"},"content":{"rendered":"<p>Colored Petri Nets<br \/>\nThe big step in Petri nets &#8211; the one that really takes them from a theoretical toy to a<br \/>\nserious tool used by protocol developers &#8211; is the extension to <em>colored<\/em> Petri nets (CPNs). Calling them &#8220;colored&#8221; is a bit of a misnomer; the original idea was to assign colors to tokens, and allow color-based expressions on the elements of the net. But study of analysis models quickly showed<br \/>\nthat you could go much further than that without losing the basic analyzability properties<br \/>\nthat are so valuable. In the full development of CPNs, you can associate essentially arbitrary<br \/>\ncollections of data with Petri net tokens, so long as you use a strong type system, and keep<br \/>\nappropriate restrictions on the expressions used in the net.  The colors thus become<br \/>\ndata types, describing the types of data that can be carried by tokens, and the kinds of tokens that<br \/>\ncan located in a place in the net. <\/p>\n<p> So that&#8217;s the fundamental idea of CPNs: tokens have types, and each token type has some data value associated with it. Below the fold, we&#8217;ll look at how we do that,<br \/>\nand what it means.<\/p>\n<p><!--more--><\/p>\n<p> Colored Petri nets add a collection of extensions to the other elements of the net to take advantage of typed tokens carrying values:<\/p>\n<ul>\n<li> Each place in the net is also assigned a data type, and can only hold tokens of<br \/>\nits assigned type type.<\/li>\n<li> Incoming edges of a transition can have <em>conditions<\/em>: the transition is only<br \/>\nenabled when some set of tokens from the source places satisfy the full set of conditions<br \/>\nfor its incoming edges. The conditions for the incoming edges of a transition can<br \/>\nreference the values from other incoming edges of the same transition &#8211; so, for example,<br \/>\nthe conditions can require that the values of two tokens coming from different incoming<br \/>\nvalues match.<\/li>\n<li> The edges going out of a transition can have <em>expressions<\/em> specifying how to compute the<br \/>\nvalues of tokens  being produced by the transition. When a transition is<br \/>\nsuccessfully fired, the expressions on its outgoing edges are evaluated to produce new tokens<br \/>\nto feed into the place at the end of the edge.<\/li>\n<\/ul>\n<p><img data-recalc-dims=\"1\" loading=\"lazy\" decoding=\"async\" alt=\"colored-net.png\" src=\"https:\/\/i0.wp.com\/scientopia.org\/img-archive\/goodmath\/img_285.png?resize=206%2C235\" width=\"206\" height=\"235\" class=\"inset right\" \/><\/p>\n<p> Let&#8217;s look at a quick example of a CPN transition. Here&#8217;s a very simple CPN. It&#8217;s got 3 places: two of them have type<br \/>\n(Int&times;String), and one has type (Int). The transition takes one token of the pair type, and one of the integer type; and it produces one token of the pair type. The edges coming into the transition declare names for the elements of the token values, and the edge leaving the transition describes how to generate the values for outgoing tokens. This little net starts with two tokens, (4,&#8221;Foo&#8221;), and (2). The transition only fires if the integer token has a value greater than or equal to one, and produces a token multipying the two integers from the incoming token. So the transition would fire, consuming two two tokens shown in the graph, and producing a token (8, &#8220;Foo&#8221;) in the bottom place.<\/p>\n<p> For colored nets, there are a ton of variations. The basic idea is that there&#8217;s some simple version of <a href=\"http:\/\/scientopia.org\/blogs\/goodmath\/2006\/08\/a-lambda-calculus-rerun\">&lambda;-calculus<\/a> which is associated with elements of the CPN:<\/p>\n<ul>\n<li> Places are assigned lambda calculus types, which define the types of values carried by tokens that can be located in the place. At runtime, the place is a <em>bag<\/em> of tokens.<\/li>\n<li> Transitions are basically functions, where the incoming edges define a tuple of input parameters to the function, and the outgoing edges form a tuple of results from the function.<br \/>\nFor our example, the transition is, basically &#8220;&amp;lamba; (v,s),w &rarr; (v*w,s)&#8221;.<\/li>\n<li> The transition can have <em>conditions<\/em> for its firing: the condition will only<br \/>\nbe enabled for incoming token values which meet the condition. In the example, the condition<br \/>\nis that the value coming on the edge from the integer-place must have a value greater than<br \/>\nor equal to one. This turns the lambda function into a guarded partial function: in our example, &#8220;&amp;lamba; (v,s),w | w &gt;= 1 &rarr; (v*w,s)&#8221;.<\/li>\n<\/ul>\n<p> The power here should be obvious: there&#8217;s a lot more capability in colored nets than there were in<br \/>\nsimple Petri nets. Colored nets are potentially Turing complete. But for tractability, implementations<br \/>\noften place constraints on the calculus used by the transitions to limit it to something simpler. Since Petri nets are used mainly for describing concurrency and coordination schemes, they don&#8217;t generally<br \/>\nneed to be Turing complete, and by constraining the calculus, you get the ability to perform analyses<br \/>\non the scheme defined by the net which can produce useful results. For example, you can prove that<br \/>\nthere are no possible deadlocks; you can prove that some event X never occurs before some other<br \/>\nevent Y; etc.<\/p>\n<p> Let&#8217;s take a look at a real example of a colored net. This is a slightly simplified version of a net taken from <a href=\"http:\/\/www.daimi.au.dk\/~kjensen\/papers_books\/brief.pdf\">a paper<\/a> introducing colored Petri nets, written by <a href=\"http:\/\/www.daimi.au.dk\/CPnets\/intro\/\">a group that implements a CPN design and analysis tool<\/a>: <\/p>\n<p><img data-recalc-dims=\"1\" loading=\"lazy\" decoding=\"async\" alt=\"petri-protocol.png\" src=\"https:\/\/i0.wp.com\/scientopia.org\/img-archive\/goodmath\/img_286.png?resize=571%2C349\" width=\"571\" height=\"349\" \/><\/p>\n<p> It describes a very<br \/>\nsimple communication protocol, which that works as follows:<\/p>\n<ol>\n<li> There are a single sender, and a single reciever.<\/li>\n<li> Both the sender and the reciever have a common sequence number, which is used to indicate that<br \/>\nthey&#8217;re in sync with one another, and no data was lost.<\/li>\n<li> The sender sends a packet of data to the reciever.<\/li>\n<li> If the packet number received by the receiver is correct, then the receiver signals the sender<br \/>\nthat it&#8217;s ready for the next packet.<\/li>\n<li> If the packet number recieved by the receiver is not correct, then it signals the sender<br \/>\nwith the number of the packet that it&#8217;s expecting.<\/li>\n<li> The sender can resend a packet no more than three times.<\/li>\n<\/ol>\n<p>.<\/p>\n<p> The Colored Petri net for this is a relatively straightforward rendition of the description<br \/>\nabove. In this net, the green places and transitions are on the sender; the pink are the reciever; and the gold are the network. The shaded places are the places that indicate the point where tokens are transferred between entities. It works as follows:<\/p>\n<ol>\n<li> The net is initialized with 4 copies of tokens containing each packet of data in the &#8220;Send&#8221; place, and the integer &#8220;1&#8221; in both &#8220;NextToSend&#8221; and &#8220;NextRec&#8221;. So &#8220;NextToSend&#8221; initially contains one token, which contains the value 1, and &#8220;Send&#8221; contains a bunch of tokens containing data to send, numbered in order.<\/li>\n<li> &#8220;SendPacket&#8221; is only enabled for tokens from &#8220;Send&#8221; and &#8220;NextToSend&#8221; which have matching integers &#8211; thus, packet 1.<\/li>\n<li> &#8220;SendPacket&#8221; fires, sending the token for packet one to &#8220;A&#8221;, which enables &#8220;TransmitPacket&#8221;, which sends it to &#8220;B&#8221;. <\/li>\n<li> Now, things get a bit interesting. &#8220;B&#8221; sends it to &#8220;ReceivePacket&#8221;, which then looks at<br \/>\nthe integer sequence number, &#8220;n&#8221;:<\/p>\n<ol>\n<li> If &#8220;n&#8221; matches the integer &#8220;k&#8221; stored in &#8220;NextRec&#8221;, then &#8220;ReceivePacket&#8221; fires, sending<br \/>\na token containing &#8220;n+1&#8221; to &#8220;NextRec&#8221;, and sending a token to &#8220;C&#8221; indicating that it<br \/>\nnext wants to receive token &#8220;n+1&#8221;. <\/li>\n<li> If &#8220;n&#8221; does not match &#8220;k&#8221;, then &#8220;RecievePacket&#8221; fires, sending a token containing &#8220;k&#8221;<br \/>\nto &#8220;C&#8221;, indicating that the reciever still hasn&#8217;t recieved packet &#8220;k&#8221;.<\/li>\n<\/ol>\n<\/li>\n<li> Whatever desired packet number was send by &#8220;RecievePacket&#8221; percolates forward to &#8220;NextToSend&#8221;,<br \/>\nwhere it starts the whole process over for the requested packet.<\/li>\n<li> If the sequencing got mangled (because of data loss along the network), the protocol basically<br \/>\nrequests a resend &#8211; that&#8217;s what the logic of &#8220;RecievePacket&#8221; is all about. Since there are four<br \/>\ncopies of each packet in &#8220;Send&#8221;, it can re-send up to 3 times. (The initial send, and 3 re-sends.)<\/li>\n<\/ol>\n<p> Hopefully, from this you can see the basic ideas of Petri nets. There are numerous other variants: stochastic Petri-nets, genomic Petri nets, heirarchical Petri nets, and more. But the basic idea<br \/>\nalways remains the same: there are places that contain tokens, and transitions that consume one set of tokens and produce another; and the transitions provide a synchronization point for the processes that<br \/>\nhave edges into them. From that basis, you get a great amount of power, and also a great amount of<br \/>\nanalyzability.<\/p>\n<p> Remember the rant that I started with, about Estelle, the formal specification language with no useful formal properties? A french group did produce a useful tool based on a variant of Estelle, called Esterelle. What Esterelle did was adopt colored petri net semantics, and constrained the actions<br \/>\nof the Estelle transition arcs to things that could be expressed in a CPN. Of course, that&#8217;s still a strange idea: they were taking a language based on communicating FSMs, and giving it semantics and<br \/>\nrestrictions based on CPNs. Why not just give up and use the Petri nets?<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Colored Petri Nets The big step in Petri nets &#8211; the one that really takes them from a theoretical toy to a serious tool used by protocol developers &#8211; is the extension to colored Petri nets (CPNs). Calling them &#8220;colored&#8221; is a bit of a misnomer; the original idea was to assign colors to tokens, [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[79,25,42,54],"tags":[],"class_list":["post-527","post","type-post","status-publish","format-standard","hentry","category-computation","category-graph-theory","category-networks","category-programming"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-8v","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/527","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=527"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/527\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=527"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=527"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=527"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}