From 69e2ee10cefc73d0d4aa8eaa13a2065ace4ba31f Mon Sep 17 00:00:00 2001 From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr> Date: Thu, 15 Jul 2010 15:40:17 +0000 Subject: [PATCH] AVATAR: Management of Timers: on AVATAR models, and also in the internal language + translation to UPPAAL --- src/avatartranslator/AvatarBlock.java | 126 ++++++---- src/avatartranslator/AvatarBlockTemplate.java | 24 +- src/avatartranslator/AvatarExpireTimer.java | 57 +++++ src/avatartranslator/AvatarResetTimer.java | 57 +++++ src/avatartranslator/AvatarSetTimer.java | 66 +++++ src/avatartranslator/AvatarSpecification.java | 11 + src/avatartranslator/AvatarStateMachine.java | 62 +++++ .../AvatarStateMachineElement.java | 14 ++ src/avatartranslator/AvatarTimerOperator.java | 66 +++++ .../touppaal/AVATAR2UPPAAL.java | 9 +- src/ui/AvatarDesignPanel.java | 4 + src/ui/AvatarDesignPanelTranslator.java | 84 +++++++ src/ui/ColorManager.java | 5 + src/ui/MainGUI.java | 24 +- src/ui/TGComponentManager.java | 22 +- src/ui/TGUIAction.java | 8 +- src/ui/avatarbd/AvatarBDBlock.java | 13 + src/ui/avatarbd/AvatarBDPanel.java | 10 + src/ui/avatarsmd/AvatarSMDExpireTimer.java | 229 +++++++++++++++++ src/ui/avatarsmd/AvatarSMDResetTimer.java | 225 +++++++++++++++++ src/ui/avatarsmd/AvatarSMDSetTimer.java | 238 ++++++++++++++++++ src/ui/avatarsmd/AvatarSMDToolBar.java | 15 ++ src/ui/window/JDialogAvatarTimer.java | 230 +++++++++++++++++ src/uppaaldesc/UPPAALTemplate.java | 5 + src/uppaaldesc/UPPAALTransition.java | 12 + 25 files changed, 1557 insertions(+), 59 deletions(-) create mode 100644 src/avatartranslator/AvatarExpireTimer.java create mode 100644 src/avatartranslator/AvatarResetTimer.java create mode 100644 src/avatartranslator/AvatarSetTimer.java create mode 100644 src/avatartranslator/AvatarTimerOperator.java create mode 100644 src/ui/avatarsmd/AvatarSMDExpireTimer.java create mode 100644 src/ui/avatarsmd/AvatarSMDResetTimer.java create mode 100644 src/ui/avatarsmd/AvatarSMDSetTimer.java create mode 100755 src/ui/window/JDialogAvatarTimer.java diff --git a/src/avatartranslator/AvatarBlock.java b/src/avatartranslator/AvatarBlock.java index c68f6ec095..56f9a8ff81 100644 --- a/src/avatartranslator/AvatarBlock.java +++ b/src/avatartranslator/AvatarBlock.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 AvatarBlock - * Creation: 20/05/2010 - * @version 1.0 20/05/2010 - * @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 AvatarBlock +* Creation: 20/05/2010 +* @version 1.0 20/05/2010 +* @author Ludovic APVRILLE +* @see +*/ package avatartranslator; @@ -244,6 +244,46 @@ public class AvatarBlock extends AvatarElement { return (asme != null); } + public void removeTimers(AvatarSpecification _spec, LinkedList<AvatarBlock> _addedBlocks) { + AvatarSignal as; + AvatarAttribute value; + + // Add new timer signals + for (AvatarAttribute aa: attributes) { + if (aa.getType() == AvatarType.TIMER) { + as = new AvatarSignal("set__" + aa.getName(), AvatarSignal.OUT, aa.getReferenceObject()); + value = new AvatarAttribute("__value", AvatarType.INTEGER, aa.getReferenceObject()); + as.addParameter(value); + addSignal(as); + addSignal(new AvatarSignal("reset__" + aa.getName(), AvatarSignal.OUT, aa.getReferenceObject())); + addSignal(new AvatarSignal("expire__" + aa.getName(), AvatarSignal.IN, aa.getReferenceObject())); + + // Create a timer block, and connect signals + AvatarBlock ab = AvatarBlockTemplate.getTimerBlock("Timer__" + aa.getName(), getReferenceObject()); + _addedBlocks.add(ab); + + AvatarRelation ar; + ar = new AvatarRelation("timerrelation", this, ab, getReferenceObject()); + ar.addSignals(getAvatarSignalWithName("set__" + aa.getName()), ab.getAvatarSignalWithName("set")); + ar.addSignals(getAvatarSignalWithName("reset__" + aa.getName()), ab.getAvatarSignalWithName("reset")); + ar.addSignals(getAvatarSignalWithName("expire__" + aa.getName()), ab.getAvatarSignalWithName("expire")); + _spec.addRelation(ar); + } + } + + // Modify the state machine + asm.removeTimers(this); + + // Remove Timer attribute + LinkedList<AvatarAttribute> tmps = attributes; + attributes = new LinkedList<AvatarAttribute>(); + for (AvatarAttribute aa: tmps) { + if (aa.getType() != AvatarType.TIMER) { + attributes.add(aa); + } + } + } + } \ No newline at end of file diff --git a/src/avatartranslator/AvatarBlockTemplate.java b/src/avatartranslator/AvatarBlockTemplate.java index 9a80fc0462..9e1716c693 100644 --- a/src/avatartranslator/AvatarBlockTemplate.java +++ b/src/avatartranslator/AvatarBlockTemplate.java @@ -59,12 +59,14 @@ public class AvatarBlockTemplate { public static AvatarBlock getTimerBlock(String _name, Object _reference) { AvatarBlock ab = new AvatarBlock(_name, _reference); - AvatarAttribute aa = new avatarAttribute("value", AvatarType.NATURAL, _reference); + AvatarAttribute aa = new AvatarAttribute("value", AvatarType.INTEGER, _reference); ab.addAttribute(aa); AvatarSignal set = new AvatarSignal("set", AvatarSignal.IN, _reference); AvatarSignal reset = new AvatarSignal("reset", AvatarSignal.IN, _reference); AvatarSignal expire = new AvatarSignal("expire", AvatarSignal.OUT, _reference); + AvatarAttribute val = new AvatarAttribute("__value", AvatarType.INTEGER, aa.getReferenceObject()); + set.addParameter(val); ab.addSignal(set); ab.addSignal(reset); ab.addSignal(expire); @@ -73,7 +75,7 @@ public class AvatarBlockTemplate { AvatarStartState ass = new AvatarStartState("start", _reference); asm.setStartState(ass); - asm.addElement(asm); + asm.addElement(ass); AvatarState as1 = new AvatarState("wait4set", _reference); asm.addElement(as1); @@ -86,16 +88,16 @@ public class AvatarBlockTemplate { asm.addElement(aaos1); AvatarActionOnSignal aaos2 = new AvatarActionOnSignal("set2", set, _reference); - aaos1.addValue("value"); + aaos2.addValue("value"); asm.addElement(aaos2); - AvatarActionOnSignal aaos3 = new AvatarActionOnSignal("reset1", set, _reference); + AvatarActionOnSignal aaos3 = new AvatarActionOnSignal("reset1", reset, _reference); asm.addElement(aaos3); - AvatarActionOnSignal aaos4 = new AvatarActionOnSignal("reset2", set, _reference); + AvatarActionOnSignal aaos4 = new AvatarActionOnSignal("reset2", reset, _reference); asm.addElement(aaos4); - AvatarActionOnSignal aaos5 = new AvatarActionOnSignal("expire", set, _reference); + AvatarActionOnSignal aaos5 = new AvatarActionOnSignal("expire", expire, _reference); asm.addElement(aaos5); AvatarTransition at; @@ -109,15 +111,17 @@ public class AvatarBlockTemplate { at = makeAvatarEmptyTransitionBetween(asm, aaos2, as2, _reference); // expire - at = makeAvatarEmptyTransitionBetween(asm, aaos5, as1, _reference); at = makeAvatarEmptyTransitionBetween(asm, as2, aaos5, _reference); at.setDelays("value", "value"); + at = makeAvatarEmptyTransitionBetween(asm, aaos5, as1, _reference); // reset - at = makeAvatarEmptyTransitionBetween(asm, aaos3, as1, _reference); at = makeAvatarEmptyTransitionBetween(asm, as1, aaos3, _reference); - at = makeAvatarEmptyTransitionBetween(asm, aaos4, as1, _reference); + at = makeAvatarEmptyTransitionBetween(asm, aaos3, as1, _reference); + at = makeAvatarEmptyTransitionBetween(asm, as2, aaos4, _reference); + at = makeAvatarEmptyTransitionBetween(asm, aaos4, as1, _reference); + return ab; @@ -126,7 +130,7 @@ public class AvatarBlockTemplate { public static AvatarTransition makeAvatarEmptyTransitionBetween(AvatarStateMachine _asm, AvatarStateMachineElement _elt1, AvatarStateMachineElement _elt2, Object _reference) { AvatarTransition at = new AvatarTransition("tr", _reference); - asm.addElement(at); + _asm.addElement(at); _elt1.addNext(at); at.addNext(_elt2); diff --git a/src/avatartranslator/AvatarExpireTimer.java b/src/avatartranslator/AvatarExpireTimer.java new file mode 100644 index 0000000000..11899bd62f --- /dev/null +++ b/src/avatartranslator/AvatarExpireTimer.java @@ -0,0 +1,57 @@ +/**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 AvatarExpireTimer + * Creation: 15/07/2010 + * @version 1.0 15/07/2010 + * @author Ludovic APVRILLE + * @see + */ + +package avatartranslator; + +import java.util.*; + + +public class AvatarExpireTimer extends AvatarTimerOperator { + + public AvatarExpireTimer(String _name, Object _referenceObject) { + super(_name, _referenceObject); + } + +} \ No newline at end of file diff --git a/src/avatartranslator/AvatarResetTimer.java b/src/avatartranslator/AvatarResetTimer.java new file mode 100644 index 0000000000..adb0e512a7 --- /dev/null +++ b/src/avatartranslator/AvatarResetTimer.java @@ -0,0 +1,57 @@ +/**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 AvatarResetTimer + * Creation: 15/07/2010 + * @version 1.0 15/07/2010 + * @author Ludovic APVRILLE + * @see + */ + +package avatartranslator; + +import java.util.*; + + +public class AvatarResetTimer extends AvatarTimerOperator { + + public AvatarResetTimer(String _name, Object _referenceObject) { + super(_name, _referenceObject); + } + +} \ No newline at end of file diff --git a/src/avatartranslator/AvatarSetTimer.java b/src/avatartranslator/AvatarSetTimer.java new file mode 100644 index 0000000000..356c40e8aa --- /dev/null +++ b/src/avatartranslator/AvatarSetTimer.java @@ -0,0 +1,66 @@ +/**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 AvatarSetTimer + * Creation: 15/07/2010 + * @version 1.0 15/07/2010 + * @author Ludovic APVRILLE + * @see + */ + +package avatartranslator; + +import java.util.*; + + +public class AvatarSetTimer extends AvatarTimerOperator { + protected String setValue; + + public AvatarSetTimer(String _name, Object _referenceObject) { + super(_name, _referenceObject); + } + + public void setTimerValue(String _setValue) { + setValue = _setValue; + } + + public String getTimerValue() { + return setValue; + } + +} \ No newline at end of file diff --git a/src/avatartranslator/AvatarSpecification.java b/src/avatartranslator/AvatarSpecification.java index afece0248c..f0ccac724c 100644 --- a/src/avatartranslator/AvatarSpecification.java +++ b/src/avatartranslator/AvatarSpecification.java @@ -126,6 +126,17 @@ public class AvatarSpecification extends AvatarElement { } } + public void removeTimers() { + LinkedList<AvatarBlock> addedBlocks = new LinkedList<AvatarBlock>(); + for(AvatarBlock block: blocks) { + block.removeTimers(this, addedBlocks); + } + + for(int i=0; i<addedBlocks.size(); i++) { + addBlock(addedBlocks.get(i)); + } + } + public AvatarRelation getAvatarRelationWithSignal(AvatarSignal _as) { for(AvatarRelation ar: relations) { if (ar.hasSignal(_as) > -1) { diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java index 47f37ffdce..6b1433203e 100644 --- a/src/avatartranslator/AvatarStateMachine.java +++ b/src/avatartranslator/AvatarStateMachine.java @@ -354,6 +354,68 @@ public class AvatarStateMachine extends AvatarElement { } return null; } + + public void removeTimers(AvatarBlock _block) { + AvatarSetTimer ast; + AvatarTimerOperator ato; + + LinkedList<AvatarStateMachineElement> olds = new LinkedList<AvatarStateMachineElement>(); + LinkedList<AvatarStateMachineElement> news = new LinkedList<AvatarStateMachineElement>(); + + + for(AvatarStateMachineElement elt: elements) { + // Set timer... + if (elt instanceof AvatarSetTimer) { + ast = (AvatarSetTimer)elt; + AvatarActionOnSignal aaos = new AvatarActionOnSignal(elt.getName(), _block.getAvatarSignalWithName("set__" + ast.getTimer().getName()), elt.getReferenceObject()); + aaos.addValue(ast.getTimerValue()); + olds.add(elt); + news.add(aaos); + + // Reset timer + } else if (elt instanceof AvatarResetTimer) { + ato = (AvatarTimerOperator)elt; + AvatarActionOnSignal aaos = new AvatarActionOnSignal(elt.getName(), _block.getAvatarSignalWithName("reset__" + ato.getTimer().getName()), elt.getReferenceObject()); + olds.add(elt); + news.add(aaos); + + // Expire timer + } else if (elt instanceof AvatarExpireTimer) { + ato = (AvatarTimerOperator)elt; + AvatarActionOnSignal aaos = new AvatarActionOnSignal(elt.getName(), _block.getAvatarSignalWithName("expire__" + ato.getTimer().getName()), elt.getReferenceObject()); + olds.add(elt); + news.add(aaos); + } + } + + // Replacing old elements with new ones + AvatarStateMachineElement oldelt, newelt; + for(int i = 0; i<olds.size(); i++) { + oldelt = olds.get(i); + newelt = news.get(i); + replace(oldelt, newelt); + } + } + + public void replace(AvatarStateMachineElement oldone, AvatarStateMachineElement newone) { + + TraceManager.addDev("Replacing " + oldone + " with " + newone); + + addElement(oldone); + removeElement(newone); + + // Previous elements + LinkedList<AvatarStateMachineElement> previous = getPreviousElementsOf(oldone); + for(AvatarStateMachineElement elt: previous) { + elt.replaceAllNext(oldone, newone); + } + + // Next elements + for(int i=0; i<oldone.nbOfNexts(); i++) { + AvatarStateMachineElement elt = oldone.getNext(i); + newone.addNext(elt); + } + } } \ No newline at end of file diff --git a/src/avatartranslator/AvatarStateMachineElement.java b/src/avatartranslator/AvatarStateMachineElement.java index a21b64db66..5c05f7a5c9 100644 --- a/src/avatartranslator/AvatarStateMachineElement.java +++ b/src/avatartranslator/AvatarStateMachineElement.java @@ -118,6 +118,20 @@ public class AvatarStateMachineElement extends AvatarElement { nexts.remove(_elt); } + public void replaceAllNext(AvatarStateMachineElement oldone, AvatarStateMachineElement newone) { + if (nexts.contains(oldone)) { + LinkedList<AvatarStateMachineElement> oldnexts = nexts; + nexts = new LinkedList<AvatarStateMachineElement>(); + for(AvatarStateMachineElement elt: oldnexts) { + if (elt == oldone) { + nexts.add(newone); + } else { + nexts.add(oldone); + } + } + } + } + public void removeAllNexts() { nexts.clear(); } diff --git a/src/avatartranslator/AvatarTimerOperator.java b/src/avatartranslator/AvatarTimerOperator.java new file mode 100644 index 0000000000..475170e138 --- /dev/null +++ b/src/avatartranslator/AvatarTimerOperator.java @@ -0,0 +1,66 @@ +/**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 AvatarTimerOperator + * Creation: 15/07/2010 + * @version 1.0 15/07/2010 + * @author Ludovic APVRILLE + * @see + */ + +package avatartranslator; + +import java.util.*; + + +public class AvatarTimerOperator extends AvatarStateMachineElement { + protected AvatarAttribute timer; + + public AvatarTimerOperator(String _name, Object _referenceObject) { + super(_name, _referenceObject); + } + + public void setTimer(AvatarAttribute _timer) { + timer = _timer; + } + + public AvatarAttribute getTimer() { + return timer; + } + +} \ No newline at end of file diff --git a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java index d315fd24bf..f2399b5529 100755 --- a/src/avatartranslator/touppaal/AVATAR2UPPAAL.java +++ b/src/avatartranslator/touppaal/AVATAR2UPPAAL.java @@ -150,8 +150,9 @@ public class AVATAR2UPPAAL { spec = new UPPAALSpec(); avspec.removeCompositeStates(); + avspec.removeTimers(); - //TraceManager.addDev("Spec:" + avspec.toString()); + //TraceManager.addDev("-> Spec:" + avspec.toString()); UPPAALLocation.reinitID(); gatesNotSynchronized = new LinkedList(); @@ -503,6 +504,9 @@ public class AVATAR2UPPAAL { loc = hash.get(_elt); if (loc != null) { + if (_previous == null) { + TraceManager.addDev("************************* NULL PREVIOUS !!!!!!!*****************"); + } tr = addTransition(_template, _previous, loc); return; } @@ -533,7 +537,6 @@ public class AVATAR2UPPAAL { setGuard(tr, arand.getVariable() + "<" + arand.getMaxValue()); _previous.setCommitted(); loc.setCommitted(); - hash.put(_elt, loc); hash.put(_elt, _previous); makeElementBehavior(_block, _template, _elt.getNext(0), loc, _end, null, false); return; @@ -551,6 +554,7 @@ public class AVATAR2UPPAAL { } state = (AvatarState)_elt; + hash.put(_elt, _previous); // We translate at the same time the state and its next transitions (guard and time + first method call) // We assume all nexts are transitions @@ -575,7 +579,6 @@ public class AVATAR2UPPAAL { // Reset the clock tmps = "h__ = 0"; loc = addLocation(_template); - hash.put(_elt, loc); tr = addTransition(_template, _previous, loc); setAssignment(tr, tmps); _previous.setCommitted(); diff --git a/src/ui/AvatarDesignPanel.java b/src/ui/AvatarDesignPanel.java index 74745193fa..ef4f7e5177 100644 --- a/src/ui/AvatarDesignPanel.java +++ b/src/ui/AvatarDesignPanel.java @@ -145,6 +145,10 @@ public class AvatarDesignPanel extends TURTLEPanel { public Vector getAllSignals(String _name) { return abdp.getAllSignalsOfBlock(_name); } + + public Vector getAllTimers(String _name) { + return abdp.getAllTimersOfBlock(_name); + } public String saveHeaderInXml() { return "<Modeling type=\"AVATAR Design\" nameTab=\"" + mgui.getTabName(this) + "\" >\n"; diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java index 990575267f..11c7b984f8 100644 --- a/src/ui/AvatarDesignPanelTranslator.java +++ b/src/ui/AvatarDesignPanelTranslator.java @@ -362,6 +362,9 @@ public class AvatarDesignPanelTranslator { AvatarStartState astart; AvatarState astate; AvatarRandom arandom; + AvatarSetTimer asettimer; + AvatarResetTimer aresettimer; + AvatarExpireTimer aexpiretimer; int i; String tmp; TAttribute ta; @@ -531,6 +534,87 @@ public class AvatarDesignPanelTranslator { asm.addElement(arandom); listE.addCor(arandom, tgc); + + // Set timer + } else if (tgc instanceof AvatarSMDSetTimer) { + tmp = ((AvatarSMDSetTimer)tgc).getTimerName(); + aa = _ab.getAvatarAttributeWithName(tmp); + if (aa == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed timer parameter: " + tmp + " in timer setting"); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + if (aa.getType() != AvatarType.TIMER) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed parameter: " + tmp + " in timer setting: shall be a parameter of type \"Timer\""); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + tmp = modifyString(((AvatarSMDSetTimer)tgc).getTimerValue()); + error = AvatarSyntaxChecker.isAValidIntExpr(_as, _ab, tmp); + if (error < 0) { + makeError(error, tdp, _ab, tgc, "value of the timer setting", tmp); + } + asettimer = new AvatarSetTimer("settimer__" + aa.getName(), tgc); + asettimer.setTimer(aa); + asettimer.setTimerValue(tmp); + asm.addElement(asettimer); + listE.addCor(asettimer, tgc); + } + } + + // Reset timer + } else if (tgc instanceof AvatarSMDResetTimer) { + tmp = ((AvatarSMDResetTimer)tgc).getTimerName(); + aa = _ab.getAvatarAttributeWithName(tmp); + if (aa == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed timer parameter: " + tmp + " in timer reset"); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + if (aa.getType() != AvatarType.TIMER) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed parameter: " + tmp + " in timer reset: shall be a parameter of type \"Timer\""); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + aresettimer = new AvatarResetTimer("resettimer__" + aa.getName(), tgc); + aresettimer.setTimer(aa); + asm.addElement(aresettimer); + listE.addCor(aresettimer, tgc); + } + } + + // Expire timer + } else if (tgc instanceof AvatarSMDExpireTimer) { + tmp = ((AvatarSMDExpireTimer)tgc).getTimerName(); + aa = _ab.getAvatarAttributeWithName(tmp); + if (aa == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed timer parameter: " + tmp + " in timer expiration"); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + if (aa.getType() != AvatarType.TIMER) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed parameter: " + tmp + " in timer expiration: shall be a parameter of type \"Timer\""); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + aexpiretimer = new AvatarExpireTimer("expiretimer__" + aa.getName(), tgc); + aexpiretimer.setTimer(aa); + asm.addElement(aexpiretimer); + listE.addCor(aexpiretimer, tgc); + } + } // Start state } else if (tgc instanceof AvatarSMDStartState) { diff --git a/src/ui/ColorManager.java b/src/ui/ColorManager.java index 5c3f9d33e0..9e3f732990 100755 --- a/src/ui/ColorManager.java +++ b/src/ui/ColorManager.java @@ -147,6 +147,11 @@ public class ColorManager { //public static final Color AVATAR_STATE = new Color(149, 193, 210); public static final Color AVATAR_STATE = new Color(193, 218, 241); + public static final Color AVATAR_SET_TIMER = new Color(255, 180, 105); + public static final Color AVATAR_RESET_TIMER = new Color(255, 180, 105); + public static final Color AVATAR_EXPIRE_TIMER = new Color(255, 180, 105); + + public static final Color AVATAR_REQUIREMENT_TOP = new Color(228, 241, 242); public static final Color AVATAR_REQUIREMENT_ATTRIBUTES = new Color(205, 196, 109); diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java index 47283b059c..7b6afad30f 100755 --- a/src/ui/MainGUI.java +++ b/src/ui/MainGUI.java @@ -2905,6 +2905,22 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener { return adp.getAllSignals(name); } + + public Vector getAllTimers() { + TURTLEPanel tp = getCurrentTURTLEPanel(); + if (tp == null) { + return null; + } + + if (!(tp instanceof AvatarDesignPanel)) { + return null; + } + AvatarDesignPanel adp = (AvatarDesignPanel)tp; + + String name = getCurrentTDiagramPanel().getName(); + + return adp.getAllTimers(name); + } public Vector getCheckingErrors() { return gtm.getCheckingErrors(); @@ -6085,6 +6101,12 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener { actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.AVATARSMD_CHOICE); } else if (command.equals(actions[TGUIAction.ASMD_RANDOM].getActionCommand())) { actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.AVATARSMD_RANDOM); + } else if (command.equals(actions[TGUIAction.ASMD_SET_TIMER].getActionCommand())) { + actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.AVATARSMD_SET_TIMER); + } else if (command.equals(actions[TGUIAction.ASMD_RESET_TIMER].getActionCommand())) { + actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.AVATARSMD_RESET_TIMER); + } else if (command.equals(actions[TGUIAction.ASMD_EXPIRE_TIMER].getActionCommand())) { + actionOnButton(TGComponentManager.COMPONENT, TGComponentManager.AVATARSMD_EXPIRE_TIMER); // AVATAR RD } else if (command.equals(actions[TGUIAction.ARD_EDIT].getActionCommand())) { @@ -6559,7 +6581,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener { newTURTLEOSDesign = createMenuItem("New TURTLE-OS Design"); newNCDesign = createMenuItem("New Network Calculus Design"); newAVATARRequirement = createMenuItem("New AVATAR Requirement Diagrams"); - newAVATARBD = createMenuItem("New AVATAR Block Diagram"); + newAVATARBD = createMenuItem("New AVATAR Design"); menu = new JPopupMenu("TURTLE analysis, design and deployment / DIPLODOCUS design / Proactive design"); menu.add(moveLeft); diff --git a/src/ui/TGComponentManager.java b/src/ui/TGComponentManager.java index 603963bdad..f36b7cccba 100755 --- a/src/ui/TGComponentManager.java +++ b/src/ui/TGComponentManager.java @@ -303,6 +303,9 @@ public class TGComponentManager { public static final int AVATARSMD_STATE = 5106; public static final int AVATARSMD_CHOICE = 5107; public static final int AVATARSMD_RANDOM = 5108; + public static final int AVATARSMD_SET_TIMER = 5109; + public static final int AVATARSMD_RESET_TIMER = 5110; + public static final int AVATARSMD_EXPIRE_TIMER = 5111; // AVATAR RD -> starts at 5200 public static final int AVATARRD_REQUIREMENT = 5200; @@ -367,6 +370,16 @@ public class TGComponentManager { case AVATARSMD_RANDOM: tgc = new AvatarSMDRandom(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp); break; + case AVATARSMD_SET_TIMER: + tgc = new AvatarSMDSetTimer(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp); + break; + case AVATARSMD_RESET_TIMER: + tgc = new AvatarSMDResetTimer(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp); + break; + case AVATARSMD_EXPIRE_TIMER: + tgc = new AvatarSMDExpireTimer(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp); + break; + case AVATARRD_REQUIREMENT: tgc = new AvatarRDRequirement(x, y, tdp.getMinX(), tdp.getMaxX(), tdp.getMinY(), tdp.getMaxY(), false, null, tdp); break; @@ -847,7 +860,14 @@ public class TGComponentManager { } else if (tgc instanceof AvatarSMDChoice) { return AVATARSMD_CHOICE; } else if (tgc instanceof AvatarSMDRandom) { - return AVATARSMD_RANDOM; + return AVATARSMD_RANDOM; + } else if (tgc instanceof AvatarSMDSetTimer) { + return AVATARSMD_SET_TIMER; + } else if (tgc instanceof AvatarSMDResetTimer) { + return AVATARSMD_RESET_TIMER; + } else if (tgc instanceof AvatarSMDExpireTimer) { + return AVATARSMD_EXPIRE_TIMER; + // AVATAR RD } else if (tgc instanceof AvatarRDRequirement) { diff --git a/src/ui/TGUIAction.java b/src/ui/TGUIAction.java index 17e3c788e9..49a2b00db8 100755 --- a/src/ui/TGUIAction.java +++ b/src/ui/TGUIAction.java @@ -312,6 +312,9 @@ public class TGUIAction extends AbstractAction { public static final int ASMD_STATE = 299; public static final int ASMD_CHOICE = 325; public static final int ASMD_RANDOM = 326; + public static final int ASMD_SET_TIMER = 327; + public static final int ASMD_RESET_TIMER = 328; + public static final int ASMD_EXPIRE_TIMER = 329; // AVATAR Requirement public static final int ARD_EDIT = 300; @@ -446,7 +449,7 @@ public class TGUIAction extends AbstractAction { //Action for the help button created by Solange public static final int PRUEBA_1 = 205; - public static final int NB_ACTION = 327; + public static final int NB_ACTION = 330; private static final TAction [] actions = new TAction[NB_ACTION]; @@ -844,6 +847,9 @@ public class TGUIAction extends AbstractAction { actions[ASMD_STATE] = new TAction("add-asmd-state", "State", IconManager.imgic5036, IconManager.imgic5036, "State", "Add a new state to the currently opened AVATAR state machine diagram", 0); actions[ASMD_CHOICE] = new TAction("add-asmd-choice", "Add Choice", IconManager.imgic208, IconManager.imgic208, "Choice", "Add a choice - non-deterministic or guarded - to the currently opened AVATAR state machine diagram", 0); actions[ASMD_RANDOM] = new TAction("add-asmd-random", "Add random", IconManager.imgic924, IconManager.imgic924, "Select random", "Add a random operator to the currently opened AVATAR State Machine diagram", 0); + actions[ASMD_SET_TIMER] = new TAction("add-asmd-setrimer", "Set timer", IconManager.imgic924, IconManager.imgic924, "Set timer", "Add a set timer operator to the currently opened AVATAR State Machine diagram", 0); + actions[ASMD_RESET_TIMER] = new TAction("add-asmd-resettimer", "Reset timer", IconManager.imgic924, IconManager.imgic924, "Reset timer", "Add a reset timer operator to the currently opened AVATAR State Machine diagram", 0); + actions[ASMD_EXPIRE_TIMER] = new TAction("add-asmd-expiretimer", "Timer expiration", IconManager.imgic924, IconManager.imgic924, "Wait for timer expiration", "Add a timer expiration operator to the currently opened AVATAR State Machine diagram", 0); // AVATAR Requirement Diagrams diff --git a/src/ui/avatarbd/AvatarBDBlock.java b/src/ui/avatarbd/AvatarBDBlock.java index 01e2101495..15298856c1 100644 --- a/src/ui/avatarbd/AvatarBDBlock.java +++ b/src/ui/avatarbd/AvatarBDBlock.java @@ -825,6 +825,19 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S return v; } + public Vector getAllTimerList() { + Vector v = new Vector(); + TAttribute a; + + for(int i=0; i<myAttributes.size(); i++) { + a = (TAttribute)(myAttributes.elementAt(i)); + if (a.getType() == TAttribute.TIMER) { + v.add(a.getId()); + } + } + return v; + } + public AvatarSignal getAvatarSignalFromName(String _name) { AvatarSignal as; for(int i=0; i<mySignals.size(); i++) { diff --git a/src/ui/avatarbd/AvatarBDPanel.java b/src/ui/avatarbd/AvatarBDPanel.java index 21766bb8c1..496de1a275 100644 --- a/src/ui/avatarbd/AvatarBDPanel.java +++ b/src/ui/avatarbd/AvatarBDPanel.java @@ -590,6 +590,16 @@ public class AvatarBDPanel extends TDiagramPanel { return null; } + public Vector getAllTimersOfBlock(String _name) { + LinkedList<AvatarBDBlock> list = getFullBlockList(); + for(AvatarBDBlock block: list) { + if (block.getBlockName().compareTo(_name) ==0) { + return block.getAllTimerList(); + } + } + return null; + } + public Vector getAttributesOfDataType(String _name) { TGComponent tgc; Iterator iterator = componentList.listIterator(); diff --git a/src/ui/avatarsmd/AvatarSMDExpireTimer.java b/src/ui/avatarsmd/AvatarSMDExpireTimer.java new file mode 100644 index 0000000000..bbbb52d717 --- /dev/null +++ b/src/ui/avatarsmd/AvatarSMDExpireTimer.java @@ -0,0 +1,229 @@ +/**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 AvatarSMDExpireTimer + * Action of waiting for the expiration of a timer + * Creation: 15/07/2010 + * @version 1.0 15/07/2010 + * @author Ludovic APVRILLE + * @see + */ + +package ui.avatarsmd; + +import java.awt.*; +import java.awt.geom.*; +import javax.swing.*; + +import java.util.*; + +import org.w3c.dom.*; + +import myutil.*; +import ui.*; +import ui.window.*; + +public class AvatarSMDExpireTimer extends AvatarSMDBasicComponent implements CheckableAccessibility, BasicErrorHighlight { + protected int lineLength = 5; + protected int textX = 5; + protected int textY = 15; + protected int arc = 5; + protected int linebreak = 10; + + protected int hourglassWidth = 10; + protected int hourglassSpace = 2; + + + protected int stateOfError = 0; // Not yet checked + + public AvatarSMDExpireTimer(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) { + super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp); + + width = 30; + height = 20; + minWidth = 30; + + nbConnectingPoint = 2; + connectingPoint = new TGConnectingPoint[2]; + connectingPoint[0] = new AvatarSMDConnectingPoint(this, 0, -lineLength, true, false, 0.5, 0.0); + connectingPoint[1] = new AvatarSMDConnectingPoint(this, 0, lineLength, false, true, 0.5, 1.0); + + addTGConnectingPointsComment(); + + moveable = true; + editable = true; + removable = true; + + name = "Reset timer"; + value = "expire(timer1)"; + //makeValue(); + + myImageIcon = IconManager.imgic904; + } + + public void internalDrawing(Graphics g) { + + int w = g.getFontMetrics().stringWidth(value); + int w1 = Math.max(minWidth, w + 2 * textX + linebreak); + if ((w1 != width) & (!tdp.isScaled())) { + setCd(x + width/2 - w1/2, y); + width = w1; //updateConnectingPoints(); + } + + + if (stateOfError > 0) { + Color c = g.getColor(); + switch(stateOfError) { + case ErrorHighlight.OK: + g.setColor(ColorManager.AVATAR_EXPIRE_TIMER); + break; + default: + g.setColor(ColorManager.UNKNOWN_BOX_ACTION); + } + // Making the polygon + int [] px1 = {x, x+width-linebreak, x+width, x+width-linebreak, x}; + int [] py1 = {y, y, y+(height/2), y+height, y+height}; + g.fillPolygon(px1, py1, 5); + g.setColor(c); + } + + //g.drawRoundRect(x, y, width, height, arc, arc); + Color c = g.getColor(); + //System.out.println("Color=" + c); + + g.drawLine(x+(width/2), y, x+(width/2), y - lineLength); + g.drawLine(x+(width/2), y+height, x+(width/2), y + lineLength + height); + + /*if (g.getColor().equals(ColorManager.NORMAL_0)) { + g.setColor(ColorManager.TML_PORT_EVENT); + }*/ + + int x1 = x + 1; + int y1 = y + 1; + int height1 = height; + int width1 = width; + g.setColor(ColorManager.AVATAR_EXPIRE_TIMER); + g.drawLine(x1, y1, x1+width1, y1); + g.drawLine(x1+width1, y1, x1+width1, y1+height1); + g.drawLine(x1, y1+height1, x1+width1, y1+height1); + g.drawLine(x1, y1, x1+linebreak, y1+height1/2); + g.drawLine(x1, y1+height1, x1+linebreak, y1+height1/2); + g.setColor(c); + + g.drawLine(x, y, x+width, y); + g.drawLine(x+width, y, x+width, y+height); + g.drawLine(x, y+height, x+width, y+height); + g.drawLine(x, y, x+linebreak, y+height/2); + g.drawLine(x, y+height, x+linebreak, y+height/2); + + // hourglass + g.drawLine(x+width+hourglassSpace, y, x+width+hourglassSpace + hourglassWidth, y); + g.drawLine(x+width+hourglassSpace, y+height, x+width+hourglassSpace + hourglassWidth, y+height); + g.drawLine(x+width+hourglassSpace, y, x+width+hourglassSpace + hourglassWidth, y+height); + g.drawLine(x+width+hourglassSpace, y+height, x+width+hourglassSpace + hourglassWidth, y); + + //g.drawString("sig()", x+(width-w) / 2, y); + g.drawString(value, x + (width - w) / 2 + textX, y + textY); + + + } + + public TGComponent isOnMe(int _x, int _y) { + if (GraphicLib.isInRectangle(_x, _y, x, y, width + hourglassSpace + hourglassWidth, height)) { + return this; + } + + if ((int)(Line2D.ptSegDistSq(x+(width/2), y-lineLength, x+(width/2), y + lineLength + height, _x, _y)) < distanceSelected) { + return this; + } + + return null; + } + + public void makeValue() { + } + + public String getTimerName() { + return AvatarSignal.getValue(value, 0); + } + + public boolean editOndoubleClick(JFrame frame) { + Vector timers = tdp.getMGUI().getAllTimers(); + TraceManager.addDev("Nb of timers:" + timers.size()); + + JDialogAvatarTimer jdat = new JDialogAvatarTimer(frame, "Timer expiration", getTimerName(), "", timers, false); + jdat.setSize(350, 300); + GraphicLib.centerOnParent(jdat); + jdat.show(); // blocked until dialog has been closed + + if (jdat.hasBeenCancelled()) { + return false; + } + + String val0 = jdat.getTimer(); + + // valid signal? + if (!AvatarSignal.isAValidUseSignal(val0)) { + JOptionPane.showMessageDialog(frame, + "Could not change the setting of the timer: invalid name for the timer", + "Error", + JOptionPane.INFORMATION_MESSAGE); + return false; + } + + value = "expire(" + val0 + ")"; + + return true; + + } + + + + + public int getType() { + return TGComponentManager.AVATARSMD_EXPIRE_TIMER; + } + + public int getDefaultConnector() { + return TGComponentManager.AVATARSMD_CONNECTOR; + } + + public void setStateAction(int _stateAction) { + stateOfError = _stateAction; + } +} diff --git a/src/ui/avatarsmd/AvatarSMDResetTimer.java b/src/ui/avatarsmd/AvatarSMDResetTimer.java new file mode 100644 index 0000000000..4291c9f20c --- /dev/null +++ b/src/ui/avatarsmd/AvatarSMDResetTimer.java @@ -0,0 +1,225 @@ +/**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 AvatarSMDResetTimer + * Action of resetting a timer + * Creation: 15/07/2010 + * @version 1.0 15/07/2010 + * @author Ludovic APVRILLE + * @see + */ + +package ui.avatarsmd; + +import java.awt.*; +import java.awt.geom.*; +import javax.swing.*; + +import java.util.*; + +import org.w3c.dom.*; + +import myutil.*; +import ui.*; +import ui.window.*; + +public class AvatarSMDResetTimer extends AvatarSMDBasicComponent implements CheckableAccessibility, BasicErrorHighlight { + protected int lineLength = 5; + protected int textX = 5; + protected int textY = 15; + protected int arc = 5; + protected int linebreak = 10; + + protected int hourglassWidth = 10; + protected int hourglassSpace = 2; + + + protected int stateOfError = 0; // Not yet checked + + public AvatarSMDResetTimer(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) { + super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp); + + width = 30; + height = 20; + minWidth = 30; + + nbConnectingPoint = 2; + connectingPoint = new TGConnectingPoint[2]; + connectingPoint[0] = new AvatarSMDConnectingPoint(this, 0, -lineLength, true, false, 0.5, 0.0); + connectingPoint[1] = new AvatarSMDConnectingPoint(this, 0, lineLength, false, true, 0.5, 1.0); + + addTGConnectingPointsComment(); + + moveable = true; + editable = true; + removable = true; + + name = "Reset timer"; + value = "reset(timer1)"; + //makeValue(); + + myImageIcon = IconManager.imgic904; + } + + public void internalDrawing(Graphics g) { + + int w = g.getFontMetrics().stringWidth(value); + int w1 = Math.max(minWidth, w + 2 * textX); + if ((w1 != width) & (!tdp.isScaled())) { + setCd(x + width/2 - w1/2, y); + width = w1; //updateConnectingPoints(); + } + + + if (stateOfError > 0) { + Color c = g.getColor(); + switch(stateOfError) { + case ErrorHighlight.OK: + g.setColor(ColorManager.AVATAR_SET_TIMER); + break; + default: + g.setColor(ColorManager.UNKNOWN_BOX_ACTION); + } + // Making the polygon + int [] px1 = {x, x+width-linebreak, x+width, x+width-linebreak, x}; + int [] py1 = {y, y, y+(height/2), y+height, y+height}; + g.fillPolygon(px1, py1, 5); + g.setColor(c); + } + + //g.drawRoundRect(x, y, width, height, arc, arc); + Color c = g.getColor(); + //System.out.println("Color=" + c); + + g.drawLine(x+(width/2), y, x+(width/2), y - lineLength); + g.drawLine(x+(width/2), y+height, x+(width/2), y + lineLength + height); + + int x1 = x + 1; + int y1 = y + 1; + int height1 = height; + int width1 = width; + g.setColor(ColorManager.AVATAR_RESET_TIMER); + g.drawLine(x1, y1, x1+width1-linebreak, y1); + g.drawLine(x1, y1+height1, x1+width1-linebreak, y1+height1); + g.drawLine(x1, y1, x1, y1+height1); + g.drawLine(x1+width1-linebreak, y1, x1+width1, y1+height1/2); + g.drawLine(x1+width1-linebreak, y1+height1, x1+width1, y1+height1/2); + g.setColor(c); + + g.drawLine(x, y, x+width-linebreak, y); + g.drawLine(x, y+height, x+width-linebreak, y+height); + g.drawLine(x, y, x, y+height); + g.drawLine(x+width-linebreak, y, x+width, y+height/2); + g.drawLine(x+width-linebreak, y+height, x+width, y+height/2); + + // hourglass + g.drawLine(x+width+hourglassSpace, y, x+width+hourglassSpace + hourglassWidth, y); + g.drawLine(x+width+hourglassSpace, y+height, x+width+hourglassSpace + hourglassWidth, y+height); + g.drawLine(x+width+hourglassSpace, y, x+width+hourglassSpace + hourglassWidth, y+height); + g.drawLine(x+width+hourglassSpace, y+height, x+width+hourglassSpace + hourglassWidth, y); + + //g.drawString("sig()", x+(width-w) / 2, y); + g.drawString(value, x + (width - w) / 2 , y + textY); + + + } + + public TGComponent isOnMe(int _x, int _y) { + if (GraphicLib.isInRectangle(_x, _y, x, y, width + hourglassSpace + hourglassWidth, height)) { + return this; + } + + if ((int)(Line2D.ptSegDistSq(x+(width/2), y-lineLength, x+(width/2), y + lineLength + height, _x, _y)) < distanceSelected) { + return this; + } + + return null; + } + + public void makeValue() { + } + + public String getTimerName() { + return AvatarSignal.getValue(value, 0); + } + + public boolean editOndoubleClick(JFrame frame) { + Vector timers = tdp.getMGUI().getAllTimers(); + TraceManager.addDev("Nb of timers:" + timers.size()); + + JDialogAvatarTimer jdat = new JDialogAvatarTimer(frame, "Reset timer", getTimerName(), "", timers, false); + jdat.setSize(350, 300); + GraphicLib.centerOnParent(jdat); + jdat.show(); // blocked until dialog has been closed + + if (jdat.hasBeenCancelled()) { + return false; + } + + String val0 = jdat.getTimer(); + + // valid signal? + if (!AvatarSignal.isAValidUseSignal(val0)) { + JOptionPane.showMessageDialog(frame, + "Could not change the setting of the timer: invalid name for the timer", + "Error", + JOptionPane.INFORMATION_MESSAGE); + return false; + } + + value = "reset(" + val0 + ")"; + + return true; + + } + + + + + public int getType() { + return TGComponentManager.AVATARSMD_RESET_TIMER; + } + + public int getDefaultConnector() { + return TGComponentManager.AVATARSMD_CONNECTOR; + } + + public void setStateAction(int _stateAction) { + stateOfError = _stateAction; + } +} diff --git a/src/ui/avatarsmd/AvatarSMDSetTimer.java b/src/ui/avatarsmd/AvatarSMDSetTimer.java new file mode 100644 index 0000000000..30b35c46d9 --- /dev/null +++ b/src/ui/avatarsmd/AvatarSMDSetTimer.java @@ -0,0 +1,238 @@ +/**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 AvatarSMDSetTimer + * Action of setting a timer + * Creation: 15/07/2010 + * @version 1.0 15/07/2010 + * @author Ludovic APVRILLE + * @see + */ + +package ui.avatarsmd; + +import java.awt.*; +import java.awt.geom.*; +import javax.swing.*; + +import java.util.*; + +import org.w3c.dom.*; + +import myutil.*; +import ui.*; +import ui.window.*; + +public class AvatarSMDSetTimer extends AvatarSMDBasicComponent implements CheckableAccessibility, BasicErrorHighlight { + protected int lineLength = 5; + protected int textX = 5; + protected int textY = 15; + protected int arc = 5; + protected int linebreak = 10; + + protected int hourglassWidth = 10; + protected int hourglassSpace = 2; + + + protected int stateOfError = 0; // Not yet checked + + public AvatarSMDSetTimer(int _x, int _y, int _minX, int _maxX, int _minY, int _maxY, boolean _pos, TGComponent _father, TDiagramPanel _tdp) { + super(_x, _y, _minX, _maxX, _minY, _maxY, _pos, _father, _tdp); + + width = 30; + height = 20; + minWidth = 30; + + nbConnectingPoint = 2; + connectingPoint = new TGConnectingPoint[2]; + connectingPoint[0] = new AvatarSMDConnectingPoint(this, 0, -lineLength, true, false, 0.5, 0.0); + connectingPoint[1] = new AvatarSMDConnectingPoint(this, 0, lineLength, false, true, 0.5, 1.0); + + addTGConnectingPointsComment(); + + moveable = true; + editable = true; + removable = true; + + name = "Set timer"; + value = "set(timer1, 10)"; + //makeValue(); + + myImageIcon = IconManager.imgic904; + } + + public void internalDrawing(Graphics g) { + + int w = g.getFontMetrics().stringWidth(value); + int w1 = Math.max(minWidth, w + 2 * textX); + if ((w1 != width) & (!tdp.isScaled())) { + setCd(x + width/2 - w1/2, y); + width = w1; //updateConnectingPoints(); + } + + + if (stateOfError > 0) { + Color c = g.getColor(); + switch(stateOfError) { + case ErrorHighlight.OK: + g.setColor(ColorManager.AVATAR_SET_TIMER); + break; + default: + g.setColor(ColorManager.UNKNOWN_BOX_ACTION); + } + // Making the polygon + int [] px1 = {x, x+width-linebreak, x+width, x+width-linebreak, x}; + int [] py1 = {y, y, y+(height/2), y+height, y+height}; + g.fillPolygon(px1, py1, 5); + g.setColor(c); + } + + //g.drawRoundRect(x, y, width, height, arc, arc); + Color c = g.getColor(); + //System.out.println("Color=" + c); + + g.drawLine(x+(width/2), y, x+(width/2), y - lineLength); + g.drawLine(x+(width/2), y+height, x+(width/2), y + lineLength + height); + + int x1 = x + 1; + int y1 = y + 1; + int height1 = height; + int width1 = width; + g.setColor(ColorManager.AVATAR_SET_TIMER); + g.drawLine(x1, y1, x1+width1-linebreak, y1); + g.drawLine(x1, y1+height1, x1+width1-linebreak, y1+height1); + g.drawLine(x1, y1, x1, y1+height1); + g.drawLine(x1+width1-linebreak, y1, x1+width1, y1+height1/2); + g.drawLine(x1+width1-linebreak, y1+height1, x1+width1, y1+height1/2); + g.setColor(c); + + g.drawLine(x, y, x+width-linebreak, y); + g.drawLine(x, y+height, x+width-linebreak, y+height); + g.drawLine(x, y, x, y+height); + g.drawLine(x+width-linebreak, y, x+width, y+height/2); + g.drawLine(x+width-linebreak, y+height, x+width, y+height/2); + + // hourglass + g.drawLine(x+width+hourglassSpace, y, x+width+hourglassSpace + hourglassWidth, y); + g.drawLine(x+width+hourglassSpace, y+height, x+width+hourglassSpace + hourglassWidth, y+height); + g.drawLine(x+width+hourglassSpace, y, x+width+hourglassSpace + hourglassWidth, y+height); + g.drawLine(x+width+hourglassSpace, y+height, x+width+hourglassSpace + hourglassWidth, y); + + //g.drawString("sig()", x+(width-w) / 2, y); + g.drawString(value, x + (width - w) / 2 , y + textY); + + + } + + public TGComponent isOnMe(int _x, int _y) { + if (GraphicLib.isInRectangle(_x, _y, x, y, width + hourglassSpace + hourglassWidth, height)) { + return this; + } + + if ((int)(Line2D.ptSegDistSq(x+(width/2), y-lineLength, x+(width/2), y + lineLength + height, _x, _y)) < distanceSelected) { + return this; + } + + return null; + } + + public void makeValue() { + } + + public String getTimerName() { + return AvatarSignal.getValue(value, 0); + } + + public String getTimerValue() { + return AvatarSignal.getValue(value, 1); + } + + public boolean editOndoubleClick(JFrame frame) { + Vector timers = tdp.getMGUI().getAllTimers(); + TraceManager.addDev("Nb of timers:" + timers.size()); + + JDialogAvatarTimer jdat = new JDialogAvatarTimer(frame, "Setting timer set", getTimerName(), getTimerValue(), timers, true); + jdat.setSize(350, 300); + GraphicLib.centerOnParent(jdat); + jdat.show(); // blocked until dialog has been closed + + if (jdat.hasBeenCancelled()) { + return false; + } + + String val0 = jdat.getTimer(); + String val1 = jdat.getValue(); + + // valid signal? + if (!AvatarSignal.isAValidUseSignal(val0)) { + JOptionPane.showMessageDialog(frame, + "Could not change the setting of the timer: invalid name for the timer", + "Error", + JOptionPane.INFORMATION_MESSAGE); + return false; + } + + if (val1.length() == 0) { + JOptionPane.showMessageDialog(frame, + "Could not change the setting of the timer: invalid value for the timer", + "Error", + JOptionPane.INFORMATION_MESSAGE); + return false; + } + + value = "setTimer(" + val0 + "," + val1 + ")"; + + return true; + + } + + + + + public int getType() { + return TGComponentManager.AVATARSMD_SET_TIMER; + } + + public int getDefaultConnector() { + return TGComponentManager.AVATARSMD_CONNECTOR; + } + + public void setStateAction(int _stateAction) { + stateOfError = _stateAction; + } +} diff --git a/src/ui/avatarsmd/AvatarSMDToolBar.java b/src/ui/avatarsmd/AvatarSMDToolBar.java index 6ba6d840b5..91157082f0 100755 --- a/src/ui/avatarsmd/AvatarSMDToolBar.java +++ b/src/ui/avatarsmd/AvatarSMDToolBar.java @@ -74,6 +74,10 @@ public class AvatarSMDToolBar extends TToolBar { mgui.actions[TGUIAction.ASMD_CHOICE].setEnabled(b); mgui.actions[TGUIAction.ASMD_RANDOM].setEnabled(b); + mgui.actions[TGUIAction.ASMD_SET_TIMER].setEnabled(b); + mgui.actions[TGUIAction.ASMD_RESET_TIMER].setEnabled(b); + mgui.actions[TGUIAction.ASMD_EXPIRE_TIMER].setEnabled(b); + mgui.actions[TGUIAction.ACT_ENHANCE].setEnabled(b); mgui.actions[TGUIAction.ACT_ZOOM_MORE].setEnabled(false); @@ -141,6 +145,17 @@ public class AvatarSMDToolBar extends TToolBar { this.addSeparator(); + + button = this.add(mgui.actions[TGUIAction.ASMD_SET_TIMER]); + button.addMouseListener(mgui.mouseHandler); + + button = this.add(mgui.actions[TGUIAction.ASMD_RESET_TIMER]); + button.addMouseListener(mgui.mouseHandler); + + button = this.add(mgui.actions[TGUIAction.ASMD_EXPIRE_TIMER]); + button.addMouseListener(mgui.mouseHandler); + + this.addSeparator(); button = this.add(mgui.actions[TGUIAction.ACT_ENHANCE]); button.addMouseListener(mgui.mouseHandler); diff --git a/src/ui/window/JDialogAvatarTimer.java b/src/ui/window/JDialogAvatarTimer.java new file mode 100755 index 0000000000..18d05020cc --- /dev/null +++ b/src/ui/window/JDialogAvatarTimer.java @@ -0,0 +1,230 @@ +/**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 JDialogAvatarTimer + * Dialog for managing timer set, reset and expire + * Creation: 15/07/2010 + * @version 1.0 15/07/2010 + * @author Ludovic APVRILLE + * @see + */ + +package ui.window; + +import java.awt.*; +import java.awt.event.*; +import javax.swing.*; +import java.util.*; + +import ui.*; + +public class JDialogAvatarTimer extends javax.swing.JDialog implements ActionListener { + + private Vector timers; + + private boolean cancelled = false; + private JPanel panel1, panel2; + + // Panel1 + private JComboBox listTimers; + private JButton selectTimer; + private JTextField ttimer; + + // Panel2 + private JTextField tvalue; + + // Main Panel + private JButton closeButton; + private JButton cancelButton; + + private String timer, value; + private boolean setValue; + + + /** Creates new form */ + public JDialogAvatarTimer(Frame _f, String _title, String _timer, String _value, Vector _timers, boolean _setValue) { + + super(_f, _title, true); + + timers = _timers; + timer = _timer; + value = _value; + setValue = _setValue; + + initComponents(); + myInitComponents(); + pack(); + } + + + private void myInitComponents() { + } + + private void initComponents() { + Container c = getContentPane(); + GridBagLayout gridbag0 = new GridBagLayout(); + GridBagLayout gridbag1 = new GridBagLayout(); + GridBagLayout gridbag2 = new GridBagLayout(); + GridBagConstraints c0 = new GridBagConstraints(); + GridBagConstraints c1 = new GridBagConstraints(); + GridBagConstraints c2 = new GridBagConstraints(); + + setFont(new Font("Helvetica", Font.PLAIN, 14)); + c.setLayout(gridbag0); + + setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE); + + panel1 = new JPanel(); + panel1.setLayout(gridbag1); + + panel1.setBorder(new javax.swing.border.TitledBorder("Timer")); + + panel1.setPreferredSize(new Dimension(300, 150)); + + // first line panel1 + c1.weighty = 1.0; + c1.weightx = 1.0; + c1.gridwidth = GridBagConstraints.REMAINDER; //end row + c1.fill = GridBagConstraints.BOTH; + c1.gridheight = 1; + panel1.add(new JLabel(" "), c1); + + // Combo box + c1.gridwidth = 1; + c1.gridheight = 1; + c1.weighty = 1.0; + c1.weightx = 1.0; + c1.fill = GridBagConstraints.HORIZONTAL; + c1.anchor = GridBagConstraints.CENTER; + c1.gridwidth = GridBagConstraints.REMAINDER; //end row + listTimers = new JComboBox(timers); + panel1.add(listTimers, c1); + + + // Selection of the timer + c1.gridwidth = GridBagConstraints.REMAINDER; //end row + selectTimer = new JButton("Select timer"); + panel1.add(selectTimer, c1); + selectTimer.setEnabled(timers.size() > 0); + selectTimer.addActionListener(this); + + // Text + c1.gridwidth = GridBagConstraints.REMAINDER; //end row + ttimer = new JTextField(timer, 30); + panel1.add(ttimer, c1); + //panel1.setEditable(true); + + // Panel2 + panel2 = new JPanel(); + panel2.setLayout(gridbag2); + panel2.setBorder(new javax.swing.border.TitledBorder("Timer value")); + panel2.setPreferredSize(new Dimension(300, 75)); + c1.weighty = 1.0; + c1.weightx = 1.0; + c1.gridwidth = GridBagConstraints.REMAINDER; //end row + c1.fill = GridBagConstraints.BOTH; + c1.gridheight = 1; + panel2.add(new JLabel(" "), c1); + c1.gridwidth = GridBagConstraints.REMAINDER; //end row + tvalue = new JTextField(value, 30); + panel2.add(tvalue, c1); + + // main panel; + c0.gridwidth = 1; + c0.gridheight = 10; + c0.weighty = 1.0; + c0.weightx = 1.0; + c0.gridwidth = GridBagConstraints.REMAINDER; //end row + + c.add(panel1, c0); + if (setValue) { + c.add(panel2, c0); + } + + c0.gridwidth = 1; + c0.gridheight = 1; + c0.fill = GridBagConstraints.HORIZONTAL; + closeButton = new JButton("Save and Close", IconManager.imgic25); + //closeButton.setPreferredSize(new Dimension(600, 50)); + closeButton.addActionListener(this); + c.add(closeButton, c0); + c0.gridwidth = GridBagConstraints.REMAINDER; //end row + cancelButton = new JButton("Cancel", IconManager.imgic27); + cancelButton.addActionListener(this); + c.add(cancelButton, c0); + } + + public void actionPerformed(ActionEvent evt) { + //String command = evt.getActionCommand(); + + // Compare the action command to the known actions. + if (evt.getSource() == closeButton) { + closeDialog(); + } else if (evt.getSource() == cancelButton) { + cancelDialog(); + } else if (evt.getSource() == selectTimer) { + selectTimer(); + } + } + + public void selectTimer() { + int index = listTimers.getSelectedIndex(); + ttimer.setText(timers.get(index).toString()); + } + + public void closeDialog() { + dispose(); + } + + public String getTimer() { + return ttimer.getText(); + } + + public String getValue() { + return tvalue.getText(); + } + + public boolean hasBeenCancelled() { + return cancelled; + } + + public void cancelDialog() { + cancelled = true; + dispose(); + } +} diff --git a/src/uppaaldesc/UPPAALTemplate.java b/src/uppaaldesc/UPPAALTemplate.java index 12f73fec24..a8482d3d54 100755 --- a/src/uppaaldesc/UPPAALTemplate.java +++ b/src/uppaaldesc/UPPAALTemplate.java @@ -173,6 +173,11 @@ public class UPPAALTemplate { int dec = initLocation.idPoint.y - initLocation.namePoint.y; initLocation.idPoint.y = y / 2; initLocation.namePoint.y = initLocation.idPoint.y - dec; + + ListIterator iterator = transitions.listIterator(); + while(iterator.hasNext()) { + ((UPPAALTransition)(iterator.next())).enhanceGraphics(); + } } public int getMaxYLocations() { diff --git a/src/uppaaldesc/UPPAALTransition.java b/src/uppaaldesc/UPPAALTransition.java index c8fa4eb07e..e938eb9490 100755 --- a/src/uppaaldesc/UPPAALTransition.java +++ b/src/uppaaldesc/UPPAALTransition.java @@ -97,6 +97,18 @@ public class UPPAALTransition { } + public void enhanceGraphics() { + if ((points.size() == 0) && (destinationLoc == sourceLoc)) { + points.add(new Point(sourceLoc.idPoint.x - 50, sourceLoc.idPoint.y - 50)); + } + + + if ((points.size() == 1) && (destinationLoc == sourceLoc)) { + Point p = (Point)(points.get(0)); + points.add(new Point(p.x+10, p.y+35)); + } + } + public boolean isAnEmptyTransition() { if (guard == null) { -- GitLab