Ada

Model

<?xml version="1.0" encoding="UTF-8"?>
<pnml>
   <net id="net1" type="http://www.pnml.org/version-2009/grammar/pnmlcoremodel">
      <name>
         <text>Package handling</text>
      </name>
      <page id="n0">
         <place id="p0">
            <name>
               <text>p0</text>
            </name>
            <initialMarking>
               <text>1</text>
            </initialMarking>
         </place>
         <place id="p1">
            <name>
               <text>p1</text>
            </name>
         </place>
         <place id="p2">
            <name>
               <text>p2</text>
            </name>
         </place>
         <place id="p3">
            <name>
               <text>p3</text>
            </name>
         </place>
         <place id="p4">
            <name>
               <text>p4</text>
            </name>
         </place>
         <place id="p5">
            <name>
               <text>p5</text>
            </name>
         </place>
         <place id="p6">
            <name>
               <text>p6</text>
            </name>
         </place>
         <place id="p7">
            <name>
               <text>p7</text>
            </name>
         </place>
         <place id="p8">
            <name>
               <text>p8</text>
            </name>
         </place>
         <place id="p9">
            <name>
               <text>p9</text>
            </name>
         </place>
         <place id="p10">
            <name>
               <text>p10</text>
            </name>
         </place>
         <place id="p11">
            <name>
               <text>p11</text>
            </name>
         </place>
         <place id="p12">
            <name>
               <text>p12</text>
            </name>
         </place>
         <place id="p13">
            <name>
               <text>p13</text>
            </name>
         </place>
         <place id="p14">
            <name>
               <text>p14</text>
            </name>
         </place>
         <place id="end">
            <name>
               <text>end</text>
            </name>
            <finalMarking>
               <text>1</text>
            </finalMarking>
         </place>
         <transition guard="((pT' &gt; 0) &amp;&amp; (pT' &lt;= 3))" id="tau1" invisible="true">
            <name>
               <text>tau1</text>
            </name>
         </transition>
         <transition guard="((pT == 1) &amp;&amp; (pL' == 0.5))" id="t1">
            <name>
               <text>getlength1</text>
            </name>
         </transition>
         <transition guard="((pT == 2) &amp;&amp; (pL' == 1))" id="t2">
            <name>
               <text>getlength2</text>
            </name>
         </transition>
         <transition guard="((pT == 3) &amp;&amp; (pL' == 2))" id="t3">
            <name>
               <text>getlength3</text>
            </name>
         </transition>
         <transition guard="((pT == 0) || ((pT != 1) &amp;&amp; (pT != 2) &amp;&amp; (pT != 3))) &amp;&amp; (pL' == 0)" id="t4">
            <name>
               <text>getlengthnoRow</text>
            </name>
         </transition>
         <transition guard="(pL == 0)" id="tau2" invisible="true">
            <name>
               <text>tau2</text>
            </name>
         </transition>
         <transition guard="(pL != 0)" id="tau3" invisible="true">
            <name>
               <text>tau3</text>
            </name>
         </transition>
         <transition guard="(pW' &gt; 0)" id="t5" invisible="true">
            <name>
               <text>measure weight</text>
            </name>
         </transition>
         <transition guard="(pW &lt;= 10)" id="tau4" invisible="true">
            <name>
               <text>tau4</text>
            </name>
         </transition>
         <transition guard="(pW &gt; 10)" id="tau5" invisible="true">
            <name>
               <text>tau5</text>
            </name>
         </transition>
         <transition guard="((pL &gt; 0) &amp;&amp; (pL &lt;= 1) &amp;&amp; (pW &gt; 0) &amp;&amp; (pW &lt;= 5) &amp;&amp; (sM' == 1))" id="t6">
            <name>
               <text>determinemode1</text>
            </name>
         </transition>
         <transition guard="((pL &gt; 1) &amp;&amp; (pL &lt;= 2) &amp;&amp; (pW &gt; 0) &amp;&amp; (pW &lt;= 5) &amp;&amp; (sM' == 2))" id="t7">
            <name>
               <text>determinemode2</text>
            </name>
         </transition>
         <transition guard="((pW &gt; 5) &amp;&amp; (pW &lt;= 10) &amp;&amp; (sM' == 2))" id="t8">
            <name>
               <text>determinemode3</text>
            </name>
         </transition>
         <transition guard="(((pL == 0) || (pW == 0) || (pL &lt;= 0) || (pW &lt;= 0)) &amp;&amp; (sM' == 0)) || (((pW &gt; 10) || ((pW &gt; 0) &amp;&amp; (pW &lt;= 5) &amp;&amp; (pL &gt; 2))) &amp;&amp; (sM' == 0))" id="t9">
            <name>
               <text>determinemodenoRow</text>
            </name>
         </transition>
         <transition guard="(sM == 0)" id="tau6" invisible="true">
            <name>
               <text>tau6</text>
            </name>
         </transition>
         <transition guard="(sM != 0)" id="tau7" invisible="true">
            <name>
               <text>tau7</text>
            </name>
         </transition>
         <transition guard="((sM == 1) &amp;&amp; (pW &gt; 6) &amp;&amp; (c' == 3))" id="t10">
            <name>
               <text>chooseconsent1</text>
            </name>
         </transition>
         <transition guard="((sM == 2) &amp;&amp; (pW &gt; 8) &amp;&amp; (c' == 1))" id="t11">
            <name>
               <text>chooseconsent2</text>
            </name>
         </transition>
         <transition guard="((((sM == 0) || (pW == 0) || ((sM != 1) &amp;&amp; (sM != 2)) || (pW &lt;= 0)) &amp;&amp; (c' == 0)) || ((((sM == 1) &amp;&amp; (pW &lt;= 6)) || ((sM == 2) &amp;&amp; (pW &lt;= 8))) &amp;&amp; (c' == 2)))" id="t12">
            <name>
               <text>chooseconsentnoRow</text>
            </name>
         </transition>
         <transition guard="(c == 1)" id="tau8" invisible="true">
            <name>
               <text>tau8</text>
            </name>
         </transition>
         <transition guard="(c == 2)" id="tau9" invisible="true">
            <name>
               <text>tau9</text>
            </name>
         </transition>
         <transition guard="(c == 3)" id="tau10" invisible="true">
            <name>
               <text>tau10</text>
            </name>
         </transition>
         <transition id="t13">
            <name>
               <text>sign declaration</text>
            </name>
         </transition>
         <transition id="tau13" invisible="true">
            <name>
               <text>tau13</text>
            </name>
         </transition>
         <transition id="tau11" invisible="true">
            <name>
               <text>tau11</text>
            </name>
         </transition>
         <transition id="t14">
            <name>
               <text>fetchdeclaration</text>
            </name>
         </transition>
         <transition id="tau12" invisible="true">
            <name>
               <text>tau12</text>
            </name>
         </transition>
         <transition id="tau14" invisible="true">
            <name>
               <text>tau14</text>
            </name>
         </transition>
         <arc id="a52" source="p12" target="tau14">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a53" source="tau14" target="end">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a52" source="p14" target="tau12">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a53" source="tau12" target="p12">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a50" source="p13" target="t14">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a51" source="t14" target="p14">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a48" source="p10" target="tau11">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a49" source="tau11" target="p12">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a46" source="p11" target="tau13">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a47" source="tau13" target="p12">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a44" source="p9" target="t13">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a45" source="t13" target="p10">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a42" source="p8" target="tau10">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a43" source="tau10" target="p13">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a40" source="p8" target="tau9">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a41" source="tau9" target="p11">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a38" source="p8" target="tau8">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a39" source="tau8" target="p9">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a32" source="p7" target="t10">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a33" source="t10" target="p8">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a34" source="p7" target="t11">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a35" source="t11" target="p8">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a36" source="p7" target="t12">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a37" source="t12" target="p8">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a30" source="p6" target="tau7">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a31" source="tau7" target="p7">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a28" source="p6" target="tau6">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a29" source="tau6" target="end">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a20" source="p5" target="t6">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a21" source="t6" target="p6">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a22" source="p5" target="t7">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a23" source="t7" target="p6">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a24" source="p5" target="t8">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a25" source="t8" target="p6">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a26" source="p5" target="t9">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a27" source="t9" target="p6">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a18" source="p4" target="tau5">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a19" source="tau5" target="end">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a16" source="p4" target="tau4">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a17" source="tau4" target="p5">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a14" source="p3" target="t5">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a15" source="t5" target="p4">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a12" source="p2" target="tau3">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a13" source="tau3" target="p3">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a10" source="p2" target="tau2">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a11" source="tau2" target="end">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a2" source="p1" target="t1">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a3" source="t1" target="p2">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a4" source="p1" target="t2">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a5" source="t2" target="p2">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a6" source="p1" target="t3">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a7" source="t3" target="p2">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a8" source="p1" target="t4">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a9" source="t4" target="p2">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a0" source="p0" target="tau1">
            <arctype> <text>normal</text> </arctype>
         </arc>
         <arc id="a1" source="tau1" target="p1">
            <arctype> <text>normal</text> </arctype>
         </arc>
      </page>
      <variables>
         <variable maxValue="10000.0" minValue="0.0" type="java.lang.Double">
            
            
            <name>pL</name>
         </variable>
         <variable maxValue="10000.0" minValue="0.0" type="java.lang.Double">
            
            
            <name>pW</name>
         </variable>
         <variable maxValue="3" minValue="0" type="java.lang.Integer">
            
            
            <name>pT</name>
         </variable>
         <variable maxValue="2" minValue="0" type="java.lang.Integer">
            
            
            <name>sM</name>
         </variable>
         <variable maxValue="3" minValue="0" type="java.lang.Integer">
            
            
            <name>c</name>
         </variable>
      </variables>
   </net>
   <property><text>E F (&lt;fetchdeclaration&gt; true)</text></property>
</pnml>

LTLf property

Ada - the arithmetic DDS analyzer

CTL* model checking with arithmetic