Ada

Model

<?xml version="1.0" encoding="UTF-8"?>
<pnml>
   <net id="net1" type="http://www.pnml.org/version-2009/grammar/pnmlcoremodel">
      <name>
         <text>Livelock example</text>
      </name>
      <page id="n0">
         <place id="start">
            <name>
               <text>start</text>
            </name>
            <initialMarking>
               <text>1</text>
            </initialMarking>
         </place>
         <place id="p">
            <name>
               <text>p</text>
            </name>
         </place>
         <place id="end">
            <name>
               <text>end</text>
            </name>
            <finalMarking>
               <text>1</text>
            </finalMarking>
         </place>
         <transition guard="(a' &gt; 0)" id="writea">
            <name>
               <text>write a</text>
            </name>
         </transition>
         <transition guard="(b' &gt; a)" id="writeb">
            <name>
               <text>write b</text>
            </name>
         </transition>
         <transition guard="(b &lt; 3)" id="check">
            <name>
               <text>check</text>
            </name>
         </transition>
        
         <arc id="a0" source="start" target="writea">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a1" source="writea" target="p">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a2" source="p" target="writeb">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a5" source="writeb" target="p">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a6" source="p" target="check">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
         <arc id="a7" source="check" target="end">
            <arctype>
               <text>normal</text>
            </arctype>
         </arc>
        
      </page>
      <variables>
         <variable maxValue="100000" minValue="0" type="java.lang.Double">
            <name>a</name>
         </variable>
         <variable maxValue="100000.0" minValue="0" type="java.lang.Double">
            <name>b</name>
         </variable>
      </variables>
      <property sound="0"/>
   </net>
</pnml>

Repair mode:

none

restrict

extend

Ada - the arithmetic DDS analyzer

checking data-aware soundness of Data Petri Nets