diff --git a/executablecode/Makefile.src b/executablecode/Makefile.src index 2b4059ec6690a462f82dbd5da91db2df9eb3b73d..e1d14955ee1c124d2e82ef39cdd7423836d38125 100755 --- a/executablecode/Makefile.src +++ b/executablecode/Makefile.src @@ -1 +1 @@ -SRCS = generated_src/main.c generated_src/B.c generated_src/A.c \ No newline at end of file +SRCS = generated_src/main.c generated_src/MainBlock.c generated_src/attack03.c generated_src/final.c generated_src/attack02.c generated_src/attack01.c generated_src/BEFORE__1.c generated_src/AFTER__2.c \ No newline at end of file diff --git a/src/attacktrees/Attack.java b/src/attacktrees/Attack.java index 668d7545862f4e22d3e0ff41dd9c41f75643704b..586df1a70209c9693181befc6ec91b60a3ee1742 100755 --- a/src/attacktrees/Attack.java +++ b/src/attacktrees/Attack.java @@ -84,5 +84,13 @@ public class Attack { public boolean isLeaf() { return (originNode == null); } + + public boolean isFinal() { + if (destinationNodes.size() == 0) { + return true; + } + + return false; + } } diff --git a/src/attacktrees/AttackNode.java b/src/attacktrees/AttackNode.java index 75fcd921c0cdb9190496abcb921b3fef39cba10f..f66a93ea5918482693cc36cb34c7a244a0334bdc 100755 --- a/src/attacktrees/AttackNode.java +++ b/src/attacktrees/AttackNode.java @@ -110,5 +110,26 @@ public abstract class AttackNode { return ret; } + + // Order attacks according to the Integer value + public void orderAttacks() { + ArrayList<Attack> newAttacks = new ArrayList<Attack>(); + ArrayList<Integer> newInputValues = new ArrayList<Integer>(); + + for(Integer i: inputValues) { + newInputValues.add(i); + } + + // sort newInputValues + Collections.sort(newInputValues); + + for(Integer i: newInputValues) { + int index = inputValues.indexOf(i); + newAttacks.add(inputAttacks.get(index)); + } + + inputAttacks = newAttacks; + inputValues = newInputValues; + } } diff --git a/src/attacktrees/TimeNode.java b/src/attacktrees/TimeNode.java index c90ab30ff74104d5b770dda8926dc2dd761bb7ce..4095ab4920d731369ef948acca81c14fbec528c5 100755 --- a/src/attacktrees/TimeNode.java +++ b/src/attacktrees/TimeNode.java @@ -55,5 +55,9 @@ public abstract class TimeNode extends AttackNode{ super(_name, _objectReference); time = _time; } + + public int getTime() { + return time; + } } diff --git a/src/attacktrees/XORNode.java b/src/attacktrees/XORNode.java new file mode 100755 index 0000000000000000000000000000000000000000..9d5ea37529c2c93556b64c4b5914598d986c6f8b --- /dev/null +++ b/src/attacktrees/XORNode.java @@ -0,0 +1,59 @@ +/**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 ORNode + * Creation: 13/04/2015 + * @version 1.0 13/04/2015 + * @author Ludovic APVRILLE + * @see + */ + +package attacktrees; + +import java.util.*; + + +public class XORNode extends BooleanNode { + + public XORNode(String _name, Object _referenceObject) { + super(_name, _referenceObject); + type = "XOR"; + } + + +} diff --git a/src/avatartranslator/AvatarAttribute.java b/src/avatartranslator/AvatarAttribute.java index 4949d659ba2ac0819e6603cac3474a2b400b5b20..87b22968d50736d2d9589bf0c06645c96336f20e 100644 --- a/src/avatartranslator/AvatarAttribute.java +++ b/src/avatartranslator/AvatarAttribute.java @@ -1,48 +1,48 @@ /**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 AvatarAttribute - * Avatar attributes, either of blocks, or manipulated by signals / methods - * 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 AvatarAttribute + * Avatar attributes, either of blocks, or manipulated by signals / methods + * Creation: 20/05/2010 + * @version 1.0 20/05/2010 + * @author Ludovic APVRILLE + * @see + */ package avatartranslator; @@ -54,102 +54,102 @@ import translator.*; import translator.tojava.*; public class AvatarAttribute extends AvatarElement{ - + // Types of parameters private int type; - private String initialValue; - - - public AvatarAttribute(String _name, int _type, Object _referenceObject) { - super(_name, _referenceObject); - /*if (_type == -1) { - TraceManager.addDev("- - - - - - - - - - - - " + _name + ": " + _type); - try { - int x = 1 / 0; - } catch (Exception e) { - e.printStackTrace(); - System.exit(0); - } - }*/ - type = _type; - } - - public void setInitialValue(String _initialValue) { - initialValue = _initialValue; - } - - public boolean hasInitialValue() { - if (getInitialValue() == null) { - return false; - } - return (!(getInitialValue().trim().length() == 0)); - } - - public String getInitialValue() { - if ((initialValue == null) || (initialValue.length() == 0)) { - return getDefaultInitialValue(); - } - return initialValue; - } - - public String getDefaultInitialValue() { - return AvatarType.getDefaultInitialValue(type); - } - - public String getDefaultInitialValueTF() { - return AvatarType.getDefaultInitialValueTF(type); - } - - public int getType() { - return type; - } - - public boolean isInt() { - return (type == AvatarType.INTEGER); - } - - public boolean isBool() { - return (type == AvatarType.BOOLEAN); - } - - public static boolean isAValidAttributeName(String id) { - if ((id == null) || (id.length() < 1)) { + private String initialValue; + + + public AvatarAttribute(String _name, int _type, Object _referenceObject) { + super(_name, _referenceObject); + /*if (_type == -1) { + TraceManager.addDev("- - - - - - - - - - - - " + _name + ": " + _type); + try { + int x = 1 / 0; + } catch (Exception e) { + e.printStackTrace(); + System.exit(0); + } + }*/ + type = _type; + } + + public void setInitialValue(String _initialValue) { + initialValue = _initialValue; + } + + public boolean hasInitialValue() { + if (getInitialValue() == null) { return false; } - + return (!(getInitialValue().trim().length() == 0)); + } + + public String getInitialValue() { + if ((initialValue == null) || (initialValue.length() == 0)) { + return getDefaultInitialValue(); + } + return initialValue; + } + + public String getDefaultInitialValue() { + return AvatarType.getDefaultInitialValue(type); + } + + public String getDefaultInitialValueTF() { + return AvatarType.getDefaultInitialValueTF(type); + } + + public int getType() { + return type; + } + + public boolean isInt() { + return (type == AvatarType.INTEGER); + } + + public boolean isBool() { + return (type == AvatarType.BOOLEAN); + } + + public static boolean isAValidAttributeName(String id) { + if ((id == null) || (id.length() < 1)) { + return false; + } + String lowerid = id.toLowerCase(); boolean b1, b2, b3, b4, b5; b1 = (id.substring(0,1)).matches("[a-zA-Z]"); b2 = id.matches("\\w*"); b3 = !RTLOTOSKeyword.isAKeyword(lowerid); b5 = !JKeyword.isAKeyword(lowerid); - - - if ((lowerid.equals(AvatarType.getStringType(0).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(1).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(2).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(3).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(4).toLowerCase()))) { - b4 = false; - } else { - b4 = true; - } - - + + + if ((lowerid.equals(AvatarType.getStringType(0).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(1).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(2).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(3).toLowerCase())) || (lowerid.equals(AvatarType.getStringType(4).toLowerCase()))) { + b4 = false; + } else { + b4 = true; + } + + return (b1 && b2 && b3 && b4 && b5); - } - - public String toString() { - String ret = AvatarType.getStringType(type) + " " + getName(); - if (initialValue == null) { - return ret; - } - - return ret + " = " + initialValue; - } - - public String toStringType() { - String ret = AvatarType.getStringType(type) + " " + getName() + " typeid= " + getType(); - if (initialValue == null) { - return ret; - } - - return ret + " = " + initialValue; - } -} \ No newline at end of file + } + + public String toString() { + String ret = AvatarType.getStringType(type) + " " + getName(); + if (initialValue == null) { + return ret; + } + + return ret + " = " + initialValue; + } + + public String toStringType() { + String ret = AvatarType.getStringType(type) + " " + getName() + " typeid= " + getType(); + if (initialValue == null) { + return ret; + } + + return ret + " = " + initialValue; + } +} diff --git a/src/avatartranslator/AvatarType.java b/src/avatartranslator/AvatarType.java index 99595f7a6e417299f2a00c355ff2404d882c9ae9..62bd9626b58d1921f48577ba5d9ed90eee01e52c 100644 --- a/src/avatartranslator/AvatarType.java +++ b/src/avatartranslator/AvatarType.java @@ -1,48 +1,48 @@ /**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 AvatarType - * Avatar type - * 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 AvatarType + * Avatar type + * Creation: 20/05/2010 + * @version 1.0 20/05/2010 + * @author Ludovic APVRILLE + * @see + */ package avatartranslator; @@ -52,62 +52,62 @@ import java.util.*; import myutil.*; public class AvatarType { - + // Types of parameters //public final static int NATURAL = 0; public final static int BOOLEAN = 1; - public final static int INTEGER = 2; - public final static int TIMER = 3; - - + public final static int INTEGER = 2; + public final static int TIMER = 3; + + public static int getType(String s) { if (s.equals("bool")) { - return BOOLEAN; + return BOOLEAN; } else if (s.equals("Boolean")) { - return BOOLEAN; + return BOOLEAN; } else if (s.equals("int")) { - return INTEGER; + return INTEGER; } else if (s.equals("Integer")) { - return INTEGER; - } else if (s.equals("Timer")) { - return TIMER; + return INTEGER; + } else if (s.equals("Timer")) { + return TIMER; } return -1; } - + public static String getStringType(int _type) { switch(_type) { - case BOOLEAN: - return "bool"; - case INTEGER: - return "int"; - case TIMER: - return "timer"; + case BOOLEAN: + return "bool"; + case INTEGER: + return "int"; + case TIMER: + return "timer"; } - return ""; + return ""; } - - public static String getDefaultInitialValue(int _type) { - switch(_type) { - case BOOLEAN: - return "false"; - case INTEGER: - return "0"; - case TIMER: - return "0"; + + public static String getDefaultInitialValue(int _type) { + switch(_type) { + case BOOLEAN: + return "false"; + case INTEGER: + return "0"; + case TIMER: + return "0"; } - return ""; - } - - public static String getDefaultInitialValueTF(int _type) { - switch(_type) { - case BOOLEAN: - return "f"; - case INTEGER: - return "0"; - case TIMER: - return "0"; + return ""; + } + + public static String getDefaultInitialValueTF(int _type) { + switch(_type) { + case BOOLEAN: + return "f"; + case INTEGER: + return "0"; + case TIMER: + return "0"; } - return ""; - } -} \ No newline at end of file + return ""; + } +} diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java index e884f577b44c09c6597abb247545afe1990a4306..80ab662c6d9a61ae4662ad6c445ea02054c32fb4 100755 --- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java +++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java @@ -950,9 +950,12 @@ public class AVATAR2ProVerif { AvatarStateMachine asm = ab.getStateMachine(); AvatarStartState ass = asm.getStartState(); - macs.clear(); - makeBlockProcesses(ab, asm, ass.getNext(0), p, tmpprocesses, states, null); + macs.clear(); + + if (ass != null) { + makeBlockProcesses(ab, asm, ass.getNext(0), p, tmpprocesses, states, null); + } } public void makeBlockProcesses(AvatarBlock _block, AvatarStateMachine _asm, AvatarStateMachineElement _asme, ProVerifProcess _p, LinkedList<ProVerifProcess> _processes, LinkedList<AvatarState> _states, String _choiceInfo) { diff --git a/src/avatartranslator/totpn/AVATAR2TPN.java b/src/avatartranslator/totpn/AVATAR2TPN.java index b48dfa3335ce4ad0c567cac034767afe3f856283..7b7ab429d6bf54c2afde88b849ea90ae4c0fd35e 100755 --- a/src/avatartranslator/totpn/AVATAR2TPN.java +++ b/src/avatartranslator/totpn/AVATAR2TPN.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 AVATAR2TPN -* Creation: 08/02/2012 -* @version 1.1 08/02/2012 -* @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 AVATAR2TPN + * Creation: 08/02/2012 + * @version 1.1 08/02/2012 + * @author Ludovic APVRILLE + * @see + */ package avatartranslator.totpn; @@ -53,269 +53,270 @@ import myutil.*; import avatartranslator.*; public class AVATAR2TPN { - - private static int GENERAL_ID = 0; - - - - private TPN tpn; - private AvatarSpecification avspec; - - private Hashtable<AvatarStateMachineElement, Place> entryPlaces; - private Hashtable<AvatarStateMachineElement, Place> exitPlaces; - private LinkedList<AvatarActionOnSignal> sendActions; - private LinkedList<AvatarActionOnSignal> receiveActions; - - - private Vector warnings; - - - - public AVATAR2TPN(AvatarSpecification _avspec) { - avspec = _avspec; - } - - - - public Vector getWarnings() { - return warnings; - } - - - - public TPN generateTPN(boolean _debug, boolean _optimize) { - GENERAL_ID = 0; - - entryPlaces = new Hashtable<AvatarStateMachineElement, Place>(); - exitPlaces = new Hashtable<AvatarStateMachineElement, Place>(); - - sendActions = new LinkedList<AvatarActionOnSignal>(); - receiveActions = new LinkedList<AvatarActionOnSignal>(); - - warnings = new Vector(); - tpn = new TPN(); - - avspec.removeCompositeStates(); - avspec.removeTimers(); - - makeBlocks(); - - //TraceManager.addDev("-> tpn:" + tpn.toString()); - - - /*if (_optimize) { - spec.optimize(); - }*/ - - - return tpn; - } - - public void makeBlocks() { - LinkedList<AvatarBlock> blocks = avspec.getListOfBlocks(); - for(AvatarBlock block: blocks) { - makeBlock(block); - } - interconnectSynchro(); - } - - public void makeBlock(AvatarBlock ab) { - AvatarStateMachine asm = ab.getStateMachine(); - AvatarStartState ass = asm.getStartState(); - - makeBlockTPN(ab, asm, ass,null); - - - } - - public void makeBlockTPN(AvatarBlock _block, AvatarStateMachine _asm, AvatarStateMachineElement _asme, AvatarStateMachineElement _previous) { - - Place p0, p1, pentry=null, pexit=null; - Transition t0; - AvatarActionOnSignal aaos; - - p0 = entryPlaces.get(_asme); - if (_previous== null) { - p1 = null; - } else { - p1 = exitPlaces.get(_previous); - } - - boolean link=false; - - // Element already taken into account? - if (p0 != null) { - // Link the exit place of the previous element to the one of the current element - if (p1 != null){ - t0 = new Transition(getTPNName(_block, _previous) + "_to_" + getTPNName(_block, _asme)); - t0.addDestinationPlace(p0); - t0.addOriginPlace(p1); - tpn.addTransition(t0); - } - return; - } - - // New element! - - //Start state - if ((_asme instanceof AvatarStartState)|| (_asme instanceof AvatarStopState) || (_asme instanceof AvatarState)) { - pentry = new Place(getTPNName(_block, _asme)); - if (_asme instanceof AvatarStartState) { - pentry.nbOfTokens = 1; - } - pexit = pentry; - entryPlaces.put(_asme, pentry); - exitPlaces.put(_asme, pexit); - //TraceManager.addDev("Adding place : " + pentry); - tpn.addPlace(pentry); - link = true; - - } else if ((_asme instanceof AvatarTransition) || (_asme instanceof AvatarRandom)) { - if (p1 != null){ - entryPlaces.put(_asme, p1); - exitPlaces.put(_asme, p1); - } else { - TraceManager.addDev("Previous element without pexit!!"); - } - - } else if (_asme instanceof AvatarActionOnSignal){ - TraceManager.addDev("??????? Analyzing actions on signals: " + _asme); - aaos = (AvatarActionOnSignal)_asme; - - if (aaos.getSignal().isOut()) { - sendActions.add(aaos); - } else { - receiveActions.add(aaos); - } - - if (p1 == null) { - TraceManager.addDev("********* NULL P1"); - } - - pentry = p1; - pexit = new Place(getTPNName(_block, _asme)); - entryPlaces.put(_asme, pentry); - exitPlaces.put(_asme, pexit); - - tpn.addPlace(pexit); - //TraceManager.addDev("Adding place : " + pentry); - - } else { - TraceManager.addDev("UNMANAGED ELEMENTS: " +_asme); - } - - - // Must link the new element to the previous one - if ((p1 != null) && (link)){ - t0 = new Transition(getTPNName(_block, _previous) + "_to_" + getTPNName(_block, _asme)); - t0.addDestinationPlace(pentry); - t0.addOriginPlace(p1); - tpn.addTransition(t0); - } - - // Work with next elements - for(int i=0; i<_asme.nbOfNexts(); i++) { - makeBlockTPN(_block, _asm, _asme.getNext(i), _asme); - } - - - - } - - public void interconnectSynchro() { - int index; - AvatarSignal sig; - Transition t0, t1; - Place pSynchro; - - //TraceManager.addDev("Interconnecting synchro"); - - // Interconnect sender and receivers together! - for(AvatarActionOnSignal destination: receiveActions) { - TraceManager.addDev("Dealing with receive actions : " + destination); - // Find the related relation - for(AvatarRelation ar: avspec.getRelations()) { - if (ar.containsSignal(destination.getSignal()) && !ar.isAsynchronous()) { - index = ar.getIndexOfSignal(destination.getSignal()); - sig = ar.getOutSignal(index); - for(AvatarActionOnSignal origin:sendActions) { - if (origin.getSignal() == sig) { - // combination found! - TraceManager.addDev("Combination found for: " + sig); - t0 = new Transition("beginning_Synchro_from_" + getTPNName(ar.getOutBlock(index), origin) + "_to_" + getTPNName(ar.getInBlock(index), destination)); - pSynchro = new Place("Synchro_from_" + getTPNName(ar.getOutBlock(index), origin) + "_to_" + getTPNName(ar.getInBlock(index), destination)); - tpn.addPlace(pSynchro); - t1 = new Transition("end_Synchro_from_" + getTPNName(ar.getOutBlock(index), origin) + "_to_" + getTPNName(ar.getInBlock(index), destination)); - - t0.addOriginPlace(entryPlaces.get(destination)); - t0.addOriginPlace(entryPlaces.get(origin)); - t0.addDestinationPlace(pSynchro); - - t1.addOriginPlace(pSynchro); - t1.addDestinationPlace(exitPlaces.get(origin)); - t1.addDestinationPlace(exitPlaces.get(destination)); - - tpn.addTransition(t0); - tpn.addTransition(t1); - - } - } - } - } - } - - } - /* Old version - public void interconnectSynchro() { - int index; - AvatarSignal sig; - Transition t0; - - //TraceManager.addDev("Interconnecting synchro"); - - // Interconnect sender and receivers together! - for(AvatarActionOnSignal destination: receiveActions) { - // Find the related relation - for(AvatarRelation ar: avspec.getRelations()) { - if (ar.containsSignal(destination.getSignal()) && !ar.isAsynchronous()) { - index = ar.getIndexOfSignal(destination.getSignal()); - sig = ar.getOutSignal(index); - for(AvatarActionOnSignal origin:sendActions) { - if (origin.getSignal() == sig) { - // combination found! - //TraceManager.addDev("Combination found"); - t0 = new Transition("Synchro from " + getShortTPNName(origin) + " to " + getShortTPNName(destination)); - t0.addOriginPlace(entryPlaces.get(origin)); - t0.addDestinationPlace(exitPlaces.get(origin)); - t0.addOriginPlace(entryPlaces.get(destination)); - t0.addDestinationPlace(exitPlaces.get(destination)); - tpn.addTransition(t0); - } - } - } - } - } - - }*/ - - public String getTPNName(AvatarBlock _block, AvatarStateMachineElement _asme) { - if (_asme instanceof AvatarActionOnSignal) { - AvatarActionOnSignal aaos = (AvatarActionOnSignal)_asme; - if (aaos.isSending()) { - return _block.getName() + "__Send__" + aaos.getSignal().getName() + "__" + _asme.getID(); - } else { - return _block.getName() + "__Receive__" + aaos.getSignal().getName() + "__" + _asme.getID(); - } - - } - - return _block.getName() + "__" + _asme.getName() + "__" + _asme.getID(); - } - - public String getShortTPNName(AvatarStateMachineElement _asme) { - return _asme.getName() + "__" + _asme.getID(); + + private static int GENERAL_ID = 0; + + + + private TPN tpn; + private AvatarSpecification avspec; + + private Hashtable<AvatarStateMachineElement, Place> entryPlaces; + private Hashtable<AvatarStateMachineElement, Place> exitPlaces; + private LinkedList<AvatarActionOnSignal> sendActions; + private LinkedList<AvatarActionOnSignal> receiveActions; + + + private Vector warnings; + + + + public AVATAR2TPN(AvatarSpecification _avspec) { + avspec = _avspec; + } + + + + public Vector getWarnings() { + return warnings; + } + + + + public TPN generateTPN(boolean _debug, boolean _optimize) { + GENERAL_ID = 0; + + entryPlaces = new Hashtable<AvatarStateMachineElement, Place>(); + exitPlaces = new Hashtable<AvatarStateMachineElement, Place>(); + + sendActions = new LinkedList<AvatarActionOnSignal>(); + receiveActions = new LinkedList<AvatarActionOnSignal>(); + + warnings = new Vector(); + tpn = new TPN(); + + avspec.removeCompositeStates(); + avspec.removeTimers(); + + makeBlocks(); + + //TraceManager.addDev("-> tpn:" + tpn.toString()); + + + /*if (_optimize) { + spec.optimize(); + }*/ + + + return tpn; + } + + public void makeBlocks() { + LinkedList<AvatarBlock> blocks = avspec.getListOfBlocks(); + for(AvatarBlock block: blocks) { + makeBlock(block); + } + interconnectSynchro(); + } + + public void makeBlock(AvatarBlock ab) { + AvatarStateMachine asm = ab.getStateMachine(); + AvatarStartState ass = asm.getStartState(); + if (ass != null) { + makeBlockTPN(ab, asm, ass,null); } - - - -} \ No newline at end of file + + + } + + public void makeBlockTPN(AvatarBlock _block, AvatarStateMachine _asm, AvatarStateMachineElement _asme, AvatarStateMachineElement _previous) { + + Place p0, p1, pentry=null, pexit=null; + Transition t0; + AvatarActionOnSignal aaos; + + p0 = entryPlaces.get(_asme); + if (_previous== null) { + p1 = null; + } else { + p1 = exitPlaces.get(_previous); + } + + boolean link=false; + + // Element already taken into account? + if (p0 != null) { + // Link the exit place of the previous element to the one of the current element + if (p1 != null){ + t0 = new Transition(getTPNName(_block, _previous) + "_to_" + getTPNName(_block, _asme)); + t0.addDestinationPlace(p0); + t0.addOriginPlace(p1); + tpn.addTransition(t0); + } + return; + } + + // New element! + + //Start state + if ((_asme instanceof AvatarStartState)|| (_asme instanceof AvatarStopState) || (_asme instanceof AvatarState)) { + pentry = new Place(getTPNName(_block, _asme)); + if (_asme instanceof AvatarStartState) { + pentry.nbOfTokens = 1; + } + pexit = pentry; + entryPlaces.put(_asme, pentry); + exitPlaces.put(_asme, pexit); + //TraceManager.addDev("Adding place : " + pentry); + tpn.addPlace(pentry); + link = true; + + } else if ((_asme instanceof AvatarTransition) || (_asme instanceof AvatarRandom)) { + if (p1 != null){ + entryPlaces.put(_asme, p1); + exitPlaces.put(_asme, p1); + } else { + TraceManager.addDev("Previous element without pexit!!"); + } + + } else if (_asme instanceof AvatarActionOnSignal){ + TraceManager.addDev("??????? Analyzing actions on signals: " + _asme); + aaos = (AvatarActionOnSignal)_asme; + + if (aaos.getSignal().isOut()) { + sendActions.add(aaos); + } else { + receiveActions.add(aaos); + } + + if (p1 == null) { + TraceManager.addDev("********* NULL P1"); + } + + pentry = p1; + pexit = new Place(getTPNName(_block, _asme)); + entryPlaces.put(_asme, pentry); + exitPlaces.put(_asme, pexit); + + tpn.addPlace(pexit); + //TraceManager.addDev("Adding place : " + pentry); + + } else { + TraceManager.addDev("UNMANAGED ELEMENTS: " +_asme); + } + + + // Must link the new element to the previous one + if ((p1 != null) && (link)){ + t0 = new Transition(getTPNName(_block, _previous) + "_to_" + getTPNName(_block, _asme)); + t0.addDestinationPlace(pentry); + t0.addOriginPlace(p1); + tpn.addTransition(t0); + } + + // Work with next elements + for(int i=0; i<_asme.nbOfNexts(); i++) { + makeBlockTPN(_block, _asm, _asme.getNext(i), _asme); + } + + + + } + + public void interconnectSynchro() { + int index; + AvatarSignal sig; + Transition t0, t1; + Place pSynchro; + + //TraceManager.addDev("Interconnecting synchro"); + + // Interconnect sender and receivers together! + for(AvatarActionOnSignal destination: receiveActions) { + TraceManager.addDev("Dealing with receive actions : " + destination); + // Find the related relation + for(AvatarRelation ar: avspec.getRelations()) { + if (ar.containsSignal(destination.getSignal()) && !ar.isAsynchronous()) { + index = ar.getIndexOfSignal(destination.getSignal()); + sig = ar.getOutSignal(index); + for(AvatarActionOnSignal origin:sendActions) { + if (origin.getSignal() == sig) { + // combination found! + TraceManager.addDev("Combination found for: " + sig); + t0 = new Transition("beginning_Synchro_from_" + getTPNName(ar.getOutBlock(index), origin) + "_to_" + getTPNName(ar.getInBlock(index), destination)); + pSynchro = new Place("Synchro_from_" + getTPNName(ar.getOutBlock(index), origin) + "_to_" + getTPNName(ar.getInBlock(index), destination)); + tpn.addPlace(pSynchro); + t1 = new Transition("end_Synchro_from_" + getTPNName(ar.getOutBlock(index), origin) + "_to_" + getTPNName(ar.getInBlock(index), destination)); + + t0.addOriginPlace(entryPlaces.get(destination)); + t0.addOriginPlace(entryPlaces.get(origin)); + t0.addDestinationPlace(pSynchro); + + t1.addOriginPlace(pSynchro); + t1.addDestinationPlace(exitPlaces.get(origin)); + t1.addDestinationPlace(exitPlaces.get(destination)); + + tpn.addTransition(t0); + tpn.addTransition(t1); + + } + } + } + } + } + + } + /* Old version + public void interconnectSynchro() { + int index; + AvatarSignal sig; + Transition t0; + + //TraceManager.addDev("Interconnecting synchro"); + + // Interconnect sender and receivers together! + for(AvatarActionOnSignal destination: receiveActions) { + // Find the related relation + for(AvatarRelation ar: avspec.getRelations()) { + if (ar.containsSignal(destination.getSignal()) && !ar.isAsynchronous()) { + index = ar.getIndexOfSignal(destination.getSignal()); + sig = ar.getOutSignal(index); + for(AvatarActionOnSignal origin:sendActions) { + if (origin.getSignal() == sig) { + // combination found! + //TraceManager.addDev("Combination found"); + t0 = new Transition("Synchro from " + getShortTPNName(origin) + " to " + getShortTPNName(destination)); + t0.addOriginPlace(entryPlaces.get(origin)); + t0.addDestinationPlace(exitPlaces.get(origin)); + t0.addOriginPlace(entryPlaces.get(destination)); + t0.addDestinationPlace(exitPlaces.get(destination)); + tpn.addTransition(t0); + } + } + } + } + } + + }*/ + + public String getTPNName(AvatarBlock _block, AvatarStateMachineElement _asme) { + if (_asme instanceof AvatarActionOnSignal) { + AvatarActionOnSignal aaos = (AvatarActionOnSignal)_asme; + if (aaos.isSending()) { + return _block.getName() + "__Send__" + aaos.getSignal().getName() + "__" + _asme.getID(); + } else { + return _block.getName() + "__Receive__" + aaos.getSignal().getName() + "__" + _asme.getID(); + } + + } + + return _block.getName() + "__" + _asme.getName() + "__" + _asme.getID(); + } + + public String getShortTPNName(AvatarStateMachineElement _asme) { + return _asme.getName() + "__" + _asme.getID(); + } + + + +} diff --git a/src/ui/AttackTreePanel.java b/src/ui/AttackTreePanel.java index 348f1ceeedf2cbc40b69ba22bbaa768a045bc555..e14ff3435c40414ea2993ab18b950b1e8591514a 100755 --- a/src/ui/AttackTreePanel.java +++ b/src/ui/AttackTreePanel.java @@ -1,48 +1,48 @@ /**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 AttackTreePanel - * Management of attack trees - * Creation: 03/11/2009 - * @version 1.0 03/11/2009 - * @author Ludovic APVRILLE - * @see MainGUI - */ + 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 AttackTreePanel + * Management of attack trees + * Creation: 03/11/2009 + * @version 1.0 03/11/2009 + * @author Ludovic APVRILLE + * @see MainGUI + */ package ui; @@ -55,83 +55,83 @@ import java.util.*; public class AttackTreePanel extends TURTLEPanel { public AttackTreeDiagramPanel atdp; - + public AttackTreePanel(MainGUI _mgui) { super(_mgui); - + tabbedPane = new JTabbedPane(); - UIManager.put("TabbedPane.tabAreaBackground", _mgui.BACK_COLOR); - UIManager.put("TabbedPane.selected", _mgui.BACK_COLOR); - SwingUtilities.updateComponentTreeUI(tabbedPane); - //tabbedPane.setOpaque(true); - + UIManager.put("TabbedPane.tabAreaBackground", _mgui.BACK_COLOR); + UIManager.put("TabbedPane.selected", _mgui.BACK_COLOR); + SwingUtilities.updateComponentTreeUI(tabbedPane); + //tabbedPane.setOpaque(true); + cl = new ChangeListener() { - public void stateChanged(ChangeEvent e){ - mgui.paneRequirementAction(e); - } - }; + public void stateChanged(ChangeEvent e){ + mgui.paneRequirementAction(e); + } + }; tabbedPane.addChangeListener(cl); tabbedPane.addMouseListener(new TURTLEPanelPopupListener(this, mgui)); - + } - + public void init() { mgui.changeMade(null, TDiagramPanel.NEW_COMPONENT); // Requirement Diagram toolbar //addRequirementDiagram("Requirement Diagram"); - + //jsp.setVisible(true); } - + public boolean addAttackTreeDiagram(String s) { AttackTreeDiagramToolbar toolBarAt = new AttackTreeDiagramToolbar(mgui); toolbars.add(toolBarAt); - + toolBarPanel = new JPanel(); - //toolBarPanel.setBackground(Color.red); + //toolBarPanel.setBackground(Color.red); toolBarPanel.setLayout(new BorderLayout()); - //toolBarPanel.setBackground(ColorManager.MainTabbedPaneSelect); - + //toolBarPanel.setBackground(ColorManager.MainTabbedPaneSelect); + //The diagram atdp = new AttackTreeDiagramPanel(mgui, toolBarAt); atdp.setName(s); atdp.tp = this; tdp = atdp; panels.add(atdp); - JScrollDiagramPanel jsp = new JScrollDiagramPanel(atdp); + JScrollDiagramPanel jsp = new JScrollDiagramPanel(atdp); atdp.jsp = jsp; jsp.setWheelScrollingEnabled(true); jsp.getVerticalScrollBar().setUnitIncrement(mgui.INCREMENT); toolBarPanel.add(toolBarAt, BorderLayout.NORTH); toolBarPanel.add(jsp, BorderLayout.CENTER); tabbedPane.addTab(s, IconManager.imgic1074, toolBarPanel, "Opens Attack Tree Diagram"); - tabbedPane.setSelectedIndex(0); + tabbedPane.setSelectedIndex(0); JPanel toolBarPanel = new JPanel(); toolBarPanel.setLayout(new BorderLayout()); - + return true; } - + public String saveHeaderInXml() { return "<Modeling type=\"AttackTree\" nameTab=\"" + mgui.getTabName(this) + "\" >\n"; } - + public String saveTailInXml() { return "</Modeling>\n\n\n"; } - + public String toString() { return mgui.getTitleAt(this) + " (SysML Parametric Diagram)"; } - + public boolean removeEnabled(int index) { if (panels.size() > 1) { return true; } return false; } - + public boolean renameEnabled(int index) { if (panels.size() == 0) { return false; @@ -139,12 +139,28 @@ public class AttackTreePanel extends TURTLEPanel { if ((panels.elementAt(index) instanceof AttackTreeDiagramPanel)){ return true; } - + return false; } - - public boolean isATDEnabled() { + + public boolean isATDEnabled() { return true; } - + + public void resetMetElements() { + //TraceManager.addDev("Reset met elements"); + TGComponent tgc; + + for(int i=0; i<panels.size(); i++) { + ListIterator iterator = ((TDiagramPanel)(panels.get(i))).getComponentList().listIterator(); + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + tgc.setAVATARMet(0); + tgc.setInternalAvatarMet(0); + + } + } + + } + } diff --git a/src/ui/AttackTreePanelTranslator.java b/src/ui/AttackTreePanelTranslator.java index 7b0c2875bc7142498f39ddb701e3fca33b3d103d..b358fd8e67a9101da4d7cbea26b16446705cc820 100644 --- a/src/ui/AttackTreePanelTranslator.java +++ b/src/ui/AttackTreePanelTranslator.java @@ -110,19 +110,19 @@ public class AttackTreePanelTranslator { LinkedList<TGComponent> allComponents = (LinkedList<TGComponent>)(atdp.getAllComponentList()); int nodeID = 0; - TGComponent father; + TGComponent father; //Create attacks, nodes for(TGComponent comp: allComponents) { if (comp instanceof ATDAttack) { ATDAttack atdatt = (ATDAttack)comp; - Attack att; - String value = atdatt.getValue(); - father = atdatt.getFather(); - if ((father != null) && (father instanceof ATDBlock)) { - value = ((ATDBlock)father).getNodeName() + "__" + value; - - } + Attack att; + String value = atdatt.getValue(); + father = atdatt.getFather(); + if ((father != null) && (father instanceof ATDBlock)) { + value = ((ATDBlock)father).getNodeName() + "__" + value; + + } att = new Attack(value, atdatt); att.setRoot(atdatt.isRootAttack()); at.addAttack(att); @@ -144,6 +144,12 @@ public class AttackTreePanelTranslator { at.addNode(andnode); listE.addCor(andnode, comp); + //XOR + } else if (cons.isXOR()) { + XORNode xornode = new XORNode("XOR__" + nodeID, cons); + at.addNode(xornode); + listE.addCor(xornode, comp); + //SEQUENCE } else if (cons.isSequence()) { SequenceNode seqnode = new SequenceNode("SEQUENCE__" + nodeID, cons); @@ -172,9 +178,9 @@ public class AttackTreePanelTranslator { int time; try { time = Integer.decode(eq).intValue(); - BeforeNode befnode = new BeforeNode("AFTER__" + nodeID, cons, time); - at.addNode(befnode); - listE.addCor(befnode, comp); + AfterNode aftnode = new AfterNode("AFTER__" + nodeID, cons, time); + at.addNode(aftnode); + listE.addCor(aftnode, comp); } catch (Exception e) { CheckingError ce = new CheckingError(CheckingError.STRUCTURE_ERROR, "Invalid time in after node"); ce.setTGComponent(comp); @@ -271,7 +277,11 @@ public class AttackTreePanelTranslator { node1.setResultingAttack(att); } - node2.addInputAttack(att, new Integer(0)); + String val = comp.getValue().trim(); + if (val.length() == 0) { + val = "0"; + } + node2.addInputAttack(att, new Integer(val)); } } catch (Exception e) { @@ -295,8 +305,8 @@ public class AttackTreePanelTranslator { AvatarBlock mainBlock = new AvatarBlock("MainBlock", null); as.addBlock(mainBlock); - // Declare all attacks - declareAllAttacks(as, mainBlock); + // Declare all attacks + declareAllAttacks(as, mainBlock); // Make block for attacks makeLeafAttackBlocks(as, mainBlock); @@ -310,24 +320,24 @@ public class AttackTreePanelTranslator { } private void declareAllAttacks(AvatarSpecification _as, AvatarBlock _main) { - AvatarRelation ar = new AvatarRelation("MainRelation", _main, _main, null); - ar.setAsynchronous(false); - ar.setPrivate(true); - ar.setBroadcast(false); - - _as.addRelation(ar); - for(Attack attack: at.getAttacks()) { - avatartranslator.AvatarSignal makeAttack = new avatartranslator.AvatarSignal("make__" + attack.getName(), AvatarSignal.IN, (Object)(listE.getTG(attack))); - _main.addSignal(makeAttack); - avatartranslator.AvatarSignal stopMakeAttack = new avatartranslator.AvatarSignal("makeStop__" + attack.getName(), AvatarSignal.IN, listE.getTG(attack)); - _main.addSignal(stopMakeAttack); - avatartranslator.AvatarSignal acceptAttack = new avatartranslator.AvatarSignal("accept__" + attack.getName(), AvatarSignal.OUT, listE.getTG(attack)); - _main.addSignal(acceptAttack); - avatartranslator.AvatarSignal stopAcceptAttack = new avatartranslator.AvatarSignal("acceptStop__" + attack.getName(), AvatarSignal.OUT, listE.getTG(attack)); - _main.addSignal(stopAcceptAttack); - ar.addSignals(makeAttack, acceptAttack); - ar.addSignals(stopMakeAttack, stopAcceptAttack); - } + AvatarRelation ar = new AvatarRelation("MainRelation", _main, _main, null); + ar.setAsynchronous(false); + ar.setPrivate(true); + ar.setBroadcast(false); + + _as.addRelation(ar); + for(Attack attack: at.getAttacks()) { + avatartranslator.AvatarSignal makeAttack = new avatartranslator.AvatarSignal("make__" + attack.getName(), AvatarSignal.OUT, (Object)(listE.getTG(attack))); + _main.addSignal(makeAttack); + avatartranslator.AvatarSignal stopMakeAttack = new avatartranslator.AvatarSignal("makeStop__" + attack.getName(), AvatarSignal.IN, listE.getTG(attack)); + _main.addSignal(stopMakeAttack); + avatartranslator.AvatarSignal acceptAttack = new avatartranslator.AvatarSignal("accept__" + attack.getName(), AvatarSignal.IN, listE.getTG(attack)); + _main.addSignal(acceptAttack); + avatartranslator.AvatarSignal stopAcceptAttack = new avatartranslator.AvatarSignal("acceptStop__" + attack.getName(), AvatarSignal.OUT, listE.getTG(attack)); + _main.addSignal(stopAcceptAttack); + ar.addSignals(makeAttack, acceptAttack); + ar.addSignals(stopMakeAttack, stopAcceptAttack); + } } private void makeLeafAttackBlocks(AvatarSpecification _as, AvatarBlock _main) { @@ -338,41 +348,44 @@ public class AttackTreePanelTranslator { _as.addBlock(ab); ab.setFather(_main); - avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("make__" + attack.getName()); - avatartranslator.AvatarSignal stopAttack = _main.getAvatarSignalWithName("makeStop__" + attack.getName()); - - if ((sigAttack != null) && (stopAttack != null)) { - makeAttackBlockSMD(ab, sigAttack, stopAttack, listE.getTG(attack)); - } - - } else if (attack.isRoot()) { - // Make the block + avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("make__" + attack.getName()); + avatartranslator.AvatarSignal stopAttack = _main.getAvatarSignalWithName("makeStop__" + attack.getName()); + + if ((sigAttack != null) && (stopAttack != null)) { + makeAttackBlockSMD(ab, sigAttack, stopAttack, listE.getTG(attack)); + } + + } else if (attack.isFinal()) { + // Make the block AvatarBlock ab = new AvatarBlock(attack.getName(), listE.getTG(attack)); _as.addBlock(ab); ab.setFather(_main); - avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("accept__" + attack.getName()); - avatartranslator.AvatarSignal stopAttack = _main.getAvatarSignalWithName("acceptStop__" + attack.getName()); - + avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("accept__" + attack.getName()); + avatartranslator.AvatarSignal stopAttack = _main.getAvatarSignalWithName("acceptStop__" + attack.getName()); + makeAttackBlockSMD(ab, sigAttack, stopAttack, listE.getTG(attack)); - } + } } } private void makeAttackBlockSMD(AvatarBlock _ab, avatartranslator.AvatarSignal _sigAttack, avatartranslator.AvatarSignal _sigStop, Object _ref) { + Object _ref1 = _ref; + _ref = null; AvatarStateMachine asm = _ab.getStateMachine(); AvatarStartState start = new AvatarStartState("start", _ref); AvatarState mainState = new AvatarState("main", _ref, false); - AvatarState mainStop = new AvatarState("myStop", _ref, false); - AvatarActionOnSignal getMake = new AvatarActionOnSignal("GettingAttack", _sigAttack, _ref); + AvatarState performedState = new AvatarState("main", _ref1, true); + AvatarState mainStop = new AvatarState("stop", _ref, false); + AvatarActionOnSignal getMake = new AvatarActionOnSignal("GettingAttack", _sigAttack, _ref1); AvatarActionOnSignal getStop = new AvatarActionOnSignal("GettingStop", _sigStop, _ref); asm.addElement(start); asm.setStartState(start); asm.addElement(mainState); - asm.addElement(mainStop); + asm.addElement(performedState); asm.addElement(getMake); asm.addElement(getStop); @@ -390,6 +403,11 @@ public class AttackTreePanelTranslator { at = new AvatarTransition("at3", _ref); asm.addElement(at); getMake.addNext(at); + at.addNext(performedState); + + at = new AvatarTransition("backToMain", _ref); + asm.addElement(at); + performedState.addNext(at); at.addNext(mainState); at = new AvatarTransition("at4", _ref); @@ -406,53 +424,515 @@ public class AttackTreePanelTranslator { private void makeAttackNodeBlocks(AvatarSpecification _as, AvatarBlock _main) { - Attack att; + Attack att; - for(AttackNode node: at.getAttackNodes()) { - if (node.isWellFormed()) { - // Make the block + for(AttackNode node: at.getAttackNodes()) { + if (node.isWellFormed()) { + // Make the block AvatarBlock ab = new AvatarBlock(node.getName(), listE.getTG(node)); _as.addBlock(ab); ab.setFather(_main); - if (node instanceof ANDNode) { - makeANDNode(_as, _main, ab, (ANDNode)node, listE.getTG(node)); - } - } - } + if (node instanceof ANDNode) { + makeANDNode(_as, _main, ab, (ANDNode)node, listE.getTG(node)); + } else if (node instanceof ORNode) { + makeORNode(_as, _main, ab, (ORNode)node, listE.getTG(node)); + } else if (node instanceof XORNode) { + makeXORNode(_as, _main, ab, (XORNode)node, listE.getTG(node)); + } else if (node instanceof SequenceNode) { + makeSequenceNode(_as, _main, ab, (SequenceNode)node, listE.getTG(node)); + } else if (node instanceof AfterNode) { + makeAfterNode(_as, _main, ab, (AfterNode)node, listE.getTG(node)); + } else if (node instanceof BeforeNode) { + makeBeforeNode(_as, _main, ab, (BeforeNode)node, listE.getTG(node)); + } + } + } } - private void makeANDNode(AvatarSpecification _as, AvatarBlock _main, AvatarBlock _ab, ANDNode node, Object _ref) { - AvatarStateMachine asm = _ab.getStateMachine(); + private void makeANDNode(AvatarSpecification _as, AvatarBlock _main, AvatarBlock _ab, ANDNode _node, Object _ref) { + Object _ref1 = _ref; + _ref = null; + AvatarStateMachine asm = _ab.getStateMachine(); - // Basic machine - AvatarStartState start = new AvatarStartState("start", _ref); + // Basic machine + AvatarStartState start = new AvatarStartState("start", _ref); AvatarState mainState = new AvatarState("main", _ref, false); - AvatarState endState = new AvatarState("end", _ref, false); - AvatarState overallState = new AvatarState("overall", _ref, false); - AvatarState mainStop = new AvatarState("myStop", _ref, false); - asm.addElement(start); + AvatarState endState = new AvatarState("end", _ref, false); + AvatarState overallState = new AvatarState("overall", _ref, false); + asm.addElement(start); asm.setStartState(start); asm.addElement(mainState); - asm.addElement(endState); - asm.addElement(overallState); - asm.addElement(mainStop); - AvatarTransition at = new AvatarTransition("at1", _ref); + asm.addElement(endState); + asm.addElement(overallState); + AvatarTransition atF = new AvatarTransition("at1", _ref); + asm.addElement(atF); + start.addNext(atF); + atF.addNext(mainState); + String finalGuard = ""; + for(Attack att: _node.getInputAttacks()) { + AvatarAttribute aa = new AvatarAttribute(att.getName() + "__performed", AvatarType.BOOLEAN, _ref); + if (finalGuard.length() ==0) { + finalGuard += "(" + att.getName() + "__performed == true)"; + } else { + finalGuard += " && (" + att.getName() + "__performed == true)"; + } + _ab.addAttribute(aa); + atF.addAction(att.getName() + "__performed = false"); + + avatartranslator.AvatarSignal sigAtt = _main.getAvatarSignalWithName("accept__" + att.getName()); + AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1); + asm.addElement(acceptAttack); + AvatarTransition at = new AvatarTransition("at_toInputAttack", _ref); + asm.addElement(at); + mainState.addNext(at); + at.addNext(acceptAttack); + at.setGuard("["+att.getName() + "__performed == false]"); + at = new AvatarTransition("at_fromInputAttack", _ref); + at.addAction(att.getName() + "__performed = true"); + asm.addElement(at); + acceptAttack.addNext(at); + at.addNext(mainState); + + + } + + // Adding resulting attack + AvatarTransition at = new AvatarTransition("at_toEnd", _ref); asm.addElement(at); - start.addNext(at); - at.addNext(mainState); - + mainState.addNext(at); + at.addNext(endState); + at.setGuard("[" + finalGuard + "]"); + + Attack resulting = _node.getResultingAttack(); + avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("make__" + resulting.getName()); + AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1); + asm.addElement(resultingAttack); + at = new AvatarTransition("at_toResultingAttack", _ref); + asm.addElement(at); + endState.addNext(at); + at.addNext(resultingAttack); + at = new AvatarTransition("at_Overall", _ref); + asm.addElement(at); + resultingAttack.addNext(at); + at.addNext(overallState); + + } + + + private void makeORNode(AvatarSpecification _as, AvatarBlock _main, AvatarBlock _ab, ORNode _node, Object _ref) { + Object _ref1 = _ref; + _ref = null; + AvatarStateMachine asm = _ab.getStateMachine(); + + // Basic machine + AvatarStartState start = new AvatarStartState("start", _ref); + AvatarState mainState = new AvatarState("main", _ref, false); + AvatarState endState = new AvatarState("end", _ref, false); + AvatarState overallState = new AvatarState("overall", _ref, false); + asm.addElement(start); + asm.setStartState(start); + asm.addElement(mainState); + asm.addElement(endState); + asm.addElement(overallState); + + AvatarTransition atF = new AvatarTransition("at1", _ref); + asm.addElement(atF); + start.addNext(atF); + atF.addNext(mainState); + String finalGuard = ""; + for(Attack att: _node.getInputAttacks()) { + AvatarAttribute aa = new AvatarAttribute(att.getName() + "__performed", AvatarType.BOOLEAN, _ref); + if (finalGuard.length() ==0) { + finalGuard += "(" + att.getName() + "__performed == true)"; + } else { + finalGuard += " || (" + att.getName() + "__performed == true)"; + } + _ab.addAttribute(aa); + atF.addAction(att.getName() + "__performed = false"); + + // From Main + avatartranslator.AvatarSignal sigAtt = _main.getAvatarSignalWithName("accept__" + att.getName()); + AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1); + asm.addElement(acceptAttack); + AvatarTransition at = new AvatarTransition("at_toInputAttack", _ref); + asm.addElement(at); + mainState.addNext(at); + at.addNext(acceptAttack); + at.setGuard("["+att.getName() + "__performed == false]"); + at = new AvatarTransition("at_fromInputAttack", _ref); + at.addAction(att.getName() + "__performed = true"); + asm.addElement(at); + acceptAttack.addNext(at); + at.addNext(mainState); + + // Link from End + acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1); + asm.addElement(acceptAttack); + at = new AvatarTransition("at_toInputAttack", _ref); + asm.addElement(at); + endState.addNext(at); + at.addNext(acceptAttack); + at.setGuard("["+att.getName() + "__performed == false]"); + at = new AvatarTransition("at_fromInputAttack", _ref); + at.addAction(att.getName() + "__performed = true"); + asm.addElement(at); + acceptAttack.addNext(at); + at.addNext(endState); + + // Link from Overall + acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1); + asm.addElement(acceptAttack); + at = new AvatarTransition("at_toInputAttack", _ref); + asm.addElement(at); + overallState.addNext(at); + at.addNext(acceptAttack); + at.setGuard("["+att.getName() + "__performed == false]"); + at = new AvatarTransition("at_fromInputAttack", _ref); + at.addAction(att.getName() + "__performed = true"); + asm.addElement(at); + acceptAttack.addNext(at); + at.addNext(overallState); + + + } + + // Adding resulting attack - + AvatarTransition at = new AvatarTransition("at_toEnd", _ref); + asm.addElement(at); + mainState.addNext(at); + at.addNext(endState); + at.setGuard("[" + finalGuard + "]"); + + Attack resulting = _node.getResultingAttack(); + avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("make__" + resulting.getName()); + AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1); + asm.addElement(resultingAttack); + at = new AvatarTransition("at_toResultingAttack", _ref); + asm.addElement(at); + endState.addNext(at); + at.addNext(resultingAttack); + at = new AvatarTransition("at_Overall", _ref); + asm.addElement(at); + resultingAttack.addNext(at); + at.addNext(overallState); + } - // Computing accept attacks - - + private void makeXORNode(AvatarSpecification _as, AvatarBlock _main, AvatarBlock _ab, XORNode _node, Object _ref) { + Object _ref1 = _ref; + _ref = null; + AvatarStateMachine asm = _ab.getStateMachine(); + + // Basic machine + AvatarStartState start = new AvatarStartState("start", _ref); + AvatarState mainState = new AvatarState("main", _ref, false); + AvatarState stoppingAll = new AvatarState("stoppingAll", _ref, false); + AvatarState endState = new AvatarState("end", _ref, false); + AvatarState overallState = new AvatarState("overall", _ref, false); + asm.addElement(start); + asm.setStartState(start); + asm.addElement(mainState); + asm.addElement(endState); + asm.addElement(overallState); + asm.addElement(stoppingAll); + AvatarTransition atF = new AvatarTransition("at1", _ref); + asm.addElement(atF); + start.addNext(atF); + atF.addNext(mainState); + String finalGuard = "oneDone == true"; + String toEndGuard = ""; + AvatarAttribute oneDone = new AvatarAttribute("oneDone", AvatarType.BOOLEAN, _ref); + _ab.addAttribute(oneDone); + atF.addAction("oneDone = false"); + for(Attack att: _node.getInputAttacks()) { + AvatarAttribute aa = new AvatarAttribute(att.getName() + "__performed", AvatarType.BOOLEAN, _ref); + _ab.addAttribute(aa); + atF.addAction(att.getName() + "__performed = false"); + if (toEndGuard.length() ==0) { + toEndGuard += "(" + att.getName() + "__performed == true)"; + } else { + toEndGuard += " && (" + att.getName() + "__performed == true)"; + } + // From Main + avatartranslator.AvatarSignal sigAtt = _main.getAvatarSignalWithName("accept__" + att.getName()); + AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1); + asm.addElement(acceptAttack); + AvatarTransition at = new AvatarTransition("at_toInputAttack", _ref); + asm.addElement(at); + mainState.addNext(at); + at.addNext(acceptAttack); + at.setGuard("[("+att.getName() + "__performed == false) && (oneDone == false)]"); + at = new AvatarTransition("at_fromInputAttack", _ref); + at.addAction(att.getName() + "__performed = true"); + at.addAction("oneDone = true"); + asm.addElement(at); + acceptAttack.addNext(at); + at.addNext(mainState); + + // Link from stoppingAll + sigAtt = _main.getAvatarSignalWithName("acceptStop__" + att.getName()); + acceptAttack = new AvatarActionOnSignal("StopAttack", sigAtt, _ref); + asm.addElement(acceptAttack); + at = new AvatarTransition("at_toInputAttack", _ref); + asm.addElement(at); + stoppingAll.addNext(at); + at.addNext(acceptAttack); + at.setGuard("["+att.getName() + "__performed == false]"); + at = new AvatarTransition("at_fromInputAttack", _ref); + at.addAction(att.getName() + "__performed = true"); + asm.addElement(at); + acceptAttack.addNext(at); + at.addNext(stoppingAll); + + } + + // Adding link to stopping all + AvatarTransition at = new AvatarTransition("at_toStoppingAll", _ref); + asm.addElement(at); + mainState.addNext(at); + at.addNext(stoppingAll); + at.setGuard("[" + finalGuard + "]"); + + + // Adding resulting attack + at = new AvatarTransition("at_toEnd", _ref); + asm.addElement(at); + stoppingAll.addNext(at); + at.addNext(endState); + at.setGuard("[" + toEndGuard + "]"); + + Attack resulting = _node.getResultingAttack(); + avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("make__" + resulting.getName()); + AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1); + asm.addElement(resultingAttack); + at = new AvatarTransition("at_toResultingAttack", _ref); + asm.addElement(at); + endState.addNext(at); + at.addNext(resultingAttack); + at = new AvatarTransition("at_Overall", _ref); + asm.addElement(at); + resultingAttack.addNext(at); + at.addNext(overallState); + + } + + + + private void makeSequenceNode(AvatarSpecification _as, AvatarBlock _main, AvatarBlock _ab, SequenceNode _node, Object _ref) { + Object _ref1 = _ref; + _ref = null; + AvatarStateMachine asm = _ab.getStateMachine(); + _node.orderAttacks(); + + // Basic machine + AvatarStartState start = new AvatarStartState("start", _ref); + AvatarState mainState = new AvatarState("main", _ref, false); + AvatarState endState = new AvatarState("end", _ref, false); + AvatarState overallState = new AvatarState("overall", _ref, false); + asm.addElement(start); + asm.setStartState(start); + asm.addElement(mainState); + asm.addElement(endState); + asm.addElement(overallState); + + + AvatarTransition at = new AvatarTransition("at", _ref); + asm.addElement(at); + start.addNext(at); + at.addNext(mainState); + + AvatarState previousState = mainState; + + // Chaining accept attacks + for(Attack att: _node.getInputAttacks()) { + AvatarState state = new AvatarState("state__" + att.getName(), _ref); + asm.addElement(state); + avatartranslator.AvatarSignal sigAtt = _main.getAvatarSignalWithName("accept__" + att.getName()); + AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1); + asm.addElement(acceptAttack); + + at = new AvatarTransition("at", _ref); + asm.addElement(at); + previousState.addNext(at); + at.addNext(acceptAttack); + at = new AvatarTransition("at", _ref); + asm.addElement(at); + acceptAttack.addNext(at); + at.addNext(state); + previousState = state; + } + + at = new AvatarTransition("at", _ref); + asm.addElement(at); + previousState.addNext(at); + at.addNext(endState); + + + // Performing resulting attack + Attack resulting = _node.getResultingAttack(); + avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("make__" + resulting.getName()); + AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1); + asm.addElement(resultingAttack); + at = new AvatarTransition("at_toResultingAttack", _ref); + asm.addElement(at); + endState.addNext(at); + at.addNext(resultingAttack); + at = new AvatarTransition("at_Overall", _ref); + asm.addElement(at); + resultingAttack.addNext(at); + at.addNext(overallState); + } + + private void makeAfterNode(AvatarSpecification _as, AvatarBlock _main, AvatarBlock _ab, AfterNode _node, Object _ref) { + Object _ref1 = _ref; + _ref = null; + AvatarStateMachine asm = _ab.getStateMachine(); + _node.orderAttacks(); + + // Basic machine + AvatarStartState start = new AvatarStartState("start", _ref); + AvatarState mainState = new AvatarState("main", _ref, false); + AvatarState endState = new AvatarState("end", _ref, false); + AvatarState overallState = new AvatarState("overall", _ref, false); + asm.addElement(start); + asm.setStartState(start); + asm.addElement(mainState); + asm.addElement(endState); + asm.addElement(overallState); + + + AvatarTransition at = new AvatarTransition("at", _ref); + asm.addElement(at); + start.addNext(at); + at.addNext(mainState); + + AvatarState previousState = mainState; + + // Chaining accept attacks + int cpt = 0; + for(Attack att: _node.getInputAttacks()) { + AvatarState state = new AvatarState("state__" + att.getName(), _ref); + asm.addElement(state); + avatartranslator.AvatarSignal sigAtt = _main.getAvatarSignalWithName("accept__" + att.getName()); + AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1); + asm.addElement(acceptAttack); + + at = new AvatarTransition("at", _ref); + asm.addElement(at); + previousState.addNext(at); + at.addNext(acceptAttack); + if (cpt > 0) { + at.setDelays("" + _node.getTime(), "" + _node.getTime()); + } + at = new AvatarTransition("at", _ref); + asm.addElement(at); + acceptAttack.addNext(at); + at.addNext(state); + previousState = state; + cpt ++; + } + + at = new AvatarTransition("at", _ref); + asm.addElement(at); + previousState.addNext(at); + at.addNext(endState); + + + // Performing resulting attack + Attack resulting = _node.getResultingAttack(); + avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("make__" + resulting.getName()); + AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1); + asm.addElement(resultingAttack); + at = new AvatarTransition("at_toResultingAttack", _ref); + asm.addElement(at); + endState.addNext(at); + at.addNext(resultingAttack); + at = new AvatarTransition("at_Overall", _ref); + asm.addElement(at); + resultingAttack.addNext(at); + at.addNext(overallState); + } + + private void makeBeforeNode(AvatarSpecification _as, AvatarBlock _main, AvatarBlock _ab, BeforeNode _node, Object _ref) { + Object _ref1 = _ref; + _ref = null; + AvatarStateMachine asm = _ab.getStateMachine(); + _node.orderAttacks(); + + // Basic machine + AvatarStartState start = new AvatarStartState("start", _ref); + AvatarState mainState = new AvatarState("main", _ref, false); + AvatarState endState = new AvatarState("end", _ref, false); + AvatarState overallState = new AvatarState("overall", _ref, false); + AvatarState timeout = new AvatarState("timeout", _ref, false); + asm.addElement(start); + asm.setStartState(start); + asm.addElement(mainState); + asm.addElement(endState); + asm.addElement(overallState); + asm.addElement(timeout); + + + AvatarTransition at = new AvatarTransition("at", _ref); + asm.addElement(at); + start.addNext(at); + at.addNext(mainState); + + AvatarState previousState = mainState; + + // Chaining accept attacks + int cpt = 0; + for(Attack att: _node.getInputAttacks()) { + AvatarState state = new AvatarState("state__" + att.getName(), _ref); + asm.addElement(state); + avatartranslator.AvatarSignal sigAtt = _main.getAvatarSignalWithName("accept__" + att.getName()); + AvatarActionOnSignal acceptAttack = new AvatarActionOnSignal("AcceptAttack", sigAtt, _ref1); + asm.addElement(acceptAttack); + + at = new AvatarTransition("at", _ref); + asm.addElement(at); + previousState.addNext(at); + at.addNext(acceptAttack); + if (cpt > 0) { + at = new AvatarTransition("at_totimeout", _ref); + asm.addElement(at); + previousState.addNext(at); + at.addNext(timeout); + at.setDelays("" + _node.getTime(), "" + _node.getTime()); + } + at = new AvatarTransition("at", _ref); + asm.addElement(at); + acceptAttack.addNext(at); + at.addNext(state); + previousState = state; + cpt ++; + } + + at = new AvatarTransition("at", _ref); + asm.addElement(at); + previousState.addNext(at); + at.addNext(endState); + + + // Performing resulting attack + Attack resulting = _node.getResultingAttack(); + avatartranslator.AvatarSignal sigAttack = _main.getAvatarSignalWithName("make__" + resulting.getName()); + AvatarActionOnSignal resultingAttack = new AvatarActionOnSignal("ResultingAttack", sigAttack, _ref1); + asm.addElement(resultingAttack); + at = new AvatarTransition("at_toResultingAttack", _ref); + asm.addElement(at); + endState.addNext(at); + at.addNext(resultingAttack); + at = new AvatarTransition("at_Overall", _ref); + asm.addElement(at); + resultingAttack.addNext(at); + at.addNext(overallState); } diff --git a/src/ui/ColorManager.java b/src/ui/ColorManager.java index 1756118bd0145fd3b311f4e7d9c10460e44a86ce..02ade04bcec797882d057e3be6063502e1e148e7 100755 --- a/src/ui/ColorManager.java +++ b/src/ui/ColorManager.java @@ -132,7 +132,8 @@ public class ColorManager { public static final Color IOD_REFERENCE = new Color(216, 187, 249); - public static Color ATD_BLOCK = new Color(196, 232, 195); + //public static Color ATD_BLOCK = new Color(196, 232, 195); + public static Color ATD_BLOCK = new Color(218, 218, 218); public static Color ATD_ATTACK = new Color(214, 187, 158); public static Color ATD_ROOT_ATTACK = new Color(243, 131, 10); public static Color ATD_CONSTRAINT = new Color(191, 153, 161); diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java index d8e6ff3799c0657e0c1581c23aa6dc3963c47254..57358991ad6e60a733cfd77fc9b62747b6f537a6 100755 --- a/src/ui/GTURTLEModeling.java +++ b/src/ui/GTURTLEModeling.java @@ -746,6 +746,19 @@ public class GTURTLEModeling { TraceManager.addDev("Could not make query for " + tgc); } } + } else if ((avatar2uppaal != null) && (tp instanceof AttackTreePanel)) { + TraceManager.addDev("Making UPPAAL queries"); + for(TGComponent tgc: list) { + TraceManager.addDev("Making UPPAAL query for " + tgc); + String s = avatar2uppaal.getUPPAALIdentification(tgc); + TraceManager.addDev("Query: " + s); + if ((s!= null) && (s.length() > 0)) { + AvatarBlock block = avatar2uppaal.getBlockFromReferenceObject(tgc); + listQ.add(s + "$" + block.getName() + "." + tgc); + } else { + TraceManager.addDev("Could not make query for " + tgc); + } + } } return listQ; @@ -2003,6 +2016,10 @@ public class GTURTLEModeling { return; } + if (adp == null) { + return; + } + adp.removeAllMutualExclusionWithMasterMutex(); diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java index 1f4d059fb5cce6337074c69b3548b49e40969160..2550fd65842b768aad0b4f31433d1c58df82c9a4 100755 --- a/src/ui/MainGUI.java +++ b/src/ui/MainGUI.java @@ -210,6 +210,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe public final static byte EDIT_PROVERIF_OK = 46; public final static byte AVATAR_SYNTAXCHECKING_OK = 47; public final static byte PANEL_CHANGED = 48; + public final static byte ATTACKTREE_SYNTAXCHECKING_OK = 49; public final static int INCREMENT = 10; @@ -668,6 +669,13 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe actions[TGUIAction.ACT_AVATAR_FV_STATICANALYSIS].setEnabled(true); actions[TGUIAction.ACT_AVATAR_EXECUTABLE_GENERATION].setEnabled(true); break; + case ATTACKTREE_SYNTAXCHECKING_OK: + actions[TGUIAction.ACT_AVATAR_SIM].setEnabled(true); + actions[TGUIAction.ACT_AVATAR_FV_UPPAAL].setEnabled(true); + actions[TGUIAction.ACT_AVATAR_FV_PROVERIF].setEnabled(false); + actions[TGUIAction.ACT_AVATAR_FV_STATICANALYSIS].setEnabled(false); + actions[TGUIAction.ACT_AVATAR_EXECUTABLE_GENERATION].setEnabled(false); + break; case REQ_OK: //actions[TGUIAction.ACT_VIEW_MATRIX].setEnabled(true); actions[TGUIAction.ACT_VALIDATION].setEnabled(true); @@ -3174,7 +3182,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Pe AttackTreePanel atp = (AttackTreePanel) tp; b = gtm.translateAttackTreePanel(atp); if (b) { - setMode(MainGUI.AVATAR_SYNTAXCHECKING_OK); + setMode(MainGUI.ATTACKTREE_SYNTAXCHECKING_OK); ret = true; if (!automatic) { JOptionPane.showMessageDialog(frame, diff --git a/src/ui/TGComponent.java b/src/ui/TGComponent.java index 8974ea8580b7022ee21fd3a18a3a5800b086d9cc..dccd8114961d95216e20f26e63187e15b1a408ad 100755 --- a/src/ui/TGComponent.java +++ b/src/ui/TGComponent.java @@ -676,6 +676,7 @@ public abstract class TGComponent implements CDElement, GenericTree { // _mode: 1 : running // 2 : selected for execution public void drawAVATARComp(Graphics g, int _mode) { + //TraceManager.addDev("drawing avatar comp=" + this); int wb = 30; int hb = 10; int wh = 15; @@ -697,6 +698,12 @@ public abstract class TGComponent implements CDElement, GenericTree { myheight = height; } + if (_mode == 1) { + g.setColor(ColorManager.CURRENT_COMMAND_RUNNING); + } else { + g.setColor(ColorManager.CURRENT_COMMAND_SUSPENDED); + } + xp[0] = myx - sep - wb -wh; yp[0] = myy + ((myheight-hb) / 2); @@ -718,11 +725,7 @@ public abstract class TGComponent implements CDElement, GenericTree { xp[6] = myx - sep - wb -wh; yp[6] = myy + ((myheight+hb) / 2); - if (_mode == 1) { - g.setColor(ColorManager.CURRENT_COMMAND_RUNNING); - } else { - g.setColor(ColorManager.CURRENT_COMMAND_SUSPENDED); - } + g.fillPolygon(xp, yp, 7); } diff --git a/src/ui/atd/ATDAttack.java b/src/ui/atd/ATDAttack.java index 0f3acaa9cdab3a4a55fa82701c8880224e9cb0c7..7550155e68011ae40562d6e403207ecfa5909155 100755 --- a/src/ui/atd/ATDAttack.java +++ b/src/ui/atd/ATDAttack.java @@ -56,7 +56,7 @@ import myutil.*; import ui.*; import ui.window.*; -public class ATDAttack extends TGCScalableWithInternalComponent implements SwallowedTGComponent, WithAttributes { +public class ATDAttack extends TGCScalableWithInternalComponent implements SwallowedTGComponent, WithAttributes, CheckableAccessibility { private int textY1 = 3; private int textY2 = 3; diff --git a/src/ui/atd/ATDConstraint.java b/src/ui/atd/ATDConstraint.java index 42b8d0d896286f53e6632c7f1dbda59e69474030..9f909456c711ed23ee018a787c0693e8c675c6b6 100755 --- a/src/ui/atd/ATDConstraint.java +++ b/src/ui/atd/ATDConstraint.java @@ -60,7 +60,7 @@ public class ATDConstraint extends TGCScalableWithInternalComponent implements private int textY1 = 5; //private int textY2 = 30; - public static final String[] STEREOTYPES = {"<<OR>>", "<<AND>>", "<<SEQUENCE>>", "<<BEFORE>>", "<<AFTER>>"}; + public static final String[] STEREOTYPES = {"<<OR>>", "<<XOR>>", "<<AND>>", "<<SEQUENCE>>", "<<BEFORE>>", "<<AFTER>>"}; protected String oldValue = ""; @@ -237,22 +237,26 @@ public class ATDConstraint extends TGCScalableWithInternalComponent implements return (value.compareTo(STEREOTYPES[0]) == 0); } - public boolean isAND() { + public boolean isXOR() { return (value.compareTo(STEREOTYPES[1]) == 0); } - public boolean isSequence() { + public boolean isAND() { return (value.compareTo(STEREOTYPES[2]) == 0); } - public boolean isBefore() { + public boolean isSequence() { return (value.compareTo(STEREOTYPES[3]) == 0); } - public boolean isAfter() { + public boolean isBefore() { return (value.compareTo(STEREOTYPES[4]) == 0); } + public boolean isAfter() { + return (value.compareTo(STEREOTYPES[5]) == 0); + } + protected String translateExtraParam() { StringBuffer sb = new StringBuffer("<extraparam>\n"); sb.append("<info equation=\"" + GTURTLEModeling.transformString(getEquation())); diff --git a/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java b/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java index 5016695501bd065708a24292ce12d928a7990a34..06d28b44fc1f6fac4d4e0052b33b314d3d4e7052 100755 --- a/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java +++ b/src/ui/avatarinteractivesimulation/JFrameAvatarInteractiveSimulation.java @@ -113,7 +113,7 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements Avatar //List of transactions private JList listPendingTransactions; - private TGComponent selectedComponentForTransaction; + private TGComponent selectedComponentForTransaction1, selectedComponentForTransaction2; private AvatarSimulationBlock previousBlock; private int invokedLater = 0; @@ -268,7 +268,8 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements Avatar Vector<AvatarSimulationPendingTransaction> ll = (Vector<AvatarSimulationPendingTransaction>)(ass.getPendingTransitions().clone()); listPendingTransactions.clearSelection(); - selectedComponentForTransaction = null; + selectedComponentForTransaction1 = null; + selectedComponentForTransaction2 = null; if (ll != null) { listPendingTransactions.setListData(ll); int random = (int)(Math.floor((Math.random()*ll.size()))); @@ -1210,7 +1211,9 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements Avatar if (avspec.getReferenceObject() instanceof AvatarDesignPanel) { ((AvatarDesignPanel)(avspec.getReferenceObject())).resetMetElements(); - } + } else if (avspec.getReferenceObject() instanceof AttackTreePanel) { + ((AttackTreePanel)(avspec.getReferenceObject())).resetMetElements(); + } } public void updateMetElements() { @@ -1395,7 +1398,7 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements Avatar public boolean isSelectedComponentFromTransaction(TGComponent _tgc) { if (isVisible()) { - return _tgc == selectedComponentForTransaction; + return (_tgc == selectedComponentForTransaction1) || (_tgc == selectedComponentForTransaction2); } return false; } @@ -1762,11 +1765,14 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements Avatar if (index > -1) { try { AvatarSimulationPendingTransaction aspt = (AvatarSimulationPendingTransaction)(listPendingTransactions.getSelectedValue()); - selectedComponentForTransaction = (TGComponent)(aspt.elementToExecute.getReferenceObject()); - if ((selectedComponentForTransaction == null) && (aspt.linkedTransaction != null)) { + selectedComponentForTransaction1 = (TGComponent)(aspt.elementToExecute.getReferenceObject()); + if ((selectedComponentForTransaction1 == null) && (aspt.linkedTransaction != null)) { //TraceManager.addDev("Adding reference object: " + aspt.linkedTransaction.elementToExecute.getReferenceObject()); - selectedComponentForTransaction = (TGComponent)(aspt.linkedTransaction.elementToExecute.getReferenceObject()); - } + selectedComponentForTransaction1 = (TGComponent)(aspt.linkedTransaction.elementToExecute.getReferenceObject()); + selectedComponentForTransaction2 = null; + } else if (aspt.linkedTransaction != null) { + selectedComponentForTransaction2 = (TGComponent)(aspt.linkedTransaction.elementToExecute.getReferenceObject()); + } if (!(busyMode == AvatarSpecificationSimulation.GATHER) && !(busyMode == AvatarSpecificationSimulation.EXECUTE)) { ass.setIndexSelectedTransaction(listPendingTransactions.getSelectedIndex()); } @@ -1782,7 +1788,8 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements Avatar } } catch (Exception ex){ TraceManager.addDev("Exception selected component"); - selectedComponentForTransaction = null; + selectedComponentForTransaction1 = null; + selectedComponentForTransaction2 = null; if (openDiagram.isSelected()) { if ((previousBlock != null) && (animate.isSelected())){ mgui.openAVATARSMD(previousBlock.getName()); @@ -1794,7 +1801,8 @@ public class JFrameAvatarInteractiveSimulation extends JFrame implements Avatar } } } else { - selectedComponentForTransaction = null; + selectedComponentForTransaction1 = null; + selectedComponentForTransaction2 = null; if ((previousBlock != null) && (animate.isSelected())) { if (openDiagram.isSelected()) { mgui.openAVATARSMD(previousBlock.getName()); diff --git a/src/ui/window/JDialogConstraintText.java b/src/ui/window/JDialogConstraintText.java index 627ef952ec8ea49c7d5e05f0320e5d870a5d3eac..9ee1986e608656982e5cebbddb9221c77f95abc4 100755 --- a/src/ui/window/JDialogConstraintText.java +++ b/src/ui/window/JDialogConstraintText.java @@ -58,39 +58,39 @@ import ui.atd.*; public class JDialogConstraintText extends javax.swing.JDialog implements ActionListener { - + private boolean regularClose; - + private JPanel panel2; private Frame frame; - + //protected JTextField taskName; - protected JComboBox stereotype; - protected JTextField textEdition; - - + protected JComboBox stereotype; + protected JTextField textEdition; + + // Main Panel private JButton closeButton; private JButton cancelButton; - - - - private ConstraintListInterface constraint; - + + + + private ConstraintListInterface constraint; + /** Creates new form */ public JDialogConstraintText(Frame _frame, String _title, ConstraintListInterface _constraint, String _text, String _label) { super(_frame, _title, true); frame = _frame; constraint = _constraint; - + initComponents(_text, _label); myInitComponents(); pack(); } - + private void myInitComponents() { } - + private void initComponents(String _text, String _label) { Container c = getContentPane(); GridBagLayout gridbag0 = new GridBagLayout(); @@ -99,48 +99,48 @@ public class JDialogConstraintText extends javax.swing.JDialog implements Action 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); - - + + panel2 = new JPanel(); panel2.setLayout(gridbag2); panel2.setBorder(new javax.swing.border.TitledBorder("Constraint attributes")); panel2.setPreferredSize(new Dimension(350, 250)); - - c1.gridwidth = 1; + + c1.gridwidth = 1; c1.gridheight = 1; c1.weighty = 1.0; c1.weightx = 1.0; c1.fill = GridBagConstraints.HORIZONTAL; c1.gridwidth = GridBagConstraints.REMAINDER; //end row - stereotype = new JComboBox(constraint.getConstraintList()); - for(int i = 0; i<constraint.getConstraintList().length; i++) { - if (constraint.getCurrentConstraint().compareTo(constraint.getConstraintList()[i]) == 0) { - stereotype.setSelectedIndex(i); - break; - } - } - panel2.add(stereotype, c1); - - c1.gridwidth = 1; - JLabel lab = new JLabel(_label + ":"); - panel2.add(lab, c1); - c1.gridwidth = GridBagConstraints.REMAINDER; //end row - textEdition = new JTextField(_text); - panel2.add(textEdition, c1); - - + stereotype = new JComboBox(constraint.getConstraintList()); + for(int i = 0; i<constraint.getConstraintList().length; i++) { + if (constraint.getCurrentConstraint().compareTo(constraint.getConstraintList()[i]) == 0) { + stereotype.setSelectedIndex(i); + break; + } + } + panel2.add(stereotype, c1); + + c1.gridwidth = 1; + JLabel lab = new JLabel(_label + ":"); + panel2.add(lab, c1); + c1.gridwidth = GridBagConstraints.REMAINDER; //end row + textEdition = new JTextField(_text); + panel2.add(textEdition, c1); + + // main panel; c0.gridheight = 10; c0.weighty = 1.0; c0.weightx = 1.0; c0.gridwidth = GridBagConstraints.REMAINDER; //end row c.add(panel2, c0); - + c0.gridwidth = 1; c0.gridheight = 1; c0.fill = GridBagConstraints.HORIZONTAL; @@ -153,10 +153,10 @@ public class JDialogConstraintText extends javax.swing.JDialog implements Action cancelButton.addActionListener(this); c.add(cancelButton, c0); } - - public void actionPerformed(ActionEvent evt) { + + public void actionPerformed(ActionEvent evt) { String command = evt.getActionCommand(); - + // Compare the action command to the known actions. if (command.equals("Save and Close")) { closeDialog(); @@ -164,28 +164,28 @@ public class JDialogConstraintText extends javax.swing.JDialog implements Action cancelDialog(); } } - + public void closeDialog() { regularClose = true; dispose(); } - + public void cancelDialog() { dispose(); } - + public boolean isRegularClose() { return regularClose; } - - public String getStereotype() { - return (String)(stereotype.getSelectedItem()); + + public String getStereotype() { + return (String)(stereotype.getSelectedItem()); } - - + + public String getText() { - return textEdition.getText(); + return textEdition.getText(); } - + }