diff --git a/build.txt b/build.txt
index 1c723c5cd50818250a5b0817e9fac2825d689e9e..6c361ce5dabae8e97273b38868b38445abedad3d 100644
--- a/build.txt
+++ b/build.txt
@@ -1 +1 @@
-14564
\ No newline at end of file
+14607
\ No newline at end of file
diff --git a/modeling/DIPLODOCUS/SmartCardProtocol.xml b/modeling/DIPLODOCUS/SmartCardProtocol.xml
index addf5299b1935ce1aead888b2e0eed312c193341..737230be075b653e24d92f0af697d383b6abd79e 100755
--- a/modeling/DIPLODOCUS/SmartCardProtocol.xml
+++ b/modeling/DIPLODOCUS/SmartCardProtocol.xml
@@ -1,6 +1,6 @@
<?xml version="1.0" encoding="UTF-8"?>
-<TURTLEGMODELING version="3.0 beta" ANIMATE_INTERACTIVE_SIMULATION="true" ACTIVATE_PENALTIES="false" UPDATE_INFORMATION_DIPLO_SIM="false" ANIMATE_WITH_INFO_DIPLO_SIM="true" OPEN_DIAG_DIPLO_SIM="false" LAST_SELECTED_MAIN_TAB="3" LAST_SELECTED_SUB_TAB="0">
+<TURTLEGMODELING version="3.0 beta" ANIMATE_INTERACTIVE_SIMULATION="true" ACTIVATE_PENALTIES="false" UPDATE_INFORMATION_DIPLO_SIM="false" ANIMATE_WITH_INFO_DIPLO_SIM="true" OPEN_DIAG_DIPLO_SIM="false" LAST_SELECTED_MAIN_TAB="1" LAST_SELECTED_SUB_TAB="0">
<Modeling type="TML Component Design" nameTab="AppC" tabs="TML Component Task Diagram$Application$TCPIP$Timer$InterfaceDevice$SmartCard" >
<TMLComponentTaskDiagramPanel name="TML Component Task Diagram" minX="0" maxX="2724" minY="0" maxY="916" channels="true" events="true" requests="true" considerExecOperators="true" considerTimingOperators="true" zoom="1.0000000000000018" >
@@ -8,8 +8,8 @@
<cdparam x="535" y="347" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="556" y="321" id="113" />
-<P2 x="534" y="395" id="68" />
+<P1 x="556" y="347" id="113" />
+<P2 x="547" y="382" id="68" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -17,8 +17,8 @@
<cdparam x="820" y="398" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="1025" y="471" id="210" />
-<P2 x="761" y="548" id="98" />
+<P1 x="1025" y="497" id="210" />
+<P2 x="761" y="574" id="98" />
<Point x="887" y="577" />
<AutomaticDrawing data="true" />
<new d="false" />
@@ -37,7 +37,7 @@
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
<P1 x="710" y="403" id="96" />
-<P2 x="693" y="321" id="135" />
+<P2 x="693" y="347" id="135" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -45,8 +45,8 @@
<cdparam x="522" y="390" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="534" y="369" id="63" />
-<P2 x="453" y="322" id="33" />
+<P1 x="521" y="382" id="63" />
+<P2 x="466" y="335" id="33" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -63,8 +63,8 @@
<cdparam x="656" y="426" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="805" y="542" id="92" />
-<P2 x="969" y="474" id="196" />
+<P1 x="816" y="552" id="92" />
+<P2 x="969" y="495" id="196" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -72,8 +72,8 @@
<cdparam x="656" y="400" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="805" y="509" id="90" />
-<P2 x="931" y="466" id="198" />
+<P1 x="816" y="519" id="90" />
+<P2 x="921" y="476" id="198" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -82,7 +82,7 @@
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
<P1 x="751" y="406" id="82" />
-<P2 x="842" y="362" id="162" />
+<P2 x="829" y="375" id="162" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -90,8 +90,8 @@
<cdparam x="689" y="292" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="842" y="388" id="166" />
-<P2 x="931" y="352" id="188" />
+<P1 x="855" y="375" id="166" />
+<P2 x="921" y="362" id="188" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -99,8 +99,8 @@
<cdparam x="656" y="377" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="805" y="481" id="86" />
-<P2 x="931" y="443" id="190" />
+<P1 x="816" y="491" id="86" />
+<P2 x="921" y="453" id="190" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -108,8 +108,8 @@
<cdparam x="656" y="351" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="805" y="448" id="88" />
-<P2 x="931" y="416" id="192" />
+<P1 x="816" y="458" id="88" />
+<P2 x="921" y="426" id="192" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -117,8 +117,8 @@
<cdparam x="741" y="296" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="931" y="387" id="194" />
-<P2 x="805" y="419" id="84" />
+<P1 x="921" y="397" id="194" />
+<P2 x="816" y="429" id="84" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -126,8 +126,8 @@
<cdparam x="735" y="260" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="931" y="317" id="186" />
-<P2 x="734" y="269" id="123" />
+<P1 x="918" y="330" id="186" />
+<P2 x="747" y="282" id="123" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -135,8 +135,8 @@
<cdparam x="641" y="230" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="734" y="235" id="125" />
-<P2 x="931" y="278" id="184" />
+<P1 x="747" y="248" id="125" />
+<P2 x="918" y="291" id="184" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -144,8 +144,8 @@
<cdparam x="641" y="195" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="734" y="190" id="127" />
-<P2 x="931" y="235" id="182" />
+<P1 x="747" y="203" id="127" />
+<P2 x="918" y="248" id="182" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -153,8 +153,8 @@
<cdparam x="740" y="353" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="842" y="362" id="161" />
-<P2 x="734" y="301" id="129" />
+<P1 x="829" y="375" id="161" />
+<P2 x="747" y="314" id="129" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -162,8 +162,8 @@
<cdparam x="460" y="270" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="534" y="282" id="119" />
-<P2 x="453" y="286" id="39" />
+<P1 x="521" y="295" id="119" />
+<P2 x="466" y="299" id="39" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -171,8 +171,8 @@
<cdparam x="387" y="129" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="453" y="116" id="43" />
-<P2 x="534" y="116" id="131" />
+<P1 x="464" y="126" id="43" />
+<P2 x="524" y="126" id="131" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -180,8 +180,8 @@
<cdparam x="389" y="200" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="453" y="202" id="37" />
-<P2 x="534" y="202" id="117" />
+<P1 x="466" y="215" id="37" />
+<P2 x="521" y="215" id="117" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -189,8 +189,8 @@
<cdparam x="460" y="236" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="534" y="247" id="115" />
-<P2 x="453" y="247" id="35" />
+<P1 x="521" y="260" id="115" />
+<P2 x="466" y="260" id="35" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -198,8 +198,8 @@
<cdparam x="389" y="163" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="453" y="156" id="41" />
-<P2 x="534" y="156" id="121" />
+<P1 x="466" y="169" id="41" />
+<P2 x="521" y="169" id="121" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -207,8 +207,8 @@
<cdparam x="967" y="190" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector from TGComponent to TGComponent" value="Connector between ports" />
-<P1 x="931" y="185" id="180" />
-<P2 x="734" y="111" id="109" />
+<P1 x="918" y="198" id="180" />
+<P2 x="747" y="124" id="109" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -216,7 +216,7 @@
<cdparam x="1028" y="535" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector from TGComponent to TGComponent" value="Connector between ports" />
-<P1 x="630" y="324" id="133" />
+<P1 x="630" y="345" id="133" />
<P2 x="669" y="406" id="94" />
<AutomaticDrawing data="true" />
<new d="false" />
@@ -225,8 +225,8 @@
<cdparam x="1308" y="303" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector from TGComponent to TGComponent" value="Connector between ports" />
-<P1 x="1232" y="368" id="146" />
-<P2 x="1167" y="370" id="200" />
+<P1 x="1222" y="378" id="146" />
+<P2 x="1178" y="380" id="200" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -234,8 +234,8 @@
<cdparam x="1172" y="437" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector from TGComponent to TGComponent" value="Connector between ports" />
-<P1 x="1167" y="405" id="202" />
-<P2 x="1232" y="403" id="148" />
+<P1 x="1178" y="415" id="202" />
+<P2 x="1222" y="413" id="148" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
@@ -243,8 +243,8 @@
<cdparam x="1041" y="162" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector from TGComponent to TGComponent" value="Connector between ports" />
-<P1 x="1167" y="198" id="204" />
-<P2 x="1167" y="266" id="206" />
+<P1 x="1178" y="208" id="204" />
+<P2 x="1178" y="276" id="206" />
<Point x="1227" y="207" />
<Point x="1227" y="247" />
<AutomaticDrawing data="true" />
@@ -272,8 +272,8 @@
<cdparam x="877" y="343" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector from TGComponent to TGComponent" value="Connector between ports" />
-<P1 x="1167" y="444" id="208" />
-<P2 x="1232" y="431" id="150" />
+<P1 x="1178" y="454" id="208" />
+<P2 x="1222" y="441" id="150" />
<AutomaticDrawing data="true" />
<new d="false" />
</CONNECTOR>
diff --git a/modeling/SysMLSec/AliceAndBob.xml b/modeling/SysMLSec/AliceAndBob.xml
index c06f7d2abb33ced98e910a1c3bd8ed8a0ae15770..3ae154ef2106bab84dbfaa5f3d4f79f83305c902 100644
--- a/modeling/SysMLSec/AliceAndBob.xml
+++ b/modeling/SysMLSec/AliceAndBob.xml
@@ -177,13 +177,13 @@
<Signal value="out chout(Message msg)" attached="true" />
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="5000" id="82" index="7" uid="a1c44cc9-9334-4d03-8988-e402248c1447" >
+<SUBCOMPONENT type="5000" id="82" index="7" uid="32384080-e86a-41de-b441-4f6ae88f1cbe" >
<father id="164" num="0" />
-<cdparam x="263" y="233" />
-<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="36" y="233" />
+<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" />
-<infoparam name="Block0" value="Bob" />
+<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" />
+<infoparam name="Block0" value="Alice" />
<new d="false" />
<TGConnectingPoint num="0" id="42" />
<TGConnectingPoint num="1" id="43" />
@@ -228,10 +228,10 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
+<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" />
<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" />
+<Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" />
<Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" />
-<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" />
<Method value="Message encrypt(Message msg, Key k)" />
<Method value="Message decrypt(Message msg, Key k)" />
<Method value="Message sencrypt(Message msg, Key k)" />
@@ -254,15 +254,17 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
-<SUBCOMPONENT type="5000" id="123" index="8" uid="32384080-e86a-41de-b441-4f6ae88f1cbe" >
+<SUBCOMPONENT type="5000" id="123" index="8" uid="a1c44cc9-9334-4d03-8988-e402248c1447" >
<father id="164" num="1" />
-<cdparam x="36" y="233" />
-<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="263" y="233" />
+<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" />
-<infoparam name="Block0" value="Alice" />
+<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" />
+<infoparam name="Block0" value="Bob" />
<new d="false" />
<TGConnectingPoint num="0" id="83" />
<TGConnectingPoint num="1" id="84" />
@@ -307,10 +309,10 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
-<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" />
<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" />
+<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" />
<Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" />
+<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" />
<Method value="Message encrypt(Message msg, Key k)" />
<Method value="Message decrypt(Message msg, Key k)" />
<Method value="Message sencrypt(Message msg, Key k)" />
@@ -333,6 +335,8 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
@@ -1555,13 +1559,13 @@
<Signal value="out chout(Message msg)" attached="true" />
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="5000" id="857" index="7" uid="e802e723-57b4-4734-af20-cddadacc10e6" >
+<SUBCOMPONENT type="5000" id="857" index="7" uid="cc150a1e-1348-4fa4-98a9-3a612b6184cc" >
<father id="939" num="0" />
-<cdparam x="36" y="233" />
-<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="263" y="233" />
+<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" />
-<infoparam name="Block0" value="Alice" />
+<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" />
+<infoparam name="Block0" value="Bob" />
<new d="false" />
<TGConnectingPoint num="0" id="817" />
<TGConnectingPoint num="1" id="818" />
@@ -1606,13 +1610,13 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
-<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" />
<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" />
+<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" />
<Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" />
-<Attribute access="0" var="0" id="pubK" value="" type="5" typeOther="Key" />
+<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" />
<Attribute access="0" var="0" id="privK" value="" type="5" typeOther="Key" />
-<Attribute access="0" var="0" id="bobPubK" value="" type="5" typeOther="Key" />
+<Attribute access="0" var="0" id="pubK" value="" type="5" typeOther="Key" />
+<Attribute access="0" var="0" id="alicePubK" value="" type="5" typeOther="Key" />
<Method value="Message encrypt(Message msg, Key k)" />
<Method value="Message decrypt(Message msg, Key k)" />
<Method value="Message sencrypt(Message msg, Key k)" />
@@ -1635,15 +1639,17 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
-<SUBCOMPONENT type="5000" id="898" index="8" uid="cc150a1e-1348-4fa4-98a9-3a612b6184cc" >
+<SUBCOMPONENT type="5000" id="898" index="8" uid="e802e723-57b4-4734-af20-cddadacc10e6" >
<father id="939" num="1" />
-<cdparam x="263" y="233" />
-<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="36" y="233" />
+<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" />
-<infoparam name="Block0" value="Bob" />
+<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" />
+<infoparam name="Block0" value="Alice" />
<new d="false" />
<TGConnectingPoint num="0" id="858" />
<TGConnectingPoint num="1" id="859" />
@@ -1688,13 +1694,13 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
+<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" />
<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" />
+<Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" />
<Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" />
-<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" />
-<Attribute access="0" var="0" id="privK" value="" type="5" typeOther="Key" />
<Attribute access="0" var="0" id="pubK" value="" type="5" typeOther="Key" />
-<Attribute access="0" var="0" id="alicePubK" value="" type="5" typeOther="Key" />
+<Attribute access="0" var="0" id="privK" value="" type="5" typeOther="Key" />
+<Attribute access="0" var="0" id="bobPubK" value="" type="5" typeOther="Key" />
<Method value="Message encrypt(Message msg, Key k)" />
<Method value="Message decrypt(Message msg, Key k)" />
<Method value="Message sencrypt(Message msg, Key k)" />
@@ -1717,6 +1723,8 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
@@ -3653,13 +3661,13 @@
<Signal value="out chout(Message msg)" attached="true" />
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="5000" id="2024" index="7" uid="f24348ab-6d4a-40e6-a942-342d6222b23f" >
+<SUBCOMPONENT type="5000" id="2024" index="7" uid="7a040a26-feb9-4e9a-a609-908679df2a0b" >
<father id="2147" num="0" />
-<cdparam x="263" y="108" />
-<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="115" y="249" />
+<sizeparam width="261" height="83" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="299" minY="0" maxY="218" />
-<infoparam name="Block0" value="Bob" />
+<cdrectangleparam minX="0" maxX="177" minY="0" maxY="261" />
+<infoparam name="Block0" value="CA" />
<new d="false" />
<TGConnectingPoint num="0" id="1984" />
<TGConnectingPoint num="1" id="1985" />
@@ -3704,30 +3712,18 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
-<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" />
-<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" />
<Attribute access="0" var="0" id="privK" value="" type="5" typeOther="Key" />
<Attribute access="0" var="0" id="pubK" value="" type="5" typeOther="Key" />
<Attribute access="0" var="0" id="alicePubK" value="" type="5" typeOther="Key" />
-<Attribute access="0" var="0" id="CAPubK" value="" type="5" typeOther="Key" />
+<Attribute access="0" var="0" id="bobPubK" value="" type="5" typeOther="Key" />
<Attribute access="0" var="0" id="aliceID" value="" type="8" typeOther="" />
+<Attribute access="0" var="0" id="bobID" value="" type="8" typeOther="" />
+<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" />
+<Attribute access="0" var="0" id="newK" value="" type="5" typeOther="Key" />
+<Attribute access="0" var="0" id="newCert" value="" type="5" typeOther="Message" />
<Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="sig" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="certOK" value="" type="4" typeOther="" />
-<Method value="Message encrypt(Message msg, Key k)" />
-<Method value="Message decrypt(Message msg, Key k)" />
-<Method value="Message sencrypt(Message msg, Key k)" />
-<Method value="Message sdecrypt(Message msg, Key k)" />
-<Method value="Message MAC(Message msg, Key k)" />
-<Method value="bool verifyMAC(Message msg, Key k, Message macmsg)" />
-<Method value="Message concat2(Message msg1, Message msg2)" />
-<Method value="Message concat3(Message msg1, Message msg2, Message msg3)" />
-<Method value="Message concat4(Message msg1, Message msg2, Message msg3, Message msg4)" />
-<Method value="get2(Message msg, Message msg1, Message msg2)" />
-<Method value="get3(Message msg, Message msg1, Message msg2, Message msg3)" />
-<Method value="get4(Message msg, Message msg1, Message msg2, Message msg3, Message msg4)" />
+<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" />
+<Attribute access="0" var="0" id="newID" value="" type="8" typeOther="" />
<Method value="Message aencrypt(Message msg, Key k)" />
<Method value="Message adecrypt(Message msg, Key k)" />
<Method value="Key pk(Key k)" />
@@ -3736,8 +3732,20 @@
<Method value="Message cert(Key k, Message msg)" />
<Method value="bool verifyCert(Message cert, Key k)" />
<Method value="Key getpk(Message cert)" />
+<Method value="Message sencrypt(Message msg, Key k)" />
+<Method value="Message sdecrypt(Message msg, Key k)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message MAC(Message msg, Key k)" />
+<Method value="bool verifyMAC(Message msg, Key k, Message macmsg)" />
+<Method value="Message concat2(Message msg1, Message msg2)" />
+<Method value="Message concat3(Message msg1, Message msg2, Message msg3)" />
+<Method value="Message concat4(Message msg1, Message msg2, Message msg3, Message msg4)" />
+<Method value="get2(Message msg, Message msg1, Message msg2)" />
+<Method value="get3(Message msg, Message msg1, Message msg2, Message msg3)" />
+<Method value="get4(Message msg, Message msg1, Message msg2, Message msg3, Message msg4)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="5000" id="2065" index="8" uid="52a07889-a0b4-45e9-a97a-a5a5e144d49b" >
@@ -3825,15 +3833,17 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
-<SUBCOMPONENT type="5000" id="2106" index="9" uid="7a040a26-feb9-4e9a-a609-908679df2a0b" >
+<SUBCOMPONENT type="5000" id="2106" index="9" uid="f24348ab-6d4a-40e6-a942-342d6222b23f" >
<father id="2147" num="2" />
-<cdparam x="115" y="249" />
-<sizeparam width="261" height="83" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="263" y="108" />
+<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="177" minY="0" maxY="261" />
-<infoparam name="Block0" value="CA" />
+<cdrectangleparam minX="0" maxX="299" minY="0" maxY="218" />
+<infoparam name="Block0" value="Bob" />
<new d="false" />
<TGConnectingPoint num="0" id="2066" />
<TGConnectingPoint num="1" id="2067" />
@@ -3878,30 +3888,22 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
+<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" />
+<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" />
+<Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" />
+<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" />
<Attribute access="0" var="0" id="privK" value="" type="5" typeOther="Key" />
<Attribute access="0" var="0" id="pubK" value="" type="5" typeOther="Key" />
<Attribute access="0" var="0" id="alicePubK" value="" type="5" typeOther="Key" />
-<Attribute access="0" var="0" id="bobPubK" value="" type="5" typeOther="Key" />
+<Attribute access="0" var="0" id="CAPubK" value="" type="5" typeOther="Key" />
<Attribute access="0" var="0" id="aliceID" value="" type="8" typeOther="" />
-<Attribute access="0" var="0" id="bobID" value="" type="8" typeOther="" />
-<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="newK" value="" type="5" typeOther="Key" />
-<Attribute access="0" var="0" id="newCert" value="" type="5" typeOther="Message" />
<Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="newID" value="" type="8" typeOther="" />
-<Method value="Message aencrypt(Message msg, Key k)" />
-<Method value="Message adecrypt(Message msg, Key k)" />
-<Method value="Key pk(Key k)" />
-<Method value="Message sign(Message msg, Key k)" />
-<Method value="bool verifySign(Message msg1, Message sig, Key k)" />
-<Method value="Message cert(Key k, Message msg)" />
-<Method value="bool verifyCert(Message cert, Key k)" />
-<Method value="Key getpk(Message cert)" />
+<Attribute access="0" var="0" id="sig" value="" type="5" typeOther="Message" />
+<Attribute access="0" var="0" id="certOK" value="" type="4" typeOther="" />
+<Method value="Message encrypt(Message msg, Key k)" />
+<Method value="Message decrypt(Message msg, Key k)" />
<Method value="Message sencrypt(Message msg, Key k)" />
<Method value="Message sdecrypt(Message msg, Key k)" />
-<Method value="Key DH(Key pubK, Key privK)" />
-<Method value="Message hash(Message msg)" />
<Method value="Message MAC(Message msg, Key k)" />
<Method value="bool verifyMAC(Message msg, Key k, Message macmsg)" />
<Method value="Message concat2(Message msg1, Message msg2)" />
@@ -3910,6 +3912,18 @@
<Method value="get2(Message msg, Message msg1, Message msg2)" />
<Method value="get3(Message msg, Message msg1, Message msg2, Message msg3)" />
<Method value="get4(Message msg, Message msg1, Message msg2, Message msg3, Message msg4)" />
+<Method value="Message aencrypt(Message msg, Key k)" />
+<Method value="Message adecrypt(Message msg, Key k)" />
+<Method value="Key pk(Key k)" />
+<Method value="Message sign(Message msg, Key k)" />
+<Method value="bool verifySign(Message msg1, Message sig, Key k)" />
+<Method value="Message cert(Key k, Message msg)" />
+<Method value="bool verifyCert(Message cert, Key k)" />
+<Method value="Key getpk(Message cert)" />
+<Method value="Key DH(Key pubK, Key privK)" />
+<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
@@ -6722,13 +6736,13 @@
<Signal value="out chout(Message msg)" attached="true" />
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="5000" id="3642" index="7" uid="7bb99390-2a74-452a-8601-e344bd028850" >
+<SUBCOMPONENT type="5000" id="3642" index="7" uid="58e32c17-1811-4588-ab32-863569a17a48" >
<father id="3724" num="0" />
-<cdparam x="263" y="233" />
-<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="36" y="233" />
+<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" />
-<infoparam name="Block0" value="Bob" />
+<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" />
+<infoparam name="Block0" value="Alice" />
<new d="false" />
<TGConnectingPoint num="0" id="3602" />
<TGConnectingPoint num="1" id="3603" />
@@ -6773,8 +6787,8 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
+<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" />
<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" />
<Method value="Message encrypt(Message msg, Key k)" />
<Method value="Message decrypt(Message msg, Key k)" />
<Method value="Message sencrypt(Message msg, Key k)" />
@@ -6797,15 +6811,17 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
-<SUBCOMPONENT type="5000" id="3683" index="8" uid="58e32c17-1811-4588-ab32-863569a17a48" >
+<SUBCOMPONENT type="5000" id="3683" index="8" uid="7bb99390-2a74-452a-8601-e344bd028850" >
<father id="3724" num="1" />
-<cdparam x="36" y="233" />
-<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="263" y="233" />
+<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" />
-<infoparam name="Block0" value="Alice" />
+<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" />
+<infoparam name="Block0" value="Bob" />
<new d="false" />
<TGConnectingPoint num="0" id="3643" />
<TGConnectingPoint num="1" id="3644" />
@@ -6850,8 +6866,8 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
-<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" />
<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" />
+<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" />
<Method value="Message encrypt(Message msg, Key k)" />
<Method value="Message decrypt(Message msg, Key k)" />
<Method value="Message sencrypt(Message msg, Key k)" />
@@ -6874,6 +6890,8 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
diff --git a/src/main/java/ai/AIBlockConnAttribWithSlicing.java b/src/main/java/ai/AIBlockConnAttribWithSlicing.java
index 66f6ee9ca2c28d9b516e0e44649b1bafa4318cf2..6fb8d4ff126edb9e45eb18aacfeee233db8c77c6 100644
--- a/src/main/java/ai/AIBlockConnAttribWithSlicing.java
+++ b/src/main/java/ai/AIBlockConnAttribWithSlicing.java
@@ -100,7 +100,7 @@ public class AIBlockConnAttribWithSlicing extends AIInteract {
"typical system blocks and their connections. Do respect the JSON format, and provide only JSON (no explanation before or after).\n",
"From the previous JSON and system specification, find the typical attributes of all blocks by imagining all the necessary attributes " +
- "that would be needed for the state machine diagram of each block. "};
+ "that would be needed for the state machine diagram of each block. Do give them respecting the specified JSON format"};
public String namesOfBlocks = "";
diff --git a/src/main/java/avatartranslator/AvatarMethod.java b/src/main/java/avatartranslator/AvatarMethod.java
index b1900492db4e649f95c07974706cab873c7f93f7..fa39ff3239bf1111c17fef97ac146f5f82f604cf 100644
--- a/src/main/java/avatartranslator/AvatarMethod.java
+++ b/src/main/java/avatartranslator/AvatarMethod.java
@@ -67,6 +67,8 @@ public class AvatarMethod extends AvatarElement implements NameChecker.NameStart
"Message hash(Message msg)",
"Message MAC(Message msg, Key k)",
"bool verifyMAC(Message msg, Key k, Message macmsg)",
+ "Message host(Key k)",
+ "Key getKey(Message msg)",
"Message concat2(Message msg1, Message msg2)",
"Message concat3(Message msg1, Message msg2, Message msg3)",
"Message concat4(Message msg1, Message msg2, Message msg3, Message msg4)",
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index 1bbc818291a8a5f74770a3246931febdb9f8ec0c..74272690f6efbc4f3048a36b92035d0986bfcd67 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -758,6 +758,7 @@ public class AvatarSpecification extends AvatarElement implements IBSParamSpec {
// We remove all non-connected blocks if at least two blocks have a relation
public void removeNonConnectedBlocks() {
+ TraceManager.addDev("Removing non connected blocks");
boolean found = false;
for (AvatarRelation ar : relations) {
if (ar.getBlock1() != ar.getBlock2()) {
@@ -779,7 +780,12 @@ public class AvatarSpecification extends AvatarElement implements IBSParamSpec {
toBeRemovedNotConnected.add(ab);
}
}
- getListOfBlocks().removeAll(toBeRemovedNotConnected);
+
+ if (toBeRemovedNotConnected.size() > 0) {
+ TraceManager.addDev("Found blocks to be removed: " + toBeRemovedNotConnected.size() + " blocks");
+ getListOfBlocks().removeAll(toBeRemovedNotConnected);
+ }
+
}
}
diff --git a/src/main/java/avatartranslator/directsimulation/AvatarSimulationBlock.java b/src/main/java/avatartranslator/directsimulation/AvatarSimulationBlock.java
index 33837dc20af708f080e465b7809541f847b025c2..7ca59e470aece2ddd4b5c445994cfc5f346f0d2a 100644
--- a/src/main/java/avatartranslator/directsimulation/AvatarSimulationBlock.java
+++ b/src/main/java/avatartranslator/directsimulation/AvatarSimulationBlock.java
@@ -41,6 +41,7 @@ package avatartranslator.directsimulation;
import avatartranslator.*;
import avatartranslator.intboolsolver.AvatarIBSExpressions;
+import avatartranslator.intboolsolver.AvatarIBSStdParser;
import avatartranslator.intboolsolver.AvatarIBSolver;
import avatartranslator.modelchecker.SpecificationBlock;
import myutil.*;
diff --git a/src/main/java/avatartranslator/directsimulation/AvatarSpecificationSimulation.java b/src/main/java/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
index a773f591eefd20a3cf12f7dde27db53a414a09ac..04c1f8486d184e3f4fba54924a24195a776045a1 100644
--- a/src/main/java/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
+++ b/src/main/java/avatartranslator/directsimulation/AvatarSpecificationSimulation.java
@@ -40,6 +40,7 @@
package avatartranslator.directsimulation;
import avatartranslator.*;
+import avatartranslator.intboolsolver.AvatarIBSolver;
import myutil.CSVObject;
import myutil.TraceManager;
@@ -178,6 +179,9 @@ public class AvatarSpecificationSimulation {
// Robustness
avspec.makeRobustness();
+ // Reset parser
+ AvatarIBSolver.clearAttributes();
+
// remove FIFOs
//avspec.removeFIFOs(2);
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 7e95f090c8f507e2881cf3ae70aa2d085918b858..a06dfd34c8ab9a70f16b2f30dd4d6dc0154aca31 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -41,6 +41,7 @@ package avatartranslator.modelchecker;
import avatartranslator.*;
import avatartranslator.intboolsolver.AvatarIBSExpressions;
+import avatartranslator.intboolsolver.AvatarIBSolver;
import myutil.BoolExpressionEvaluator;
import myutil.Conversion;
import myutil.IntExpressionEvaluator;
@@ -926,6 +927,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
spec.setAttributeOptRatio(compressionFactor);
spec.generateAllExpressionSolvers();
+ // Reset parser
+ AvatarIBSolver.clearAttributes();
+
prepareTransitions();
prepareBlocks();
diff --git a/src/main/java/avatartranslator/toexecutable/AVATAR2CPOSIX.java b/src/main/java/avatartranslator/toexecutable/AVATAR2CPOSIX.java
index e0f1f8c279c7bd8f92bf241ac4855163118bc5c9..fb256804e38d6b30c4fb02d2df26b6c821e67673 100755
--- a/src/main/java/avatartranslator/toexecutable/AVATAR2CPOSIX.java
+++ b/src/main/java/avatartranslator/toexecutable/AVATAR2CPOSIX.java
@@ -44,6 +44,7 @@ import java.util.List;
import java.util.Vector;
import avatartranslator.*;
+import avatartranslator.intboolsolver.AvatarIBSolver;
import common.SpecConfigTTool;
import myutil.Conversion;
import myutil.FileException;
@@ -162,6 +163,9 @@ public class AVATAR2CPOSIX {
avspec.removeLibraryFunctionCalls();
avspec.removeTimers();
+ // Reset parser
+ AvatarIBSolver.clearAttributes();
+
//TraceManager.addDev("AVATAR2CPOSIX avspec=" + avspec);
diff --git a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
index 37d4306e57fbb3823751a85d77825b0d3e157df8..0e6d5bba0815b6847829e4ea1cc487b7a8de4da4 100755
--- a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -39,6 +39,7 @@
package avatartranslator.toproverif;
import avatartranslator.*;
+import avatartranslator.intboolsolver.AvatarIBSolver;
import common.ConfigurationTTool;
import myutil.FileException;
import myutil.FileUtils;
@@ -72,6 +73,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
private final static String TRUE = "TRUE";
private final static String FALSE = "FALSE";
private final static String PK_PK = "pk";
+ private final static String HOST = "host";
+ private final static String GETKEY = "getKey";
private final static String PK_ENCRYPT = "aencrypt";
private final static String PK_DECRYPT = "adecrypt";
private final static String PK_SIGN = "sign";
@@ -448,6 +451,9 @@ public class AVATAR2ProVerif implements AvatarTranslator {
this.avspec.removeTimers();
+ // Reset parser
+ AvatarIBSolver.clearAttributes();
+
this.dummyDataCounter = 0;
List<AvatarAttribute> allKnowledge = this.makeStartingProcess();
@@ -513,6 +519,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
this.spec.addDeclaration(new ProVerifComment("HASH"));
this.spec.addDeclaration(new ProVerifFunc(HASH_HASH, new String[]{"bitstring"}, "bitstring"));
+ this.spec.addDeclaration(new ProVerifComment("Key and host"));
+ this.spec.addDeclaration(new ProVerifFunc(HOST, new String[]{"bitstring"}, "bitstring"));
+ this.spec.addDeclaration(new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("x", "bitstring")}, GETKEY + " (" + HOST + " (x)) = " +
+ "x"));
+
+
this.spec.addDeclaration(new ProVerifComment("Channel"));
this.spec.addDeclaration(new ProVerifVar(CH_MAINCH, "channel"));
// TODO: add one encryption function per signal
diff --git a/src/main/java/avatartranslator/tosysmlv2/AVATAR2SysMLV2.java b/src/main/java/avatartranslator/tosysmlv2/AVATAR2SysMLV2.java
index 22f948363f58f7acb9d7e005ccaf8e8b68601979..1e5e6b0b997d9445a26d685460a5e9828d92292b 100644
--- a/src/main/java/avatartranslator/tosysmlv2/AVATAR2SysMLV2.java
+++ b/src/main/java/avatartranslator/tosysmlv2/AVATAR2SysMLV2.java
@@ -47,6 +47,7 @@ import java.util.Scanner;
import java.util.Vector;
import avatartranslator.*;
+import avatartranslator.intboolsolver.AvatarIBSolver;
import common.SpecConfigTTool;
import myutil.Conversion;
import myutil.FileException;
@@ -165,6 +166,8 @@ public class AVATAR2SysMLV2 {
avspec.removeCompositeStates();
avspec.removeLibraryFunctionCalls();
avspec.removeTimers();
+ // Reset parser
+ AvatarIBSolver.clearAttributes();
//TraceManager.addDev("AVATAR2CPOSIX avspec=" + avspec);
diff --git a/src/main/java/avatartranslator/totpn/AVATAR2TPN.java b/src/main/java/avatartranslator/totpn/AVATAR2TPN.java
index a7574f70e6ddb169c524f216bf3630860ca17459..d3a26b67b8d1eee4b0237266887fa8ab211e3f84 100755
--- a/src/main/java/avatartranslator/totpn/AVATAR2TPN.java
+++ b/src/main/java/avatartranslator/totpn/AVATAR2TPN.java
@@ -42,6 +42,7 @@
package avatartranslator.totpn;
import avatartranslator.*;
+import avatartranslator.intboolsolver.AvatarIBSolver;
import myutil.TraceManager;
import tpndescription.Place;
import tpndescription.TPN;
@@ -104,6 +105,9 @@ public class AVATAR2TPN {
avspec.removeLibraryFunctionCalls ();
avspec.removeTimers();
+ // Reset parser
+ AvatarIBSolver.clearAttributes();
+
makeBlocks();
//TraceManager.addDev("-> tpn:" + tpn.toString());
diff --git a/src/main/java/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/main/java/avatartranslator/touppaal/AVATAR2UPPAAL.java
index 55dab417efc195c5e99f6b20ed93cd7bed95849a..7a76a72de034a152c5c41839ccb689a0329cf802 100755
--- a/src/main/java/avatartranslator/touppaal/AVATAR2UPPAAL.java
+++ b/src/main/java/avatartranslator/touppaal/AVATAR2UPPAAL.java
@@ -39,6 +39,7 @@
package avatartranslator.touppaal;
import avatartranslator.*;
+import avatartranslator.intboolsolver.AvatarIBSolver;
import common.SpecConfigTTool;
import myutil.Conversion;
import myutil.FileException;
@@ -164,6 +165,9 @@ public class AVATAR2UPPAAL {
avspec.removeTimers();
//avspec.removeElseGuards();
+ // Reset parser
+ AvatarIBSolver.clearAttributes();
+
//avspec.removeFIFOs(2);
avspec.makeRobustness();
diff --git a/src/main/java/tmltranslator/dsez3engine/InputInstance.java b/src/main/java/tmltranslator/dsez3engine/InputInstance.java
index 1317ba4a102bff431a4bca9afc1a2b66c8aee616..fc7387a546e2a53da7a6944c4a1ac83113b21a63 100644
--- a/src/main/java/tmltranslator/dsez3engine/InputInstance.java
+++ b/src/main/java/tmltranslator/dsez3engine/InputInstance.java
@@ -31,9 +31,13 @@ public class InputInstance {
for (HwNode hwNode : architecture.getHwNodes()) {
if (hwNode instanceof HwExecutionNode) {
- if ((((HwExecutionNode) hwNode).supportOperation(tmlTask.getOperation()) ) || (((HwExecutionNode) hwNode).getOperation().equals(" ")))
- feasibleCPUs.add((HwExecutionNode) hwNode);
-
+ if (tmlTask == null) {
+ if( (((HwExecutionNode) hwNode).getOperation().equals(" ")))
+ feasibleCPUs.add( (HwExecutionNode) hwNode);
+ } else {
+ if ((((HwExecutionNode) hwNode).supportOperation(tmlTask.getOperation())) || (((HwExecutionNode) hwNode).getOperation().equals(" ")))
+ feasibleCPUs.add((HwExecutionNode) hwNode);
+ }
}
}
diff --git a/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java b/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
index e1a0c27fb00f4a2b11f8c59363a5f44f36ede651..a2c86d5d7cc510047d3a44ac548f79e301acaf57 100644
--- a/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
+++ b/src/main/java/tmltranslator/dsez3engine/OptimizationModel.java
@@ -800,7 +800,7 @@ public class OptimizationModel {
//Creating an expression for latency
- //Calculating end time of last task
+ // Calculating end time of last task
TMLTask finalTask = inputInstance.getFinalTask(inputInstance.getModeling());
int finalTaskIndex = inputInstance.getModeling().getTasks().indexOf(inputInstance.getFinalTask(inputInstance.getModeling()));
ArithExpr wcet_last = ctx.mkInt(0);
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index f214577bd0c1ee1dd938aae998b80bf8625d7554..5e52a0a94bf4cc62fcb907557cb3be10d57eb39d 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -2865,7 +2865,8 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
*/
}
- JDialogLoadingNetworkModel jdlnm = new JDialogLoadingNetworkModel(frame, this, "Opening a network model", ConfigurationTTool.URL_MODEL);
+ JDialogLoadingNetworkModel jdlnm = new JDialogLoadingNetworkModel(frame, this,
+ "Opening a model from TTool's repository", ConfigurationTTool.URL_MODEL);
GraphicLib.centerOnParent(jdlnm, 700, 800);
jdlnm.setVisible(true); // blocked until dialog has been closed
}
diff --git a/src/main/java/ui/networkmodelloader/JDialogLoadingNetworkModel.java b/src/main/java/ui/networkmodelloader/JDialogLoadingNetworkModel.java
index 002b028ebffe647557df7183275e14574e06e757..62c5687cbf1ce1a953c1b8315970f6b3ec248490 100644
--- a/src/main/java/ui/networkmodelloader/JDialogLoadingNetworkModel.java
+++ b/src/main/java/ui/networkmodelloader/JDialogLoadingNetworkModel.java
@@ -68,7 +68,8 @@ import java.util.ArrayList;;
*/
public class JDialogLoadingNetworkModel extends javax.swing.JFrame implements ActionListener, Runnable, LoaderFacilityInterface, CallbackLoaderInterface {
- public final static String[] FEATURES = {"all", "diplodocus", "avatar", "sysml-sec", "assumptions", "requirements", "attacktrees", "properties", "partitioning", "analysis", "design", "prototyping", "securityprotocol", "codegeneration"};
+ public final static String[] FEATURES = {"all", "diplodocus", "avatar", "sysml-sec", "assumptions", "requirements", "attacktrees", "properties",
+ "partitioning", "analysis", "design", "prototyping", "securityprotocol", "codegeneration"};
public final static String[] PROPS = {"safety", "security", "performance"};
@@ -270,13 +271,13 @@ public class JDialogLoadingNetworkModel extends javax.swing.JFrame implements Ac
String inputLine = null;
NetworkModel nm = null;
while ((inputLine = in.readLine()) != null) {
- if (inputLine.startsWith("#FILE")) {
+ if (inputLine.toUpperCase().startsWith("#FILE")) {
//TraceManager.addDev("Loading network model: " + inputLine.substring(5).trim());
nm = new NetworkModel(inputLine.substring(5).trim());
listOfModels.add(nm);
}
- if (inputLine.startsWith("-FEATURES")) {
+ if (inputLine.toUpperCase().startsWith("-FEATURES")) {
if (nm != null) {
String tmp = inputLine.substring(9, inputLine.length()).trim().toLowerCase();
for (int i = 1; i < FEATURES.length; i++) {
@@ -286,7 +287,7 @@ public class JDialogLoadingNetworkModel extends javax.swing.JFrame implements Ac
}
}
- if (inputLine.startsWith("-PROPS")) {
+ if (inputLine.toUpperCase().startsWith("-PROPS")) {
if (nm != null) {
String tmp = inputLine.substring(6, inputLine.length()).trim().toLowerCase();
for (int i = 0; i < PROPS.length; i++) {
@@ -296,20 +297,20 @@ public class JDialogLoadingNetworkModel extends javax.swing.JFrame implements Ac
}
}
- if (inputLine.startsWith("-AUTHOR")) {
+ if (inputLine.toUpperCase().startsWith("-AUTHOR")) {
if (nm != null) {
nm.author = inputLine.substring(7, inputLine.length()).trim();
}
}
- if (inputLine.startsWith("-DESCRIPTION")) {
+ if (inputLine.toUpperCase().startsWith("-DESCRIPTION")) {
if (nm != null) {
nm.description = inputLine.substring(12, inputLine.length()).trim();
}
}
- if (inputLine.startsWith("-IMG")) {
+ if (inputLine.toUpperCase().startsWith("-IMG")) {
if (nm != null) {
nm.image = inputLine.substring(4, inputLine.length()).trim();
//TraceManager.addDev("Dealing with image:" + nm.image);
diff --git a/src/main/java/ui/util/DefaultText.java b/src/main/java/ui/util/DefaultText.java
index 6aaed3fddbc0eebeeaec3dff068e53cdace01de6..05b5d83af913f82cf8adf57806409a14b5df7fe3 100755
--- a/src/main/java/ui/util/DefaultText.java
+++ b/src/main/java/ui/util/DefaultText.java
@@ -50,8 +50,8 @@ package ui.util;
*/
public class DefaultText {
- public static String BUILD = "14563";
- public static String DATE = "2023/10/02 03:21:02 CET";
+ public static String BUILD = "14606";
+ public static String DATE = "2023/11/13 03:21:06 CET";
public static StringBuffer sbAbout = makeAbout();
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 0b186642020c26baaffe9858202e3654e7bb3437..a38e02aadd96e2567db00a30661535ad9b1c8ab4 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -146,6 +146,8 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
private static boolean DRAW_AVATAR = false;
+ private JLabel labelError;
+
protected MainGUI mgui;
private AvatarDesignPanel adp;
@@ -1489,6 +1491,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
}
CODE_PATH = code1.getText();
EXECUTE_PATH = exe2.getText();
+
if (stateReachabilityAll.isSelected()) {
REACHABILITY_OPTION = REACHABILITY_ALL;
} else if (stateReachabilitySelected.isSelected()) {
@@ -1921,7 +1924,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
this.results = this.pvoa.getResults();
if (this.results.keySet().size() == 0) {
- label = new JLabel("ERROR: no properties to prove");
+ label = new JLabel("ERROR: no properties to be proved");
label.setAlignmentX(Component.LEFT_ALIGNMENT);
this.jta.add(label, this.createGbc(0));
}