diff --git a/modeling/modelsForTestingTTool/testdiplo.xml b/modeling/modelsForTestingTTool/testdiplo.xml
index bfe0d7def72822cb7b3c9f381e0785a6e575cac8..7e8fe19360c98259493ed4bb15ee81492ff631d1 100644
--- a/modeling/modelsForTestingTTool/testdiplo.xml
+++ b/modeling/modelsForTestingTTool/testdiplo.xml
@@ -8,8 +8,8 @@
<cdparam x="202" y="135" />
<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="202" y="135" id="89" />
-<P2 x="716" y="122" id="74" />
+<P1 x="202" y="135" id="95" />
+<P2 x="716" y="122" id="78" />
<Point x="494" y="61" />
<AutomaticDrawing data="true" />
</CONNECTOR><SUBCOMPONENT type="-1" id="1" >
@@ -26,14 +26,14 @@
<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="1041" y="214" id="11" />
-<P2 x="279" y="167" id="95" />
+<P2 x="279" y="167" id="89" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="126" id="4" >
<cdparam x="662" y="349" />
<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="875" y="362" id="63" />
+<P1 x="875" y="362" id="59" />
<P2 x="1019" y="214" id="12" />
<AutomaticDrawing data="true" />
</CONNECTOR>
@@ -41,7 +41,7 @@
<cdparam x="665" 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="878" y="145" id="78" />
+<P1 x="878" y="145" id="74" />
<P2 x="1024" y="205" id="14" />
<AutomaticDrawing data="true" />
</CONNECTOR>
@@ -57,7 +57,7 @@
<cdparam x="236" y="311" />
<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="236" y="285" id="93" />
+<P1 x="236" y="285" id="91" />
<P2 x="411" y="460" id="27" />
<AutomaticDrawing data="true" />
</CONNECTOR>
@@ -66,7 +66,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="424" y="229" id="48" />
-<P2 x="675" y="395" id="59" />
+<P2 x="675" y="395" id="63" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<CONNECTOR type="126" id="9" >
@@ -81,7 +81,7 @@
<cdparam x="292" y="207" />
<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="279" y="218" id="91" />
+<P1 x="279" y="218" id="93" />
<P2 x="408" y="221" id="43" />
<AutomaticDrawing data="true" />
</CONNECTOR>
@@ -174,14 +174,14 @@
</COMPONENT>
<SUBCOMPONENT type="1203" id="60" >
<father id="73" num="0" />
-<cdparam x="662" y="395" />
+<cdparam x="862" y="362" />
<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="137" />
-<infoparam name="Primitive port" value="Event evt2" />
+<infoparam name="Primitive port" value="Event jevt2" />
<TGConnectingPoint num="0" id="59" />
<extraparam>
-<Prop commName="evt2" 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" />
+<Prop commName="jevt2" 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" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -208,14 +208,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="64" >
<father id="73" num="2" />
-<cdparam x="862" y="362" />
+<cdparam x="662" y="395" />
<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="137" />
-<infoparam name="Primitive port" value="Event jevt2" />
+<infoparam name="Primitive port" value="Event evt2" />
<TGConnectingPoint num="0" id="63" />
<extraparam>
-<Prop commName="jevt2" 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" />
+<Prop commName="evt2" 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" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -244,15 +244,15 @@
</COMPONENT>
<SUBCOMPONENT type="1203" id="75" >
<father id="88" num="0" />
-<cdparam x="703" y="122" />
+<cdparam x="865" y="145" />
<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="137" />
-<infoparam name="Primitive port" value="Event comm" />
+<infoparam name="Primitive port" value="Event jevt1" />
<TGConnectingPoint num="0" id="74" />
<extraparam>
-<Prop commName="comm" 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" />
-<Type type="1" typeOther="" />
+<Prop commName="jevt1" 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" />
+<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -278,15 +278,15 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="79" >
<father id="88" num="2" />
-<cdparam x="865" y="145" />
+<cdparam x="703" y="122" />
<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="137" />
-<infoparam name="Primitive port" value="Event jevt1" />
+<infoparam name="Primitive port" value="Event comm" />
<TGConnectingPoint num="0" id="78" />
<extraparam>
-<Prop commName="jevt1" 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" />
-<Type type="0" typeOther="" />
+<Prop commName="comm" 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" />
+<Type type="1" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -314,15 +314,15 @@
</COMPONENT>
<SUBCOMPONENT type="1203" id="90" >
<father id="105" num="0" />
-<cdparam x="189" y="135" />
+<cdparam x="266" y="167" />
<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="137" />
-<infoparam name="Primitive port" value="Event testEvt" />
+<infoparam name="Primitive port" value="Event jevt" />
<TGConnectingPoint num="0" id="89" />
<extraparam>
-<Prop commName="testEvt" 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" />
-<Type type="1" typeOther="" />
+<Prop commName="jevt" 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" />
+<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -331,14 +331,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="92" >
<father id="105" num="1" />
-<cdparam x="266" y="218" />
+<cdparam x="223" y="285" />
<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="137" />
-<infoparam name="Primitive port" value="Event evsrc" />
+<infoparam name="Primitive port" value="Channel ch1" />
<TGConnectingPoint num="0" id="91" />
<extraparam>
-<Prop commName="evsrc" 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" />
+<Prop commName="ch1" 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" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -348,14 +348,14 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="94" >
<father id="105" num="2" />
-<cdparam x="223" y="285" />
+<cdparam x="266" y="218" />
<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="137" />
-<infoparam name="Primitive port" value="Channel ch1" />
+<infoparam name="Primitive port" value="Event evsrc" />
<TGConnectingPoint num="0" id="93" />
<extraparam>
-<Prop commName="ch1" 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" />
+<Prop commName="evsrc" 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" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -365,15 +365,15 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1203" id="96" >
<father id="105" num="3" />
-<cdparam x="266" y="167" />
+<cdparam x="189" y="135" />
<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="137" />
-<infoparam name="Primitive port" value="Event jevt" />
+<infoparam name="Primitive port" value="Event testEvt" />
<TGConnectingPoint num="0" id="95" />
<extraparam>
-<Prop commName="jevt" 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" />
-<Type type="0" typeOther="" />
+<Prop commName="testEvt" 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" />
+<Type type="1" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -1293,7 +1293,7 @@
<cdparam x="579" y="395" />
<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="666" y="385" id="352" />
+<P1 x="653" y="398" id="352" />
<P2 x="487" y="255" id="319" />
<AutomaticDrawing data="true" />
</CONNECTOR>
@@ -1301,7 +1301,7 @@
<cdparam x="574" y="163" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<infoparam name="connector" value="Connector between ports" />
-<P1 x="669" y="150" id="330" />
+<P1 x="656" y="163" id="330" />
<P2 x="487" y="238" id="317" />
<AutomaticDrawing data="true" />
</CONNECTOR>
@@ -1310,7 +1310,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="504" y="247" id="314" />
-<P2 x="363" y="151" id="341" />
+<P2 x="376" y="164" id="341" />
<AutomaticDrawing data="true" />
</CONNECTOR>
<COMPONENT type="1208" id="329" >
@@ -1449,8 +1449,8 @@
<TMLActivityDiagramPanel name="T1" minX="10" maxX="2500" minY="10" maxY="1500" >
<COMPONENT type="1008" id="365" >
-<cdparam x="176" y="106" />
-<sizeparam width="71" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="177" y="106" />
+<sizeparam width="68" 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="comm1(x)" />
@@ -1501,8 +1501,8 @@
<TMLActivityDiagramPanel name="T0" minX="10" maxX="2500" minY="10" maxY="1500" >
<COMPONENT type="1010" id="374" >
-<cdparam x="384" y="131" />
-<sizeparam width="75" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="385" y="131" />
+<sizeparam width="72" 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="wait event" value="comm0(x) " />
@@ -1553,8 +1553,8 @@
<TMLActivityDiagramPanel name="T2" minX="10" maxX="2500" minY="10" maxY="1500" >
<COMPONENT type="1008" id="383" >
-<cdparam x="468" y="113" />
-<sizeparam width="71" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="469" y="113" />
+<sizeparam width="68" 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="comm2(x)" />
@@ -1647,11 +1647,11 @@
</COMPONENT>
<SUBCOMPONENT type="1101" id="398" >
<father id="441" num="0" />
-<cdparam x="445" y="269" />
-<sizeparam width="109" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="413" y="213" />
+<sizeparam width="106" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="141" minY="0" maxY="160" />
-<infoparam name="TGComponent" value="Design3::T2" />
+<cdrectangleparam minX="0" maxX="144" minY="0" maxY="160" />
+<infoparam name="TGComponent" value="Design3::T1" />
<TGConnectingPoint num="0" id="390" />
<TGConnectingPoint num="1" id="391" />
<TGConnectingPoint num="2" id="392" />
@@ -1661,15 +1661,15 @@
<TGConnectingPoint num="6" id="396" />
<TGConnectingPoint num="7" id="397" />
<extraparam>
-<info value="Design3::T2" taskName="T2" referenceTaskName="Design3" priority="0" operation="TMLComp_2" fatherComponentMECType="0" />
+<info value="Design3::T1" taskName="T1" referenceTaskName="Design3" priority="0" operation="TMLComp_2" fatherComponentMECType="0" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="1101" id="407" >
<father id="441" num="1" />
<cdparam x="405" y="170" />
-<sizeparam width="109" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<sizeparam width="106" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="141" minY="0" maxY="160" />
+<cdrectangleparam minX="0" maxX="144" minY="0" maxY="160" />
<infoparam name="TGComponent" value="Design3::T0" />
<TGConnectingPoint num="0" id="399" />
<TGConnectingPoint num="1" id="400" />
@@ -1685,11 +1685,11 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1101" id="416" >
<father id="441" num="2" />
-<cdparam x="413" y="213" />
-<sizeparam width="109" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="445" y="269" />
+<sizeparam width="106" height="40" minWidth="100" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
-<cdrectangleparam minX="0" maxX="141" minY="0" maxY="160" />
-<infoparam name="TGComponent" value="Design3::T1" />
+<cdrectangleparam minX="0" maxX="144" minY="0" maxY="160" />
+<infoparam name="TGComponent" value="Design3::T2" />
<TGConnectingPoint num="0" id="408" />
<TGConnectingPoint num="1" id="409" />
<TGConnectingPoint num="2" id="410" />
@@ -1699,7 +1699,7 @@
<TGConnectingPoint num="6" id="414" />
<TGConnectingPoint num="7" id="415" />
<extraparam>
-<info value="Design3::T1" taskName="T1" referenceTaskName="Design3" priority="0" operation="TMLComp_2" fatherComponentMECType="0" />
+<info value="Design3::T2" taskName="T2" referenceTaskName="Design3" priority="0" operation="TMLComp_2" fatherComponentMECType="0" />
</extraparam>
</SUBCOMPONENT>
@@ -1828,6 +1828,14 @@
<Modeling type="TML Component Design" nameTab="Design5" >
<TMLComponentTaskDiagramPanel name="TML Component Task Diagram" minX="10" maxX="2500" minY="10" maxY="1500" channels="true" events="true" requests="true" zoom="1.0" >
+<CONNECTOR type="126" id="575" >
+<cdparam x="408" y="185" />
+<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="408" y="185" id="564" />
+<P2 x="631" y="177" id="574" />
+<AutomaticDrawing data="true" />
+</CONNECTOR>
<CONNECTOR type="126" id="477" >
<cdparam x="408" y="226" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -1853,8 +1861,25 @@
<extraparam>
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="1203" id="479" >
+<SUBCOMPONENT type="1203" id="565" >
<father id="488" num="0" />
+<cdparam x="631" y="164" />
+<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="137" />
+<infoparam name="Primitive port" value="Channel comm" />
+<TGConnectingPoint num="0" id="574" />
+<extraparam>
+<Prop commName="evt" 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" />
+<Type type="0" typeOther="" />
+<Type type="0" typeOther="" />
+<Type type="0" typeOther="" />
+<Type type="0" typeOther="" />
+<Type type="0" typeOther="" />
+</extraparam>
+</SUBCOMPONENT>
+<SUBCOMPONENT type="1203" id="479" >
+<father id="488" num="1" />
<cdparam x="631" y="202" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
@@ -1862,7 +1887,7 @@
<infoparam name="Primitive port" value="Channel comm" />
<TGConnectingPoint num="0" id="478" />
<extraparam>
-<Prop commName="comm" 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" />
+<Prop commName="comm" 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" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -1888,8 +1913,25 @@
<extraparam>
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="1203" id="490" >
+<SUBCOMPONENT type="1203" id="555" >
<father id="499" num="0" />
+<cdparam x="382" y="172" />
+<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="137" />
+<infoparam name="Primitive port" value="Channel comm" />
+<TGConnectingPoint num="0" id="564" />
+<extraparam>
+<Prop commName="evt" 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" />
+<Type type="0" typeOther="" />
+<Type type="0" typeOther="" />
+<Type type="0" typeOther="" />
+<Type type="0" typeOther="" />
+<Type type="0" typeOther="" />
+</extraparam>
+</SUBCOMPONENT>
+<SUBCOMPONENT type="1203" id="490" >
+<father id="499" num="1" />
<cdparam x="382" y="213" />
<sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
@@ -1897,7 +1939,7 @@
<infoparam name="Primitive port" value="Channel comm" />
<TGConnectingPoint num="0" id="489" />
<extraparam>
-<Prop commName="comm" commType="0" origin="true" finite="false" blocking="false" maxSamples="8" widthSamples="4" isLossy="false" isPrex="false" isPostex="false" lossPercentage="0" maxNbOfLoss="0" dataFlowType="VOID" associatedEvent="VOID" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" />
+<Prop commName="comm" 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" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
<Type type="0" typeOther="" />
@@ -2021,12 +2063,99 @@
<MainCode value="void __user_init() {"/>
<MainCode value="}"/>
<Optimized value="true" />
-<Validated value="" />
+<Validated value="Block0;" />
<Ignored value="" />
+<COMPONENT type="5000" id="542" >
+<cdparam x="156" y="114" />
+<sizeparam width="250" height="200" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<hidden value="false" />
+<cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" />
+<infoparam name="Block0" value="Block0" />
+<TGConnectingPoint num="0" id="518" />
+<TGConnectingPoint num="1" id="519" />
+<TGConnectingPoint num="2" id="520" />
+<TGConnectingPoint num="3" id="521" />
+<TGConnectingPoint num="4" id="522" />
+<TGConnectingPoint num="5" id="523" />
+<TGConnectingPoint num="6" id="524" />
+<TGConnectingPoint num="7" id="525" />
+<TGConnectingPoint num="8" id="526" />
+<TGConnectingPoint num="9" id="527" />
+<TGConnectingPoint num="10" id="528" />
+<TGConnectingPoint num="11" id="529" />
+<TGConnectingPoint num="12" id="530" />
+<TGConnectingPoint num="13" id="531" />
+<TGConnectingPoint num="14" id="532" />
+<TGConnectingPoint num="15" id="533" />
+<TGConnectingPoint num="16" id="534" />
+<TGConnectingPoint num="17" id="535" />
+<TGConnectingPoint num="18" id="536" />
+<TGConnectingPoint num="19" id="537" />
+<TGConnectingPoint num="20" id="538" />
+<TGConnectingPoint num="21" id="539" />
+<TGConnectingPoint num="22" id="540" />
+<TGConnectingPoint num="23" id="541" />
+<extraparam>
+<CryptoBlock value="false" />
+<Attribute access="0" id="x" value="1" type="8" typeOther="" />
+</extraparam>
+</COMPONENT>
+
</AVATARBlockDiagramPanel>
+<AVATARStateMachineDiagramPanel name="Block0" minX="10" maxX="2500" minY="10" maxY="1500" >
+<CONNECTOR type="5102" id="549" >
+<cdparam x="407" y="70" />
+<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<infoparam name="connector" value="null" />
+<TGConnectingPoint num="0" id="548" />
+<P1 x="407" y="70" id="552" />
+<P2 x="394" y="131" id="550" />
+<AutomaticDrawing data="true" />
+</CONNECTOR><SUBCOMPONENT type="-1" id="547" >
+<father id="549" num="0" />
+<cdparam x="400" y="100" />
+<sizeparam width="58" height="15" 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="List of all parameters of an Avatar SMD transition" value="" />
+<TGConnectingPoint num="0" id="543" />
+<TGConnectingPoint num="1" id="544" />
+<TGConnectingPoint num="2" id="545" />
+<TGConnectingPoint num="3" id="546" />
+<extraparam>
+<guard value="[ ]" />
+<afterMin value="" />
+<afterMax value="" />
+<computeMin value="" />
+<computeMax value="" />
+<actions value="x = x + 1" />
+</extraparam>
+</SUBCOMPONENT>
+
+<COMPONENT type="5101" id="551" >
+<cdparam x="384" y="136" />
+<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="550" />
+</COMPONENT>
+
+<COMPONENT type="5100" id="553" >
+<cdparam x="400" y="50" />
+<sizeparam width="15" height="15" 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="start state" value="null" />
+<TGConnectingPoint num="0" id="552" />
+</COMPONENT>
+
+
+</AVATARStateMachineDiagramPanel>
+
</Modeling>
diff --git a/src/tmltranslator/TMLModeling.java b/src/tmltranslator/TMLModeling.java
index 1be87364ef8894b49c708279302d8c48acaa0bb3..1a0ebe81fd446289ab7d9f193c37a728e7f39ddf 100755
--- a/src/tmltranslator/TMLModeling.java
+++ b/src/tmltranslator/TMLModeling.java
@@ -56,6 +56,9 @@ import proverifspec.*;
public class TMLModeling {
+
+ public final String SEP1 = "_S_";
+
private List<TMLTask> tasks;
private List<TMLChannel> channels;
private List<TMLRequest> requests;
@@ -2009,7 +2012,7 @@ public class TMLModeling {
int i;
// Create the new task and its activity diagram
- TMLTask forkTask = new TMLTask("FORKTASK__" + _ch.getName(), _ch.getReferenceObject(), null);
+ TMLTask forkTask = new TMLTask("FORKTASK" + SEP1 + _ch.getName(), _ch.getReferenceObject(), null);
TMLActivity forkActivity = forkTask.getActivityDiagram();
addTask(forkTask);
@@ -2017,9 +2020,9 @@ public class TMLModeling {
int nb = _ch.getDestinationTasks().size();
TMLChannel[] chans = new TMLChannel[nb];
for(i=0; i<nb; i++) {
- chans[i] = new TMLChannel("FORKCHANNEL__" + i + "__" + _ch.getName(), _ch.getReferenceObject());
+ chans[i] = new TMLChannel("FORKCHANNEL" + SEP1 + i + SEP1 + _ch.getName(), _ch.getReferenceObject());
chans[i].setTasks(forkTask, _ch.getDestinationTasks().get(i));
- chans[i].setPorts(new TMLPort("FORKPORTORIGIN__" + i + "__" + _ch.getName(), _ch.getReferenceObject()), _ch.getDestinationPorts().get(i));
+ chans[i].setPorts(new TMLPort("FORKPORTORIGIN" + SEP1 + i + SEP1 + _ch.getName(), _ch.getReferenceObject()), _ch.getDestinationPorts().get(i));
chans[i].setType(_ch.getType());
chans[i].setMax(_ch.getMax());
chans[i].setSize(_ch.getSize());
@@ -2035,7 +2038,7 @@ public class TMLModeling {
// Transform the original channel into a basic channel
_ch.setTasks(_ch.getOriginTasks().get(0), forkTask);
- _ch.setPorts(_ch.getOriginPorts().get(0), new TMLPort("FORKPORTDESTINATION__" + _ch.getName(), _ch.getReferenceObject()));
+ _ch.setPorts(_ch.getOriginPorts().get(0), new TMLPort("FORKPORTDESTINATION" + SEP1 + _ch.getName(), _ch.getReferenceObject()));
_ch.removeComplexInformations();
// Make the activity diagram of the fork task
@@ -2059,7 +2062,7 @@ public class TMLModeling {
TMLWriteChannel []writes = new TMLWriteChannel[nb];
for(i=0; i<nb; i++) {
- writes[i] = new TMLWriteChannel("WriteOfFork__" + i, null);
+ writes[i] = new TMLWriteChannel("WriteOfFork" + SEP1 + i, null);
writes[i].addChannel(chans[i]);
writes[i].setNbOfSamples("1");
forkActivity.addElement(writes[i]);
@@ -2081,7 +2084,7 @@ public class TMLModeling {
int i, j;
// Create the new task and its activity diagram
- TMLTask forkTask = new TMLTask("FORKTASK__EVT__" + _evt.getName(), _evt.getReferenceObject(), null);
+ TMLTask forkTask = new TMLTask("FORKTASK" + SEP1 + "EVT" + SEP1 + _evt.getName(), _evt.getReferenceObject(), null);
TMLActivity forkActivity = forkTask.getActivityDiagram();
addTask(forkTask);
@@ -2089,9 +2092,9 @@ public class TMLModeling {
int nb = _evt.getDestinationTasks().size();
TMLEvent[] evts = new TMLEvent[nb];
for(i=0; i<nb; i++) {
- evts[i] = new TMLEvent("FORKEVENT__" + i + "__" + _evt.getName(), _evt.getReferenceObject(), _evt.getMaxSize(), _evt.isBlocking());
+ evts[i] = new TMLEvent("FORKEVENT" + SEP1 + i + SEP1 + _evt.getName(), _evt.getReferenceObject(), _evt.getMaxSize(), _evt.isBlocking());
evts[i].setTasks(forkTask, _evt.getDestinationTasks().get(i));
- evts[i].setPorts(new TMLPort("FORKPORTORIGIN__" + i + "__" + _evt.getName(), _evt.getReferenceObject()), _evt.getDestinationPorts().get(i));
+ evts[i].setPorts(new TMLPort("FORKPORTORIGIN" + SEP1 + i + SEP1 + _evt.getName(), _evt.getReferenceObject()), _evt.getDestinationPorts().get(i));
//evts[i].setType(_evt.getType());
//evts[i].setMax(_evt.getMax());
//evts[i].setSize(_evt.getSize());
@@ -2110,7 +2113,7 @@ public class TMLModeling {
// Transform the original event into a basic event
_evt.setTasks(_evt.getOriginTasks().get(0), forkTask);
- _evt.setPorts(_evt.getOriginPorts().get(0), new TMLPort("FORKPORTDESTINATION__" + _evt.getName(), _evt.getReferenceObject()));
+ _evt.setPorts(_evt.getOriginPorts().get(0), new TMLPort("FORKPORTDESTINATION" + SEP1 + _evt.getName(), _evt.getReferenceObject()));
_evt.removeComplexInformations();
// Adding attributes to the task
@@ -2127,10 +2130,10 @@ public class TMLModeling {
TMLStopState stop2 = new TMLStopState("stop2OfFork", null);
forkActivity.addElement(stop2);
TMLForLoop junction = new TMLForLoop("junctionOfFork", null);
- junction.setInit("fork__i=0");
- junction.setCondition("fork__i<1");
- junction.setIncrement("fork__i=fork__i");
- TMLAttribute attr = new TMLAttribute("fork__i", "fork__i", new TMLType(TMLType.NATURAL), "0");
+ junction.setInit("fork" + SEP1 + "i=0");
+ junction.setCondition("fork" + SEP1 + "i<1");
+ junction.setIncrement("fork" + SEP1 + "i=fork__i");
+ TMLAttribute attr = new TMLAttribute("fork" + SEP1 + "i", "fork" + SEP1 +"i", new TMLType(TMLType.NATURAL), "0");
forkTask.addAttribute(attr);
forkActivity.addElement(junction);
TMLWaitEvent read = new TMLWaitEvent("WaitOfFork", null);
@@ -2143,7 +2146,7 @@ public class TMLModeling {
TMLSendEvent []writes = new TMLSendEvent[nb];
for(i=0; i<nb; i++) {
- writes[i] = new TMLSendEvent("WriteEvtOfFork__" + i, null);
+ writes[i] = new TMLSendEvent("WriteEvtOfFork" + SEP1 + i, null);
writes[i].setEvent(evts[i]);
for(j=0; j<_evt.getNbOfParams(); j++) {
writes[i].addParam("attr_" + j);
@@ -2198,7 +2201,7 @@ public class TMLModeling {
int i;
// Create the new task and its activity diagram
- TMLTask joinTask = new TMLTask("JOINTASK__" + _ch.getName(), _ch.getReferenceObject(), null);
+ TMLTask joinTask = new TMLTask("JOINTASK" + SEP1 + _ch.getName(), _ch.getReferenceObject(), null);
TMLActivity joinActivity = joinTask.getActivityDiagram();
addTask(joinTask);
@@ -2206,9 +2209,9 @@ public class TMLModeling {
int nb = _ch.getOriginTasks().size();
TMLChannel[] chans = new TMLChannel[nb];
for(i=0; i<nb; i++) {
- chans[i] = new TMLChannel("JOINCHANNEL__" + i + "__" + _ch.getName(), _ch.getReferenceObject());
+ chans[i] = new TMLChannel("JOINCHANNEL" + SEP1 + i + "__" + _ch.getName(), _ch.getReferenceObject());
chans[i].setTasks(_ch.getOriginTasks().get(i), joinTask);
- chans[i].setPorts(_ch.getOriginPorts().get(i), new TMLPort("JOINPORTDESTINATION__" + i + "__" + _ch.getName(), _ch.getReferenceObject()));
+ chans[i].setPorts(_ch.getOriginPorts().get(i), new TMLPort("JOINPORTDESTINATION" + SEP1 + i + SEP1 + _ch.getName(), _ch.getReferenceObject()));
chans[i].setType(_ch.getType());
chans[i].setMax(_ch.getMax());
chans[i].setSize(_ch.getSize());
@@ -2224,7 +2227,7 @@ public class TMLModeling {
// Transform the original channel into a basic channel
_ch.setTasks(joinTask, _ch.getDestinationTasks().get(0));
- _ch.setPorts(new TMLPort("JOINPORTORIGIN__" + _ch.getName(), _ch.getReferenceObject()), _ch.getDestinationPorts().get(0));
+ _ch.setPorts(new TMLPort("JOINPORTORIGIN" + SEP1 + _ch.getName(), _ch.getReferenceObject()), _ch.getDestinationPorts().get(0));
_ch.removeComplexInformations();
// Make the activity diagram of the fork task
@@ -2248,7 +2251,7 @@ public class TMLModeling {
TMLReadChannel []reads = new TMLReadChannel[nb];
for(i=0; i<nb; i++) {
- reads[i] = new TMLReadChannel("ReadOfJoin__" + i, null);
+ reads[i] = new TMLReadChannel("ReadOfJoin" + SEP1 + i, null);
reads[i].addChannel(chans[i]);
reads[i].setNbOfSamples("1");
joinActivity.addElement(reads[i]);
@@ -2269,7 +2272,7 @@ public class TMLModeling {
int i, j;
// Create the new task and its activity diagram
- TMLTask joinTask = new TMLTask("JOINTASK__EVT__" + _evt.getName(), _evt.getReferenceObject(), null);
+ TMLTask joinTask = new TMLTask("JOINTASK" + SEP1 + "EVT" + SEP1 + _evt.getName(), _evt.getReferenceObject(), null);
TMLActivity joinActivity = joinTask.getActivityDiagram();
addTask(joinTask);
@@ -2277,9 +2280,9 @@ public class TMLModeling {
int nb = _evt.getOriginTasks().size();
TMLEvent[] evts = new TMLEvent[nb];
for(i=0; i<nb; i++) {
- evts[i] = new TMLEvent("JOINEVENT__" + i + "__" + _evt.getName(), _evt.getReferenceObject(), _evt.getMaxSize(), _evt.isBlocking());
+ evts[i] = new TMLEvent("JOINEVENT" + SEP1 + i + SEP1 + _evt.getName(), _evt.getReferenceObject(), _evt.getMaxSize(), _evt.isBlocking());
evts[i].setTasks(_evt.getOriginTasks().get(i), joinTask);
- evts[i].setPorts(_evt.getOriginPorts().get(i), new TMLPort("JOINPORTDESTINATION__" + i + "__" + _evt.getName(), _evt.getReferenceObject()));
+ evts[i].setPorts(_evt.getOriginPorts().get(i), new TMLPort("JOINPORTDESTINATION" + SEP1 + i + SEP1 + _evt.getName(), _evt.getReferenceObject()));
for(j=0; j<_evt.getNbOfParams(); j++) {
evts[i].addParam(_evt.getType(j));
}
@@ -2295,7 +2298,7 @@ public class TMLModeling {
// Transform the original channel into a basic channel
_evt.setTasks(joinTask, _evt.getDestinationTasks().get(0));
- _evt.setPorts(new TMLPort("JOINPORTORIGIN__" + _evt.getName(), _evt.getReferenceObject()), _evt.getDestinationPorts().get(0));
+ _evt.setPorts(new TMLPort("JOINPORTORIGIN" + SEP1 + _evt.getName(), _evt.getReferenceObject()), _evt.getDestinationPorts().get(0));
_evt.removeComplexInformations();
// Adding attributes to the task
@@ -2312,10 +2315,10 @@ public class TMLModeling {
TMLStopState stop2 = new TMLStopState("stop2OfFork", null);
joinActivity.addElement(stop2);
TMLForLoop junction = new TMLForLoop("junctionOfJoin", null);
- junction.setInit("join__i=0");
- junction.setCondition("join__i<1");
- junction.setIncrement("join__i=join__i");
- TMLAttribute attr = new TMLAttribute("join__i", "join__i", new TMLType(TMLType.NATURAL), "0");
+ junction.setInit("join" + SEP1 + "i=0");
+ junction.setCondition("join" + SEP1 + "i<1");
+ junction.setIncrement("join" + SEP1 + "i=join" + SEP1 + "i");
+ TMLAttribute attr = new TMLAttribute("join" + SEP1 +"i", "join" + SEP1 + "i", new TMLType(TMLType.NATURAL), "0");
joinTask.addAttribute(attr);
joinActivity.addElement(junction);
TMLSendEvent notify = new TMLSendEvent("NotifyOfJoin", null);
@@ -2327,7 +2330,7 @@ public class TMLModeling {
TMLWaitEvent []waits = new TMLWaitEvent[nb];
for(i=0; i<nb; i++) {
- waits[i] = new TMLWaitEvent("WaitOfJoin__" + i, null);
+ waits[i] = new TMLWaitEvent("WaitOfJoin" + SEP1 + i, null);
waits[i].setEvent(evts[i]);
for(j=0; j<_evt.getNbOfParams(); j++) {
waits[i].addParam("attr_" + j);
diff --git a/src/tmltranslator/touppaal/TML2UPPAAL.java b/src/tmltranslator/touppaal/TML2UPPAAL.java
index c1950d6ccbe03d0112d54e7124bd2234390bc857..e73b550c573f775e11585715c28b0e48d05fff58 100755
--- a/src/tmltranslator/touppaal/TML2UPPAAL.java
+++ b/src/tmltranslator/touppaal/TML2UPPAAL.java
@@ -1,47 +1,47 @@
/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
-*
-* ludovic.apvrille AT enst.fr
-*
-* This software is a computer program whose purpose is to allow the
-* edition of TURTLE analysis, design and deployment diagrams, to
-* allow the generation of RT-LOTOS or Java code from this diagram,
-* and at last to allow the analysis of formal validation traces
-* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
-* from INRIA Rhone-Alpes.
-*
-* This software is governed by the CeCILL license under French law and
-* abiding by the rules of distribution of free software. You can use,
-* modify and/ or redistribute the software under the terms of the CeCILL
-* license as circulated by CEA, CNRS and INRIA at the following URL
-* "http://www.cecill.info".
-*
-* As a counterpart to the access to the source code and rights to copy,
-* modify and redistribute granted by the license, users are provided only
-* with a limited warranty and the software's author, the holder of the
-* economic rights, and the successive licensors have only limited
-* liability.
-*
-* In this respect, the user's attention is drawn to the risks associated
-* with loading, using, modifying and/or developing or reproducing the
-* software by the user in light of its specific status of free software,
-* that may mean that it is complicated to manipulate, and that also
-* therefore means that it is reserved for developers and experienced
-* professionals having in-depth computer knowledge. Users are therefore
-* encouraged to load and test the software's suitability as regards their
-* requirements in conditions enabling the security of their systems and/or
-* data to be ensured and, more generally, to use and operate it in the
-* same conditions as regards security.
-*
-* The fact that you are presently reading this means that you have had
-* knowledge of the CeCILL license and that you accept its terms.
-*
-* /**
-* Class TML2UPPAAL
-* Creation: 03/11/2006
-* @version 1.0 03/11/2006
-* @author Ludovic APVRILLE
-* @see
-*/
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *
+ * /**
+ * Class TML2UPPAAL
+ * Creation: 03/11/2006
+ * @version 1.0 03/11/2006
+ * @author Ludovic APVRILLE
+ * @see
+ */
package tmltranslator.touppaal;
@@ -53,20 +53,20 @@ import uppaaldesc.*;
public class TML2UPPAAL {
-
+
//private static int gateId;
-
+
private TMLModeling tmlmodeling;
private UPPAALSpec spec;
private RelationTMLUPPAAL rtu;
private UPPAALTemplate lossTemplate;
private Vector<String> lossNames;
-
- // private boolean debug;
+
+ // private boolean debug;
private int sizeInfiniteFIFO = DEFAULT_INFINITE_FIFO_SIZE;
-
+
private int currentX, currentY;
-
+
public final static int STEP_X = 0;
public final static int STEP_Y = 75;
public final static int STEP_LOOP_X = 75;
@@ -78,733 +78,732 @@ public class TML2UPPAAL {
public final static int ASSIGN_Y = 0;
public final static int GUARD_X = 0;
public final static int GUARD_Y = -20;
-
- public static final int DEFAULT_INFINITE_FIFO_SIZE = 1024;
-
-
+
+ public static final int DEFAULT_INFINITE_FIFO_SIZE = 1024;
+
+
public TML2UPPAAL(TMLModeling _tmlmodeling) {
tmlmodeling = _tmlmodeling;
- TraceManager.addDev("TML2UPPAAL");
+ TraceManager.addDev("TML2UPPAAL");
}
-
+
// Returns a list of all file names ..
public void saveInFile(String path) throws FileException {
FileUtils.saveFile(path + "spec.xml", spec.makeSpec());
//System.out.println("spec.xml generated:\n" + spec.getFullSpec());
}
-
- public void saveInPathFile(String PathFile) throws FileException {
+
+ public void saveInPathFile(String PathFile) throws FileException {
FileUtils.saveFile(PathFile, spec.makeSpec());
//System.out.println("spec.xml generated:\n" + spec.getFullSpec());
}
-
- public String getUPPAALSpec() {
- return spec.makeSpec();
- }
-
+
+ public String getUPPAALSpec() {
+ return spec.makeSpec();
+ }
+
public void print() {
/*// Print each automatas
- ListIterator iterator = automatas.listIterator();
- Automata aut;
-
- while(iterator.hasNext()) {
- aut = (Automata)(iterator.next());
- System.out.println("Automata: " + aut.getName());
- System.out.println(aut.toAUT());
- }*/
+ ListIterator iterator = automatas.listIterator();
+ Automata aut;
+
+ while(iterator.hasNext()) {
+ aut = (Automata)(iterator.next());
+ System.out.println("Automata: " + aut.getName());
+ System.out.println(aut.toAUT());
+ }*/
+ }
+
+ public void setSizeInfiniteFIFO(int _size) {
+ sizeInfiniteFIFO = _size;
+ }
+
+ public RelationTMLUPPAAL getRelationTMLUPPAAL() {
+ return rtu;
}
-
- public void setSizeInfiniteFIFO(int _size) {
- sizeInfiniteFIFO = _size;
- }
-
- public RelationTMLUPPAAL getRelationTMLUPPAAL() {
- return rtu;
- }
-
+
public UPPAALSpec generateUPPAAL(boolean _debug) {
- TraceManager.addDev("Generating UPPAAL Specification from TML");
- tmlmodeling.removeAllRandomSequences();
-
- // debug = _debug;
+ TraceManager.addDev("Generating UPPAAL Specification from TML");
+ tmlmodeling.removeAllRandomSequences();
+
+ // debug = _debug;
spec = new UPPAALSpec();
- rtu = new RelationTMLUPPAAL();
- lossTemplate = null;
-
+ rtu = new RelationTMLUPPAAL();
+ lossTemplate = null;
+
// Must fill spec!
-
+
makeGlobal();
makeChannels();
makeRequests();
makeEvents();
-
+
// Make tasks
makeTasks();
-
+
// Instanciation of the system
makeSystem();
-
- return spec;
-
+
+ return spec;
}
-
+
public void makeGlobal() {
- spec.addGlobalDeclaration("const int DEFAULT_INFINITE_SIZE = " + sizeInfiniteFIFO + ";\n\n");
- spec.addGlobalDeclaration("int min(int a, int b) {\nif (a<b) {\nreturn a;\n} else {\nreturn b;\n}\n}\n\n");
- spec.addGlobalDeclaration("int max(int a, int b) {\nif (a>b) {\nreturn a;\n} else {\nreturn b;\n}\n}\n\n");
-
+ spec.addGlobalDeclaration("const int DEFAULT_INFINITE_SIZE = " + sizeInfiniteFIFO + ";\n\n");
+ spec.addGlobalDeclaration("int min(int a, int b) {\nif (a<b) {\nreturn a;\n} else {\nreturn b;\n}\n}\n\n");
+ spec.addGlobalDeclaration("int max(int a, int b) {\nif (a>b) {\nreturn a;\n} else {\nreturn b;\n}\n}\n\n");
+
}
-
+
public void makeChannels() {
- Iterator<TMLChannel> iterator = tmlmodeling.getListIteratorChannels();
-
- while(iterator.hasNext()) {
- makeChannel(iterator.next());
- }
+ Iterator<TMLChannel> iterator = tmlmodeling.getListIteratorChannels();
+
+ while(iterator.hasNext()) {
+ makeChannel(iterator.next());
+ }
}
-
+
public void makeChannel(TMLChannel ch) {
- if (ch.getType() == TMLChannel.BRBW) {
-
- spec.addGlobalDeclaration("urgent chan rd__" + ch.getName() + ", wr__" + ch.getName() + ";\n");
- if (ch.isLossy()) {
- spec.addTemplate(new UPPAALFiniteFIFOTemplateLoss("channel__" + ch.getName(), ch.getName(), ch.getMax(), ch.getMaxNbOfLoss()));
- makeLoss("ch__" + ch.getName());
- } else {
- spec.addTemplate(new UPPAALFiniteFIFOTemplate("channel__" + ch.getName(), ch.getName(), ch.getMax()));
-
- }
- } else if (ch.getType() == TMLChannel.BRNBW) {
- spec.addGlobalDeclaration("urgent chan rd__" + ch.getName() + ", wr__" + ch.getName() + ";\n");
- if (ch.isLossy()) {
- spec.addTemplate(new UPPAALInfiniteFIFOTemplateLoss("channel__" + ch.getName(), ch.getName(), ch.getMaxNbOfLoss()));
- makeLoss("ch__" + ch.getName());
- } else {
- spec.addTemplate(new UPPAALInfiniteFIFOTemplate("channel__" + ch.getName(), ch.getName()));
- }
- } else if (ch.getType() == TMLChannel.NBRNBW) {
- spec.addGlobalDeclaration("urgent chan rd__" + ch.getName() + ", wr__" + ch.getName() + ";\n");
- if (ch.isLossy()) {
- spec.addTemplate(new UPPAALMemoryTemplateLoss("channel__" + ch.getName(), ch.getName(), ch.getMaxNbOfLoss()));
- makeLoss("ch__" + ch.getName());
- } else {
- spec.addTemplate(new UPPAALMemoryTemplate("channel__" + ch.getName(), ch.getName()));
- }
- }
+ if (ch.getType() == TMLChannel.BRBW) {
+
+ spec.addGlobalDeclaration("urgent chan rd__" + ch.getName() + ", wr__" + ch.getName() + ";\n");
+ if (ch.isLossy()) {
+ spec.addTemplate(new UPPAALFiniteFIFOTemplateLoss("channel__" + ch.getName(), ch.getName(), ch.getMax(), ch.getMaxNbOfLoss()));
+ makeLoss("ch__" + ch.getName());
+ } else {
+ spec.addTemplate(new UPPAALFiniteFIFOTemplate("channel__" + ch.getName(), ch.getName(), ch.getMax()));
+
+ }
+ } else if (ch.getType() == TMLChannel.BRNBW) {
+ spec.addGlobalDeclaration("urgent chan rd__" + ch.getName() + ", wr__" + ch.getName() + ";\n");
+ if (ch.isLossy()) {
+ spec.addTemplate(new UPPAALInfiniteFIFOTemplateLoss("channel__" + ch.getName(), ch.getName(), ch.getMaxNbOfLoss()));
+ makeLoss("ch__" + ch.getName());
+ } else {
+ spec.addTemplate(new UPPAALInfiniteFIFOTemplate("channel__" + ch.getName(), ch.getName()));
+ }
+ } else if (ch.getType() == TMLChannel.NBRNBW) {
+ spec.addGlobalDeclaration("urgent chan rd__" + ch.getName() + ", wr__" + ch.getName() + ";\n");
+ if (ch.isLossy()) {
+ spec.addTemplate(new UPPAALMemoryTemplateLoss("channel__" + ch.getName(), ch.getName(), ch.getMaxNbOfLoss()));
+ makeLoss("ch__" + ch.getName());
+ } else {
+ spec.addTemplate(new UPPAALMemoryTemplate("channel__" + ch.getName(), ch.getName()));
+ }
+ }
}
-
+
public void makeRequests() {
- Iterator<TMLRequest> iterator = tmlmodeling.getListIteratorRequests();
-
- while(iterator.hasNext()) {
- makeRequest( iterator.next() );
- }
+ Iterator<TMLRequest> iterator = tmlmodeling.getListIteratorRequests();
+
+ while(iterator.hasNext()) {
+ makeRequest( iterator.next() );
+ }
}
-
+
public void makeRequest(TMLRequest request) {
- for(int i=0; i<request.getNbOfParams(); i++) {
- spec.addGlobalDeclaration(request.getType(i).toString() + " head" + i + "__" + request.getName()+ ";\n");
- spec.addGlobalDeclaration(request.getType(i).toString() + " tail" + i + "__" + request.getName()+ ";\n");
- }
- spec.addGlobalDeclaration("urgent chan request__" + request.getName() + ", wait__" + request.getName() + ";\n");
- if (request.isLossy()) {
- TraceManager.addDev("Lossy req");
- spec.addTemplate(new UPPAALRequestTemplateWithLoss("ReqManager__" + request.getName(), request, "DEFAULT_INFINITE_SIZE", request.getMaxNbOfLoss()));
- makeLoss("req__" + request.getName());
- } else {
- TraceManager.addDev("Non lossy req");
- spec.addTemplate(new UPPAALRequestTemplate("ReqManager__" + request.getName(), request, "DEFAULT_INFINITE_SIZE"));
- }
+ for(int i=0; i<request.getNbOfParams(); i++) {
+ spec.addGlobalDeclaration(request.getType(i).toString() + " head" + i + "__" + request.getName()+ ";\n");
+ spec.addGlobalDeclaration(request.getType(i).toString() + " tail" + i + "__" + request.getName()+ ";\n");
+ }
+ spec.addGlobalDeclaration("urgent chan request__" + request.getName() + ", wait__" + request.getName() + ";\n");
+ if (request.isLossy()) {
+ TraceManager.addDev("Lossy req");
+ spec.addTemplate(new UPPAALRequestTemplateWithLoss("ReqManager__" + request.getName(), request, "DEFAULT_INFINITE_SIZE", request.getMaxNbOfLoss()));
+ makeLoss("req__" + request.getName());
+ } else {
+ TraceManager.addDev("Non lossy req");
+ spec.addTemplate(new UPPAALRequestTemplate("ReqManager__" + request.getName(), request, "DEFAULT_INFINITE_SIZE"));
+ }
}
-
+
public void makeEvents() {
- Iterator<TMLEvent> iterator = tmlmodeling.getListIteratorEvents();
-
- while(iterator.hasNext()) {
- makeEvent( iterator.next());
- }
+ Iterator<TMLEvent> iterator = tmlmodeling.getListIteratorEvents();
+
+ while(iterator.hasNext()) {
+ makeEvent( iterator.next());
+ }
}
-
+
public void makeEvent(TMLEvent event) {
- for(int i=0; i<event.getNbOfParams(); i++) {
- spec.addGlobalDeclaration(event.getType(i).toString() + " eventHead" + i + "__" + event.getName()+ ";\n");
- spec.addGlobalDeclaration(event.getType(i).toString() + " eventTail" + i + "__" + event.getName()+ ";\n");
- }
- spec.addGlobalDeclaration("urgent chan eventSend__" + event.getName() + ", eventNotify__" + event.getName() + ", eventNotified__" + event.getName()+ ";\n");
- spec.addGlobalDeclaration("int notified__" + event.getName() + ";\n");
- if (event.isLossy()) {
- spec.addTemplate(new UPPAALEventTemplateWithLoss("EvtManager__" + event.getName(), event, "DEFAULT_INFINITE_SIZE", event.getMaxNbOfLoss()));
- makeLoss("evt__" + event.getName());
- } else {
- spec.addTemplate(new UPPAALEventTemplate("EvtManager__" + event.getName(), event, "DEFAULT_INFINITE_SIZE"));
- }
+ for(int i=0; i<event.getNbOfParams(); i++) {
+ spec.addGlobalDeclaration(event.getType(i).toString() + " eventHead" + i + "__" + event.getName()+ ";\n");
+ spec.addGlobalDeclaration(event.getType(i).toString() + " eventTail" + i + "__" + event.getName()+ ";\n");
+ }
+ spec.addGlobalDeclaration("urgent chan eventSend__" + event.getName() + ", eventNotify__" + event.getName() + ", eventNotified__" + event.getName()+ ";\n");
+ spec.addGlobalDeclaration("int notified__" + event.getName() + ";\n");
+ if (event.isLossy()) {
+ spec.addTemplate(new UPPAALEventTemplateWithLoss("EvtManager__" + event.getName(), event, "DEFAULT_INFINITE_SIZE", event.getMaxNbOfLoss()));
+ makeLoss("evt__" + event.getName());
+ } else {
+ spec.addTemplate(new UPPAALEventTemplate("EvtManager__" + event.getName(), event, "DEFAULT_INFINITE_SIZE"));
+ }
}
-
+
public void makeTasks() {
- Iterator<TMLTask> iterator = tmlmodeling.getListIteratorTasks();
-
- while(iterator.hasNext()) {
- makeTask( iterator.next() );
- }
+ Iterator<TMLTask> iterator = tmlmodeling.getListIteratorTasks();
+
+ while(iterator.hasNext()) {
+ makeTask( iterator.next() );
+ }
}
-
+
public void makeTask(TMLTask task) {
- // We do not take into account if the task is requested or not
-
- // Generate template
- UPPAALTemplate template = new UPPAALTemplate();
- template.setName(task.getName());
- spec.addTemplate(template);
- rtu.addTMLTaskTemplate(task, template);
-
- // Attributes
- makeAttributes(task, template);
-
- // Behavior
- makeBehavior(task, template);
-
+ // We do not take into account if the task is requested or not
+
+ // Generate template
+ UPPAALTemplate template = new UPPAALTemplate();
+ template.setName(task.getName());
+ spec.addTemplate(template);
+ rtu.addTMLTaskTemplate(task, template);
+
+ // Attributes
+ makeAttributes(task, template);
+
+ // Behavior
+ makeBehavior(task, template);
+
}
-
+
public void makeAttributes(TMLTask task, UPPAALTemplate template) {
- Iterator<TMLAttribute> iterator = task.getAttributes().listIterator();
- TMLAttribute tmlatt;
-
- while(iterator.hasNext()) {
- tmlatt = iterator.next();
- if (tmlatt.hasInitialValue()) {
- template.addDeclaration(tmlatt.getType().toString() + " " + tmlatt.getName() + " = " + tmlatt.getInitialValue() +";\n");
- } else {
- template.addDeclaration(tmlatt.getType().toString() + " " + tmlatt.getName() + ";\n");
- }
- }
-
- template.addDeclaration("int nb__rd;\nint nb__wr;\n");
- if (task.isRequested()) {
- TMLRequest req = task.getRequest();
-
- //System.out.println(task.getAttributeString());
-
- for(int i=0; i<req.getNbOfParams(); i++) {
- if (task.getAttributeByName("arg" + (i+1) + "__req") == null) {
- //System.out.println("Adding attribute for the request:" + " arg" + (i+1) + "__req");
- template.addDeclaration(req.getType(i).toString() + "arg" + (i+1) + "__req;\n");
- }
- }
- }
-
- if (task.hasTMLRandom()) {
- template.addDeclaration("int min__random;\n");
- template.addDeclaration("int max__random;\n");
- }
+ Iterator<TMLAttribute> iterator = task.getAttributes().listIterator();
+ TMLAttribute tmlatt;
+
+ while(iterator.hasNext()) {
+ tmlatt = iterator.next();
+ if (tmlatt.hasInitialValue()) {
+ template.addDeclaration(tmlatt.getType().toString() + " " + tmlatt.getName() + " = " + tmlatt.getInitialValue() +";\n");
+ } else {
+ template.addDeclaration(tmlatt.getType().toString() + " " + tmlatt.getName() + ";\n");
+ }
+ }
+
+ template.addDeclaration("int nb__rd;\nint nb__wr;\n");
+ if (task.isRequested()) {
+ TMLRequest req = task.getRequest();
+
+ //System.out.println(task.getAttributeString());
+
+ for(int i=0; i<req.getNbOfParams(); i++) {
+ if (task.getAttributeByName("arg" + (i+1) + "__req") == null) {
+ //System.out.println("Adding attribute for the request:" + " arg" + (i+1) + "__req");
+ template.addDeclaration(req.getType(i).toString() + "arg" + (i+1) + "__req;\n");
+ }
+ }
+ }
+
+ if (task.hasTMLRandom()) {
+ template.addDeclaration("int min__random;\n");
+ template.addDeclaration("int max__random;\n");
+ }
}
-
+
public void makeBehavior(TMLTask task, UPPAALTemplate template) {
- // Request is not yet taken into account
- TMLActivityElement first = task.getActivityDiagram().getFirst();
-
- currentX = 0; currentY = -220;
-
- if (task.isRequested()) {
- UPPAALLocation loc, loc1;
- UPPAALTransition tr;
- loc = addLocation(template);
- template.setInitLocation(loc);
- loc1 = addLocation(template);
- tr = addTransition(template, loc, loc1);
- setSynchronization(tr, "wait__" + task.getRequest().getName() + "?");
- String s = "";
- for(int i=0; i<task.getRequest().getNbOfParams(); i++) {
- if (i!= 0) {
- s+= ",\n";
- }
- s += " arg" + (i+1) + "__req = head" + i + "__" + task.getRequest().getName();
- }
- setAssignment(tr, s);
- currentX += STEP_LOOP_X;
-
- // skip start state
- makeElementBehavior(task, template, first.getNextElement(0), loc1, loc);
- } else {
- makeElementBehavior(task, template, first, null, null);
- }
+ // Request is not yet taken into account
+ TMLActivityElement first = task.getActivityDiagram().getFirst();
+
+ currentX = 0; currentY = -220;
+
+ if (task.isRequested()) {
+ UPPAALLocation loc, loc1;
+ UPPAALTransition tr;
+ loc = addLocation(template);
+ template.setInitLocation(loc);
+ loc1 = addLocation(template);
+ tr = addTransition(template, loc, loc1);
+ setSynchronization(tr, "wait__" + task.getRequest().getName() + "?");
+ String s = "";
+ for(int i=0; i<task.getRequest().getNbOfParams(); i++) {
+ if (i!= 0) {
+ s+= ",\n";
+ }
+ s += " arg" + (i+1) + "__req = head" + i + "__" + task.getRequest().getName();
+ }
+ setAssignment(tr, s);
+ currentX += STEP_LOOP_X;
+
+ // skip start state
+ makeElementBehavior(task, template, first.getNextElement(0), loc1, loc);
+ } else {
+ makeElementBehavior(task, template, first, null, null);
+ }
}
-
+
public void makeElementBehavior(TMLTask task, UPPAALTemplate template, TMLActivityElement elt, UPPAALLocation previous, UPPAALLocation end) {
- UPPAALLocation loc, loc1, loc2,/* loc3,*/ loc4;
- UPPAALTransition tr, tr1, tr2, tr3;
- TMLReadChannel rc;
- TMLWriteChannel wc;
- TMLForLoop tmlloop;
- TMLSendRequest sr;
- TMLChoice choice;
- TMLSendEvent sendevt;
- TMLWaitEvent waitevt;
- TMLNotifiedEvent notifiedevt;
- TMLSequence seq;
- TMLRandom random;
-
- //System.out.println("Making behavior of " + task.getName() + " elt = " + elt);
-
- if (elt == null) {
- return;
- }
-
- // Start state
- if (elt instanceof TMLStartState) {
- loc = addLocation(template);
- template.setInitLocation(loc);
- rtu.addTMLActivityElementLocation(elt, loc, loc);
- makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
- return;
-
- // Stop state
- } else if (elt instanceof TMLStopState) {
- if (end == null) {
- rtu.addTMLActivityElementLocation(elt, previous, previous);
- return;
- }
- previous.setCommitted();
- tr = addTransition(template, previous, end);
- rtu.addTMLActivityElementLocation(elt, previous, end);
- return;
-
- // Read samples
- } else if (elt instanceof TMLReadChannel) {
- rc = (TMLReadChannel)elt;
- loc = addLocation(template);
- tr = addTransition(template, previous, loc);
- previous.setCommitted();
- loc.setUrgent();
- setAssignment(tr, "nb__rd = " + rc.getNbOfSamples());
-
- tr1 = addTransition(template, loc, loc);
- setGuard(tr1, "nb__rd>0");
- setSynchronization(tr1, "rd__" +rc.getChannel(0).getName() + "!");
- setAssignment(tr1, "nb__rd = nb__rd - 1");
-
- loc1 = addLocation(template);
- tr2 = addTransition(template, loc, loc1);
- setGuard(tr2, "nb__rd==0");
- rtu.addTMLActivityElementLocation(elt, previous, loc1);
- makeElementBehavior(task, template, elt.getNextElement(0), loc1, end);
-
- //tr.synchronization = "rd__" + rc.getChannel().getName() + "!";
-
- // Write channel
- } else if (elt instanceof TMLWriteChannel) {
- wc = (TMLWriteChannel)elt;
-
- loc = addLocation(template);
- tr = addTransition(template, previous, loc);
- setAssignment(tr, "nb__wr = " + wc.getNbOfSamples());
- previous.setCommitted();
- loc.setUrgent();
-
- // no support for multiwrite
- if (wc.getNbOfChannels() == 1) {
- tr1 = addTransition(template, loc, loc);
- setGuard(tr1, "nb__wr>0");
- setSynchronization(tr1, "wr__" +wc.getChannel(0).getName() + "!");
- setAssignment(tr1, "nb__wr = nb__wr - 1");
-
- loc1 = addLocation(template);
- tr2 = addTransition(template, loc, loc1);
- setGuard(tr2, "nb__wr==0");
- rtu.addTMLActivityElementLocation(elt, previous, loc1);
-
- } else {
- loc2 = loc;
- loc1 = null;
- for(int k=0; k<wc.getNbOfChannels(); k++) {
- tr1 = addTransition(template, loc, loc);
- setGuard(tr1, "nb__wr>0");
- setSynchronization(tr1, "wr__" +wc.getChannel(k).getName() + "!");
- setAssignment(tr1, "nb__wr = nb__wr - 1");
-
- if (k == (wc.getNbOfChannels()-1)) {
- loc1 = addLocation(template);
- tr2 = addTransition(template, loc, loc1);
- setGuard(tr2, "nb__wr==0");
- rtu.addTMLActivityElementLocation(elt, previous, loc1);
- } else {
- loc1 = addLocation(template);
- tr2 = addTransition(template, loc, loc1);
- setGuard(tr2, "nb__wr == 0");
- setAssignment(tr2, "nb__wr = " + wc.getNbOfSamples());
- loc = loc1;
- }
- }
- }
-
- makeElementBehavior(task, template, elt.getNextElement(0), loc1, end);
-
- // Send Request
- } else if (elt instanceof TMLSendRequest) {
- sr = (TMLSendRequest)elt;
- loc = addLocation(template);
- tr = addTransition(template, previous, loc);
- setSynchronization(tr, "request__" + sr.getRequest().getName() + "!");
- String s = "";
- for(int i=0; i<sr.getRequest().getNbOfParams(); i++) {
- if (i != 0) {
- s += ",\n";
- }
- s += "tail" + i + "__" + sr.getRequest().getName()+ " = " + sr.getParam(i);
- }
- setAssignment(tr, s);
- rtu.addTMLActivityElementLocation(elt, previous, loc);
- makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
-
- // Send Event
- } else if (elt instanceof TMLSendEvent) {
- sendevt = (TMLSendEvent)elt;
- loc = addLocation(template);
- tr = addTransition(template, previous, loc);
- setSynchronization(tr, "eventSend__" + sendevt.getEvent().getName() + "!");
- String s = "";
- for(int i=0; i<sendevt.getEvent().getNbOfParams(); i++) {
- if (i != 0) {
- s += ",\n";
- }
- s += "eventTail" + i + "__" + sendevt.getEvent().getName()+ " = " + sendevt.getParam(i);
- }
- setAssignment(tr, s);
- rtu.addTMLActivityElementLocation(elt, previous, loc);
- makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
-
- // Wait event
- } else if (elt instanceof TMLWaitEvent) {
- waitevt = (TMLWaitEvent)elt;
- loc = addLocation(template);
- tr = addTransition(template, previous, loc);
- setSynchronization(tr, "eventNotify__" + waitevt.getEvent().getName() + "?");
- String s = "";
- for(int i=0; i<waitevt.getEvent().getNbOfParams(); i++) {
- if (i != 0) {
- s += ",\n";
- }
- s += waitevt.getParam(i) + "= eventHead" + i + "__" + waitevt.getEvent().getName();
- }
- setAssignment(tr, s);
- rtu.addTMLActivityElementLocation(elt, previous, loc);
- makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
-
- // Notified event
- } else if (elt instanceof TMLNotifiedEvent) {
- notifiedevt = (TMLNotifiedEvent)elt;
- loc = addLocation(template);
- tr = addTransition(template, previous, loc);
- setSynchronization(tr, "eventNotified__" + notifiedevt.getEvent().getName() + "?");
- setAssignment(tr, notifiedevt.getVariable() + " = notified__" + notifiedevt.getEvent().getName());
- rtu.addTMLActivityElementLocation(elt, previous, loc);
- makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
-
- // Action State
- } else if (elt instanceof TMLActionState) {
- if (((TMLActionState)elt).getAction().indexOf("<<") > -1) {
- rtu.addTMLActivityElementLocation(elt, previous, previous);
- makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
- return;
- }
-
- if (((TMLActionState)elt).getAction().indexOf("exit(") > -1) {
- rtu.addTMLActivityElementLocation(elt, previous, previous);
- makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
- return;
- }
-
- String action =((TMLActionState)elt).getAction();
- action = action.trim();
- if (action.endsWith(";")) {
- action = action.substring(0, action.length() - 1);
- }
-
- loc = addLocation(template);
- tr = addTransition(template, previous, loc);
- setAssignment(tr, action);
- rtu.addTMLActivityElementLocation(elt, previous, loc);
- makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
-
- // Random
- } else if (elt instanceof TMLRandom) {
- random = (TMLRandom)elt;
- loc = addLocation(template);
- previous.setCommitted();
- loc.setCommitted();
- tr = addTransition(template, previous, loc);
- setAssignment(tr, "min__random =" + random.getMinValue() + ", max__random = " + random.getMaxValue());
-
-
- loc1 = addLocation(template);
- tr1 = addTransition(template, loc, loc1);
- setAssignment(tr1, random.getVariable() + " = min__random");
- setGuard(tr1, "min__random < max__random + 1");
-
- tr2 = addTransition(template, loc, loc);
- setAssignment(tr2, "min__random = min__random + 1");
- setGuard(tr2, "min__random < max__random ");
-
- makeElementBehavior(task, template, elt.getNextElement(0), loc1, end);
-
- // EXEC operations -> ignored
- } else if ((elt instanceof TMLExecI) || (elt instanceof TMLExecC) ||(elt instanceof TMLExecIInterval)|| (elt instanceof TMLExecCInterval)|| (elt instanceof TMLDelay)) {
- rtu.addTMLActivityElementLocation(elt, previous, previous);
- makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
-
- // Sequence
- } else if (elt instanceof TMLSequence) {
- seq = ((TMLSequence)elt);
-
- // Make sure the sequence is sorted;
- seq.sortNexts();
-
- // Check at least for sequences with two nexts
- if (seq.getNbNext() < 2) {
- // nothing to do!
- rtu.addTMLActivityElementLocation(elt, previous, previous);
- makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
- return;
- }
-
- // Take the last one ...
- currentX = currentX + (seq.getNbNext()-1)*STEP_LOOP_X;
- loc = addLocation(template);
- rtu.addTMLActivityElementLocation(elt, previous, loc);
- makeElementBehavior(task, template, elt.getNextElement(seq.getNbNext()-1), loc, end);
-
- for (int i=seq.getNbNext()-2; i>=0; i--) {
- System.out.println("Making sequence i=" + i);
- currentX -= STEP_LOOP_X;
- loc1 = addLocation(template);
- makeElementBehavior(task, template, elt.getNextElement(i), loc1, loc);
- loc = loc1;
- }
-
- tr = addTransition(template, previous, loc);
-
- // Loop
- } else if (elt instanceof TMLForLoop) {
- String tmpc;
- tmlloop = ((TMLForLoop)elt);
- loc = addLocation(template);
- previous.setCommitted();
- loc.setCommitted();
- tr = addTransition(template, previous, loc);
- setAssignment(tr, tmlloop.getInit());
-
- currentX += STEP_LOOP_X;
- loc1 = addLocation(template);
- tr1 = addTransition(template, loc, loc1);
- loc4 = addLocation(template);
- loc4.setCommitted();
- tr2 = addTransition(template, loc4, loc);
- setAssignment(tr2, tmlloop.getIncrement());
- currentX += STEP_LOOP_X;
-
- tmpc = tmlloop.getCondition();
- if (tmpc.length() ==0) {
- tmpc = "true";
- }
- setGuard(tr1, tmpc);
- makeElementBehavior(task, template, elt.getNextElement(0), loc1, loc4);
- currentX -= STEP_LOOP_X;
- currentX -= STEP_LOOP_X;
-
- loc2 = addLocation(template);
- tr3 = addTransition(template, loc, loc2);
- setGuard(tr3, "!(" + tmpc + ")");
- rtu.addTMLActivityElementLocation(elt, previous, loc2);
- makeElementBehavior(task, template, elt.getNextElement(1), loc2, end);
-
- // TMLSelectEvt
- } else if (elt instanceof TMLSelectEvt) {
- for(int i=0; i<elt.getNbNext(); i++) {
- makeElementBehavior(task, template, elt.getNextElement(i), previous, end);
- currentX += STEP_LOOP_X;
- }
- rtu.addTMLActivityElementLocation(elt, previous, previous);
-
- // Choice
- } else if (elt instanceof TMLChoice) {
- choice = (TMLChoice)elt;
- String g;
-
- if (choice.getNbGuard() ==0 ) {
- rtu.addTMLActivityElementLocation(elt, previous, previous);
- makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
- return;
- }
-
- // Nb of guards > 0
- int index1 = choice.getElseGuard(), index2 = choice.getAfterGuard();
-
- if (index2 != -1) {
- // [after]
- loc = addLocation(template);
- makeElementBehavior(task, template, elt.getNextElement(index2), loc, end);
- end = loc;
- currentX += STEP_LOOP_X;
- }
-
- for(int i=0; i<choice.getNbGuard(); i++) {
- if (i != index2) {
- if (i != index1) {
- g = choice.getGuard(i);
- if (choice.isStochasticGuard(i)) {
- g = "[ ]";
- }
- g = Conversion.replaceAllChar(g, '[', "(");
- g = Conversion.replaceAllChar(g, ']', ")");
- g = g.trim();
- if ((g.compareTo("()") == 0) ||(g.compareTo("( )") == 0)) {
- g = " ";
- }
- loc1 = addLocation(template);
- tr1 = addTransition(template, previous, loc1);
- setGuard(tr1, g);
- makeElementBehavior(task, template, elt.getNextElement(i), loc1, end);
- } else {
- // else transition
- int cpt = 0;
- String gs = "";
- for(int j=0; j<choice.getNbGuard(); j++) {
- if ((j != index2) && (j != index1)) {
- g = choice.getGuard(j);
- //System.out.println("Got guard = " + g);
- g = Conversion.replaceAllChar(g, '[', "(");
- g = Conversion.replaceAllChar(g, ']', ")");
- if (cpt == 0) {
- gs = g;
- } else {
- gs = "((" + gs + ")||(" + g + "))";
- }
- cpt ++;
- }
- }
- gs = "!" + gs;
- //System.out.println("Else guard=" + gs);
- loc1 = addLocation(template);
- tr1 = addTransition(template, previous, loc1);
- setGuard(tr1, gs);
- rtu.addTMLActivityElementLocation(elt, previous, loc1);
- makeElementBehavior(task, template, elt.getNextElement(i), loc1, end);
- }
- currentX += STEP_LOOP_X;
- }
- }
-
- } else {
- System.out.println("Warning: elt = " + elt + " is not yet taken into account .. skipping");
- rtu.addTMLActivityElementLocation(elt, previous, previous);
- makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
- }
-
-
+ UPPAALLocation loc, loc1, loc2,/* loc3,*/ loc4;
+ UPPAALTransition tr, tr1, tr2, tr3;
+ TMLReadChannel rc;
+ TMLWriteChannel wc;
+ TMLForLoop tmlloop;
+ TMLSendRequest sr;
+ TMLChoice choice;
+ TMLSendEvent sendevt;
+ TMLWaitEvent waitevt;
+ TMLNotifiedEvent notifiedevt;
+ TMLSequence seq;
+ TMLRandom random;
+
+ //System.out.println("Making behavior of " + task.getName() + " elt = " + elt);
+
+ if (elt == null) {
+ return;
+ }
+
+ // Start state
+ if (elt instanceof TMLStartState) {
+ loc = addLocation(template);
+ template.setInitLocation(loc);
+ rtu.addTMLActivityElementLocation(elt, loc, loc);
+ makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
+ return;
+
+ // Stop state
+ } else if (elt instanceof TMLStopState) {
+ if (end == null) {
+ rtu.addTMLActivityElementLocation(elt, previous, previous);
+ return;
+ }
+ previous.setCommitted();
+ tr = addTransition(template, previous, end);
+ rtu.addTMLActivityElementLocation(elt, previous, end);
+ return;
+
+ // Read samples
+ } else if (elt instanceof TMLReadChannel) {
+ rc = (TMLReadChannel)elt;
+ loc = addLocation(template);
+ tr = addTransition(template, previous, loc);
+ previous.setCommitted();
+ loc.setUrgent();
+ setAssignment(tr, "nb__rd = " + rc.getNbOfSamples());
+
+ tr1 = addTransition(template, loc, loc);
+ setGuard(tr1, "nb__rd>0");
+ setSynchronization(tr1, "rd__" +rc.getChannel(0).getName() + "!");
+ setAssignment(tr1, "nb__rd = nb__rd - 1");
+
+ loc1 = addLocation(template);
+ tr2 = addTransition(template, loc, loc1);
+ setGuard(tr2, "nb__rd==0");
+ rtu.addTMLActivityElementLocation(elt, previous, loc1);
+ makeElementBehavior(task, template, elt.getNextElement(0), loc1, end);
+
+ //tr.synchronization = "rd__" + rc.getChannel().getName() + "!";
+
+ // Write channel
+ } else if (elt instanceof TMLWriteChannel) {
+ wc = (TMLWriteChannel)elt;
+
+ loc = addLocation(template);
+ tr = addTransition(template, previous, loc);
+ setAssignment(tr, "nb__wr = " + wc.getNbOfSamples());
+ previous.setCommitted();
+ loc.setUrgent();
+
+ // no support for multiwrite
+ if (wc.getNbOfChannels() == 1) {
+ tr1 = addTransition(template, loc, loc);
+ setGuard(tr1, "nb__wr>0");
+ setSynchronization(tr1, "wr__" +wc.getChannel(0).getName() + "!");
+ setAssignment(tr1, "nb__wr = nb__wr - 1");
+
+ loc1 = addLocation(template);
+ tr2 = addTransition(template, loc, loc1);
+ setGuard(tr2, "nb__wr==0");
+ rtu.addTMLActivityElementLocation(elt, previous, loc1);
+
+ } else {
+ loc2 = loc;
+ loc1 = null;
+ for(int k=0; k<wc.getNbOfChannels(); k++) {
+ tr1 = addTransition(template, loc, loc);
+ setGuard(tr1, "nb__wr>0");
+ setSynchronization(tr1, "wr__" +wc.getChannel(k).getName() + "!");
+ setAssignment(tr1, "nb__wr = nb__wr - 1");
+
+ if (k == (wc.getNbOfChannels()-1)) {
+ loc1 = addLocation(template);
+ tr2 = addTransition(template, loc, loc1);
+ setGuard(tr2, "nb__wr==0");
+ rtu.addTMLActivityElementLocation(elt, previous, loc1);
+ } else {
+ loc1 = addLocation(template);
+ tr2 = addTransition(template, loc, loc1);
+ setGuard(tr2, "nb__wr == 0");
+ setAssignment(tr2, "nb__wr = " + wc.getNbOfSamples());
+ loc = loc1;
+ }
+ }
+ }
+
+ makeElementBehavior(task, template, elt.getNextElement(0), loc1, end);
+
+ // Send Request
+ } else if (elt instanceof TMLSendRequest) {
+ sr = (TMLSendRequest)elt;
+ loc = addLocation(template);
+ tr = addTransition(template, previous, loc);
+ setSynchronization(tr, "request__" + sr.getRequest().getName() + "!");
+ String s = "";
+ for(int i=0; i<sr.getRequest().getNbOfParams(); i++) {
+ if (i != 0) {
+ s += ",\n";
+ }
+ s += "tail" + i + "__" + sr.getRequest().getName()+ " = " + sr.getParam(i);
+ }
+ setAssignment(tr, s);
+ rtu.addTMLActivityElementLocation(elt, previous, loc);
+ makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
+
+ // Send Event
+ } else if (elt instanceof TMLSendEvent) {
+ sendevt = (TMLSendEvent)elt;
+ loc = addLocation(template);
+ tr = addTransition(template, previous, loc);
+ setSynchronization(tr, "eventSend__" + sendevt.getEvent().getName() + "!");
+ String s = "";
+ for(int i=0; i<sendevt.getEvent().getNbOfParams(); i++) {
+ if (i != 0) {
+ s += ",\n";
+ }
+ s += "eventTail" + i + "__" + sendevt.getEvent().getName()+ " = " + sendevt.getParam(i);
+ }
+ setAssignment(tr, s);
+ rtu.addTMLActivityElementLocation(elt, previous, loc);
+ makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
+
+ // Wait event
+ } else if (elt instanceof TMLWaitEvent) {
+ waitevt = (TMLWaitEvent)elt;
+ loc = addLocation(template);
+ tr = addTransition(template, previous, loc);
+ setSynchronization(tr, "eventNotify__" + waitevt.getEvent().getName() + "?");
+ String s = "";
+ for(int i=0; i<waitevt.getEvent().getNbOfParams(); i++) {
+ if (i != 0) {
+ s += ",\n";
+ }
+ s += waitevt.getParam(i) + "= eventHead" + i + "__" + waitevt.getEvent().getName();
+ }
+ setAssignment(tr, s);
+ rtu.addTMLActivityElementLocation(elt, previous, loc);
+ makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
+
+ // Notified event
+ } else if (elt instanceof TMLNotifiedEvent) {
+ notifiedevt = (TMLNotifiedEvent)elt;
+ loc = addLocation(template);
+ tr = addTransition(template, previous, loc);
+ setSynchronization(tr, "eventNotified__" + notifiedevt.getEvent().getName() + "?");
+ setAssignment(tr, notifiedevt.getVariable() + " = notified__" + notifiedevt.getEvent().getName());
+ rtu.addTMLActivityElementLocation(elt, previous, loc);
+ makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
+
+ // Action State
+ } else if (elt instanceof TMLActionState) {
+ if (((TMLActionState)elt).getAction().indexOf("<<") > -1) {
+ rtu.addTMLActivityElementLocation(elt, previous, previous);
+ makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
+ return;
+ }
+
+ if (((TMLActionState)elt).getAction().indexOf("exit(") > -1) {
+ rtu.addTMLActivityElementLocation(elt, previous, previous);
+ makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
+ return;
+ }
+
+ String action =((TMLActionState)elt).getAction();
+ action = action.trim();
+ if (action.endsWith(";")) {
+ action = action.substring(0, action.length() - 1);
+ }
+
+ loc = addLocation(template);
+ tr = addTransition(template, previous, loc);
+ setAssignment(tr, action);
+ rtu.addTMLActivityElementLocation(elt, previous, loc);
+ makeElementBehavior(task, template, elt.getNextElement(0), loc, end);
+
+ // Random
+ } else if (elt instanceof TMLRandom) {
+ random = (TMLRandom)elt;
+ loc = addLocation(template);
+ previous.setCommitted();
+ loc.setCommitted();
+ tr = addTransition(template, previous, loc);
+ setAssignment(tr, "min__random =" + random.getMinValue() + ", max__random = " + random.getMaxValue());
+
+
+ loc1 = addLocation(template);
+ tr1 = addTransition(template, loc, loc1);
+ setAssignment(tr1, random.getVariable() + " = min__random");
+ setGuard(tr1, "min__random < max__random + 1");
+
+ tr2 = addTransition(template, loc, loc);
+ setAssignment(tr2, "min__random = min__random + 1");
+ setGuard(tr2, "min__random < max__random ");
+
+ makeElementBehavior(task, template, elt.getNextElement(0), loc1, end);
+
+ // EXEC operations -> ignored
+ } else if ((elt instanceof TMLExecI) || (elt instanceof TMLExecC) ||(elt instanceof TMLExecIInterval)|| (elt instanceof TMLExecCInterval)|| (elt instanceof TMLDelay)) {
+ rtu.addTMLActivityElementLocation(elt, previous, previous);
+ makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
+
+ // Sequence
+ } else if (elt instanceof TMLSequence) {
+ seq = ((TMLSequence)elt);
+
+ // Make sure the sequence is sorted;
+ seq.sortNexts();
+
+ // Check at least for sequences with two nexts
+ if (seq.getNbNext() < 2) {
+ // nothing to do!
+ rtu.addTMLActivityElementLocation(elt, previous, previous);
+ makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
+ return;
+ }
+
+ // Take the last one ...
+ currentX = currentX + (seq.getNbNext()-1)*STEP_LOOP_X;
+ loc = addLocation(template);
+ rtu.addTMLActivityElementLocation(elt, previous, loc);
+ makeElementBehavior(task, template, elt.getNextElement(seq.getNbNext()-1), loc, end);
+
+ for (int i=seq.getNbNext()-2; i>=0; i--) {
+ System.out.println("Making sequence i=" + i);
+ currentX -= STEP_LOOP_X;
+ loc1 = addLocation(template);
+ makeElementBehavior(task, template, elt.getNextElement(i), loc1, loc);
+ loc = loc1;
+ }
+
+ tr = addTransition(template, previous, loc);
+
+ // Loop
+ } else if (elt instanceof TMLForLoop) {
+ String tmpc;
+ tmlloop = ((TMLForLoop)elt);
+ loc = addLocation(template);
+ previous.setCommitted();
+ loc.setCommitted();
+ tr = addTransition(template, previous, loc);
+ setAssignment(tr, tmlloop.getInit());
+
+ currentX += STEP_LOOP_X;
+ loc1 = addLocation(template);
+ tr1 = addTransition(template, loc, loc1);
+ loc4 = addLocation(template);
+ loc4.setCommitted();
+ tr2 = addTransition(template, loc4, loc);
+ setAssignment(tr2, tmlloop.getIncrement());
+ currentX += STEP_LOOP_X;
+
+ tmpc = tmlloop.getCondition();
+ if (tmpc.length() ==0) {
+ tmpc = "true";
+ }
+ setGuard(tr1, tmpc);
+ makeElementBehavior(task, template, elt.getNextElement(0), loc1, loc4);
+ currentX -= STEP_LOOP_X;
+ currentX -= STEP_LOOP_X;
+
+ loc2 = addLocation(template);
+ tr3 = addTransition(template, loc, loc2);
+ setGuard(tr3, "!(" + tmpc + ")");
+ rtu.addTMLActivityElementLocation(elt, previous, loc2);
+ makeElementBehavior(task, template, elt.getNextElement(1), loc2, end);
+
+ // TMLSelectEvt
+ } else if (elt instanceof TMLSelectEvt) {
+ for(int i=0; i<elt.getNbNext(); i++) {
+ makeElementBehavior(task, template, elt.getNextElement(i), previous, end);
+ currentX += STEP_LOOP_X;
+ }
+ rtu.addTMLActivityElementLocation(elt, previous, previous);
+
+ // Choice
+ } else if (elt instanceof TMLChoice) {
+ choice = (TMLChoice)elt;
+ String g;
+
+ if (choice.getNbGuard() ==0 ) {
+ rtu.addTMLActivityElementLocation(elt, previous, previous);
+ makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
+ return;
+ }
+
+ // Nb of guards > 0
+ int index1 = choice.getElseGuard(), index2 = choice.getAfterGuard();
+
+ if (index2 != -1) {
+ // [after]
+ loc = addLocation(template);
+ makeElementBehavior(task, template, elt.getNextElement(index2), loc, end);
+ end = loc;
+ currentX += STEP_LOOP_X;
+ }
+
+ for(int i=0; i<choice.getNbGuard(); i++) {
+ if (i != index2) {
+ if (i != index1) {
+ g = choice.getGuard(i);
+ if (choice.isStochasticGuard(i)) {
+ g = "[ ]";
+ }
+ g = Conversion.replaceAllChar(g, '[', "(");
+ g = Conversion.replaceAllChar(g, ']', ")");
+ g = g.trim();
+ if ((g.compareTo("()") == 0) ||(g.compareTo("( )") == 0)) {
+ g = " ";
+ }
+ loc1 = addLocation(template);
+ tr1 = addTransition(template, previous, loc1);
+ setGuard(tr1, g);
+ makeElementBehavior(task, template, elt.getNextElement(i), loc1, end);
+ } else {
+ // else transition
+ int cpt = 0;
+ String gs = "";
+ for(int j=0; j<choice.getNbGuard(); j++) {
+ if ((j != index2) && (j != index1)) {
+ g = choice.getGuard(j);
+ //System.out.println("Got guard = " + g);
+ g = Conversion.replaceAllChar(g, '[', "(");
+ g = Conversion.replaceAllChar(g, ']', ")");
+ if (cpt == 0) {
+ gs = g;
+ } else {
+ gs = "((" + gs + ")||(" + g + "))";
+ }
+ cpt ++;
+ }
+ }
+ gs = "!" + gs;
+ //System.out.println("Else guard=" + gs);
+ loc1 = addLocation(template);
+ tr1 = addTransition(template, previous, loc1);
+ setGuard(tr1, gs);
+ rtu.addTMLActivityElementLocation(elt, previous, loc1);
+ makeElementBehavior(task, template, elt.getNextElement(i), loc1, end);
+ }
+ currentX += STEP_LOOP_X;
+ }
+ }
+
+ } else {
+ System.out.println("Warning: elt = " + elt + " is not yet taken into account .. skipping");
+ rtu.addTMLActivityElementLocation(elt, previous, previous);
+ makeElementBehavior(task, template, elt.getNextElement(0), previous, end);
+ }
+
+
}
-
+
public UPPAALLocation addLocation(UPPAALTemplate template) {
- UPPAALLocation loc = new UPPAALLocation();
- loc.idPoint.x = currentX;
- loc.idPoint.y = currentY;
- loc.namePoint.x = currentX + NAME_X;
- loc.namePoint.y = currentY + NAME_Y;
- template.addLocation(loc);
- currentX += STEP_X;
- currentY += STEP_Y;
- return loc;
+ UPPAALLocation loc = new UPPAALLocation();
+ loc.idPoint.x = currentX;
+ loc.idPoint.y = currentY;
+ loc.namePoint.x = currentX + NAME_X;
+ loc.namePoint.y = currentY + NAME_Y;
+ template.addLocation(loc);
+ currentX += STEP_X;
+ currentY += STEP_Y;
+ return loc;
}
-
+
public UPPAALTransition addTransition(UPPAALTemplate template, UPPAALLocation loc1, UPPAALLocation loc2) {
- UPPAALTransition tr = new UPPAALTransition();
- tr.sourceLoc = loc1;
- tr.destinationLoc = loc2;
- template.addTransition(tr);
- // Nails?
- return tr;
+ UPPAALTransition tr = new UPPAALTransition();
+ tr.sourceLoc = loc1;
+ tr.destinationLoc = loc2;
+ template.addTransition(tr);
+ // Nails?
+ return tr;
}
-
+
public void setSynchronization(UPPAALTransition tr, String s) {
- tr.synchronization = modifyString(s);
- tr.synchronizationPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + SYNCHRO_X;
- tr.synchronizationPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + SYNCHRO_Y;
+ tr.synchronization = modifyString(s);
+ tr.synchronizationPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + SYNCHRO_X;
+ tr.synchronizationPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + SYNCHRO_Y;
}
-
+
public void setGuard(UPPAALTransition tr, String s) {
- tr.guard = modifyString(s);
- tr.guardPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + GUARD_X;
- tr.guardPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + GUARD_Y;
+ tr.guard = modifyString(s);
+ tr.guardPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + GUARD_X;
+ tr.guardPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + GUARD_Y;
}
-
+
public void setAssignment(UPPAALTransition tr, String s) {
- tr.assignment = modifyString(s);
- tr.assignmentPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + ASSIGN_X;
- tr.assignmentPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + ASSIGN_Y;
+ tr.assignment = modifyString(s);
+ tr.assignmentPoint.x = (tr.sourceLoc.idPoint.x + tr.destinationLoc.idPoint.x)/2 + ASSIGN_X;
+ tr.assignmentPoint.y = (tr.sourceLoc.idPoint.y + tr.destinationLoc.idPoint.y)/2 + ASSIGN_Y;
}
-
+
public void makeSystem() {
- Iterator<UPPAALTemplate> iterator = spec.getTemplates().listIterator();
- UPPAALTemplate template;
- String system = "system ";
- String dec = "";
- int id = 0;
-
- while(iterator.hasNext()) {
- template = iterator.next();
- template.setIdInstanciation(id);
- dec += template.getName() + "__" + id + " = " + template.getName() + "();\n";
- system += template.getName() + "__" + id;
- if (iterator.hasNext()) {
- system += ",";
- } else {
- system += ";";
- }
- id ++;
- }
-
- spec.addInstanciation(dec+system);
+ Iterator<UPPAALTemplate> iterator = spec.getTemplates().listIterator();
+ UPPAALTemplate template;
+ String system = "system ";
+ String dec = "";
+ int id = 0;
+
+ while(iterator.hasNext()) {
+ template = iterator.next();
+ template.setIdInstanciation(id);
+ dec += template.getName() + "__" + id + " = " + template.getName() + "();\n";
+ system += template.getName() + "__" + id;
+ if (iterator.hasNext()) {
+ system += ",";
+ } else {
+ system += ";";
+ }
+ id ++;
+ }
+
+ spec.addInstanciation(dec+system);
}
-
- public void makeLoss(String name) {
- TraceManager.addDev("Makking loss");
- if (lossTemplate == null) {
- lossTemplate = new UPPAALTemplate();
- lossTemplate.setName("LossManager__");
- spec.addTemplate(lossTemplate);
- UPPAALLocation loc = addLocation(lossTemplate);
- loc.name = "main__loss";
- lossTemplate.setInitLocation(loc);
- lossNames = new Vector<String>();
- } else {
- // loss already computed?
- for(String s: lossNames) {
- if (s.compareTo(name) == 0) {
- return;
- }
- }
- }
-
- lossNames.add(name);
-
- UPPAALTransition tr = addTransition(lossTemplate, lossTemplate.getInitLocation(), lossTemplate.getInitLocation());
- setSynchronization(tr, name + "__loss?");
- tr = addTransition(lossTemplate, lossTemplate.getInitLocation(), lossTemplate.getInitLocation());
- setSynchronization(tr, name + "__noloss?");
-
- spec.addGlobalDeclaration("\n// Lossy communications\n");
- spec.addGlobalDeclaration("urgent chan " + name + "__loss, " + name + "__noloss;\n");
-
- }
-
+
+ public void makeLoss(String name) {
+ TraceManager.addDev("Makking loss");
+ if (lossTemplate == null) {
+ lossTemplate = new UPPAALTemplate();
+ lossTemplate.setName("LossManager__");
+ spec.addTemplate(lossTemplate);
+ UPPAALLocation loc = addLocation(lossTemplate);
+ loc.name = "main__loss";
+ lossTemplate.setInitLocation(loc);
+ lossNames = new Vector<String>();
+ } else {
+ // loss already computed?
+ for(String s: lossNames) {
+ if (s.compareTo(name) == 0) {
+ return;
+ }
+ }
+ }
+
+ lossNames.add(name);
+
+ UPPAALTransition tr = addTransition(lossTemplate, lossTemplate.getInitLocation(), lossTemplate.getInitLocation());
+ setSynchronization(tr, name + "__loss?");
+ tr = addTransition(lossTemplate, lossTemplate.getInitLocation(), lossTemplate.getInitLocation());
+ setSynchronization(tr, name + "__noloss?");
+
+ spec.addGlobalDeclaration("\n// Lossy communications\n");
+ spec.addGlobalDeclaration("urgent chan " + name + "__loss, " + name + "__noloss;\n");
+
+ }
+
public String modifyString(String _input) {
//System.out.println("Modify string=" + _input);
try {
- _input = Conversion.changeBinaryOperatorWithUnary(_input, "div", "/");
- _input = Conversion.changeBinaryOperatorWithUnary(_input, "mod", "%");
+ _input = Conversion.changeBinaryOperatorWithUnary(_input, "div", "/");
+ _input = Conversion.changeBinaryOperatorWithUnary(_input, "mod", "%");
} catch (Exception e) {
- System.out.println("Exception when changing binary operator in " + _input);
+ System.out.println("Exception when changing binary operator in " + _input);
}
//System.out.println("Modified string=" + _input);
return _input;
}
-
+
}
diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java
index bd5ba37a9a54c64c76fe11ef0b7207b82b41f621..e60278412de239b1704394e0ea5df9b0faa23ab7 100644
--- a/src/ui/MainGUI.java
+++ b/src/ui/MainGUI.java
@@ -4014,12 +4014,20 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe
}*/
TraceManager.addDev( "About to open the window at line 4198" );
if (showWindow) {
- JDialogUPPAALGeneration jgen = new JDialogUPPAALGeneration(frame, this, "UPPAAL code generation", ConfigurationTTool.UPPAALCodeDirectory, JDialogUPPAALGeneration.DIPLODOCUS_MODE);
+ TURTLEPanel tp = getCurrentTURTLEPanel();
+ boolean result = false;
+ if ((tp instanceof TMLDesignPanel) || (tp instanceof TMLComponentDesignPanel)) {
+ result = gtm.generateUPPAALFromTML(ConfigurationTTool.UPPAALCodeDirectory, false, 1024, true);
+ }
+ if (result != false) {
+ formalValidation();
+ }
+ /*JDialogUPPAALGeneration jgen = new JDialogUPPAALGeneration(frame, this, "UPPAAL code generation", ConfigurationTTool.UPPAALCodeDirectory, JDialogUPPAALGeneration.DIPLODOCUS_MODE);
// jgen.setSize(450, 500);
GraphicLib.centerOnParent(jgen, 450, 500);
- jgen.setVisible(true);
-
- }
+ jgen.setVisible(true);*/
+
+ }
return;
}
}
diff --git a/src/ui/window/JDialogUPPAALValidation.java b/src/ui/window/JDialogUPPAALValidation.java
index 013c16abbabafb7f4310d103e25f2b72b0b53119..211d588a0f3c85a196266d8da1a773fc102ad5cf 100755
--- a/src/ui/window/JDialogUPPAALValidation.java
+++ b/src/ui/window/JDialogUPPAALValidation.java
@@ -92,6 +92,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
protected java.util.List<String> customQueries;
public Map<String, Integer> verifMap;
protected int status = -1;
+
/** Creates new form */
public JDialogUPPAALValidation(Frame f, MainGUI _mgui, String title, String _cmdVerifyta, String _pathTrace, String _fileName, String _spec, String _host, TURTLEPanel _tp) {
super(f, title, true);
@@ -113,7 +114,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
customChecks = new LinkedList<JCheckBox>();
initComponents();
myInitComponents();
- verifMap = new HashMap<String, Integer>();
+ verifMap = new HashMap<String, Integer>();
pack();
//getGlassPane().addMouseListener( new MouseAdapter() {});
@@ -316,15 +317,15 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
public void run() {
- // String cmd1 = "";
- // String data1;
+ // String cmd1 = "";
+ // String data1;
int id = 0;
String query;
String name;
int trace_id = 0;
int index;
String fn;
- int result;
+ int result;
rshc = new RshClient(host);
RshClient rshctmp = rshc;
@@ -355,11 +356,11 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
ArrayList<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
if ((list != null) && (list.size() > 0)){
for(TGComponentAndUPPAALQuery cq: list) {
- String s = cq.uppaalQuery;
+ String s = cq.uppaalQuery;
index = s.indexOf('$');
- if (cq.tgc != null) {
- cq.tgc.setReachability(TGComponent.ACCESSIBILITY_UNKNOWN);
- }
+ if (cq.tgc != null) {
+ cq.tgc.setReachability(TGComponent.ACCESSIBILITY_UNKNOWN);
+ }
if ((index != -1) && (mode != NOT_STARTED)) {
name = s.substring(index+1, s.length());
//TraceManager.addDev("****\n name=" + name + " list=" + list + "\n****\n");
@@ -367,14 +368,14 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
//jta.append("\n\n--------------------------------------------\n");
jta.append("\nReachability of: " + name + "\n");
result = workQuery("E<> " + query, fn, trace_id, rshc);
- if (cq.tgc != null) {
- if (result == 0) {
- cq.tgc.setReachability(TGComponent.ACCESSIBILITY_KO);
- cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
- } else if (result == 1) {
- cq.tgc.setReachability(TGComponent.ACCESSIBILITY_OK);
- }
- }
+ if (cq.tgc != null) {
+ if (result == 0) {
+ cq.tgc.setReachability(TGComponent.ACCESSIBILITY_KO);
+ cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
+ } else if (result == 1) {
+ cq.tgc.setReachability(TGComponent.ACCESSIBILITY_OK);
+ }
+ }
trace_id++;
} else {
jta.append("A component could not be studied (internal error)\n");
@@ -388,11 +389,11 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
if (stateA.isSelected() && (mode != NOT_STARTED)) {
ArrayList<TGComponentAndUPPAALQuery> list = mgui.gtm.getUPPAALQueries(tp);
if ((list != null) && (list.size() > 0)){
- for(TGComponentAndUPPAALQuery cq: list) {
- if (cq.tgc != null) {
- cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_UNKNOWN);
- }
- String s = cq.uppaalQuery;
+ for(TGComponentAndUPPAALQuery cq: list) {
+ if (cq.tgc != null) {
+ cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_UNKNOWN);
+ }
+ String s = cq.uppaalQuery;
index = s.indexOf('$');
if ((index != -1) && (mode != NOT_STARTED)) {
name = s.substring(index+1, s.length());
@@ -400,13 +401,13 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
//jta.append("\n--------------------------------------------\n");
jta.append("\nLiveness of: " + name + "\n");
result = workQuery("A<> " + query, fn, trace_id, rshc);
- if (cq.tgc != null) {
- if (result == 0) {
- cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
- } else if (result == 1) {
- cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_OK);
- }
- }
+ if (cq.tgc != null) {
+ if (result == 0) {
+ cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_KO);
+ } else if (result == 1) {
+ cq.tgc.setLiveness(TGComponent.ACCESSIBILITY_OK);
+ }
+ }
trace_id++;
} else {
jta.append("A component could not be studied (internal error)\n");
@@ -472,14 +473,14 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
if (j.isSelected()){
jta.append(j.getText()+"\n");
String translation = translateCustomQuery(j.getText());
- jta.append(translation);
- status = -1;
+ jta.append(translation);
+ status = -1;
workQuery(translation, fn, trace_id, rshc);
- verifMap.put(j.getText(), status);
+ verifMap.put(j.getText(), status);
trace_id++;
}
}
-
+
mgui.modelBacktracingUPPAAL(verifMap);
}
@@ -513,7 +514,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
} catch (LauncherException le1) {}
return;
}
-
+
mode = NOT_STARTED;
setButtons();
}
@@ -568,7 +569,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
// return: 1: property is satisfied
private int workQuery(String query, String fn, int trace_id, RshClient rshc) throws LauncherException {
- int ret = -1;
+ int ret = -1;
TraceManager.addDev("Working on query: " + query);
@@ -584,7 +585,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
cmd1 += fn + ".xml " + fn + ".q";
//jta.append("--------------------------------------------\n");
- //TraceManager.addDev("Query:>" + cmd1 + "<");
+ //TraceManager.addDev("Query:>" + cmd1 + "<");
data = processCmd(cmd1);
//TraceManager.addDev("Results:>" + data + "<");
if(showDetails.isSelected()) {
@@ -598,19 +599,19 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
}
else if (data.indexOf("Property is satisfied") >-1){
jta.append("-> property is satisfied\n");
- status=1;
- ret = 1;
+ status=1;
+ ret = 1;
}
else if (data.indexOf("Property is NOT satisfied") > -1) {
jta.append("-> property is NOT satisfied\n");
- status = 0;
- ret = 0;
+ status = 0;
+ ret = 0;
}
else {
jta.append("ERROR -> property could not be studied\n");
- status=2;
-
-
+ status=2;
+
+
}
} else {
jta.append("** verification stopped **\n");
@@ -622,8 +623,8 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti
generateTraceFile(fn, trace_id, rshc);
}
- return ret;
-
+ return ret;
+
}
private void generateTraceFile(String fn, int trace_id, RshClient rshc) throws LauncherException{
diff --git a/uppaal/README b/uppaal/README
new file mode 100644
index 0000000000000000000000000000000000000000..8129927f613251d9b16899c0c15de603081c796b
--- /dev/null
+++ b/uppaal/README
@@ -0,0 +1 @@
+Dir in which uppaal spec are generated
\ No newline at end of file