From a3d75faa68ac55bd508434af04bdfc30abb7c8ac Mon Sep 17 00:00:00 2001
From: apvrille <ludovic.apvrille@eurecom.fr>
Date: Tue, 6 Feb 2018 17:24:24 +0100
Subject: [PATCH] Updating how reachability and liveness are displayed in order
 to remove previous infos when making a new formal verif

---
 modeling/SysMLSec/at_zeuszitmo.xml            | 303 +++++++++---------
 src/main/java/ui/MainGUI.java                 |  15 +
 src/main/java/ui/TDiagramPanel.java           |  12 +
 src/main/java/ui/TURTLEPanel.java             |  13 +-
 .../ui/window/JDialogAvatarModelChecker.java  |   4 +-
 .../ui/window/JDialogUPPAALValidation.java    |  11 +-
 6 files changed, 200 insertions(+), 158 deletions(-)

diff --git a/modeling/SysMLSec/at_zeuszitmo.xml b/modeling/SysMLSec/at_zeuszitmo.xml
index 3facbfdb48..313aa8448b 100644
--- a/modeling/SysMLSec/at_zeuszitmo.xml
+++ b/modeling/SysMLSec/at_zeuszitmo.xml
@@ -9,7 +9,7 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector" value="" />
 <TGConnectingPoint num="0" id="1" />
-<P1  x="663" y="785" id="228" />
+<P1  x="663" y="785" id="303" />
 <P2  x="757" y="658" id="203" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
@@ -36,8 +36,8 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector from TGComponent to TGComponent" value="" />
 <TGConnectingPoint num="0" id="7" />
-<P1  x="938" y="416" id="614" />
-<P2  x="937" y="382" id="630" />
+<P1  x="938" y="416" id="651" />
+<P2  x="937" y="382" id="629" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
 <CONNECTOR type="133" id="12" >
@@ -46,8 +46,8 @@
 <infoparam name="connector from TGComponent to TGComponent" value="2" />
 <TGConnectingPoint num="0" id="10" />
 <TGConnectingPoint num="1" id="11" />
-<P1  x="937" y="347" id="627" />
-<P2  x="892" y="314" id="612" />
+<P1  x="937" y="347" id="626" />
+<P2  x="892" y="314" id="675" />
 <Point x="931" y="331" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR><SUBCOMPONENT type="-1" id="9" >
@@ -64,8 +64,8 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector from TGComponent to TGComponent" value="" />
 <TGConnectingPoint num="0" id="13" />
-<P1  x="861" y="279" id="601" />
-<P2  x="821" y="250" id="680" />
+<P1  x="861" y="279" id="664" />
+<P2  x="821" y="250" id="579" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
 <CONNECTOR type="133" id="16" >
@@ -73,7 +73,7 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector from TGComponent to TGComponent" value="1" />
 <TGConnectingPoint num="0" id="15" />
-<P1  x="663" y="840" id="303" />
+<P1  x="663" y="840" id="228" />
 <P2  x="726" y="814" id="197" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
@@ -82,7 +82,7 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector from TGComponent to TGComponent" value="" />
 <TGConnectingPoint num="0" id="17" />
-<P1  x="893" y="783" id="355" />
+<P1  x="893" y="783" id="405" />
 <P2  x="917" y="682" id="184" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
@@ -92,7 +92,7 @@
 <infoparam name="connector from TGComponent to TGComponent" value="" />
 <TGConnectingPoint num="0" id="19" />
 <P1  x="819" y="805" id="196" />
-<P2  x="838" y="800" id="352" />
+<P2  x="838" y="800" id="402" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
 <CONNECTOR type="133" id="22" >
@@ -109,7 +109,7 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector from TGComponent to TGComponent" value="" />
 <TGConnectingPoint num="0" id="23" />
-<P1  x="983" y="720" id="406" />
+<P1  x="983" y="720" id="356" />
 <P2  x="979" y="682" id="185" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
@@ -127,8 +127,8 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector from TGComponent to TGComponent" value="1" />
 <TGConnectingPoint num="0" id="27" />
