diff --git a/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml b/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml
index 6e267401d56a62df20ee72b344db0a41cfb6cd04..572ffcb301d250ac67f55e3598bea644ba1f7b47 100644
--- a/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml
+++ b/modeling/MicroWaveOven_SafetySecurity_fullMethodo.xml
@@ -4239,7 +4239,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="2157" >
<father id="2164" num="0" />
<cdparam x="127" y="638" />
-<sizeparam width="44" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="39" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-75" maxX="-20" minY="10" maxY="35" />
<infoparam name="guard 1" value="[ else ]" />
@@ -4247,7 +4247,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="2158" >
<father id="2164" num="1" />
<cdparam x="219" y="638" />
-<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="12" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="35" maxX="55" minY="10" maxY="35" />
<infoparam name="guard 2" value="[ ]" />
@@ -4255,7 +4255,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="2159" >
<father id="2164" num="2" />
<cdparam x="222" y="673" />
-<sizeparam width="146" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="135" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="20" maxX="40" minY="45" maxY="70" />
<infoparam name="guard 3" value="[ cookingTimeElapsed ]" />
@@ -4371,7 +4371,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="2247" >
<father id="2254" num="0" />
<cdparam x="254" y="473" />
-<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="12" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-75" maxX="-20" minY="10" maxY="35" />
<infoparam name="guard 1" value="[ ]" />
@@ -4379,7 +4379,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="2248" >
<father id="2254" num="1" />
<cdparam x="314" y="473" />
-<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="12" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="35" maxX="55" minY="10" maxY="35" />
<infoparam name="guard 2" value="[ ]" />
@@ -4387,7 +4387,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="2249" >
<father id="2254" num="2" />
<cdparam x="299" y="508" />
-<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="12" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="20" maxX="40" minY="45" maxY="70" />
<infoparam name="guard 3" value="[ ]" />
@@ -4581,7 +4581,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="2401" >
<father id="2408" num="0" />
<cdparam x="346" y="183" />
-<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="12" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-75" maxX="-20" minY="10" maxY="35" />
<infoparam name="guard 1" value="[ ]" />
@@ -4589,7 +4589,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="2402" >
<father id="2408" num="1" />
<cdparam x="406" y="183" />
-<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="12" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="35" maxX="55" minY="10" maxY="35" />
<infoparam name="guard 2" value="[ ]" />
@@ -4597,7 +4597,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="2403" >
<father id="2408" num="2" />
<cdparam x="391" y="218" />
-<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="12" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="20" maxX="40" minY="45" maxY="70" />
<infoparam name="guard 3" value="[ ]" />
@@ -5038,7 +5038,7 @@ or by a maintenance station
<MainCode value=" }"/>
<MainCode value=""/>
<MainCode value="}"/>
-<Optimized value="true" />
+<Optimized value="false" />
<Validated value="ObserverProp1;RemotelyControlledMicrowave;MicroWaveOven;WirelessInterface;Door;Magnetron;Controller;ControlPanel;Bell;RemoteControl;" />
<Ignored value="" />
@@ -5174,7 +5174,7 @@ or by a maintenance station
</CONNECTOR>
<COMPONENT type="302" id="2683" >
<cdparam x="382" y="26" />
-<sizeparam width="668" height="97" minWidth="80" minHeight="10" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="616" height="97" minWidth="80" minHeight="10" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
<infoparam name="Proverif Pragma" value="#InitialSystemKnowledge RemoteControl.PSK WirelessInterface.PSK
@@ -6739,7 +6739,7 @@ or by a maintenance station
</CONNECTOR><SUBCOMPONENT type="-1" id="3406" >
<father id="3408" num="0" />
<cdparam x="407" y="249" />
-<sizeparam width="52" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="47" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -6768,7 +6768,7 @@ or by a maintenance station
</CONNECTOR><SUBCOMPONENT type="-1" id="3413" >
<father id="3415" num="0" />
<cdparam x="414" y="365" />
-<sizeparam width="64" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="59" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -6826,7 +6826,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="3423" >
<father id="3428" num="3" />
<cdparam x="246" y="301" />
-<sizeparam width="53" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="47" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -6855,7 +6855,7 @@ or by a maintenance station
</CONNECTOR><SUBCOMPONENT type="-1" id="3433" >
<father id="3435" num="0" />
<cdparam x="412" y="172" />
-<sizeparam width="64" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="59" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -6952,8 +6952,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="3494" >
-<cdparam x="377" y="379" />
-<sizeparam width="61" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="380" y="379" />
+<sizeparam width="55" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="closed()" />
@@ -6970,8 +6970,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="3505" >
-<cdparam x="381" y="184" />
-<sizeparam width="52" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="384" y="184" />
+<sizeparam width="47" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="open()" />
@@ -7923,7 +7923,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="3828" >
<father id="3833" num="3" />
<cdparam x="158" y="477" />
-<sizeparam width="212" height="60" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="205" height="60" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -7953,7 +7953,7 @@ or by a maintenance station
</CONNECTOR><SUBCOMPONENT type="-1" id="3838" >
<father id="3840" num="0" />
<cdparam x="513" y="302" />
-<sizeparam width="208" height="60" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="201" height="60" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -7983,7 +7983,7 @@ or by a maintenance station
</CONNECTOR><SUBCOMPONENT type="-1" id="3845" >
<father id="3847" num="0" />
<cdparam x="397" y="475" />
-<sizeparam width="137" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="130" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -8011,7 +8011,7 @@ or by a maintenance station
</CONNECTOR><SUBCOMPONENT type="-1" id="3852" >
<father id="3854" num="0" />
<cdparam x="252" y="341" />
-<sizeparam width="181" height="30" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="166" height="30" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -8081,7 +8081,7 @@ or by a maintenance station
<SUBCOMPONENT type="-1" id="3863" >
<father id="3869" num="4" />
<cdparam x="448" y="590" />
-<sizeparam width="64" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="59" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -8239,8 +8239,8 @@ or by a maintenance station
</SUBCOMPONENT>
<COMPONENT type="5103" id="3915" >
-<cdparam x="597" y="562" />
-<sizeparam width="149" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="605" y="562" />
+<sizeparam width="133" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="obs_magnetronStart()" />
@@ -8257,8 +8257,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="3926" >
-<cdparam x="626" y="493" />
-<sizeparam width="90" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="630" y="493" />
+<sizeparam width="82" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="obs_closed()" />
@@ -8275,8 +8275,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="3937" >
-<cdparam x="631" y="307" />
-<sizeparam width="81" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="634" y="307" />
+<sizeparam width="74" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="obs_open()" />
@@ -8293,8 +8293,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="3948" >
-<cdparam x="616" y="185" />
-<sizeparam width="90" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="620" y="185" />
+<sizeparam width="82" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="obs_closed()" />
@@ -8311,8 +8311,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="3959" >
-<cdparam x="621" y="70" />
-<sizeparam width="81" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="624" y="70" />
+<sizeparam width="74" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="obs_open()" />
@@ -8380,8 +8380,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5104" id="4011" >
-<cdparam x="279" y="184" />
-<sizeparam width="157" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="287" y="184" />
+<sizeparam width="141" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Receive signal" value="remoteStart(duration)" />
@@ -8398,8 +8398,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5104" id="4022" >
-<cdparam x="640" y="262" />
-<sizeparam width="60" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="643" y="262" />
+<sizeparam width="55" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Receive signal" value="open()" />
@@ -8467,8 +8467,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="4074" >
-<cdparam x="395" y="554" />
-<sizeparam width="66" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="398" y="554" />
+<sizeparam width="60" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="ringBell()" />
@@ -8486,8 +8486,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5104" id="4085" >
-<cdparam x="631" y="36" />
-<sizeparam width="60" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="634" y="36" />
+<sizeparam width="55" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="open()" />
@@ -8555,8 +8555,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5104" id="4137" >
-<cdparam x="437" y="183" />
-<sizeparam width="111" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="442" y="183" />
+<sizeparam width="100" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="start(duration)" />
@@ -8582,8 +8582,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="4150" >
-<cdparam x="613" y="350" />
-<sizeparam width="116" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="619" y="350" />
+<sizeparam width="104" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="stopMagnetron()" />
@@ -8600,8 +8600,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="4161" >
-<cdparam x="370" y="512" />
-<sizeparam width="116" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="376" y="512" />
+<sizeparam width="104" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="stopMagnetron()" />
@@ -8618,8 +8618,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="4172" >
-<cdparam x="612" y="527" />
-<sizeparam width="118" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="619" y="527" />
+<sizeparam width="105" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="startMagnetron()" />
@@ -8636,8 +8636,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="4183" >
-<cdparam x="369" y="309" />
-<sizeparam width="118" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="376" y="309" />
+<sizeparam width="105" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="startMagnetron()" />
@@ -8654,8 +8654,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5104" id="4194" >
-<cdparam x="637" y="460" />
-<sizeparam width="69" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="640" y="460" />
+<sizeparam width="63" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="closed()" />
@@ -8672,8 +8672,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5104" id="4205" >
-<cdparam x="627" y="150" />
-<sizeparam width="69" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="630" y="150" />
+<sizeparam width="63" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="closed()" />
@@ -8791,8 +8791,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="4298" >
-<cdparam x="354" y="355" />
-<sizeparam width="149" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="362" y="355" />
+<sizeparam width="133" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="obs_magnetronStart()" />
@@ -8809,7 +8809,7 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5106" id="4339" >
-<cdparam x="251" y="240" />
+<cdparam x="237" y="234" />
<sizeparam width="543" height="394" minWidth="40" minHeight="30" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
@@ -9256,6 +9256,7 @@ or by a maintenance station
<TGConnectingPoint num="37" id="4494" />
<TGConnectingPoint num="38" id="4495" />
<TGConnectingPoint num="39" id="4496" />
+<accessibility />
<extraparam>
<entryCode value="" />
<entryCode value="printf("\nDRING DRING DRING !!!!\n\n");" />
@@ -9326,6 +9327,7 @@ or by a maintenance station
<TGConnectingPoint num="37" id="4546" />
<TGConnectingPoint num="38" id="4547" />
<TGConnectingPoint num="39" id="4548" />
+<accessibility />
<extraparam>
</extraparam>
</COMPONENT>
@@ -9347,7 +9349,7 @@ or by a maintenance station
<cdparam x="516" y="268" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector from List of all parameters of an Avatar SMD transition to UML Note" value="null" />
-<P1 x="516" y="129" id="4555" />
+<P1 x="503" y="132" id="4555" />
<P2 x="661" y="85" id="4625" />
<AutomaticDrawing data="false" />
</CONNECTOR>
@@ -9362,7 +9364,7 @@ or by a maintenance station
</CONNECTOR><SUBCOMPONENT type="-1" id="4557" >
<father id="4559" num="0" />
<cdparam x="343" y="131" />
-<sizeparam width="173" height="30" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="160" height="30" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -9443,11 +9445,11 @@ or by a maintenance station
<infoparam name="connector" value="null" />
<TGConnectingPoint num="0" id="4579" />
<P1 x="373" y="427" id="4587" />
-<P2 x="375" y="442" id="4680" />
+<P2 x="373" y="494" id="4680" />
<AutomaticDrawing data="true" />
</CONNECTOR><SUBCOMPONENT type="-1" id="4578" >
<father id="4580" num="0" />
-<cdparam x="373" y="467" />
+<cdparam x="382" y="458" />
<sizeparam width="10" height="15" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
@@ -9517,7 +9519,7 @@ or by a maintenance station
<COMPONENT type="301" id="4638" >
<cdparam x="661" y="78" />
-<sizeparam width="271" height="15" minWidth="50" minHeight="20" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="251" height="15" minWidth="50" minHeight="20" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="UML Note" value="Encrypting data with the pre shared key
@@ -9594,7 +9596,7 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5101" id="4681" >
-<cdparam x="365" y="447" />
+<cdparam x="363" y="499" />
<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
@@ -9603,8 +9605,8 @@ or by a maintenance station
</COMPONENT>
<COMPONENT type="5103" id="4692" >
-<cdparam x="258" y="296" />
-<sizeparam width="179" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="266" y="296" />
+<sizeparam width="163" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="wirelessChannelWrite(msg)" />
diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java
index 3fcf2e016f848550594a4d72689560f1a2707ad5..b6f4df7ce885be5b735e3a03a30f712c9996429a 100644
--- a/src/avatartranslator/AvatarStateMachine.java
+++ b/src/avatartranslator/AvatarStateMachine.java
@@ -1577,7 +1577,7 @@ public class AvatarStateMachine extends AvatarElement {
AvatarTransition at = (AvatarTransition)(elt.getNext(0));
if (at.getNext(0) instanceof AvatarStateElement) {
if (at.isEmpty() && at.hasNonDeterministicGuard()) {
- if ((_canOptimize) || (!(elt.isCheckable()))){
+ if ((_canOptimize) && (!(elt.isCheckable()))){
foundState1 = (AvatarStateElement) elt;
foundAt = at;
foundState2 = (AvatarStateElement)(at.getNext(0));
diff --git a/src/avatartranslator/modelchecker/AvatarModelChecker.java b/src/avatartranslator/modelchecker/AvatarModelChecker.java
index 57b40909b6f9083b398fb34229b39b5673019986..ed18a50fa9e39a9cb793fe42ac1c6be1beb4b26a 100644
--- a/src/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -180,7 +180,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
reachabilities = new ArrayList<SpecificationReachability>();
for(AvatarBlock block: spec.getListOfBlocks()) {
for(AvatarStateMachineElement elt: block.getStateMachine().getListOfElements()) {
- if (elt instanceof AvatarStateElement) {
+ if ((elt instanceof AvatarStateElement) || (elt.isCheckable())){
SpecificationReachability reach = new SpecificationReachability(elt, block);
reachabilities.add(reach);
}
@@ -407,7 +407,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
private synchronized void emptyPendingStates() {
- pendingStates.clear();
+ if (pendingStates != null) {
+ pendingStates.clear();
+ }
nbOfCurrentComputations = 0;
}
@@ -1161,6 +1163,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return new String(sb);
}
+ public ArrayList<SpecificationReachability> getAllReachabilities() {
+ return reachabilities;
+ }
+
public String reachabilityToString() {
if (!studyReachability) {
return "Reachability not activated";
diff --git a/src/ui/ColorManager.java b/src/ui/ColorManager.java
index e5180f2b65c62eb53fa2aea633fb6669b639c7e5..05ddc10a6aa705743e1816abdf553621a8b6d184 100755
--- a/src/ui/ColorManager.java
+++ b/src/ui/ColorManager.java
@@ -61,7 +61,7 @@ public class ColorManager {
public static final Color POINTER_ON_ME_0 = Color.red;
public static final Color ACCESSIBILITY = Color.red;
public static final Color ACCESSIBILITY_UNKNOWN = Color.DARK_GRAY;
- public static final Color ACCESSIBILITY_OK = Color.green;
+ public static final Color ACCESSIBILITY_OK = new Color(0, 232, 0);
public static final Color ACCESSIBILITY_KO = Color.red;
public static final Color MUTEX_OK = new Color(5, 100, 7);
public static final Color BREAKPOINT = new Color(13, 248, 18);
diff --git a/src/ui/TGComponent.java b/src/ui/TGComponent.java
index 7b788ab7fd62355c70e3e663d818902243d67f0f..baa55ecf926a6089829bc1a95d5abd17d8691002 100755
--- a/src/ui/TGComponent.java
+++ b/src/ui/TGComponent.java
@@ -909,6 +909,9 @@ public abstract class TGComponent implements CDElement, GenericTree {
public void drawAccessibility(int type, Graphics g, int _x, int _y, String value) {
Color c;
+ Color oldC = g.getColor();
+ Font f = g.getFont();
+ g.setFont(f.deriveFont(Font.BOLD));
switch(type) {
case ACCESSIBILITY_OK:
c = ColorManager.ACCESSIBILITY_OK;
@@ -919,9 +922,12 @@ public abstract class TGComponent implements CDElement, GenericTree {
default:
c = ColorManager.ACCESSIBILITY_UNKNOWN;
}
-
+
+ g.drawString(value, _x-1, _y-1);
g.setColor(c);
g.drawString(value, _x, _y);
+ g.setFont(f);
+ g.setColor(oldC);
}
@@ -947,7 +953,7 @@ public abstract class TGComponent implements CDElement, GenericTree {
drawOutFreeTGConnectingPointsCompatibleWith(g, getDefaultConnector());
}
- if (accessibility) {
+ if ((accessibility) || (reachability != ACCESSIBILITY_UNKNOWN) || (liveness != ACCESSIBILITY_UNKNOWN)) {
drawAccessibility(reachability, g, x+width-18, y-1, "R");
drawAccessibility(liveness, g, x+width-10, y-1, "L");
if ((reachability == ACCESSIBILITY_UNKNOWN) && (liveness == ACCESSIBILITY_UNKNOWN)) {
diff --git a/src/ui/window/JDialogAvatarModelChecker.java b/src/ui/window/JDialogAvatarModelChecker.java
index 24be3645dcc5ce421d8b3fb984a9f425db63a7bb..3bd2786ed66708487b58de539521fc9f360e09a4 100644
--- a/src/ui/window/JDialogAvatarModelChecker.java
+++ b/src/ui/window/JDialogAvatarModelChecker.java
@@ -66,12 +66,12 @@ import java.util.concurrent.TimeUnit;
public class JDialogAvatarModelChecker extends javax.swing.JDialog implements ActionListener, Runnable, MasterProcessInterface {
public final static String [] INFOS = {"Not started", "Running", "Stopped by user", "Finished"};
public final static Color [] COLORS = {Color.darkGray, Color.magenta, Color.red, Color.blue};
-
+
public final static int REACHABILITY_ALL = 1;
public final static int REACHABILITY_SELECTED = 2;
public final static int REACHABILITY_NONE = 3;
-
+
protected static String graphDir;
protected static boolean graphSelected = false;
protected static String graphDirDot;
@@ -79,7 +79,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
protected static boolean ignoreEmptyTransitionsSelected = true;
protected static boolean ignoreConcurrenceBetweenInternalActionsSelected = true;
protected static int reachabilitySelected = REACHABILITY_NONE;
-
+
protected MainGUI mgui;
protected final static int NOT_STARTED = 1;
@@ -106,10 +106,10 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
//protected ButtonGroup exegroup;
//protected JLabel gen, comp;
//protected JTextField code1, code2, unitcycle, compiler1, exe1, exe2, exe3, exe2int, loopLimit;
-
+
protected JRadioButton noReachability, reachabilityCheckable, reachabilityAllStates;
protected ButtonGroup reachabilities;
-
+
protected JCheckBox saveGraphAUT, saveGraphDot, ignoreEmptyTransitions, ignoreConcurrenceBetweenInternalActions;
protected JTextField graphPath, graphPathDot;
protected JTabbedPane jp1;
@@ -124,7 +124,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
private boolean hasError = false;
//protected boolean startProcess = false;
-
+
/** Creates new form */
@@ -132,16 +132,16 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
super(f, title, true);
mgui = _mgui;
- spec = _spec;
+ spec = _spec;
- if (graphDir == null) {
- graphDir = _graphDir + File.separator + "avatar.aut";
- }
- if (graphDirDot == null) {
- graphDirDot = _graphDir + File.separator + "avatar.dot";
- }
+ if (graphDir == null) {
+ graphDir = _graphDir + File.separator + "avatar.aut";
+ }
+ if (graphDirDot == null) {
+ graphDirDot = _graphDir + File.separator + "avatar.dot";
+ }
- initComponents();
+ initComponents();
myInitComponents();
pack();
@@ -169,55 +169,55 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
jp01.setLayout(gridbag01);
jp01.setBorder(new javax.swing.border.TitledBorder("Options"));
- c01.gridwidth = 1;
- c01.gridheight = 1;
- c01.weighty = 1.0;
- c01.weightx = 1.0;
- c01.fill = GridBagConstraints.HORIZONTAL;
- c01.gridwidth = GridBagConstraints.REMAINDER; //end row
- ignoreEmptyTransitions = new JCheckBox("Do not display empty transitions as internal actions", ignoreEmptyTransitionsSelected);
- ignoreEmptyTransitions.addActionListener(this);
- jp01.add(ignoreEmptyTransitions, c01);
- ignoreConcurrenceBetweenInternalActions = new JCheckBox("Ignore concurrency between internal actions", ignoreConcurrenceBetweenInternalActionsSelected);
- ignoreConcurrenceBetweenInternalActions.addActionListener(this);
- jp01.add(ignoreConcurrenceBetweenInternalActions, c01);
-
-
- // Reachability
- reachabilities = new ButtonGroup();
-
- noReachability = new JRadioButton("No reachability");
- noReachability.addActionListener(this);
- jp01.add(noReachability, c01);
- reachabilities.add(noReachability);
-
- reachabilityCheckable = new JRadioButton("Reachability of selected states");
- reachabilityCheckable.addActionListener(this);
- jp01.add(reachabilityCheckable, c01);
- reachabilities.add(reachabilityCheckable);
-
- reachabilityAllStates = new JRadioButton("Reachability of all states");
- reachabilityAllStates.addActionListener(this);
- jp01.add(reachabilityAllStates, c01);
- reachabilities.add(reachabilityAllStates);
-
- noReachability.setSelected(reachabilitySelected == REACHABILITY_NONE);
- reachabilityCheckable.setSelected(reachabilitySelected == REACHABILITY_SELECTED);
- reachabilityAllStates.setSelected(reachabilitySelected == REACHABILITY_ALL);
-
- // RG
- saveGraphAUT = new JCheckBox("Save RG (AUT format) in:", graphSelected);
- saveGraphAUT.addActionListener(this);
- jp01.add(saveGraphAUT, c01);
- graphPath = new JTextField(graphDir);
- jp01.add(graphPath, c01);
- saveGraphDot = new JCheckBox("Save RG (dotty format) in:", graphSelectedDot);
- saveGraphDot.addActionListener(this);
- jp01.add(saveGraphDot, c01);
- graphPathDot = new JTextField(graphDirDot);
- jp01.add(graphPathDot, c01);
- c.add(jp01, BorderLayout.NORTH);
-
+ c01.gridwidth = 1;
+ c01.gridheight = 1;
+ c01.weighty = 1.0;
+ c01.weightx = 1.0;
+ c01.fill = GridBagConstraints.HORIZONTAL;
+ c01.gridwidth = GridBagConstraints.REMAINDER; //end row
+ ignoreEmptyTransitions = new JCheckBox("Do not display empty transitions as internal actions", ignoreEmptyTransitionsSelected);
+ ignoreEmptyTransitions.addActionListener(this);
+ jp01.add(ignoreEmptyTransitions, c01);
+ ignoreConcurrenceBetweenInternalActions = new JCheckBox("Ignore concurrency between internal actions", ignoreConcurrenceBetweenInternalActionsSelected);
+ ignoreConcurrenceBetweenInternalActions.addActionListener(this);
+ jp01.add(ignoreConcurrenceBetweenInternalActions, c01);
+
+
+ // Reachability
+ reachabilities = new ButtonGroup();
+
+ noReachability = new JRadioButton("No reachability");
+ noReachability.addActionListener(this);
+ jp01.add(noReachability, c01);
+ reachabilities.add(noReachability);
+
+ reachabilityCheckable = new JRadioButton("Reachability of selected states");
+ reachabilityCheckable.addActionListener(this);
+ jp01.add(reachabilityCheckable, c01);
+ reachabilities.add(reachabilityCheckable);
+
+ reachabilityAllStates = new JRadioButton("Reachability of all states");
+ reachabilityAllStates.addActionListener(this);
+ jp01.add(reachabilityAllStates, c01);
+ reachabilities.add(reachabilityAllStates);
+
+ noReachability.setSelected(reachabilitySelected == REACHABILITY_NONE);
+ reachabilityCheckable.setSelected(reachabilitySelected == REACHABILITY_SELECTED);
+ reachabilityAllStates.setSelected(reachabilitySelected == REACHABILITY_ALL);
+
+ // RG
+ saveGraphAUT = new JCheckBox("Save RG (AUT format) in:", graphSelected);
+ saveGraphAUT.addActionListener(this);
+ jp01.add(saveGraphAUT, c01);
+ graphPath = new JTextField(graphDir);
+ jp01.add(graphPath, c01);
+ saveGraphDot = new JCheckBox("Save RG (dotty format) in:", graphSelectedDot);
+ saveGraphDot.addActionListener(this);
+ jp01.add(saveGraphDot, c01);
+ graphPathDot = new JTextField(graphDirDot);
+ jp01.add(graphPathDot, c01);
+ c.add(jp01, BorderLayout.NORTH);
+
jta = new ScrolledJTextArea();
@@ -243,88 +243,88 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
stop.addActionListener(this);
close.addActionListener(this);
- // Information
- JPanel jplow = new JPanel(new BorderLayout());
-
- JPanel jpinfo = new JPanel();
+ // Information
+ JPanel jplow = new JPanel(new BorderLayout());
+
+ JPanel jpinfo = new JPanel();
GridBagLayout gridbag02 = new GridBagLayout();
GridBagConstraints c02 = new GridBagConstraints();
jpinfo.setLayout(gridbag02);
jpinfo.setBorder(new javax.swing.border.TitledBorder("Graph information"));
- jplow.add(jpinfo, BorderLayout.NORTH);
- c02.gridheight = 1;
- c02.weighty = 1.0;
- c02.weightx = 1.0;
- c02.fill = GridBagConstraints.HORIZONTAL;
- //c02.gridwidth = 1;
- //jpinfo.add(new JLabel(""), c02);
- c02.gridwidth = GridBagConstraints.REMAINDER; //end row
- info = new JLabel();
- info.setFont(new Font("Serif", Font.BOLD, 16));
- updateInfo();
- jpinfo.add(info, c02);
- jpinfo.add(new JLabel(" "), c02);
- // nb of states, nb of links, nb of pending states, elapsed time, nbOfStatesPerSeconds
-
-
- c02.gridwidth = 1;
- jpinfo.add(new JLabel("Nb of states:"), c02);
- //c02.gridwidth = GridBagConstraints.REMAINDER; //end row
- nbOfStates = new JLabel("-");
- jpinfo.add(nbOfStates, c02);
-
-
- c02.gridwidth = 1;
- jpinfo.add(new JLabel("Nb of transitions:"), c02);
- c02.gridwidth = GridBagConstraints.REMAINDER; //end row
- nbOfLinks = new JLabel("-");
- jpinfo.add(nbOfLinks, c02);
-
- c02.gridwidth = 1;
- jpinfo.add(new JLabel("Reachability found:"), c02);
- //c02.gridwidth = GridBagConstraints.REMAINDER; //end row
- nbOfReachabilities = new JLabel("-");
- jpinfo.add(nbOfReachabilities, c02);
-
- c02.gridwidth = 1;
- jpinfo.add(new JLabel("Reachability not found:"), c02);
- c02.gridwidth = GridBagConstraints.REMAINDER; //end row
- nbOfReachabilitiesNotFound = new JLabel("-");
- jpinfo.add(nbOfReachabilitiesNotFound, c02);
-
-
- c02.gridwidth = 1;
- jpinfo.add(new JLabel("Nb of deadlock states:"), c02);
- c02.gridwidth = GridBagConstraints.REMAINDER; //end row
- nbOfDeadlocks = new JLabel("-");
- jpinfo.add(nbOfDeadlocks, c02);
-
- c02.gridwidth = 1;
- jpinfo.add(new JLabel("Nb of pending states:"), c02);
- //c02.gridwidth = GridBagConstraints.REMAINDER; //end row
- nbOfPendingStates = new JLabel("-");
- jpinfo.add(nbOfPendingStates, c02);
-
- c02.gridwidth = 1;
- jpinfo.add(new JLabel("Nb of states/seconds:"), c02);
- c02.gridwidth = GridBagConstraints.REMAINDER; //end row
- nbOfStatesPerSecond = new JLabel("-");
- jpinfo.add(nbOfStatesPerSecond, c02);
-
-
- c02.gridwidth = 1;
- jpinfo.add(new JLabel("Elapsed timed:"), c02);
- c02.gridwidth = GridBagConstraints.REMAINDER; //end row
- elapsedTime = new JLabel("-");
- jpinfo.add(elapsedTime, c02);
-
-
+ jplow.add(jpinfo, BorderLayout.NORTH);
+ c02.gridheight = 1;
+ c02.weighty = 1.0;
+ c02.weightx = 1.0;
+ c02.fill = GridBagConstraints.HORIZONTAL;
+ //c02.gridwidth = 1;
+ //jpinfo.add(new JLabel(""), c02);
+ c02.gridwidth = GridBagConstraints.REMAINDER; //end row
+ info = new JLabel();
+ info.setFont(new Font("Serif", Font.BOLD, 16));
+ updateInfo();
+ jpinfo.add(info, c02);
+ jpinfo.add(new JLabel(" "), c02);
+ // nb of states, nb of links, nb of pending states, elapsed time, nbOfStatesPerSeconds
+
+
+ c02.gridwidth = 1;
+ jpinfo.add(new JLabel("Nb of states:"), c02);
+ //c02.gridwidth = GridBagConstraints.REMAINDER; //end row
+ nbOfStates = new JLabel("-");
+ jpinfo.add(nbOfStates, c02);
+
+
+ c02.gridwidth = 1;
+ jpinfo.add(new JLabel("Nb of transitions:"), c02);
+ c02.gridwidth = GridBagConstraints.REMAINDER; //end row
+ nbOfLinks = new JLabel("-");
+ jpinfo.add(nbOfLinks, c02);
+
+ c02.gridwidth = 1;
+ jpinfo.add(new JLabel("Reachability found:"), c02);
+ //c02.gridwidth = GridBagConstraints.REMAINDER; //end row
+ nbOfReachabilities = new JLabel("-");
+ jpinfo.add(nbOfReachabilities, c02);
+
+ c02.gridwidth = 1;
+ jpinfo.add(new JLabel("Reachability not found:"), c02);
+ c02.gridwidth = GridBagConstraints.REMAINDER; //end row
+ nbOfReachabilitiesNotFound = new JLabel("-");
+ jpinfo.add(nbOfReachabilitiesNotFound, c02);
+
+
+ c02.gridwidth = 1;
+ jpinfo.add(new JLabel("Nb of deadlock states:"), c02);
+ c02.gridwidth = GridBagConstraints.REMAINDER; //end row
+ nbOfDeadlocks = new JLabel("-");
+ jpinfo.add(nbOfDeadlocks, c02);
+
+ c02.gridwidth = 1;
+ jpinfo.add(new JLabel("Nb of pending states:"), c02);
+ //c02.gridwidth = GridBagConstraints.REMAINDER; //end row
+ nbOfPendingStates = new JLabel("-");
+ jpinfo.add(nbOfPendingStates, c02);
+
+ c02.gridwidth = 1;
+ jpinfo.add(new JLabel("Nb of states/seconds:"), c02);
+ c02.gridwidth = GridBagConstraints.REMAINDER; //end row
+ nbOfStatesPerSecond = new JLabel("-");
+ jpinfo.add(nbOfStatesPerSecond, c02);
+
+
+ c02.gridwidth = 1;
+ jpinfo.add(new JLabel("Elapsed timed:"), c02);
+ c02.gridwidth = GridBagConstraints.REMAINDER; //end row
+ elapsedTime = new JLabel("-");
+ jpinfo.add(elapsedTime, c02);
+
+
JPanel jp2 = new JPanel();
jp2.add(start);
jp2.add(stop);
jp2.add(close);
- jplow.add(jp2, BorderLayout.SOUTH);
+ jplow.add(jp2, BorderLayout.SOUTH);
c.add(jplow, BorderLayout.SOUTH);
@@ -340,16 +340,16 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
} else if (command.equals("Close")) {
closeDialog();
} else if (evt.getSource() == saveGraphAUT) {
- setButtons();
- } else if (evt.getSource() == saveGraphDot) {
- setButtons();
- } else if (evt.getSource() == ignoreEmptyTransitions) {
- setButtons();
- } else if (evt.getSource() == ignoreConcurrenceBetweenInternalActions) {
- setButtons();
- } else {
- setButtons();
- }
+ setButtons();
+ } else if (evt.getSource() == saveGraphDot) {
+ setButtons();
+ } else if (evt.getSource() == ignoreEmptyTransitions) {
+ setButtons();
+ } else if (evt.getSource() == ignoreConcurrenceBetweenInternalActions) {
+ setButtons();
+ } else {
+ setButtons();
+ }
}
public void closeDialog() {
@@ -360,18 +360,18 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
}
public synchronized void stopProcess() {
- if (amc != null) {
- amc.stopModelChecking();
- }
+ if (amc != null) {
+ amc.stopModelChecking();
+ }
mode = STOPPED;
setButtons();
go = false;
}
public synchronized void startProcess() {
- if (mode == STARTED) {
- return;
- }
+ if (mode == STARTED) {
+ return;
+ }
t = new Thread(this);
mode = STARTED;
setButtons();
@@ -381,7 +381,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
private void testGo() throws InterruptedException {
if (go == false) {
- TraceManager.addDev("Interrupted by user");
+ TraceManager.addDev("Interrupted by user");
throw new InterruptedException("Stopped by user");
}
}
@@ -396,78 +396,92 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
TraceManager.addDev("Thread started");
File testFile;
try {
- reinitValues();
- jta.append("Starting the model checker\n");
- amc = new AvatarModelChecker(spec);
- endDate = null;
- previousNbOfStates = 0;
- startDate = new Date();
- mcm = new ModelCheckerMonitor(this);
- java.util.Timer timer = new java.util.Timer(true);
- timer.scheduleAtFixedRate(mcm, 0, 500);
-
- // Setting options
- amc.setIgnoreEmptyTransitions(ignoreEmptyTransitionsSelected);
- amc.setIgnoreConcurrenceBetweenInternalActions(ignoreConcurrenceBetweenInternalActionsSelected);
-
- // Reachability
- int res;
- if (reachabilitySelected == REACHABILITY_SELECTED) {
- res = amc.setReachabilityOfSelected();
- jta.append("Reachability of " + res + " selected elements activated\n");
-
- }
-
- if (reachabilitySelected == REACHABILITY_ALL) {
- res = amc.setReachabilityOfAllStates();
- jta.append("Reachability of " + res + " states activated\n");
- }
-
- // RG?
- if (graphSelected || graphSelectedDot) {
- amc.setComputeRG(true);
- jta.append("Computation of Reachability Graph activated\n");
- }
-
- // Starting model checking
- testGo();
-
- amc.startModelChecking();
- timer.cancel();
- endDate = new Date();
- updateValues();
+ reinitValues();
+ jta.append("Starting the model checker\n");
+ amc = new AvatarModelChecker(spec);
+ endDate = null;
+ previousNbOfStates = 0;
+ startDate = new Date();
+ mcm = new ModelCheckerMonitor(this);
+ java.util.Timer timer = new java.util.Timer(true);
+ timer.scheduleAtFixedRate(mcm, 0, 500);
+
+ // Setting options
+ amc.setIgnoreEmptyTransitions(ignoreEmptyTransitionsSelected);
+ amc.setIgnoreConcurrenceBetweenInternalActions(ignoreConcurrenceBetweenInternalActionsSelected);
+
+ // Reachability
+ int res;
+ if (reachabilitySelected == REACHABILITY_SELECTED) {
+ res = amc.setReachabilityOfSelected();
+ jta.append("Reachability of " + res + " selected elements activated\n");
+
+ for(SpecificationReachability sr: amc.getReachabilities()){
+ handleReachability(sr.ref1, sr.result);
+ handleReachability(sr.ref1, sr.result);
+ }
+ }
+
+ if (reachabilitySelected == REACHABILITY_ALL) {
+ res = amc.setReachabilityOfAllStates();
+ jta.append("Reachability of " + res + " states activated\n");
+ for(SpecificationReachability sr: amc.getReachabilities()){
+ handleReachability(sr.ref1, sr.result);
+ handleReachability(sr.ref1, sr.result);
+ }
+ }
+
+ // RG?
+ if (graphSelected || graphSelectedDot) {
+ amc.setComputeRG(true);
+ jta.append("Computation of Reachability Graph activated\n");
+ }
+
+ // Starting model checking
+ testGo();
+
+ amc.startModelChecking();
+ timer.cancel();
+ endDate = new Date();
+ updateValues();
jta.append("\n\nModel checking done\n");
- jta.append("Nb of states:" + amc.getNbOfStates() + "\n");
- jta.append("Nb of links:" + amc.getNbOfLinks() + "\n");
-
- if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL)) {
- jta.append("\nReachabilities found:\n");
- jta.append(amc.reachabilityToString());
- }
-
- //TraceManager.addDev(amc.toString());
- //TraceManager.addDev(amc.toString());
- if (saveGraphAUT.isSelected()) {
- try {
- String graph = amc.toAUT();
- //TraceManager.addDev("graph AUT=\n" + graph);
- FileUtils.saveFile(graphPath.getText(), graph);
- jta.append("Graph saved in " + graphPath.getText() + "\n");
- } catch (Exception e) {
- jta.append("Graph could not be saved in " + graphPath.getText() + "\n");
- }
- }
- if (saveGraphDot.isSelected()) {
- try {
- String graph = amc.toDOT();
- //TraceManager.addDev("graph AUT=\n" + graph);
- FileUtils.saveFile(graphPathDot.getText(), graph);
- jta.append("Graph saved in " + graphPathDot.getText()+ "\n");
- } catch (Exception e) {
- jta.append("Graph could not be saved in " + graphPathDot.getText()+ "\n");
- }
- }
-
+ jta.append("Nb of states:" + amc.getNbOfStates() + "\n");
+ jta.append("Nb of links:" + amc.getNbOfLinks() + "\n");
+
+ if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL)) {
+ jta.append("\nReachabilities found:\n");
+ jta.append(amc.reachabilityToString());
+
+ // Back annotation on diagrams
+ for(SpecificationReachability sr: amc.getReachabilities()){
+ //TraceManager.addDev("Handing reachability of " + sr);
+ handleReachability(sr.ref1, sr.result);
+ handleReachability(sr.ref1, sr.result);
+ }
+ }
+
+ //TraceManager.addDev(amc.toString());
+ //TraceManager.addDev(amc.toString());
+ if (saveGraphAUT.isSelected()) {
+ try {
+ String graph = amc.toAUT();
+ //TraceManager.addDev("graph AUT=\n" + graph);
+ FileUtils.saveFile(graphPath.getText(), graph);
+ jta.append("Graph saved in " + graphPath.getText() + "\n");
+ } catch (Exception e) {
+ jta.append("Graph could not be saved in " + graphPath.getText() + "\n");
+ }
+ }
+ if (saveGraphDot.isSelected()) {
+ try {
+ String graph = amc.toDOT();
+ //TraceManager.addDev("graph AUT=\n" + graph);
+ FileUtils.saveFile(graphPathDot.getText(), graph);
+ jta.append("Graph saved in " + graphPathDot.getText()+ "\n");
+ } catch (Exception e) {
+ jta.append("Graph could not be saved in " + graphPathDot.getText()+ "\n");
+ }
+ }
} catch (InterruptedException ie) {
jta.append("Interrupted\n");
@@ -481,52 +495,76 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
//System.out.println("Selected item=" + selectedItem);
}
+ protected void handleReachability(Object _o, SpecificationReachabilityType _res) {
+ if (_o instanceof AvatarStateMachineElement) {
+ Object o = ((AvatarStateMachineElement)_o).getReferenceObject();
+ if (o instanceof TGComponent) {
+ TGComponent tgc = (TGComponent)(o);
+ //TraceManager.addDev("Reachability of tgc=" + tgc);
+ switch(_res) {
+ case NOTCOMPUTED:
+ tgc.setReachability(TGComponent.ACCESSIBILITY_UNKNOWN);
+ tgc.setLiveness(TGComponent.ACCESSIBILITY_UNKNOWN);
+ break;
+ case REACHABLE:
+ tgc.setReachability(TGComponent.ACCESSIBILITY_OK);
+ break;
+ case NONREACHABLE:
+ tgc.setReachability(TGComponent.ACCESSIBILITY_KO);
+ tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
+ break;
+ }
+ tgc.getTDiagramPanel().repaint();
+ }
+ }
+ }
+
protected void checkMode() {
mode = NOT_STARTED;
}
protected void setButtons() {
- graphSelected = saveGraphAUT.isSelected();
- graphPath.setEnabled(saveGraphAUT.isSelected());
- graphSelectedDot = saveGraphDot.isSelected();
- graphPathDot.setEnabled(saveGraphDot.isSelected());
- ignoreEmptyTransitionsSelected = ignoreEmptyTransitions.isSelected();
- ignoreConcurrenceBetweenInternalActionsSelected = ignoreConcurrenceBetweenInternalActions.isSelected();
-
- if (noReachability.isSelected()) {
- reachabilitySelected = REACHABILITY_NONE;
- } else if ( reachabilityCheckable.isSelected()) {
- reachabilitySelected = REACHABILITY_SELECTED;
- } else {
- reachabilitySelected = REACHABILITY_ALL;
- }
-
+ graphSelected = saveGraphAUT.isSelected();
+ graphPath.setEnabled(saveGraphAUT.isSelected());
+ graphSelectedDot = saveGraphDot.isSelected();
+ graphPathDot.setEnabled(saveGraphDot.isSelected());
+ ignoreEmptyTransitionsSelected = ignoreEmptyTransitions.isSelected();
+ ignoreConcurrenceBetweenInternalActionsSelected = ignoreConcurrenceBetweenInternalActions.isSelected();
+
+ if (noReachability.isSelected()) {
+ reachabilitySelected = REACHABILITY_NONE;
+ } else if ( reachabilityCheckable.isSelected()) {
+ reachabilitySelected = REACHABILITY_SELECTED;
+ } else {
+ reachabilitySelected = REACHABILITY_ALL;
+ }
+
switch(mode) {
- case NOT_STARTED:
- if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL) || graphSelected || graphSelectedDot) {
- start.setEnabled(true);
- } else {
- start.setEnabled(false);
- }
- stop.setEnabled(false);
- close.setEnabled(true);
- //setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
- getGlassPane().setVisible(false);
- break;
- case STARTED:
+ case NOT_STARTED:
+ if ((reachabilitySelected == REACHABILITY_SELECTED) || (reachabilitySelected == REACHABILITY_ALL) || graphSelected || graphSelectedDot) {
+ start.setEnabled(true);
+ } else {
start.setEnabled(false);
- stop.setEnabled(true);
- close.setEnabled(false);
- getGlassPane().setVisible(true);
- //setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
- break;
- case STOPPED:
- default:
- start.setEnabled(false);
- stop.setEnabled(false);
- close.setEnabled(true);
- getGlassPane().setVisible(false);
- break;
+ }
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ //setCursor(Cursor.getPredefinedCursor(Cursor.DEFAULT_CURSOR));
+ getGlassPane().setVisible(false);
+ break;
+ case STARTED:
+ start.setEnabled(false);
+ stop.setEnabled(true);
+ close.setEnabled(false);
+ getGlassPane().setVisible(true);
+ //setCursor(Cursor.getPredefinedCursor(Cursor.WAIT_CURSOR));
+ break;
+ case STOPPED:
+ default:
+ start.setEnabled(false);
+ stop.setEnabled(false);
+ close.setEnabled(true);
+ getGlassPane().setVisible(false);
+ break;
}
}
@@ -543,104 +581,104 @@ public class JDialogAvatarModelChecker extends javax.swing.JDialog implements Ac
}
public void updateValues() {
- TraceManager.addDev("Updating values...");
- try {
- if (amc != null) {
- int nbOfStatess = amc.getNbOfStates();
- nbOfStates.setText(""+nbOfStatess);
- nbOfLinks.setText(""+amc.getNbOfLinks());
-
- // Reachability and deadlocks
- int nb = amc.getNbOfReachabilities();
- if (nb == -1) {
- //nbOfReachabilities.setText("-");
- } else {
- nbOfReachabilities.setText("" + nb);
- }
- nb = amc.getNbOfRemainingReachabilities();
- nbOfReachabilitiesNotFound.setText("" + nb);
-
-
- nbOfDeadlocks.setText(""+amc.getNbOfDeadlocks());
-
-
- nbOfPendingStates.setText(""+amc.getNbOfPendingStates());
- Date d;
- previousDate = new Date();
- if (endDate != null) {
- d = endDate;
- } else {
- d = previousDate;
- }
- long duration = d.getTime() - startDate.getTime();
-
- String t = String.format("%02d min %02d sec %03d msec",
- TimeUnit.MILLISECONDS.toMinutes(duration),
- TimeUnit.MILLISECONDS.toSeconds(duration) - TimeUnit.MINUTES.toSeconds(TimeUnit.MILLISECONDS.toMinutes(duration)),
- duration
- );
-
- long diffInSeconds = TimeUnit.MILLISECONDS.toSeconds(duration);
- long diffInMinutes = TimeUnit.MILLISECONDS.toMinutes(duration);
- //long diffInMs = TimeUnit.MILLISECONDS.toMilliseconds(duration);
- elapsedTime.setText(t);
- long diff = 0;
- if (endDate != null) {
- diff = nbOfStatess;
- } else {
- diff = nbOfStatess - previousNbOfStates;
- }
- previousNbOfStates = nbOfStatess;
- //if (diff == 0) {
-
-
- nbOfStatesPerSecond.setText(""+1000*diff/duration);
-
- updateInfo();
- //}
- }
- } catch (Exception e) {
- }
+ TraceManager.addDev("Updating values...");
+ try {
+ if (amc != null) {
+ int nbOfStatess = amc.getNbOfStates();
+ nbOfStates.setText(""+nbOfStatess);
+ nbOfLinks.setText(""+amc.getNbOfLinks());
+
+ // Reachability and deadlocks
+ int nb = amc.getNbOfReachabilities();
+ if (nb == -1) {
+ //nbOfReachabilities.setText("-");
+ } else {
+ nbOfReachabilities.setText("" + nb);
+ }
+ nb = amc.getNbOfRemainingReachabilities();
+ nbOfReachabilitiesNotFound.setText("" + nb);
+
+
+ nbOfDeadlocks.setText(""+amc.getNbOfDeadlocks());
+
+
+ nbOfPendingStates.setText(""+amc.getNbOfPendingStates());
+ Date d;
+ previousDate = new Date();
+ if (endDate != null) {
+ d = endDate;
+ } else {
+ d = previousDate;
+ }
+ long duration = d.getTime() - startDate.getTime();
+
+ String t = String.format("%02d min %02d sec %03d msec",
+ TimeUnit.MILLISECONDS.toMinutes(duration),
+ TimeUnit.MILLISECONDS.toSeconds(duration) - TimeUnit.MINUTES.toSeconds(TimeUnit.MILLISECONDS.toMinutes(duration)),
+ duration
+ );
+
+ long diffInSeconds = TimeUnit.MILLISECONDS.toSeconds(duration);
+ long diffInMinutes = TimeUnit.MILLISECONDS.toMinutes(duration);
+ //long diffInMs = TimeUnit.MILLISECONDS.toMilliseconds(duration);
+ elapsedTime.setText(t);
+ long diff = 0;
+ if (endDate != null) {
+ diff = nbOfStatess;
+ } else {
+ diff = nbOfStatess - previousNbOfStates;
+ }
+ previousNbOfStates = nbOfStatess;
+ //if (diff == 0) {
+
+
+ nbOfStatesPerSecond.setText(""+1000*diff/duration);
+
+ updateInfo();
+ //}
+ }
+ } catch (Exception e) {
+ }
}
public void reinitValues() {
- nbOfStates.setText("-");
- nbOfLinks.setText("-");
- nbOfReachabilities.setText("-");
- nbOfReachabilitiesNotFound.setText("-");
- nbOfDeadlocks.setText("-");
- nbOfPendingStates.setText("-");
- nbOfStatesPerSecond.setText("-");
- elapsedTime.setText("-");
+ nbOfStates.setText("-");
+ nbOfLinks.setText("-");
+ nbOfReachabilities.setText("-");
+ nbOfReachabilitiesNotFound.setText("-");
+ nbOfDeadlocks.setText("-");
+ nbOfPendingStates.setText("-");
+ nbOfStatesPerSecond.setText("-");
+ elapsedTime.setText("-");
}
public int getStateIndex() {
- if (amc == null) {
- return 0;
- }
-
- if (endDate == null) {
- return 1;
- }
-
- return amc.hasBeenStoppedBeforeCompletion() ? 2 : 3;
-
+ if (amc == null) {
+ return 0;
+ }
+
+ if (endDate == null) {
+ return 1;
+ }
+
+ return amc.hasBeenStoppedBeforeCompletion() ? 2 : 3;
+
}
public void updateInfo() {
- info.setForeground(COLORS[getStateIndex()]);
- info.setText(INFOS[getStateIndex()]);
+ info.setForeground(COLORS[getStateIndex()]);
+ info.setText(INFOS[getStateIndex()]);
}
private class ModelCheckerMonitor extends TimerTask {
- private JDialogAvatarModelChecker jdamc;
- public ModelCheckerMonitor(JDialogAvatarModelChecker _jdamc) {
- jdamc = _jdamc;
- }
-
- public void run() {
- jdamc.updateValues();
- }
-
+ private JDialogAvatarModelChecker jdamc;
+ public ModelCheckerMonitor(JDialogAvatarModelChecker _jdamc) {
+ jdamc = _jdamc;
+ }
+
+ public void run() {
+ jdamc.updateValues();
+ }
+
}
}
diff --git a/src/ui/window/JDialogUPPAALValidation.java b/src/ui/window/JDialogUPPAALValidation.java
index 41ba2939f50d2d86ae1b268a467d645fe3d77361..5731d0869b0eb1528d57c0ef467acab07499e00c 100755
--- a/src/ui/window/JDialogUPPAALValidation.java
+++ b/src/ui/window/JDialogUPPAALValidation.java
@@ -391,6 +391,9 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
ArrayList<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
if ((list != null) && (list.size() > 0)){
for(TGComponentAndUPPAALQuery cq: list) {
+ if (cq.tgc != null) {
+ cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_UNKNOWN);
+ }
String s = cq.uppaalQuery;
index = s.indexOf('$');
if ((index != -1) && (mode != NOT_STARTED)) {
@@ -398,7 +401,14 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
query = s.substring(0, index);
//jta.append("\n--------------------------------------------\n");
jta.append("\nLiveness of: " + name + "\n");
- workQuery("A<> " + query, fn, trace_id, rshc);
+ result = workQuery("A<> " + query, fn, trace_id, rshc);
+ if (cq.tgc != null) {
+ if (result == 0) {
+ cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
+ } else if (result == 1) {
+ cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_OK);
+ }
+ }
trace_id++;
} else {
jta.append("A component could not be studied (internal error)\n");