From 8c9b4be25252fa0da8c3f7a8654967ecc55a0071 Mon Sep 17 00:00:00 2001
From: Johannes Mey <johannes.mey@tu-dresden.de>
Date: Wed, 24 Jun 2020 10:33:54 +0200
Subject: [PATCH] positions, offsets, and line widths must be integers
 according to the ecore. this is an inconsistency between the spec and the
 ecore.

---
 .../resources/haddadin_automaton_flat.pnml    | 340 +++++++++---------
 1 file changed, 170 insertions(+), 170 deletions(-)

diff --git a/src/main/resources/haddadin_automaton_flat.pnml b/src/main/resources/haddadin_automaton_flat.pnml
index 1048cf4..042a0ab 100644
--- a/src/main/resources/haddadin_automaton_flat.pnml
+++ b/src/main/resources/haddadin_automaton_flat.pnml
@@ -344,28 +344,28 @@
       <place id="AM">
         <name>
           <graphics>
-            <offset x="52.0" y="-68.0"/>
+            <offset x="52" y="-68"/>
           </graphics>
           <text>Autonomous Mode</text>
         </name>
         <graphics>
-          <position x="452.0" y="128.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="452" y="128"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
         <initialMarking>
           <toolspecific tool="org.pnml.tool" version="1.0">
             <tokengraphics>
-              <tokenposition x="-2.0" y="-2.0"/>
-              <tokenposition x="2.0" y="0.0"/>
-              <tokenposition x="-2.0" y="2.0"/>
+              <tokenposition x="-2" y="-2"/>
+              <tokenposition x="2" y="0"/>
+              <tokenposition x="-2" y="2"/>
             </tokengraphics>
           </toolspecific>
           <graphics>
             <fill color="#ffffff"/>
-            <line shape="line" color="#000000" width="1.0"/>
-            <offset x="-68.0" y="-32.0"/>
+            <line shape="line" color="#000000" width="1"/>
+            <offset x="-68" y="-32"/>
             <font family="Ubuntu" size="9pt"/>
           </graphics>
           <text>1</text>
@@ -374,402 +374,402 @@
       <place id="CM">
         <name>
           <graphics>
-            <offset x="-152.0" y="-44.0"/>
+            <offset x="-152" y="-44"/>
           </graphics>
           <text>Collaboration Mode</text>
         </name>
         <graphics>
-          <position x="272.0" y="332.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="272" y="332"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </place>
       <place id="HFM">
         <name>
           <graphics>
-            <offset x="22.0" y="-72.0"/>
+            <offset x="22" y="-72"/>
           </graphics>
           <text>Human-Friendly Mode</text>
         </name>
         <graphics>
-          <position x="650.0" y="324.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="650" y="324"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </place>
       <place id="wasAM">
         <name>
           <graphics>
-            <offset x="-32.0" y="88.0"/>
+            <offset x="-32" y="88"/>
           </graphics>
           <text>WasInAutonomousMode</text>
         </name>
         <graphics>
-          <position x="1016.0" y="440.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="1016" y="440"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </place>
       <place id="wasHFM">
         <name>
           <graphics>
-            <offset x="18.0" y="21.0"/>
+            <offset x="18" y="21"/>
           </graphics>
           <text>WasInHumanFriendlyMode</text>
         </name>
         <graphics>
-          <position x="763.0" y="492.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="763" y="492"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </place>
       <place id="FRM">
         <name>
           <graphics>
-            <offset x="-128.0" y="4.0"/>
+            <offset x="-128" y="4"/>
           </graphics>
           <text>Fault Reaction Mode</text>
         </name>
         <graphics>
-          <position x="464.0" y="500.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="464" y="500"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </place>
       <place id="wasCM">
         <name>
           <graphics>
-            <offset x="-104.0" y="64.0"/>
+            <offset x="-104" y="64"/>
           </graphics>
           <text>WasInCollaborationMode</text>
         </name>
         <graphics>
-          <position x="176.0" y="512.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="176" y="512"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </place>
       <transition id="Am2Cm">
         <graphics>
-          <position x="320.0" y="176.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="320" y="176"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a1" source="AM" target="Am2Cm">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="454.0" y="126.0"/>
-          <position x="365.0" y="184.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="454" y="126"/>
+          <position x="365" y="184"/>
         </graphics>
       </arc>
       <arc id="a2" source="Am2Cm" target="CM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="320.0" y="176.0"/>
-          <position x="284.0" y="237.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="320" y="176"/>
+          <position x="284" y="237"/>
         </graphics>
       </arc>
       <transition id="Cm2Am">
         <graphics>