-<P1  x="711" y="347" id="656" />
-<P2  x="830" y="314" id="611" />
+<P1  x="711" y="347" id="605" />
+<P2  x="830" y="314" id="674" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
 <CONNECTOR type="133" id="30" >
@@ -136,8 +136,8 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector from TGComponent to TGComponent" value="0" />
 <TGConnectingPoint num="0" id="29" />
-<P1  x="805" y="435" id="578" />
-<P2  x="877" y="433" id="615" />
+<P1  x="805" y="435" id="679" />
+<P2  x="877" y="433" id="652" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
 <CONNECTOR type="133" id="32" >
@@ -155,7 +155,7 @@
 <infoparam name="connector from TGComponent to TGComponent" value="1" />
 <TGConnectingPoint num="0" id="33" />
 <P1  x="955" y="578" id="376" />
-<P2  x="938" y="451" id="617" />
+<P2  x="938" y="451" id="654" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
 <CONNECTOR type="133" id="36" >
@@ -164,7 +164,7 @@
 <infoparam name="connector from TGComponent to TGComponent" value="" />
 <TGConnectingPoint num="0" id="35" />
 <P1  x="653" y="563" id="732" />
-<P2  x="676" y="373" id="660" />
+<P2  x="676" y="373" id="609" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
 <CONNECTOR type="133" id="38" >
@@ -181,7 +181,7 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector from TGComponent to TGComponent" value="" />
 <TGConnectingPoint num="0" id="39" />
-<P1  x="600" y="733" id="253" />
+<P1  x="600" y="733" id="278" />
 <P2  x="726" y="658" id="210" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
@@ -190,7 +190,7 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector from TGComponent to TGComponent" value="" />
 <TGConnectingPoint num="0" id="41" />
-<P1  x="395" y="888" id="277" />
+<P1  x="395" y="888" id="252" />
 <P2  x="342" y="888" id="215" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
@@ -199,7 +199,7 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector from TGComponent to TGComponent" value="" />
 <TGConnectingPoint num="0" id="43" />
-<P1  x="244" y="830" id="479" />
+<P1  x="244" y="830" id="454" />
 <P2  x="249" y="871" id="217" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
@@ -209,7 +209,7 @@
 <infoparam name="connector from TGComponent to TGComponent" value="" />
 <TGConnectingPoint num="0" id="45" />
 <P1  x="311" y="871" id="218" />
-<P2  x="299" y="773" id="460" />
+<P2  x="299" y="773" id="485" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
 <CONNECTOR type="133" id="48" >
@@ -217,7 +217,7 @@
 <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <infoparam name="connector from TGComponent to TGComponent" value="" />
 <TGConnectingPoint num="0" id="47" />
-<P1  x="249" y="747" id="451" />
+<P1  x="249" y="747" id="476" />
 <P2  x="259" y="678" id="529" />
 <AutomaticDrawing  data="true" />
 </CONNECTOR>
@@ -518,12 +518,12 @@
 </COMPONENT>
 <SUBCOMPONENT type="1401" id="250" >
 <father id="350" num="0" />
-<cdparam x="370" y="768" />
-<sizeparam width="293" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="340" y="823" />
+<sizeparam width="323" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <enabled value="true" />
-<cdrectangleparam minX="0" maxX="10" minY="0" maxY="205" />
-<infoparam name="TGComponent" value="RedirectHTTPRequestFromBankToFakeBank" />
+<cdrectangleparam minX="0" maxX="-20" minY="0" maxY="205" />
+<infoparam name="TGComponent" value="RequestUserToInstallMobileFakeBankApplication" />
 <TGConnectingPoint num="0" id="226" />
 <TGConnectingPoint num="1" id="227" />
 <TGConnectingPoint num="2" id="228" />
@@ -554,12 +554,12 @@
 </SUBCOMPONENT>
 <SUBCOMPONENT type="1401" id="275" >
 <father id="350" num="1" />
