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: registration</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="p5">
            <name>
               <text>p5</text>
            </name>
         </place>
         <place id="end">
            <name>
               <text>end</text>
            </name>
            <finalMarking>
               <text>1</text>
            </finalMarking>
         </place>
         <transition id="age">
            <name>
               <text>age changed</text>
            </name>
            <writeVariable>time</writeVariable>
         </transition>
         <transition guard="(statusOcc' == True)" id="bed">
            <name>
               <text>bed statusOcc</text>
            </name>
         </transition>
         <transition id="mun">
            <name>
               <text>municipality changed</text>
            </name>
         </transition>
         <transition id="pat">
            <name>
               <text>patient changed</text>
            </name>
         </transition>
         <transition id="pid">
            <name>
               <text>patient ID changed</text>
            </name>
         </transition>
         <transition id="tra" guard="(time' &lt; time + 5)">
            <name>
               <text>transfer</text>
            </name>
         </transition>
         <arc id="a0" source="start" target="age">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a1" source="age" target="p1">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a2" source="p1" target="bed">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a5" source="bed" target="p2">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a6" source="p2" target="mun">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a7" source="mun" target="p3">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a8" source="p3" target="pat">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a9" source="pat" target="p4">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a10" source="p4" target="pid">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a11" source="pid" target="p5">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a12" source="p5" target="tra">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a13" source="tra" target="end">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
      </page>
      <variables>
         <variable maxValue="100000" minValue="0" type="java.lang.Double">
            <name>time</name>
         </variable>
         <variable maxValue="100000.0" minValue="0" type="java.lang.Boolean">
            <name>statusOcc</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