{"id":76,"date":"2012-11-20T15:45:08","date_gmt":"2012-11-20T14:45:08","guid":{"rendered":"https:\/\/project.inria.fr\/plasma-lab\/?page_id=76"},"modified":"2016-07-01T16:12:49","modified_gmt":"2016-07-01T14:12:49","slug":"dining-philosophers","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/plasma-lab\/examples\/dining-philosophers\/","title":{"rendered":"Dining philosophers"},"content":{"rendered":"<style><!--\n.center { margin:auto; }\n--><\/style>\n<h3>Introduction<\/h3>\n<p>To test the model-checking performance of PLASMA we created increasingly complex models based on the probabilistic dining philosophers of (Pnueli, Zuck 1986). Especially we used this range of model for our IGRIDA distributed experimentation. Results of this experimentation can be found <a href=\"https:\/\/project.inria.fr\/plasma-lab\/igrida-experimentation\/\">here<\/a>. Here is the model for the case of 3 philosophers. You can <strong><a href=\"http:\/\/plasma-lab.gforge.inria.fr\/plasma_lab_examples\/DTMC\/Philosophers.plasma\">download a Plasma Lab project file<\/a><\/strong> containing models and a liveness property for 3 philosophers to 300 philosophers.<\/p>\n<div id=\"attachment_673\" style=\"width: 265px\" class=\"wp-caption aligncenter\"><a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/philoAutomata.png\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-673\" class=\"size-medium wp-image-673\" title=\"philoAutomata\" alt=\"\" src=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/philoAutomata-255x300.png\" width=\"255\" height=\"300\" srcset=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/philoAutomata-255x300.png 255w, https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/philoAutomata-871x1024.png 871w, https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/philoAutomata.png 909w\" sizes=\"auto, (max-width: 255px) 100vw, 255px\" \/><\/a><p id=\"caption-attachment-673\" class=\"wp-caption-text\">Automata modelling a philosopher<\/p><\/div>\n<hr \/>\n<h3>Model<\/h3>\n<div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p>\n<pre class=\"first-p\">\/\/ Randomised dining philosophers based on (Pnueli, Zuck 1986)<\/pre>\n<p>dtmc<\/p>\n<p>formula lfree = p2&gt;=0 &amp; p2&lt;=4 | p2=6 | p2=10; formula rfree = p3&gt;=0 &amp; p3&lt;=3 | p3=5 | p3=7; module phil1 p1: [0..10]; [] p1=0 -&gt; 0.2 : (p1&#8217;=0) + 0.8 : (p1&#8217;=1);<br \/>\n[] p1=1 -&gt; 0.5 : (p1&#8217;=2) + 0.5 : (p1&#8217;=3);<br \/>\n[] p1=2 &amp; lfree -&gt; (p1&#8217;=4);<br \/>\n[] p1=2 &amp; !lfree -&gt; (p1&#8217;=2);<br \/>\n[] p1=3 &amp; rfree -&gt; (p1&#8217;=5);<br \/>\n[] p1=3 &amp; !rfree -&gt; (p1&#8217;=3);<br \/>\n[] p1=4 &amp; rfree -&gt; (p1&#8217;=8);<br \/>\n[] p1=4 &amp; !rfree -&gt; (p1&#8217;=6);<br \/>\n[] p1=5 &amp; lfree -&gt; (p1&#8217;=8);<br \/>\n[] p1=5 &amp; !lfree -&gt; (p1&#8217;=7);<br \/>\n[] p1=6 -&gt; (p1&#8217;=1);<br \/>\n[] p1=7 -&gt; (p1&#8217;=1);<br \/>\n[] p1=8 -&gt; (p1&#8217;=9);<br \/>\n[] p1=9 -&gt; (p1&#8217;=10);<br \/>\n[] p1=10 -&gt; (p1&#8217;=0);<br \/>\nendmodule<\/p>\n<p>module phil2 = phil1 [p1=p2, p2=p3, p3=p1] endmodule<br \/>\nmodule phil3 = phil1 [p1=p3, p2=p1, p3=p2] endmodule<\/p>\n<p>\/\/ labels<br \/>\nlabel &#8220;hungry&#8221; = ((p1&gt;0)&amp;(p1&lt;8))|((p2&gt;0)&amp;(p2&lt;8))|((p3&gt;0)&amp;(p3&lt;8)); label &#8220;eat&#8221; = ((p1&gt;=8)&amp;(p1&lt;=9))|((p2&gt;=8)&amp;(p2&lt;=9))|((p3&gt;=8)&amp;(p3&lt;=9));<\/p>\n<div><\/div><\/div>\n<div style=\"text-align: center;\">\n<p><strong><strong>Download : <a href=\"http:\/\/plasma-lab.gforge.inria.fr\/plasma_lab_examples\/DTMC\/Philosophers.plasma\">Philosophers.plasma<\/a><\/strong><\/strong><\/p>\n<hr \/>\n<h3 style=\"text-align: left;\">Requirement<\/h3>\n<\/div>\n<p>We checked a property saying <em>&#8220;fatally one of the philosophers will be hungry and after that, fatally, one of the philosophers will eat&#8221;<\/em>.<\/p>\n<div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p>F&lt;=#1000 (hungry &amp;(X&lt;=#1 F&lt;=#1000 eat)) <\/div>\n<p>We checked this property with the <strong>Chernoff method<\/strong> and parameters <strong>epsilon = 0.001<\/strong>, <strong>delta = 0.01<\/strong>. With these parameters Plasma Lab will check the property with a <strong>confidence of 99% and a precision of 0.1%<\/strong>.<br \/>\nWe used this model to benchmark Plasma Lab and compare it against others Statistical Model Checking tools. The results are given below.<\/p>\n<table class=\"center\" border=\"1\">\n<tbody>\n<tr>\n<th>#Philosophers<\/th>\n<th>Time (s)<\/th>\n<\/tr>\n<tr>\n<td>3<\/td>\n<td>6.27<\/td>\n<\/tr>\n<tr>\n<td>10<\/td>\n<td>16.629<\/td>\n<\/tr>\n<tr>\n<td>30<\/td>\n<td>89.100<\/td>\n<\/tr>\n<tr>\n<td>100<\/td>\n<td>724.944<\/td>\n<\/tr>\n<tr>\n<td>300<\/td>\n<td>4347.504<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div id=\"attachment_675\" style=\"width: 310px\" class=\"wp-caption aligncenter\"><a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/PhiloCompare.png\"><img loading=\"lazy\" decoding=\"async\" aria-describedby=\"caption-attachment-675\" class=\"size-medium wp-image-675 aligncenter\" title=\"PhiloCompare\" alt=\"\" src=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/PhiloCompare-300x174.png\" width=\"300\" height=\"174\" srcset=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/PhiloCompare-300x174.png 300w, https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/PhiloCompare.png 1002w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a><p id=\"caption-attachment-675\" class=\"wp-caption-text\">Comparison between PRISM Numerical Analysis and Plasma Lab. Time(ms) against number of philosophers.<\/p><\/div>\n<hr \/>\n<h3>Importance splitting<\/h3>\n<p>We experiment the <a title=\"Importance splitting\" href=\"https:\/\/project.inria.fr\/plasma-lab\/importance-splitting\/\">importance splitting algorithm<\/a> on this example. We consider the model with 150 philosophers and we estimate the probability that a given philosopher will eat within 30 steps. This property \\(\\phi=F^{30} Eat\\) can be decomposed into 5 sub-properties that the philosopher must satisfy before satisfying \\(\\phi\\):<a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/Phil2-2.png\"><img loading=\"lazy\" decoding=\"async\" class=\"size-medium wp-image-1603 alignleft\" style=\"margin-left: 50px; margin-right: 50px;\" alt=\"Phil2-2\" src=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/Phil2-2-300x247.png\" width=\"300\" height=\"247\" srcset=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/Phil2-2-300x247.png 300w, https:\/\/project.inria.fr\/plasma-lab\/files\/2012\/11\/Phil2-2.png 623w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/a><\/p>\n<ul>\n<ul>\n<ul>\n<li>\\(\\phi_0=F^{30} Think\\)<\/li>\n<\/ul>\n<\/ul>\n<li>\\(\\phi_1=F^{30} Choose\\)<\/li>\n<li>\\(\\phi_2=F^{30} Try\\)<\/li>\n<li>\\(\\phi_3=F^{30} 1^{st} Stick\\)<\/li>\n<li>\\(\\phi_4=F^{30} 2^{nd} Stick\\)<\/li>\n<li>\\(\\phi_5=F^{30} Eat\\)<\/li>\n<\/ul>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p>\n<p>&nbsp;<\/p>\n<p>We first consider the following observer to compute a score function for this model:<br \/>\n<div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p><br \/>\nobserver rareObserver<br \/>\nscore : double init 0;<br \/>\nc : clock;<br \/>\ndecided : bool init false;<br \/>\ns : [0..5] init 0;<\/p>\n<p class=\"first-p\">[] p1=1 &amp; s=0 -&gt; (score&#8217;=1)&amp;(s&#8217;=1);<br \/>\n[] (p1=2 | p1=3) &amp; (s=1) -&gt; (score&#8217;=2)&amp;(s&#8217;=2);<br \/>\n[] (p1=4 | p1=5) &amp; (s=2) -&gt; (score&#8217;=3)&amp;(s&#8217;=3);<br \/>\n[] p1=8 &amp; (s=3) -&gt; (score&#8217;=4)&amp;(s&#8217;=4);<br \/>\n[] p1 &gt;8 &amp; score &lt;5 &amp; (s=4) -&gt; (score&#8217;=5)&amp;(s&#8217;=5);<br \/>\n[] (c=30) -&gt; (decided&#8217;=true);<br \/>\nendobserver<br \/>\n<\/div><\/p>\n<p style=\"text-align: justify;\">This score function increase the score each time a new sub-property is satisfied. It is adequate to be used with the fixed level algorithm.<\/p>\n<p style=\"text-align: justify;\">We then refine the observer such that the score also takes into account the time at which a new level is satisfied\u00a0 (using the clock c). It is such that the score is between \\(]0,1[ \\text{ if } \\phi_1\\) is satisfied, between \\(]1,2[ \\text{ if } \\phi_2\\) is satisfied, etc&#8230; When the score becomes higher than 4 the property \\(\\phi\\) is satisfied. This observer is optimized for the adaptive algorithm.<\/p>\n<p style=\"text-align: justify;\"><div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p><\/p>\n<p style=\"text-align: justify;\" class=\"first-p\">observer rareObserver<br \/>\ndecided : bool init false;<br \/>\nc : clock;<br \/>\ns : [0..5] init 0;<\/p>\n<p>[] c=30 -&gt; (decided&#8217;= true);<br \/>\n[] p1=1 &amp; s=0 -&gt; (s&#8217;=1);<br \/>\n[] (p1=2 | p1=3) &amp; (s=1) -&gt; (s&#8217;=2);<br \/>\n[] (p1=4 | p1=5) &amp; (s=2) -&gt; (s&#8217;=3);<br \/>\n[] p1=8 &amp; (s=3) -&gt; (s&#8217;=4);<br \/>\n[] p1 &gt;8 &amp; (s=4) -&gt; (s&#8217;=5);<br \/>\nendobserver<\/p>\n<p>observer score<br \/>\nscore : double init 0;<\/p>\n<p>[] true -&gt; (score&#8217;=s-(s-c)\/(s-31));<br \/>\nendobserver<\/p>\n<p style=\"text-align: justify;\"><\/div><\/p>\n<p>The model with the observer can be downloaded <a href=\"http:\/\/plasma-lab.gforge.inria.fr\/plasma_lab_examples\/Rare\/PhilosophersRare.plasma\"><strong>here<\/strong><\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Introduction To test the model-checking performance of PLASMA we created increasingly complex models based on the probabilistic dining philosophers of (Pnueli, Zuck 1986). Especially we used this range of model for our IGRIDA distributed experimentation. Results of this experimentation can be found here. Here is the model for the case\u2026<\/p>\n<p> <a class=\"continue-reading-link\" href=\"https:\/\/project.inria.fr\/plasma-lab\/examples\/dining-philosophers\/\"><span>Continue reading<\/span><i class=\"crycon-right-dir\"><\/i><\/a> <\/p>\n","protected":false},"author":234,"featured_media":0,"parent":236,"menu_order":0,"comment_status":"closed","ping_status":"open","template":"","meta":{"footnotes":""},"class_list":["post-76","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/76","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/users\/234"}],"replies":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/comments?post=76"}],"version-history":[{"count":60,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/76\/revisions"}],"predecessor-version":[{"id":2175,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/76\/revisions\/2175"}],"up":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/236"}],"wp:attachment":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/media?parent=76"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}