Ada

Model

<?xml version="1.0" encoding="UTF-8"?>
<pnml>
   <net id="net1" type="http://www.pnml.org/version-2009/grammar/pnmlcoremodel">
      <name>
         <text>Digital whiteboard: discharge</text>
      </name>
      <page id="n0">
         <place id="start">
            <name>
               <text>start</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="end">
            <name>
               <text>end</text>
            </name>
            <finalMarking>
               <text>1</text>
            </finalMarking>
         </place>
         <transition id="bed1" guard="(statusLedig' == True)">
            <name>
               <text>bed status</text>
            </name>
            <writeVariable>org1</writeVariable>
         </transition>
         <transition id="bed2" guard="(statusLedig' == True)">
            <name>
               <text>bed status</text>
            </name>
            <writeVariable>org2</writeVariable>
         </transition>
         <transition id="mth1" guard="(org1' == org1)">
            <name>
               <text>move to history</text>
            </name>
         </transition>
         <transition id="mth2" guard="(org2' == org2)">
            <name>
               <text>move to history</text>
            </name>
         </transition>
         <transition id="tra1" guard="((org1' == org1) &amp;&amp; (valueHistory' == True))">
            <name>
               <text>Transfer</text>
            </name>
         </transition>
         <transition id="tra2" guard="((org2' == org2) &amp;&amp; (valueHistory' == True))">
            <name>
               <text>Transfer</text>
            </name>
         </transition>
         <arc id="a0" source="start" target="bed1">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a1" source="bed1" target="p1">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a2" source="p1" target="bed2">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a5" source="bed2" target="p2">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a6" source="p2" target="tra1">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a7" source="p2" target="mth1">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a8" source="tra1" target="p3">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a9" source="p3" target="tra2">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a10" source="tra2" target="end">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a11" source="mth1" target="p4">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a12" source="p4" target="mth2">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a13" source="mth2" target="end">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
      </page>
      <variables>
         <variable maxValue="100000" minValue="0" type="java.lang.Integer">
            <name>org1</name>
         </variable>
         <variable maxValue="100000" minValue="0" type="java.lang.Integer">
            <name>org2</name>
         </variable>
         <variable maxValue="100000.0" minValue="0" type="java.lang.Boolean">
            <name>statusLedig</name>
         </variable>
         <variable maxValue="100000.0" minValue="0" type="java.lang.Boolean">
            <name>valueHistory</name>
         </variable>
      </variables>
   </net>
   <property><text> A G E F end</text></property>
</pnml>

LTLf property

Ada - the arithmetic DDS analyzer

CTL* model checking with arithmetic