-<cdparam x="448" y="716" />
-<sizeparam width="152" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="395" y="871" />
+<sizeparam width="134" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <enabled value="true" />
-<cdrectangleparam minX="0" maxX="151" minY="0" maxY="205" />
-<infoparam name="TGComponent" value="InstallMaliciousPlugin" />
+<cdrectangleparam minX="0" maxX="169" minY="0" maxY="205" />
+<infoparam name="TGComponent" value="ExploitVunerability" />
 <TGConnectingPoint num="0" id="251" />
 <TGConnectingPoint num="1" id="252" />
 <TGConnectingPoint num="2" id="253" />
@@ -590,12 +590,12 @@
 </SUBCOMPONENT>
 <SUBCOMPONENT type="1401" id="300" >
 <father id="350" num="2" />
-<cdparam x="395" y="871" />
-<sizeparam width="134" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="448" y="716" />
+<sizeparam width="152" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <enabled value="true" />
-<cdrectangleparam minX="0" maxX="169" minY="0" maxY="205" />
-<infoparam name="TGComponent" value="ExploitVunerability" />
+<cdrectangleparam minX="0" maxX="151" minY="0" maxY="205" />
+<infoparam name="TGComponent" value="InstallMaliciousPlugin" />
 <TGConnectingPoint num="0" id="276" />
 <TGConnectingPoint num="1" id="277" />
 <TGConnectingPoint num="2" id="278" />
@@ -626,12 +626,12 @@
 </SUBCOMPONENT>
 <SUBCOMPONENT type="1401" id="325" >
 <father id="350" num="3" />
-<cdparam x="340" y="823" />
-<sizeparam width="323" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="370" y="768" />
+<sizeparam width="293" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <enabled value="true" />
-<cdrectangleparam minX="0" maxX="-20" minY="0" maxY="205" />
-<infoparam name="TGComponent" value="RequestUserToInstallMobileFakeBankApplication" />
+<cdrectangleparam minX="0" maxX="10" minY="0" maxY="205" />
+<infoparam name="TGComponent" value="RedirectHTTPRequestFromBankToFakeBank" />
 <TGConnectingPoint num="0" id="301" />
 <TGConnectingPoint num="1" id="302" />
 <TGConnectingPoint num="2" id="303" />
@@ -694,12 +694,12 @@
 </COMPONENT>
 <SUBCOMPONENT type="1401" id="375" >
 <father id="450" num="0" />
-<cdparam x="838" y="783" />
-<sizeparam width="223" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="873" y="720" />
+<sizeparam width="147" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <enabled value="true" />
-<cdrectangleparam minX="0" maxX="1" minY="0" maxY="296" />
-<infoparam name="TGComponent" value="UserInstallsFakeBankApplication" />
+<cdrectangleparam minX="0" maxX="77" minY="0" maxY="296" />
+<infoparam name="TGComponent" value="SilentlyInterceptSMS" />
 <TGConnectingPoint num="0" id="351" />
 <TGConnectingPoint num="1" id="352" />
 <TGConnectingPoint num="2" id="353" />
@@ -766,12 +766,12 @@
 </SUBCOMPONENT>
 <SUBCOMPONENT type="1401" id="425" >
 <father id="450" num="2" />
-<cdparam x="873" y="720" />
-<sizeparam width="147" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="838" y="783" />
+<sizeparam width="223" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <enabled value="true" />
-<cdrectangleparam minX="0" maxX="77" minY="0" maxY="296" />
-<infoparam name="TGComponent" value="SilentlyInterceptSMS" />
+<cdrectangleparam minX="0" maxX="1" minY="0" maxY="296" />
+<infoparam name="TGComponent" value="UserInstallsFakeBankApplication" />
 <TGConnectingPoint num="0" id="401" />
 <TGConnectingPoint num="1" id="402" />
 <TGConnectingPoint num="2" id="403" />
@@ -834,12 +834,12 @@
 </COMPONENT>
 <SUBCOMPONENT type="1401" id="475" >
 <father id="525" num="0" />
