diff --git a/modeling/modelsForTestingTTool/testdiplo.xml b/modeling/modelsForTestingTTool/testdiplo.xml index 7e8fe19360c98259493ed4bb15ee81492ff631d1..a2746f131335b599c8c9bb931882a55aab9d2058 100644 --- a/modeling/modelsForTestingTTool/testdiplo.xml +++ b/modeling/modelsForTestingTTool/testdiplo.xml @@ -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="653" y="398" id="352" /> +<P1 x="666" y="385" 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="656" y="163" id="330" /> +<P1 x="669" y="150" 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="376" y="164" id="341" /> +<P2 x="363" y="151" id="341" /> <AutomaticDrawing data="true" /> </CONNECTOR> <COMPONENT type="1208" id="329" > @@ -1828,64 +1828,64 @@ <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" > +<CONNECTOR type="126" id="477" > <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" /> +<P1 x="408" y="183" id="492" /> +<P2 x="631" y="177" id="479" /> <AutomaticDrawing data="true" /> </CONNECTOR> -<CONNECTOR type="126" id="477" > +<CONNECTOR type="126" id="478" > <cdparam x="408" y="226" /> <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="226" id="489" /> -<P2 x="631" y="215" id="478" /> +<P1 x="408" y="225" id="494" /> +<P2 x="631" y="215" id="481" /> <AutomaticDrawing data="true" /> </CONNECTOR> -<COMPONENT type="1202" id="488" > +<COMPONENT type="1202" id="491" > <cdparam x="644" y="144" /> <sizeparam width="200" height="150" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> <cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> <infoparam name="Primitive component" value="TMLComp_1" /> -<TGConnectingPoint num="0" id="480" /> -<TGConnectingPoint num="1" id="481" /> -<TGConnectingPoint num="2" id="482" /> -<TGConnectingPoint num="3" id="483" /> -<TGConnectingPoint num="4" id="484" /> -<TGConnectingPoint num="5" id="485" /> -<TGConnectingPoint num="6" id="486" /> -<TGConnectingPoint num="7" id="487" /> +<TGConnectingPoint num="0" id="483" /> +<TGConnectingPoint num="1" id="484" /> +<TGConnectingPoint num="2" id="485" /> +<TGConnectingPoint num="3" id="486" /> +<TGConnectingPoint num="4" id="487" /> +<TGConnectingPoint num="5" id="488" /> +<TGConnectingPoint num="6" id="489" /> +<TGConnectingPoint num="7" id="490" /> <extraparam> </extraparam> </COMPONENT> -<SUBCOMPONENT type="1203" id="565" > -<father id="488" num="0" /> +<SUBCOMPONENT type="1203" id="480" > +<father id="491" 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" /> +<infoparam name="Primitive port" value="Event evt" /> +<TGConnectingPoint num="0" id="479" /> <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="1" 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" /> +<SUBCOMPONENT type="1203" id="482" > +<father id="491" 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" /> <cdrectangleparam minX="-13" maxX="187" minY="-13" maxY="137" /> <infoparam name="Primitive port" value="Channel comm" /> -<TGConnectingPoint num="0" id="478" /> +<TGConnectingPoint num="0" id="481" /> <extraparam> <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="" /> @@ -1896,48 +1896,48 @@ </extraparam> </SUBCOMPONENT> -<COMPONENT type="1202" id="499" > -<cdparam x="195" y="134" /> +<COMPONENT type="1202" id="504" > +<cdparam x="195" y="133" /> <sizeparam width="200" height="150" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> <cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> <infoparam name="Primitive component" value="TMLComp_0" /> -<TGConnectingPoint num="0" id="491" /> -<TGConnectingPoint num="1" id="492" /> -<TGConnectingPoint num="2" id="493" /> -<TGConnectingPoint num="3" id="494" /> -<TGConnectingPoint num="4" id="495" /> -<TGConnectingPoint num="5" id="496" /> -<TGConnectingPoint num="6" id="497" /> -<TGConnectingPoint num="7" id="498" /> +<TGConnectingPoint num="0" id="496" /> +<TGConnectingPoint num="1" id="497" /> +<TGConnectingPoint num="2" id="498" /> +<TGConnectingPoint num="3" id="499" /> +<TGConnectingPoint num="4" id="500" /> +<TGConnectingPoint num="5" id="501" /> +<TGConnectingPoint num="6" id="502" /> +<TGConnectingPoint num="7" id="503" /> <extraparam> </extraparam> </COMPONENT> -<SUBCOMPONENT type="1203" id="555" > -<father id="499" num="0" /> -<cdparam x="382" y="172" /> +<SUBCOMPONENT type="1203" id="493" > +<father id="504" num="0" /> +<cdparam x="382" y="170" /> <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" /> +<infoparam name="Primitive port" value="Event evt" /> +<TGConnectingPoint num="0" id="492" /> <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="1" 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" /> +<SUBCOMPONENT type="1203" id="495" > +<father id="504" num="1" /> +<cdparam x="382" y="212" /> <sizeparam width="26" height="26" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> <cdrectangleparam minX="-13" maxX="187" minY="-13" maxY="137" /> <infoparam name="Primitive port" value="Channel comm" /> -<TGConnectingPoint num="0" id="489" /> +<TGConnectingPoint num="0" id="494" /> <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="uint_16" associatedEvent="" checkConf="false" checkConfStatus="0" checkAuth="false" checkWeakAuthStatus="0" checkStrongAuthStatus="0" /> <Type type="0" typeOther="" /> @@ -1952,102 +1952,102 @@ </TMLComponentTaskDiagramPanel> <TMLActivityDiagramPanel name="TMLComp_1" minX="10" maxX="2500" minY="10" maxY="1500" > -<COMPONENT type="1001" id="501" > +<COMPONENT type="1001" id="506" > <cdparam x="410" y="154" /> <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="500" /> +<TGConnectingPoint num="0" id="505" /> </COMPONENT> -<COMPONENT type="1009" id="504" > +<COMPONENT type="1009" id="509" > <cdparam x="380" y="100" /> <sizeparam width="69" 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="read channel" value="comm(1) " /> -<TGConnectingPoint num="0" id="502" /> -<TGConnectingPoint num="1" id="503" /> +<TGConnectingPoint num="0" id="507" /> +<TGConnectingPoint num="1" id="508" /> <extraparam> <Data channelName="comm" nbOfSamples="1" secPattern="" /> </extraparam> </COMPONENT> -<COMPONENT type="1000" id="506" > +<COMPONENT type="1000" id="511" > <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="505" /> +<TGConnectingPoint num="0" id="510" /> </COMPONENT> -<CONNECTOR type="115" id="507" > +<CONNECTOR type="115" id="512" > <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" /> -<P1 x="407" y="70" id="505" /> -<P2 x="414" y="95" id="502" /> +<P1 x="407" y="70" id="510" /> +<P2 x="414" y="95" id="507" /> <AutomaticDrawing data="true" /> </CONNECTOR> -<CONNECTOR type="115" id="508" > +<CONNECTOR type="115" id="513" > <cdparam x="414" y="125" /> <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <infoparam name="connector" value="null" /> -<P1 x="414" y="125" id="503" /> -<P2 x="420" y="149" id="500" /> +<P1 x="414" y="125" id="508" /> +<P2 x="420" y="149" id="505" /> <AutomaticDrawing data="true" /> </CONNECTOR> </TMLActivityDiagramPanel> <TMLActivityDiagramPanel name="TMLComp_0" minX="10" maxX="2500" minY="10" maxY="1500" > -<COMPONENT type="1001" id="510" > +<COMPONENT type="1001" id="515" > <cdparam x="423" y="193" /> <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="509" /> +<TGConnectingPoint num="0" id="514" /> </COMPONENT> -<COMPONENT type="1006" id="513" > +<COMPONENT type="1006" id="518" > <cdparam x="402" y="119" /> <sizeparam width="65" height="20" minWidth="30" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> <cdrectangleparam minX="10" maxX="2500" minY="10" maxY="1500" /> <infoparam name="write channel" value="comm(1)" /> -<TGConnectingPoint num="0" id="511" /> -<TGConnectingPoint num="1" id="512" /> +<TGConnectingPoint num="0" id="516" /> +<TGConnectingPoint num="1" id="517" /> <extraparam> <Data channelName="comm" nbOfSamples="1" secPattern="" /> </extraparam> </COMPONENT> -<COMPONENT type="1000" id="515" > +<COMPONENT type="1000" id="520" > <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="514" /> +<TGConnectingPoint num="0" id="519" /> </COMPONENT> -<CONNECTOR type="115" id="516" > +<CONNECTOR type="115" id="521" > <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" /> -<P1 x="407" y="70" id="514" /> -<P2 x="434" y="114" id="511" /> +<P1 x="407" y="70" id="519" /> +<P2 x="434" y="114" id="516" /> <AutomaticDrawing data="true" /> </CONNECTOR> -<CONNECTOR type="115" id="517" > +<CONNECTOR type="115" id="522" > <cdparam x="434" y="144" /> <sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <infoparam name="connector" value="null" /> -<P1 x="434" y="144" id="512" /> -<P2 x="433" y="188" id="509" /> +<P1 x="434" y="144" id="517" /> +<P2 x="433" y="188" id="514" /> <AutomaticDrawing data="true" /> </CONNECTOR> @@ -2066,36 +2066,36 @@ <Validated value="Block0;" /> <Ignored value="" /> -<COMPONENT type="5000" id="542" > +<COMPONENT type="5000" id="547" > <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" /> +<TGConnectingPoint num="0" id="523" /> +<TGConnectingPoint num="1" id="524" /> +<TGConnectingPoint num="2" id="525" /> +<TGConnectingPoint num="3" id="526" /> +<TGConnectingPoint num="4" id="527" /> +<TGConnectingPoint num="5" id="528" /> +<TGConnectingPoint num="6" id="529" /> +<TGConnectingPoint num="7" id="530" /> +<TGConnectingPoint num="8" id="531" /> +<TGConnectingPoint num="9" id="532" /> +<TGConnectingPoint num="10" id="533" /> +<TGConnectingPoint num="11" id="534" /> +<TGConnectingPoint num="12" id="535" /> +<TGConnectingPoint num="13" id="536" /> +<TGConnectingPoint num="14" id="537" /> +<TGConnectingPoint num="15" id="538" /> +<TGConnectingPoint num="16" id="539" /> +<TGConnectingPoint num="17" id="540" /> +<TGConnectingPoint num="18" id="541" /> +<TGConnectingPoint num="19" id="542" /> +<TGConnectingPoint num="20" id="543" /> +<TGConnectingPoint num="21" id="544" /> +<TGConnectingPoint num="22" id="545" /> +<TGConnectingPoint num="23" id="546" /> <extraparam> <CryptoBlock value="false" /> <Attribute access="0" id="x" value="1" type="8" typeOther="" /> @@ -2106,25 +2106,25 @@ </AVATARBlockDiagramPanel> <AVATARStateMachineDiagramPanel name="Block0" minX="10" maxX="2500" minY="10" maxY="1500" > -<CONNECTOR type="5102" id="549" > +<CONNECTOR type="5102" id="554" > <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" /> +<TGConnectingPoint num="0" id="553" /> +<P1 x="407" y="70" id="557" /> +<P2 x="394" y="131" id="555" /> <AutomaticDrawing data="true" /> -</CONNECTOR><SUBCOMPONENT type="-1" id="547" > -<father id="549" num="0" /> +</CONNECTOR><SUBCOMPONENT type="-1" id="552" > +<father id="554" 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" /> +<TGConnectingPoint num="0" id="548" /> +<TGConnectingPoint num="1" id="549" /> +<TGConnectingPoint num="2" id="550" /> +<TGConnectingPoint num="3" id="551" /> <extraparam> <guard value="[ ]" /> <afterMin value="" /> @@ -2135,22 +2135,22 @@ </extraparam> </SUBCOMPONENT> -<COMPONENT type="5101" id="551" > +<COMPONENT type="5101" id="556" > <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" /> +<TGConnectingPoint num="0" id="555" /> </COMPONENT> -<COMPONENT type="5100" id="553" > +<COMPONENT type="5100" id="558" > <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" /> +<TGConnectingPoint num="0" id="557" /> </COMPONENT> diff --git a/src/ui/JToolBarMainTurtle.java b/src/ui/JToolBarMainTurtle.java index e4e8bd9fee64a939a5fda14e890277ddd9d8cf34..9dfa8c39c0c95c83ae812301a809ad237bb566ee 100755 --- a/src/ui/JToolBarMainTurtle.java +++ b/src/ui/JToolBarMainTurtle.java @@ -164,6 +164,10 @@ public class JToolBarMainTurtle extends JToolBar implements ActionListener //} avatarFVUPPAAL = add(mgui.actions[TGUIAction.ACT_AVATAR_FV_UPPAAL]); avatarFVUPPAAL.addMouseListener(mgui.mouseHandler); + if (MainGUI.uppaalOn) { + genuppaal = add(mgui.actions[TGUIAction.ACT_GEN_UPPAAL]); + genuppaal.addMouseListener(mgui.mouseHandler); + } if (MainGUI.proverifOn) { avatarFVProVerif = add(mgui.actions[TGUIAction.ACT_AVATAR_FV_PROVERIF]); avatarFVProVerif.addMouseListener(mgui.mouseHandler); @@ -194,11 +198,6 @@ public class JToolBarMainTurtle extends JToolBar implements ActionListener genlotos.addMouseListener(mgui.mouseHandler); } - if (MainGUI.uppaalOn) { - genuppaal = add(mgui.actions[TGUIAction.ACT_GEN_UPPAAL]); - genuppaal.addMouseListener(mgui.mouseHandler); - } - /*if (MainGUI.proverifOn) { button = add(mgui.actions[TGUIAction.ACT_GEN_PROVERIF]); button.addMouseListener(mgui.mouseHandler); @@ -425,7 +424,7 @@ public class JToolBarMainTurtle extends JToolBar implements ActionListener } if (validation != null) { - validation.setVisible(b); + validation.setVisible(!b); } if (oneClickrtlotos != null) { diff --git a/src/ui/TGUIAction.java b/src/ui/TGUIAction.java index b307ddaa2d06e85f90e0826e77836e046ecc2ba0..be6f07814b1181b927fefe401530927e1c428613 100755 --- a/src/ui/TGUIAction.java +++ b/src/ui/TGUIAction.java @@ -701,7 +701,7 @@ public class TGUIAction extends AbstractAction { actions[ACT_GEN_LOTOS] = new TAction("gen_lotos-command", "Generate LOTOS", IconManager.imgic90, IconManager.imgic90, "Generate LOTOS specification", "Generates a LOTOS specification from TTool diagrams", '0'); actions[ACT_ONECLICK_LOTOS_RG] = new TAction("gen_rglotos-command", "One-click LOTOS-based verification", IconManager.imgic342, IconManager.imgic342, "One-click LOTOS-based verification", "Generates a LOTOS-based RG from TTool diagrams", '0'); actions[ACT_ONECLICK_RTLOTOS_RG] = new TAction("gen_rgrtlotos-command", "Generate RT-LOTOS-based RG", IconManager.imgic342, IconManager.imgic342, "Generate RT-LOTOS-based RG ", "Generates an RT-LOTOS-based RG from TTool diagrams", '0'); - actions[ACT_GEN_UPPAAL] = new TAction("gen_uppaal-command", "Generate UPPAAL", IconManager.imgic92, IconManager.imgic92, "Generate UPPAAL specification", "Generates a UPPAAL specification from TTool diagrams", '0'); + actions[ACT_GEN_UPPAAL] = new TAction("gen_uppaal-command", "Safety formal verification with UPPAAL", IconManager.imgic86, IconManager.imgic86, "Generate UPPAAL specification", "Generates a UPPAAL specification from TTool diagrams", '0'); actions[ACT_GEN_PROVERIF] = new TAction("gen_proverif-command", "Generate ProVerif Code", IconManager.imgic34, IconManager.imgic35, "Generate ProVerif specification", "Generates a ProVerif specification from AVATAR diagrams", '0'); actions[ACT_AVATAR_MODEL_CHECKER] = new TAction("avatar-model-checker", "Avatar model checker", IconManager.imgic140, IconManager.imgic140, "Avatar model checker", "Executes the AVATAR model checker from an AVATAR design", '0'); actions[ACT_GEN_JAVA] = new TAction("gen_java-command", "Generate JAVA", IconManager.imgic38, IconManager.imgic39, "Generate JAVA", "Generates Java code from TURTLE diagrams", 0); @@ -737,7 +737,7 @@ public class TGUIAction extends AbstractAction { actions[ACT_DSE] = new TAction("auto-dse", "Automated Design Space Exploration", IconManager.imgic89, IconManager.imgic89, "Automated Design Space Exploration", "Find the optimal mapping and security additions automatically",0); // AVATAR actions[ACT_AVATAR_SIM] = new TAction("avatar-simu", "Interactive simulation", IconManager.imgic18, IconManager.imgic18, "Interactive simulation", "Interactive simulation of the AVATAR design under edition", '2'); - actions[ACT_AVATAR_FV_UPPAAL] = new TAction("avatar-formal-verification-uppaal", "Formal verification with UPPAAL (Safety)", IconManager.imgic86, IconManager.imgic86, "Formal verification with UPPAAL (Safety)", "Formal verification with UPPAAL (Safety) of the AVATAR design under edition", '3'); + actions[ACT_AVATAR_FV_UPPAAL] = new TAction("avatar-formal-verification-uppaal", "Safety formal verification with UPPAAL (Safety)", IconManager.imgic86, IconManager.imgic86, "Formal verification with UPPAAL (Safety)", "Formal verification with UPPAAL (Safety) of the AVATAR design under edition", '3'); actions[ACT_AVATAR_FV_PROVERIF] = new TAction("avatar-formal-verification-proverif", "Security verification", IconManager.imgic88, IconManager.imgic88, "Security verification", "Security formal verification (with ProVerif)", '4'); actions[ACT_AVATAR_FV_STATICANALYSIS] = new TAction("avatar-formal-verification-staticanalysis", "Safety analysis (invariants)", IconManager.imgic96, IconManager.imgic96, "Safaty analysis (invariants)", "Safety analysis using the invariant tecnique", '5'); actions[ACT_AVATAR_EXECUTABLE_GENERATION] = new TAction("avatar-executable-generation", "Code generation" , IconManager.imgic94, IconManager.imgic94, "Code generation", "Generation of C-POSIX executable code from AVATAR design under edition", '6'); diff --git a/src/ui/window/JDialogUPPAALValidation.java b/src/ui/window/JDialogUPPAALValidation.java index 211d588a0f3c85a196266d8da1a773fc102ad5cf..d9b272999f92a5b5cc1e344a28428f4810dfe144 100755 --- a/src/ui/window/JDialogUPPAALValidation.java +++ b/src/ui/window/JDialogUPPAALValidation.java @@ -88,11 +88,16 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti protected JTextField translatedText; protected TURTLEPanel tp; protected java.util.List<JCheckBox> customChecks; + protected boolean hasFiniteSize; + protected static String sizeInfiniteFIFO = "8"; + protected JTextField sizeOfInfiniteFIFO; + + 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); @@ -128,6 +133,20 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti } protected void initComponents() { + int index = spec.indexOf("DEFAULT_INFINITE_SIZE"); + String size = "1024"; + hasFiniteSize = (index > -1); + if (hasFiniteSize) { + String subspec = spec.substring(index+24, spec.length()); + int indexEnd = subspec.indexOf(";"); + //TraceManager.addDev("indexEnd = " + indexEnd + " subspec=" + subspec); + if (indexEnd == -1) { + hasFiniteSize = false; + } else { + size = subspec.substring(0, indexEnd); + TraceManager.addDev("size=" + size); + } + } Container c = getContentPane(); setFont(new Font("Helvetica", Font.PLAIN, 14)); @@ -143,7 +162,7 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti // first line panel1 //c1.gridwidth = 3; - c1.gridheight = 1; + c1.gridheight = 3; c1.weighty = 1.0; c1.weightx = 1.0; c1.gridwidth = GridBagConstraints.REMAINDER; //end row @@ -155,6 +174,34 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti jp1.add(deadlockE, c1); deadlockE.setSelected(deadlockEChecked);*/ + JPanel jp01 = new JPanel(); + GridBagLayout gridbag01 = new GridBagLayout(); + GridBagConstraints c01 = new GridBagConstraints(); + jp01.setLayout(gridbag01); + jp01.setBorder(new javax.swing.border.TitledBorder("Options of UPPAAL Specification")); + + + // first line panel01 + //c1.gridwidth = 3; + + c01.gridheight = 1; + c01.weighty = 1.0; + c01.weightx = 1.0; + c01.gridwidth = GridBagConstraints.REMAINDER; //end row + c01.fill = GridBagConstraints.BOTH; + c01.gridheight = 1; + + + sizeOfInfiniteFIFO = new JTextField(size, 10); + c01.gridwidth = 1; + jp01.add(new JLabel("Size of infinite FIFO = "), c01); + c01.gridwidth = GridBagConstraints.REMAINDER; //end row + jp01.add(sizeOfInfiniteFIFO, c01); + jp1.add(jp01, c1); + + c1.gridheight = 1; + + deadlockA = new JCheckBox("Search for absence of deadock situations"); deadlockA.addActionListener(this); jp1.add(deadlockA, c1); @@ -308,6 +355,17 @@ public class JDialogUPPAALValidation extends javax.swing.JDialog implements Acti } public void startProcess() { + // hack spec if necessary. + if (hasFiniteSize) { + int index = spec.indexOf("DEFAULT_INFINITE_SIZE"); + String specEnd = spec.substring(index+24, spec.length()); + String specbeg = spec.substring(0, index+24); + specbeg += sizeOfInfiniteFIFO.getText(); + specEnd = specEnd.substring(specEnd.indexOf(";"), specEnd.length()); + spec = specbeg + specEnd; + //TraceManager.addDev("spec=" + spec); + } + t = new Thread(this); mode = STARTED; setButtons();