From 8c255280b2947c46090bdc93f88e6f2af3f2beee Mon Sep 17 00:00:00 2001
From: apvrille <ludovic.apvrille@eurecom.fr>
Date: Tue, 21 Mar 2017 16:39:29 +0100
Subject: [PATCH] Update on TTool uppaal diplo management
---
modeling/modelsForTestingTTool/testdiplo.xml | 250 ++--
src/tmltranslator/touppaal/TML2UPPAAL.java | 1415 +++++++++---------
src/ui/MainGUI.java | 14 +-
3 files changed, 863 insertions(+), 816 deletions(-)
diff --git a/modeling/modelsForTestingTTool/testdiplo.xml b/modeling/modelsForTestingTTool/testdiplo.xml
index 1ce39ec054..7e8fe19360 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" >
@@ -1647,11 +1647,11 @@
</COMPONENT>
<SUBCOMPONENT type="1101" id="398" >
<father id="441" num="0" />
-<cdparam x="445" y="269" />
+<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="144" minY="0" maxY="160" />
-<infoparam name="TGComponent" value="Design3::T2" />
+<infoparam name="TGComponent" value="Design3::T1" />
<TGConnectingPoint num="0" id="390" />
<TGConnectingPoint num="1" id="391" />
<TGConnectingPoint num="2" id="392" />
@@ -1661,7 +1661,7 @@
<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" >
@@ -1685,11 +1685,11 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="1101" id="416" >
<father id="441" num="2" />
-<cdparam x="413" y="213" />
+<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="144" minY="0" maxY="160" />
-<infoparam name="TGComponent" value="Design3::T1" />
+<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,39 +2063,39 @@
<MainCode value="void __user_init() {"/>
<MainCode value="}"/>
<Optimized value="true" />
-<Validated value="" />
+<Validated value="Block0;" />
<Ignored value="" />
-<COMPONENT type="5000" id="1206" >
+<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="1207" />
-<TGConnectingPoint num="1" id="1208" />
-<TGConnectingPoint num="2" id="1209" />
-<TGConnectingPoint num="3" id="1210" />
-<TGConnectingPoint num="4" id="1211" />
-<TGConnectingPoint num="5" id="1212" />
-<TGConnectingPoint num="6" id="1213" />
-<TGConnectingPoint num="7" id="1214" />
-<TGConnectingPoint num="8" id="1215" />
-<TGConnectingPoint num="9" id="1216" />
-<TGConnectingPoint num="10" id="1217" />
-<TGConnectingPoint num="11" id="1218" />
-<TGConnectingPoint num="12" id="1219" />
-<TGConnectingPoint num="13" id="1220" />
-<TGConnectingPoint num="14" id="1221" />
-<TGConnectingPoint num="15" id="1222" />
-<TGConnectingPoint num="16" id="1223" />
-<TGConnectingPoint num="17" id="1224" />
-<TGConnectingPoint num="18" id="1225" />
-<TGConnectingPoint num="19" id="1226" />
-<TGConnectingPoint num="20" id="1227" />
-<TGConnectingPoint num="21" id="1228" />
-<TGConnectingPoint num="22" id="1229" />
-<TGConnectingPoint num="23" id="1230" />
+<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="" />
@@ -2064,43 +2106,25 @@
</AVATARBlockDiagramPanel>
<AVATARStateMachineDiagramPanel name="Block0" minX="10" maxX="2500" minY="10" maxY="1500" >
-<COMPONENT type="5101" id="1233" >
-<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="1234" />
-</COMPONENT>
-
-<COMPONENT type="5100" id="1231" >
-<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="1232" />
-</COMPONENT>
-
-<CONNECTOR type="5102" id="1235" >
+<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="1236" />
-<P1 x="407" y="70" id="1232" />
-<P2 x="394" y="131" id="1234" />
+<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="1237" >
-<father id="1235" num="0" />
+</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="1238" />
-<TGConnectingPoint num="1" id="1239" />
-<TGConnectingPoint num="2" id="1240" />
-<TGConnectingPoint num="3" id="1241" />
+<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="" />
@@ -2108,11 +2132,27 @@
<computeMin value="" />
<computeMax value="" />
<actions value="x = x + 1" />
-<filesToIncludeLine value="" />
-<codeToIncludeLine value="" />
</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>
diff --git a/src/tmltranslator/touppaal/TML2UPPAAL.java b/src/tmltranslator/touppaal/TML2UPPAAL.java
index c1950d6ccb..e73b550c57 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 1d2ff57137..e60278412d 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;
}
}
--
GitLab