-<cdparam x="199" y="747" />
-<sizeparam width="100" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="176" y="795" />
+<sizeparam width="137" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <enabled value="true" />
-<cdrectangleparam minX="0" maxX="44" minY="0" maxY="93" />
-<infoparam name="TGComponent" value="InstallTrojan" />
+<cdrectangleparam minX="0" maxX="7" minY="0" maxY="93" />
+<infoparam name="TGComponent" value="ExploitVulnerability" />
 <TGConnectingPoint num="0" id="451" />
 <TGConnectingPoint num="1" id="452" />
 <TGConnectingPoint num="2" id="453" />
@@ -870,12 +870,12 @@
 </SUBCOMPONENT>
 <SUBCOMPONENT type="1401" id="500" >
 <father id="525" num="1" />
-<cdparam x="176" y="795" />
-<sizeparam width="137" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="199" y="747" />
+<sizeparam width="100" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <enabled value="true" />
-<cdrectangleparam minX="0" maxX="7" minY="0" maxY="93" />
-<infoparam name="TGComponent" value="ExploitVulnerability" />
+<cdrectangleparam minX="0" maxX="44" minY="0" maxY="93" />
+<infoparam name="TGComponent" value="InstallTrojan" />
 <TGConnectingPoint num="0" id="476" />
 <TGConnectingPoint num="1" id="477" />
 <TGConnectingPoint num="2" id="478" />
@@ -1006,12 +1006,12 @@
 </COMPONENT>
 <SUBCOMPONENT type="1401" id="600" >
 <father id="726" num="0" />
-<cdparam x="674" y="418" />
-<sizeparam width="131" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="668" y="215" />
+<sizeparam width="306" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <enabled value="true" />
-<cdrectangleparam minX="0" maxX="260" minY="0" maxY="264" />
-<infoparam name="TGComponent" value="SendTANToServer" />
+<cdrectangleparam minX="0" maxX="85" minY="0" maxY="264" />
+<infoparam name="TGComponent" value="IllegalBankAccountTransactionBasedOnToken" />
 <TGConnectingPoint num="0" id="576" />
 <TGConnectingPoint num="1" id="577" />
 <TGConnectingPoint num="2" id="578" />
@@ -1036,17 +1036,19 @@
 <TGConnectingPoint num="21" id="597" />
 <TGConnectingPoint num="22" id="598" />
 <TGConnectingPoint num="23" id="599" />
+<accessibility />
 <extraparam>
-<info description="blah blah blah" root="false" />
+<info description="blah blah blah" root="true" />
 </extraparam>
 </SUBCOMPONENT>
-<SUBCOMPONENT type="1402" id="613" >
+<SUBCOMPONENT type="1401" id="625" >
 <father id="726" num="1" />
-<cdparam x="800" y="279" />
-<sizeparam width="123" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="676" y="347" />
+<sizeparam width="141" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
-<cdrectangleparam minX="0" maxX="245" minY="0" maxY="264" />
-<infoparam name="TGComponent" value="&lt;&lt;SEQUENCE&gt;&gt;" />
+<enabled value="true" />
+<cdrectangleparam minX="0" maxX="250" minY="0" maxY="264" />
+<infoparam name="TGComponent" value="LogOnBankAccount" />
 <TGConnectingPoint num="0" id="601" />
 <TGConnectingPoint num="1" id="602" />
 <TGConnectingPoint num="2" id="603" />
@@ -1059,114 +1061,112 @@
 <TGConnectingPoint num="9" id="610" />
 <TGConnectingPoint num="10" id="611" />
 <TGConnectingPoint num="11" id="612" />
+<TGConnectingPoint num="12" id="613" />
+<TGConnectingPoint num="13" id="614" />
+<TGConnectingPoint num="14" id="615" />
+<TGConnectingPoint num="15" id="616" />
+<TGConnectingPoint num="16" id="617" />
+<TGConnectingPoint num="17" id="618" />
+<TGConnectingPoint num="18" id="619" />
+<TGConnectingPoint num="19" id="620" />
+<TGConnectingPoint num="20" id="621" />
+<TGConnectingPoint num="21" id="622" />
+<TGConnectingPoint num="22" id="623" />
+<TGConnectingPoint num="23" id="624" />
 <extraparam>
