diff --git a/modeling/SoCLib/rover.xml b/modeling/SoCLib/rover.xml
index 4d51755958da4125fc0fd8882f1a555db3e0b101..2cf44e5dcd16ba7a5e37dfe3356d2b9cb1d9b7d4 100644
--- a/modeling/SoCLib/rover.xml
+++ b/modeling/SoCLib/rover.xml
@@ -8,40 +8,40 @@
<cdparam x="480" y="262" />
<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="480" y="262" id="66" />
-<P2 x="479" y="296" id="26" />
+<P1 x="480" y="262" id="52" />
+<P2 x="479" y="296" id="22" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="126" id="2" >
<cdparam x="601" y="181" />
<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="685" y="179" id="52" />
-<P2 x="804" y="179" id="9" />
+<P1 x="685" y="179" id="66" />
+<P2 x="804" y="179" id="11" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="126" id="3" >
<cdparam x="601" y="205" />
<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="685" y="230" id="62" />
-<P2 x="804" y="230" id="11" />
+<P1 x="685" y="230" id="56" />
+<P2 x="804" y="230" id="9" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="126" id="4" >
<cdparam x="375" y="154" />
<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="375" y="164" id="54" />
-<P2 x="270" y="164" id="37" />
+<P1 x="375" y="164" id="64" />
+<P2 x="270" y="164" id="41" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="126" id="5" >
<cdparam x="445" y="153" />
<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="375" y="193" id="56" />
-<P2 x="270" y="195" id="41" />
+<P1 x="375" y="193" id="62" />
+<P2 x="270" y="195" id="37" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="126" id="6" >
@@ -49,7 +49,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="270" y="225" id="39" />
-<P2 x="375" y="225" id="64" />
+<P2 x="375" y="225" id="54" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="126" id="7" >
@@ -57,15 +57,15 @@
<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="418" y="296" id="24" />
-<P2 x="418" y="262" id="58" />
+<P2 x="418" y="262" id="60" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="126" id="8" >
<cdparam x="547" y="288" />
<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="549" y="262" id="60" />
-<P2 x="548" y="296" id="22" />
+<P1 x="549" y="262" id="58" />
+<P2 x="548" y="296" id="26" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<COMPONENT type="1202" id="21" >
@@ -90,14 +90,14 @@
</COMPONENT>
<SUBCOMPONENT type="1203" id="10" >
<father id="21" num="0" />
-<cdparam x="804" y="166" />
+<cdparam x="804" y="217" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="229" minY="-13" maxY="117" />
-<infoparam name="Primitive port" value="Event newCommand" />
+<infoparam name="Primitive port" value="Channel motorCommand" />
<TGConnectingPoint num="0" id="9" />
<extraparam>
-<Prop commName="newCommand" commType="1" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="motorCommand" commType="0" origin="false" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -107,14 +107,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="12" >
<father id="21" num="1" />
-<cdparam x="804" y="217" />
+<cdparam x="804" y="166" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="229" minY="-13" maxY="117" />
-<infoparam name="Primitive port" value="Channel motorCommand" />
+<infoparam name="Primitive port" value="Event newCommand" />
<TGConnectingPoint num="0" id="11" />
<extraparam>
-<Prop commName="motorCommand" commType="0" origin="false" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="newCommand" commType="1" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -125,7 +125,7 @@
<COMPONENT type="1202" id="36" >
<cdparam x="381" y="309" />
-<sizeparam width="291" height="98" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="291" height="97" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
<infoparam name="Primitive component" value="TemperatureSensor" />
@@ -141,18 +141,20 @@
<Data isAttacker="No" />
<Attribute access="2" id="samplingRate" value="" type="0" typeOther="" />
<Attribute access="2" id="sensorOn" value="" type="4" typeOther="" />
+<Attribute access="2" id="i" value="" type="0" typeOther="" />
+<Attribute access="2" id="change" value="" type="4" typeOther="" />
</extraparam>
</COMPONENT>
<SUBCOMPONENT type="1203" id="23" >
<father id="36" num="0" />
-<cdparam x="535" y="296" />
+<cdparam x="466" y="296" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="-13" maxX="278" minY="-13" maxY="85" />
-<infoparam name="Primitive port" value="Event startTemp" />
+<cdrectangleparam minX="-13" maxX="278" minY="-13" maxY="84" />
+<infoparam name="Primitive port" value="Event stopTemp" />
<TGConnectingPoint num="0" id="22" />
<extraparam>
-<Prop commName="startTemp" commType="1" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="stopTemp" commType="1" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -165,7 +167,7 @@
<cdparam x="405" y="296" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="-13" maxX="278" minY="-13" maxY="85" />
+<cdrectangleparam minX="-13" maxX="278" minY="-13" maxY="84" />
<infoparam name="Primitive port" value="Channel tempData" />
<TGConnectingPoint num="0" id="24" />
<extraparam>
@@ -179,14 +181,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="27" >
<father id="36" num="2" />
-<cdparam x="466" y="296" />
+<cdparam x="535" y="296" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="-13" maxX="278" minY="-13" maxY="85" />
-<infoparam name="Primitive port" value="Event stopTemp" />
+<cdrectangleparam minX="-13" maxX="278" minY="-13" maxY="84" />
+<infoparam name="Primitive port" value="Event startTemp" />
<TGConnectingPoint num="0" id="26" />
<extraparam>
-<Prop commName="stopTemp" commType="1" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="startTemp" commType="1" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -212,18 +214,19 @@
<extraparam>
<Data isAttacker="No" />
<Attribute access="2" id="samplingRate" value="" type="0" typeOther="" />
+<Attribute access="2" id="change" value="" type="4" typeOther="" />
</extraparam>
</COMPONENT>
<SUBCOMPONENT type="1203" id="38" >
<father id="51" num="0" />
-<cdparam x="244" y="151" />
+<cdparam x="244" y="182" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="187" minY="-13" maxY="109" />
-<infoparam name="Primitive port" value="Event changeRate" />
+<infoparam name="Primitive port" value="Channel samplingRate" />
<TGConnectingPoint num="0" id="37" />
<extraparam>
-<Prop commName="changeRate" commType="1" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="samplingRate" commType="0" origin="false" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -250,14 +253,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="42" >
<father id="51" num="2" />
-<cdparam x="244" y="182" />
+<cdparam x="244" y="151" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="187" minY="-13" maxY="109" />
-<infoparam name="Primitive port" value="Channel samplingRate" />
+<infoparam name="Primitive port" value="Event changeRate" />
<TGConnectingPoint num="0" id="41" />
<extraparam>
-<Prop commName="samplingRate" commType="0" origin="false" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="changeRate" commType="1" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -289,14 +292,14 @@
</COMPONENT>
<SUBCOMPONENT type="1203" id="53" >
<father id="76" num="0" />
-<cdparam x="659" y="166" />
+<cdparam x="467" y="236" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="271" minY="-13" maxY="111" />
-<infoparam name="Primitive port" value="Event newCommand" />
+<infoparam name="Primitive port" value="Event stopTemp" />
<TGConnectingPoint num="0" id="52" />
<extraparam>
-<Prop commName="newCommand" commType="1" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="stopTemp" commType="1" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -306,14 +309,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="55" >
<father id="76" num="1" />
-<cdparam x="375" y="151" />
+<cdparam x="375" y="212" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="271" minY="-13" maxY="111" />
-<infoparam name="Primitive port" value="Event changeRate" />
+<infoparam name="Primitive port" value="Channel ultrasonicData" />
<TGConnectingPoint num="0" id="54" />
<extraparam>
-<Prop commName="changeRate" commType="1" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="ultrasonicData" commType="0" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -323,14 +326,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="57" >
<father id="76" num="2" />
-<cdparam x="375" y="180" />
+<cdparam x="659" y="217" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="271" minY="-13" maxY="111" />
-<infoparam name="Primitive port" value="Channel samplingRate" />
+<infoparam name="Primitive port" value="Channel motorCommand" />
<TGConnectingPoint num="0" id="56" />
<extraparam>
-<Prop commName="samplingRate" commType="0" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="motorCommand" commType="0" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -340,14 +343,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="59" >
<father id="76" num="3" />
-<cdparam x="405" y="236" />
+<cdparam x="536" y="236" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="271" minY="-13" maxY="111" />
-<infoparam name="Primitive port" value="Channel tempData" />
+<infoparam name="Primitive port" value="Event startTemp" />
<TGConnectingPoint num="0" id="58" />
<extraparam>
-<Prop commName="tempData" commType="0" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="startTemp" commType="1" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -357,14 +360,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="61" >
<father id="76" num="4" />
-<cdparam x="536" y="236" />
+<cdparam x="405" y="236" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="271" minY="-13" maxY="111" />
-<infoparam name="Primitive port" value="Event startTemp" />
+<infoparam name="Primitive port" value="Channel tempData" />
<TGConnectingPoint num="0" id="60" />
<extraparam>
-<Prop commName="startTemp" commType="1" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="tempData" commType="0" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -374,14 +377,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="63" >
<father id="76" num="5" />
-<cdparam x="659" y="217" />
+<cdparam x="375" y="180" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="271" minY="-13" maxY="111" />
-<infoparam name="Primitive port" value="Channel motorCommand" />
+<infoparam name="Primitive port" value="Channel samplingRate" />
<TGConnectingPoint num="0" id="62" />
<extraparam>
-<Prop commName="motorCommand" commType="0" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="samplingRate" commType="0" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -391,14 +394,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="65" >
<father id="76" num="6" />
-<cdparam x="375" y="212" />
+<cdparam x="375" y="151" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="271" minY="-13" maxY="111" />
-<infoparam name="Primitive port" value="Channel ultrasonicData" />
+<infoparam name="Primitive port" value="Event changeRate" />
<TGConnectingPoint num="0" id="64" />
<extraparam>
-<Prop commName="ultrasonicData" commType="0" origin="false" finite="false" blocking="true" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="changeRate" commType="1" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -408,14 +411,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="67" >
<father id="76" num="7" />
-<cdparam x="467" y="236" />
+<cdparam x="659" y="166" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-13" maxX="271" minY="-13" maxY="111" />
-<infoparam name="Primitive port" value="Event stopTemp" />
+<infoparam name="Primitive port" value="Event newCommand" />
<TGConnectingPoint num="0" id="66" />
<extraparam>
-<Prop commName="stopTemp" commType="1" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
+<Prop commName="newCommand" commType="1" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" referenceReq="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -562,6 +565,66 @@
</TMLActivityDiagramPanel>
<TMLActivityDiagramPanel name="TemperatureSensor" minX="10" maxX="2500" minY="10" maxY="1500" >
+<CONNECTOR type="115" id="244875" >
+<cdparam x="537" y="485" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="537" y="485" id="244874" />
+<P2 x="537" y="509" id="119" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<COMPONENT type="1017" id="244872" >
+<cdparam x="462" y="460" />
+<sizeparam width="150" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="notified event" value="change=?stopTemp()" />
+<TGConnectingPoint num="0" id="244873" />
+<TGConnectingPoint num="1" id="244874" />
+<extraparam>
+<Data eventName="stopTemp" variable="change" />
+</extraparam>
+</COMPONENT>
+
+<CONNECTOR type="115" id="244871" >
+<cdparam x="386" y="162" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="409" y="210" id="122544" />
+<P2 x="409" y="245" id="122426" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<COMPONENT type="1001" id="122430" >
+<cdparam x="401" y="300" />
+<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="stop state" value="null" />
+<TGConnectingPoint num="0" id="122431" />
+</COMPONENT>
+
+<CONNECTOR type="115" id="122429" >
+<cdparam x="493" y="264" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="493" y="264" id="122427" />
+<P2 x="539" y="345" id="128" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<COMPONENT type="1014" id="122425" >
+<cdparam x="325" y="250" />
+<sizeparam width="168" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="for loop" value="for(i=0;sensorOn;i = i+1)" />
+<TGConnectingPoint num="0" id="122426" />
+<TGConnectingPoint num="1" id="122427" />
+<TGConnectingPoint num="2" id="122428" />
+<extraparam>
+<Data init="i=0" condition="sensorOn" increment="i = i+1" />
+</extraparam>
+</COMPONENT>
+
<COMPONENT type="1030" id="105" >
<cdparam x="279" y="73" />
<sizeparam width="92" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -573,7 +636,7 @@
</COMPONENT>
<COMPONENT type="1001" id="107" >
-<cdparam x="321" y="400" />
+<cdparam x="451" y="586" />
<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -582,7 +645,7 @@
</COMPONENT>
<COMPONENT type="1001" id="109" >
-<cdparam x="489" y="517" />
+<cdparam x="619" y="703" />
<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -590,18 +653,8 @@
<TGConnectingPoint num="0" id="108" />
</COMPONENT>
-<COMPONENT type="1011" id="112" >
-<cdparam x="444" y="457" />
-<sizeparam width="110" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<hidden value="false" />
-<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
-<infoparam name="action state" value="sensorOn=false" />
-<TGConnectingPoint num="0" id="110" />
-<TGConnectingPoint num="1" id="111" />
-</COMPONENT>
-
<COMPONENT type="1010" id="115" >
-<cdparam x="456" y="402" />
+<cdparam x="586" y="588" />
<sizeparam width="86" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -614,7 +667,7 @@
</COMPONENT>
<COMPONENT type="1012" id="123" >
-<cdparam x="392" y="333" />
+<cdparam x="522" y="519" />
<sizeparam width="30" height="30" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -626,23 +679,23 @@
</COMPONENT>
<SUBCOMPONENT type="-1" id="116" >
<father id="123" num="0" />
-<cdparam x="367" y="343" />
-<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="447" y="529" />
+<sizeparam width="40" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-75" maxX="-20" minY="10" maxY="35" />
-<infoparam name="guard 1" value="[ ]" />
+<infoparam name="guard 1" value="[ else]" />
</SUBCOMPONENT>
<SUBCOMPONENT type="-1" id="117" >
<father id="123" num="1" />
-<cdparam x="427" y="343" />
-<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="557" y="529" />
+<sizeparam width="61" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="35" maxX="55" minY="10" maxY="35" />
-<infoparam name="guard 2" value="[ ]" />
+<infoparam name="guard 2" value="[ change]" />
</SUBCOMPONENT>
<SUBCOMPONENT type="-1" id="118" >
<father id="123" num="2" />
-<cdparam x="412" y="378" />
+<cdparam x="542" y="564" />
<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="20" maxX="40" minY="45" maxY="70" />
@@ -650,7 +703,7 @@
</SUBCOMPONENT>
<COMPONENT type="1006" id="126" >
-<cdparam x="362" y="257" />
+<cdparam x="492" y="413" />
<sizeparam width="90" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -663,7 +716,7 @@
</COMPONENT>
<COMPONENT type="1013" id="130" >
-<cdparam x="404" y="194" />
+<cdparam x="534" y="350" />
<sizeparam width="10" height="30" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -673,7 +726,7 @@
</COMPONENT>
<SUBCOMPONENT type="-1" id="127" >
<father id="130" num="0" />
-<cdparam x="419" y="214" />
+<cdparam x="549" y="370" />
<sizeparam width="85" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-75" maxX="30" minY="10" maxY="30" />
@@ -707,55 +760,55 @@
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
<P1 x="409" y="157" id="132" />
-<P2 x="409" y="189" id="128" />
+<P2 x="409" y="180" id="122543" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="115" id="137" >
-<cdparam x="407" y="216" />
+<cdparam x="537" y="372" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
-<P1 x="409" y="229" id="129" />
-<P2 x="407" y="252" id="124" />
+<P1 x="539" y="385" id="129" />
+<P2 x="537" y="408" id="124" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="115" id="138" >
-<cdparam x="407" y="282" />
+<cdparam x="537" y="438" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
-<P1 x="407" y="282" id="125" />
-<P2 x="407" y="323" id="119" />
+<P1 x="537" y="438" id="125" />
+<P2 x="537" y="455" id="244873" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="115" id="139" >
-<cdparam x="447" y="348" />
+<cdparam x="577" y="534" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
-<P1 x="447" y="348" id="121" />
-<P2 x="499" y="397" id="113" />
+<P1 x="577" y="534" id="121" />
+<P2 x="629" y="583" id="113" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="115" id="140" >
-<cdparam x="367" y="348" />
+<cdparam x="497" y="534" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
-<P1 x="499" y="427" id="114" />
-<P2 x="499" y="452" id="110" />
+<P1 x="629" y="613" id="114" />
+<P2 x="629" y="638" id="110" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="115" id="141" >
-<cdparam x="499" y="482" />
+<cdparam x="629" y="668" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
-<P1 x="499" y="482" id="111" />
-<P2 x="499" y="512" id="108" />
+<P1 x="629" y="668" id="111" />
+<P2 x="629" y="698" id="108" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="115" id="142" >
-<cdparam x="367" y="348" />
+<cdparam x="497" y="534" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
-<P1 x="367" y="348" id="120" />
-<P2 x="331" y="395" id="106" />
+<P1 x="497" y="534" id="120" />
+<P2 x="461" y="581" id="106" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="115" id="143" >
@@ -774,55 +827,112 @@
<P2 x="409" y="127" id="131" />
<AutomaticDrawing data="true" />
</CONNECTOR>
+<CONNECTOR type="115" id="122432" >
+<cdparam x="409" y="275" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="409" y="275" id="122428" />
+<P2 x="411" y="295" id="122431" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<COMPONENT type="1011" id="122545" >
+<cdparam x="356" y="185" />
+<sizeparam width="106" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="action state" value="sensorOn=true" />
+<TGConnectingPoint num="0" id="122543" />
+<TGConnectingPoint num="1" id="122544" />
+</COMPONENT>
+
+<COMPONENT type="1011" id="112" >
+<cdparam x="574" y="643" />
+<sizeparam width="110" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="action state" value="sensorOn=false" />
+<TGConnectingPoint num="0" id="110" />
+<TGConnectingPoint num="1" id="111" />
+</COMPONENT>
+
</TMLActivityDiagramPanel>
<TMLActivityDiagramPanel name="DistanceSensor" minX="10" maxX="2500" minY="10" maxY="1500" >
-<COMPONENT type="1001" id="146" >
-<cdparam x="482" y="294" />
+<CONNECTOR type="115" id="244879" >
+<cdparam x="491" y="326" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="491" y="326" id="244878" />
+<P2 x="491" y="360" id="2122" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<COMPONENT type="1017" id="244876" >
+<cdparam x="409" y="301" />
+<sizeparam width="164" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="notified event" value="change=?changeRate()" />
+<TGConnectingPoint num="0" id="244877" />
+<TGConnectingPoint num="1" id="244878" />
+<extraparam>
+<Data eventName="changeRate" variable="change" />
+</extraparam>
+</COMPONENT>
+
+<COMPONENT type="1001" id="2131" >
+<cdparam x="555" y="422" />
<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
<infoparam name="stop state" value="null" />
-<TGConnectingPoint num="0" id="145" />
+<TGConnectingPoint num="0" id="2132" />
</COMPONENT>
-<COMPONENT type="1012" id="154" >
-<cdparam x="397" y="109" />
+<COMPONENT type="1012" id="2121" >
+<cdparam x="476" y="370" />
<sizeparam width="30" height="30" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
<infoparam name="choice" value="null" />
-<TGConnectingPoint num="0" id="150" />
-<TGConnectingPoint num="1" id="151" />
-<TGConnectingPoint num="2" id="152" />
-<TGConnectingPoint num="3" id="153" />
-</COMPONENT>
-<SUBCOMPONENT type="-1" id="147" >
-<father id="154" num="0" />
-<cdparam x="372" y="119" />
-<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<TGConnectingPoint num="0" id="2122" />
+<TGConnectingPoint num="1" id="2123" />
+<TGConnectingPoint num="2" id="2124" />
+<TGConnectingPoint num="3" id="2125" />
+</COMPONENT>
+<SUBCOMPONENT type="-1" id="2126" >
+<father id="2121" num="0" />
+<cdparam x="401" y="380" />
+<sizeparam width="61" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="-75" maxX="-20" minY="10" maxY="35" />
-<infoparam name="guard 1" value="[ ]" />
+<infoparam name="guard 1" value="[ change]" />
</SUBCOMPONENT>
-<SUBCOMPONENT type="-1" id="148" >
-<father id="154" num="1" />
-<cdparam x="432" y="119" />
-<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<SUBCOMPONENT type="-1" id="2127" >
+<father id="2121" num="1" />
+<cdparam x="511" y="380" />
+<sizeparam width="40" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="35" maxX="55" minY="10" maxY="35" />
-<infoparam name="guard 2" value="[ ]" />
+<infoparam name="guard 2" value="[ else]" />
</SUBCOMPONENT>
-<SUBCOMPONENT type="-1" id="149" >
-<father id="154" num="2" />
-<cdparam x="417" y="154" />
+<SUBCOMPONENT type="-1" id="2128" >
+<father id="2121" num="2" />
+<cdparam x="496" y="415" />
<sizeparam width="14" height="15" minWidth="10" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="20" maxX="40" minY="45" maxY="70" />
<infoparam name="guard 3" value="[ ]" />
</SUBCOMPONENT>
+<CONNECTOR type="115" id="2120" >
+<cdparam x="374" y="83" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="374" y="83" id="156" />
+<P2 x="491" y="163" id="164" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
<COMPONENT type="1030" id="157" >
<cdparam x="282" y="69" />
<sizeparam width="92" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -834,7 +944,7 @@
</COMPONENT>
<COMPONENT type="1001" id="159" >
-<cdparam x="324" y="292" />
+<cdparam x="393" y="563" />
<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -875,7 +985,7 @@
</COMPONENT>
<COMPONENT type="1009" id="169" >
-<cdparam x="276" y="231" />
+<cdparam x="345" y="502" />
<sizeparam width="117" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -888,7 +998,7 @@
</COMPONENT>
<COMPONENT type="1010" id="172" >
-<cdparam x="284" y="167" />
+<cdparam x="353" y="438" />
<sizeparam width="100" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -910,30 +1020,6 @@
<TGConnectingPoint num="0" id="173" />
</COMPONENT>
-<CONNECTOR type="115" id="175" >
-<cdparam x="452" y="124" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<infoparam name="connector" value="null" />
-<P1 x="452" y="124" id="152" />
-<P2 x="491" y="163" id="164" />
-<AutomaticDrawing data="true" />
-</CONNECTOR>
-<CONNECTOR type="115" id="176" >
-<cdparam x="522" y="230" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<infoparam name="connector" value="null" />
-<P1 x="372" y="124" id="151" />
-<P2 x="334" y="162" id="170" />
-<AutomaticDrawing data="true" />
-</CONNECTOR>
-<CONNECTOR type="115" id="177" >
-<cdparam x="374" y="83" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<infoparam name="connector" value="null" />
-<P1 x="374" y="83" id="156" />
-<P2 x="412" y="99" id="150" />
-<AutomaticDrawing data="true" />
-</CONNECTOR>
<CONNECTOR type="115" id="178" >
<cdparam x="491" y="193" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -943,19 +1029,19 @@
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="115" id="179" >
-<cdparam x="334" y="192" />
+<cdparam x="403" y="463" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
-<P1 x="334" y="192" id="171" />
-<P2 x="334" y="226" id="167" />
+<P1 x="403" y="463" id="171" />
+<P2 x="403" y="497" id="167" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="115" id="180" >
-<cdparam x="334" y="256" />
+<cdparam x="403" y="527" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
-<P1 x="334" y="256" id="168" />
-<P2 x="334" y="287" id="158" />
+<P1 x="403" y="527" id="168" />
+<P2 x="403" y="558" id="158" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="115" id="181" >
@@ -966,18 +1052,92 @@
<P2 x="328" y="64" id="155" />
<AutomaticDrawing data="true" />
</CONNECTOR>
-<CONNECTOR type="115" id="182" >
+<CONNECTOR type="115" id="2129" >
<cdparam x="491" y="270" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
<P1 x="491" y="270" id="162" />
-<P2 x="492" y="289" id="145" />
+<P2 x="491" y="296" id="244877" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<CONNECTOR type="115" id="2130" >
+<cdparam x="482" y="376" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="451" y="385" id="2123" />
+<P2 x="403" y="433" id="170" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<CONNECTOR type="115" id="2133" >
+<cdparam x="531" y="385" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="531" y="385" id="2124" />
+<P2 x="565" y="417" id="2132" />
<AutomaticDrawing data="true" />
</CONNECTOR>
</TMLActivityDiagramPanel>
<TMLActivityDiagramPanel name="MainControl" minX="10" maxX="2500" minY="10" maxY="1500" >
+<CONNECTOR type="115" id="489769" >
+<cdparam x="1174" y="641" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="1174" y="641" id="332" />
+<P2 x="1192" y="797" id="200" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<CONNECTOR type="115" id="489768" >
+<cdparam x="658" y="598" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="658" y="598" id="323" />
+<P2 x="642" y="677" id="204" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<CONNECTOR type="115" id="489767" >
+<cdparam x="805" y="719" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="805" y="719" id="245231" />
+<P2 x="806" y="744" id="30897" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<CONNECTOR type="115" id="244880" >
+<cdparam x="146" y="573" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="146" y="573" id="281" />
+<P2 x="121" y="711" id="212" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<CONNECTOR type="115" id="61209" >
+<cdparam x="806" y="774" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="806" y="774" id="30898" />
+<P2 x="807" y="820" id="202" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<CONNECTOR type="115" id="15296" >
+<cdparam x="834" y="668" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="770" y="624" id="13434" />
+<P2 x="805" y="689" id="245230" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<COMPONENT type="1030" id="2134" >
+<cdparam x="459" y="69" />
+<sizeparam width="92" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="for ever loop" value="Loop for ever" />
+<TGConnectingPoint num="0" id="2135" />
+<TGConnectingPoint num="1" id="2136" />
+</COMPONENT>
+
<COMPONENT type="301" id="199" >
<cdparam x="10" y="434" />
<sizeparam width="256" height="27" minWidth="20" minHeight="10" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -1009,7 +1169,7 @@ a motor command and new state
</COMPONENT>
<COMPONENT type="1001" id="201" >
-<cdparam x="1164" y="675" />
+<cdparam x="1182" y="802" />
<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -1018,7 +1178,7 @@ a motor command and new state
</COMPONENT>
<COMPONENT type="1001" id="203" >
-<cdparam x="759" y="604" />
+<cdparam x="797" y="825" />
<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -1027,7 +1187,7 @@ a motor command and new state
</COMPONENT>
<COMPONENT type="1001" id="205" >
-<cdparam x="648" y="633" />
+<cdparam x="632" y="682" />
<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -1063,7 +1223,7 @@ a motor command and new state
</COMPONENT>
<COMPONENT type="1001" id="213" >
-<cdparam x="136" y="606" />
+<cdparam x="111" y="716" />
<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
@@ -1071,15 +1231,6 @@ a motor command and new state
<TGConnectingPoint num="0" id="212" />
</COMPONENT>
-<COMPONENT type="1001" id="215" >
-<cdparam x="510" y="109" />
-<sizeparam width="20" height="20" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<hidden value="false" />
-<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
-<infoparam name="stop state" value="null" />
-<TGConnectingPoint num="0" id="214" />
-</COMPONENT>
-
<COMPONENT type="1009" id="218" >
<cdparam x="1015" y="192" />
<sizeparam width="94" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -1155,17 +1306,6 @@ a motor command and new state
</extraparam>
</COMPONENT>
-<COMPONENT type="1020" id="236" >
-<cdparam x="471" y="67" />
-<sizeparam width="98" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<hidden value="false" />
-<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
-<infoparam name="for loop" value="10" />
-<TGConnectingPoint num="0" id="233" />
-<TGConnectingPoint num="1" id="234" />
-<TGConnectingPoint num="2" id="235" />
-</COMPONENT>
-
<COMPONENT type="1013" id="240" >
<cdparam x="264" y="258" />
<sizeparam width="10" height="30" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -1358,32 +1498,6 @@ state 2: obstacles in close proximity
</extraparam>
</COMPONENT>
-<COMPONENT type="1008" id="294" >
-<cdparam x="221" y="655" />
-<sizeparam width="96" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<hidden value="false" />
-<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
-<infoparam name="send event" value="changeRate()" />
-<TGConnectingPoint num="0" id="292" />
-<TGConnectingPoint num="1" id="293" />
-<extraparam>
-<Data eventName="changeRate" nbOfParams="5" />
-</extraparam>
-</COMPONENT>
-
-<COMPONENT type="1008" id="297" >
-<cdparam x="373" y="761" />
-<sizeparam width="84" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<hidden value="false" />
-<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
-<infoparam name="send event" value="startTemp()" />
-<TGConnectingPoint num="0" id="295" />
-<TGConnectingPoint num="1" id="296" />
-<extraparam>
-<Data eventName="startTemp" nbOfParams="5" />
-</extraparam>
-</COMPONENT>
-
<COMPONENT type="1012" id="305" >
<cdparam x="254" y="494" />
<sizeparam width="30" height="30" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -1590,19 +1704,6 @@ state 2: obstacles in close proximity
</extraparam>
</COMPONENT>
-<COMPONENT type="1006" id="351" >
-<cdparam x="486" y="649" />
-<sizeparam width="113" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<hidden value="false" />
-<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
-<infoparam name="write channel" value="samplingRate(1)" />
-<TGConnectingPoint num="0" id="349" />
-<TGConnectingPoint num="1" id="350" />
-<extraparam>
-<Data channelName="samplingRate" nbOfSamples="1" secPattern="" isAttacker="No" />
-</extraparam>
-</COMPONENT>
-
<COMPONENT type="1008" id="354" >
<cdparam x="494" y="594" />
<sizeparam width="96" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -1799,14 +1900,6 @@ state 2: obstacles in close proximity
<P2 x="269" y="484" id="301" />
<AutomaticDrawing data="true" />
</CONNECTOR>
-<CONNECTOR type="115" id="392" >
-<cdparam x="606" y="81" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<infoparam name="connector" value="null" />
-<P1 x="569" y="81" id="234" />
-<P2 x="658" y="104" id="309" />
-<AutomaticDrawing data="true" />
-</CONNECTOR>
<CONNECTOR type="115" id="393" >
<cdparam x="542" y="564" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -1863,14 +1956,6 @@ state 2: obstacles in close proximity
<P2 x="1062" y="187" id="216" />
<AutomaticDrawing data="true" />
</CONNECTOR>
-<CONNECTOR type="115" id="400" >
-<cdparam x="621" y="71" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<infoparam name="connector" value="null" />
-<P1 x="520" y="30" id="317" />
-<P2 x="520" y="62" id="233" />
-<AutomaticDrawing data="true" />
-</CONNECTOR>
<CONNECTOR type="115" id="401" >
<cdparam x="375" y="118" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -2063,22 +2148,6 @@ state 2: obstacles in close proximity
<P2 x="1062" y="417" id="361" />
<AutomaticDrawing data="true" />
</CONNECTOR>
-<CONNECTOR type="115" id="425" >
-<cdparam x="520" y="92" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<infoparam name="connector" value="null" />
-<P1 x="520" y="92" id="235" />
-<P2 x="520" y="104" id="214" />
-<AutomaticDrawing data="true" />
-</CONNECTOR>
-<CONNECTOR type="115" id="426" >
-<cdparam x="146" y="573" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<infoparam name="connector" value="null" />
-<P1 x="146" y="573" id="281" />
-<P2 x="146" y="601" id="212" />
-<AutomaticDrawing data="true" />
-</CONNECTOR>
<CONNECTOR type="115" id="427" >
<cdparam x="269" y="735" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -2103,28 +2172,12 @@ state 2: obstacles in close proximity
<P2 x="542" y="700" id="206" />
<AutomaticDrawing data="true" />
</CONNECTOR>
-<CONNECTOR type="115" id="430" >
-<cdparam x="658" y="598" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<infoparam name="connector" value="null" />
-<P1 x="658" y="598" id="323" />
-<P2 x="658" y="628" id="204" />
-<AutomaticDrawing data="true" />
-</CONNECTOR>
<CONNECTOR type="115" id="431" >
<cdparam x="769" y="571" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="null" />
<P1 x="769" y="571" id="320" />
-<P2 x="769" y="599" id="202" />
-<AutomaticDrawing data="true" />
-</CONNECTOR>
-<CONNECTOR type="115" id="432" >
-<cdparam x="1174" y="641" />
-<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
-<infoparam name="connector" value="null" />
-<P1 x="1174" y="641" id="332" />
-<P2 x="1174" y="670" id="200" />
+<P2 x="770" y="594" id="13433" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="115" id="433" >
@@ -2159,6 +2212,100 @@ state 2: obstacles in close proximity
<P2 x="1063" y="859" id="378" />
<AutomaticDrawing data="true" />
</CONNECTOR>
+<CONNECTOR type="115" id="2137" >
+<cdparam x="520" y="30" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="520" y="30" id="317" />
+<P2 x="505" y="64" id="2135" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<CONNECTOR type="115" id="2138" >
+<cdparam x="603" y="82" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<P1 x="551" y="83" id="2136" />
+<P2 x="658" y="104" id="309" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
+<COMPONENT type="1008" id="294" >
+<cdparam x="221" y="655" />
+<sizeparam width="96" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="send event" value="changeRate()" />
+<TGConnectingPoint num="0" id="292" />
+<TGConnectingPoint num="1" id="293" />
+<extraparam>
+<Data eventName="changeRate" nbOfParams="5" />
+</extraparam>
+</COMPONENT>
+
+<COMPONENT type="1008" id="13435" >
+<cdparam x="722" y="599" />
+<sizeparam width="96" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="send event" value="changeRate()" />
+<TGConnectingPoint num="0" id="13433" />
+<TGConnectingPoint num="1" id="13434" />
+<extraparam>
+<Data eventName="changeRate" nbOfParams="5" />
+</extraparam>
+</COMPONENT>
+
+<COMPONENT type="1008" id="297" >
+<cdparam x="373" y="761" />
+<sizeparam width="84" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="send event" value="startTemp()" />
+<TGConnectingPoint num="0" id="295" />
+<TGConnectingPoint num="1" id="296" />
+<extraparam>
+<Data eventName="startTemp" nbOfParams="5" />
+</extraparam>
+</COMPONENT>
+
+<COMPONENT type="1008" id="30899" >
+<cdparam x="764" y="749" />
+<sizeparam width="84" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="send event" value="startTemp()" />
+<TGConnectingPoint num="0" id="30897" />
+<TGConnectingPoint num="1" id="30898" />
+<extraparam>
+<Data eventName="startTemp" nbOfParams="5" />
+</extraparam>
+</COMPONENT>
+
+<COMPONENT type="1006" id="245232" >
+<cdparam x="749" y="694" />
+<sizeparam width="113" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="write channel" value="samplingRate(1)" />
+<TGConnectingPoint num="0" id="245230" />
+<TGConnectingPoint num="1" id="245231" />
+<extraparam>
+<Data channelName="samplingRate" nbOfSamples="1" secPattern="" isAttacker="No" />
+</extraparam>
+</COMPONENT>
+
+<COMPONENT type="1006" id="351" >
+<cdparam x="486" y="649" />
+<sizeparam width="113" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="write channel" value="samplingRate(1)" />
+<TGConnectingPoint num="0" id="349" />
+<TGConnectingPoint num="1" id="350" />
+<extraparam>
+<Data channelName="samplingRate" nbOfSamples="1" secPattern="" isAttacker="No" />
+</extraparam>
+</COMPONENT>
+
</TMLActivityDiagramPanel>
@@ -2278,11 +2425,11 @@ state 2: obstacles in close proximity
</COMPONENT>
<SUBCOMPONENT type="1101" id="495" >
<father id="547" num="0" />
-<cdparam x="435" y="179" />
-<sizeparam width="159" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="436" y="135" />
+<sizeparam width="152" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="61" minY="0" maxY="175" />
-<infoparam name="TGComponent" value="Rover::MotorControl" />
+<cdrectangleparam minX="0" maxX="68" minY="0" maxY="175" />
+<infoparam name="TGComponent" value="Rover::MainControl" />
<TGConnectingPoint num="0" id="487" />
<TGConnectingPoint num="1" id="488" />
<TGConnectingPoint num="2" id="489" />
@@ -2292,16 +2439,16 @@ state 2: obstacles in close proximity
<TGConnectingPoint num="6" id="493" />
<TGConnectingPoint num="7" id="494" />
<extraparam>
-<info value="Rover::MotorControl" taskName="MotorControl" referenceTaskName="Rover" priority="0" operation="MotorControl" fatherComponentMECType="0" />
+<info value="Rover::MainControl" taskName="MainControl" referenceTaskName="Rover" priority="0" operation="MainControl" fatherComponentMECType="0" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="1101" id="504" >
<father id="547" num="1" />
-<cdparam x="435" y="267" />
-<sizeparam width="203" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="435" y="223" />
+<sizeparam width="177" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="17" minY="0" maxY="175" />
-<infoparam name="TGComponent" value="Rover::TemperatureSensor" />
+<cdrectangleparam minX="0" maxX="43" minY="0" maxY="175" />
+<infoparam name="TGComponent" value="Rover::DistanceSensor" />
<TGConnectingPoint num="0" id="496" />
<TGConnectingPoint num="1" id="497" />
<TGConnectingPoint num="2" id="498" />
@@ -2311,16 +2458,16 @@ state 2: obstacles in close proximity
<TGConnectingPoint num="6" id="502" />
<TGConnectingPoint num="7" id="503" />
<extraparam>
-<info value="Rover::TemperatureSensor" taskName="TemperatureSensor" referenceTaskName="Rover" priority="0" operation="TemperatureSensor" fatherComponentMECType="0" />
+<info value="Rover::DistanceSensor" taskName="DistanceSensor" referenceTaskName="Rover" priority="0" operation="DistanceSensor" fatherComponentMECType="0" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="1101" id="513" >
<father id="547" num="2" />
-<cdparam x="435" y="223" />
-<sizeparam width="177" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="435" y="267" />
+<sizeparam width="203" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="43" minY="0" maxY="175" />
-<infoparam name="TGComponent" value="Rover::DistanceSensor" />
+<cdrectangleparam minX="0" maxX="17" minY="0" maxY="175" />
+<infoparam name="TGComponent" value="Rover::TemperatureSensor" />
<TGConnectingPoint num="0" id="505" />
<TGConnectingPoint num="1" id="506" />
<TGConnectingPoint num="2" id="507" />
@@ -2330,16 +2477,16 @@ state 2: obstacles in close proximity
<TGConnectingPoint num="6" id="511" />
<TGConnectingPoint num="7" id="512" />
<extraparam>
-<info value="Rover::DistanceSensor" taskName="DistanceSensor" referenceTaskName="Rover" priority="0" operation="DistanceSensor" fatherComponentMECType="0" />
+<info value="Rover::TemperatureSensor" taskName="TemperatureSensor" referenceTaskName="Rover" priority="0" operation="TemperatureSensor" fatherComponentMECType="0" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="1101" id="522" >
<father id="547" num="3" />
-<cdparam x="436" y="135" />
-<sizeparam width="152" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="435" y="179" />
+<sizeparam width="159" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="68" minY="0" maxY="175" />
-<infoparam name="TGComponent" value="Rover::MainControl" />
+<cdrectangleparam minX="0" maxX="61" minY="0" maxY="175" />
+<infoparam name="TGComponent" value="Rover::MotorControl" />
<TGConnectingPoint num="0" id="514" />
<TGConnectingPoint num="1" id="515" />
<TGConnectingPoint num="2" id="516" />
@@ -2349,7 +2496,7 @@ state 2: obstacles in close proximity
<TGConnectingPoint num="6" id="520" />
<TGConnectingPoint num="7" id="521" />
<extraparam>
-<info value="Rover::MainControl" taskName="MainControl" referenceTaskName="Rover" priority="0" operation="MainControl" fatherComponentMECType="0" />
+<info value="Rover::MotorControl" taskName="MotorControl" referenceTaskName="Rover" priority="0" operation="MotorControl" fatherComponentMECType="0" />
</extraparam>
</SUBCOMPONENT>
@@ -2444,8 +2591,7 @@ state 2: obstacles in close proximity
<sizeparam width="269" height="58" minWidth="80" minHeight="10" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
-<infoparam name="Proverif Pragma" value="
-" />
+<infoparam name="Proverif Pragma" value="" />
<TGConnectingPoint num="0" id="556" />
<TGConnectingPoint num="1" id="557" />
<TGConnectingPoint num="2" id="558" />
@@ -2463,6 +2609,7 @@ state 2: obstacles in close proximity
<TGConnectingPoint num="14" id="570" />
<TGConnectingPoint num="15" id="571" />
<extraparam>
+<Line value="" />
</extraparam>
</COMPONENT>
@@ -5561,11 +5708,11 @@ state 2: obstacles in close proximity
</COMPONENT>
<SUBCOMPONENT type="5362" id="1986" >
<father id="2029" num="0" />
-<cdparam x="868" y="250" />
-<sizeparam width="190" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="862" y="154" />
+<sizeparam width="201" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="133" minY="0" maxY="160" />
-<infoparam name="TGComponent" value="MainControl/in tempData" />
+<cdrectangleparam minX="0" maxX="122" minY="0" maxY="160" />
+<infoparam name="TGComponent" value="MainControl/in sensorData" />
<TGConnectingPoint num="0" id="1978" />
<TGConnectingPoint num="1" id="1979" />
<TGConnectingPoint num="2" id="1980" />
@@ -5575,7 +5722,7 @@ state 2: obstacles in close proximity
<TGConnectingPoint num="6" id="1984" />
<TGConnectingPoint num="7" id="1985" />
<extraparam>
-<info value="MainControl/in tempData" channelName="MainControl/in tempData(int temp) #--# TemperatureSensor/out tempData(int temp)" fullChannelName="Design::MainControl/in tempData(int temp) #--# TemperatureSensor/out tempData(int temp)" referenceDiagram="Design" />
+<info value="MainControl/in sensorData" channelName="MainControl/in sensorData(int distanceLeft, int distanceFront, int distanceRight) #--# DistanceSensor/out sensorData(int distanceLeft, int distanceFront, int distanceRight)" fullChannelName="Design::MainControl/in sensorData(int distanceLeft, int distanceFront, int distanceRight) #--# DistanceSensor/out sensorData(int distanceLeft, int distanceFront, int distanceRight)" referenceDiagram="Design" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="5362" id="1995" >
@@ -5599,11 +5746,11 @@ state 2: obstacles in close proximity
</SUBCOMPONENT>
<SUBCOMPONENT type="5362" id="2004" >
<father id="2029" num="2" />
-<cdparam x="862" y="154" />
-<sizeparam width="201" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="868" y="250" />
+<sizeparam width="190" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="122" minY="0" maxY="160" />
-<infoparam name="TGComponent" value="MainControl/in sensorData" />
+<cdrectangleparam minX="0" maxX="133" minY="0" maxY="160" />
+<infoparam name="TGComponent" value="MainControl/in tempData" />
<TGConnectingPoint num="0" id="1996" />
<TGConnectingPoint num="1" id="1997" />
<TGConnectingPoint num="2" id="1998" />
@@ -5613,7 +5760,7 @@ state 2: obstacles in close proximity
<TGConnectingPoint num="6" id="2002" />
<TGConnectingPoint num="7" id="2003" />
<extraparam>
-<info value="MainControl/in sensorData" channelName="MainControl/in sensorData(int distanceLeft, int distanceFront, int distanceRight) #--# DistanceSensor/out sensorData(int distanceLeft, int distanceFront, int distanceRight)" fullChannelName="Design::MainControl/in sensorData(int distanceLeft, int distanceFront, int distanceRight) #--# DistanceSensor/out sensorData(int distanceLeft, int distanceFront, int distanceRight)" referenceDiagram="Design" />
+<info value="MainControl/in tempData" channelName="MainControl/in tempData(int temp) #--# TemperatureSensor/out tempData(int temp)" fullChannelName="Design::MainControl/in tempData(int temp) #--# TemperatureSensor/out tempData(int temp)" referenceDiagram="Design" />
</extraparam>
</SUBCOMPONENT>
@@ -5690,11 +5837,11 @@ state 2: obstacles in close proximity
</COMPONENT>
<SUBCOMPONENT type="5352" id="2063" >
<father id="2115" num="0" />
-<cdparam x="102" y="176" />
-<sizeparam width="160" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="100" y="44" />
+<sizeparam width="167" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="90" minY="0" maxY="173" />
-<infoparam name="TGComponent" value="Design::MainControl" />
+<cdrectangleparam minX="0" maxX="83" minY="0" maxY="173" />
+<infoparam name="TGComponent" value="Design::MotorControl" />
<TGConnectingPoint num="0" id="2055" />
<TGConnectingPoint num="1" id="2056" />
<TGConnectingPoint num="2" id="2057" />
@@ -5704,16 +5851,16 @@ state 2: obstacles in close proximity
<TGConnectingPoint num="6" id="2061" />
<TGConnectingPoint num="7" id="2062" />
<extraparam>
-<info value="Design::MainControl" taskName="MainControl" referenceTaskName="Design" />
+<info value="Design::MotorControl" taskName="MotorControl" referenceTaskName="Design" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="5352" id="2072" >
<father id="2115" num="1" />
-<cdparam x="101" y="133" />
-<sizeparam width="185" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="101" y="89" />
+<sizeparam width="211" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="65" minY="0" maxY="173" />
-<infoparam name="TGComponent" value="Design::DistanceSensor" />
+<cdrectangleparam minX="0" maxX="39" minY="0" maxY="173" />
+<infoparam name="TGComponent" value="Design::TemperatureSensor" />
<TGConnectingPoint num="0" id="2064" />
<TGConnectingPoint num="1" id="2065" />
<TGConnectingPoint num="2" id="2066" />
@@ -5723,16 +5870,16 @@ state 2: obstacles in close proximity
<TGConnectingPoint num="6" id="2070" />
<TGConnectingPoint num="7" id="2071" />
<extraparam>
-<info value="Design::DistanceSensor" taskName="DistanceSensor" referenceTaskName="Design" />
+<info value="Design::TemperatureSensor" taskName="TemperatureSensor" referenceTaskName="Design" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="5352" id="2081" >
<father id="2115" num="2" />
-<cdparam x="101" y="89" />
-<sizeparam width="211" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="101" y="133" />
+<sizeparam width="185" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="39" minY="0" maxY="173" />
-<infoparam name="TGComponent" value="Design::TemperatureSensor" />
+<cdrectangleparam minX="0" maxX="65" minY="0" maxY="173" />
+<infoparam name="TGComponent" value="Design::DistanceSensor" />
<TGConnectingPoint num="0" id="2073" />
<TGConnectingPoint num="1" id="2074" />
<TGConnectingPoint num="2" id="2075" />
@@ -5742,16 +5889,16 @@ state 2: obstacles in close proximity
<TGConnectingPoint num="6" id="2079" />
<TGConnectingPoint num="7" id="2080" />
<extraparam>
-<info value="Design::TemperatureSensor" taskName="TemperatureSensor" referenceTaskName="Design" />
+<info value="Design::DistanceSensor" taskName="DistanceSensor" referenceTaskName="Design" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="5352" id="2090" >
<father id="2115" num="3" />
-<cdparam x="100" y="44" />
-<sizeparam width="167" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="102" y="176" />
+<sizeparam width="160" height="40" minWidth="75" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="83" minY="0" maxY="173" />
-<infoparam name="TGComponent" value="Design::MotorControl" />
+<cdrectangleparam minX="0" maxX="90" minY="0" maxY="173" />
+<infoparam name="TGComponent" value="Design::MainControl" />
<TGConnectingPoint num="0" id="2082" />
<TGConnectingPoint num="1" id="2083" />
<TGConnectingPoint num="2" id="2084" />
@@ -5761,7 +5908,7 @@ state 2: obstacles in close proximity
<TGConnectingPoint num="6" id="2088" />
<TGConnectingPoint num="7" id="2089" />
<extraparam>
-<info value="Design::MotorControl" taskName="MotorControl" referenceTaskName="Design" />
+<info value="Design::MainControl" taskName="MainControl" referenceTaskName="Design" />
</extraparam>
</SUBCOMPONENT>
diff --git a/src/main/java/tmltranslator/toavatar/TML2Avatar.java b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
index fd1fe54a3324c512eebf0e3ca0c8dcb77fa0facb..b337ace68689ebbb0a516c5c659f4e6cbd8870ea 100644
--- a/src/main/java/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
@@ -1,40 +1,38 @@
-/* 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.
- */
+/* 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.
+*/
@@ -48,127 +46,126 @@ import tmltranslator.*;
import ui.TGComponent;
import ui.tmlad.*;
import ui.tmlcompd.TMLCPrimitivePort;
-
import java.util.*;
import java.util.regex.Matcher;
import java.util.regex.Pattern;
-/**
- * Class AVATAR2ProVerif
- * Creation: 29/02/2016
- * @version 1.1 29/02/2016
- * @author Ludovic APVRILLE, Letitia LI
- */
-public class TML2Avatar {
- private TMLMapping<?> tmlmap;
- private TMLModeling<?> tmlmodel;
-
- private Map<SecurityPattern, List<AvatarAttribute>> symKeys = new HashMap<SecurityPattern, List<AvatarAttribute>>();
- private Map<SecurityPattern, List<AvatarAttribute>> pubKeys = new HashMap<SecurityPattern, List<AvatarAttribute>>();
- private Map<String, String> nameMap = new HashMap<String, String>();
- //private AvatarAttribute pKey;
- public Map<TMLChannel, Integer> channelMap = new HashMap<TMLChannel,Integer>();
- public Map<TMLTask, AvatarBlock> taskBlockMap = new HashMap<TMLTask, AvatarBlock>();
- public Map<String, Integer> originDestMap = new HashMap<String, Integer>();
- private Map<String, AvatarSignal> signalInMap = new HashMap<String, AvatarSignal>();
- private Map<String, AvatarSignal> signalOutMap = new HashMap<String, AvatarSignal>();
- public Map<String, Object> stateObjectMap = new HashMap<String, Object>();
- public Map<TMLTask, List<SecurityPattern>> accessKeys = new HashMap<TMLTask, List<SecurityPattern>>();
-
- HashMap<String, List<String>> secChannelMap = new HashMap<String, List<String>>();
-
- HashMap<String, AvatarAttributeState> signalAuthOriginMap = new HashMap<String, AvatarAttributeState>();
- HashMap<String, AvatarAttributeState> signalAuthDestMap = new HashMap<String, AvatarAttributeState>();
-
- public ArrayList<SecurityPattern> secPatterns = new ArrayList<SecurityPattern>();
-
- List<AvatarSignal> signals = new ArrayList<AvatarSignal>();
- private final static Integer channelPublic = 0;
- private final static Integer channelPrivate = 1;
- private final static Integer channelUnreachable = 2;
- public int loopLimit = 1;
- AvatarSpecification avspec;
- ArrayList<String> attrsToCheck;
- List<String> allStates;
- boolean mc = false;
- boolean security=false;
- public TML2Avatar(TMLMapping<?> tmlmap, boolean modelcheck, boolean sec) {
- this.tmlmap = tmlmap;
- this.tmlmodel = tmlmap.getTMLModeling();
- allStates = new ArrayList<String>();
- attrsToCheck=new ArrayList<String>();
- mc=modelcheck;
- security=sec;
- }
-
- public void checkConnections(){
- List<HwLink> links = tmlmap.getTMLArchitecture().getHwLinks();
- for (TMLTask t1:tmlmodel.getTasks()){
- List<SecurityPattern> keys = new ArrayList<SecurityPattern>();
- accessKeys.put(t1, keys);
- HwExecutionNode node1 = (HwExecutionNode) tmlmap.getHwNodeOf(t1);
- //Try to find memory using only private buses
- List<HwNode> toVisit = new ArrayList<HwNode>();
- //List<HwNode> toMemory = new ArrayList<HwNode>();
- List<HwNode> complete = new ArrayList<HwNode>();
- for (HwLink link:links){
- if (link.hwnode==node1){
- if (link.bus.privacy==1){
- toVisit.add(link.bus);
- }
- }
- }
- boolean memory=false;
- //memloop:
- while (toVisit.size()>0){
- HwNode curr = toVisit.remove(0);
- for (HwLink link: links){
- if (curr == link.bus){
- if (link.hwnode instanceof HwMemory){
- memory=true;
- List<SecurityPattern> patterns = tmlmap.getMappedPatterns((HwMemory) link.hwnode);
- accessKeys.get(t1).addAll(patterns);
- // break memloop;
- }
- if (!complete.contains(link.hwnode) && !toVisit.contains(link.hwnode) && link.hwnode instanceof HwBridge){
- toVisit.add(link.hwnode);
- }
- }
- else if (curr == link.hwnode){
- if (!complete.contains(link.bus) && !toVisit.contains(link.bus)){
+ /**
+ * Class AVATAR2ProVerif
+ * Creation: 29/02/2016
+ * @version 1.1 29/02/2016
+ * @author Ludovic APVRILLE, Letitia LI
+ */
+ public class TML2Avatar {
+ private TMLMapping<?> tmlmap;
+ private TMLModeling<?> tmlmodel;
+
+ private Map<SecurityPattern, List<AvatarAttribute>> symKeys = new HashMap<SecurityPattern, List<AvatarAttribute>>();
+ private Map<SecurityPattern, List<AvatarAttribute>> pubKeys = new HashMap<SecurityPattern, List<AvatarAttribute>>();
+ private Map<String, String> nameMap = new HashMap<String, String>();
+ //private AvatarAttribute pKey;
+ public Map<TMLChannel, Integer> channelMap = new HashMap<TMLChannel,Integer>();
+ public Map<TMLTask, AvatarBlock> taskBlockMap = new HashMap<TMLTask, AvatarBlock>();
+ public Map<String, Integer> originDestMap = new HashMap<String, Integer>();
+ private Map<String, AvatarSignal> signalInMap = new HashMap<String, AvatarSignal>();
+ private Map<String, AvatarSignal> signalOutMap = new HashMap<String, AvatarSignal>();
+ public Map<String, Object> stateObjectMap = new HashMap<String, Object>();
+ public Map<TMLTask, List<SecurityPattern>> accessKeys = new HashMap<TMLTask, List<SecurityPattern>>();
+
+ HashMap<String, List<String>> secChannelMap = new HashMap<String, List<String>>();
+
+ HashMap<String, AvatarAttributeState> signalAuthOriginMap = new HashMap<String, AvatarAttributeState>();
+ HashMap<String, AvatarAttributeState> signalAuthDestMap = new HashMap<String, AvatarAttributeState>();
+
+ public ArrayList<SecurityPattern> secPatterns = new ArrayList<SecurityPattern>();
+
+ List<AvatarSignal> signals = new ArrayList<AvatarSignal>();
+ private final static Integer channelPublic = 0;
+ private final static Integer channelPrivate = 1;
+ private final static Integer channelUnreachable = 2;
+ public int loopLimit = 1;
+ AvatarSpecification avspec;
+ ArrayList<String> attrsToCheck;
+ List<String> allStates;
+ boolean mc = false;
+ boolean security=false;
+ public TML2Avatar(TMLMapping<?> tmlmap, boolean modelcheck, boolean sec) {
+ this.tmlmap = tmlmap;
+ this.tmlmodel = tmlmap.getTMLModeling();
+ allStates = new ArrayList<String>();
+ attrsToCheck=new ArrayList<String>();
+ mc=modelcheck;
+ security=sec;
+ }
+
+ public void checkConnections(){
+ List<HwLink> links = tmlmap.getTMLArchitecture().getHwLinks();
+ for (TMLTask t1:tmlmodel.getTasks()){
+ List<SecurityPattern> keys = new ArrayList<SecurityPattern>();
+ accessKeys.put(t1, keys);
+ HwExecutionNode node1 = (HwExecutionNode) tmlmap.getHwNodeOf(t1);
+ //Try to find memory using only private buses
+ List<HwNode> toVisit = new ArrayList<HwNode>();
+ //List<HwNode> toMemory = new ArrayList<HwNode>();
+ List<HwNode> complete = new ArrayList<HwNode>();
+ for (HwLink link:links){
+ if (link.hwnode==node1){
+ if (link.bus.privacy==1){
toVisit.add(link.bus);
}
}
}
- complete.add(curr);
- }
- // System.out.println("Memory found ?"+ memory);
- for (TMLTask t2:tmlmodel.getTasks()){
- HwExecutionNode node2 = (HwExecutionNode) tmlmap.getHwNodeOf(t2);
- if (!memory){
- //There is no path to a private memory
- originDestMap.put(t1.getName()+"__"+t2.getName(), channelPublic);
- }
- else if (node1==node2){
- originDestMap.put(t1.getName()+"__"+t2.getName(), channelPrivate);
- }
- else {
- //Navigate architecture for node
-
- //HwNode last = node1;
- List<HwNode> found = new ArrayList<HwNode>();
- List<HwNode> done = new ArrayList<HwNode>();
- List<HwNode> path = new ArrayList<HwNode>();
- Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
+ boolean memory=false;
+ //memloop:
+ while (toVisit.size()>0){
+ HwNode curr = toVisit.remove(0);
for (HwLink link: links){
- if (link.hwnode == node1){
- found.add(link.bus);
- List<HwNode> tmp = new ArrayList<HwNode>();
- tmp.add(link.bus);
- pathMap.put(link.bus, tmp);
+ if (curr == link.bus){
+ if (link.hwnode instanceof HwMemory){
+ memory=true;
+ List<SecurityPattern> patterns = tmlmap.getMappedPatterns((HwMemory) link.hwnode);
+ accessKeys.get(t1).addAll(patterns);
+ // break memloop;
+ }
+ if (!complete.contains(link.hwnode) && !toVisit.contains(link.hwnode) && link.hwnode instanceof HwBridge){
+ toVisit.add(link.hwnode);
+ }
+ }
+ else if (curr == link.hwnode){
+ if (!complete.contains(link.bus) && !toVisit.contains(link.bus)){
+ toVisit.add(link.bus);
+ }
}
}
- outerloop:
+ complete.add(curr);
+ }
+ // System.out.println("Memory found ?"+ memory);
+ for (TMLTask t2:tmlmodel.getTasks()){
+ HwExecutionNode node2 = (HwExecutionNode) tmlmap.getHwNodeOf(t2);
+ if (!memory){
+ //There is no path to a private memory
+ originDestMap.put(t1.getName()+"__"+t2.getName(), channelPublic);
+ }
+ else if (node1==node2){
+ originDestMap.put(t1.getName()+"__"+t2.getName(), channelPrivate);
+ }
+ else {
+ //Navigate architecture for node
+
+ //HwNode last = node1;
+ List<HwNode> found = new ArrayList<HwNode>();
+ List<HwNode> done = new ArrayList<HwNode>();
+ List<HwNode> path = new ArrayList<HwNode>();
+ Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
+ for (HwLink link: links){
+ if (link.hwnode == node1){
+ found.add(link.bus);
+ List<HwNode> tmp = new ArrayList<HwNode>();
+ tmp.add(link.bus);
+ pathMap.put(link.bus, tmp);
+ }
+ }
+outerloop:
while (found.size()>0){
HwNode curr = found.remove(0);
for (HwLink link: links){
@@ -195,1706 +192,1803 @@ public class TML2Avatar {
}
done.add(curr);
}
- if (path.size() ==0){
- originDestMap.put(t1.getName()+"__"+t2.getName(), channelUnreachable);
- }
- else {
- int priv=1;
- HwBus bus;
- //Check if all buses and bridges are private
- for (HwNode n: path){
- if (n instanceof HwBus){
- bus = (HwBus) n;
- if (bus.privacy ==0){
- priv=0;
- break;
+ if (path.size() ==0){
+ originDestMap.put(t1.getName()+"__"+t2.getName(), channelUnreachable);
+ }
+ else {
+ int priv=1;
+ HwBus bus;
+ //Check if all buses and bridges are private
+ for (HwNode n: path){
+ if (n instanceof HwBus){
+ bus = (HwBus) n;
+ if (bus.privacy ==0){
+ priv=0;
+ break;
+ }
}
}
+ originDestMap.put(t1.getName()+"__"+t2.getName(), priv);
}
- originDestMap.put(t1.getName()+"__"+t2.getName(), priv);
}
}
}
}
- }
-
- public void checkChannels(){
- List<TMLChannel> channels = tmlmodel.getChannels();
- List<TMLTask> destinations = new ArrayList<TMLTask>();
- TMLTask a;
- for (TMLChannel channel: channels){
- destinations.clear();
- if (channel.isBasicChannel()){
- a = channel.getOriginTask();
- destinations.add(channel.getDestinationTask());
- }
- else {
- a=channel.getOriginTasks().get(0);
- destinations.addAll(channel.getDestinationTasks());
- }
- HwExecutionNode node1 = (HwExecutionNode) tmlmap.getHwNodeOf(a);
- for (TMLTask t: destinations){
- //List<HwBus> buses = new ArrayList<HwBus>();
- HwNode node2 = tmlmap.getHwNodeOf(t);
-
- if (node1==node2){
- channelMap.put(channel, channelPrivate);
+
+ public void checkChannels(){
+ List<TMLChannel> channels = tmlmodel.getChannels();
+ List<TMLTask> destinations = new ArrayList<TMLTask>();
+ TMLTask a;
+ for (TMLChannel channel: channels){
+ destinations.clear();
+ if (channel.isBasicChannel()){
+ a = channel.getOriginTask();
+ destinations.add(channel.getDestinationTask());
}
-
- if (node1!=node2){
- //Navigate architecture for node
- List<HwLink> links = tmlmap.getTMLArchitecture().getHwLinks();
- //HwNode last = node1;
- List<HwNode> found = new ArrayList<HwNode>();
- List<HwNode> done = new ArrayList<HwNode>();
- List<HwNode> path = new ArrayList<HwNode>();
- Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
-
- for (HwLink link: links){
- if (link.hwnode == node1){
- found.add(link.bus);
- List<HwNode> tmp = new ArrayList<HwNode>();
- tmp.add(link.bus);
- pathMap.put(link.bus, tmp);
- }
+ else {
+ a=channel.getOriginTasks().get(0);
+ destinations.addAll(channel.getDestinationTasks());
+ }
+ HwExecutionNode node1 = (HwExecutionNode) tmlmap.getHwNodeOf(a);
+ for (TMLTask t: destinations){
+ //List<HwBus> buses = new ArrayList<HwBus>();
+ HwNode node2 = tmlmap.getHwNodeOf(t);
+
+ if (node1==node2){
+ channelMap.put(channel, channelPrivate);
}
- outerloop:
- while (found.size()>0){
- HwNode curr = found.remove(0);
+
+ if (node1!=node2){
+ //Navigate architecture for node
+ List<HwLink> links = tmlmap.getTMLArchitecture().getHwLinks();
+ //HwNode last = node1;
+ List<HwNode> found = new ArrayList<HwNode>();
+ List<HwNode> done = new ArrayList<HwNode>();
+ List<HwNode> path = new ArrayList<HwNode>();
+ Map<HwNode, List<HwNode>> pathMap = new HashMap<HwNode, List<HwNode>>();
+
for (HwLink link: links){
- if (curr == link.bus){
- if (link.hwnode == node2){
- path = pathMap.get(curr);
- break outerloop;
- }
- if (!done.contains(link.hwnode) && !found.contains(link.hwnode) && link.hwnode instanceof HwBridge){
- found.add(link.hwnode);
- List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
- tmp.add(link.hwnode);
- pathMap.put(link.hwnode, tmp);
- }
+ if (link.hwnode == node1){
+ found.add(link.bus);
+ List<HwNode> tmp = new ArrayList<HwNode>();
+ tmp.add(link.bus);
+ pathMap.put(link.bus, tmp);
}
- else if (curr == link.hwnode){
- if (!done.contains(link.bus) && !found.contains(link.bus)){
- found.add(link.bus);
- List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
- tmp.add(link.bus);
- pathMap.put(link.bus, tmp);
+ }
+outerloop:
+ while (found.size()>0){
+ HwNode curr = found.remove(0);
+ for (HwLink link: links){
+ if (curr == link.bus){
+ if (link.hwnode == node2){
+ path = pathMap.get(curr);
+ break outerloop;
+ }
+ if (!done.contains(link.hwnode) && !found.contains(link.hwnode) && link.hwnode instanceof HwBridge){
+ found.add(link.hwnode);
+ List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
+ tmp.add(link.hwnode);
+ pathMap.put(link.hwnode, tmp);
+ }
+ }
+ else if (curr == link.hwnode){
+ if (!done.contains(link.bus) && !found.contains(link.bus)){
+ found.add(link.bus);
+ List<HwNode> tmp = new ArrayList<HwNode>(pathMap.get(curr));
+ tmp.add(link.bus);
+ pathMap.put(link.bus, tmp);
+ }
}
}
+ done.add(curr);
}
- done.add(curr);
- }
-
- if (path.size() ==0){
- // System.out.println("Path does not exist for channel " + channel.getName() + " between Task " + a.getTaskName() + " and Task " + t.getTaskName());
- channelMap.put(channel, channelUnreachable);
- }
- else {
- int priv=1;
- HwBus bus;
- //Check if all buses and bridges are private
- for (HwNode n: path){
- if (n instanceof HwBus){
- bus = (HwBus) n;
- if (bus.privacy ==0){
- priv=0;
- break;
+
+ if (path.size() ==0){
+ // System.out.println("Path does not exist for channel " + channel.getName() + " between Task " + a.getTaskName() + " and Task " + t.getTaskName());
+ channelMap.put(channel, channelUnreachable);
+ }
+ else {
+ int priv=1;
+ HwBus bus;
+ //Check if all buses and bridges are private
+ for (HwNode n: path){
+ if (n instanceof HwBus){
+ bus = (HwBus) n;
+ if (bus.privacy ==0){
+ priv=0;
+ break;
+ }
}
}
+
+ channelMap.put(channel, priv);
+ //System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is " + (priv==1 ? "confidential" : "not confidential"));
}
-
- channelMap.put(channel, priv);
- //System.out.println("Channel "+channel.getName() + " between Task "+ a.getTaskName() + " and Task " + t.getTaskName() + " is " + (priv==1 ? "confidential" : "not confidential"));
}
}
- }
- }
- }
-
- public List<AvatarStateMachineElement> translateState(TMLActivityElement ae, AvatarBlock block){
-
-// TMLActionState tmlaction;
-// TMLChoice tmlchoice;
-// TMLExecI tmlexeci;
-// TMLExecIInterval tmlexecii;
- // TMLExecC tmlexecc;
- // TMLExecCInterval tmlexecci;
-// TMLForLoop tmlforloop;
-// TMLReadChannel tmlreadchannel;
-// TMLSendEvent tmlsendevent;
-// TMLSendRequest tmlsendrequest;
-// TMLStopState tmlstopstate;
-// TMLWaitEvent tmlwaitevent;
-// TMLNotifiedEvent tmlnotifiedevent;
-// TMLWriteChannel tmlwritechannel;
-// TMLSequence tmlsequence;
-// TMLRandomSequence tmlrsequence;
-// TMLSelectEvt tmlselectevt;
-// TMLDelay tmldelay;
-
- AvatarTransition tran= new AvatarTransition(block, "", null);
- List<AvatarStateMachineElement> elementList = new ArrayList<AvatarStateMachineElement>();
-
- if (ae==null){
- return elementList;
- }
-
- if (ae instanceof TMLStopState){
- AvatarStopState stops= new AvatarStopState(ae.getName(), ae.getReferenceObject());
- elementList.add(stops);
- return elementList;
- }
- else if (ae instanceof TMLStartState){
- AvatarStartState ss= new AvatarStartState(ae.getName(), ae.getReferenceObject());
- tran = new AvatarTransition(block, "__after_" + ae.getName(), ss.getReferenceObject());
- ss.addNext(tran);
- elementList.add(ss);
- elementList.add(tran);
- }
- else if (ae instanceof TMLRandom){
- AvatarRandom ar = new AvatarRandom(ae.getName(), ae.getReferenceObject());
- TMLRandom tmlr = (TMLRandom) ae;
- ar.setVariable(tmlr.getVariable());
- ar.setValues(tmlr.getMinValue(), tmlr.getMaxValue());
- tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- ar.addNext(tran);
- //Add to list
- elementList.add(ar);
- elementList.add(tran);
- }
- else if (ae instanceof TMLSequence){
- //Get all list of sequences and paste together
- List<AvatarStateMachineElement> seq = translateState(ae.getNextElement(0), block);
- List<AvatarStateMachineElement> tmp;
- // elementList.addAll(seq);
- //get rid of any stops in the middle of the sequence and replace with the start of the next sequence
- for (int i=1; i< ae.getNbNext(); i++){
- tmp = translateState(ae.getNextElement(i), block);
- for (AvatarStateMachineElement e: seq){
- if (e instanceof AvatarStopState){
- //ignore
- }
- else if (e.getNexts().size()==0){
- e.addNext(tmp.get(0));
- elementList.add(e);
- }
- else if (e.getNext(0) instanceof AvatarStopState){
- //Remove the transition to AvatarStopState
- e.removeNext(0);
- e.addNext(tmp.get(0));
- elementList.add(e);
- }
- else {
- elementList.add(e);
- }
- }
- //elementList.addAll(tmp);
- seq = tmp;
- }
- //Put stop states on the end of the last in sequence
-
- for (AvatarStateMachineElement e: seq){
- if (e.getNexts().size()==0 && !(e instanceof AvatarStopState)){
- AvatarStopState stop = new AvatarStopState("stop", null);
- e.addNext(stop);
- elementList.add(stop);
- }
- elementList.add(e);
- }
- return elementList;
-
- }
- else if (ae instanceof TMLSendRequest){
- TMLSendRequest sr= (TMLSendRequest) ae;
- TMLRequest req = sr.getRequest();
- AvatarSignal sig;
- boolean checkAcc=false;
- if (ae.getReferenceObject()!=null){
- checkAcc=((TGComponent)ae.getReferenceObject()).getCheckableAccessibility();
- }
- AvatarState signalState = new AvatarState("signalstate_"+ae.getName().replaceAll(" ","")+"_"+req.getName().replaceAll(" ",""),ae.getReferenceObject(), checkAcc);
- AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_"+ae.getName()+"_"+req.getName(), ae.getReferenceObject());
- if (!signalOutMap.containsKey(req.getName())){
- sig = new AvatarSignal(getName(req.getName()), AvatarSignal.OUT, req.getReferenceObject());
- signals.add(sig);
- signalOutMap.put(req.getName(), sig);
- block.addSignal(sig);
- }
- else {
- sig=signalOutMap.get(req.getName());
+ }
}
- AvatarActionOnSignal as= new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
- for (int i=0; i<sr.getNbOfParams(); i++){
- if (block.getAvatarAttributeWithName(sr.getParam(i))==null){
- //Throw Error
- System.out.println("Missing Attribute " + sr.getParam(i));
- as.addValue("tmp");
- }
- else {
- as.addValue(sr.getParam(i));
- }
- }
- //Create new value to send....
- AvatarAttribute requestData= new AvatarAttribute(req.getName()+"__reqData", AvatarType.INTEGER, block, null);
- as.addValue(req.getName()+"__reqData");
- if (block.getAvatarAttributeWithName(req.getName()+"__reqData")==null){
- block.addAttribute(requestData);
- }
- if (req.checkAuth){
- AvatarAttributeState authOrig = new AvatarAttributeState(block.getName()+"."+signalState.getName()+"."+requestData.getName(),ae.getReferenceObject(),requestData, signalState);
- signalAuthOriginMap.put(req.getName(), authOrig);
- }
- tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- elementList.add(signalState);
- signalState.addNext(signalTran);
- elementList.add(signalTran);
- signalTran.addNext(as);
- elementList.add(as);
- as.addNext(tran);
- elementList.add(tran);
- }
- else if (ae instanceof TMLRandomSequence){
- //HashMap<Integer, List<AvatarStateMachineElement>> seqs = new HashMap<Integer, List<AvatarStateMachineElement>>();
- AvatarState choiceState = new AvatarState("seqchoice__"+ae.getName().replaceAll(" ",""), ae.getReferenceObject());
- elementList.add(choiceState);
- if (ae.getNbNext()==2){
- List<AvatarStateMachineElement> set0= translateState(ae.getNextElement(0), block);
- List<AvatarStateMachineElement> set1 = translateState(ae.getNextElement(1), block);
-// elementList.addAll(set0);
-
- //Remove stop states of sets and route their transitions to the first element of the following sequence
- for (AvatarStateMachineElement e: set0){
- if (e instanceof AvatarStopState){
- //ignore
- }
- else if (e.getNexts().size()==0){
- e.addNext(set1.get(0));
- elementList.add(e);
- }
- else if (e.getNext(0) instanceof AvatarStopState){
- //Remove the transition to AvatarStopState
- e.removeNext(0);
- e.addNext(set1.get(0));
- elementList.add(e);
+ public List<AvatarStateMachineElement> translateState(TMLActivityElement ae, AvatarBlock block){
+
+ // TMLActionState tmlaction;
+ // TMLChoice tmlchoice;
+ // TMLExecI tmlexeci;
+ // TMLExecIInterval tmlexecii;
+ // TMLExecC tmlexecc;
+ // TMLExecCInterval tmlexecci;
+ // TMLForLoop tmlforloop;
+ // TMLReadChannel tmlreadchannel;
+ // TMLSendEvent tmlsendevent;
+ // TMLSendRequest tmlsendrequest;
+ // TMLStopState tmlstopstate;
+ // TMLWaitEvent tmlwaitevent;
+ // TMLNotifiedEvent tmlnotifiedevent;
+ // TMLWriteChannel tmlwritechannel;
+ // TMLSequence tmlsequence;
+ // TMLRandomSequence tmlrsequence;
+ // TMLSelectEvt tmlselectevt;
+ // TMLDelay tmldelay;
+
+ AvatarTransition tran= new AvatarTransition(block, "", null);
+ List<AvatarStateMachineElement> elementList = new ArrayList<AvatarStateMachineElement>();
+
+ if (ae==null){
+ return elementList;
+ }
+
+ if (ae instanceof TMLStopState){
+ AvatarStopState stops= new AvatarStopState(ae.getName(), ae.getReferenceObject());
+ elementList.add(stops);
+ return elementList;
+ }
+ else if (ae instanceof TMLStartState){
+ AvatarStartState ss= new AvatarStartState(ae.getName(), ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_" + ae.getName(), ss.getReferenceObject());
+ ss.addNext(tran);
+ elementList.add(ss);
+ elementList.add(tran);
}
- else {
- elementList.add(e);
+ else if (ae instanceof TMLRandom){
+ AvatarRandom ar = new AvatarRandom(ae.getName(), ae.getReferenceObject());
+ TMLRandom tmlr = (TMLRandom) ae;
+ ar.setVariable(tmlr.getVariable());
+ ar.setValues(tmlr.getMinValue(), tmlr.getMaxValue());
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ ar.addNext(tran);
+ //Add to list
+ elementList.add(ar);
+ elementList.add(tran);
}
- }
+ else if (ae instanceof TMLSequence){
+ //Get all list of sequences and paste together
+ List<AvatarStateMachineElement> seq = translateState(ae.getNextElement(0), block);
+ List<AvatarStateMachineElement> tmp;
+ // elementList.addAll(seq);
+ //get rid of any stops in the middle of the sequence and replace with the start of the next sequence
+ for (int i=1; i< ae.getNbNext(); i++){
+ tmp = translateState(ae.getNextElement(i), block);
+ for (AvatarStateMachineElement e: seq){
+ if (e instanceof AvatarStopState){
+ //ignore
+ }
+ else if (e.getNexts().size()==0){
+ e.addNext(tmp.get(0));
+ elementList.add(e);
+ }
+ else if (e.getNext(0) instanceof AvatarStopState){
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(tmp.get(0));
+ elementList.add(e);
+ }
+ else {
+ elementList.add(e);
+ }
+ }
+ //elementList.addAll(tmp);
+ seq = tmp;
+ }
+ //Put stop states on the end of the last in sequence
+ for (AvatarStateMachineElement e: seq){
+ if (e.getNexts().size()==0 && !(e instanceof AvatarStopState)){
+ AvatarStopState stop = new AvatarStopState("stop", null);
+ e.addNext(stop);
+ elementList.add(stop);
+ }
+ elementList.add(e);
+ }
+ return elementList;
- //Build branch 0
- tran = new AvatarTransition(block, "__after_"+ae.getName()+"_0", ae.getReferenceObject());
- choiceState.addNext(tran);
- elementList.add(tran);
- tran.addNext(set0.get(0));
- //Put stop states at the end of set1 if they don't already exist
- AvatarStopState stop = new AvatarStopState("stop", null);
- for (AvatarStateMachineElement e: set1){
- if (e.getNexts().size()==0 && (e instanceof AvatarTransition)){
- e.addNext(stop);
- }
- elementList.add(e);
- }
- elementList.add(stop);
-
- //Build branch 1
- List<AvatarStateMachineElement> set0_1 = translateState(ae.getNextElement(0), block);
- List<AvatarStateMachineElement> set1_1 = translateState(ae.getNextElement(1), block);
- for (AvatarStateMachineElement e: set1_1){
- if (e instanceof AvatarStopState){
- //ignore
- }
- else if (e.getNexts().size()==0){
- e.addNext(set0_1.get(0));
- elementList.add(e);
- }
- else if (e.getNext(0) instanceof AvatarStopState){
- //Remove the transition to AvatarStopState
- e.removeNext(0);
- e.addNext(set0_1.get(0));
- elementList.add(e);
- }
- else {
- elementList.add(e);
- }
- }
- tran = new AvatarTransition(block, "__after_"+ae.getName()+"_1", ae.getReferenceObject());
- elementList.add(tran);
- choiceState.addNext(tran);
- tran.addNext(set1_1.get(0));
- stop = new AvatarStopState("stop", null);
- for (AvatarStateMachineElement e: set0_1){
- if (e.getNexts().size()==0 && (e instanceof AvatarTransition)){
- e.addNext(stop);
- }
- elementList.add(e);
- }
- elementList.add(stop);
-
- }
- else {
- //This gets really complicated in ProVerif
- for (int i=0; i< ae.getNbNext(); i++){
- //For each of the possible state blocks, translate 1 and recurse on the remaining random sequence
- tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae.getReferenceObject());
- choiceState.addNext(tran);
- List<AvatarStateMachineElement> tmp = translateState(ae.getNextElement(i), block);
- tran.addNext(tmp.get(0));
- TMLRandomSequence newSeq = new TMLRandomSequence("seqchoice__"+i+"_"+ae.getNbNext()+"_"+ae.getName(), ae.getReferenceObject());
- for (int j=0; j< ae.getNbNext(); j++){
- if (j!=i){
- newSeq.addNext(ae.getNextElement(j));
}
- }
- tran = new AvatarTransition(block, "__after_"+ae.getNextElement(i).getName(), ae.getReferenceObject());
- tmp.get(tmp.size()-1).addNext(tran);
- elementList.addAll(tmp);
- elementList.add(tran);
- List<AvatarStateMachineElement> nexts = translateState(newSeq, block);
- elementList.addAll(nexts);
- tran.addNext(nexts.get(0));
- }
- }
- return elementList;
- }
- else if (ae instanceof TMLActivityElementEvent){
- TMLActivityElementEvent aee = (TMLActivityElementEvent) ae;
- TMLEvent evt = aee.getEvent();
- boolean checkAcc = false;
- if (ae.getReferenceObject()!=null){
- checkAcc =((TGComponent) ae.getReferenceObject()).getCheckableAccessibility();
- }
- AvatarState signalState = new AvatarState("signalstate_"+ae.getName().replaceAll(" ","")+"_"+evt.getName(),ae.getReferenceObject(), checkAcc);
- AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_"+ae.getName()+"_"+evt.getName(), ae.getReferenceObject());
- if (ae instanceof TMLSendEvent){
- AvatarSignal sig;
- if (!signalOutMap.containsKey(evt.getName())){
- sig = new AvatarSignal(getName(evt.getName()), AvatarSignal.OUT, evt.getReferenceObject());
- signals.add(sig);
- block.addSignal(sig);
- signalOutMap.put(evt.getName(), sig);
+ else if (ae instanceof TMLSendRequest){
+ TMLSendRequest sr= (TMLSendRequest) ae;
+ TMLRequest req = sr.getRequest();
+ AvatarSignal sig;
+ boolean checkAcc=false;
+ if (ae.getReferenceObject()!=null){
+ checkAcc=((TGComponent)ae.getReferenceObject()).getCheckableAccessibility();
}
- else {
- sig=signalOutMap.get(evt.getName());
- }
- AvatarActionOnSignal as= new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
- for (int i=0; i< aee.getNbOfParams(); i++){
- if (block.getAvatarAttributeWithName(aee.getParam(i))==null){
- //Throw Error
- as.addValue("tmp");
- System.out.println("Missing Attribute " + aee.getParam(i));
- }
- else {
- as.addValue(aee.getParam(i));
- }
- }
-
- tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- elementList.add(signalState);
- signalState.addNext(signalTran);
- elementList.add(signalTran);
- signalTran.addNext(as);
- elementList.add(as);
- as.addNext(tran);
- elementList.add(tran);
-
-
- }
- else if (ae instanceof TMLWaitEvent){
- AvatarSignal sig;
- if (!signalInMap.containsKey(evt.getName())){
- sig = new AvatarSignal(getName(evt.getName()), AvatarSignal.IN, evt.getReferenceObject());
- signals.add(sig);
- block.addSignal(sig);
- signalInMap.put(evt.getName(), sig);
- }
- else {
- sig=signalInMap.get(evt.getName());
- }
- AvatarActionOnSignal as= new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
- for (int i=0; i< aee.getNbOfParams(); i++){
-
- if (block.getAvatarAttributeWithName(aee.getParam(i))==null){
- //Throw Error
- as.addValue("tmp");
- System.out.println("Missing Attribute " + aee.getParam(i));
- }
- else {
- as.addValue(aee.getParam(i));
- }
- }
-
- tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- elementList.add(signalState);
- signalState.addNext(signalTran);
- elementList.add(signalTran);
- signalTran.addNext(as);
- elementList.add(as);
- as.addNext(tran);
- elementList.add(tran);
- }
- else {
- //Notify Event, I don't know how to translate this
- AvatarRandom as = new AvatarRandom(ae.getName(), ae.getReferenceObject());
- tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- as.setVariable(aee.getVariable());
- as.setValues("0", "1");
- as.addNext(tran);
- elementList.add(as);
- elementList.add(tran);
- }
-
- }
- else if (ae instanceof TMLActivityElementWithAction){
- //Might be encrypt or decrypt
- AvatarState as = new AvatarState(ae.getValue().replaceAll(" ","")+"_"+ae.getName().replaceAll(" ",""), ae.getReferenceObject());
- tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- as.addNext(tran);
- elementList.add(as);
- elementList.add(tran);
- if (security && ae.securityPattern!=null){
- //If encryption
- if (ae.securityPattern!=null && ae.getName().contains("encrypt")){
- secPatterns.add(ae.securityPattern);
- if (ae.securityPattern.type.equals("Advanced")){
- //Type Advanced
- tran.addAction(ae.securityPattern.formula);
+ AvatarState signalState = new AvatarState("signalstate_"+ae.getName().replaceAll(" ","")+"_"+req.getName().replaceAll(" ",""),ae.getReferenceObject(), checkAcc);
+ AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_"+ae.getName()+"_"+req.getName(), ae.getReferenceObject());
+ if (!signalOutMap.containsKey(req.getName())){
+ sig = new AvatarSignal(getName(req.getName()), AvatarSignal.OUT, req.getReferenceObject());
+ signals.add(sig);
+ signalOutMap.put(req.getName(), sig);
+ block.addSignal(sig);
+ }
+ else {
+ sig=signalOutMap.get(req.getName());
}
- else if (ae.securityPattern.type.equals("Symmetric Encryption")){
- //Type Symmetric Encryption
- if (!ae.securityPattern.nonce.isEmpty()){
- //Concatenate nonce to data
-
- //Create concat2 method
- block.addAttribute(new AvatarAttribute(ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
-
- AvatarMethod concat2 = new AvatarMethod("concat2",ae);
- concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
- concat2.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) !=null && block.getAvatarAttributeWithName(ae.securityPattern.nonce)!=null){
- block.addMethod(concat2);
- tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name + ","+ae.securityPattern.nonce+")");
+ AvatarActionOnSignal as= new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ for (int i=0; i<sr.getNbOfParams(); i++){
+ if (block.getAvatarAttributeWithName(sr.getParam(i))==null){
+ //Throw Error
+ System.out.println("Missing Attribute " + sr.getParam(i));
+ as.addValue("tmp");
+ }
+ else {
+ as.addValue(sr.getParam(i));
+ }
+ }
+ //Create new value to send....
+ AvatarAttribute requestData= new AvatarAttribute(req.getName()+"__reqData", AvatarType.INTEGER, block, null);
+ as.addValue(req.getName()+"__reqData");
+ if (block.getAvatarAttributeWithName(req.getName()+"__reqData")==null){
+ block.addAttribute(requestData);
+ }
+ if (req.checkAuth){
+ AvatarAttributeState authOrig = new AvatarAttributeState(block.getName()+"."+signalState.getName()+"."+requestData.getName(),ae.getReferenceObject(),requestData, signalState);
+ signalAuthOriginMap.put(req.getName(), authOrig);
+ }
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ elementList.add(signalState);
+ signalState.addNext(signalTran);
+ elementList.add(signalTran);
+ signalTran.addNext(as);
+ elementList.add(as);
+ as.addNext(tran);
+ elementList.add(tran);
+ }
+ else if (ae instanceof TMLRandomSequence){
+ //HashMap<Integer, List<AvatarStateMachineElement>> seqs = new HashMap<Integer, List<AvatarStateMachineElement>>();
+ AvatarState choiceState = new AvatarState("seqchoice__"+ae.getName().replaceAll(" ",""), ae.getReferenceObject());
+ elementList.add(choiceState);
+ if (ae.getNbNext()==2){
+ List<AvatarStateMachineElement> set0= translateState(ae.getNextElement(0), block);
+ List<AvatarStateMachineElement> set1 = translateState(ae.getNextElement(1), block);
+ // elementList.addAll(set0);
+
+ //Remove stop states of sets and route their transitions to the first element of the following sequence
+ for (AvatarStateMachineElement e: set0){
+ if (e instanceof AvatarStopState){
+ //ignore
+ }
+ else if (e.getNexts().size()==0){
+ e.addNext(set1.get(0));
+ elementList.add(e);
+ }
+ else if (e.getNext(0) instanceof AvatarStopState){
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(set1.get(0));
+ elementList.add(e);
+ }
+ else {
+ elementList.add(e);
}
}
- if (!ae.securityPattern.key.isEmpty()){
- //Securing a key
- //Create sencrypt method for key
- block.addAttribute(new AvatarAttribute(ae.securityPattern.key, AvatarType.INTEGER, block,null));
- block.addAttribute(new AvatarAttribute("encryptedKey_"+ae.securityPattern.key, AvatarType.INTEGER, block,null));
- block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
- AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae);
- sencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.key));
- sencrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
- sencrypt.addReturnParameter(block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key));
-
- if (block.getAvatarAttributeWithName(ae.securityPattern.key)!=null && block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null){
- block.addMethod(sencrypt);
- tran.addAction("encryptedKey_"+ ae.securityPattern.key + " = sencrypt(key_"+ae.securityPattern.key+", key_"+ae.securityPattern.name+")");
+ //Build branch 0
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_0", ae.getReferenceObject());
+ choiceState.addNext(tran);
+ elementList.add(tran);
+ tran.addNext(set0.get(0));
+ //Put stop states at the end of set1 if they don't already exist
+ AvatarStopState stop = new AvatarStopState("stop", null);
+ for (AvatarStateMachineElement e: set1){
+ if (e.getNexts().size()==0 && (e instanceof AvatarTransition)){
+ e.addNext(stop);
}
+ elementList.add(e);
}
- else {
- //Securing data
-
- //Create sencrypt method for data
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block,null));
- block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
-
- AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae);
- sencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- sencrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
- sencrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
-
- if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null){
- block.addMethod(sencrypt);
+ elementList.add(stop);
+
+ //Build branch 1
+ List<AvatarStateMachineElement> set0_1 = translateState(ae.getNextElement(0), block);
+ List<AvatarStateMachineElement> set1_1 = translateState(ae.getNextElement(1), block);
+ for (AvatarStateMachineElement e: set1_1){
+ if (e instanceof AvatarStopState){
+ //ignore
+ }
+ else if (e.getNexts().size()==0){
+ e.addNext(set0_1.get(0));
+ elementList.add(e);
+ }
+ else if (e.getNext(0) instanceof AvatarStopState){
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(set0_1.get(0));
+ elementList.add(e);
}
- tran.addAction(ae.securityPattern.name+"_encrypted = sencrypt("+ae.securityPattern.name+", key_"+ae.securityPattern.name+")");
+ else {
+ elementList.add(e);
+ }
+ }
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_1", ae.getReferenceObject());
+ elementList.add(tran);
+ choiceState.addNext(tran);
+ tran.addNext(set1_1.get(0));
+ stop = new AvatarStopState("stop", null);
+ for (AvatarStateMachineElement e: set0_1){
+ if (e.getNexts().size()==0 && (e instanceof AvatarTransition)){
+ e.addNext(stop);
+ }
+ elementList.add(e);
}
- //Set as origin for authenticity
- ae.securityPattern.originTask=block.getName();
- ae.securityPattern.state1=as;
+ elementList.add(stop);
+
}
- else if (ae.securityPattern.type.equals("Asymmetric Encryption")){
- if (!ae.securityPattern.nonce.isEmpty()){
- //Concatenating a nonce
- //Add concat2 method
- block.addAttribute(new AvatarAttribute(ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- AvatarMethod concat2 = new AvatarMethod("concat2",ae);
- concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) !=null && block.getAvatarAttributeWithName(ae.securityPattern.nonce)!=null){
- block.addMethod(concat2);
- tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name + ","+ae.securityPattern.nonce+")");
- }
- }
- //Securing a key instead of data
- if (!ae.securityPattern.key.isEmpty()){
- //Add aencrypt method
- AvatarMethod aencrypt = new AvatarMethod("aencrypt", ae);
- block.addAttribute(new AvatarAttribute("encryptedKey_"+ae.securityPattern.key, AvatarType.INTEGER, block,null));
- aencrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.key));
- aencrypt.addParameter(block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name));
- aencrypt.addReturnParameter(block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key));
- if (block.getAvatarAttributeWithName("key_"+ae.securityPattern.key)!=null && block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key)!=null){
- block.addMethod(aencrypt);
- tran.addAction("encryptedKey_"+ ae.securityPattern.key + " = aencrypt(key_"+ae.securityPattern.key+", pubKey_"+ae.securityPattern.name+")");
+ else {
+ //This gets really complicated in ProVerif
+ for (int i=0; i< ae.getNbNext(); i++){
+ //For each of the possible state blocks, translate 1 and recurse on the remaining random sequence
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae.getReferenceObject());
+ choiceState.addNext(tran);
+ List<AvatarStateMachineElement> tmp = translateState(ae.getNextElement(i), block);
+ tran.addNext(tmp.get(0));
+ TMLRandomSequence newSeq = new TMLRandomSequence("seqchoice__"+i+"_"+ae.getNbNext()+"_"+ae.getName(), ae.getReferenceObject());
+ for (int j=0; j< ae.getNbNext(); j++){
+ if (j!=i){
+ newSeq.addNext(ae.getNextElement(j));
+ }
}
+ tran = new AvatarTransition(block, "__after_"+ae.getNextElement(i).getName(), ae.getReferenceObject());
+ tmp.get(tmp.size()-1).addNext(tran);
+ elementList.addAll(tmp);
+ elementList.add(tran);
+ List<AvatarStateMachineElement> nexts = translateState(newSeq, block);
+ elementList.addAll(nexts);
+ tran.addNext(nexts.get(0));
}
- else {
- //Securing data
-
- //Add aencrypt method
- AvatarMethod aencrypt = new AvatarMethod("aencrypt", ae);
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("pubKey_"+ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
- aencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- aencrypt.addParameter(block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name));
- aencrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
- if (block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null){
- block.addMethod(aencrypt);
- tran.addAction(ae.securityPattern.name+"_encrypted = aencrypt("+ae.securityPattern.name+", pubKey_"+ae.securityPattern.name+")");
- }
- }
- //Set as origin state for authenticity
- ae.securityPattern.originTask=block.getName();
- ae.securityPattern.state1=as;
}
- else if (ae.securityPattern.type.equals("Nonce")){
- //Create a nonce by a random function
- AvatarRandom arandom = new AvatarRandom("randomnonce",ae.getReferenceObject());
- arandom.setVariable(ae.securityPattern.name);
- arandom.setValues("0","10");
- elementList.add(arandom);
- tran.addNext(arandom);
- tran = new AvatarTransition(block, "__afterrandom_"+ae.getName(), ae.getReferenceObject());
- arandom.addNext(tran);
- elementList.add(tran);
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ return elementList;
+ }
+ else if (ae instanceof TMLActivityElementEvent){
+ TMLActivityElementEvent aee = (TMLActivityElementEvent) ae;
+ TMLEvent evt = aee.getEvent();
+ boolean checkAcc = false;
+ if (ae.getReferenceObject()!=null){
+ checkAcc =((TGComponent) ae.getReferenceObject()).getCheckableAccessibility();
}
- else if (ae.securityPattern.type.equals("Hash")){
- AvatarMethod hash = new AvatarMethod("hash", ae);
- hash.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
- block.addMethod(hash);
+ AvatarState signalState = new AvatarState("signalstate_"+ae.getName().replaceAll(" ","")+"_"+evt.getName(),ae.getReferenceObject(), checkAcc);
+ AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_"+ae.getName()+"_"+evt.getName(), ae.getReferenceObject());
+ if (ae instanceof TMLSendEvent){
+ AvatarSignal sig;
+ if (!signalOutMap.containsKey(evt.getName())){
+ sig = new AvatarSignal(getName(evt.getName()), AvatarSignal.OUT, evt.getReferenceObject());
+ signals.add(sig);
+ block.addSignal(sig);
+ signalOutMap.put(evt.getName(), sig);
}
- tran.addAction(ae.securityPattern.name+"_encrypted = hash("+ae.securityPattern.name+")");
- }
- else if (ae.securityPattern.type.equals("MAC")){
-
- if (!ae.securityPattern.nonce.isEmpty()){
- //Add nonce
-
- //Add concat2 method
- AvatarMethod concat = new AvatarMethod("concat2", ae);
- concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
- concat.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) !=null && block.getAvatarAttributeWithName(ae.securityPattern.nonce)!=null){
- block.addMethod(concat);
- tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name+","+ae.securityPattern.nonce+")");
+ else {
+ sig=signalOutMap.get(evt.getName());
+ }
+ AvatarActionOnSignal as= new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ for (int i=0; i< aee.getNbOfParams(); i++){
+ if (block.getAvatarAttributeWithName(aee.getParam(i))==null){
+ //Throw Error
+ as.addValue("tmp");
+ System.out.println("Missing Attribute " + aee.getParam(i));
+ }
+ else {
+ as.addValue(aee.getParam(i));
}
}
- //Create MAC method
- AvatarMethod mac = new AvatarMethod("MAC", ae);
- AvatarAttribute macattr = new AvatarAttribute(ae.securityPattern.name +"_mac", AvatarType.INTEGER, block, null);
- block.addAttribute(macattr);
-
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null)); //msg + mac(msg)
-
- mac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- mac.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
- mac.addReturnParameter(macattr);
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ elementList.add(signalState);
+ signalState.addNext(signalTran);
+ elementList.add(signalTran);
+ signalTran.addNext(as);
+ elementList.add(as);
+ as.addNext(tran);
+ elementList.add(tran);
- if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null){
- block.addMethod(mac);
- tran.addAction(ae.securityPattern.name+"_mac = MAC("+ae.securityPattern.name+",key_"+ae.securityPattern.name+")");
- }
- //Concatenate msg and mac(msg)
-
- //Create concat2 method
- AvatarMethod concat = new AvatarMethod("concat2", ae);
- concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_mac"));
- concat.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
- //concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null){
- block.addMethod(concat);
- tran.addAction(ae.securityPattern.name+"_encrypted = concat2("+ae.securityPattern.name +","+ae.securityPattern.name+"_mac)");
- }
- ae.securityPattern.originTask=block.getName();
- ae.securityPattern.state1=as;
}
- //Set attributestate for authenticity
- AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName()+"."+as.getName()+"."+ae.securityPattern.name,ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), as);
- signalAuthOriginMap.put(ae.securityPattern.name, authOrigin);
-
- }
- else if (ae.securityPattern!=null && ae.getName().contains("decrypt")){
- //Decryption action
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
- if (ae.securityPattern.type.equals("Symmetric Encryption")){
- if (!ae.securityPattern.key.isEmpty()){
- //Decrypting a key
- //Add sdecrypt method
- AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae);
- block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.key, AvatarType.INTEGER, block,null));
- block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
- block.addAttribute(new AvatarAttribute("encryptedKey_"+ae.securityPattern.key, AvatarType.INTEGER, block,null));
-
- sdecrypt.addParameter(block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key));
- sdecrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
- sdecrypt.addReturnParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.key));
- if (block.getAvatarAttributeWithName("key_"+ae.securityPattern.key)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key)!=null){
- block.addMethod(sdecrypt);
- tran.addAction(ae.securityPattern.key+" = sdecrypt(encryptedKey_"+ae.securityPattern.key+", key_"+ae.securityPattern.name+")");
- }
+ else if (ae instanceof TMLWaitEvent){
+ AvatarSignal sig;
+ if (!signalInMap.containsKey(evt.getName())){
+ sig = new AvatarSignal(getName(evt.getName()), AvatarSignal.IN, evt.getReferenceObject());
+ signals.add(sig);
+ block.addSignal(sig);
+ signalInMap.put(evt.getName(), sig);
}
else {
- //Decrypting data
- AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae);
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
- block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block,null));
-
- sdecrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
- sdecrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
- sdecrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
- block.addMethod(sdecrypt);
- tran.addAction(ae.securityPattern.name+" = sdecrypt("+ae.securityPattern.name+"_encrypted, key_"+ae.securityPattern.name+")");
- }
- }
- if (!ae.securityPattern.nonce.isEmpty()){
- //Separate out the nonce
- block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- //Add get2 method
- AvatarMethod get2 = new AvatarMethod("get2",ae);
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.nonce));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.nonce)!=null) {
- block.addMethod(get2);
- tran.addAction("get2("+ae.securityPattern.name + ","+ae.securityPattern.name+",testnonce_"+ae.securityPattern.nonce+")");
- }
-
- //Add state after get2 statement
- AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ","")+"_guarded", ae.getReferenceObject());
- tran.addNext(guardState);
- tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
- guardState.addNext(tran);
- elementList.add(guardState);
- elementList.add(tran);
-
- //Guard transition to determine if nonce matches
- tran.setGuard("testnonce_"+ae.securityPattern.nonce+"==" + ae.securityPattern.nonce);
+ sig=signalInMap.get(evt.getName());
}
- //Add a dummy state afterwards for authenticity after decrypting the data
- AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ","")+"_dummy", ae.getReferenceObject());
- ae.securityPattern.state2=dummy;
- tran.addNext(dummy);
- tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- dummy.addNext(tran);
- elementList.add(dummy);
- elementList.add(tran);
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+dummy.getName()+"."+ae.securityPattern.name,ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
- signalAuthDestMap.put(ae.securityPattern.name, authDest);
- }
- else if (ae.securityPattern.type.equals("Asymmetric Encryption")){
- AvatarMethod adecrypt = new AvatarMethod("adecrypt", ae);
-
- if (!ae.securityPattern.key.isEmpty()){
- //Decrypting key
- block.addAttribute(new AvatarAttribute("encryptedKey_"+ae.securityPattern.key,AvatarType.INTEGER,block,null));
- block.addAttribute(new AvatarAttribute("privKey_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
- block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.key, AvatarType.INTEGER, block,null));
-
- adecrypt.addParameter(block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key));
- adecrypt.addParameter(block.getAvatarAttributeWithName("privKey_"+ae.securityPattern.name));
- adecrypt.addReturnParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.key));
-
- if (block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key)!=null && block.getAvatarAttributeWithName("privKey_"+ae.securityPattern.name)!= null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.key)!=null){
- block.addMethod(adecrypt);
- tran.addAction("key_"+ae.securityPattern.key+" = adecrypt(encryptedKey_"+ae.securityPattern.key+", privKey_"+ae.securityPattern.name+")");
+ AvatarActionOnSignal as= new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ for (int i=0; i< aee.getNbOfParams(); i++){
+
+ if (block.getAvatarAttributeWithName(aee.getParam(i))==null){
+ //Throw Error
+ as.addValue("tmp");
+ System.out.println("Missing Attribute " + aee.getParam(i));
}
- }
- else {
- //Decrypting data
-
- //Add adecrypt method
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted",AvatarType.INTEGER,block,null));
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name,AvatarType.INTEGER,block,null));
- block.addAttribute(new AvatarAttribute("privKey_"+ae.securityPattern.name,AvatarType.INTEGER,block,null));
-
- adecrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
- adecrypt.addParameter(block.getAvatarAttributeWithName("privKey_"+ae.securityPattern.name));
- adecrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null && block.getAvatarAttributeWithName("privKey_"+ae.securityPattern.name)!= null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
- block.addMethod(adecrypt);
- tran.addAction(ae.securityPattern.name+" = adecrypt("+ae.securityPattern.name+"_encrypted, privKey_"+ae.securityPattern.name+")");
- }
- }
- //elementList.add(as);
- // elementList.add(tran);
- //as.addNext(tran);
- if (!ae.securityPattern.nonce.isEmpty()){
- block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- AvatarMethod get2 = new AvatarMethod("get2",ae);
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.nonce));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null) {
- block.addMethod(get2);
- }
+ else {
+ as.addValue(aee.getParam(i));
+ }
+ }
- tran.addAction("get2("+ae.securityPattern.name + ","+ae.securityPattern.name+",testnonce_"+ae.securityPattern.nonce+")");
- AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ","")+"_guarded", ae.getReferenceObject());
- tran.addNext(guardState);
- tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
- guardState.addNext(tran);
- tran.setGuard("testnonce_"+ae.securityPattern.nonce+"==" + ae.securityPattern.nonce);
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ elementList.add(signalState);
+ signalState.addNext(signalTran);
+ elementList.add(signalTran);
+ signalTran.addNext(as);
+ elementList.add(as);
+ as.addNext(tran);
+ elementList.add(tran);
}
- AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ","")+"_dummy", ae.getReferenceObject());
- tran.addNext(dummy);
+ else {
+ //Notify Event, I don't know how to translate this
+ AvatarRandom as = new AvatarRandom(ae.getName(), ae.getReferenceObject());
tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- dummy.addNext(tran);
- elementList.add(dummy);
- elementList.add(tran);
- ae.securityPattern.state2=dummy;
- if (ae.securityPattern.nonce.isEmpty()){
-
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+dummy.getName()+"."+ae.securityPattern.name,ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
- signalAuthDestMap.put(ae.securityPattern.name, authDest);
- }
- else {
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+dummy.getName()+"."+ae.securityPattern.name,ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
- signalAuthDestMap.put(ae.securityPattern.name, authDest);
+ as.setVariable(aee.getVariable());
+ as.setValues("0", "1");
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
}
- }
- else if (ae.securityPattern.type.equals("MAC")){
- AvatarMethod get2 = new AvatarMethod("get2",ae);
- AvatarAttribute mac= new AvatarAttribute(ae.securityPattern.name+"_mac", AvatarType.INTEGER, block, null);
- block.addAttribute(mac);
-
- // AvatarAttribute msg= new AvatarAttribute(ae.securityPattern.name+"_msg");
-
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(mac);
- block.addMethod(get2);
-
- tran.addAction("get2("+ae.securityPattern.name+"_encrypted,"+ae.securityPattern.name+","+ae.securityPattern.name+"_mac)");
-
- AvatarMethod verifymac = new AvatarMethod("verifyMAC", ae);
- block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.name, AvatarType.BOOLEAN, block, null));
- verifymac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- verifymac.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
- verifymac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_mac"));
- verifymac.addReturnParameter(block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.name));
-
- if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null){
- block.addMethod(verifymac);
- }
+ }
+ else if (ae instanceof TMLActivityElementWithAction){
+ //Might be encrypt or decrypt
+ AvatarState as = new AvatarState(ae.getValue().replaceAll(" ","")+"_"+ae.getName().replaceAll(" ",""), ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
+ if (security && ae.securityPattern!=null){
+ //If encryption
+ if (ae.securityPattern!=null && ae.getName().contains("encrypt")){
+ secPatterns.add(ae.securityPattern);
+ if (ae.securityPattern.type.equals("Advanced")){
+ //Type Advanced
+ tran.addAction(ae.securityPattern.formula);
+ }
+ else if (ae.securityPattern.type.equals("Symmetric Encryption")){
+ //Type Symmetric Encryption
+ if (!ae.securityPattern.nonce.isEmpty()){
+ //Concatenate nonce to data
+
+ //Create concat2 method
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+
+ AvatarMethod concat2 = new AvatarMethod("concat2",ae);
+ concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
+ concat2.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) !=null && block.getAvatarAttributeWithName(ae.securityPattern.nonce)!=null){
+ block.addMethod(concat2);
+ tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name + ","+ae.securityPattern.nonce+")");
+ }
+ }
+ if (!ae.securityPattern.key.isEmpty()){
+ //Securing a key
+
+ //Create sencrypt method for key
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.key, AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute("encryptedKey_"+ae.securityPattern.key, AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
+
+ AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae);
+ sencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.key));
+ sencrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
+ sencrypt.addReturnParameter(block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key));
+
+ if (block.getAvatarAttributeWithName(ae.securityPattern.key)!=null && block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null){
+ block.addMethod(sencrypt);
+ tran.addAction("encryptedKey_"+ ae.securityPattern.key + " = sencrypt(key_"+ae.securityPattern.key+", key_"+ae.securityPattern.name+")");
+ }
+ }
+ else {
+ //Securing data
- tran.addAction("testnonce_"+ae.securityPattern.name+"=verifyMAC("+ae.securityPattern.name+", key_"+ae.securityPattern.name+","+ae.securityPattern.name+"_mac)");
- if (!ae.securityPattern.nonce.isEmpty()){
- block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- tran.addAction("get2("+ae.securityPattern.name + ","+ae.securityPattern.name+",testnonce_"+ae.securityPattern.nonce+")");
- }
- //elementList.add(as);
- //elementList.add(tran);
+ //Create sencrypt method for data
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
- //as.addNext(tran);
- AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ","")+"_guarded", ae.getReferenceObject());
- tran.addNext(guardState);
+ AvatarMethod sencrypt = new AvatarMethod("sencrypt", ae);
+ sencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ sencrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
+ sencrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null){
+ block.addMethod(sencrypt);
+ }
+ tran.addAction(ae.securityPattern.name+"_encrypted = sencrypt("+ae.securityPattern.name+", key_"+ae.securityPattern.name+")");
+ }
+ //Set as origin for authenticity
+ ae.securityPattern.originTask=block.getName();
+ ae.securityPattern.state1=as;
+ }
+ else if (ae.securityPattern.type.equals("Asymmetric Encryption")){
+ if (!ae.securityPattern.nonce.isEmpty()){
+ //Concatenating a nonce
+ //Add concat2 method
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ AvatarMethod concat2 = new AvatarMethod("concat2",ae);
+ concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) !=null && block.getAvatarAttributeWithName(ae.securityPattern.nonce)!=null){
+ block.addMethod(concat2);
+ tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name + ","+ae.securityPattern.nonce+")");
+ }
+ }
+ //Securing a key instead of data
+ if (!ae.securityPattern.key.isEmpty()){
+ //Add aencrypt method
+ AvatarMethod aencrypt = new AvatarMethod("aencrypt", ae);
+ block.addAttribute(new AvatarAttribute("encryptedKey_"+ae.securityPattern.key, AvatarType.INTEGER, block,null));
+ aencrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.key));
+ aencrypt.addParameter(block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name));
+ aencrypt.addReturnParameter(block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key));
+ if (block.getAvatarAttributeWithName("key_"+ae.securityPattern.key)!=null && block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key)!=null){
+ block.addMethod(aencrypt);
+ tran.addAction("encryptedKey_"+ ae.securityPattern.key + " = aencrypt(key_"+ae.securityPattern.key+", pubKey_"+ae.securityPattern.name+")");
+ }
+ }
+ else {
+ //Securing data
+
+ //Add aencrypt method
+ AvatarMethod aencrypt = new AvatarMethod("aencrypt", ae);
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("pubKey_"+ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
+ aencrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ aencrypt.addParameter(block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name));
+ aencrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
+ if (block.getAvatarAttributeWithName("pubKey_"+ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null){
+ block.addMethod(aencrypt);
+ tran.addAction(ae.securityPattern.name+"_encrypted = aencrypt("+ae.securityPattern.name+", pubKey_"+ae.securityPattern.name+")");
+ }
+ }
+ //Set as origin state for authenticity
+ ae.securityPattern.originTask=block.getName();
+ ae.securityPattern.state1=as;
+ }
+ else if (ae.securityPattern.type.equals("Nonce")){
+ //Create a nonce by a random function
+ AvatarRandom arandom = new AvatarRandom("randomnonce",ae.getReferenceObject());
+ arandom.setVariable(ae.securityPattern.name);
+ arandom.setValues("0","10");
+ elementList.add(arandom);
+ tran.addNext(arandom);
+ tran = new AvatarTransition(block, "__afterrandom_"+ae.getName(), ae.getReferenceObject());
+ arandom.addNext(tran);
+ elementList.add(tran);
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ }
+ else if (ae.securityPattern.type.equals("Hash")){
+ AvatarMethod hash = new AvatarMethod("hash", ae);
+ hash.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
+ block.addMethod(hash);
+ }
+ tran.addAction(ae.securityPattern.name+"_encrypted = hash("+ae.securityPattern.name+")");
+ }
+ else if (ae.securityPattern.type.equals("MAC")){
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null)); //msg + mac(msg)
+ if (!ae.securityPattern.nonce.isEmpty()){
+ //Add nonce
+
+ //Add concat2 method
+ AvatarMethod concat = new AvatarMethod("concat2", ae);
+ concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
+ concat.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) !=null && block.getAvatarAttributeWithName(ae.securityPattern.nonce)!=null){
+ block.addMethod(concat);
+ tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name+","+ae.securityPattern.nonce+")");
+ }
+ }
- tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
-
+ //Create MAC method
+ AvatarMethod mac = new AvatarMethod("MAC", ae);
+ AvatarAttribute macattr = new AvatarAttribute(ae.securityPattern.name +"_mac", AvatarType.INTEGER, block, null);
+ block.addAttribute(macattr);
- elementList.add(guardState);
- elementList.add(tran);
- guardState.addNext(tran);
- if (!ae.securityPattern.nonce.isEmpty()){
-
- //Add extra state and transition
- tran.setGuard("testnonce_"+ae.securityPattern.nonce+"==" + ae.securityPattern.nonce);
- AvatarState guardState2 = new AvatarState(ae.getName().replaceAll(" ","")+"_guarded2", ae.getReferenceObject());
- tran.addNext(guardState2);
- tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
- elementList.add(guardState2);
- elementList.add(tran);
+
- guardState2.addNext(tran);
- }
- tran.setGuard("testnonce_"+ae.securityPattern.name);
- }
- AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ","")+"_dummy", ae.getReferenceObject());
- ae.securityPattern.state2=dummy;
- tran.addNext(dummy);
- elementList.add(tran);
- tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- dummy.addNext(tran);
- elementList.add(dummy);
- elementList.add(tran);
+ mac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ mac.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
+ mac.addReturnParameter(macattr);
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+dummy.getName()+"."+ae.securityPattern.name,ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
- signalAuthDestMap.put(ae.securityPattern.name, authDest);
-
- //Can't decrypt hash or nonce
- }
- }
- else {
- //Translate state without security
- }
- }
- else if (ae instanceof TMLActivityElementWithIntervalAction){
- AvatarState as = new AvatarState(ae.getName().replaceAll(" ",""), ae.getReferenceObject());
- tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- as.addNext(tran);
- elementList.add(as);
- elementList.add(tran);
- }
- else if (ae instanceof TMLActivityElementChannel){
- TMLActivityElementChannel aec = (TMLActivityElementChannel) ae;
- TMLChannel ch = aec.getChannel(0);
- AvatarSignal sig;
- boolean checkAcc=false;
- if (ae.getReferenceObject()!=null){
- checkAcc=((TGComponent)ae.getReferenceObject()).getCheckableAccessibility();
- }
- AvatarState signalState = new AvatarState("signalstate_"+ae.getName().replaceAll(" ","")+"_"+ch.getName(),ae.getReferenceObject(), checkAcc);
- AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_"+ae.getName()+"_"+ch.getName(), ae.getReferenceObject());
- if (ae instanceof TMLReadChannel){
- //Create signal if it does not already exist
- if (!signalInMap.containsKey(ch.getName())){
- sig = new AvatarSignal(getName(ch.getName()), AvatarSignal.IN, ch.getReferenceObject());
- signals.add(sig);
- signalInMap.put(ch.getName(), sig);
- block.addSignal(sig);
- AvatarAttribute channelData= new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null);
- if (block.getAvatarAttributeWithName(getName(ch.getName())+"_chData")==null){
- block.addAttribute(channelData);
- }
- sig.addParameter(channelData);
- }
- else {
- sig=signalInMap.get(ch.getName());
- }
- AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
-
- if (ae.securityPattern!=null){
- //If nonce
- if (ae.securityPattern.type.equals("Nonce")){
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
- as.addValue(ae.securityPattern.name);
- }
- //Send the encrypted key
- else if (!ae.securityPattern.key.isEmpty()){
- as.addValue("encryptedKey_"+ae.securityPattern.key);
- AvatarAttribute data= new AvatarAttribute("encryptedKey_"+ae.securityPattern.key, AvatarType.INTEGER, block, null);
- block.addAttribute(data);
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null){
+ block.addMethod(mac);
+ tran.addAction(ae.securityPattern.name+"_mac = MAC("+ae.securityPattern.name+",key_"+ae.securityPattern.name+")");
+ }
+
+ //Concatenate msg and mac(msg)
+
+ //Create concat2 method
+ AvatarMethod concat = new AvatarMethod("concat2", ae);
+ concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_mac"));
+ concat.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
+ //concat.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null){
+ block.addMethod(concat);
+ tran.addAction(ae.securityPattern.name+"_encrypted = concat2("+ae.securityPattern.name +","+ae.securityPattern.name+"_mac)");
+ }
+ ae.securityPattern.originTask=block.getName();
+ ae.securityPattern.state1=as;
+ }
+ //Set attributestate for authenticity
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
+ AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName()+"."+as.getName()+"."+ae.securityPattern.name,ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), as);
+ signalAuthOriginMap.put(ae.securityPattern.name, authOrigin);
+ }
+
+ }
+ else if (ae.securityPattern!=null && ae.getName().contains("decrypt")){
+ //Decryption action
+ //block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ //block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
+ if (ae.securityPattern.type.equals("Symmetric Encryption")){
+ if (!ae.securityPattern.key.isEmpty()){
+ //Decrypting a key
+ //Add sdecrypt method
+ AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae);
+ block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.key, AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute("encryptedKey_"+ae.securityPattern.key, AvatarType.INTEGER, block,null));
+
+ sdecrypt.addParameter(block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key));
+ sdecrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
+ sdecrypt.addReturnParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.key));
+ if (block.getAvatarAttributeWithName("key_"+ae.securityPattern.key)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key)!=null){
+ block.addMethod(sdecrypt);
+ tran.addAction("key_"+ae.securityPattern.key+" = sdecrypt(encryptedKey_"+ae.securityPattern.key+", key_"+ae.securityPattern.name+")");
+ }
+ }
+ else {
+ //Decrypting data
+ AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae);
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block,null));
+
+ sdecrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
+ sdecrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
+ sdecrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
+ block.addMethod(sdecrypt);
+ tran.addAction(ae.securityPattern.name+" = sdecrypt("+ae.securityPattern.name+"_encrypted, key_"+ae.securityPattern.name+")");
+ }
+ }
+ if (!ae.securityPattern.nonce.isEmpty()){
+ //Separate out the nonce
+ block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ //Add get2 method
+ AvatarMethod get2 = new AvatarMethod("get2",ae);
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.nonce));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.nonce)!=null) {
+ block.addMethod(get2);
+ tran.addAction("get2("+ae.securityPattern.name + ","+ae.securityPattern.name+",testnonce_"+ae.securityPattern.nonce+")");
+ }
+
+ //Add state after get2 statement
+ AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ","")+"_guarded", ae.getReferenceObject());
+ tran.addNext(guardState);
+ tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
+ guardState.addNext(tran);
+ elementList.add(guardState);
+ elementList.add(tran);
+
+ //Guard transition to determine if nonce matches
+ tran.setGuard("testnonce_"+ae.securityPattern.nonce+"==" + ae.securityPattern.nonce);
+ }
+ //Add a dummy state afterwards for authenticity after decrypting the data
+ AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ","")+"_dummy", ae.getReferenceObject());
+ ae.securityPattern.state2=dummy;
+ tran.addNext(dummy);
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ dummy.addNext(tran);
+ elementList.add(dummy);
+ elementList.add(tran);
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
+ AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+dummy.getName()+"."+ae.securityPattern.name,ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
+ signalAuthDestMap.put(ae.securityPattern.name, authDest);
+ }
+ }
+ else if (ae.securityPattern.type.equals("Asymmetric Encryption")){
+ AvatarMethod adecrypt = new AvatarMethod("adecrypt", ae);
+
+ if (!ae.securityPattern.key.isEmpty()){
+ //Decrypting key
+
+
+ //Add adecrypt method
+ block.addAttribute(new AvatarAttribute("encryptedKey_"+ae.securityPattern.key,AvatarType.INTEGER,block,null));
+ block.addAttribute(new AvatarAttribute("privKey_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute("key_"+ae.securityPattern.key, AvatarType.INTEGER, block,null));
+
+ adecrypt.addParameter(block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key));
+ adecrypt.addParameter(block.getAvatarAttributeWithName("privKey_"+ae.securityPattern.name));
+ adecrypt.addReturnParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.key));
+
+ if (block.getAvatarAttributeWithName("encryptedKey_"+ae.securityPattern.key)!=null && block.getAvatarAttributeWithName("privKey_"+ae.securityPattern.name)!= null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.key)!=null){
+ block.addMethod(adecrypt);
+ tran.addAction("key_"+ae.securityPattern.key+" = adecrypt(encryptedKey_"+ae.securityPattern.key+", privKey_"+ae.securityPattern.name+")");
+ }
+ }
+ else {
+ //Decrypting data
+
+ //Add adecrypt method
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted",AvatarType.INTEGER,block,null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name,AvatarType.INTEGER,block,null));
+ block.addAttribute(new AvatarAttribute("privKey_"+ae.securityPattern.name,AvatarType.INTEGER,block,null));
+
+ adecrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
+ adecrypt.addParameter(block.getAvatarAttributeWithName("privKey_"+ae.securityPattern.name));
+ adecrypt.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null && block.getAvatarAttributeWithName("privKey_"+ae.securityPattern.name)!= null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
+ block.addMethod(adecrypt);
+ tran.addAction(ae.securityPattern.name+" = adecrypt("+ae.securityPattern.name+"_encrypted, privKey_"+ae.securityPattern.name+")");
+ }
+ }
+ if (!ae.securityPattern.nonce.isEmpty()){
+ block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ AvatarMethod get2 = new AvatarMethod("get2",ae);
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.nonce));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null) {
+ block.addMethod(get2);
+ }
+
+ tran.addAction("get2("+ae.securityPattern.name + ","+ae.securityPattern.name+",testnonce_"+ae.securityPattern.nonce+")");
+ AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ","")+"_guarded", ae.getReferenceObject());
+ tran.addNext(guardState);
+ tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
+ elementList.add(guardState);
+ elementList.add(tran);
+ guardState.addNext(tran);
+ tran.setGuard("testnonce_"+ae.securityPattern.nonce+"==" + ae.securityPattern.nonce);
+ }
+ AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ","")+"_dummy", ae.getReferenceObject());
+ tran.addNext(dummy);
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ dummy.addNext(tran);
+ elementList.add(dummy);
+ elementList.add(tran);
+ ae.securityPattern.state2=dummy;
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
+ AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+dummy.getName()+"."+ae.securityPattern.name,ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
+ signalAuthDestMap.put(ae.securityPattern.name, authDest);
+ }
+ }
+ else if (ae.securityPattern.type.equals("MAC")){
+ //Separate MAC from MSG
+
+ //Add get2 method
+ AvatarMethod get2 = new AvatarMethod("get2",ae);
+ AvatarAttribute mac= new AvatarAttribute(ae.securityPattern.name+"_mac", AvatarType.INTEGER, block, null);
+ block.addAttribute(mac);
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted",AvatarType.INTEGER,block,null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name,AvatarType.INTEGER,block,null));
+
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(mac);
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null){
+ block.addMethod(get2);
+ tran.addAction("get2("+ae.securityPattern.name+"_encrypted,"+ae.securityPattern.name+","+ae.securityPattern.name+"_mac)");
+ }
+
+ //Add verifymac method
+ AvatarMethod verifymac = new AvatarMethod("verifyMAC", ae);
+ block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.name, AvatarType.BOOLEAN, block, null));
+
+ verifymac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ verifymac.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
+ verifymac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_mac"));
+ verifymac.addReturnParameter(block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.name));
+
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null){
+ block.addMethod(verifymac);
+ tran.addAction("testnonce_"+ae.securityPattern.name+"=verifyMAC("+ae.securityPattern.name+", key_"+ae.securityPattern.name+","+ae.securityPattern.name+"_mac)");
+
+ }
+
+
+ if (!ae.securityPattern.nonce.isEmpty()){
+ block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ tran.addAction("get2("+ae.securityPattern.name + ","+ae.securityPattern.name+",testnonce_"+ae.securityPattern.nonce+")");
+ }
+
+ AvatarState guardState = new AvatarState(ae.getName().replaceAll(" ","")+"_guarded", ae.getReferenceObject());
+ tran.addNext(guardState);
+ tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
+ elementList.add(guardState);
+ elementList.add(tran);
+ guardState.addNext(tran);
+ tran.setGuard("testnonce_"+ae.securityPattern.name);
+
+ if (!ae.securityPattern.nonce.isEmpty()){
+
+ //Add extra state and transition
+
+ AvatarState guardState2 = new AvatarState(ae.getName().replaceAll(" ","")+"_guarded2", ae.getReferenceObject());
+ tran.addNext(guardState2);
+ tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
+ tran.setGuard("testnonce_"+ae.securityPattern.nonce+"==" + ae.securityPattern.nonce);
+ elementList.add(guardState2);
+ elementList.add(tran);
+
+ guardState2.addNext(tran);
+ }
+ AvatarState dummy = new AvatarState(ae.getName().replaceAll(" ","")+"_dummy", ae.getReferenceObject());
+ ae.securityPattern.state2=dummy;
+ tran.addNext(dummy);
+ elementList.add(tran);
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ dummy.addNext(tran);
+ elementList.add(dummy);
+ elementList.add(tran);
+
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null){
+ AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+dummy.getName()+"."+ae.securityPattern.name,ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
+ signalAuthDestMap.put(ae.securityPattern.name, authDest);
+ }
+ }
+
+
+ //Can't decrypt hash or nonce
+ }
}
else {
- //Send the encrypted data
- if (!secChannelMap.containsKey(ae.securityPattern.name)){
- List<String> tmp=new ArrayList<String>();
- secChannelMap.put(ae.securityPattern.name,tmp);
- }
- secChannelMap.get(ae.securityPattern.name).add(ch.getName());
- as.addValue(ae.securityPattern.name+"_encrypted");
- AvatarAttribute data= new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(data);
+ //Translate state without security
}
}
- else {
- as.addValue(getName(ch.getName())+"_chData");
+ else if (ae instanceof TMLActivityElementWithIntervalAction){
+ AvatarState as = new AvatarState(ae.getName().replaceAll(" ",""), ae.getReferenceObject());
+ tran = new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
}
+ else if (ae instanceof TMLActivityElementChannel){
+ TMLActivityElementChannel aec = (TMLActivityElementChannel) ae;
+ TMLChannel ch = aec.getChannel(0);
+ AvatarSignal sig;
+ boolean checkAcc=false;
+ if (ae.getReferenceObject()!=null){
+ checkAcc=((TGComponent)ae.getReferenceObject()).getCheckableAccessibility();
+ }
+ AvatarState signalState = new AvatarState("signalstate_"+ae.getName().replaceAll(" ","")+"_"+ch.getName(),ae.getReferenceObject(), checkAcc);
+ AvatarTransition signalTran = new AvatarTransition(block, "__after_signalstate_"+ae.getName()+"_"+ch.getName(), ae.getReferenceObject());
+ if (ae instanceof TMLReadChannel){
+ //Create signal if it does not already exist
+ if (!signalInMap.containsKey(ch.getName())){
+ sig = new AvatarSignal(getName(ch.getName()), AvatarSignal.IN, ch.getReferenceObject());
+ signals.add(sig);
+ signalInMap.put(ch.getName(), sig);
+ block.addSignal(sig);
+ AvatarAttribute channelData= new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null);
+ if (block.getAvatarAttributeWithName(getName(ch.getName())+"_chData")==null){
+ block.addAttribute(channelData);
+ }
+ sig.addParameter(channelData);
+ }
+ else {
+ sig=signalInMap.get(ch.getName());
+ }
+ AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
- tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- elementList.add(signalState);
- signalState.addNext(signalTran);
- elementList.add(signalTran);
- signalTran.addNext(as);
- as.addNext(tran);
- elementList.add(as);
- elementList.add(tran);
- if (ch.checkAuth){
- //Add aftersignal state
- AvatarState afterSignalState = new AvatarState("aftersignalstate_"+ae.getName().replaceAll(" ","")+"_"+ch.getName(),ae.getReferenceObject());
- tran.addNext(afterSignalState);
- tran = new AvatarTransition(block, "__aftersignalstate_"+ae.getName(), ae.getReferenceObject());
- afterSignalState.addNext(tran);
- elementList.add(afterSignalState);
- elementList.add(tran);
- if (block.getAvatarAttributeWithName(getName(ch.getName())+"_chData")==null){
- AvatarAttribute channelData= new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null);
- block.addAttribute(channelData);
- }
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+afterSignalState.getName()+"."+getName(ch.getName())+"_chData",ae.getReferenceObject(),block.getAvatarAttributeWithName(getName(ch.getName())+"_chData"), afterSignalState);
- signalAuthDestMap.put(ch.getName(), authDest);
- }
+ if (ae.securityPattern!=null){
+ //If nonce
+ if (ae.securityPattern.type.equals("Nonce")){
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
+ as.addValue(ae.securityPattern.name);
+ }
+ //Send the encrypted key
+ else if (!ae.securityPattern.key.isEmpty()){
+ as.addValue("encryptedKey_"+ae.securityPattern.key);
+ AvatarAttribute data= new AvatarAttribute("encryptedKey_"+ae.securityPattern.key, AvatarType.INTEGER, block, null);
+ block.addAttribute(data);
+ }
+ else {
+ //Send the encrypted data
+ if (!secChannelMap.containsKey(ae.securityPattern.name)){
+ List<String> tmp=new ArrayList<String>();
+ secChannelMap.put(ae.securityPattern.name,tmp);
+ }
+ secChannelMap.get(ae.securityPattern.name).add(ch.getName());
+ as.addValue(ae.securityPattern.name+"_encrypted");
+ AvatarAttribute data= new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
+ block.addAttribute(data);
+ }
+ }
+ else {
+ as.addValue(getName(ch.getName())+"_chData");
+ }
- }
- else {
- //WriteChannel
-
- if (!signalOutMap.containsKey(ch.getName())){
- //Add signal if it does not exist
- sig = new AvatarSignal(getName(ch.getName()), AvatarSignal.OUT, ch.getReferenceObject());
- signals.add(sig);
- block.addSignal(sig);
- signalOutMap.put(ch.getName(), sig);
- AvatarAttribute channelData= new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null);
- if (block.getAvatarAttributeWithName(getName(ch.getName())+"_chData")==null){
- block.addAttribute(channelData);
- }
- sig.addParameter(channelData);
- }
- else {
- sig=signalOutMap.get(ch.getName());
- }
- if (ch.checkConf){
- if (!attrsToCheck.contains(getName(ch.getName())+"_chData")){
- AvatarAttribute attr = block.getAvatarAttributeWithName(getName(ch.getName())+"_chData");
- if (attr != null)
- {
- attrsToCheck.add(getName(ch.getName())+"_chData");
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ch.getName()+"_chData", ch.getReferenceObject(), attr));
- }
- }
- }
- if (ch.checkAuth){
- if (block.getAvatarAttributeWithName(getName(ch.getName())+"_chData")==null){
- AvatarAttribute channelData= new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null);
- block.addAttribute(channelData);
- }
- AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName()+"."+signalState.getName()+"."+getName(ch.getName())+"_chData",ae.getReferenceObject(),block.getAvatarAttributeWithName(getName(ch.getName())+"_chData"), signalState);
- signalAuthOriginMap.put(ch.getName(), authOrigin);
- }
- AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ elementList.add(signalState);
+ signalState.addNext(signalTran);
+ elementList.add(signalTran);
+ signalTran.addNext(as);
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
+ if (ch.checkAuth){
+ //Add aftersignal state
+ AvatarState afterSignalState = new AvatarState("aftersignalstate_"+ae.getName().replaceAll(" ","")+"_"+ch.getName(),ae.getReferenceObject());
+ tran.addNext(afterSignalState);
+ tran = new AvatarTransition(block, "__aftersignalstate_"+ae.getName(), ae.getReferenceObject());
+ afterSignalState.addNext(tran);
+ elementList.add(afterSignalState);
+ elementList.add(tran);
+ if (block.getAvatarAttributeWithName(getName(ch.getName())+"_chData")==null){
+ AvatarAttribute channelData= new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null);
+ block.addAttribute(channelData);
+ }
+ AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+afterSignalState.getName()+"."+getName(ch.getName())+"_chData",ae.getReferenceObject(),block.getAvatarAttributeWithName(getName(ch.getName())+"_chData"), afterSignalState);
+ signalAuthDestMap.put(ch.getName(), authDest);
+ }
- if (ae.securityPattern!=null){
- //send nonce
- if (ae.securityPattern.type.equals("Nonce")){
- as.addValue(ae.securityPattern.name);
- }
- //send encrypted key
- else if (!ae.securityPattern.key.isEmpty()){
- as.addValue("encryptedKey_"+ae.securityPattern.key);
- AvatarAttribute data= new AvatarAttribute("encryptedKey_"+ae.securityPattern.key, AvatarType.INTEGER, block, null);
- block.addAttribute(data);
}
else {
- //send encrypted data
- as.addValue(ae.securityPattern.name+"_encrypted");
- AvatarAttribute data= new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(data);
- if (!secChannelMap.containsKey(ae.securityPattern.name)){
- List<String> tmp=new ArrayList<String>();
- secChannelMap.put(ae.securityPattern.name,tmp);
- }
- secChannelMap.get(ae.securityPattern.name).add(ch.getName());
+ //WriteChannel
+
+ if (!signalOutMap.containsKey(ch.getName())){
+ //Add signal if it does not exist
+ sig = new AvatarSignal(getName(ch.getName()), AvatarSignal.OUT, ch.getReferenceObject());
+ signals.add(sig);
+ block.addSignal(sig);
+ signalOutMap.put(ch.getName(), sig);
+ AvatarAttribute channelData= new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null);
+ if (block.getAvatarAttributeWithName(getName(ch.getName())+"_chData")==null){
+ block.addAttribute(channelData);
+ }
+ sig.addParameter(channelData);
+ }
+ else {
+ sig=signalOutMap.get(ch.getName());
+ }
+ //Add the confidentiality pragma for this channel data
+ if (ch.checkConf){
+ if (!attrsToCheck.contains(getName(ch.getName())+"_chData")){
+ AvatarAttribute attr = block.getAvatarAttributeWithName(getName(ch.getName())+"_chData");
+ if (attr != null)
+ {
+ attrsToCheck.add(getName(ch.getName())+"_chData");
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ch.getName()+"_chData", ch.getReferenceObject(), attr));
+ }
+ }
+ }
+ //Add the authenticity pragma for this channel data
+ if (ch.checkAuth){
+ if (block.getAvatarAttributeWithName(getName(ch.getName())+"_chData")==null){
+ AvatarAttribute channelData= new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null);
+ block.addAttribute(channelData);
+ }
+ AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName()+"."+signalState.getName()+"."+getName(ch.getName())+"_chData",ae.getReferenceObject(),block.getAvatarAttributeWithName(getName(ch.getName())+"_chData"), signalState);
+ signalAuthOriginMap.put(ch.getName(), authOrigin);
+ }
+ AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
+
+ if (ae.securityPattern!=null){
+ //send nonce
+ if (ae.securityPattern.type.equals("Nonce")){
+ as.addValue(ae.securityPattern.name);
+ }
+ //send encrypted key
+ else if (!ae.securityPattern.key.isEmpty()){
+ as.addValue("encryptedKey_"+ae.securityPattern.key);
+ AvatarAttribute data= new AvatarAttribute("encryptedKey_"+ae.securityPattern.key, AvatarType.INTEGER, block, null);
+ block.addAttribute(data);
+ }
+ else {
+ //send encrypted data
+ as.addValue(ae.securityPattern.name+"_encrypted");
+ AvatarAttribute data= new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
+ block.addAttribute(data);
+ if (!secChannelMap.containsKey(ae.securityPattern.name)){
+ List<String> tmp=new ArrayList<String>();
+ secChannelMap.put(ae.securityPattern.name,tmp);
+ }
+ secChannelMap.get(ae.securityPattern.name).add(ch.getName());
+ }
+ }
+ else {
+ //No security pattern
+ System.out.println("no security pattern for " + ch.getName());
+ as.addValue(getName(ch.getName())+"_chData");
+ }
+
+ tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
+ elementList.add(signalState);
+ signalState.addNext(signalTran);
+ elementList.add(signalTran);
+ signalTran.addNext(as);
+ as.addNext(tran);
+ elementList.add(as);
+ elementList.add(tran);
+ }
+ }
+ else if (ae instanceof TMLForLoop){
+ TMLForLoop loop = (TMLForLoop)ae;
+ if (loop.isInfinite()){
+ //Make initializaton, then choice state with transitions
+ List<AvatarStateMachineElement> elements=translateState(ae.getNextElement(0), block);
+ /*List<AvatarStateMachineElement> afterloop =*/ translateState(ae.getNextElement(1), block);
+ AvatarState initState = new AvatarState(ae.getName().replaceAll(" ","")+"__init", ae.getReferenceObject());
+ elementList.add(initState);
+ //Build transition to choice
+ tran = new AvatarTransition(block, "loop_init__"+ae.getName(), ae.getReferenceObject());
+ tran.addAction(AvatarTerm.createActionFromString(block, "loop_index=0"));
+ elementList.add(tran);
+ initState.addNext(tran);
+ //Choice state
+ AvatarState as = new AvatarState(ae.getName().replaceAll(" ","")+"__choice", ae.getReferenceObject());
+ elementList.add(as);
+ tran.addNext(as);
+ //transition to first element of loop
+ tran = new AvatarTransition(block, "loop_increment__"+ae.getName(), ae.getReferenceObject());
+ //Set default loop limit guard
+ tran.setGuard(AvatarGuard.createFromString(block, "loop_index != "+loopLimit));
+ tran.addAction(AvatarTerm.createActionFromString(block, "loop_index = loop_index + 1"));
+ tran.addNext(elements.get(0));
+ as.addNext(tran);
+ elementList.add(tran);
+ //Process elements in loop to remove stop states and empty transitions, and loop back to choice
+ for (AvatarStateMachineElement e: elements){
+ if (e instanceof AvatarStopState){
+ }
+ else if (e.getNexts().size()==0){
+ if (e instanceof AvatarTransition){
+ e.addNext(as);
+ elementList.add(e);
+ }
+ }
+ else if (e.getNext(0) instanceof AvatarStopState){
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(as);
+ elementList.add(e);
+ }
+ else {
+ elementList.add(e);
+ }
+ }
+
+ //Transition if exiting loop
+ tran=new AvatarTransition(block, "end_loop__"+ae.getName(), ae.getReferenceObject());
+ tran.setGuard(new AvatarGuardElse());
+ as.addNext(tran);
+ AvatarStopState stop = new AvatarStopState("stop", null);
+ tran.addNext(stop);
+ elementList.add(tran);
+ elementList.add(stop);
+ return elementList;
}
- }
- else {
- //No security pattern
- System.out.println("no security pattern for " + ch.getName());
- as.addValue(getName(ch.getName())+"_chData");
- }
+ else {
+ //Make initializaton, then choice state with transitions
+ List<AvatarStateMachineElement> elements=translateState(ae.getNextElement(0), block);
+ List<AvatarStateMachineElement> afterloop = translateState(ae.getNextElement(1), block);
+ AvatarState initState = new AvatarState(ae.getName().replaceAll(" ","")+"__init", ae.getReferenceObject());
+ elementList.add(initState);
+ //Build transition to choice
+ tran = new AvatarTransition(block, "loop_init__"+ae.getName(), ae.getReferenceObject());
+ tran.addAction(AvatarTerm.createActionFromString(block, loop.getInit()));
+ tran.addAction(AvatarTerm.createActionFromString(block, "loop_index=0"));
+ elementList.add(tran);
+ initState.addNext(tran);
+ //Choice state
+ AvatarState as = new AvatarState(ae.getName().replaceAll(" ","")+"__choice", ae.getReferenceObject());
+ elementList.add(as);
+ tran.addNext(as);
+ //transition to first element of loop
+ tran = new AvatarTransition(block, "loop_increment__"+ae.getName(), ae.getReferenceObject());
+ //Set default loop limit guard
+ tran.setGuard(AvatarGuard.createFromString(block, "loop_index != "+loopLimit));
+ /*AvatarGuard guard = */AvatarGuard.createFromString (block, loop.getCondition().replaceAll("<", "!="));
+ int error = AvatarSyntaxChecker.isAValidGuard(avspec, block, loop.getCondition().replaceAll("<","!="));
+ if (error != 0) {
+ tran.addGuard(loop.getCondition().replaceAll("<", "!="));
+ }
+ tran.addAction(AvatarTerm.createActionFromString(block, loop.getIncrement()));
+ tran.addAction(AvatarTerm.createActionFromString(block, "loop_index = loop_index + 1"));
+ if (elements.size()>0){
+ tran.addNext(elements.get(0));
+ as.addNext(tran);
+ elementList.add(tran);
+ }
+ //Process elements in loop to remove stop states and empty transitions, and loop back to choice
+ for (AvatarStateMachineElement e: elements){
+ if (e instanceof AvatarStopState){
+ }
+ else if (e.getNexts().size()==0){
+ e.addNext(as);
+ elementList.add(e);
+ }
+ else if (e.getNext(0) instanceof AvatarStopState){
+ //Remove the transition to AvatarStopState
+ e.removeNext(0);
+ e.addNext(as);
+ elementList.add(e);
+ }
+ else {
+ elementList.add(e);
+ }
+ }
- tran= new AvatarTransition(block, "__after_"+ae.getName(), ae.getReferenceObject());
- elementList.add(signalState);
- signalState.addNext(signalTran);
- elementList.add(signalTran);
- signalTran.addNext(as);
- as.addNext(tran);
- elementList.add(as);
- elementList.add(tran);
- }
- }
- else if (ae instanceof TMLForLoop){
- TMLForLoop loop = (TMLForLoop)ae;
- if (loop.isInfinite()){
- //Make initializaton, then choice state with transitions
- List<AvatarStateMachineElement> elements=translateState(ae.getNextElement(0), block);
- /*List<AvatarStateMachineElement> afterloop =*/ translateState(ae.getNextElement(1), block);
- AvatarState initState = new AvatarState(ae.getName().replaceAll(" ","")+"__init", ae.getReferenceObject());
- elementList.add(initState);
- //Build transition to choice
- tran = new AvatarTransition(block, "loop_init__"+ae.getName(), ae.getReferenceObject());
- tran.addAction(AvatarTerm.createActionFromString(block, "loop_index=0"));
- elementList.add(tran);
- initState.addNext(tran);
- //Choice state
- AvatarState as = new AvatarState(ae.getName().replaceAll(" ","")+"__choice", ae.getReferenceObject());
- elementList.add(as);
- tran.addNext(as);
- //transition to first element of loop
- tran = new AvatarTransition(block, "loop_increment__"+ae.getName(), ae.getReferenceObject());
- //Set default loop limit guard
- tran.setGuard(AvatarGuard.createFromString(block, "loop_index != "+loopLimit));
- tran.addAction(AvatarTerm.createActionFromString(block, "loop_index = loop_index + 1"));
- tran.addNext(elements.get(0));
- as.addNext(tran);
- elementList.add(tran);
- //Process elements in loop to remove stop states and empty transitions, and loop back to choice
- for (AvatarStateMachineElement e: elements){
- if (e instanceof AvatarStopState){
- }
- else if (e.getNexts().size()==0){
- if (e instanceof AvatarTransition){
- e.addNext(as);
- elementList.add(e);
- }
- }
- else if (e.getNext(0) instanceof AvatarStopState){
- //Remove the transition to AvatarStopState
- e.removeNext(0);
- e.addNext(as);
- elementList.add(e);
- }
- else {
- elementList.add(e);
- }
- }
-
- //Transition if exiting loop
- tran=new AvatarTransition(block, "end_loop__"+ae.getName(), ae.getReferenceObject());
- tran.setGuard(new AvatarGuardElse());
- as.addNext(tran);
- AvatarStopState stop = new AvatarStopState("stop", null);
- tran.addNext(stop);
- elementList.add(tran);
- elementList.add(stop);
- return elementList;
- }
- else {
- //Make initializaton, then choice state with transitions
- List<AvatarStateMachineElement> elements=translateState(ae.getNextElement(0), block);
- List<AvatarStateMachineElement> afterloop = translateState(ae.getNextElement(1), block);
- AvatarState initState = new AvatarState(ae.getName().replaceAll(" ","")+"__init", ae.getReferenceObject());
- elementList.add(initState);
- //Build transition to choice
- tran = new AvatarTransition(block, "loop_init__"+ae.getName(), ae.getReferenceObject());
- tran.addAction(AvatarTerm.createActionFromString(block, loop.getInit()));
- tran.addAction(AvatarTerm.createActionFromString(block, "loop_index=0"));
- elementList.add(tran);
- initState.addNext(tran);
- //Choice state
- AvatarState as = new AvatarState(ae.getName().replaceAll(" ","")+"__choice", ae.getReferenceObject());
- elementList.add(as);
- tran.addNext(as);
- //transition to first element of loop
- tran = new AvatarTransition(block, "loop_increment__"+ae.getName(), ae.getReferenceObject());
- //Set default loop limit guard
- tran.setGuard(AvatarGuard.createFromString(block, "loop_index != "+loopLimit));
- /*AvatarGuard guard = */AvatarGuard.createFromString (block, loop.getCondition().replaceAll("<", "!="));
- int error = AvatarSyntaxChecker.isAValidGuard(avspec, block, loop.getCondition().replaceAll("<","!="));
- if (error != 0) {
- tran.addGuard(loop.getCondition().replaceAll("<", "!="));
+ //Transition if exiting loop
+ tran=new AvatarTransition(block, "end_loop__"+ae.getName(), ae.getReferenceObject());
+ tran.setGuard(new AvatarGuardElse());
+ as.addNext(tran);
+ if (afterloop.size()==0){
+ afterloop.add(new AvatarStopState("stop", null));
+ }
+ tran.addNext(afterloop.get(0));
+ elementList.add(tran);
+ elementList.addAll(afterloop);
+ return elementList;
}
- tran.addAction(AvatarTerm.createActionFromString(block, loop.getIncrement()));
- tran.addAction(AvatarTerm.createActionFromString(block, "loop_index = loop_index + 1"));
- if (elements.size()>0){
- tran.addNext(elements.get(0));
- as.addNext(tran);
- elementList.add(tran);
- }
- //Process elements in loop to remove stop states and empty transitions, and loop back to choice
- for (AvatarStateMachineElement e: elements){
- if (e instanceof AvatarStopState){
- }
- else if (e.getNexts().size()==0){
- e.addNext(as);
- elementList.add(e);
}
- else if (e.getNext(0) instanceof AvatarStopState){
- //Remove the transition to AvatarStopState
- e.removeNext(0);
- e.addNext(as);
- elementList.add(e);
+ else if (ae instanceof TMLChoice){
+ AvatarState as = new AvatarState(ae.getName().replaceAll(" ",""), ae.getReferenceObject());
+ //Make many choices
+ elementList.add(as);
+ TMLChoice c = (TMLChoice) ae;
+ for (int i=0; i<c.getNbGuard(); i++){
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae.getReferenceObject());
+ //tran.setGuard(c.getGuard(i));
+ as.addNext(tran);
+ List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(i), block);
+ if (nexts.size()>0){
+ tran.addNext(nexts.get(0));
+ elementList.add(tran);
+ elementList.addAll(nexts);
+ }
+ }
+ return elementList;
+
+ }
+ else if (ae instanceof TMLSelectEvt){
+ AvatarState as = new AvatarState(ae.getName().replaceAll(" ",""), ae.getReferenceObject());
+ elementList.add(as);
+ //Make many choices
+ //TMLSelectEvt c = (TMLSelectEvt) ae;
+ for (int i=0; i < ae.getNbNext(); i++){
+ tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae.getReferenceObject());
+ as.addNext(tran);
+ List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(i), block);
+ tran.addNext(nexts.get(0));
+ elementList.add(tran);
+ elementList.addAll(nexts);
+ }
+ return elementList;
}
else {
- elementList.add(e);
+ System.out.println("undefined tml element " + ae);
+ }
+ List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(0), block);
+ if (nexts.size()==0){
+ //in an infinite loop i hope
+ return elementList;
}
- }
-
- //Transition if exiting loop
- tran=new AvatarTransition(block, "end_loop__"+ae.getName(), ae.getReferenceObject());
- tran.setGuard(new AvatarGuardElse());
- as.addNext(tran);
- if (afterloop.size()==0){
- afterloop.add(new AvatarStopState("stop", null));
- }
- tran.addNext(afterloop.get(0));
- elementList.add(tran);
- elementList.addAll(afterloop);
- return elementList;
- }
- }
- else if (ae instanceof TMLChoice){
- AvatarState as = new AvatarState(ae.getName().replaceAll(" ",""), ae.getReferenceObject());
- //Make many choices
- elementList.add(as);
- TMLChoice c = (TMLChoice) ae;
- for (int i=0; i<c.getNbGuard(); i++){
- tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae.getReferenceObject());
- //tran.setGuard(c.getGuard(i));
- as.addNext(tran);
- List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(i), block);
- if (nexts.size()>0){
tran.addNext(nexts.get(0));
- elementList.add(tran);
elementList.addAll(nexts);
+ return elementList;
}
- }
- return elementList;
- }
- else if (ae instanceof TMLSelectEvt){
- AvatarState as = new AvatarState(ae.getName().replaceAll(" ",""), ae.getReferenceObject());
- elementList.add(as);
- //Make many choices
- //TMLSelectEvt c = (TMLSelectEvt) ae;
- for (int i=0; i < ae.getNbNext(); i++){
- tran = new AvatarTransition(block, "__after_"+ae.getName()+"_"+i, ae.getReferenceObject());
- as.addNext(tran);
- List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(i), block);
- tran.addNext(nexts.get(0));
- elementList.add(tran);
- elementList.addAll(nexts);
- }
- return elementList;
- }
- else {
- System.out.println("undefined tml element " + ae);
- }
- List<AvatarStateMachineElement> nexts = translateState(ae.getNextElement(0), block);
- if (nexts.size()==0){
- //in an infinite loop i hope
- return elementList;
- }
- tran.addNext(nexts.get(0));
- elementList.addAll(nexts);
- return elementList;
- }
+ public String processName(String name, int id){
+ name = name.replaceAll("-","_").replaceAll(" ","");
+ if (allStates.contains(name)){
+ return name+id;
- public String processName(String name, int id){
- name = name.replaceAll("-","_").replaceAll(" ","");
- if (allStates.contains(name)){
- return name+id;
-
- }
- else {
- allStates.add(name);
- return name;
- }
- }
-/* public AvatarPragma generatePragma(String[] s){
-
- }*/
-
- public String getName(String s){
- if (nameMap.containsKey(s)){
- return nameMap.get(s);
- }
- else {
- if (!s.contains("__")){
- nameMap.put(s,s);
- return s;
- }
- else if (s.split("__").length==1){
- nameMap.put(s,s.split("__")[s.split("__").length-1]);
- return s.split("__")[s.split("__").length-1];
- }
- else if (s.contains("JOIN")){
- String t="";
- t+=s.split("__")[0];
- for (int i=2; i< s.split("__").length; i++){
- t+="JOIN"+s.split("__")[i];
- }
- nameMap.put(s,t);
- return t;
}
else {
- nameMap.put(s,s.split("__")[s.split("__").length-1]);
- return s.split("__")[s.split("__").length-1];
+ allStates.add(name);
+ return name;
}
}
- }
-
- public AvatarSpecification generateAvatarSpec(String _loopLimit){
+ /* public AvatarPragma generatePragma(String[] s){
- TraceManager.addDev("security patterns " + tmlmodel.secPatterns);
- TraceManager.addDev("keys " + tmlmap.mappedSecurity);
-
+ }*/
- //TODO: Make state names readable
- //TODO: Put back numeric guards
- //TODO: Calcuate for temp variable
- if (tmlmap.getTMLModeling().getTGComponent()!=null){
- this.avspec = new AvatarSpecification("spec", tmlmap.getTMLModeling().getTGComponent().getTDiagramPanel().tp);
- }
- else {
- this.avspec = new AvatarSpecification("spec", null);
- }
- attrsToCheck.clear();
- //tmlmodel.removeForksAndJoins();
- //Only set the loop limit if it's a number
- String pattern = "^[0-9]{1,2}$";
- Pattern r = Pattern.compile(pattern);
- Matcher m = r.matcher(_loopLimit);
- if (m.find()){
- loopLimit = Integer.valueOf(_loopLimit);
- }
- for (TMLChannel channel: tmlmodel.getChannels()){
- for (TMLCPrimitivePort p: channel.ports){
- channel.checkConf = channel.checkConf || p.checkConf;
- channel.checkAuth = channel.checkAuth || p.checkAuth;
- }
- }
- for (TMLEvent event: tmlmodel.getEvents()){
- if (event.port !=null && event.port2 ==null){
- event.checkConf = event.port.checkConf || event.port2.checkConf;
- event.checkAuth = event.port.checkAuth || event.port2.checkAuth;
- }
- }
- for (TMLRequest request: tmlmodel.getRequests()){
- for (TMLCPrimitivePort p: request.ports){
- request.checkConf = p.checkConf || request.checkConf;
- request.checkAuth = p.checkAuth || request.checkAuth;
- }
- }
-
- AvatarBlock top = new AvatarBlock("TOP__TOP", avspec, null);
- if (mc){
- avspec.addBlock(top);
- AvatarStateMachine topasm = top.getStateMachine();
- AvatarStartState topss = new AvatarStartState("start", null);
- topasm.setStartState(topss);
- topasm.addElement(topss);
- }
-
- List<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
-
- for (TMLTask task:tasks){
- AvatarBlock block = new AvatarBlock(task.getName().split("__")[task.getName().split("__").length-1], avspec, task.getReferenceObject());
- if (mc){
- block.setFather(top);
+ public String getName(String s){
+ if (nameMap.containsKey(s)){
+ return nameMap.get(s);
+ }
+ else {
+ if (!s.contains("__")){
+ nameMap.put(s,s);
+ return s;
+ }
+ else if (s.split("__").length==1){
+ nameMap.put(s,s.split("__")[s.split("__").length-1]);
+ return s.split("__")[s.split("__").length-1];
+ }
+ else if (s.contains("JOIN")){
+ String t="";
+ t+=s.split("__")[0];
+ for (int i=2; i< s.split("__").length; i++){
+ t+="JOIN"+s.split("__")[i];
+ }
+ nameMap.put(s,t);
+ return t;
+ }
+ else {
+ nameMap.put(s,s.split("__")[s.split("__").length-1]);
+ return s.split("__")[s.split("__").length-1];
+ }
+ }
}
- taskBlockMap.put(task, block);
- avspec.addBlock(block);
- }
-
- checkConnections();
- checkChannels();
-
- distributeKeys();
- TraceManager.addDev("ALL KEYS " +accessKeys);
+ public AvatarSpecification generateAvatarSpec(String _loopLimit){
- for (TMLTask task:tasks){
-
- AvatarBlock block = taskBlockMap.get(task);
- //Add temp variable for unsendable signals
+ TraceManager.addDev("security patterns " + tmlmodel.secPatterns);
+ TraceManager.addDev("keys " + tmlmap.mappedSecurity);
- //Add all signals
- for (TMLChannel chan: tmlmodel.getChannels(task)){
- if (chan.hasOriginTask(task)){
- AvatarSignal sig = new AvatarSignal(getName(chan.getName()), AvatarSignal.OUT, chan.getReferenceObject());
- block.addSignal(sig);
- signals.add(sig);
- AvatarAttribute channelData= new AvatarAttribute(getName(chan.getName())+"_chData", AvatarType.INTEGER, block, null);
- if (block.getAvatarAttributeWithName(getName(chan.getName())+"_chData")==null){
- block.addAttribute(channelData);
- }
- sig.addParameter(channelData);
- signalOutMap.put(chan.getName(),sig);
+ //TODO: Make state names readable
+ //TODO: Put back numeric guards
+ //TODO: Calcuate for temp variable
+ if (tmlmap.getTMLModeling().getTGComponent()!=null){
+ this.avspec = new AvatarSpecification("spec", tmlmap.getTMLModeling().getTGComponent().getTDiagramPanel().tp);
}
- else if (chan.hasDestinationTask(task)){
- AvatarSignal sig = new AvatarSignal(getName(chan.getName()), AvatarSignal.IN, chan.getReferenceObject());
- block.addSignal(sig);
- signals.add(sig);
- signalInMap.put(chan.getName(),sig);
- AvatarAttribute channelData= new AvatarAttribute(getName(chan.getName())+"_chData", AvatarType.INTEGER, block, null);
- if (block.getAvatarAttributeWithName(getName(chan.getName())+"_chData")==null){
- block.addAttribute(channelData);
+ else {
+ this.avspec = new AvatarSpecification("spec", null);
+ }
+ attrsToCheck.clear();
+ //tmlmodel.removeForksAndJoins();
+ //Only set the loop limit if it's a number
+ String pattern = "^[0-9]{1,2}$";
+ Pattern r = Pattern.compile(pattern);
+ Matcher m = r.matcher(_loopLimit);
+ if (m.find()){
+ loopLimit = Integer.valueOf(_loopLimit);
+ }
+ for (TMLChannel channel: tmlmodel.getChannels()){
+ for (TMLCPrimitivePort p: channel.ports){
+ channel.checkConf = channel.checkConf || p.checkConf;
+ channel.checkAuth = channel.checkAuth || p.checkAuth;
}
- sig.addParameter(channelData);
- }
- }
- AvatarAttribute tmp = new AvatarAttribute("tmp", AvatarType.INTEGER, block, null);
- block.addAttribute(tmp);
-
- /* tmp = new AvatarAttribute("aliceandbob", AvatarType.INTEGER, block, null);
- block.addAttribute(tmp);
- tmp = new AvatarAttribute("aliceandbob_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(tmp);*/
- AvatarAttribute loop_index = new AvatarAttribute("loop_index", AvatarType.INTEGER, block, null);
- block.addAttribute(loop_index);
- for (TMLAttribute attr: task.getAttributes()){
- AvatarType type;
- if (attr.getType().getType()==TMLType.NATURAL){
- type = AvatarType.INTEGER;
- }
- else if (attr.getType().getType()==TMLType.BOOLEAN) {
- type = AvatarType.BOOLEAN;
- }
- else {
- type = AvatarType.UNDEFINED;
- }
- AvatarAttribute avattr = new AvatarAttribute(attr.getName(), type, block, null);
- block.addAttribute(avattr);
- }
- //AvatarTransition last;
- AvatarStateMachine asm = block.getStateMachine();
-
- //TODO: Create a fork with many requests. This looks terrible
- if (tmlmodel.getRequestToMe(task)!=null){
- //Create iteration attribute
- AvatarAttribute req_loop_index= new AvatarAttribute("req_loop_index", AvatarType.INTEGER, block, null);
- block.addAttribute(req_loop_index);
-
- //TMLRequest request= tmlmodel.getRequestToMe(task);
- //Oh this is fun...let's restructure the state machine
- //Create own start state, and ignore the returned one
- List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
- AvatarStartState ss = new AvatarStartState("start", task.getActivityDiagram().get(0).getReferenceObject());
- asm.addElement(ss);
- AvatarTransition at= new AvatarTransition(block, "__after_start", task.getActivityDiagram().get(0).getReferenceObject());
- at.addAction(AvatarTerm.createActionFromString(block, "req_loop_index = 0"));
- ss.addNext(at);
- asm.addElement(at);
-
- AvatarState loopstart = new AvatarState("loopstart", task.getActivityDiagram().get(0).getReferenceObject());
- at.addNext(loopstart);
- asm.addElement(loopstart);
-
- //Find the original start state, transition, and next element
- AvatarStateMachineElement start = elementList.get(0);
- AvatarStateMachineElement startTran= start.getNext(0);
- AvatarStateMachineElement newStart = startTran.getNext(0);
- elementList.remove(start);
- elementList.remove(startTran);
- //Find every stop state, remove them, reroute transitions to them
- //For now, route every transition to stop state to remove the loop on requests
-
- for (AvatarStateMachineElement e: elementList){
- e.setName(processName(e.getName(), e.getID()));
- stateObjectMap.put(task.getName().split("__")[1]+"__"+e.getName(), e.getReferenceObject());
-
- if (e instanceof AvatarStopState){
- //ignore it
}
- else {
- for (int i=0; i< e.getNexts().size(); i++){
- if (e.getNext(i) instanceof AvatarStopState){
- e.removeNext(i);
- //Route it back to the loop start
- e.addNext(loopstart);
+ for (TMLEvent event: tmlmodel.getEvents()){
+ if (event.port !=null && event.port2 ==null){
+ event.checkConf = event.port.checkConf || event.port2.checkConf;
+ event.checkAuth = event.port.checkAuth || event.port2.checkAuth;
}
}
- asm.addElement(e);
+ for (TMLRequest request: tmlmodel.getRequests()){
+ for (TMLCPrimitivePort p: request.ports){
+ request.checkConf = p.checkConf || request.checkConf;
+ request.checkAuth = p.checkAuth || request.checkAuth;
+ }
}
- }
- //Create exit after # of loop iterations is maxed out
- /*AvatarStopState stop =*/ new AvatarStopState("stop", task.getActivityDiagram().get(0).getReferenceObject());
- /*AvatarTransition exitTran = */new AvatarTransition(block, "to_stop", task.getActivityDiagram().get(0).getReferenceObject());
-
-
- //Add Requests, direct transition to start of state machine
- for (Object obj: tmlmodel.getRequestsToMe(task)){
- TMLRequest req = (TMLRequest) obj;
- AvatarTransition incrTran = new AvatarTransition(block, "__after_loopstart__"+req.getName(), task.getActivityDiagram().get(0).getReferenceObject());
- incrTran.addAction(AvatarTerm.createActionFromString(block,"req_loop_index = req_loop_index + 1"));
- incrTran.setGuard(AvatarGuard.createFromString(block, "req_loop_index != " + loopLimit));
- asm.addElement(incrTran);
- loopstart.addNext(incrTran);
- AvatarSignal sig;
- if (!signalInMap.containsKey(req.getName())){
- sig = new AvatarSignal(getName(req.getName()), AvatarSignal.IN, req.getReferenceObject());
- block.addSignal(sig);
- signals.add(sig);
- signalInMap.put(req.getName(),sig);
- }
- else {
- sig = signalInMap.get(req.getName());
+ AvatarBlock top = new AvatarBlock("TOP__TOP", avspec, null);
+ if (mc){
+ avspec.addBlock(top);
+ AvatarStateMachine topasm = top.getStateMachine();
+ AvatarStartState topss = new AvatarStartState("start", null);
+ topasm.setStartState(topss);
+ topasm.addElement(topss);
}
- AvatarActionOnSignal as= new AvatarActionOnSignal("getRequest__"+req.getName(), sig, req.getReferenceObject());
- incrTran.addNext(as);
- asm.addElement(as);
- as.addValue(req.getName()+"__reqData");
- AvatarAttribute requestData= new AvatarAttribute(req.getName()+"__reqData", AvatarType.INTEGER, block, null);
- block.addAttribute(requestData);
- for (int i=0; i< req.getNbOfParams(); i++){
- if (block.getAvatarAttributeWithName(req.getParam(i))==null){
- //Throw Error
- as.addValue("tmp");
- }
- else {
- as.addValue(req.getParam(i));
+
+ List<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
+
+ for (TMLTask task:tasks){
+ AvatarBlock block = new AvatarBlock(task.getName().split("__")[task.getName().split("__").length-1], avspec, task.getReferenceObject());
+ if (mc){
+ block.setFather(top);
}
- }
- AvatarTransition tran = new AvatarTransition(block, "__after_" + req.getName(), task.getActivityDiagram().get(0).getReferenceObject());
- as.addNext(tran);
- asm.addElement(tran);
- if (req.checkAuth){
- AvatarState afterSignalState = new AvatarState("aftersignalstate_"+req.getName().replaceAll(" ","")+"_"+req.getName().replaceAll(" ",""),req.getReferenceObject());
- AvatarTransition afterSignalTran = new AvatarTransition(block, "__aftersignalstate_"+req.getName(), req.getReferenceObject());
- tran.addNext(afterSignalState);
- afterSignalState.addNext(afterSignalTran);
- asm.addElement(afterSignalState);
- asm.addElement(afterSignalTran);
- afterSignalTran.addNext(newStart);
- AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+afterSignalState.getName()+"."+requestData.getName(),obj,requestData, afterSignalState);
- signalAuthDestMap.put(req.getName(), authDest);
- }
- else {
- tran.addNext(newStart);
+ taskBlockMap.put(task, block);
+ avspec.addBlock(block);
}
- }
+ checkConnections();
+ checkChannels();
-
- asm.setStartState(ss);
-
- }
- else {
- //Not requested
- List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
- for (AvatarStateMachineElement e: elementList){
- e.setName(processName(e.getName(), e.getID()));
- asm.addElement(e);
- stateObjectMap.put(task.getName().split("__")[1]+"__"+e.getName(), e.getReferenceObject());
- }
- asm.setStartState((AvatarStartState) elementList.get(0));
- }
- for (SecurityPattern secPattern: secPatterns){
- AvatarAttribute sec = new AvatarAttribute(secPattern.name, AvatarType.INTEGER, block, null);
- AvatarAttribute enc = new AvatarAttribute(secPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
- block.addAttribute(sec);
- block.addAttribute(enc);
- avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ secPattern.name, null, sec));
- }
-
- }
-
-
- //Add authenticity pragmas
- for (String s: signalAuthOriginMap.keySet()){
- if (signalAuthDestMap.containsKey(s)){
- AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity("#Authenticity " + signalAuthOriginMap.get(s).getName() + " " + signalAuthDestMap.get(s).getName(), signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
- //System.out.println("adding pragma " + s);
- avspec.addPragma(pragma);
- }
- }
+ distributeKeys();
- //Create relations
- //Channels are ?? to ??
- //Requests are n to 1
- //Events are ?? to ??
- AvatarBlock fifo = new AvatarBlock("FIFO", avspec,null);
- for (TMLChannel channel:tmlmodel.getChannels()){
- if (channel.getName().contains("JOINCHANNEL")){
- AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
- ar.setPrivate(false);
- if (channel.getType()==TMLChannel.BRBW){
- ar.setAsynchronous(true);
- ar.setSizeOfFIFO(channel.getSize());
- ar.setBlocking(true);
- }
- else if (channel.getType()==TMLChannel.BRNBW){
- ar.setAsynchronous(true);
- ar.setSizeOfFIFO(channel.getSize());
- ar.setBlocking(false);
- }
- else {
- //Create new block, hope for best
- if (mc){
- fifo = createFifo(channel.getName());
- ar.setAsynchronous(false);
- }
- }
- //System.out.println(channel.getName() + " " +channel.getOriginTask().getName() + " " + channel.getDestinationTask().getName());
- //Find in signal
- //Sig1 contains IN Signals, Sig2 contains OUT signals
- List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
- List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
- for (AvatarSignal sig: taskBlockMap.get(channel.getDestinationTask()).getSignals()){
- if (sig.getInOut()==AvatarSignal.IN){
- String name = sig.getName();
- String tmp = getName(channel.getName());
- if (name.equals(tmp.split("JOIN")[tmp.split("JOIN").length-1]) || name.equals(tmp)){
- sig1.add(sig);
+ System.out.println("ALL KEYS " +accessKeys);
+ for (TMLTask t: accessKeys.keySet()){
+ System.out.println("TASK " +t.getName());
+ for (SecurityPattern sp: accessKeys.get(t)){
+ System.out.println(sp.name);
}
}
- }
- for (AvatarSignal sig: taskBlockMap.get(channel.getOriginTask()).getSignals()){
- if (sig.getInOut()==AvatarSignal.OUT){
- String name = sig.getName();
- String tmp = getName(channel.getName());
- if (name.equals(tmp.split("JOIN")[tmp.split("JOIN").length-1]) || name.equals(tmp)){
- sig2.add(sig);
+
+ for (TMLTask task:tasks){
+
+ AvatarBlock block = taskBlockMap.get(task);
+ //Add temp variable for unsendable signals
+
+ //Add all signals
+ for (TMLChannel chan: tmlmodel.getChannels(task)){
+ if (chan.hasOriginTask(task)){
+ AvatarSignal sig = new AvatarSignal(getName(chan.getName()), AvatarSignal.OUT, chan.getReferenceObject());
+
+ block.addSignal(sig);
+ signals.add(sig);
+ AvatarAttribute channelData= new AvatarAttribute(getName(chan.getName())+"_chData", AvatarType.INTEGER, block, null);
+ if (block.getAvatarAttributeWithName(getName(chan.getName())+"_chData")==null){
+ block.addAttribute(channelData);
+ }
+ sig.addParameter(channelData);
+ signalOutMap.put(chan.getName(),sig);
+ }
+ else if (chan.hasDestinationTask(task)){
+ AvatarSignal sig = new AvatarSignal(getName(chan.getName()), AvatarSignal.IN, chan.getReferenceObject());
+ block.addSignal(sig);
+ signals.add(sig);
+ signalInMap.put(chan.getName(),sig);
+ AvatarAttribute channelData= new AvatarAttribute(getName(chan.getName())+"_chData", AvatarType.INTEGER, block, null);
+ if (block.getAvatarAttributeWithName(getName(chan.getName())+"_chData")==null){
+ block.addAttribute(channelData);
+ }
+ sig.addParameter(channelData);
+ }
}
- }
- }
- System.out.println("Signals " +sig1 + " " + sig2);
- if (sig1.size()==1 && sig2.size()==1){
- if (channel.getType()==TMLChannel.NBRNBW && mc){
- AvatarSignal read = fifo.getSignalByName("readSignal");
-
- ar.block2= fifo;
- //Set IN signal with read
- ar.addSignals(sig1.get(0), read);
- AvatarRelation ar2= new AvatarRelation(channel.getName()+"2", fifo, taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
- AvatarSignal write = fifo.getSignalByName("writeSignal");
- //set OUT signal with write
- ar2.addSignals(write, sig2.get(0));
- System.out.println("Set " + sig2.get(0) + " and write");
- ar2.setAsynchronous(false);
- avspec.addRelation(ar2);
+ AvatarAttribute tmp = new AvatarAttribute("tmp", AvatarType.INTEGER, block, null);
+ block.addAttribute(tmp);
+
+ /* tmp = new AvatarAttribute("aliceandbob", AvatarType.INTEGER, block, null);
+ block.addAttribute(tmp);
+ tmp = new AvatarAttribute("aliceandbob_encrypted", AvatarType.INTEGER, block, null);
+ block.addAttribute(tmp);*/
+ AvatarAttribute loop_index = new AvatarAttribute("loop_index", AvatarType.INTEGER, block, null);
+ block.addAttribute(loop_index);
+ for (TMLAttribute attr: task.getAttributes()){
+ AvatarType type;
+ if (attr.getType().getType()==TMLType.NATURAL){
+ type = AvatarType.INTEGER;
+ }
+ else if (attr.getType().getType()==TMLType.BOOLEAN) {
+ type = AvatarType.BOOLEAN;
+ }
+ else {
+ type = AvatarType.UNDEFINED;
+ }
+ AvatarAttribute avattr = new AvatarAttribute(attr.getName(), type, block, null);
+ block.addAttribute(avattr);
+ }
+ //AvatarTransition last;
+ AvatarStateMachine asm = block.getStateMachine();
+
+ //TODO: Create a fork with many requests. This looks terrible
+ if (tmlmodel.getRequestToMe(task)!=null){
+ //Create iteration attribute
+ AvatarAttribute req_loop_index= new AvatarAttribute("req_loop_index", AvatarType.INTEGER, block, null);
+ block.addAttribute(req_loop_index);
+
+ //TMLRequest request= tmlmodel.getRequestToMe(task);
+ //Oh this is fun...let's restructure the state machine
+ //Create own start state, and ignore the returned one
+ List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
+ AvatarStartState ss = new AvatarStartState("start", task.getActivityDiagram().get(0).getReferenceObject());
+ asm.addElement(ss);
+ AvatarTransition at= new AvatarTransition(block, "__after_start", task.getActivityDiagram().get(0).getReferenceObject());
+ at.addAction(AvatarTerm.createActionFromString(block, "req_loop_index = 0"));
+ ss.addNext(at);
+ asm.addElement(at);
+
+ AvatarState loopstart = new AvatarState("loopstart", task.getActivityDiagram().get(0).getReferenceObject());
+ at.addNext(loopstart);
+ asm.addElement(loopstart);
+
+ //Find the original start state, transition, and next element
+ AvatarStateMachineElement start = elementList.get(0);
+ AvatarStateMachineElement startTran= start.getNext(0);
+ AvatarStateMachineElement newStart = startTran.getNext(0);
+ elementList.remove(start);
+ elementList.remove(startTran);
+ //Find every stop state, remove them, reroute transitions to them
+ //For now, route every transition to stop state to remove the loop on requests
+
+ for (AvatarStateMachineElement e: elementList){
+ e.setName(processName(e.getName(), e.getID()));
+ stateObjectMap.put(task.getName().split("__")[1]+"__"+e.getName(), e.getReferenceObject());
+
+ if (e instanceof AvatarStopState){
+ //ignore it
+ }
+ else {
+ for (int i=0; i< e.getNexts().size(); i++){
+ if (e.getNext(i) instanceof AvatarStopState){
+ e.removeNext(i);
+ //Route it back to the loop start
+ e.addNext(loopstart);
+ }
+ }
+ asm.addElement(e);
+ }
+ }
+
+ //Create exit after # of loop iterations is maxed out
+ /*AvatarStopState stop =*/ new AvatarStopState("stop", task.getActivityDiagram().get(0).getReferenceObject());
+ /*AvatarTransition exitTran = */new AvatarTransition(block, "to_stop", task.getActivityDiagram().get(0).getReferenceObject());
+
+
+ //Add Requests, direct transition to start of state machine
+ for (Object obj: tmlmodel.getRequestsToMe(task)){
+ TMLRequest req = (TMLRequest) obj;
+ AvatarTransition incrTran = new AvatarTransition(block, "__after_loopstart__"+req.getName(), task.getActivityDiagram().get(0).getReferenceObject());
+ incrTran.addAction(AvatarTerm.createActionFromString(block,"req_loop_index = req_loop_index + 1"));
+ incrTran.setGuard(AvatarGuard.createFromString(block, "req_loop_index != " + loopLimit));
+ asm.addElement(incrTran);
+ loopstart.addNext(incrTran);
+ AvatarSignal sig;
+ if (!signalInMap.containsKey(req.getName())){
+ sig = new AvatarSignal(getName(req.getName()), AvatarSignal.IN, req.getReferenceObject());
+ block.addSignal(sig);
+ signals.add(sig);
+ signalInMap.put(req.getName(),sig);
+ }
+ else {
+ sig = signalInMap.get(req.getName());
+ }
+ AvatarActionOnSignal as= new AvatarActionOnSignal("getRequest__"+req.getName(), sig, req.getReferenceObject());
+ incrTran.addNext(as);
+ asm.addElement(as);
+ as.addValue(req.getName()+"__reqData");
+ AvatarAttribute requestData= new AvatarAttribute(req.getName()+"__reqData", AvatarType.INTEGER, block, null);
+ block.addAttribute(requestData);
+ for (int i=0; i< req.getNbOfParams(); i++){
+ if (block.getAvatarAttributeWithName(req.getParam(i))==null){
+ //Throw Error
+ as.addValue("tmp");
+ }
+ else {
+ as.addValue(req.getParam(i));
+ }
+ }
+ AvatarTransition tran = new AvatarTransition(block, "__after_" + req.getName(), task.getActivityDiagram().get(0).getReferenceObject());
+ as.addNext(tran);
+ asm.addElement(tran);
+ if (req.checkAuth){
+ AvatarState afterSignalState = new AvatarState("aftersignalstate_"+req.getName().replaceAll(" ","")+"_"+req.getName().replaceAll(" ",""),req.getReferenceObject());
+ AvatarTransition afterSignalTran = new AvatarTransition(block, "__aftersignalstate_"+req.getName(), req.getReferenceObject());
+ tran.addNext(afterSignalState);
+ afterSignalState.addNext(afterSignalTran);
+ asm.addElement(afterSignalState);
+ asm.addElement(afterSignalTran);
+ afterSignalTran.addNext(newStart);
+ AvatarAttributeState authDest = new AvatarAttributeState(block.getName()+"."+afterSignalState.getName()+"."+requestData.getName(),obj,requestData, afterSignalState);
+ signalAuthDestMap.put(req.getName(), authDest);
+ }
+ else {
+ tran.addNext(newStart);
+ }
+
+ }
+
+
+ asm.setStartState(ss);
+
}
else {
- ar.addSignals(sig2.get(0), sig1.get(0));
- }
- }
- avspec.addRelation(ar);
- }
-
- else if (channel.isBasicChannel()){
- //System.out.println("checking channel " + channel.getName());
- AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
- LinkedList<HwCommunicationNode> path =tmlmap.findNodesForElement(channel);
- if (path.size()!=0){
- ar.setPrivate(true);
- for (HwCommunicationNode node:path){
- if (node instanceof HwBus){
- if (((HwBus) node).privacy ==0){
- ar.setPrivate(false);
- }
+ //Not requested
+ List<AvatarStateMachineElement> elementList= translateState(task.getActivityDiagram().get(0), block);
+ for (AvatarStateMachineElement e: elementList){
+ e.setName(processName(e.getName(), e.getID()));
+ asm.addElement(e);
+ stateObjectMap.put(task.getName().split("__")[1]+"__"+e.getName(), e.getReferenceObject());
}
+ asm.setStartState((AvatarStartState) elementList.get(0));
}
+ for (SecurityPattern secPattern: secPatterns){
+ AvatarAttribute sec = new AvatarAttribute(secPattern.name, AvatarType.INTEGER, block, null);
+ AvatarAttribute enc = new AvatarAttribute(secPattern.name+"_encrypted", AvatarType.INTEGER, block, null);
+ block.addAttribute(sec);
+ block.addAttribute(enc);
+ avspec.addPragma(new AvatarPragmaSecret("#Confidentiality "+block.getName() + "."+ secPattern.name, null, sec));
+ }
+
}
- else {
- ar.setPrivate(originDestMap.get(channel.getOriginTask().getName()+"__"+channel.getDestinationTask().getName())==1);
- }
- if (channel.getType()==TMLChannel.BRBW){
- ar.setAsynchronous(true);
- ar.setSizeOfFIFO(channel.getSize());
- ar.setBlocking(true);
- }
- else if (channel.getType()==TMLChannel.BRNBW){
- ar.setAsynchronous(true);
- ar.setSizeOfFIFO(channel.getSize());
- ar.setBlocking(false);
- }
- else {
- //Create new block, hope for best
- if (mc){
- fifo = createFifo(channel.getName());
- ar.setAsynchronous(false);
- }
- }
- //Find in signal
- List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
- //Sig1 contains IN Signals, Sig2 contains OUT signals
- List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.IN){
- String name = sig.getName();
- if (name.equals(getName(channel.getName()))){
- sig1.add(sig);
- }
+
+
+ //Add authenticity pragmas
+ for (String s: signalAuthOriginMap.keySet()){
+ if (signalAuthDestMap.containsKey(s)){
+ AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity("#Authenticity " + signalAuthOriginMap.get(s).getName() + " " + signalAuthDestMap.get(s).getName(), signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
+ //System.out.println("adding pragma " + s);
+ avspec.addPragma(pragma);
}
}
- //Find out signal
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.OUT){
- String name = sig.getName();
- if (name.equals(getName(channel.getName()))){
- sig2.add(sig);
+
+ //Create relations
+ //Channels are ?? to ??
+ //Requests are n to 1
+ //Events are ?? to ??
+ AvatarBlock fifo = new AvatarBlock("FIFO", avspec,null);
+ for (TMLChannel channel:tmlmodel.getChannels()){
+ if (channel.getName().contains("JOINCHANNEL")){
+ AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
+ ar.setPrivate(false);
+ if (channel.getType()==TMLChannel.BRBW){
+ ar.setAsynchronous(true);
+ ar.setSizeOfFIFO(channel.getSize());
+ ar.setBlocking(true);
+ }
+ else if (channel.getType()==TMLChannel.BRNBW){
+ ar.setAsynchronous(true);
+ ar.setSizeOfFIFO(channel.getSize());
+ ar.setBlocking(false);
+ }
+ else {
+ //Create new block, hope for best
+ if (mc){
+ fifo = createFifo(channel.getName());
+ ar.setAsynchronous(false);
+ }
}
+ //System.out.println(channel.getName() + " " +channel.getOriginTask().getName() + " " + channel.getDestinationTask().getName());
+ //Find in signal
+ //Sig1 contains IN Signals, Sig2 contains OUT signals
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ for (AvatarSignal sig: taskBlockMap.get(channel.getDestinationTask()).getSignals()){
+ if (sig.getInOut()==AvatarSignal.IN){
+ String name = sig.getName();
+ String tmp = getName(channel.getName());
+ if (name.equals(tmp.split("JOIN")[tmp.split("JOIN").length-1]) || name.equals(tmp)){
+ sig1.add(sig);
+ }
+ }
+ }
+ for (AvatarSignal sig: taskBlockMap.get(channel.getOriginTask()).getSignals()){
+ if (sig.getInOut()==AvatarSignal.OUT){
+ String name = sig.getName();
+ String tmp = getName(channel.getName());
+ if (name.equals(tmp.split("JOIN")[tmp.split("JOIN").length-1]) || name.equals(tmp)){
+ sig2.add(sig);
+ }
+ }
+ }
+ System.out.println("Signals " +sig1 + " " + sig2);
+ if (sig1.size()==1 && sig2.size()==1){
+ if (channel.getType()==TMLChannel.NBRNBW && mc){
+ AvatarSignal read = fifo.getSignalByName("readSignal");
+
+ ar.block2= fifo;
+ //Set IN signal with read
+ ar.addSignals(sig1.get(0), read);
+ AvatarRelation ar2= new AvatarRelation(channel.getName()+"2", fifo, taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
+ AvatarSignal write = fifo.getSignalByName("writeSignal");
+ //set OUT signal with write
+ ar2.addSignals(write, sig2.get(0));
+ System.out.println("Set " + sig2.get(0) + " and write");
+ ar2.setAsynchronous(false);
+ avspec.addRelation(ar2);
+ }
+ else {
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ }
+ }
+ avspec.addRelation(ar);
}
- }
- if (sig1.size()==0){
- sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
- }
- if (sig2.size()==0){
- sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
- }
- if (sig1.size()==1 && sig2.size()==1){
- if (channel.getType()==TMLChannel.NBRNBW && mc){
- AvatarSignal read = fifo.getSignalByName("readSignal");
-
- ar.block2= fifo;
- //Set IN signal with read
- ar.addSignals(sig1.get(0), read);
- AvatarRelation ar2= new AvatarRelation(channel.getName()+"2", fifo, taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
- AvatarSignal write = fifo.getSignalByName("writeSignal");
- //set OUT signal with write
- ar2.addSignals(write, sig2.get(0));
- System.out.println("Set " + sig2.get(0) + " and write");
- ar2.setAsynchronous(false);
- avspec.addRelation(ar2);
+
+ else if (channel.isBasicChannel()){
+ //System.out.println("checking channel " + channel.getName());
+ AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(channel.getOriginTask()), taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
+ LinkedList<HwCommunicationNode> path =tmlmap.findNodesForElement(channel);
+ if (path.size()!=0){
+ ar.setPrivate(true);
+ for (HwCommunicationNode node:path){
+ if (node instanceof HwBus){
+ if (((HwBus) node).privacy ==0){
+ ar.setPrivate(false);
+ }
+ }
+ }
+ }
+ else {
+ ar.setPrivate(originDestMap.get(channel.getOriginTask().getName()+"__"+channel.getDestinationTask().getName())==1);
+ }
+ if (channel.getType()==TMLChannel.BRBW){
+ ar.setAsynchronous(true);
+ ar.setSizeOfFIFO(channel.getSize());
+ ar.setBlocking(true);
+ }
+ else if (channel.getType()==TMLChannel.BRNBW){
+ ar.setAsynchronous(true);
+ ar.setSizeOfFIFO(channel.getSize());
+ ar.setBlocking(false);
+ }
+ else {
+ //Create new block, hope for best
+ if (mc){
+ fifo = createFifo(channel.getName());
+ ar.setAsynchronous(false);
+ }
+ }
+ //Find in signal
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ //Sig1 contains IN Signals, Sig2 contains OUT signals
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.IN){
+ String name = sig.getName();
+ if (name.equals(getName(channel.getName()))){
+ sig1.add(sig);
+ }
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.OUT){
+ String name = sig.getName();
+ if (name.equals(getName(channel.getName()))){
+ sig2.add(sig);
+ }
+ }
+ }
+ if (sig1.size()==0){
+ sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
+ }
+ if (sig2.size()==0){
+ sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
+ }
+ if (sig1.size()==1 && sig2.size()==1){
+ if (channel.getType()==TMLChannel.NBRNBW && mc){
+ AvatarSignal read = fifo.getSignalByName("readSignal");
+
+ ar.block2= fifo;
+ //Set IN signal with read
+ ar.addSignals(sig1.get(0), read);
+ AvatarRelation ar2= new AvatarRelation(channel.getName()+"2", fifo, taskBlockMap.get(channel.getDestinationTask()), channel.getReferenceObject());
+ AvatarSignal write = fifo.getSignalByName("writeSignal");
+ //set OUT signal with write
+ ar2.addSignals(write, sig2.get(0));
+ System.out.println("Set " + sig2.get(0) + " and write");
+ ar2.setAsynchronous(false);
+ avspec.addRelation(ar2);
+ }
+ else {
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ }
+ }
+ else {
+ //Create relation if it does not exist
+ if (top.getSignalByName(getName(channel.getName())+"in")==null){
+ AvatarRelation relation= new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
+ AvatarSignal s1 = new AvatarSignal(getName(channel.getName())+"in", AvatarSignal.IN, null);
+ AvatarSignal s2 = new AvatarSignal(getName(channel.getName())+"out", AvatarSignal.OUT, null);
+ top.addSignal(s1);
+ top.addSignal(s2);
+ relation.addSignals(s2,s1);
+ avspec.addRelation(relation);
+ System.out.println("Failure to match signals for TMLChannel "+ channel.getName());
+ }
+ }
+ avspec.addRelation(ar);
}
else {
- ar.addSignals(sig2.get(0), sig1.get(0));
+ System.out.println("Found non-basic channel");
+ //If not a basic channel, create a relation between TOP block and itself
+ AvatarRelation relation= new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
+ AvatarSignal s1 = new AvatarSignal(getName(channel.getName())+"in", AvatarSignal.IN, null);
+ AvatarSignal s2 = new AvatarSignal(getName(channel.getName())+"out", AvatarSignal.OUT, null);
+ top.addSignal(s1);
+ top.addSignal(s2);
+ relation.addSignals(s2,s1);
+ avspec.addRelation(relation);
+ for (TMLTask t1: channel.getOriginTasks()){
+ for (TMLTask t2: channel.getDestinationTasks()){
+ AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(t1), taskBlockMap.get(t2), channel.getReferenceObject());
+ ar.setPrivate(originDestMap.get(t1.getName()+"__"+t2.getName())==1);
+ //Find in signal
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.IN){
+ String name = sig.getName();
+ if (name.equals(getName(channel.getName()))){
+ sig1.add(sig);
+ }
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.OUT){
+ String name = sig.getName();
+ if (name.equals(getName(channel.getName()))){
+ sig2.add(sig);
+ }
+ }
+ }
+ if (sig1.size()==0){
+ sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
+ }
+ if (sig2.size()==0){
+ sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
+ }
+ if (sig1.size()==1 && sig2.size()==1){
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ }
+ else {
+ System.out.println("Failure to match signals for TMLChannel "+ channel.getName() + " between " + t1.getName() + " and "+ t2.getName());
+ }
+ avspec.addRelation(ar);
+ }
+ }
}
}
- else {
- //Create relation if it does not exist
- if (top.getSignalByName(getName(channel.getName())+"in")==null){
- AvatarRelation relation= new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
- AvatarSignal s1 = new AvatarSignal(getName(channel.getName())+"in", AvatarSignal.IN, null);
- AvatarSignal s2 = new AvatarSignal(getName(channel.getName())+"out", AvatarSignal.OUT, null);
- top.addSignal(s1);
- top.addSignal(s2);
- relation.addSignals(s2,s1);
- avspec.addRelation(relation);
- System.out.println("Failure to match signals for TMLChannel "+ channel.getName());
+ for (TMLRequest request: tmlmodel.getRequests()){
+ for (TMLTask t1: request.getOriginTasks()){
+ AvatarRelation ar = new AvatarRelation(request.getName(), taskBlockMap.get(t1), taskBlockMap.get(request.getDestinationTask()), request.getReferenceObject());
+ ar.setPrivate(originDestMap.get(t1.getName()+"__"+request.getDestinationTask().getName())==1);
+ List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
+ List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.IN){
+ String name = sig.getName();
+
+ if (name.equals(getName(request.getName()))){
+ sig1.add(sig);
+ }
+ }
+ }
+ //Find out signal
+ for (AvatarSignal sig: signals){
+ if (sig.getInOut()==AvatarSignal.OUT){
+ String name = sig.getName();
+
+ if (name.equals(getName(request.getName()))){
+ sig2.add(sig);
+ }
+ }
+ }
+ if (sig1.size()==0){
+ sig1.add(new AvatarSignal(getName(request.getName()), AvatarSignal.IN, null));
+ }
+ if (sig2.size()==0){
+ sig2.add(new AvatarSignal(getName(request.getName()), AvatarSignal.OUT, null));
+ }
+ if (sig1.size()==1 && sig2.size()==1){
+ ar.addSignals(sig2.get(0), sig1.get(0));
+ }
+ else {
+ //Throw error
+ System.out.println("Could not match for " + request.getName());
+ }
+
+ ar.setAsynchronous(false);
+ avspec.addRelation(ar);
}
}
- avspec.addRelation(ar);
- }
- else {
- System.out.println("Found non-basic channel");
- //If not a basic channel, create a relation between TOP block and itself
- AvatarRelation relation= new AvatarRelation(channel.getName(), top, top, channel.getReferenceObject());
- AvatarSignal s1 = new AvatarSignal(getName(channel.getName())+"in", AvatarSignal.IN, null);
- AvatarSignal s2 = new AvatarSignal(getName(channel.getName())+"out", AvatarSignal.OUT, null);
- top.addSignal(s1);
- top.addSignal(s2);
- relation.addSignals(s2,s1);
- avspec.addRelation(relation);
- for (TMLTask t1: channel.getOriginTasks()){
- for (TMLTask t2: channel.getDestinationTasks()){
- AvatarRelation ar= new AvatarRelation(channel.getName(), taskBlockMap.get(t1), taskBlockMap.get(t2), channel.getReferenceObject());
- ar.setPrivate(originDestMap.get(t1.getName()+"__"+t2.getName())==1);
- //Find in signal
+ for (TMLEvent event: tmlmodel.getEvents()){
+
+ AvatarRelation ar = new AvatarRelation(event.getName(), taskBlockMap.get(event.getOriginTask()), taskBlockMap.get(event.getDestinationTask()), event.getReferenceObject());
+ ar.setPrivate(originDestMap.get(event.getOriginTask().getName()+"__"+event.getDestinationTask().getName())==1);
List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
for (AvatarSignal sig: signals){
if (sig.getInOut()==AvatarSignal.IN){
String name = sig.getName();
- if (name.equals(getName(channel.getName()))){
+ if (name.equals(getName(event.getName()))){
sig1.add(sig);
}
}
@@ -1903,283 +1997,200 @@ public class TML2Avatar {
for (AvatarSignal sig: signals){
if (sig.getInOut()==AvatarSignal.OUT){
String name = sig.getName();
- if (name.equals(getName(channel.getName()))){
+ if (name.equals(getName(event.getName()))){
sig2.add(sig);
}
}
}
if (sig1.size()==0){
- sig1.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.IN, null));
+ sig1.add(new AvatarSignal(getName(event.getName()), AvatarSignal.IN, null));
}
if (sig2.size()==0){
- sig2.add(new AvatarSignal(getName(channel.getName()), AvatarSignal.OUT, null));
+ sig2.add(new AvatarSignal(getName(event.getName()), AvatarSignal.OUT, null));
}
if (sig1.size()==1 && sig2.size()==1){
ar.addSignals(sig2.get(0), sig1.get(0));
}
- else {
- System.out.println("Failure to match signals for TMLChannel "+ channel.getName() + " between " + t1.getName() + " and "+ t2.getName());
- }
- avspec.addRelation(ar);
+ else {
+ //Throw error
+ System.out.println("Could not match for " + event.getName());
+ }
+ if (event.isBlocking()){
+ ar.setAsynchronous(true);
+ ar.setBlocking(true);
+ ar.setSizeOfFIFO(event.getMaxSize());
+ }
+ else {
+ ar.setAsynchronous(true);
+ ar.setBlocking(false);
+ ar.setSizeOfFIFO(event.getMaxSize());
+
+ }
+ avspec.addRelation(ar);
}
- }
- }
- }
- for (TMLRequest request: tmlmodel.getRequests()){
- for (TMLTask t1: request.getOriginTasks()){
- AvatarRelation ar = new AvatarRelation(request.getName(), taskBlockMap.get(t1), taskBlockMap.get(request.getDestinationTask()), request.getReferenceObject());
- ar.setPrivate(originDestMap.get(t1.getName()+"__"+request.getDestinationTask().getName())==1);
- List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
- List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.IN){
- String name = sig.getName();
-
- if (name.equals(getName(request.getName()))){
- sig1.add(sig);
- }
+ //check that all signals are put in relations
+ AvatarRelation ar = avspec.getAvatarRelationWithSignal(sig);
+ if (ar==null){
+ System.out.println("missing relation for " + sig.getName());
}
}
- //Find out signal
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.OUT){
- String name = sig.getName();
-
- if (name.equals(getName(request.getName()))){
- sig2.add(sig);
+ //Check if we matched up all signals
+ for (SecurityPattern sp:symKeys.keySet()){
+ if (symKeys.get(sp).size()>1){
+ String keys = "";
+ for (AvatarAttribute key: symKeys.get(sp)){
+ keys= keys+" "+key.getBlock().getName() + "."+key.getName();
}
+ avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge"+ keys, null, symKeys.get(sp), true));
}
}
- if (sig1.size()==0){
- sig1.add(new AvatarSignal(getName(request.getName()), AvatarSignal.IN, null));
- }
- if (sig2.size()==0){
- sig2.add(new AvatarSignal(getName(request.getName()), AvatarSignal.OUT, null));
- }
- if (sig1.size()==1 && sig2.size()==1){
- ar.addSignals(sig2.get(0), sig1.get(0));
- }
- else {
- //Throw error
- System.out.println("Could not match for " + request.getName());
- }
-
- ar.setAsynchronous(false);
- avspec.addRelation(ar);
- }
- }
- for (TMLEvent event: tmlmodel.getEvents()){
-
- AvatarRelation ar = new AvatarRelation(event.getName(), taskBlockMap.get(event.getOriginTask()), taskBlockMap.get(event.getDestinationTask()), event.getReferenceObject());
- ar.setPrivate(originDestMap.get(event.getOriginTask().getName()+"__"+event.getDestinationTask().getName())==1);
- List<AvatarSignal> sig1 = new ArrayList<AvatarSignal>();
- List<AvatarSignal> sig2 = new ArrayList<AvatarSignal>();
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.IN){
- String name = sig.getName();
- if (name.equals(getName(event.getName()))){
- sig1.add(sig);
- }
- }
- }
- //Find out signal
- for (AvatarSignal sig: signals){
- if (sig.getInOut()==AvatarSignal.OUT){
- String name = sig.getName();
- if (name.equals(getName(event.getName()))){
- sig2.add(sig);
- }
- }
- }
- if (sig1.size()==0){
- sig1.add(new AvatarSignal(getName(event.getName()), AvatarSignal.IN, null));
- }
- if (sig2.size()==0){
- sig2.add(new AvatarSignal(getName(event.getName()), AvatarSignal.OUT, null));
- }
- if (sig1.size()==1 && sig2.size()==1){
- ar.addSignals(sig2.get(0), sig1.get(0));
- }
- else {
- //Throw error
- System.out.println("Could not match for " + event.getName());
- }
- if (event.isBlocking()){
- ar.setAsynchronous(true);
- ar.setBlocking(true);
- ar.setSizeOfFIFO(event.getMaxSize());
- }
- else {
- ar.setAsynchronous(true);
- ar.setBlocking(false);
- ar.setSizeOfFIFO(event.getMaxSize());
-
- }
- avspec.addRelation(ar);
- }
- for (AvatarSignal sig: signals){
- //check that all signals are put in relations
- AvatarRelation ar = avspec.getAvatarRelationWithSignal(sig);
- if (ar==null){
- System.out.println("missing relation for " + sig.getName());
- }
- }
- //Check if we matched up all signals
- for (SecurityPattern sp:symKeys.keySet()){
- if (symKeys.get(sp).size()>1){
- String keys = "";
- for (AvatarAttribute key: symKeys.get(sp)){
- keys= keys+" "+key.getBlock().getName() + "."+key.getName();
- }
- avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge"+ keys, null, symKeys.get(sp), true));
- }
- }
- for (SecurityPattern sp:pubKeys.keySet()){
- if (pubKeys.get(sp).size()!=0){
- String keys = "";
- for (AvatarAttribute key: symKeys.get(sp)){
- keys= keys+" "+key.getBlock().getName() + "."+key.getName();
+ for (SecurityPattern sp:pubKeys.keySet()){
+ if (pubKeys.get(sp).size()!=0){
+ String keys = "";
+ for (AvatarAttribute key: symKeys.get(sp)){
+ keys= keys+" "+key.getBlock().getName() + "."+key.getName();
+ }
+ avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge "+sp.name, null, pubKeys.get(sp),true));
+ }
}
- avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge "+sp.name, null, pubKeys.get(sp),true));
- }
- }
- tmlmap.getTMLModeling().secChannelMap = secChannelMap;
+ tmlmap.getTMLModeling().secChannelMap = secChannelMap;
- System.out.println("avatar spec\n" +avspec);
- return avspec;
- }
+ // System.out.println("avatar spec\n" +avspec);
+ return avspec;
+ }
- public void backtraceReachability(HashMap<AvatarPragmaReachability, ProVerifQueryResult> reachabilityResults) {
- for (AvatarPragmaReachability pragma: reachabilityResults.keySet())
- {
- ProVerifQueryResult result = reachabilityResults.get(pragma);
- if (!result.isProved())
- continue;
-
- int r = result.isSatisfied() ? 1 : 2;
-
- String s = pragma.getBlock().getName() + "__" + pragma.getState().getName();
-
- if (stateObjectMap.containsKey(s)) {
- Object obj = stateObjectMap.get(s);
- if (obj instanceof TMLADWriteChannel){
- TMLADWriteChannel wc =(TMLADWriteChannel) obj;
- wc.reachabilityInformation=r;
- }
- if (obj instanceof TMLADReadChannel){
- TMLADReadChannel wc =(TMLADReadChannel) obj;
- wc.reachabilityInformation=r;
- }
-
- if (obj instanceof TMLADSendEvent){
- TMLADSendEvent wc =(TMLADSendEvent) obj;
- wc.reachabilityInformation=r;
- }
-
- if (obj instanceof TMLADSendRequest){
- TMLADSendRequest wc =(TMLADSendRequest) obj;
- wc.reachabilityInformation=r;
- }
- if (obj instanceof TMLADWaitEvent){
- TMLADWaitEvent wc =(TMLADWaitEvent) obj;
- wc.reachabilityInformation=r;
- }
- }
- }
- }
+ public void backtraceReachability(HashMap<AvatarPragmaReachability, ProVerifQueryResult> reachabilityResults) {
+ for (AvatarPragmaReachability pragma: reachabilityResults.keySet())
+ {
+ ProVerifQueryResult result = reachabilityResults.get(pragma);
+ if (!result.isProved())
+ continue;
+
+ int r = result.isSatisfied() ? 1 : 2;
- public void distributeKeys(){
- List<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
- for (TMLTask t:accessKeys.keySet()){
- AvatarBlock b = taskBlockMap.get(t);
- for (SecurityPattern sp: accessKeys.get(t)){
- if (sp.type.equals("Symmetric Encryption") || sp.type.equals("MAC")){
- AvatarAttribute key = new AvatarAttribute("key_"+sp.name, AvatarType.INTEGER, b, null);
- if (symKeys.containsKey(sp)){
- symKeys.get(sp).add(key);
+ String s = pragma.getBlock().getName() + "__" + pragma.getState().getName();
+
+ if (stateObjectMap.containsKey(s)) {
+ Object obj = stateObjectMap.get(s);
+ if (obj instanceof TMLADWriteChannel){
+ TMLADWriteChannel wc =(TMLADWriteChannel) obj;
+ wc.reachabilityInformation=r;
}
- else {
- LinkedList<AvatarAttribute> tmp = new LinkedList<AvatarAttribute>();
- tmp.add(key);
- symKeys.put(sp, tmp);
+ if (obj instanceof TMLADReadChannel){
+ TMLADReadChannel wc =(TMLADReadChannel) obj;
+ wc.reachabilityInformation=r;
}
- b.addAttribute(key);
- }
- else if (sp.type.equals("Asymmetric Encryption")){
- AvatarAttribute pubkey = new AvatarAttribute("pubKey_"+sp.name, AvatarType.INTEGER, b, null);
- b.addAttribute(pubkey);
- AvatarAttribute privkey = new AvatarAttribute("privKey_"+sp.name, AvatarType.INTEGER, b, null);
- b.addAttribute(privkey);
- avspec.addPragma(new AvatarPragmaPrivatePublicKey("PrivatePublicKey "+sp.name, null, privkey, pubkey));
- if (pubKeys.containsKey(sp)){
- pubKeys.get(sp).add(pubkey);
+
+ if (obj instanceof TMLADSendEvent){
+ TMLADSendEvent wc =(TMLADSendEvent) obj;
+ wc.reachabilityInformation=r;
}
- else {
- LinkedList<AvatarAttribute> tmp = new LinkedList<AvatarAttribute>();
- tmp.add(pubkey);
- pubKeys.put(sp, tmp);
- }
- //Distribute public key everywhere
- for (TMLTask task2 : tasks){
- AvatarBlock b2 = taskBlockMap.get(task2);
- pubkey = new AvatarAttribute("pubKey_"+sp.name, AvatarType.INTEGER, b2, null);
- b2.addAttribute(pubkey);
+
+ if (obj instanceof TMLADSendRequest){
+ TMLADSendRequest wc =(TMLADSendRequest) obj;
+ wc.reachabilityInformation=r;
+ }
+ if (obj instanceof TMLADWaitEvent){
+ TMLADWaitEvent wc =(TMLADWaitEvent) obj;
+ wc.reachabilityInformation=r;
}
}
}
}
- }
- public AvatarBlock createFifo(String name){
- AvatarBlock fifo = new AvatarBlock("FIFO__FIFO"+name, avspec, null);
- AvatarState root = new AvatarState("root",null, false);
- AvatarSignal read = new AvatarSignal("readSignal", AvatarSignal.IN, null);
- AvatarAttribute data = new AvatarAttribute("data", AvatarType.INTEGER, fifo, null);
- fifo.addAttribute(data);
- read.addParameter(data);
- AvatarSignal write = new AvatarSignal("writeSignal", AvatarSignal.OUT, null);
- write.addParameter(data);
- AvatarStartState start = new AvatarStartState("start", null);
- AvatarTransition afterStart = new AvatarTransition(fifo, "afterStart", null);
- fifo.addSignal(read);
- fifo.addSignal(write);
- AvatarTransition toRead = new AvatarTransition(fifo, "toReadSignal", null);
- AvatarTransition toWrite = new AvatarTransition(fifo, "toWriteSignal", null);
- AvatarTransition afterRead = new AvatarTransition(fifo, "afterReadSignal", null);
- AvatarTransition afterWrite = new AvatarTransition(fifo, "afterWriteSignal", null);
- AvatarActionOnSignal readAction= new AvatarActionOnSignal("read", read, null);
- AvatarActionOnSignal writeAction= new AvatarActionOnSignal("write", write, null);
-
- AvatarStateMachine asm = fifo.getStateMachine();
- asm.addElement(start);
- asm.setStartState(start);
- asm.addElement(afterStart);
- asm.addElement(root);
- asm.addElement(toRead);
- asm.addElement(toWrite);
- asm.addElement(afterRead);
- asm.addElement(afterWrite);
- asm.addElement(readAction);
- asm.addElement(writeAction);
-
- start.addNext(afterStart);
- afterStart.addNext(root);
- root.addNext(toRead);
- root.addNext(toWrite);
- toRead.addNext(readAction);
- toWrite.addNext(writeAction);
- readAction.addNext(afterRead);
- writeAction.addNext(afterWrite);
- afterRead.addNext(root);
- afterWrite.addNext(root);
-
- avspec.addBlock(fifo);
- return fifo;
- }
- public AvatarSpecification convertToSecurityType(AvatarSpecification spec){
- return spec;
- }
+ public void distributeKeys(){
+ List<TMLTask> tasks = tmlmap.getTMLModeling().getTasks();
+ for (TMLTask t:accessKeys.keySet()){
+ AvatarBlock b = taskBlockMap.get(t);
+ for (SecurityPattern sp: accessKeys.get(t)){
+ if (sp.type.equals("Symmetric Encryption") || sp.type.equals("MAC")){
+ AvatarAttribute key = new AvatarAttribute("key_"+sp.name, AvatarType.INTEGER, b, null);
+ if (symKeys.containsKey(sp)){
+ symKeys.get(sp).add(key);
+ }
+ else {
+ LinkedList<AvatarAttribute> tmp = new LinkedList<AvatarAttribute>();
+ tmp.add(key);
+ symKeys.put(sp, tmp);
+ }
+ b.addAttribute(key);
+ }
+ else if (sp.type.equals("Asymmetric Encryption")){
+ AvatarAttribute pubkey = new AvatarAttribute("pubKey_"+sp.name, AvatarType.INTEGER, b, null);
+ b.addAttribute(pubkey);
+ AvatarAttribute privkey = new AvatarAttribute("privKey_"+sp.name, AvatarType.INTEGER, b, null);
+ b.addAttribute(privkey);
+ avspec.addPragma(new AvatarPragmaPrivatePublicKey("PrivatePublicKey "+sp.name, null, privkey, pubkey));
+ if (pubKeys.containsKey(sp)){
+ pubKeys.get(sp).add(pubkey);
+ }
+ else {
+ LinkedList<AvatarAttribute> tmp = new LinkedList<AvatarAttribute>();
+ tmp.add(pubkey);
+ pubKeys.put(sp, tmp);
+ }
+ //Distribute public key everywhere
+ for (TMLTask task2 : tasks){
+ AvatarBlock b2 = taskBlockMap.get(task2);
+ pubkey = new AvatarAttribute("pubKey_"+sp.name, AvatarType.INTEGER, b2, null);
+ b2.addAttribute(pubkey);
+ }
+ }
+ }
+ }
+ }
+ public AvatarBlock createFifo(String name){
+ AvatarBlock fifo = new AvatarBlock("FIFO__FIFO"+name, avspec, null);
+ AvatarState root = new AvatarState("root",null, false);
+ AvatarSignal read = new AvatarSignal("readSignal", AvatarSignal.IN, null);
+ AvatarAttribute data = new AvatarAttribute("data", AvatarType.INTEGER, fifo, null);
+ fifo.addAttribute(data);
+ read.addParameter(data);
+ AvatarSignal write = new AvatarSignal("writeSignal", AvatarSignal.OUT, null);
+ write.addParameter(data);
+ AvatarStartState start = new AvatarStartState("start", null);
+ AvatarTransition afterStart = new AvatarTransition(fifo, "afterStart", null);
+ fifo.addSignal(read);
+ fifo.addSignal(write);
+ AvatarTransition toRead = new AvatarTransition(fifo, "toReadSignal", null);
+ AvatarTransition toWrite = new AvatarTransition(fifo, "toWriteSignal", null);
+ AvatarTransition afterRead = new AvatarTransition(fifo, "afterReadSignal", null);
+ AvatarTransition afterWrite = new AvatarTransition(fifo, "afterWriteSignal", null);
+ AvatarActionOnSignal readAction= new AvatarActionOnSignal("read", read, null);
+ AvatarActionOnSignal writeAction= new AvatarActionOnSignal("write", write, null);
+
+ AvatarStateMachine asm = fifo.getStateMachine();
+ asm.addElement(start);
+ asm.setStartState(start);
+ asm.addElement(afterStart);
+ asm.addElement(root);
+ asm.addElement(toRead);
+ asm.addElement(toWrite);
+ asm.addElement(afterRead);
+ asm.addElement(afterWrite);
+ asm.addElement(readAction);
+ asm.addElement(writeAction);
+
+ start.addNext(afterStart);
+ afterStart.addNext(root);
+ root.addNext(toRead);
+ root.addNext(toWrite);
+ toRead.addNext(readAction);
+ toWrite.addNext(writeAction);
+ readAction.addNext(afterRead);
+ writeAction.addNext(afterWrite);
+ afterRead.addNext(root);
+ afterWrite.addNext(root);
+
+ avspec.addBlock(fifo);
+ return fifo;
+ }
+
+ public AvatarSpecification convertToSecurityType(AvatarSpecification spec){
+ return spec;
+ }
-}
+ }
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index 8882717642394621300beeff4e35da23d98b4ecc..7bb68e4d458daf84f7607f1bfc6808a404b011f4 100755
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -2725,8 +2725,8 @@ public class GTURTLEModeling {
}
// System.out.println(tmlm.securityTaskMap);
for (SecurityPattern sp: tmlm.securityTaskMap.keySet()){
- if (sp.type.contains("Encryption") || sp.type.equals("MAC")){
- TraceManager.addDev("Finding security "+sp);
+ if (sp.type.contains("Symmetric Encryption") || sp.type.equals("MAC")){
+ TraceManager.addDev("Adding keys for "+sp.name);
for (TMLTask t:tmlm.securityTaskMap.get(sp)){
ArrayList<HwMemory> mems = new ArrayList<HwMemory>();
boolean keyFound=false;
@@ -2796,6 +2796,76 @@ public class GTURTLEModeling {
}
}
}
+ else if (sp.type.contains("Asymmetric Encryption")){
+ for (TMLTask t:tmlm.securityTaskMap.get(sp)){
+ ArrayList<HwMemory> mems = new ArrayList<HwMemory>();
+ boolean keyFound=false;
+ HwExecutionNode node1 = (HwExecutionNode) tmap.getHwNodeOf(t);
+ //Try to find memory using only private buses
+ List<HwNode> toVisit = new ArrayList<HwNode>();
+ // List<HwNode> toMemory = new ArrayList<HwNode>();
+ List<HwNode> complete = new ArrayList<HwNode>();
+ for (HwLink link:links){
+ if (link.hwnode==node1){
+ if (link.bus.privacy==1){
+ toVisit.add(link.bus);
+ }
+ }
+ }
+ memloop:
+ while (toVisit.size()>0){
+ HwNode curr = toVisit.remove(0);
+ for (HwLink link: links){
+ if (curr == link.bus){
+ if (link.hwnode instanceof HwMemory){
+ mems.add((HwMemory) link.hwnode);
+ TMLArchiMemoryNode memNode= (TMLArchiMemoryNode) listE.getTG(link.hwnode);
+ ArrayList<TMLArchiKey> keys = memNode.getKeyList();
+ String patternString= "";
+ for (TMLArchiKey key: keys){
+ if (key.getValue().equals(sp.name)){
+
+ keyFound=true;
+ break memloop;
+ }
+ patternString += key.getValue();
+ patternString += " ";
+ }
+ TraceManager.addDev("Memory "+ link.hwnode.getName() + " has currently mapped: " + patternString);
+ }
+ if (!complete.contains(link.hwnode) && !toVisit.contains(link.hwnode) && link.hwnode instanceof HwBridge){
+ toVisit.add(link.hwnode);
+ }
+ }
+ else if (curr == link.hwnode){
+ if (!complete.contains(link.bus) && !toVisit.contains(link.bus)){
+ toVisit.add(link.bus);
+ }
+ }
+ }
+ complete.add(curr);
+ }
+ if (!keyFound){
+ if (mems.size()>0){
+ TMLArchiMemoryNode memNode= (TMLArchiMemoryNode) listE.getTG(mems.get(0));
+ TMLArchiKey key = new TMLArchiKey(memNode.x, memNode.y, memNode.tdp.getMinX(), memNode.tdp.getMaxX(), memNode.tdp.getMinY(), memNode.tdp.getMaxY(), false, memNode, memNode.tdp);
+ key.setReferenceKey(sp.name);
+ key.makeFullValue();
+ TraceManager.addDev("Adding " +sp.name+ " key to " +memNode.getName());
+ TraceManager.addDev("Adding " +sp + " key to " +memNode.getName());
+ memNode.tdp.addComponent(key, memNode.x, memNode.y, true,true);
+ memNode.tdp.repaint();
+ }
+ else {
+ System.out.println("Can't map key to memory for " + sp.name + " on task " + t.getName());
+ UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Cannot map key in memory for " + sp.name + " on task " + t.getName());
+ ce.setTDiagramPanel(tmap.getCorrespondanceList().getTG(tmap.getArch().getFirstCPU()).getTDiagramPanel());
+ ce.setTGComponent(null);
+ checkingErrors.add(ce);
+ }
+ }
+ }
+ }
}
TraceManager.addDev("Mapping finished");
}