diff --git a/modeling/proverif.xml b/modeling/proverif.xml
index 0c2dcb385337424a1f87f10f34bd4b550cb43393..f2dc812c68daf27ba049daecec0a4eb2f284ea48 100644
--- a/modeling/proverif.xml
+++ b/modeling/proverif.xml
@@ -1,12 +1,12 @@
<?xml version="1.0" encoding="ISO-8859-1"?>
-<TURTLEGMODELING version="0.92">
+<TURTLEGMODELING version="0.93-beta1">
<Modeling type="AVATAR Design" nameTab="KeyMasterProtocol" >
<AVATARBlockDiagramPanel name="AVATAR Block Diagram" minX="10" maxX="1400" minY="10" maxY="900" >
<COMPONENT type="5000" id="25" >
-<cdparam x="814" y="226" />
-<sizeparam width="250" height="214" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="170" y="180" />
+<sizeparam width="135" height="214" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Block0" value="ECUN" />
@@ -66,8 +66,8 @@
</COMPONENT>
<COMPONENT type="5000" id="75" >
-<cdparam x="404" y="179" />
-<sizeparam width="389" height="511" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="584" y="10" />
+<sizeparam width="324" height="324" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Block0" value="KM" />
@@ -134,10 +134,10 @@
</COMPONENT>
<SUBCOMPONENT type="5000" id="50" >
<father id="75" num="0" />
-<cdparam x="543" y="347" />
-<sizeparam width="250" height="307" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="684" y="74" />
+<sizeparam width="212" height="134" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="139" minY="0" maxY="204" />
+<cdrectangleparam minX="0" maxX="112" minY="0" maxY="190" />
<infoparam name="Block0" value="TimerKM" />
<TGConnectingPoint num="0" id="26" />
<TGConnectingPoint num="1" id="27" />
@@ -186,8 +186,8 @@
</SUBCOMPONENT>
<COMPONENT type="5000" id="100" >
-<cdparam x="41" y="247" />
-<sizeparam width="281" height="264" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="309" y="181" />
+<sizeparam width="223" height="212" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Block0" value="ECU1" />
@@ -248,8 +248,8 @@
</COMPONENT>
<COMPONENT type="301" id="109" >
-<cdparam x="33" y="10" />
-<sizeparam width="427" height="155" minWidth="50" minHeight="20" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="163" y="10" />
+<sizeparam width="416" height="164" minWidth="50" minHeight="20" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="UML Note" value="#Confidentiality ECU1.SesK
@@ -284,8 +284,8 @@
</COMPONENT>
<COMPONENT type="5003" id="118" >
-<cdparam x="170" y="547" />
-<sizeparam width="123" height="88" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="660" y="340" />
+<sizeparam width="102" height="54" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="DataType0" value="Message" />
@@ -303,8 +303,8 @@
</COMPONENT>
<COMPONENT type="5003" id="127" >
-<cdparam x="33" y="546" />
-<sizeparam width="121" height="91" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="544" y="339" />
+<sizeparam width="110" height="56" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="DataType0" value="Key" />
@@ -335,7 +335,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="128" >
<father id="129" num="0" />
<cdparam x="654" y="1057" />
-<sizeparam width="223" height="30" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="223" height="32" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -360,7 +360,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="130" >
<father id="131" num="0" />
<cdparam x="413" y="957" />
-<sizeparam width="46" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="46" height="16" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -383,7 +383,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="132" >
<father id="133" num="0" />
<cdparam x="570" y="959" />
-<sizeparam width="24" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="24" height="16" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -429,7 +429,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="136" >
<father id="137" num="0" />
<cdparam x="548" y="832" />
-<sizeparam width="240" height="30" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="240" height="32" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -454,7 +454,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="138" >
<father id="139" num="0" />
<cdparam x="529" y="457" />
-<sizeparam width="291" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="291" height="16" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -523,7 +523,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="144" >
<father id="145" num="0" />
<cdparam x="440" y="381" />
-<sizeparam width="201" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="201" height="16" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -570,7 +570,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="148" >
<father id="149" num="0" />
<cdparam x="565" y="553" />
-<sizeparam width="323" height="90" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="323" height="96" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -631,7 +631,7 @@
<SUBCOMPONENT type="-1" id="153" >
<father id="154" num="1" />
<cdparam x="446" y="292" />
-<sizeparam width="226" height="30" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="226" height="32" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -1043,7 +1043,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="440" >
<father id="441" num="0" />
<cdparam x="437" y="926" />
-<sizeparam width="191" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="191" height="16" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -1066,7 +1066,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="442" >
<father id="443" num="0" />
<cdparam x="728" y="893" />
-<sizeparam width="217" height="45" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="217" height="48" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1900" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -1114,7 +1114,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="446" >
<father id="447" num="0" />
<cdparam x="938" y="1171" />
-<sizeparam width="315" height="75" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="315" height="80" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -1165,7 +1165,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="450" >
<father id="451" num="0" />
<cdparam x="531" y="526" />
-<sizeparam width="307" height="30" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="307" height="32" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -1190,7 +1190,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="452" >
<father id="453" num="0" />
<cdparam x="263" y="392" />
-<sizeparam width="190" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="190" height="16" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -1282,7 +1282,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="460" >
<father id="461" num="0" />
<cdparam x="851" y="1007" />
-<sizeparam width="186" height="30" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="186" height="32" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -1306,7 +1306,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="462" >
<father id="463" num="0" />
<cdparam x="414" y="254" />
-<sizeparam width="218" height="30" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="218" height="32" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -1331,7 +1331,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="464" >
<father id="465" num="0" />
<cdparam x="622" y="620" />
-<sizeparam width="307" height="75" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="307" height="80" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -1368,7 +1368,7 @@
<SUBCOMPONENT type="-1" id="467" >
<father id="468" num="1" />
<cdparam x="492" y="361" />
-<sizeparam width="160" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="160" height="16" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -1414,7 +1414,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="471" >
<father id="472" num="0" />
<cdparam x="885" y="1097" />
-<sizeparam width="130" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="130" height="16" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -1515,8 +1515,8 @@
</COMPONENT>
<COMPONENT type="5103" id="535" >
-<cdparam x="481" y="690" />
-<sizeparam width="96" height="20" minWidth="30" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="483" y="690" />
+<sizeparam width="93" height="20" minWidth="30" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1900" />
<infoparam name="Send signal" value="chout(settimer)" />
@@ -1908,7 +1908,7 @@
<COMPONENT type="5104" id="829" >
<cdparam x="358" y="142" />
-<sizeparam width="81" height="20" minWidth="30" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="80" height="20" minWidth="30" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1900" />
<infoparam name="Send signal" value="chin(msg8)" />
@@ -1970,7 +1970,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="834" >
<father id="835" num="0" />
<cdparam x="274" y="118" />
-<sizeparam width="215" height="105" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="215" height="112" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
<infoparam name="List of all parameters of an Avatar SMD transition" value="" />
@@ -2023,7 +2023,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="838" >
<father id="839" num="0" />
<cdparam x="512" y="818" />
-<sizeparam width="174" height="60" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="174" height="64" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -2050,7 +2050,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="840" >
<father id="841" num="0" />
<cdparam x="254" y="699" />
-<sizeparam width="152" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="152" height="16" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -2073,7 +2073,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="842" >
<father id="843" num="0" />
<cdparam x="446" y="694" />
-<sizeparam width="126" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="126" height="16" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -2096,7 +2096,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="844" >
<father id="845" num="0" />
<cdparam x="160" y="553" />
-<sizeparam width="42" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="42" height="16" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -2119,7 +2119,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="846" >
<father id="847" num="0" />
<cdparam x="357" y="554" />
-<sizeparam width="24" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="24" height="16" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -2142,7 +2142,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="848" >
<father id="849" num="0" />
<cdparam x="252" y="429" />
-<sizeparam width="200" height="45" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="200" height="48" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -2498,7 +2498,7 @@
<COMPONENT type="5103" id="1086" >
<cdparam x="188" y="204" />
-<sizeparam width="81" height="20" minWidth="30" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="80" height="20" minWidth="30" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
<infoparam name="Send signal" value="chout(msg6)" />
@@ -2739,14 +2739,12 @@
<Modeling type="AVATAR Design" nameTab="Example" >
<AVATARBlockDiagramPanel name="AVATAR Block Diagram" minX="10" maxX="1400" minY="10" maxY="900" >
<COMPONENT type="301" id="1179" >
-<cdparam x="203" y="52" />
-<sizeparam width="411" height="95" minWidth="50" minHeight="20" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="147" y="96" />
+<sizeparam width="394" height="68" minWidth="50" minHeight="20" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="UML Note" value="#InitialCommonKnowledge Alice.sk Bob.sk
-
#Confidentiality Alice.secretData
-
#Authenticity Alice.sendingMessage.m1 Bob.messageDecrypted.m2
" />
<TGConnectingPoint num="0" id="1171" />
@@ -2759,16 +2757,14 @@
<TGConnectingPoint num="7" id="1178" />
<extraparam>
<Line value="#InitialCommonKnowledge Alice.sk Bob.sk" />
-<Line value="" />
<Line value="#Confidentiality Alice.secretData" />
-<Line value="" />
<Line value="#Authenticity Alice.sendingMessage.m1 Bob.messageDecrypted.m2" />
</extraparam>
</COMPONENT>
<COMPONENT type="5000" id="1204" >
-<cdparam x="413" y="178" />
-<sizeparam width="353" height="231" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="382" y="171" />
+<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Block0" value="Bob" />
@@ -2819,8 +2815,8 @@
</COMPONENT>
<COMPONENT type="5000" id="1229" >
-<cdparam x="50" y="177" />
-<sizeparam width="355" height="234" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="158" y="172" />
+<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Block0" value="Alice" />
@@ -2871,8 +2867,8 @@
</COMPONENT>
<COMPONENT type="5003" id="1238" >
-<cdparam x="451" y="463" />
-<sizeparam width="192" height="137" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="383" y="310" />
+<sizeparam width="129" height="61" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="DataType0" value="Message" />
@@ -2890,8 +2886,8 @@
</COMPONENT>
<COMPONENT type="5003" id="1247" >
-<cdparam x="152" y="460" />
-<sizeparam width="189" height="142" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="194" y="311" />
+<sizeparam width="123" height="62" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="DataType0" value="Key" />
@@ -2922,7 +2918,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="1248" >
<father id="1249" num="0" />
<cdparam x="431" y="403" />
-<sizeparam width="143" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="143" height="16" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -2946,7 +2942,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="1250" >
<father id="1251" num="0" />
<cdparam x="419" y="312" />
-<sizeparam width="207" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="207" height="16" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -3126,8 +3122,8 @@
</COMPONENT>
<COMPONENT type="5104" id="1343" >
-<cdparam x="372" y="176" />
-<sizeparam width="68" height="20" minWidth="30" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="373" y="176" />
+<sizeparam width="66" height="20" minWidth="30" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="chin(m2)" />
@@ -3244,7 +3240,7 @@
</CONNECTOR><SUBCOMPONENT type="-1" id="1375" >
<father id="1376" num="0" />
<cdparam x="415" y="162" />
-<sizeparam width="185" height="30" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="185" height="32" minWidth="0" minHeight="0" maxWidth="1000" 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="" />
@@ -3283,8 +3279,8 @@
</SUBCOMPONENT>
<COMPONENT type="5103" id="1389" >
-<cdparam x="373" y="285" />
-<sizeparam width="68" height="20" minWidth="30" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="374" y="285" />
+<sizeparam width="66" height="20" minWidth="30" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
<infoparam name="Send signal" value="chout(m1)" />
@@ -3390,4 +3386,167 @@
+<Modeling type="AVATAR Design" nameTab="AVATAR Design" >
+<AVATARBlockDiagramPanel name="AVATAR Block Diagram" minX="10" maxX="1400" minY="10" maxY="900" >
+<CONNECTOR type="5002" id="3025" >
+<cdparam x="269" y="201" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector from Block0 to Block0" value="" />
+<P1 x="324" y="185" id="1459" />
+<P2 x="385" y="209" id="1485" />
+<AutomaticDrawing data="true" />
+<extraparam>
+<isd value="in fromnet()" />
+<oso value="out tonet()" />
+<FIFOType asynchronous="true" size="1" blocking="false" />
+</extraparam>
+</CONNECTOR>
+<COMPONENT type="5000" id="1472" >
+<cdparam x="385" y="133" />
+<sizeparam width="131" height="102" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
+<infoparam name="Block0" value="Bob" />
+<TGConnectingPoint num="0" id="1473" />
+<TGConnectingPoint num="1" id="1474" />
+<TGConnectingPoint num="2" id="1475" />
+<TGConnectingPoint num="3" id="1476" />
+<TGConnectingPoint num="4" id="1477" />
+<TGConnectingPoint num="5" id="1478" />
+<TGConnectingPoint num="6" id="1479" />
+<TGConnectingPoint num="7" id="1480" />
+<TGConnectingPoint num="8" id="1481" />
+<TGConnectingPoint num="9" id="1482" />
+<TGConnectingPoint num="10" id="1483" />
+<TGConnectingPoint num="11" id="1484" />
+<TGConnectingPoint num="12" id="1485" />
+<TGConnectingPoint num="13" id="1486" />
+<TGConnectingPoint num="14" id="1487" />
+<TGConnectingPoint num="15" id="1488" />
+<TGConnectingPoint num="16" id="1489" />
+<TGConnectingPoint num="17" id="1490" />
+<TGConnectingPoint num="18" id="1491" />
+<TGConnectingPoint num="19" id="1492" />
+<TGConnectingPoint num="20" id="1493" />
+<TGConnectingPoint num="21" id="1494" />
+<TGConnectingPoint num="22" id="1495" />
+<TGConnectingPoint num="23" id="1496" />
+<extraparam>
+<Attribute access="0" id="receivedData" value="" type="8" typeOther="" />
+<Attribute access="0" id="m" value="" type="5" typeOther="Message" />
+<Attribute access="0" id="sk" value="" type="5" typeOther="Key" />
+<Signal value="in fromnet()" />
+</extraparam>
+</COMPONENT>
+
+<COMPONENT type="5000" id="1445" >
+<cdparam x="201" y="103" />
+<sizeparam width="123" height="110" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
+<infoparam name="Block0" value="Alice" />
+<TGConnectingPoint num="0" id="1446" />
+<TGConnectingPoint num="1" id="1447" />
+<TGConnectingPoint num="2" id="1448" />
+<TGConnectingPoint num="3" id="1449" />
+<TGConnectingPoint num="4" id="1450" />
+<TGConnectingPoint num="5" id="1451" />
+<TGConnectingPoint num="6" id="1452" />
+<TGConnectingPoint num="7" id="1453" />
+<TGConnectingPoint num="8" id="1454" />
+<TGConnectingPoint num="9" id="1455" />
+<TGConnectingPoint num="10" id="1456" />
+<TGConnectingPoint num="11" id="1457" />
+<TGConnectingPoint num="12" id="1458" />
+<TGConnectingPoint num="13" id="1459" />
+<TGConnectingPoint num="14" id="1460" />
+<TGConnectingPoint num="15" id="1461" />
+<TGConnectingPoint num="16" id="1462" />
+<TGConnectingPoint num="17" id="1463" />
+<TGConnectingPoint num="18" id="1464" />
+<TGConnectingPoint num="19" id="1465" />
+<TGConnectingPoint num="20" id="1466" />
+<TGConnectingPoint num="21" id="1467" />
+<TGConnectingPoint num="22" id="1468" />
+<TGConnectingPoint num="23" id="1469" />
+<extraparam>
+<Attribute access="0" id="secretData" value="" type="8" typeOther="" />
+<Attribute access="0" id="m" value="" type="5" typeOther="Message" />
+<Attribute access="0" id="sk" value="" type="5" typeOther="Key" />
+<Signal value="out tonet()" />
+</extraparam>
+</COMPONENT>
+
+<COMPONENT type="5003" id="2735" >
+<cdparam x="380" y="246" />
+<sizeparam width="116" height="77" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
+<infoparam name="DataType0" value="Message" />
+<TGConnectingPoint num="0" id="2727" />
+<TGConnectingPoint num="1" id="2728" />
+<TGConnectingPoint num="2" id="2729" />
+<TGConnectingPoint num="3" id="2730" />
+<TGConnectingPoint num="4" id="2731" />
+<TGConnectingPoint num="5" id="2732" />
+<TGConnectingPoint num="6" id="2733" />
+<TGConnectingPoint num="7" id="2734" />
+<extraparam>
+<Attribute access="0" id="data" value="" type="0" typeOther="" />
+</extraparam>
+</COMPONENT>
+
+<COMPONENT type="5003" id="2744" >
+<cdparam x="201" y="244" />
+<sizeparam width="130" height="76" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
+<infoparam name="DataType0" value="Key" />
+<TGConnectingPoint num="0" id="2736" />
+<TGConnectingPoint num="1" id="2737" />
+<TGConnectingPoint num="2" id="2738" />
+<TGConnectingPoint num="3" id="2739" />
+<TGConnectingPoint num="4" id="2740" />
+<TGConnectingPoint num="5" id="2741" />
+<TGConnectingPoint num="6" id="2742" />
+<TGConnectingPoint num="7" id="2743" />
+<extraparam>
+<Attribute access="0" id="data" value="" type="8" typeOther="" />
+</extraparam>
+</COMPONENT>
+
+
+</AVATARBlockDiagramPanel>
+
+<AVATARStateMachineDiagramPanel name="Alice" minX="10" maxX="1400" minY="10" maxY="900" >
+<COMPONENT type="5100" id="1470" >
+<cdparam x="400" y="50" />
+<sizeparam width="15" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
+<infoparam name="start state" value="null" />
+<TGConnectingPoint num="0" id="1471" />
+</COMPONENT>
+
+
+</AVATARStateMachineDiagramPanel>
+
+<AVATARStateMachineDiagramPanel name="Bob" minX="10" maxX="1400" minY="10" maxY="900" >
+<COMPONENT type="5100" id="1497" >
+<cdparam x="400" y="50" />
+<sizeparam width="15" height="15" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="900" />
+<infoparam name="start state" value="null" />
+<TGConnectingPoint num="0" id="1498" />
+</COMPONENT>
+
+
+</AVATARStateMachineDiagramPanel>
+
+</Modeling>
+
+
+
+
</TURTLEGMODELING>
\ No newline at end of file
diff --git a/src/avatartranslator/directsimulation/AvatarSimulationBlock.java b/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
index cf37f30218cec7bbd5ca0fac675fd2e3eb430cf7..d1f54087ee0e4f57d7a8c405380528974037e2b4 100644
--- a/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
+++ b/src/avatartranslator/directsimulation/AvatarSimulationBlock.java
@@ -65,8 +65,15 @@ public class AvatarSimulationBlock {
completed = false;
}
- public LinkedList<AvatarSimulationTransaction> getPendingTransactions(LinkedList<AvatarSimulationTransaction> _allTransactions, long _clockValue, int _maxTransationsInARow) {
- LinkedList<AvatarSimulationTransaction> ll = new LinkedList<AvatarSimulationTransaction>();
+ public String getName() {
+ if (block != null) {
+ return block.getName();
+ }
+ return "noname";
+ }
+
+ public LinkedList<AvatarSimulationPendingTransaction> getPendingTransactions(LinkedList<AvatarSimulationTransaction> _allTransactions, long _clockValue, int _maxTransationsInARow) {
+ LinkedList<AvatarSimulationPendingTransaction> ll = new LinkedList<AvatarSimulationPendingTransaction>();
if (completed) {
return ll;
@@ -76,7 +83,7 @@ public class AvatarSimulationBlock {
runToNextBlockingElement(_allTransactions, _clockValue, _maxTransationsInARow);
}
- if (completed) {
+ if ((lastTransaction == null) || completed) {
return ll;
}
@@ -84,8 +91,26 @@ public class AvatarSimulationBlock {
// ...
// ...
// To be done!
-
-
+ AvatarSimulationPendingTransaction aspt;
+ for(int i=0; i<lastTransaction.executedElement.nbOfNexts(); i++) {
+ aspt = new AvatarSimulationPendingTransaction();
+ aspt.asb = this;
+ aspt.elementToExecute = lastTransaction.executedElement.getNext(i);
+ if ((aspt.elementToExecute instanceof AvatarTransition) && (lastTransaction.executedElement instanceof AvatarState)) {
+ AvatarTransition trans = (AvatarTransition)(aspt.elementToExecute);
+ if (!trans.hasDelay() && (trans.getNbOfAction() == 0)){
+ // empty transition, "empty" is the meaning of actions -> look for an action after
+ if(trans.getNext(0) != null) {
+ if (trans.getNext(0) instanceof AvatarActionOnSignal) {
+ aspt.involvedElement = trans;
+ aspt.elementToExecute = trans.getNext(0);
+ }
+ }
+ }
+ }
+ aspt.clockValue = _clockValue;
+ ll.add(aspt);
+ }
return ll;
}
diff --git a/src/avatartranslator/directsimulation/AvatarSimulationPendingTransaction.java b/src/avatartranslator/directsimulation/AvatarSimulationPendingTransaction.java
new file mode 100644
index 0000000000000000000000000000000000000000..bc7971c8e8a91b6e73ae88e53e0c6da965fc93b8
--- /dev/null
+++ b/src/avatartranslator/directsimulation/AvatarSimulationPendingTransaction.java
@@ -0,0 +1,71 @@
+/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+
+ludovic.apvrille AT enst.fr
+
+This software is a computer program whose purpose is to allow the
+edition of TURTLE analysis, design and deployment diagrams, to
+allow the generation of RT-LOTOS or Java code from this diagram,
+and at last to allow the analysis of formal validation traces
+obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+from INRIA Rhone-Alpes.
+
+This software is governed by the CeCILL license under French law and
+abiding by the rules of distribution of free software. You can use,
+modify and/ or redistribute the software under the terms of the CeCILL
+license as circulated by CEA, CNRS and INRIA at the following URL
+"http://www.cecill.info".
+
+As a counterpart to the access to the source code and rights to copy,
+modify and redistribute granted by the license, users are provided only
+with a limited warranty and the software's author, the holder of the
+economic rights, and the successive licensors have only limited
+liability.
+
+In this respect, the user's attention is drawn to the risks associated
+with loading, using, modifying and/or developing or reproducing the
+software by the user in light of its specific status of free software,
+that may mean that it is complicated to manipulate, and that also
+therefore means that it is reserved for developers and experienced
+professionals having in-depth computer knowledge. Users are therefore
+encouraged to load and test the software's suitability as regards their
+requirements in conditions enabling the security of their systems and/or
+data to be ensured and, more generally, to use and operate it in the
+same conditions as regards security.
+
+The fact that you are presently reading this means that you have had
+knowledge of the CeCILL license and that you accept its terms.
+
+/**
+ * Class AvatarSimulationPendingTransaction
+ * Avatar: notion of pending transaction in simulation
+ * Creation: 11/01/2011
+ * @version 1.0 11/01/2011
+ * @author Ludovic APVRILLE
+ * @see
+ */
+
+
+package avatartranslator.directsimulation;
+
+import java.util.*;
+
+import avatartranslator.*;
+import myutil.*;
+
+public class AvatarSimulationPendingTransaction {
+
+ public AvatarSimulationBlock asb;
+ public AvatarStateMachineElement elementToExecute;
+ public AvatarStateMachineElement involvedElement; //(transition)
+ public long clockValue;
+
+ public AvatarSimulationPendingTransaction() {
+ }
+
+
+
+ public String toString() {
+ String res = " @" + clockValue + " " + elementToExecute + " in block " + asb.getName();
+ return res;
+ }
+}
\ No newline at end of file
diff --git a/src/avatartranslator/directsimulation/AvatarSimulationTransaction.java b/src/avatartranslator/directsimulation/AvatarSimulationTransaction.java
index 4b6d6249a249d2889a93686c919317997510ecf0..fc15cf0f77aa7597b047cb45d7ab8f8667137a5a 100644
--- a/src/avatartranslator/directsimulation/AvatarSimulationTransaction.java
+++ b/src/avatartranslator/directsimulation/AvatarSimulationTransaction.java
@@ -79,7 +79,7 @@ public class AvatarSimulationTransaction {
}
public String toString() {
- String res = "" + id + " @" + clockValueWhenPerformed + " " + executedElement + " in block " + block.getName() + "\n";
+ String res = "" + id + " @" + clockValueWhenPerformed + " " + executedElement + " in block " + block.getName() + "\nattributes=";
for(String s: attributeValues) {
res += s + " ";
}
diff --git a/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java b/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
index 09ac7c6c3b83eff32b7b8408d47e2cb3e26d0f75..a3592357735dcf7cb0040337d7a4d2719027a609 100644
--- a/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
+++ b/src/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
@@ -61,7 +61,7 @@ public class AvatarSpecificationSimulation {
private long clockValue;
private LinkedList<AvatarSimulationBlock> blocks;
private LinkedList<AvatarActionOnSignal> asynchronousMessages;
- private LinkedList<AvatarSimulationTransaction> pendingTransactions;
+ private LinkedList<AvatarSimulationPendingTransaction> pendingTransactions;
private LinkedList<AvatarSimulationTransaction> allTransactions;
public AvatarSpecificationSimulation(AvatarSpecification _avspec) {
@@ -92,7 +92,7 @@ public class AvatarSpecificationSimulation {
asynchronousMessages = new LinkedList<AvatarActionOnSignal>();
// Create the structure for pending and executed transactions
- pendingTransactions = new LinkedList<AvatarSimulationTransaction>();
+ pendingTransactions = new LinkedList<AvatarSimulationPendingTransaction>();
allTransactions = new LinkedList<AvatarSimulationTransaction>();
}
@@ -102,7 +102,7 @@ public class AvatarSpecificationSimulation {
public void runSimulation() {
int index[];
- LinkedList<AvatarSimulationTransaction> selectedTransactions;
+ LinkedList<AvatarSimulationPendingTransaction> selectedTransactions;
TraceManager.addDev("Simulation started at time: " + clockValue);
boolean go = true;
@@ -125,7 +125,7 @@ public class AvatarSpecificationSimulation {
}
}
- TraceManager.addDev("Simulation finished at time: " + clockValue);
+ TraceManager.addDev("Simulation finished at time: " + clockValue + "\n--------------------------------------");
printExecutedTransactions();
}
@@ -138,8 +138,13 @@ public class AvatarSpecificationSimulation {
}
}
- public LinkedList<AvatarSimulationTransaction> selectTransactions(LinkedList<AvatarSimulationTransaction> _pendingTransactions) {
- LinkedList<AvatarSimulationTransaction> ll = new LinkedList<AvatarSimulationTransaction>();
+ public LinkedList<AvatarSimulationPendingTransaction> selectTransactions(LinkedList<AvatarSimulationPendingTransaction> _pendingTransactions) {
+ LinkedList<AvatarSimulationPendingTransaction> ll = new LinkedList<AvatarSimulationPendingTransaction>();
+
+
+
+
+
return ll;
}
diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
index 9b433e2fd3dcf4cd34cf852d697ba19a9e6a2749..45d816f768f8817acb17474e1196720b16df9939 100755
--- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
+++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java
@@ -654,7 +654,6 @@ public class AVATAR2UPPAAL {
public UPPAALLocation translateAvatarActionOnSignal(AvatarActionOnSignal _aaos, AvatarBlock _block, UPPAALTemplate _template, UPPAALLocation _previous, String _guard) {
- UPPAALLocation loc1;
String [] ss = manageSynchro(_block, _aaos);
UPPAALLocation loc = addLocation(_template);
@@ -669,24 +668,17 @@ public class AVATAR2UPPAAL {
TraceManager.addDev("* * * * * * * * * * * * * * * * Action on signal " + _aaos.getSignal().getName());
- /*loc1 = hash.get(_aaos);
- if (loc1 == null) {
- hash.put(_aaos, loc);
- /*if (_aaos.isCheckable()) {
- loc1 = addLocation(_template);
- tr = addTransition(_template, loc, loc1);
- TraceManager.addDev("---> Action on signal " + _aaos + " is selected for checking");
+ if (_aaos.isCheckable()) {
+ if (hashChecking.get(_aaos) == null) {
hashChecking.put(_aaos, loc);
loc.unsetOptimizable();
- loc.setCommitted();
+ /*} else {
+ UPPAALLocation loc1 = (UPPAALLocation)(hashChecking.get(_aaos));
+ UPPAALTransition tr1 = addTransition(_template, loc, loc1);
+ loc = loc1;
+ loc.setCommitted();*/
}
- } else {
- // Must link to the other location
- tr = addTransition(_template, loc, loc1);
- loc.setCommitted();
- TraceManager.addDev("<--- Action on signal " + _aaos + " is linked to a previous translation of it");
- return loc1;
- }*/
+ }
return loc;
}
@@ -716,7 +708,7 @@ public class AVATAR2UPPAAL {
tr = addTransition(_template, _previous, loc1);
tmps = convertGuard(_at.getGuard());
setGuard(tr, tmps);
- TraceManager.addDev("MAKE CHOICefrom guard");
+ TraceManager.addDev("MAKE CHOICE from guard");
setSynchronization(tr, "makeChoice!");
madeTheChoice = true;
loc = loc1;
@@ -888,6 +880,12 @@ public class AVATAR2UPPAAL {
if (hashChecking.get(at.getNext(0)) == null) {
hashChecking.put(aaos, locend);
locend.unsetOptimizable();
+ } else {
+ // Enforce the new information
+ TraceManager.addDev("---------------- Already set as checkable -> enforcing new information");
+ hashChecking.remove(aaos);
+ hashChecking.put(aaos, locend);
+ locend.unsetOptimizable();
}
}
@@ -1326,6 +1324,7 @@ public class AVATAR2UPPAAL {
if (loc != null) {
ret += "." + loc.name;
} else {
+ TraceManager.addDev("Unknown element in hash checking");
return null;
}
} else {
diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java
index 69c671032eecadb759cce2e3f89e30c1657aade2..687d40ec5f951106635e97656ff69800644b5953 100644
--- a/src/ui/AvatarDesignPanelTranslator.java
+++ b/src/ui/AvatarDesignPanelTranslator.java
@@ -307,6 +307,7 @@ public class AvatarDesignPanelTranslator {
ab = new AvatarBlock(block.getBlockName(), block);
_as.addBlock(ab);
listE.addCor(ab, block);
+ block.setAVATARID(ab.getID());
// Create attributes
v = block.getAttributeList();
@@ -654,6 +655,7 @@ public class AvatarDesignPanelTranslator {
}
//adag.setActionValue(makeTIFAction(asmdrs.getValue(), "?"));
listE.addCor(aaos, tgc);
+ tgc.setAVATARID(aaos.getID());
asm.addElement(aaos);
}
}
@@ -712,6 +714,7 @@ public class AvatarDesignPanelTranslator {
}
//adag.setActionValue(makeTIFAction(asmdrs.getValue(), "?"));
listE.addCor(aaos, tgc);
+ tgc.setAVATARID(aaos.getID());
asm.addElement(aaos);
}
}
@@ -727,6 +730,7 @@ public class AvatarDesignPanelTranslator {
astate.setCheckable();
}
listE.addCor(astate, tgc);
+ tgc.setAVATARID(astate.getID());
// Choice
@@ -735,6 +739,7 @@ public class AvatarDesignPanelTranslator {
choiceID ++;
asm.addElement(astate);
listE.addCor(astate, tgc);
+ tgc.setAVATARID(astate.getID());
// Random
} else if (tgc instanceof AvatarSMDRandom) {
@@ -763,6 +768,7 @@ public class AvatarDesignPanelTranslator {
asm.addElement(arandom);
listE.addCor(arandom, tgc);
+ tgc.setAVATARID(arandom.getID());
// Set timer
} else if (tgc instanceof AvatarSMDSetTimer) {
@@ -792,6 +798,7 @@ public class AvatarDesignPanelTranslator {
asettimer.setTimerValue(tmp);
asm.addElement(asettimer);
listE.addCor(asettimer, tgc);
+ tgc.setAVATARID(asettimer.getID());
}
}
@@ -817,6 +824,7 @@ public class AvatarDesignPanelTranslator {
aresettimer.setTimer(aa);
asm.addElement(aresettimer);
listE.addCor(aresettimer, tgc);
+ tgc.setAVATARID(aresettimer.getID());
}
}
@@ -842,6 +850,7 @@ public class AvatarDesignPanelTranslator {
aexpiretimer.setTimer(aa);
asm.addElement(aexpiretimer);
listE.addCor(aexpiretimer, tgc);
+ tgc.setAVATARID(aexpiretimer.getID());
}
}
@@ -849,6 +858,7 @@ public class AvatarDesignPanelTranslator {
} else if (tgc instanceof AvatarSMDStartState) {
astart = new AvatarStartState("start", tgc);
listE.addCor(astart, tgc);
+ tgc.setAVATARID(astart.getID());
asm.addElement(astart);
if (tgc.getFather() == null) {
asm.setStartState(astart);
@@ -858,6 +868,7 @@ public class AvatarDesignPanelTranslator {
} else if (tgc instanceof AvatarSMDStopState) {
astop = new AvatarStopState("stop", tgc);
listE.addCor(astop, tgc);
+ tgc.setAVATARID(astop.getID());
asm.addElement(astop);
}
}
@@ -985,6 +996,7 @@ public class AvatarDesignPanelTranslator {
element1.addNext(at);
at.addNext(element2);
listE.addCor(at, tgc);
+ tgc.setAVATARID(at.getID());
asm.addElement(at);
}
}
@@ -1209,470 +1221,7 @@ public class AvatarDesignPanelTranslator {
return !(TAttribute.isAValidId(tmp, false, false));
}
- /*public TURTLEModeling generateTURTLEModeling() {
- LinkedList<AvatarBDBlock> blocks = adp.getAvatarBDPanel().getFullBlockList();
- return generateTURTLEModeling(blocks, "");
- }
-
- public TURTLEModeling generateTURTLEModeling(Vector blocks, String preName) {
- LinkedList<AvatarBDBlock> ll = new LinkedList<AvatarBDBlock>();
- for(int i=0; i<blocks.size(); i++) {
- ll.add((AvatarBDBlock)blocks.get(i));
- }
- return generateTURTLEModeling(ll, preName);
- }
-
- public TURTLEModeling generateTURTLEModeling(LinkedList<AvatarBDBlock> blocks, String preName) {
- TURTLEModeling tmodel = new TURTLEModeling();
- createTClassesFromBlocks(tmodel, blocks, preName);
- createRelationsBetweenTClasses(tmodel, blocks, preName);
- //addTClasses(adp, blocks, preName, tmodel);
- //addRelations(adp, tmodel);
- return tmodel;
- }
-
- private void addCheckingError(CheckingError ce) {
- if (checkingErrors == null) {
- checkingErrors = new Vector();
- }
- checkingErrors.addElement(ce);
- }
-
- private void addWarning(CheckingError ce) {
- if (warnings == null) {
- warnings = new Vector();
- }
- warnings.addElement(ce);
- }
-
- public void createTClassesFromBlocks(TURTLEModeling tm, LinkedList<AvatarBDBlock> blocks, String preName) {
- TClass t;
- Vector v;
- int i;
- TAttribute a;
- Param p;
- AvatarMethod am;
- Gate g;
- AvatarSignal as;
-
- for(AvatarBDBlock block: blocks) {
- t = new TClass(preName + block.getBlockName(), true);
-
- tm.addTClass(t);
- listE.addCor(t, block, preName);
-
- // Create attributes
- v = block.getAttributeList();
- for(i=0; i<v.size(); i++) {
- a = (TAttribute)(v.elementAt(i));
- if ((a.getType() == TAttribute.NATURAL) || (a.getType() == TAttribute.INTEGER)){
- p = new Param(a.getId(), Param.NAT, a.getInitialValue());
- p.setAccess(a.getAccessString());
- t.addParameter(p);
- }
- if (a.getType() == TAttribute.BOOLEAN) {
- p = new Param(a.getId(), Param.BOOL, a.getInitialValue());
- p.setAccess(a.getAccessString());
- t.addParameter(p);
- }
- }
-
- // Create internal gates
- v = block.getMethodList();
- for(i=0; i<v.size(); i++) {
- am = (AvatarMethod)(v.get(i));
- g = new Gate(am.getId(), Gate.GATE, false);
- t.addGate(g);
- }
-
- // Create external gates from signals
- v = block.getSignalList();
- for(i=0; i<v.size(); i++) {
- as = (AvatarSignal)(v.get(i));
- if (as.getInOut() == AvatarSignal.IN) {
- g = new Gate(as.getId(), Gate.INGATE, false);
- } else {
- g = new Gate(as.getId(), Gate.OUTGATE, false);
- }
- t.addGate(g);
- }
-
- // Activity Diagram
- buildStateMachineDiagram(tm, block, t);
- }
- }
-
- private void buildStateMachineDiagram(TURTLEModeling tm, AvatarBDBlock block, TClass t) {
- int j;
- //TActivityDiagramPanel tadp;
- AvatarSMDPanel asmdp = block.getAvatarSMDPanel();
- String name = block.getBlockName();
- TDiagramPanel tdp;
-
- int size = checkingErrors.size();
-
- if (asmdp == null) {
- return;
- }
-
- tdp = (TDiagramPanel)asmdp;
-
- int indexTdp = panels.indexOf(tdp);
- if (indexTdp > -1) {
- TraceManager.addDev("Found similar diagram for " + block.getBlockName());
- t.setActivityDiagram((activities.get(indexTdp)).duplicate(t));
-
- //System.out.println("AD of " + t.getName() + "=");
- //t.getActivityDiagram().print();
-
- // Must fill correspondances!
- ADComponent ad0, ad1;
- TGComponent tgcad;
- for(int adi=0; adi<t.getActivityDiagram().size(); adi++) {
- ad0 = (ADComponent)(t.getActivityDiagram().get(adi));
- ad1 = (ADComponent)(activities.get(indexTdp).get(adi));
- tgcad = listE.getTG(ad1);
- if (tgcad != null ){
- //System.out.println("Adding correspondance for " + ad0);
- listE.addCor(ad0, tgcad);
- }
- }
-
- return;
- }
-
- // search for start state
- LinkedList list = asmdp.getComponentList();
- Iterator iterator = list.listIterator();
- TGComponent tgc;
- AvatarSMDStartState tss = null;
- int cptStart = 0;
- while(iterator.hasNext()) {
- tgc = (TGComponent)(iterator.next());
- if (tgc instanceof AvatarSMDStartState){
- tss = (AvatarSMDStartState)tgc;
- cptStart ++;
- }
- }
-
- if (tss == null) {
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "No start state in the state machine diagram of " + name);
- ce.setTClass(t);
- ce.setTDiagramPanel(tdp);
- addCheckingError(ce);
- return;
- }
-
- if (cptStart > 1) {
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "More than one start state in the state machine diagram of " + name);
- ce.setTClass(t);
- ce.setTDiagramPanel(tdp);
- addCheckingError(ce);
- return;
- }
-
- // This shall also be true for all composite state: at most one start state!
- tgc = checkForStartStateOfCompositeStates(asmdp);
- if (tgc != null) {
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "More than one start state in composite state");
- ce.setTClass(t);
- ce.setTDiagramPanel(tdp);
- ce.setTGComponent(tgc);
- addCheckingError(ce);
- return;
- }
-
- // Creation of the activity diagram
- ADStart ads;
- ADStop adstop;
- ads = new ADStart();
-
- listE.addCor(ads, tss);
- ActivityDiagram ad = new ActivityDiagram(ads);
-
- adstop = new ADStop();
- ads.addNext(adstop);
- ad.add(adstop);
-
- t.setActivityDiagram(ad);
-
- // First pass: creating TIF components, but no interconnection between them
- ADParallel adpar;
- iterator = asmdp.getAllComponentList().listIterator();
- ADActionStateWithGate adag;
- Gate g;
- ADJunction adj;
- ADChoice adch;
-
- AvatarSMDReceiveSignal asmdrs;
- AvatarSMDSendSignal asmdss;
-
- while(iterator.hasNext()) {
- tgc = (TGComponent)(iterator.next());
-
- // Parallel
- if (tgc instanceof AvatarSMDParallel) {
- adpar = new ADParallel();
- listE.addCor(adpar, tgc);
- ad.add(adpar);
-
- // Receive signal
- } else if (tgc instanceof AvatarSMDReceiveSignal) {
- asmdrs = (AvatarSMDReceiveSignal)tgc;
- g = t.getGateByName(asmdrs.getSignalName());
- if (g == null) {
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Unknown signal: " + asmdrs.getSignalName());
- ce.setTClass(t);
- ce.setTDiagramPanel(tdp);
- ce.setTGComponent(tgc);
- addCheckingError(ce);
- } else {
- adag = new ADActionStateWithGate(g);
- adag.setActionValue(makeTIFAction(asmdrs.getValue(), "?"));
- listE.addCor(adag, tgc);
- ad.add(adag);
- }
-
- // Send signal
- } else if (tgc instanceof AvatarSMDSendSignal) {
- asmdss = (AvatarSMDSendSignal)tgc;
- g = t.getGateByName(asmdss.getSignalName());
- if (g == null) {
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Unknown signal: " + asmdss.getSignalName());
- ce.setTClass(t);
- ce.setTDiagramPanel(tdp);
- ce.setTGComponent(tgc);
- addCheckingError(ce);
- } else {
- adag = new ADActionStateWithGate(g);
- adag.setActionValue(makeTIFAction(asmdss.getValue(), "!"));
- listE.addCor(adag, tgc);
- ad.add(adag);
- }
-
- // State
- } else if (tgc instanceof AvatarSMDState) {
- // First case: no internal
- // One junction followed by one choice
- // The junction remains the reference
- adj = new ADJunction();
- listE.addCor(adj, tgc);
- ad.add(adj);
- adch = new ADChoice();
- ad.add(adch);
- adj.addNext(adch);
-
- // Start state
- } else if (tgc instanceof AvatarSMDStartState) {
-
-
- // Stop state
- } else if (tgc instanceof AvatarSMDStopState) {
- adstop = new ADStop();
- listE.addCor(adstop, tgc);
- ad.add(adstop);
- }
- }
-
- if (checkingErrors.size() != size) {
- return;
- }
-
- // Second pass: connectors between components
- iterator = asmdp.getAllComponentList().listIterator();
- AvatarSMDConnector asmdco;
- TGComponent tgc1, tgc2;
- Object o;
- boolean first;
-
- while(iterator.hasNext()) {
- tgc = (TGComponent)(iterator.next());
- if (tgc instanceof AvatarSMDConnector) {
- asmdco = (AvatarSMDConnector)tgc;
- tgc1 = tdp.getComponentToWhichBelongs(asmdco.getTGConnectingPointP1());
- tgc2 = tdp.getComponentToWhichBelongs(asmdco.getTGConnectingPointP2());
- if ((tgc1 == null) || (tgc2 == null)) {
- TraceManager.addDev("tgcs null in Avatar translation");
- } else {
- // First case: not quiting a composite state
- first = true;
- if (tgc1 instanceof AvatarSMDState) {
- if (((AvatarSMDState)tgc1).isACompositeState()) {
- first = false;
- }
- }
- if (first) {
- connect(asmdco, tgc1, tgc2, tss, ad, t, tdp);
- } else {
- // Second case: not yet implemented...
- }
- }
- }
- }
-
- panels.add(tdp);
- activities.add(ad);
- }
-
- private void connect(AvatarSMDConnector _asmdco, TGComponent _tgc1, TGComponent _tgc2, AvatarSMDStartState _tss, ActivityDiagram _ad, TClass _t, TDiagramPanel _tdp) {
- ADComponent adc1, adc2;
- ADComponent adc;
- String s1, s2;
- ADChoice adch;
- ADTimeInterval adti;
- ADDelay addelay;
- boolean hasChoice = false;
- Vector<String> v;
- Gate g;
- Param p;
- ADActionStateWithGate adag;
- ADActionStateWithParam adap;
-
- // Search for the two elements to connect
- if (_tgc1 instanceof AvatarSMDStartState) {
- if (_tgc1 != _tss) {
- _tgc1 = _tgc1.getFather(); // Shall be a state!
- }
- }
-
- // Search for the two related TIF Components
- adc1 = listE.getADComponent(_tgc1);
- adc2 = listE.getADComponent(_tgc2);
-
-
-
- if ((adc1 == null) || (adc2 == null)) {
- TraceManager.addDev("adcs null in Avatar translation");
- } else {
- adc = adc1;
-
- if (_tgc1 instanceof AvatarSMDState) {
- adc1 = adc1.getNext(0); // shall be a choice!
- }
-
- // Guard
- if (adc1 instanceof ADChoice) {
- adch = (ADChoice)adc1;
- s1 = _asmdco.getGuard();
- if (s1 == null) {
- s1 = "[ ]";
- }
- adch.addGuard(s1);
- hasChoice = true;
- }
-
- // Delay
- s1 = _asmdco.getTotalMinDelay();
- s2 = _asmdco.getTotalMaxDelay();
- if (s1.length() > 0) {
- if (s2.length() > 0) {
- adti = new ADTimeInterval();
- adti.setValue(s1, s2);
- _ad.add(adti);
- listE.addCor(adti, _asmdco);
- adc.addNext(adti);
- adc = adti;
- } else {
- addelay = new ADDelay();
- addelay.setValue(s1);
- _ad.add(addelay);
- listE.addCor(addelay, _asmdco);
- adc.addNext(addelay);
- adc = addelay;
- }
- }
-
- // Actions
- v = _asmdco.getActions();
- if (v.size() == 0) {
- if (hasChoice) {
- // Must make an action to make the choice deterministic, except if the next component is an action!
- if (!((_tgc2 instanceof AvatarSMDReceiveSignal) || (_tgc2 instanceof AvatarSMDSendSignal))) {
- adc = makeChoiceAction(_ad, _t, adc, _asmdco);
- TraceManager.addDev("Adding artifical action for choice to be deterministic");
- }
- }
- } else {
- // has actions!
- if (!isActionOnGate(_t, v.get(0))) {
- if (hasChoice) {
- // Must make an action to make the choice deterministic, except if the next component is an action!
- if (!((_tgc2 instanceof AvatarSMDReceiveSignal) || (_tgc2 instanceof AvatarSMDSendSignal))) {
- adc = makeChoiceAction(_ad, _t, adc, _asmdco);
- TraceManager.addDev("Adding artifical action for choice to be deterministic");
- }
- }
- }
-
- for (String action: v) {
- g = getGateFromActionState(_t, action);
- p = getParamFromActionState(_t, action);
- if (g != null) {
- adag = new ADActionStateWithGate(g);
- _ad.addElement(adag);
- adag.setActionValue(makeTIFAction(action, "!"));
- listE.addCor(adag, _asmdco);
- adc.addNext(adag);
- adc = adag;
- } else if (p != null) {
- adap = new ADActionStateWithParam(p);
- _ad.addElement(adap);
- adap.setActionValue(makeTIFActionOnParam(action));
- listE.addCor(adap, _asmdco);
- adc.addNext(adap);
- adc = adap;
- } else {
- CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed action: " + action);
- ce.setTClass(_t);
- ce.setTDiagramPanel(_tdp);
- ce.setTGComponent(_asmdco);
- addCheckingError(ce);
- return;
- }
- }
- }
-
- adc.addNext(adc2);
- }
-
- }
-
- private boolean isActionOnGate(TClass _t, String _s) {
- Gate g = getGateFromActionState(_t, _s);
- return (g != null);
- }
-
- private Gate getGateFromActionState(TClass _t, String _action) {
- String action = _action;
- int index0 = action.indexOf("(");
- if (index0 != -1) {
- action = _action.substring(0, index0);
- }
-
- return _t.getGateByName(action);
- }
-
- private Param getParamFromActionState(TClass _t, String _action) {
- String action = _action;
- int index0 = action.indexOf("(");
- if (index0 != -1) {
- action = _action.substring(0, index0);
- }
-
- return _t.getParamByName(action);
- }
-
- private ADComponent makeChoiceAction(ActivityDiagram _ad, TClass _t, ADComponent _adc, TGComponent _asmdco) {
- Gate g = _t.addNewGateIfApplicable("choice__", true);
- ADActionStateWithGate adag = new ADActionStateWithGate(g);
- adag.setActionValue("");
- _ad.add(adag);
- _adc.addNext(adag);
- listE.addCor(adag, _asmdco);
- return adag;
- }
-
- private String makeTIFActionOnParam(String _s) {
+ /*private String makeTIFActionOnParam(String _s) {
String ret = _s.trim();
int index0 = ret.indexOf("=");
if (index0 == -1) {
@@ -1718,51 +1267,6 @@ public class AvatarDesignPanelTranslator {
}
}
return null;
- }
-
-
- public void createRelationsBetweenTClasses(TURTLEModeling tm, LinkedList<AvatarBDBlock> blocks, String preName) {
- adp.getAvatarBDPanel().updateAllSignalsOnConnectors();
- Iterator iterator = adp.getAvatarBDPanel().getComponentList().listIterator();
-
- TGComponent tgc;
- AvatarBDPortConnector port;
- AvatarBDBlock block1, block2;
- LinkedList<String> l1, l2;
- int i;
- String name1, name2;
- Relation r;
- TClass t1, t2;
- Gate g1, g2;
-
- while(iterator.hasNext()) {
- tgc = (TGComponent)(iterator.next());
- if (tgc instanceof AvatarBDPortConnector) {
- port = (AvatarBDPortConnector)tgc;
- block1 = port.getAvatarBDBlock1();
- block2 = port.getAvatarBDBlock2();
-
- t1 = tm.getTClassWithName(preName + block1.getBlockName());
- t2 = tm.getTClassWithName(preName + block2.getBlockName());
- r = new Relation(Relation.SYN, t1, t2, true);
- // Signals of l1
- l1 = port.getListOfSignalsOrigin();
- l2 = port.getListOfSignalsDestination();
-
- for(i=0; i<l1.size(); i++) {
- name1 = AvatarSignal.getSignalNameFromFullSignalString(l1.get(i));
- name2 = AvatarSignal.getSignalNameFromFullSignalString(l2.get(i));
- g1 = t1.getGateByName(name1);
- g2 = t2.getGateByName(name2);
- if ((g1 != null) && (g2 != null)) {
- r.addGates(g1, g2);
- } else {
- TraceManager.addDev("null gates in AVATAR relation: " + name1 + " " + name2);
- }
- }
- tm.addRelation(r);
- }
- }
}*/
diff --git a/src/ui/ColorManager.java b/src/ui/ColorManager.java
index 9e3f732990ce84339f9063725b40d359c55c1634..edc62d14549c9c3d0e80189fd88164e22d50d802 100755
--- a/src/ui/ColorManager.java
+++ b/src/ui/ColorManager.java
@@ -67,6 +67,7 @@ public class ColorManager {
public static final Color CURRENT_COMMAND_TERMINATED = new Color(255, 42, 50, 200);
public static final Color CURRENT_COMMAND_UNKNOWN = new Color(107, 97, 97, 200);
public static final Color DIPLOID = new Color(163, 5, 253);
+ public static final Color AVATARID = new Color(163, 5, 253);
public static Color SELECTED_0 = Color.blue;
public static final Color MOVING_0 = Color.magenta;
public static final Color ADDING_0 = Color.lightGray;
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index bd5cfdfa825520c70753fbc8d0f4f978791e86fd..166089541cbf9f578adaaa85bc10dbe13ccbdec4 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -1637,7 +1637,7 @@ public class GTURTLEModeling {
AvatarDesignPanelTranslator adpt = new AvatarDesignPanelTranslator(adp);
avatarspec = adpt.generateAvatarSpecification(blocks);
optimizeAvatar = _optimize;
- TraceManager.addDev("AvatarSpec:" + avatarspec.toString() + "\n\n");
+ //TraceManager.addDev("AvatarSpec:" + avatarspec.toString() + "\n\n");
tmState = 3;
listE = adpt.getCorrespondanceTGElement();
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index 1825265fa647f54d5b11bd4ac523cc7ed8f85469..15311f716039fdcea168837eb3a584dd28b12bb8 100755
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -5626,6 +5626,19 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
}
}
+ // AVATAR Simulation
+ public void setAVATARIDs(boolean b) {
+ TDiagramPanel.AVATAR_ID_ON = b;
+ TDiagramPanel tdp = getCurrentTDiagramPanel();
+ if (tdp != null) {
+ tdp.repaint();
+ }
+ }
+
+ public void toggleAVATARIDs() {
+ setAVATARIDs(!TDiagramPanel.AVATAR_ID_ON);
+ TraceManager.addDev("AVATAR id: " + TDiagramPanel.AVATAR_ID_ON);
+ }
// For simulation purpose
public void resetAllDIPLOIDs() {
@@ -6137,6 +6150,8 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener {
toggleAttributes();
} else if (command.equals(actions[TGUIAction.ACT_TOGGLE_DIPLO_ID].getActionCommand())) {
toggleDiploIDs();
+ } else if (command.equals(actions[TGUIAction.ACT_TOGGLE_AVATAR_ID].getActionCommand())) {
+ toggleAVATARIDs();
} else if (command.equals(actions[TGUIAction.ACT_TOGGLE_GATES].getActionCommand())) {
toggleGates();
} else if (command.equals(actions[TGUIAction.ACT_TOGGLE_SYNCHRO].getActionCommand())) {
diff --git a/src/ui/TDiagramPanel.java b/src/ui/TDiagramPanel.java
index 9782a2caf4c3710a6724e3be0a23de5a43954c4e..265ac4c18ea4436e40807f522ccb00c2a4eb977c 100755
--- a/src/ui/TDiagramPanel.java
+++ b/src/ui/TDiagramPanel.java
@@ -193,6 +193,9 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree {
public static boolean DIPLO_ANIMATE_ON;
public static boolean DIPLO_ID_ON;
public static boolean DIPLO_TRANSACTION_PROGRESSION_ON;
+
+ // AVATAR ID -> for simulation purpose
+ public static boolean AVATAR_ID_ON;
// Constructor
public TDiagramPanel(MainGUI _mgui, TToolBar _ttb) {
diff --git a/src/ui/TGComponent.java b/src/ui/TGComponent.java
index b60f17c0103d682fd94646ca10669edd9edabf1f..78e8949aff562f02937effa0f9015b916b246b6d 100755
--- a/src/ui/TGComponent.java
+++ b/src/ui/TGComponent.java
@@ -106,6 +106,10 @@ public abstract class TGComponent implements CDElement, GenericTree {
private int DIPLOID = -1;
private boolean DIPLO_running = false;
+ // AVATAR ID
+ private int AVATARID = -1;
+ private boolean AVATAR_running = false;
+
// Zone of drawing -> relative to father if applicable
protected int minX;
@@ -469,6 +473,13 @@ public abstract class TGComponent implements CDElement, GenericTree {
}
}
+ public void drawAVATARID(Graphics g) {
+ if (getAVATARID() != -1) {
+ g.setColor(ColorManager.AVATARID);
+ g.drawString(""+getAVATARID(), x+width, y+height + 5);
+ }
+ }
+
public void drawRunningDiploID(Graphics g, RunningInfo ri) {
//System.out.println("Drawing running DIPLO");
int wb = 30;
@@ -679,6 +690,8 @@ public abstract class TGComponent implements CDElement, GenericTree {
}
} else if (tdp.DIPLO_ID_ON) {
drawDiploID(g);
+ } else if (tdp.AVATAR_ID_ON) {
+ drawAVATARID(g);
}
if (this instanceof EmbeddedComment) {
@@ -2283,6 +2296,15 @@ public abstract class TGComponent implements CDElement, GenericTree {
return DIPLOID;
}
+ // AVATAR ID
+ public void setAVATARID(int _ID) {
+ AVATARID = _ID;
+ }
+
+ public int getAVATARID() {
+ return AVATARID;
+ }
+
// saving
diff --git a/src/ui/TGConnector.java b/src/ui/TGConnector.java
index f2a5089ab099910d0ad20edd9729998422e17a89..6f711736cf04eec01f03524cd9e3a1db04b2c02c 100755
--- a/src/ui/TGConnector.java
+++ b/src/ui/TGConnector.java
@@ -220,6 +220,21 @@ public abstract class TGConnector extends TGCWithInternalComponent {
makeSquareWithoutMovingTGComponents();
return true;
}
+
+ public void drawAVATARID(Graphics g) {
+ if (getAVATARID() != -1) {
+ g.setColor(ColorManager.AVATARID);
+ int xx, yy;
+ if (getIndexOfLastTGCPointOfConnector() >= 0) {
+ xx = tgcomponent[0].x;
+ yy = tgcomponent[0].y;
+ } else {
+ xx = p2.getX();
+ yy = p2.getY();
+ }
+ g.drawString(""+getAVATARID(), (p1.getX()+xx)/2, ((p1.getY()+yy)/2) + 5);
+ }
+ }
public void makeSquareWithoutMovingTGComponents() {
if ((p1 == null) ||(p2 == null)) {
diff --git a/src/ui/TGUIAction.java b/src/ui/TGUIAction.java
index c2768bdb3dd6a8c1cfcde1ff252127950a869c81..c10584852ad1795cee0edc48cb6d878a12479306 100755
--- a/src/ui/TGUIAction.java
+++ b/src/ui/TGUIAction.java
@@ -441,6 +441,7 @@ public class TGUIAction extends AbstractAction {
public static final int ACT_TOGGLE_ATTR = 220;
public static final int ACT_TOGGLE_DIPLO_ID = 264;
+ public static final int ACT_TOGGLE_AVATAR_ID = 334;
public static final int ACT_TOGGLE_INTERNAL_COMMENT = 227;
@@ -453,7 +454,7 @@ public class TGUIAction extends AbstractAction {
//Action for the help button created by Solange
public static final int PRUEBA_1 = 205;
- public static final int NB_ACTION = 334;
+ public static final int NB_ACTION = 335;
private static final TAction [] actions = new TAction[NB_ACTION];
@@ -541,6 +542,7 @@ public class TGUIAction extends AbstractAction {
actions[ACT_TOGGLE_ATTR] = new TAction("toggle-attr-command", "Show / hide attributes (OFF -> partial -> Full)", IconManager.imgic138, IconManager.imgic138, "Show / hide element attributes (OFF -> Partial -> Full)", "Show / hide attributes (OFF -> Partial -> Full)", '0');
actions[ACT_TOGGLE_DIPLO_ID] = new TAction("toggle-tml-id", "Show / hide DIPLODOCUS IDs", IconManager.imgic138, IconManager.imgic138, "Show / hide DIPLODOCUS IDs", "Show / hide DIPLODOCUS IDs", '0');
+ actions[ACT_TOGGLE_AVATAR_ID] = new TAction("toggle-avatar-id", "Show / hide AVATAR IDs", IconManager.imgic138, IconManager.imgic138, "Show / hide AVATAR IDs", "Show / hide AVATAR IDs", '0');
actions[ACT_TOGGLE_INTERNAL_COMMENT] = new TAction("toggle-internal-comment-command", "Show / hide (OFF -> partial -> Full)", IconManager.imgic138, IconManager.imgic138, "Show / hide internal comments (OFF -> partial -> Full)", "Show / hide internal comments (OFF -> partial -> Full)", '0');
@@ -549,7 +551,7 @@ public class TGUIAction extends AbstractAction {
actions[ACT_GEN_LOTOS] = new TAction("gen_lotos-command", "Generate LOTOS", IconManager.imgic34, IconManager.imgic35, "Generate LOTOS specification", "Generates a LOTOS specification from TURTLE diagrams", '0');
actions[ACT_ONECLICK_LOTOS_RG] = new TAction("gen_rglotos-command", "Generate LOTOS-based RG", IconManager.imgic342, IconManager.imgic342, "Generate LOTOS-based RG ", "Generates a LOTOS-based RG from TURTLE diagrams", '0');
actions[ACT_ONECLICK_RTLOTOS_RG] = new TAction("gen_rgrtlotos-command", "Generate RT-LOTOS-based RG", IconManager.imgic342, IconManager.imgic342, "Generate RT-LOTOS-based RG ", "Generates an RT-LOTOS-based RG from TURTLE diagrams", '0');
- actions[ACT_GEN_UPPAAL] = new TAction("gen_uppaal-command", "Generate UPPAAL", IconManager.imgic34, IconManager.imgic35, "Generate UPPAAL specification", "Generates a UPPAAL specification from DIPLODOCUS diagrams", '0');
+ actions[ACT_GEN_UPPAAL] = new TAction("gen_uppaal-command", "Generate UPPAAL", IconManager.imgic34, IconManager.imgic35, "Generate UPPAAL specification", "Generates a UPPAAL specification from TTool diagrams", '0');
actions[ACT_GEN_PROVERIF] = new TAction("gen_proverif-command", "Generate ProVerif Code", IconManager.imgic34, IconManager.imgic35, "Generate ProVerif specification", "Generates a ProVerif specification from AVATAR diagrams", '0');
actions[ACT_GEN_JAVA] = new TAction("gen_java-command", "Generate JAVA", IconManager.imgic38, IconManager.imgic39, "Generate JAVA", "Generates Java code from TURTLE diagrams", 0);
actions[ACT_SIMU_JAVA] = new TAction("gen_simujava-command", "Java-based simulation", IconManager.imgic38, IconManager.imgic39, "JAVA-based simualtion", "Simulate diagrams using Java language", 0);
diff --git a/src/ui/avatarsmd/AvatarSMDToolBar.java b/src/ui/avatarsmd/AvatarSMDToolBar.java
index 91157082f02d265086267baeec67beb79454a0aa..b39bd7174b8daaf46d7a3164abc63eb3f50bb681 100755
--- a/src/ui/avatarsmd/AvatarSMDToolBar.java
+++ b/src/ui/avatarsmd/AvatarSMDToolBar.java
@@ -83,6 +83,9 @@ public class AvatarSMDToolBar extends TToolBar {
mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false);
mgui.actions[TGUIAction.ACT_ZOOM_LESS].setEnabled(false);
mgui.actions[TGUIAction.ACT_SHOW_ZOOM].setEnabled(false);
+
+ mgui.actions[TGUIAction.ACT_TOGGLE_AVATAR_ID].setEnabled(b);
+
mgui.updateZoomInfo();
}
@@ -163,12 +166,12 @@ public class AvatarSMDToolBar extends TToolBar {
/*this.addSeparator();
button = this.add(mgui.actions[TGUIAction.ACT_TOGGLE_INTERNAL_COMMENT]);
- button.addMouseListener(mgui.mouseHandler);
+ button.addMouseListener(mgui.mouseHandler);*/
this.addSeparator();
- button = this.add(mgui.actions[TGUIAction.ACT_TOGGLE_DIPLO_ID]);
- button.addMouseListener(mgui.mouseHandler);*/
+ button = this.add(mgui.actions[TGUIAction.ACT_TOGGLE_AVATAR_ID]);
+ button.addMouseListener(mgui.mouseHandler);
}
} // Class