-<info equation="" />
+<info description="blah blah blah" root="false" />
 </extraparam>
 </SUBCOMPONENT>
-<SUBCOMPONENT type="1402" id="626" >
+<SUBCOMPONENT type="1401" id="650" >
 <father id="726" num="2" />
-<cdparam x="877" y="416" />
-<sizeparam width="123" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<hidden value="false" />
-<cdrectangleparam minX="0" maxX="245" minY="0" maxY="264" />
-<infoparam name="TGComponent" value="&lt;&lt;BEFORE&gt;&gt;" />
-<TGConnectingPoint num="0" id="614" />
-<TGConnectingPoint num="1" id="615" />
-<TGConnectingPoint num="2" id="616" />
-<TGConnectingPoint num="3" id="617" />
-<TGConnectingPoint num="4" id="618" />
-<TGConnectingPoint num="5" id="619" />
-<TGConnectingPoint num="6" id="620" />
-<TGConnectingPoint num="7" id="621" />
-<TGConnectingPoint num="8" id="622" />
-<TGConnectingPoint num="9" id="623" />
-<TGConnectingPoint num="10" id="624" />
-<TGConnectingPoint num="11" id="625" />
-<extraparam>
-<info equation="120" />
-</extraparam>
-</SUBCOMPONENT>
-<SUBCOMPONENT type="1401" id="651" >
-<father id="726" num="3" />
 <cdparam x="818" y="347" />
 <sizeparam width="238" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <enabled value="true" />
 <cdrectangleparam minX="0" maxX="153" minY="0" maxY="264" />
 <infoparam name="TGComponent" value="PerformTokenBasedAuthentication" />
-<TGConnectingPoint num="0" id="627" />
-<TGConnectingPoint num="1" id="628" />
-<TGConnectingPoint num="2" id="629" />
-<TGConnectingPoint num="3" id="630" />
-<TGConnectingPoint num="4" id="631" />
-<TGConnectingPoint num="5" id="632" />
-<TGConnectingPoint num="6" id="633" />
-<TGConnectingPoint num="7" id="634" />
-<TGConnectingPoint num="8" id="635" />
-<TGConnectingPoint num="9" id="636" />
-<TGConnectingPoint num="10" id="637" />
-<TGConnectingPoint num="11" id="638" />
-<TGConnectingPoint num="12" id="639" />
-<TGConnectingPoint num="13" id="640" />
-<TGConnectingPoint num="14" id="641" />
-<TGConnectingPoint num="15" id="642" />
-<TGConnectingPoint num="16" id="643" />
-<TGConnectingPoint num="17" id="644" />
-<TGConnectingPoint num="18" id="645" />
-<TGConnectingPoint num="19" id="646" />
-<TGConnectingPoint num="20" id="647" />
-<TGConnectingPoint num="21" id="648" />
-<TGConnectingPoint num="22" id="649" />
-<TGConnectingPoint num="23" id="650" />
-<latencyCheck />
+<TGConnectingPoint num="0" id="626" />
+<TGConnectingPoint num="1" id="627" />
+<TGConnectingPoint num="2" id="628" />
+<TGConnectingPoint num="3" id="629" />
+<TGConnectingPoint num="4" id="630" />
+<TGConnectingPoint num="5" id="631" />
+<TGConnectingPoint num="6" id="632" />
+<TGConnectingPoint num="7" id="633" />
+<TGConnectingPoint num="8" id="634" />
+<TGConnectingPoint num="9" id="635" />
+<TGConnectingPoint num="10" id="636" />
+<TGConnectingPoint num="11" id="637" />
+<TGConnectingPoint num="12" id="638" />
+<TGConnectingPoint num="13" id="639" />
+<TGConnectingPoint num="14" id="640" />
+<TGConnectingPoint num="15" id="641" />
+<TGConnectingPoint num="16" id="642" />
+<TGConnectingPoint num="17" id="643" />
+<TGConnectingPoint num="18" id="644" />
+<TGConnectingPoint num="19" id="645" />
+<TGConnectingPoint num="20" id="646" />
+<TGConnectingPoint num="21" id="647" />
+<TGConnectingPoint num="22" id="648" />
+<TGConnectingPoint num="23" id="649" />
 <extraparam>
 <info description="blah blah blah" root="false" />
 </extraparam>
 </SUBCOMPONENT>