-          <position x="404.0" y="248.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="404" y="248"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a3" source="CM" target="Cm2Am">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="271.0" y="312.0"/>
-          <position x="359.0" y="308.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="271" y="312"/>
+          <position x="359" y="308"/>
         </graphics>
       </arc>
       <arc id="a4" source="Cm2Am" target="AM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="404.0" y="248.0"/>
-          <position x="432.0" y="111.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="404" y="248"/>
+          <position x="432" y="111"/>
         </graphics>
       </arc>
       <transition id="Am2Hfm">
         <graphics>
-          <position x="608.0" y="188.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="608" y="188"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a5" source="Am2Hfm" target="HFM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="608.0" y="188.0"/>
-          <position x="598.0" y="263.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="608" y="188"/>
+          <position x="598" y="263"/>
         </graphics>
       </arc>
       <arc id="a6" source="AM" target="Am2Hfm">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="445.0" y="127.0"/>
-          <position x="593.0" y="135.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="445" y="127"/>
+          <position x="593" y="135"/>
         </graphics>
       </arc>
       <transition id="Hfm2Am">
         <graphics>
-          <position x="536.0" y="224.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="536" y="224"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a7" source="HFM" target="Hfm2Am">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="650.0" y="324.0"/>
-          <position x="575.0" y="281.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="650" y="324"/>
+          <position x="575" y="281"/>
         </graphics>
       </arc>
       <arc id="a8" source="Hfm2Am" target="AM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="536.0" y="224.0"/>
-          <position x="478.0" y="130.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="536" y="224"/>
+          <position x="478" y="130"/>
         </graphics>
       </arc>
       <transition id="Cm2Hfm">
         <graphics>
-          <position x="458.0" y="303.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="458" y="303"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a9" source="CM" target="Cm2Hfm">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="264.0" y="333.0"/>
-          <position x="429.0" y="309.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="264" y="333"/>
+          <position x="429" y="309"/>
         </graphics>
       </arc>
       <arc id="a10" source="Cm2Hfm" target="HFM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="458.0" y="303.0"/>
-          <position x="623.0" y="326.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="458" y="303"/>
+          <position x="623" y="326"/>
         </graphics>
       </arc>
       <transition id="Hfm2Cm">
         <graphics>
-          <position x="463.0" y="361.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="463" y="361"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a11" source="HFM" target="Hfm2Cm">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="623.0" y="328.0"/>
-          <position x="448.0" y="366.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="623" y="328"/>
+          <position x="448" y="366"/>
         </graphics>
       </arc>
       <arc id="a12" source="Hfm2Cm" target="CM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="463.0" y="361.0"/>
-          <position x="293.0" y="347.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="463" y="361"/>
+          <position x="293" y="347"/>
         </graphics>
       </arc>
       <transition id="Cm2Fm">
         <graphics>
-          <position x="295.0" y="430.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="295" y="430"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a13" source="CM" target="Cm2Fm">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="273.0" y="325.0"/>
-          <position x="268.0" y="390.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="273" y="325"/>
+          <position x="268" y="390"/>
         </graphics>
       </arc>
       <arc id="a28" source="Cm2Fm" target="wasCM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="295.0" y="430.0"/>
-          <position x="182.0" y="492.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="295" y="430"/>
+          <position x="182" y="492"/>
         </graphics>
       </arc>
       <arc id="a29" source="Cm2Fm" target="FRM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="295.0" y="430.0"/>
-          <position x="430.0" y="471.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="295" y="430"/>
+          <position x="430" y="471"/>
         </graphics>
       </arc>
       <transition id="Fm2Cm">
         <graphics>
-          <position x="339.0" y="632.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="339" y="632"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a14" source="wasCM" target="Fm2Cm">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="175.0" y="511.0"/>
-          <position x="327.0" y="592.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="175" y="511"/>
+          <position x="327" y="592"/>
         </graphics>
       </arc>
       <arc id="a15" source="FRM" target="Fm2Cm">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="464.0" y="499.0"/>
-          <position x="356.0" y="601.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="464" y="499"/>
+          <position x="356" y="601"/>
         </graphics>
       </arc>
       <arc id="a16" source="Fm2Cm" target="CM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="315.0" y="629.0"/>
-          <position x="8.0" y="592.0"/>
-          <position x="254.0" y="326.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="315" y="629"/>
+          <position x="8" y="592"/>
+          <position x="254" y="326"/>
         </graphics>
       </arc>
       <transition id="Hfm2Fm">
         <graphics>