-<SUBCOMPONENT type="1401" id="676" >
+<SUBCOMPONENT type="1402" id="663" >
+<father id="726" num="3" />
+<cdparam x="877" y="416" />
+<sizeparam width="123" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="0" maxX="245" minY="0" maxY="264" />
+<infoparam name="TGComponent" value="&lt;&lt;BEFORE&gt;&gt;" />
+<TGConnectingPoint num="0" id="651" />
+<TGConnectingPoint num="1" id="652" />
+<TGConnectingPoint num="2" id="653" />
+<TGConnectingPoint num="3" id="654" />
+<TGConnectingPoint num="4" id="655" />
+<TGConnectingPoint num="5" id="656" />
+<TGConnectingPoint num="6" id="657" />
+<TGConnectingPoint num="7" id="658" />
+<TGConnectingPoint num="8" id="659" />
+<TGConnectingPoint num="9" id="660" />
+<TGConnectingPoint num="10" id="661" />
+<TGConnectingPoint num="11" id="662" />
+<extraparam>
+<info equation="120" />
+</extraparam>
+</SUBCOMPONENT>
+<SUBCOMPONENT type="1402" id="676" >
 <father id="726" num="4" />
-<cdparam x="676" y="347" />
-<sizeparam width="141" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="800" y="279" />
+<sizeparam width="123" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
-<enabled value="true" />
-<cdrectangleparam minX="0" maxX="250" minY="0" maxY="264" />
-<infoparam name="TGComponent" value="LogOnBankAccount" />
-<TGConnectingPoint num="0" id="652" />
-<TGConnectingPoint num="1" id="653" />
-<TGConnectingPoint num="2" id="654" />
-<TGConnectingPoint num="3" id="655" />
-<TGConnectingPoint num="4" id="656" />
-<TGConnectingPoint num="5" id="657" />
-<TGConnectingPoint num="6" id="658" />
-<TGConnectingPoint num="7" id="659" />
-<TGConnectingPoint num="8" id="660" />
-<TGConnectingPoint num="9" id="661" />
-<TGConnectingPoint num="10" id="662" />
-<TGConnectingPoint num="11" id="663" />
-<TGConnectingPoint num="12" id="664" />
-<TGConnectingPoint num="13" id="665" />
-<TGConnectingPoint num="14" id="666" />
-<TGConnectingPoint num="15" id="667" />
-<TGConnectingPoint num="16" id="668" />
-<TGConnectingPoint num="17" id="669" />
-<TGConnectingPoint num="18" id="670" />
-<TGConnectingPoint num="19" id="671" />
-<TGConnectingPoint num="20" id="672" />
-<TGConnectingPoint num="21" id="673" />
-<TGConnectingPoint num="22" id="674" />
-<TGConnectingPoint num="23" id="675" />
+<cdrectangleparam minX="0" maxX="245" minY="0" maxY="264" />
+<infoparam name="TGComponent" value="&lt;&lt;SEQUENCE&gt;&gt;" />
+<TGConnectingPoint num="0" id="664" />
+<TGConnectingPoint num="1" id="665" />
+<TGConnectingPoint num="2" id="666" />
+<TGConnectingPoint num="3" id="667" />
+<TGConnectingPoint num="4" id="668" />
+<TGConnectingPoint num="5" id="669" />
+<TGConnectingPoint num="6" id="670" />
+<TGConnectingPoint num="7" id="671" />
+<TGConnectingPoint num="8" id="672" />
+<TGConnectingPoint num="9" id="673" />
+<TGConnectingPoint num="10" id="674" />
+<TGConnectingPoint num="11" id="675" />
 <extraparam>
-<info description="blah blah blah" root="false" />
+<info equation="" />
 </extraparam>
 </SUBCOMPONENT>
 <SUBCOMPONENT type="1401" id="701" >
 <father id="726" num="5" />
-<cdparam x="668" y="215" />
-<sizeparam width="306" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="674" y="418" />
+<sizeparam width="131" height="35" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
 <hidden value="false" />
 <enabled value="true" />
-<cdrectangleparam minX="0" maxX="85" minY="0" maxY="264" />
-<infoparam name="TGComponent" value="IllegalBankAccountTransactionBasedOnToken" />
+<cdrectangleparam minX="0" maxX="260" minY="0" maxY="264" />
+<infoparam name="TGComponent" value="SendTANToServer" />
 <TGConnectingPoint num="0" id="677" />
 <TGConnectingPoint num="1" id="678" />
 <TGConnectingPoint num="2" id="679" />
@@ -1191,9 +1191,8 @@
 <TGConnectingPoint num="21" id="698" />
 <TGConnectingPoint num="22" id="699" />
 <TGConnectingPoint num="23" id="700" />
-<accessibility />
 <extraparam>
-<info description="blah blah blah" root="true" />
+<info description="blah blah blah" root="false" />
 </extraparam>
 </SUBCOMPONENT>
 
@@ -1305,4 +1304,4 @@
 
 
 
-</TURTLEGMODELING>
\ No newline at end of file
+</TURTLEGMODELING>
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index cb4d8d0218..c16130ad09 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -8426,6 +8426,21 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
         return null;
     }
 