-          <position x="637.0" y="425.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="637" y="425"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a17" source="HFM" target="Hfm2Fm">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="652.0" y="329.0"/>
-          <position x="652.0" y="402.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="652" y="329"/>
+          <position x="652" y="402"/>
         </graphics>
       </arc>
       <arc id="a17" source="Hfm2Fm" target="FRM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="637.0" y="425.0"/>
-          <position x="492.0" y="465.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="637" y="425"/>
+          <position x="492" y="465"/>
         </graphics>
       </arc>
       <arc id="a18" source="Hfm2Fm" target="wasHFM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="637.0" y="425.0"/>
-          <position x="725.0" y="469.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="637" y="425"/>
+          <position x="725" y="469"/>
         </graphics>
       </arc>
       <transition id="Fm2Hfm">
         <graphics>
-          <position x="637.0" y="577.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="637" y="577"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a19" source="wasHFM" target="Fm2Hfm">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="731.0" y="483.0"/>
-          <position x="623.0" y="577.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="731" y="483"/>
+          <position x="623" y="577"/>
         </graphics>
       </arc>
       <arc id="a20" source="FRM" target="Fm2Hfm">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="457.0" y="497.0"/>
-          <position x="613.0" y="577.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="457" y="497"/>
+          <position x="613" y="577"/>
         </graphics>
       </arc>
       <arc id="a21" source="Fm2Hfm" target="HFM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="642.0" y="574.0"/>
-          <position x="693.0" y="544.0"/>
-          <position x="644.0" y="321.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="642" y="574"/>
+          <position x="693" y="544"/>
+          <position x="644" y="321"/>
         </graphics>
       </arc>
       <transition id="Am2Fm">
         <graphics>
-          <position x="972.0" y="261.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="972" y="261"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a22" source="AM" target="Am2Fm">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="456.0" y="107.0"/>
-          <position x="729.0" y="100.0"/>
-          <position x="937.0" y="227.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="456" y="107"/>
+          <position x="729" y="100"/>
+          <position x="937" y="227"/>
         </graphics>
       </arc>
       <arc id="a23" source="Am2Fm" target="wasAM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="973.0" y="264.0"/>
-          <position x="1028.0" y="404.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="973" y="264"/>
+          <position x="1028" y="404"/>
         </graphics>
       </arc>
       <arc id="a24" source="Am2Fm" target="FRM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="972.0" y="261.0"/>
-          <position x="944.0" y="525.0"/>
-          <position x="584.0" y="693.0"/>
-          <position x="493.0" y="514.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="972" y="261"/>
+          <position x="944" y="525"/>
+          <position x="584" y="693"/>
+          <position x="493" y="514"/>
         </graphics>
       </arc>
       <transition id="Fm2Am">
         <graphics>
-          <position x="714.0" y="758.0"/>
-          <dimension x="40.0" y="40.0"/>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
+          <position x="714" y="758"/>
+          <dimension x="40" y="40"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
           <fill color="#ffffff"/>
         </graphics>
       </transition>
       <arc id="a25" source="FRM" target="Fm2Am">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="446.0" y="505.0"/>
-          <position x="448.0" y="514.0"/>
-          <position x="464.0" y="682.0"/>
-          <position x="674.0" y="727.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="446" y="505"/>
+          <position x="448" y="514"/>
+          <position x="464" y="682"/>
+          <position x="674" y="727"/>
         </graphics>
       </arc>
       <arc id="a26" source="wasAM" target="Fm2Am">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="988.0" y="434.0"/>
-          <position x="720.0" y="738.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="988" y="434"/>
+          <position x="720" y="738"/>
         </graphics>
       </arc>
       <arc id="a27" source="Fm2Am" target="AM">
         <graphics>
-          <line shape="line" color="#b0b0b0" width="1.0"/>
-          <position x="715.0" y="757.0"/>
-          <position x="1073.0" y="580.0"/>
-          <position x="1109.0" y="376.0"/>
-          <position x="941.0" y="160.0"/>
-          <position x="761.0" y="64.0"/>
-          <position x="452.0" y="105.0"/>
+          <line shape="line" color="#b0b0b0" width="1"/>
+          <position x="715" y="757"/>
+          <position x="1073" y="580"/>
+          <position x="1109" y="376"/>
+          <position x="941" y="160"/>
+          <position x="761" y="64"/>
+          <position x="452" y="105"/>
         </graphics>
       </arc>
     </page>
-- 
GitLab