+    public void resetReachability() {
+        TURTLEPanel tp = getCurrentTURTLEPanel();
+        if (tp != null) {
+            tp.resetReachability();
+        }
+    }
+
+    public void resetLiveness() {
+        TURTLEPanel tp = getCurrentTURTLEPanel();
+        if (tp != null) {
+            tp.resetReachability();
+        }
+    }
+
+
     public synchronized void resetRunningID() {
         if (runningIDs != null) {
             runningIDs.clear();
diff --git a/src/main/java/ui/TDiagramPanel.java b/src/main/java/ui/TDiagramPanel.java
index db7989072f..fec3f64ba4 100755
--- a/src/main/java/ui/TDiagramPanel.java
+++ b/src/main/java/ui/TDiagramPanel.java
@@ -3341,6 +3341,18 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
             tgc.setDIPLOID(-1);
     }
 
+    public void resetReachability () {
+        for (TGComponent tgc: this.componentList)
+            tgc.setReachability(TGComponent.ACCESSIBILITY_UNKNOWN);;
+    }
+
+    public void resetLiveness () {
+        for (TGComponent tgc: this.componentList)
+            tgc.setReachability(TGComponent.ACCESSIBILITY_UNKNOWN);;
+    }
+
+
+
     public void getListOfBreakPoints( java.util.List<Point> points, int taskID) {
         for (TGComponent tgc: this.componentList)
             if (tgc.getBreakpoint() && (tgc.getDIPLOID() != -1)) {
diff --git a/src/main/java/ui/TURTLEPanel.java b/src/main/java/ui/TURTLEPanel.java
index 0995f4f84d..d015334a59 100755
--- a/src/main/java/ui/TURTLEPanel.java
+++ b/src/main/java/ui/TURTLEPanel.java
@@ -373,6 +373,18 @@ public abstract class TURTLEPanel implements GenericTree {
         }
     }
 
+    public void resetReachability() {
+        for (int i = 0; i < panels.size(); i++) {
+            panelAt(i).resetReachability();
+        }
+    }
+
+    public void resetLiveness() {
+        for (int i = 0; i < panels.size(); i++) {
+            panelAt(i).resetLiveness();
+        }
+    }
+
     public void searchForText(String text, Vector<Object> elements) {
         if (panelAt(0) != null) {
             String s = saveHeaderInXml(null).toLowerCase();
@@ -406,5 +418,4 @@ public abstract class TURTLEPanel implements GenericTree {
         return false;
     }
 
-
 }
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 333ddba367..285e898807 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -514,6 +514,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
             // Reachability
             int res;
             if (reachabilitySelected == REACHABILITY_SELECTED) {
+                mgui.resetReachability();
                 res = amc.setReachabilityOfSelected();
                 jta.append("Reachability of " + res + " selected elements activated\n");
 
@@ -526,6 +527,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
             }
 
             if (reachabilitySelected == REACHABILITY_ALL) {
+                mgui.resetReachability();
                 res = amc.setReachabilityOfAllStates();
                 jta.append("Reachability of " + res + " states activated\n");
                 for (SpecificationReachability sr : amc.getReachabilities()) {
@@ -645,7 +647,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
             Object o = ((AvatarStateMachineElement) _o).getReferenceObject();
             if (o instanceof TGComponent) {
                 TGComponent tgc = (TGComponent) (o);
-                TraceManager.addDev("Reachability of tgc=" + tgc + " value=" + tgc.getValue() + " class=" + tgc.getClass());
+                //TraceManager.addDev("Reachability of tgc=" + tgc + " value=" + tgc.getValue() + " class=" + tgc.getClass());
                 switch (_res) {
                     case NOTCOMPUTED:
                         tgc.setReachability(TGComponent.ACCESSIBILITY_UNKNOWN);
diff --git a/src/main/java/ui/window/JDialogUPPAALValidation.java b/src/main/java/ui/window/JDialogUPPAALValidation.java
index e6366456d5..bbb3088f2e 100755
--- a/src/main/java/ui/window/JDialogUPPAALValidation.java
+++ b/src/main/java/ui/window/JDialogUPPAALValidation.java
@@ -367,7 +367,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
         stateL.setToolTipText("Study the fact that, if accessed,  a given state is eventually followed by another one");
         jp1.add(stateL, c1);
         stateL.setSelected(stateLChecked);*/
-	
+
         c1.gridwidth = GridBagConstraints.REMAINDER;
         custom = new JCheckBox("Safety pragmas");
         custom.addActionListener(this);
@@ -575,6 +575,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
             }
 
             if ((stateR_Selected.isSelected() || stateR_All.isSelected()) && (mode != NOT_STARTED)) {
+                mgui.resetReachability();
                 java.util.List<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp, stateR_All.isSelected());
 
                 if ((list != null) && (list.size() > 0)){
@@ -615,6 +616,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
             }
 
             if ((stateL_Selected.isSelected()|| stateL_All.isSelected()) && (mode != NOT_STARTED)) {
+                mgui.resetLiveness();
                 java.util.List<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp, stateL_All.isSelected());
                 if ((list != null) && (list.size() > 0)){
                     for(TGComponentAndUPPAALQuery cq: list) {
@@ -650,6 +652,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
                     jta.append("Liveness: No selected component found on diagrams\n\n");
                 }
             }
+
             if (stateLe_Selected.isSelected() && (mode != NOT_STARTED)) {
                 java.util.List<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
                 String s1, s2, name1, name2, query1, query2;
@@ -758,7 +761,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
         setButtons();
     }
 
-    
+
     private String translateCustomQuery(String query){
         UPPAALSpec spec = mgui.gtm.getLastUPPAALSpecification();
         AVATAR2UPPAAL avatar2uppaal = mgui.gtm.getAvatar2Uppaal();
@@ -971,7 +974,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
             //stateA.setEnabled(true);
 	    stateLe_None.setEnabled(true);
             stateLe_Selected.setEnabled(true);
-	    
+
             generateTrace.setEnabled(true);
             showDetails.setEnabled(true);
             for (JCheckBox cb: customChecks){
@@ -993,7 +996,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
 			}
 			start.setEnabled(selected);
 		    }
-		    
+
 		} else {
 		    start.setEnabled(false);
 		}
-- 
GitLab