diff --git a/Makefile b/Makefile index 8d596517c0905854688f22aa63d68d4a1a0907ef..932ace5fd9f18e5fdbe01bfe325382eab9c09868 100755 --- a/Makefile +++ b/Makefile @@ -13,7 +13,7 @@ GZIP = gzip -9 -f DEBUG = -g CLASSPATH = -classpath CLASSPATH = -sourcepath -PACKAGE = avatartranslator automata compiler/tmlparser vcd nc ddtranslator launcher myutil tpndescription sddescription sdtranslator translator tmltranslator tmltranslator/toautomata tmltranslator/tosystemc tmltranslator/tomappingsystemc tmltranslator/tomappingsystemc2 tmltranslator/touppaal tmltranslator/toturtle translator/tojava translator/tosimujava translator/totpn translator/touppaal ui ui/avatarbd ui/avatarsmd ui/avatarrd ui/ad ui/cd ui/oscd ui/osad ui/dd ui/ebrdd ui/file ui/graph ui/iod ui/ncdd ui/procsd ui/prosmdui/prosmd/util ui/tmlad ui/tmlcd ui/tmldd ui/tmlcomp ui/req ui/sd ui/tree ui/ucd ui/window tmltranslator tmltranslator/toturtle req/ebrdd tmltranslator/tosystemc tmatrix uppaaldesc fr/inria/oasis/vercors/cttool/model remotesimulation +PACKAGE = avatartranslator avatartranslator/toturtle automata compiler/tmlparser vcd nc ddtranslator launcher myutil tpndescription sddescription sdtranslator translator tmltranslator tmltranslator/toautomata tmltranslator/tosystemc tmltranslator/tomappingsystemc tmltranslator/tomappingsystemc2 tmltranslator/touppaal tmltranslator/toturtle translator/tojava translator/tosimujava translator/totpn translator/touppaal ui ui/avatarbd ui/avatarsmd ui/avatarrd ui/ad ui/cd ui/oscd ui/osad ui/dd ui/ebrdd ui/file ui/graph ui/iod ui/ncdd ui/procsd ui/prosmdui/prosmd/util ui/tmlad ui/tmlcd ui/tmldd ui/tmlcomp ui/req ui/sd ui/tree ui/ucd ui/window tmltranslator tmltranslator/toturtle req/ebrdd tmltranslator/tosystemc tmatrix uppaaldesc fr/inria/oasis/vercors/cttool/model remotesimulation BUILDER = builder.jar BUILD_INFO = build.txt BUILD_TO_MODIFY = src/ui/DefaultText.java @@ -80,7 +80,7 @@ basic: ttooljar_std: rm -f $(TTOOL_BIN)/$(TTOOL_BINARY) cp $(TTOOL_SRC)/ui/images/$(STD_LOGO) $(TTOOL_SRC)/ui/images/$(LOGO) - cd $(TTOOL_SRC); $(JAR) cmf $(TTOOL_JAR_TXT) $(TTOOL_BIN)/$(TTOOL_BINARY) Main.class vcd/*.class avatartranslator/*.class automata/*.class compiler/tmlparser/*.class nc/*.class tmltranslator/*.class tmltranslator/toautomata/*.class tmatrix/*.class tmltranslator/toturtle/*.class tmltranslator/touppaal/*.class tmltranslator/tosystemc/*.class tmltranslator/tomappingsystemc/*.class tmltranslator/tomappingsystemc2/*.class tpndescription/*.class ddtranslator/*.class launcher/*.class myutil/*.class sddescription/*.class sdtranslator/*.class translator/*.class translator/tojava/*.class translator/tosimujava/*.class translator/touppaal/*.class translator/totpn/*.class req/ebrdd/*.java ui/*.class ui/*/*.class ui/*/*/*.class uppaaldesc/*.class ui/images/*.* ui/images/toolbarButtonGraphics/general/*.gif ui/images/toolbarButtonGraphics/media/*.gif $(TTOOL_BIN)/$(LAUNCHER_BINARY) RTLLauncher.class launcher/*.class fr/inria/oasis/vercors/cttool/model/*.class remotesimulation/*.class + cd $(TTOOL_SRC); $(JAR) cmf $(TTOOL_JAR_TXT) $(TTOOL_BIN)/$(TTOOL_BINARY) Main.class vcd/*.class avatartranslator/*.class avatartranslator/toturtle/*.java automata/*.class compiler/tmlparser/*.class nc/*.class tmltranslator/*.class tmltranslator/toautomata/*.class tmatrix/*.class tmltranslator/toturtle/*.class tmltranslator/touppaal/*.class tmltranslator/tosystemc/*.class tmltranslator/tomappingsystemc/*.class tmltranslator/tomappingsystemc2/*.class tpndescription/*.class ddtranslator/*.class launcher/*.class myutil/*.class sddescription/*.class sdtranslator/*.class translator/*.class translator/tojava/*.class translator/tosimujava/*.class translator/touppaal/*.class translator/totpn/*.class req/ebrdd/*.java ui/*.class ui/*/*.class ui/*/*/*.class uppaaldesc/*.class ui/images/*.* ui/images/toolbarButtonGraphics/general/*.gif ui/images/toolbarButtonGraphics/media/*.gif $(TTOOL_BIN)/$(LAUNCHER_BINARY) RTLLauncher.class launcher/*.class fr/inria/oasis/vercors/cttool/model/*.class remotesimulation/*.class launcher: diff --git a/src/avatartranslator/AvatarActionOnSignal.java b/src/avatartranslator/AvatarActionOnSignal.java index 832e6144d6f07aca76248ba7b564740ffc67c7fa..17aa7ee28bc09721de6e9987f74d345750eb38fc 100644 --- a/src/avatartranslator/AvatarActionOnSignal.java +++ b/src/avatartranslator/AvatarActionOnSignal.java @@ -71,7 +71,7 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement { } public String getValue(int _index) { - return value.get(_index); + return values.get(_index); } public boolean isSending() { diff --git a/src/avatartranslator/AvatarAttribute.java b/src/avatartranslator/AvatarAttribute.java index 317302846af9daba3e17707af7621fad91285436..a907bc12aa10b5e29ab2491346979bb83c5f68be 100644 --- a/src/avatartranslator/AvatarAttribute.java +++ b/src/avatartranslator/AvatarAttribute.java @@ -73,10 +73,26 @@ public class AvatarAttribute extends AvatarElement{ return initialValue; } + public String getDefaultInitialValue() { + return AvatarType.getDefaultInitialValue(type); + } + public int getType() { return type; } + public boolean isInt() { + return (type == AvatarType.INTEGER); + } + + public boolean isNat() { + return (type == AvatarType.NATURAL); + } + + public boolean isBool() { + return (type == AvatarType.BOOLEAN); + } + public static boolean isAValidAttributeName(String id) { if ((id == null) || (id.length() < 1)) { return false; diff --git a/src/avatartranslator/AvatarBlock.java b/src/avatartranslator/AvatarBlock.java index a872fb86d55653b6ab93be0799dda02f2a3b2233..845bde8b85b01be08c5cec20ab9d1295736c980c 100644 --- a/src/avatartranslator/AvatarBlock.java +++ b/src/avatartranslator/AvatarBlock.java @@ -47,6 +47,8 @@ package avatartranslator; import java.util.*; +import myutil.*; + public class AvatarBlock extends AvatarElement { @@ -91,20 +93,62 @@ public class AvatarBlock extends AvatarElement { } public String toString() { - StringBuffer sb = new StringBuffer("block:" + getName() + "\n"); + StringBuffer sb = new StringBuffer("block:" + getName() + " ID=" + getID() + " \n"); + if (getFather() != null) { + sb.append(" subblock of: " + getFather().getName() + " ID=" + getFather().getID()+ "\n"); + } else { + sb.append(" top level block\n"); + } for(AvatarAttribute attribute: attributes) { - sb.append(" attribute: " + attribute.toString() + "\n"); + sb.append(" attribute: " + attribute.toString() + " ID=" + attribute.getID() + "\n"); } for(AvatarMethod method: methods) { - sb.append(" method: " + method.toString() + "\n"); + sb.append(" method: " + method.toString() + " ID=" + method.getID() + "\n"); } for(AvatarSignal signal: signals) { - sb.append(" signal: " + signal.toString() + "\n"); + sb.append(" signal: " + signal.toString() + " ID=" + signal.getID() + "\n"); + } + if (asm != null) { + sb.append(asm.toString()); + } else { + sb.append("No state machine"); } return sb.toString(); } + public int attributeNb() { + return attributes.size(); + } + + public AvatarAttribute getAttribute(int _index) { + return attributes.get(_index); + } + + + public AvatarAttribute getAvatarAttributeWithName(String _name) { + for(AvatarAttribute attribute: attributes) { + if (attribute.getName().compareTo(_name)== 0) { + return attribute; + } + } + return null; + } + + public AvatarMethod getAvatarMethodWithName(String _name) { + for(AvatarMethod method: methods) { + if (method.getName().compareTo(_name)== 0) { + return method; + } + } + + if (getFather() != null) { + return getFather().getAvatarMethodWithName(_name); + } + + return null; + } + public AvatarSignal getAvatarSignalWithName(String _name) { for(AvatarSignal signal: signals) { if (signal.getName().compareTo(_name)== 0) { @@ -112,9 +156,55 @@ public class AvatarBlock extends AvatarElement { } } + if (getFather() != null) { + return getFather().getAvatarSignalWithName(_name); + } + return null; } + public boolean isAValidMethodCall(String _s) { + int index0 = _s.indexOf("("); + int index1 = _s.indexOf(")"); + if ((index0 == -1) || (index1 == -1) || (index1 < index0)) { + return false; + } + + String method = _s.substring(0, index0); + TraceManager.addDev("method=" + method); + AvatarMethod am = getAvatarMethodWithName(method); + if (am == null) { + return false; + } + + String params = _s.substring(index0+1, index1).trim(); + TraceManager.addDev("params=" + params); + if (params.length() == 0) { + if (am.getListOfAttributes().size() == 0) { + return true; + } else { + return false; + } + } + TraceManager.addDev("params=" + params); + String [] actions = params.split(","); + if (am.getListOfAttributes().size() != actions.length) { + return false; + } + + AvatarAttribute aa; + for(int i=0; i<actions.length; i++) { + TraceManager.addDev("params=" + params + "actions=" + actions[i]); + aa = getAvatarAttributeWithName(actions[i]); + if (aa == null) { + return false; + } + } + + return true; + + } + } \ No newline at end of file diff --git a/src/avatartranslator/AvatarSpecification.java b/src/avatartranslator/AvatarSpecification.java index 77dac9ee4467a243551a4d7044c887be6bdbc682..7a7c310dfc31cc3422852062fd412d23a5c49fa6 100644 --- a/src/avatartranslator/AvatarSpecification.java +++ b/src/avatartranslator/AvatarSpecification.java @@ -52,6 +52,7 @@ import java.util.*; import myutil.*; public class AvatarSpecification extends AvatarElement { + private String[] ops = {">", "<", "+", "-", "*", "/", "[", "]", "(", ")", ":", "=", "==", ",", "!", "?", "{", "}"}; private LinkedList<AvatarBlock> blocks; private LinkedList<AvatarRelation> relations; @@ -78,7 +79,7 @@ public class AvatarSpecification extends AvatarElement { public String toString() { StringBuffer sb = new StringBuffer("Blocks:\n"); for(AvatarBlock block: blocks) { - sb.append(block.toString()); + sb.append("*** " + block.toString()+"\n"); } sb.append("\nRelations:\n"); for(AvatarRelation relation: relations) { @@ -98,4 +99,15 @@ public class AvatarSpecification extends AvatarElement { return null; } + + public String putAttributeValueInString(String _source, AvatarAttribute _at) { + return Conversion.putVariableValueInString(ops, _source, _at.getName(), _at.getDefaultInitialValue()); + } + + + public void removeCompositeStates() { + for(AvatarBlock block: blocks) { + block.getStateMachine().removeCompositeStates(); + } + } } \ No newline at end of file diff --git a/src/avatartranslator/AvatarState.java b/src/avatartranslator/AvatarState.java index d0814f69d44825b3dca47999977c990c292d26de..d33f5cf8a46807e84e19cc463d2192a821089e70 100644 --- a/src/avatartranslator/AvatarState.java +++ b/src/avatartranslator/AvatarState.java @@ -50,25 +50,8 @@ import java.util.*; public class AvatarState extends AvatarStateMachineElement { - private AvatarStateMachine asm; - - - public AvatarState(String _name, Object _referenceObject) { super(_name, _referenceObject); } - - public void setStateMachine(AvatarStateMAchine _asm) { - asm = _asm; - } - - public boolean isACompositeState() { - return (asm != null); - } - - public AvatarStateMachine getStateMachine() { - return asm; - } - } \ No newline at end of file diff --git a/src/avatartranslator/AvatarStateMachine.java b/src/avatartranslator/AvatarStateMachine.java index 59627fd2b1b55451cf7e1395a38aaa8243d6ddcf..a89b1f1eed66f071ff2182a5960da4e6f9d3752e 100644 --- a/src/avatartranslator/AvatarStateMachine.java +++ b/src/avatartranslator/AvatarStateMachine.java @@ -73,6 +73,105 @@ public class AvatarStateMachine extends AvatarElement { public LinkedList<AvatarStateMachineElement> getListOfElements() { return elements; } + + public String toString() { + StringBuffer sb = new StringBuffer("State machine Id=" + getID() + "\n"); + + for(AvatarStateMachineElement element: elements) { + sb.append(element.toString() + "\n"); + } + + return sb.toString(); + } + + public void removeCompositeStates() { + AvatarTransition at; + + at = getCompositeTransition(); + if (at != null) { + TraceManager.addDev("*** Found composite transition: " + at.toString()); + } + + /*while((at = getCompositeTransition()) != null) { + removeCompositeTransition(at); + }*/ + } + + private AvatarTransition getCompositeTransition() { + for(AvatarStateMachineElement element: elements) { + if (element instanceof AvatarTransition) { + if ((isACompositeTransition((AvatarTransition)element))) { + return (AvatarTransition)element; + } + } + } + + return null; + } + + // Checks whether the previous element is a state with an internal state machine + private boolean isACompositeTransition(AvatarTransition _at) { + AvatarStateMachineElement element = getPreviousElementOf(_at); + if (element == null) { + return false; + } + + if (!(element instanceof AvatarState)) { + return false; + } + + AvatarState state = (AvatarState)element; + return hasInternalComponents(state); + } + + private boolean hasInternalComponents(AvatarState _state) { + for(AvatarStateMachineElement element: elements) { + if (element.getState() == _state) { + return true; + } + } + + return false; + } + + private void removeCompositeTransition(AvatarTransition _at) { + AvatarState state = (AvatarState)(getPreviousElementOf(_at)); + for(AvatarStateMachineElement element: elements) { + if (element.hasInUpperState(state) == true) { + // We found a candidate! + } + } + // For each element elt in the composite state at the origin of at: + // make a new transition from elt to the destinaton of _at + // Si elt un peu special, need to add also intermediate states + // add this transition + + // Remove the old transition + + // Shall work! + + } + + private AvatarStateMachineElement getPreviousElementOf(AvatarStateMachineElement _elt) { + for(AvatarStateMachineElement element: elements) { + if (element.hasNext(_elt)) { + return element; + } + } + + return null; + } + + public AvatarState getStateWithName(String _name) { + for(AvatarStateMachineElement element: elements) { + if (element instanceof AvatarState) { + if (element.getName().compareTo(_name) == 0) { + return (AvatarState)element; + } + } + } + return null; + } } \ No newline at end of file diff --git a/src/avatartranslator/AvatarStateMachineElement.java b/src/avatartranslator/AvatarStateMachineElement.java index 2abd801376726fdf549e43e7f971900ccfa180e2..8b13068f0adf1921da205883ceac2e80e7f36249 100644 --- a/src/avatartranslator/AvatarStateMachineElement.java +++ b/src/avatartranslator/AvatarStateMachineElement.java @@ -51,6 +51,7 @@ import java.util.*; public class AvatarStateMachineElement extends AvatarElement { private LinkedList<AvatarStateMachineElement> nexts; + private AvatarState myState; public AvatarStateMachineElement(String _name, Object _referenceObject) { super(_name, _referenceObject); @@ -61,5 +62,46 @@ public class AvatarStateMachineElement extends AvatarElement { nexts.add(_element); } + public void setState(AvatarState _as) { + myState = _as; + } + + public AvatarState getState() { + return myState; + } + + public boolean hasInUpperState(AvatarState _as) { + if (getState() == _as) { + return true; + } + + if (getState() != null) { + return getState().hasInUpperState(_as); + } + + return false; + } + + public String toString() { + String ret = getName() + " ID=" + getID(); + if (myState == null) { + ret += " / top level operator\n"; + } else { + ret += " / in state " + myState.getName() + " ID=" + myState.getID() + "\n"; + } + + ret += "nexts= "; + int cpt=0; + for(AvatarStateMachineElement element: nexts) { + ret += cpt + ":" + element.getName() + "/ ID=" + element.getID() + " "; + cpt ++; + } + return ret; + } + + public boolean hasNext(AvatarStateMachineElement _elt) { + return nexts.contains(_elt); + } + } \ No newline at end of file diff --git a/src/avatartranslator/AvatarSyntaxChecker.java b/src/avatartranslator/AvatarSyntaxChecker.java new file mode 100644 index 0000000000000000000000000000000000000000..3235a7facaecb75cde3f27b726af80e9e6f648f2 --- /dev/null +++ b/src/avatartranslator/AvatarSyntaxChecker.java @@ -0,0 +1,179 @@ +/**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 AvatarSyntaxChecker + * Creation: 21/05/2010 + * @version 1.0 21/05/2010 + * @author Ludovic APVRILLE + * @see + */ + +package avatartranslator; + +import java.io.*; +import java.util.*; + +import compiler.tmlparser.*; +import myutil.*; + + +public class AvatarSyntaxChecker { + + + public AvatarSyntaxChecker() { + } + + public static int isAValidGuard(AvatarSpecification _as, AvatarBlock _ab, String _guard) { + String tmp = _guard.replaceAll(" ", "").trim(); + if (tmp.compareTo("[]") == 0) { + return 0; + } + return parse(_as, _ab, "guard", _guard); + } + + public static int isAValidIntExpr(AvatarSpecification _as, AvatarBlock _ab, String _expr) { + if (_expr.trim().length() == 0) { + return 0; + } + return parse(_as, _ab, "actionnat", _expr); + } + + public static int isAValidVariableExpr(AvatarSpecification _as, AvatarBlock _ab, String _expr) { + int index0 = _expr.indexOf("="); + if (index0 == -1) { + return -1; + } + + String attributeName = _expr.substring(0, index0).trim(); + AvatarAttribute aa = _ab.getAvatarAttributeWithName(attributeName); + if (aa == null) { + return -1; + } + + String action = _expr.substring(index0 + 1, _expr.length()).trim(); + + if (aa.isInt() || aa.isNat()) { + return parse(_as, _ab, "actionnat", action); + } else if (aa.isBool()) { + return parse(_as, _ab, "actionbool", action); + } + return -1; + } + + /** + * Parsing in two steps: + * 1. Parsing the expression with no variable checking + * 2. Parsing the expression with variables values to see whether variables are well-placed or not + * The second parsing is performed iff the first one succeeds + * return -1 in case of error in first pass + * return -2 in case of error in second pass + * return -3 in case a variable has not been declared + */ + public static int parse(AvatarSpecification _as, AvatarBlock _ab, String _parseCmd, String _action) { + TMLExprParser parser; + SimpleNode root; + int i; + + // First parsing + parser = new TMLExprParser(new StringReader(_parseCmd + " " + _action)); + try { + //System.out.println("\nParsing :" + parseCmd + " " + action); + root = parser.CompilationUnit(); + //root.dump("pref="); + //System.out.println("Parse ok"); + } catch (ParseException e) { + TraceManager.addDev("\nAvatar Parsing :" + _parseCmd + " " + _action); + TraceManager.addDev("ParseException --------> Parse error in :" + _parseCmd + " " + _action); + return -1; + } catch (TokenMgrError tke) { + TraceManager.addDev("Avatar TokenMgrError --------> Parse error in :" + _parseCmd + " " + _action); + return -1; + } + + // Second parsing + // We only replace variables values after the "=" sign + int index = _action.indexOf('='); + String modif = _action; + + if (_parseCmd.startsWith("ass")) { + if (index != -1) { + modif = _action.substring(index+1, _action.length()); + } + + _parseCmd = "action" + _parseCmd.substring(3, _parseCmd.length()); + } + + for(i=0; i<_ab.attributeNb(); i++) { + modif = _as.putAttributeValueInString(modif, _ab.getAttribute(i)); + } + + parser = new TMLExprParser(new StringReader(_parseCmd + " " + modif)); + try { + //System.out.println("\nParsing :" + parseCmd + " " + modif); + root = parser.CompilationUnit(); + //root.dump("pref="); + //System.out.println("Parse ok"); + } catch (ParseException e) { + TraceManager.addDev("\nAvatar Parsing :" + _parseCmd + " " + modif); + TraceManager.addDev("\nn(Original parsing :" + _parseCmd + " " + _action); + TraceManager.addDev("ParseException --------> Parse error in :" + _parseCmd + " " + _action); + return -2; + } catch (TokenMgrError tke ) { + TraceManager.addDev("\nnAvatar Parsing :" + _parseCmd + " " + modif); + TraceManager.addDev("TokenMgrError --------> Parse error in :" + _parseCmd + " " + _action); + return -2; + } + + // Tree analysis: if the tree contains a variable, then, this variable has not been declared + ArrayList<String> vars = root.getVariables(); + for(String s: vars) { + // is that string a variable? + if ((s.compareTo("true") != 0) && (s.compareTo("false") != 0) && (s.compareTo("nil") != 0)) { + TraceManager.addDev("Variable not declared: " +s); + return -3; + } + } + + return 0; + + } + + + + +} \ No newline at end of file diff --git a/src/avatartranslator/AvatarTransition.java b/src/avatartranslator/AvatarTransition.java index 155b31004ffd6860b37f4664b871eda43461fe9a..beb960052175ee60d15133b2d2754b122dd482ec 100644 --- a/src/avatartranslator/AvatarTransition.java +++ b/src/avatartranslator/AvatarTransition.java @@ -55,7 +55,7 @@ public class AvatarTransition extends AvatarStateMachineElement { private LinkedList<String> actions; // actions on variable, or method call - public AvatarTransition(String _name, AvatarSignal _signal, Object _referenceObject) { + public AvatarTransition(String _name, Object _referenceObject) { super(_name, _referenceObject); actions = new LinkedList<String>(); } @@ -73,7 +73,11 @@ public class AvatarTransition extends AvatarStateMachineElement { } public String getAction(int _index) { - return value.get(_index); + return actions.get(_index); + } + + public void addAction(String _action) { + actions.add(_action); } public void setDelays(String _minDelay, String _maxDelay) { @@ -101,5 +105,20 @@ public class AvatarTransition extends AvatarStateMachineElement { public String getMaxCompute() { return maxCompute; } + + public AvatarTransition cloneMe() { + AvatarTransition at = new AvatarTransition(getName(), getReferenceObject()); + at.setGuard(getGuard()); + at.setDelays(getMinDelay(), getMaxDelay()); + at.setComputes(getMinCompute(), getMaxCompute()); + + for(int i=0; i<getNbOfAction(); i++) { + at.addAction(getAction(i)); + } + + return at; + } + + } \ No newline at end of file diff --git a/src/avatartranslator/AvatarType.java b/src/avatartranslator/AvatarType.java index 731f61b09a9c2d8eee39acebe5ecd92af0896eb1..a0a489ea9a52deaf9b3da4133962d3737e3f883c 100644 --- a/src/avatartranslator/AvatarType.java +++ b/src/avatartranslator/AvatarType.java @@ -70,8 +70,8 @@ public class AvatarType { return -1; } - public static String getStringType(int type) { - switch(type) { + public static String getStringType(int _type) { + switch(_type) { case NATURAL: return "nat"; case BOOLEAN: @@ -81,4 +81,16 @@ public class AvatarType { } return ""; } + + public static String getDefaultInitialValue(int _type) { + switch(_type) { + case NATURAL: + return "0"; + case BOOLEAN: + return "false"; + case INTEGER: + return "0"; + } + return ""; + } } \ No newline at end of file diff --git a/src/avatartranslator/toturtle/AVATAR2TURTLE.java b/src/avatartranslator/toturtle/AVATAR2TURTLE.java new file mode 100644 index 0000000000000000000000000000000000000000..9a4597315c7a00f435ffb418f677e55a0f343806 --- /dev/null +++ b/src/avatartranslator/toturtle/AVATAR2TURTLE.java @@ -0,0 +1,1210 @@ +/**Copyright or 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 AVATAR2TURTLE +* Creation: 21/05/2010 +* @version 1.0 21/05/2010 +* @author Ludovic APVRILLE +* @see +*/ + +package avatartranslator.toturtle; + +import java.util.*; + +import avatartranslator.*; +import myutil.*; +import translator.*; +import ui.*; + + +public class AVATAR2TURTLE { + + //private static int gateId; + + private AvatarSpecification spec; + private TURTLEModeling tm; + private Vector checkingErrors; + + + public AVATAR2TURTLE(AvatarSpecification _spec) { + spec = _spec; + } + + public Vector getCheckingErrors() { + return checkingErrors; + } + + + public TURTLEModeling generateTURTLEModeling() { + //System.out.println("generate TM"); + //tmlmodeling.removeAllRandomSequences(); + spec.removeCompositeStates(); + + tm = new TURTLEModeling(); + checkingErrors = new Vector(); + + // Create TClasses -> same name as TML tasks + //nbClass = 0; + //System.out.println("Tclasses"); + createTClasses(); + //System.out.println("Channels"); + /*createChannelTClasses(); + //System.out.println("Events"); + createEventTClasses(); + //System.out.println("Requests"); + createRequestTClasses(); + //System.out.println("AD of tclasses"); + createADOfTClasses(); + //System.out.println("All done");*/ + + return tm; + } + + private void createTClasses() { + TClass tc; + for(AvatarBlock block: spec.getListOfBlocks()) { + if (block.getFather() == null) { + tc = new TClass(block.getName(), true); + tm.addTClass(tc); + ActivityDiagram ad = new ActivityDiagram(); + tc.setActivityDiagram(ad); + } + } + //makeAttributes(task, tcl); + } + + /*private void createChannelTClasses() { + ListIterator iterator = tmlmodeling.getListIteratorChannels(); + TMLChannel channel; + TClassChannelBRNBW tch1; + TClassChannelNBRNBW tch2; + TClassChannelBRBW tch3; + String name; + + while(iterator.hasNext()) { + channel = (TMLChannel)(iterator.next()); + name = getChannelString(channel); + switch(channel.getType()) { + case TMLChannel.BRNBW: + tch1 = new TClassChannelBRNBW(name, channel.getName()); + tch1.makeTClass(); + tm.addTClass(tch1); + break; + case TMLChannel.BRBW: + tch3 = new TClassChannelBRBW(name, channel.getName()); + tch3.makeTClass(channel.getMax()); + tm.addTClass(tch3); + break; + default: + tch2 = new TClassChannelNBRNBW(name, channel.getName()); + tch2.makeTClass(); + tm.addTClass(tch2); + } + } + } + + private String getChannelString(TMLChannel channel) { + String name; + switch(channel.getType()) { + case TMLChannel.BRNBW: + name = nameChannelBRNBW + channel.getName(); + break; + default: + name = nameChannelNBRNBW + channel.getName(); + } + return name; + } + + private void createEventTClasses() { + ListIterator iterator = tmlmodeling.getListIteratorEvents(); + TMLEvent event; + TClassEventInfinite tce; + TClassEventFinite tcef; + TClassEventFiniteBlocking tcefb; + + while(iterator.hasNext()) { + event = (TMLEvent)(iterator.next()); + if (event.isInfinite()) { + tce = new TClassEventInfinite(nameEvent + event.getName(), event.getName(), event.getNbOfParams()); + tce.addWriteGate(); + tce.addReadGate(); + //if (event.canBeNotified()) { + tce.addSizeGate(); + //} + tce.makeTClass(); + tm.addTClass(tce); + } else { + if (event.isBlocking()) { + tcefb = new TClassEventFiniteBlocking(nameEvent + event.getName(), event.getName(), event.getNbOfParams(), event.getMaxSize()); + tcefb.addWriteGate(); + tcefb.addReadGate(); + //if (event.canBeNotified()) { + tcefb.addSizeGate(); + //} + tcefb.makeTClass(); + tm.addTClass(tcefb); + } else { + tcef = new TClassEventFinite(nameEvent + event.getName(), event.getName(), event.getNbOfParams(), event.getMaxSize()); + tcef.addWriteGate(); + tcef.addReadGate(); + //if (event.canBeNotified()) { + tcef.addSizeGate(); + //} + tcef.makeTClass(); + tm.addTClass(tcef); + } + } + } + } + + private void createRequestTClasses() { + ListIterator iterator = tmlmodeling.getListIteratorRequests(); + TMLRequest request; + TClassRequest tcr; + ListIterator ite; + TMLTask task; + + while(iterator.hasNext()) { + request = (TMLRequest)(iterator.next()); + tcr = new TClassRequest(nameRequest + request.getName(), request.getName(), request.getNbOfParams()); + ite = request.getOriginTasks().listIterator(); + while(ite.hasNext()) { + task = (TMLTask)(ite.next()); + tcr.addWriteGate(task.getName()); + } + tcr.addReadGate(); // Assume that request is going to only one class + tcr.makeTClass(); + tm.addTClass(tcr); + } + } + + private void createADOfTClasses() { + TClass t; + + for(int i=0; i<nbClass; i++) { + t = tm.getTClassAtIndex(i); + //System.out.println("Create AD"); + createADOfTClass(t, (TMLTask)(tmlmodeling.getTasks().get(i))); + //System.out.println("End create AD"); + } + } + + private void createADOfTClass(TClass tclass, TMLTask task) { + // For each element, make a translation + Vector newElements = new Vector(); // elements of AD + Vector baseElements = new Vector(); // elements of basic task + + //System.out.println("Making AD of " + tclass.getName()); + translateAD(newElements, baseElements, tclass, task, task.getActivityDiagram().getFirst(), null, null); + + // DANGER: if task may be requested, the AD must be modified!!!! + //System.out.println("task requested?"); + if (task.isRequested()) { + setADRequested(tclass, task); + } + //System.out.println("end task requested?"); + + setGatesToTask(tclass, task); + } + + + private ADComponent translateAD(Vector newElements, Vector baseElements, TClass tclass, TMLTask task, TMLActivityElement tmle, ADComponent previous, ADJunction adjunc) { + //ADEmpty empty; + ADActionStateWithParam adacparam, adacparam1, adacparam2, adacparam3, adacparam4; + ADChoice adchoice; + ADDelay addelay; + ADTimeInterval adinterval; + ADJunction adj, adj1, adj2; + ADActionStateWithGate adag, adagtmp; + //ADStop adstop; + //ADSequence adseq; + + + Gate g, g1; + + TMLChoice tmlchoice; + TMLForLoop tmlforloop; + TMLActivityElementChannel acch; + TMLActivityElementEvent acevt; + TMLSendRequest tmlreq; + TMLSequence tmlseq; + TMLSelectEvt tmlselectevt; + TMLRandom tmlrandom; + + ADComponent adc, adc1, adc2; + + String action, tmp; + //String param; + Param parameter, parameter0, parameter1, parameter2; + + int i; + //int j, k; + + // Translate AD components + + // START STATE + + //System.out.println("Call to TMLE=" + tmle.toString()); + try { + + if (tmle instanceof TMLStartState) { + adc = tclass.getActivityDiagram().getStartState(); + baseElements.add(tmle); + newElements.add(adc); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adc, adjunc); + adc.addNext(adc1); + return adc; + + // STOP State + } else if (tmle instanceof TMLStopState) { + return endOfActivity(newElements, baseElements, tclass, adjunc); + + // TML Junction + } else if (tmle instanceof TMLJunction) { + return translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), previous, adjunc); + + // EXECIInterval + } else if (tmle instanceof TMLActionState) { + action = ((TMLActionState)tmle).getAction(); + // Eliminate cout << + if (printAnalyzer(action)) { + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), previous, adjunc); + return adc1; + } else { + action = modifyString(action); + action = removeLastSemicolon(action); + parameter = null; + if ((parameter = paramAnalyzer(action, tclass)) != null) { + adacparam = new ADActionStateWithParam(parameter); + adacparam.setActionValue(getActionValueParam(action, tclass)); + newElements.add(adacparam); + baseElements.add(tmle); + tclass.getActivityDiagram().add(adacparam); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adacparam, adjunc); + adacparam.addNext(adc1); + return adacparam; + } else { + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), previous, adjunc); + return adc1; + } + } + + // CHOICE + } else if (tmle instanceof TMLChoice) { + //System.out.println("TML Choice!"); + tmlchoice = (TMLChoice)tmle; + adchoice = new ADChoice(); + newElements.add(adchoice); + baseElements.add(tmle); + tclass.getActivityDiagram().add(adchoice); + + //System.out.println("Get guards nb=" + tmlchoice.getNbGuard()); + //String guard = ""; + + if (tmlchoice.getNbGuard() !=0 ) { + int index1 = tmlchoice.getElseGuard(), index2 = tmlchoice.getAfterGuard(); + if (index2 != -1) { + //System.out.println("Managing after"); + adj = new ADJunction(); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(index2), adchoice, adj); + tclass.getActivityDiagram().add(adj); + } else { + adj = adjunc; + } + + for(i=0; i<tmlchoice.getNbGuard(); i++) { + //System.out.println("Get guards i=" + i); + //System.out.println("ADjunc=" + adjunc); + if (i==index1) { + action = modifyString(tmlchoice.getValueOfElse()); + } else { + if (tmlchoice.isStochasticGuard(i)) { + action = "[ ]"; + } else { + action = modifyString(tmlchoice.getGuard(i)); + } + + } + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(i), adchoice, adj); + if (adc1 == null) { + //System.out.println("Null adc1"); + } else { + //System.out.println("adc1 = " +adc1); + } + g = tclass.addNewGateIfApplicable("branching"); + adag = new ADActionStateWithGate(g); + adag.setActionValue(""); + adag.addNext(adc1); + tclass.getActivityDiagram().add(adag); + adchoice.addGuard(action); + adchoice.addNext(adag); + } + //System.out.println("Return adchoice ..."); + return adchoice; + } else { + return endOfActivity(newElements, baseElements, tclass, adjunc); + } + + } else if (tmle instanceof TMLSelectEvt) { + tmlselectevt = (TMLSelectEvt)(tmle); + adchoice = new ADChoice(); + newElements.add(adchoice); + baseElements.add(tmle); + tclass.getActivityDiagram().add(adchoice); + for(i=0; i<tmlselectevt.getNbNext(); i++) { + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(i), adchoice, adjunc); + adchoice.addNext(adc1); + adchoice.addGuard("[]"); + } + return adchoice; + + // EXECI + } else if (tmle instanceof TMLExecI) { + addelay = new ADDelay(); + newElements.add(addelay); + baseElements.add(tmle); + tclass.getActivityDiagram().add(addelay); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), addelay, adjunc); + addelay.setValue(modifyString(((TMLExecI)tmle).getAction())); + addelay.addNext(adc1); + return addelay; + + // EXECIInterval + } else if (tmle instanceof TMLExecIInterval) { + adinterval = new ADTimeInterval(); + newElements.add(adinterval); + baseElements.add(tmle); + tclass.getActivityDiagram().add(adinterval); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adinterval, adjunc); + adinterval.setValue(modifyString(((TMLExecIInterval)tmle).getMinDelay()), modifyString(((TMLExecIInterval)tmle).getMaxDelay())); + adinterval.addNext(adc1); + return adinterval; + + // EXECC + } else if (tmle instanceof TMLExecC) { + addelay = new ADDelay(); + newElements.add(addelay); + baseElements.add(tmle); + tclass.getActivityDiagram().add(addelay); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), addelay, adjunc); + addelay.setValue(modifyString(((TMLExecC)tmle).getAction())); + addelay.addNext(adc1); + return addelay; + + // EXECCInterval + } else if (tmle instanceof TMLExecCInterval) { + adinterval = new ADTimeInterval(); + newElements.add(adinterval); + baseElements.add(tmle); + tclass.getActivityDiagram().add(adinterval); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adinterval, adjunc); + adinterval.setValue(modifyString(((TMLExecCInterval)tmle).getMinDelay()), modifyString(((TMLExecCInterval)tmle).getMaxDelay())); + adinterval.addNext(adc1); + return adinterval; + + // DELAY + } else if (tmle instanceof TMLDelay) { + adinterval = new ADTimeInterval(); + newElements.add(adinterval); + baseElements.add(tmle); + tclass.getActivityDiagram().add(adinterval); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adinterval, adjunc); + adinterval.setValue(modifyString(((TMLDelay)tmle).getMinDelay()), modifyString(((TMLDelay)tmle).getMaxDelay())); + adinterval.addNext(adc1); + return adinterval; + + // TMLRandom + } else if (tmle instanceof TMLRandom) { + tmlrandom = (TMLRandom)tmle; + + parameter0 = tclass.addNewParamIfApplicable("min__random", Param.NAT, "0"); + parameter1 = tclass.addNewParamIfApplicable("max__random", Param.NAT, "0"); + parameter2 = tclass.addNewParamIfApplicable(tmlrandom.getVariable(), Param.NAT, "0"); + + adacparam1 = new ADActionStateWithParam(parameter0); + action = modifyString("min(" + tmlrandom.getMinValue() + ", " + tmlrandom.getMaxValue() + ")"); + adacparam1.setActionValue(action); + newElements.add(adacparam1); + baseElements.add(tmle); + + adacparam2 = new ADActionStateWithParam(parameter1); + action = modifyString("max(" + tmlrandom.getMinValue() + ", " + tmlrandom.getMaxValue() + ")"); + adacparam2.setActionValue(action); + + adacparam3 = new ADActionStateWithParam(parameter2); + action = modifyString("min__random"); + adacparam3.setActionValue(action); + + adacparam4 = new ADActionStateWithParam(parameter0); + action = modifyString("min__random + 1"); + adacparam4.setActionValue(action); + + tclass.getActivityDiagram().add(adacparam1); + + adacparam1.addNext(adacparam2); + + adj1 = new ADJunction(); + adacparam2.addNext(adj1); + + adchoice = new ADChoice(); + adj1.addNext(adchoice); + adchoice.addGuard("[min__random < (max__random + 1)]"); + adchoice.addNext(adacparam3); + adchoice.addGuard("[min__random < max__random]"); + adchoice.addNext(adacparam4); + adacparam4.addNext(adj1); + + tclass.getActivityDiagram().add(adacparam1); + tclass.getActivityDiagram().add(adacparam2); + tclass.getActivityDiagram().add(adacparam3); + tclass.getActivityDiagram().add(adacparam4); + tclass.getActivityDiagram().add(adj1); + tclass.getActivityDiagram().add(adchoice); + + adc2 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adacparam3, adjunc); + adacparam3.addNext(adc2); + + return adacparam1; + + // TMLFORLOOP + } else if (tmle instanceof TMLForLoop) { + tmlforloop = (TMLForLoop)tmle; + action = modifyString(tmlforloop.getInit()); + //System.out.println("FOR action = " + action); + parameter = null; + if ((action.length() == 0) || ((parameter = paramAnalyzer(action, tclass)) != null)) { + //System.out.println("parameter1 ok"); + if (action.length() != 0) { + adacparam1 = new ADActionStateWithParam(parameter); + adacparam1.setActionValue(getActionValueParam(action, tclass)); + } else { + adacparam1 = null; + } + + action = modifyString(tmlforloop.getIncrement()); + parameter = null; + if ((action.length() == 0) || ((parameter = paramAnalyzer(action, tclass)) != null)) { + //System.out.println("New loop"); + if (action.length() != 0) { + adacparam2 = new ADActionStateWithParam(parameter); + adacparam2.setActionValue(getActionValueParam(action, tclass)); + } else { + adacparam2 = null; + } + + adchoice = new ADChoice(); + adj1 = new ADJunction(); + adj2 = new ADJunction(); + + newElements.add(adacparam1); + baseElements.add(tmle); + + if (adacparam1 != null) { + tclass.getActivityDiagram().add(adacparam1); + newElements.add(adacparam1); + } else { + newElements.add(adj1); + } + if (adacparam2 != null) { + tclass.getActivityDiagram().add(adacparam2); + } + tclass.getActivityDiagram().add(adchoice); + tclass.getActivityDiagram().add(adj1); + tclass.getActivityDiagram().add(adj2); + + if (adacparam1 != null) { + adacparam1.addNext(adj1); + } + adj1.addNext(adchoice); + if (adacparam2 != null) { + adacparam2.addNext(adj1); + adj2.addNext(adacparam2); + } else { + adj2.addNext(adj1); + } + + action = (modifyString(tmlforloop.getCondition())); + if (action.length() == 0) { + action = "true"; + } + adchoice.addGuard("[" + action + "]"); + if (adacparam1 != null) { + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adacparam1, adj2); + } else { + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adj1, adj2); + } + adchoice.addNext(adc1); + + action = Conversion.replaceAllChar(action, '[', "("); + action = Conversion.replaceAllChar(action, ']', ")"); + adchoice.addGuard("[not(" + action + ")]"); + if (adacparam1 != null) { + adc2 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(1), adacparam1, adjunc); + } else { + adc2 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(1), adj1, adjunc); + } + adchoice.addNext(adc2); + + if (adacparam1 != null) { + return adacparam1; + } else { + return adj1; + } + } + } + // Error! -> bad parameter + //return translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), previous, adjunc); + CheckingError error = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Parameter undeclared in For operator:" + action); + error.setTClass(tclass); + checkingErrors.add(error); + + // TML Sequence + } else if (tmle instanceof TMLSequence) { + //System.out.println("TML sequence !"); + tmlseq = (TMLSequence)tmle; + + if (tmlseq.getNbNext() == 0) { + return endOfActivity(newElements, baseElements, tclass, adjunc); + } + + + if (tmlseq.getNbNext() == 1) { + return translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), previous, adjunc); + } + + tmlseq.sortNexts(); + // At least 2 next elements + adj2 = null; + adc2 = null; + for(i=1; i<tmlseq.getNbNext(); i++) { + adj1 = new ADJunction(); + if (adj2 == null) { + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(i-1), previous, adj1); + } else { + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(i-1), adj2, adj1); + } + if (adj2 == null) { + adc2 = adc1; + //newElements.add(adc1); + //baseElements.add(tmle); + } else { + adj2.addNext(adc1); + } + //tclass.getActivityDiagram().add(adc1); + tclass.getActivityDiagram().add(adj1); + adj2 = adj1; + } + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(tmlseq.getNbNext()-1), previous, adjunc); + //tclass.getActivityDiagram().add(adc1); + adj2.addNext(adc1); + return adc2; + + // TML Read Channel + } else if (tmle instanceof TMLReadChannel) { // READ MUST BE MODIFIED + acch = (TMLActivityElementChannel)tmle; + + if ((acch.getNbOfSamples().trim().compareTo("1")) == 0) { + g = addGateChannel("rd", acch, 0, tclass); + TClass tcl = tm.getTClassWithName(getChannelString(acch.getChannel(0))); + g1 = tcl.getGateByName("rd__" + acch.getChannel(0).getName()); + tm.addSynchroRelation(tclass, g, tcl, g1); + adag = new ADActionStateWithGate(g); + adag.setActionValue(""); + tclass.getActivityDiagram().add(adag); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adag, adjunc); + adag.addNext(adc1); + newElements.add(adag); + baseElements.add(tmle); + return adag; + + } else { + parameter = tclass.addNewParamIfApplicable("cpt__0", "nat", "0"); + adacparam = new ADActionStateWithParam(parameter); + adacparam.setActionValue(acch.getNbOfSamples()); + tclass.getActivityDiagram().add(adacparam); + + adj = new ADJunction(); + tclass.getActivityDiagram().add(adj); + adacparam.addNext(adj); + + adchoice = new ADChoice(); + tclass.getActivityDiagram().add(adchoice); + adj.addNext(adchoice); + + adacparam1 = new ADActionStateWithParam(parameter); + adacparam1.setActionValue("cpt__0 - 1"); + tclass.getActivityDiagram().add(adacparam1); + adacparam1.addNext(adj); + + g = addGateChannel("rd", acch, 0, tclass); + TClass tcl = tm.getTClassWithName(getChannelString(acch.getChannel(0))); + g1 = tcl.getGateByName("rd__" + acch.getChannel(0).getName()); + tm.addSynchroRelation(tclass, g, tcl, g1); + + adag = new ADActionStateWithGate(g); + adag.setActionValue(""); + tclass.getActivityDiagram().add(adag); + adag.addNext(adacparam1); + + adchoice.addNext(adag); + adchoice.addGuard("[cpt__0 > 0]"); + + newElements.add(adacparam); + baseElements.add(tmle); + + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adacparam, adjunc); + adchoice.addNext(adc1); + adchoice.addGuard("[cpt__0 == 0]"); + return adacparam; + } + + // TMLSendEvent + } else if (tmle instanceof TMLSendEvent) { + acevt = (TMLActivityElementEvent)tmle; + g = tclass.addNewGateIfApplicable("notify__" + acevt.getEvent().getName()); + TClass tcl = tm.getTClassWithName(nameEvent + acevt.getEvent().getName()); + g1 = ((TClassEventCommon)(tcl)).getGateWrite(); + tm.addSynchroRelation(tclass, g, tcl, g1); + + adacparam2 = null; + adacparam = null; + adag = new ADActionStateWithGate(g); + action = ""; + for (i=0; i<acevt.getNbOfParams(); i++) { + if (acevt.getParam(i).length() > 0) { + if (!Conversion.isNumeralOrId(acevt.getParam(i))) { + tmp = "ntmp__" + i; + if (acevt.getEvent().getType(i).getType() == TMLType.NATURAL) { + parameter = tclass.addNewParamIfApplicable(tmp, Param.NAT, "0"); + } else { + parameter = tclass.addNewParamIfApplicable(tmp, Param.BOOL, "false"); + } + + adacparam1 = new ADActionStateWithParam(parameter); + adacparam1.setActionValue(modifyString(acevt.getParam(i))); + tclass.getActivityDiagram().add(adacparam1); + if (adacparam == null) { + adacparam2 = adacparam1; + adacparam = adacparam1; + } else { + adacparam.addNext(adacparam1); + adacparam = adacparam1; + } + } else { + tmp = modifyString(acevt.getParam(i)); + } + action += "!" + modifyString(tmp); + } + } + if (adacparam != null) { + adacparam.addNext(adag); + } + adag.setActionValue(action); + + baseElements.add(tmle); + tclass.getActivityDiagram().add(adag); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adag, adjunc); + adag.addNext(adc1); + + if (adacparam2 != null) { + newElements.add(adacparam2); + return adacparam2; + } + newElements.add(adag); + return adag; + + // TMLSendRequest + } else if (tmle instanceof TMLSendRequest) { + tmlreq = (TMLSendRequest)tmle; + g = tclass.addNewGateIfApplicable("sendReq__" + tmlreq.getRequest().getName() + "__" + task.getName()); + TClass tcl = tm.getTClassWithName(nameRequest + tmlreq.getRequest().getName()); + //g1 = tcl.getGateByName("sendReq"); + //int index = tmlreq.getRequest().getOriginTasks().indexOf(task); + //System.out.println("task=" + task.getName() + " index=" + index); + //g1 = (Gate)(((TClassRequest)tcl).getGatesWrite().get(index)); + g1 = (Gate)(((TClassRequest)tcl).getGateWrite(task.getName())); + //System.out.println("task=" + task.getName() + " index=" + index + "gate=" + g.getName()); + tm.addSynchroRelation(tclass, g, tcl, g1); + + adacparam2 = null; + adacparam = null; + adag = new ADActionStateWithGate(g); + action = ""; + for (i=0; i<tmlreq.getNbOfParams(); i++) { + if (tmlreq.getParam(i).length() > 0) { + if (!Conversion.isNumeralOrId(tmlreq.getParam(i))) { + tmp = "ntmp__" + i; + if (tmlreq.getRequest().getType(i).getType() == TMLType.NATURAL) { + parameter = tclass.addNewParamIfApplicable(tmp, Param.NAT, "0"); + } else { + parameter = tclass.addNewParamIfApplicable(tmp, Param.BOOL, "false"); + } + + adacparam1 = new ADActionStateWithParam(parameter); + adacparam1.setActionValue(modifyString(tmlreq.getParam(i))); + tclass.getActivityDiagram().add(adacparam1); + if (adacparam == null) { + adacparam2 = adacparam1; + adacparam = adacparam1; + } else { + adacparam.addNext(adacparam1); + adacparam = adacparam1; + } + } else { + tmp = modifyString(tmlreq.getParam(i)); + } + action += "!" + modifyString(tmp); + } + } + if (adacparam != null) { + adacparam.addNext(adag); + } + adag.setActionValue(action); + + baseElements.add(tmle); + tclass.getActivityDiagram().add(adag); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adag, adjunc); + adag.addNext(adc1); + + if (adacparam2 != null) { + newElements.add(adacparam2); + return adacparam2; + } + newElements.add(adag); + return adag; + + // TMLWaitEvent + } else if (tmle instanceof TMLWaitEvent) { + acevt = (TMLActivityElementEvent)tmle; + g = tclass.addNewGateIfApplicable("wait__" + acevt.getEvent().getName()); + TClass tcl = tm.getTClassWithName(nameEvent + acevt.getEvent().getName()); + g1 = ((TClassEventCommon)(tcl)).getGateRead(); + tm.addSynchroRelation(tclass, g, tcl, g1); + + adag = new ADActionStateWithGate(g); + action = ""; + for (i=0; i<acevt.getNbOfParams(); i++) { + if (acevt.getParam(i).length() > 0) { + action += "?" + modifyString(acevt.getParam(i)) + ":" + TMLType.getLOTOSStringType(acevt.getEvent().getType(i).getType()); + } + } + adag.setActionValue(action); + + newElements.add(adag); + baseElements.add(tmle); + tclass.getActivityDiagram().add(adag); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adag, adjunc); + adag.addNext(adc1); + return adag; + + // TMLNotifiedEvent + } else if (tmle instanceof TMLNotifiedEvent) { + acevt = (TMLActivityElementEvent)tmle; + g = tclass.addNewGateIfApplicable("notified__" + acevt.getEvent().getName()); + TClass tcl = tm.getTClassWithName(nameEvent + acevt.getEvent().getName()); + g1 = ((TClassEventCommon)(tcl)).getGateSize(); + + if (g1 == null) { + return null; + } + + tm.addSynchroRelation(tclass, g, tcl, g1); + + adag = new ADActionStateWithGate(g); + action = "?" + acevt.getVariable() + ":nat"; + adag.setActionValue(action); + + newElements.add(adag); + baseElements.add(tmle); + tclass.getActivityDiagram().add(adag); + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adag, adjunc); + adag.addNext(adc1); + return adag; + + // TMLWriteChannel + } else if (tmle instanceof TMLWriteChannel) { + acch = (TMLActivityElementChannel)tmle; + if ((acch.getNbOfSamples().trim().compareTo("1")) == 0) { + adag = null; + adagtmp = null; + for(int k=0; k<acch.getNbOfChannels(); k++) { + g = addGateChannel("wr", acch, k, tclass); + TClass tcl = tm.getTClassWithName(getChannelString(acch.getChannel(k))); + g1 = tcl.getGateByName("wr__"+acch.getChannel(k).getName()); + tm.addSynchroRelation(tclass, g, tcl, g1); + adag = new ADActionStateWithGate(g); + adag.setActionValue(""); + tclass.getActivityDiagram().add(adag); + if (adagtmp != null) { + adagtmp.addNext(adag); + } + adagtmp = adag; + + } + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adag, adjunc); + adag.addNext(adc1); + newElements.add(adag); + baseElements.add(tmle); + return adag; + } else { + parameter = tclass.addNewParamIfApplicable("cpt__0", "nat", "0"); + adchoice = null; + adacparam2 = null; + + for(int k=0; k<acch.getNbOfChannels(); k++) { + + adacparam = new ADActionStateWithParam(parameter); + adacparam.setActionValue(acch.getNbOfSamples()); + tclass.getActivityDiagram().add(adacparam); + + if (k ==0) { + newElements.add(adacparam); + baseElements.add(tmle); + adacparam2 = adacparam; + } else { + adchoice.addNext(adacparam); + } + + adj = new ADJunction(); + tclass.getActivityDiagram().add(adj); + adacparam.addNext(adj); + + adchoice = new ADChoice(); + tclass.getActivityDiagram().add(adchoice); + adj.addNext(adchoice); + + adacparam1 = new ADActionStateWithParam(parameter); + adacparam1.setActionValue("cpt__0 - 1"); + tclass.getActivityDiagram().add(adacparam1); + adacparam1.addNext(adj); + + g = addGateChannel("wr", acch, k, tclass); + TClass tcl = tm.getTClassWithName(getChannelString(acch.getChannel(k))); + g1 = tcl.getGateByName("wr__"+acch.getChannel(k).getName()); + tm.addSynchroRelation(tclass, g, tcl, g1); + + adag = new ADActionStateWithGate(g); + adag.setActionValue(""); + tclass.getActivityDiagram().add(adag); + adchoice.addNext(adag); + adchoice.addGuard("[cpt__0 > 0]"); + + adag.addNext(adacparam1); + + if (k == (acch.getNbOfChannels()-1)) { + adc1 = translateAD(newElements, baseElements, tclass, task, tmle.getNextElement(0), adacparam1, adjunc); + adchoice.addNext(adc1); + } + + adchoice.addGuard("[cpt__0 == 0]"); + } + + return adacparam2; + + + + + } + } + } catch (Exception e) { + System.out.println("Exception in AD diagram analysis -> " + e.getMessage()); + return null; + } + + return null; + + } + + private void setADRequested(TClass tclass, TMLTask task) { + // attributes + int n = task.getRequest().getNbOfParams(); + int i; + //String type; + + for(i=0; i<n; i++) { + switch (task.getRequest().getType(i).getType()) { + case TMLType.NATURAL: + tclass.addNewParamIfApplicable("arg" + (i+1) + "__req", "nat", "0"); + break; + default: + tclass.addNewParamIfApplicable("arg" + (i+1) + "__req", "bool", "0"); + } + } + + // Modifying AD + ADStart start = tclass.getActivityDiagram().getStartState(); + ADComponent adc = start.getNext(0); + ADJunction adj = new ADJunction(); + ADActionStateWithGate adag; + //ADSequence adseq; + Gate g, g1; + String action; + + g = tclass.addNewGateIfApplicable("waitReq__" + task.getRequest().getName()); + TClass tcl = tm.getTClassWithName(nameRequest + task.getRequest().getName()); + g1 = ((TClassRequest)(tcl)).getGateRead(); + tm.addSynchroRelation(tclass, g, tcl, g1); + + adag = new ADActionStateWithGate(g); + action = ""; + for (i=0; i<task.getRequest().getNbOfParams(); i++) { + action += "?arg" + (i+1) + "__req:nat"; + } + adag.setActionValue(action); + + // Search for all adcomponents which next is a stop ... Replace this next to a next to the first adjunction + //System.out.println("Remove all elements .."); + try { + tm.removeAllElement(Class.forName("translator.ADStop"), adj, tclass.getActivityDiagram()); + } catch (ClassNotFoundException cnfe ) {} + //System.out.println("All elements removed ..."); + tclass.getActivityDiagram().add(adag); + tclass.getActivityDiagram().add(adj); + + // End of AD should be linked to the beginning! + start.removeAllNext(); + start.addNext(adj); + adj.addNext(adag); + adag.addNext(adc); + + + } + + private void setGatesToTask(TClass tclass, TMLTask task) { + setGatesEvt(tclass, task); + setGatesRequest(tclass, task); + setGatesChannel(tclass, task); + } + + private void setGatesEvt(TClass tclass, TMLTask task) { + ListIterator iterator = tmlmodeling.getListIteratorEvents(); + TMLEvent event; + Gate g, g1; + TClass tcl; + + while(iterator.hasNext()) { + event = (TMLEvent)(iterator.next()); + + if (task == event.getOriginTask()) { + g = tclass.addNewGateIfApplicable("notify__" + event.getName()); + tcl = tm.getTClassWithName(nameEvent + event.getName()); + g1 = ((TClassEventCommon)(tcl)).getGateWrite(); + tm.addSynchroRelation(tclass, g, tcl, g1); + } + + if (task == event.getDestinationTask()) { + //Wait + g = tclass.addNewGateIfApplicable("wait__" + event.getName()); + tcl = tm.getTClassWithName(nameEvent + event.getName()); + g1 = ((TClassEventCommon)(tcl)).getGateRead(); + tm.addSynchroRelation(tclass, g, tcl, g1); + + // Notified + g = tclass.addNewGateIfApplicable("notified__" + event.getName()); + tcl = tm.getTClassWithName(nameEvent + event.getName()); + g1 = ((TClassEventCommon)(tcl)).getGateSize(); + tm.addSynchroRelation(tclass, g, tcl, g1); + } + } + } + + private void setGatesRequest(TClass tclass, TMLTask task) { + ListIterator iterator = tmlmodeling.getListIteratorRequests(); + TMLRequest request; + Gate g, g1; + TClass tcl; + int index; + + while(iterator.hasNext()) { + request = (TMLRequest)(iterator.next()); + g = tclass.addNewGateIfApplicable("sendReq__" + request.getName() + "__" + task.getName()); + tcl = tm.getTClassWithName(nameRequest + request.getName()); + //g1 = tcl.getGateByName("sendReq"); + index = request.getOriginTasks().indexOf(task); + if (index != -1) { + //System.out.println("task=" + task.getName() + " index=" + index); + g1 = (Gate)(((TClassRequest)tcl).getGatesWrite().get(index)); + //System.out.println("task=" + task.getName() + " index=" + index + "gate=" + g.getName()); + tm.addSynchroRelation(tclass, g, tcl, g1); + } + } + } + + private void setGatesChannel(TClass tclass, TMLTask task) { + ListIterator iterator = tmlmodeling.getListIteratorChannels(); + TMLChannel channel; + Gate g, g1; + TClass tcl; + //int index; + //String name; + + while(iterator.hasNext()) { + channel = (TMLChannel)(iterator.next()); + + if (task == channel.getOriginTask()) { + g = tclass.addNewGateIfApplicable("wr__" + channel.getName()); + tcl = tm.getTClassWithName(getChannelString(channel)); + g1 = tcl.getGateByName("wr__"+channel.getName()); + tm.addSynchroRelation(tclass, g, tcl, g1); + } + + if (task == channel.getDestinationTask()) { + g = tclass.addNewGateIfApplicable("rd__" + channel.getName()); + tcl = tm.getTClassWithName(getChannelString(channel)); + g1 = tcl.getGateByName("rd__"+channel.getName()); + tm.addSynchroRelation(tclass, g, tcl, g1); + + } + } + } + + + + + private ADComponent endOfActivity(Vector newElements, Vector baseElements, TClass tclass, ADJunction adjunc) { + if (adjunc == null) { + ADStop adstop = new ADStop(); + newElements.add(adstop); + baseElements.add(adstop); + tclass.getActivityDiagram().add(adstop); + return adstop; + } else { + return adjunc; + } + } + + private Gate addGateChannel(String name, TMLActivityElementChannel tmle, int _index, TClass tclass) { + name = name + "__" + tmle.getChannel(_index).getName(); + return tclass.addNewGateIfApplicable(name); + } + + private boolean printAnalyzer(String action) { + action = action.trim(); + if (action.startsWith("cout") || action.startsWith("std::cout")) { + return true; + } + return false; + + } + + private String modifyString(String _input) { + _input = Conversion.replaceAllString(_input, "<<", "*"); + _input = Conversion.replaceAllString(_input, ">>", "/"); + + // Replaces &&, || and ! + _input = Conversion.replaceAllString(_input,"&&", "and"); + _input = Conversion.replaceAllString(_input, "||", "or"); + _input = Conversion.replaceAllString(_input, "!", "not"); + _input = Conversion.replaceAllStringNonAlphanumerical(_input, "i", "i_0"); + + return _input; + } + + private void makeAttributes(TMLTask task, TClass tcl) { + ListIterator iterator = task.getAttributes().listIterator(); + TMLAttribute tmla; + //Param para; + + while(iterator.hasNext()) { + tmla = (TMLAttribute)(iterator.next()); + switch (tmla.type.getType()) { + case TMLType.NATURAL: + //System.out.println("Adding nat attribute:" + modifyString(tmla.name)); + tcl.addNewParamIfApplicable(modifyString(tmla.name), "nat", modifyString(tmla.initialValue)); + break; + default: + tcl.addNewParamIfApplicable(modifyString(tmla.name), "bool", modifyString(tmla.initialValue)); + } + } + } + + // Returns Param if action starts with a Param ... + private Param paramAnalyzer(String action, TClass tcl) { + int index = action.indexOf("="); + if (index < 0) { + // ++ expression ? + index = action.indexOf("++"); + if (index < 0) { + // -- expression + index = action.indexOf("--"); + if (index < 0) { + return null; + } + } + } + + action = action.substring(0, index); + action = action.trim(); + + return tcl.getParamByName(action); + } + + private String getActionValueParam(String action, TClass tcl) { + int index = action.indexOf("="); + if (index < 0) { + // ++ expression ? + index = action.indexOf("++"); + if (index < 0) { + // -- expression + index = action.indexOf("--"); + if (index < 0) { + return null; + } else { + action = action.substring(0, index); + action = action.trim(); + return action + "-1"; + } + } else { + action = action.substring(0, index); + action = action.trim(); + return action + "+1"; + } + } + + return action = action.substring(index+1, action.length()).trim(); + } + + private String removeLastSemicolon(String action) { + action = action.trim(); + if (action.charAt(action.length()-1) == ';') { + return action.substring(0, action.length()-1); + } + return action; + }*/ +} diff --git a/src/translator/TURTLEModelChecker.java b/src/translator/TURTLEModelChecker.java index bd047931039c56b1da783a2727ecd476c44caf9d..562e2f0c89aca563a8c377bbc8f72834b3bb8597 100755 --- a/src/translator/TURTLEModelChecker.java +++ b/src/translator/TURTLEModelChecker.java @@ -385,6 +385,10 @@ public class TURTLEModelChecker { int j; ADChoice choice; + if (ad == null) { + return; + } + for(int i=0; i<ad.size(); i++) { ad1 = (ADComponent)(ad.elementAt(i)); diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java index 8b80f8a68a578b79a5f4d4361c7fd62ebcd199bb..79942d30663c909b3b926e77ea6543317cf336c2 100644 --- a/src/ui/AvatarDesignPanelTranslator.java +++ b/src/ui/AvatarDesignPanelTranslator.java @@ -107,6 +107,7 @@ public class AvatarDesignPanelTranslator { ui.AvatarSignal uias; avatartranslator.AvatarMethod atam; avatartranslator.AvatarSignal atas; + TGComponent tgc1, tgc2; for(AvatarBDBlock block: _blocks) { ab = new AvatarBlock(block.getBlockName(), block); @@ -158,6 +159,22 @@ public class AvatarDesignPanelTranslator { } + // Make block hierarchy + for(AvatarBlock block: _as.getListOfBlocks()) { + tgc1 = listE.getTG(block); + if ((tgc1 != null) && (tgc1.getFather() != null)) { + tgc2 = tgc1.getFather(); + ab = listE.getAvatarBlock(tgc2); + if (ab != null) { + block.setFather(ab); + } + } + } + + // Make state machine of blocks + for(AvatarBlock block: _as.getListOfBlocks()) { + makeStateMachine(_as, block); + } } @@ -172,6 +189,379 @@ public class AvatarDesignPanelTranslator { } } + public void makeStateMachine(AvatarSpecification _as, AvatarBlock _ab) { + AvatarBDBlock block = (AvatarBDBlock)(listE.getTG(_ab)); + if (block == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "No corresponding graphical block for " + _ab.getName()); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(adp.getAvatarBDPanel()); + addCheckingError(ce); + return; + } + + AvatarSMDPanel asmdp = block.getAvatarSMDPanel(); + String name = block.getBlockName(); + TDiagramPanel tdp; + + int size = checkingErrors.size(); + + if (asmdp == null) { + return; + } + + tdp = (TDiagramPanel)asmdp; + + // search for start state + LinkedList list = asmdp.getComponentList(); + Iterator iterator = list.listIterator(); + TGComponent tgc; + AvatarSMDStartState tss = null; + int cptStart = 0; + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + if (tgc instanceof AvatarSMDStartState){ + tss = (AvatarSMDStartState)tgc; + cptStart ++; + } + } + + if (tss == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "No start state in the state machine diagram of " + name); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + return; + } + + if (cptStart > 1) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "More than one start state in the state machine diagram of " + name); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + addCheckingError(ce); + return; + } + + // This shall also be true for all composite state: at most one start state! + tgc = checkForStartStateOfCompositeStates(asmdp); + if (tgc != null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "More than one start state in composite state"); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + return; + } + + // First pass: creating TIF components, but no interconnection between them + iterator = asmdp.getAllComponentList().listIterator(); + AvatarSMDReceiveSignal asmdrs; + AvatarSMDSendSignal asmdss; + + AvatarStateMachine asm = _ab.getStateMachine(); + avatartranslator.AvatarSignal atas; + AvatarActionOnSignal aaos; + AvatarAttribute aa; + AvatarStopState astop; + AvatarStartState astart; + AvatarState astate; + int i; + String tmp; + + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + + // Receive signal + if (tgc instanceof AvatarSMDReceiveSignal) { + asmdrs = (AvatarSMDReceiveSignal)tgc; + atas = _ab.getAvatarSignalWithName(asmdrs.getSignalName()); + if (atas == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Unknown signal: " + asmdrs.getSignalName()); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + aaos = new AvatarActionOnSignal("action_on_signal", atas, tgc); + if (aaos.isSending()) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "a sending signal is used for receiving: " + asmdrs.getValue()); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } + if (asmdrs.getNbOfValues() == -1) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed signal: " + asmdrs.getValue()); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + for(i=0; i<asmdrs.getNbOfValues(); i++) { + tmp = asmdrs.getValue(i); + if (tmp.length() == 0) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed parameter: " + tmp + " in signal expression: " + asmdrs.getValue()); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + // Check that tmp is the identifier of an attribute + aa = _ab.getAvatarAttributeWithName(tmp); + if (aa == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed parameter: " + tmp + " in signal expression: " + asmdrs.getValue()); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + aaos.addValue(tmp); + } + } + } + //adag.setActionValue(makeTIFAction(asmdrs.getValue(), "?")); + listE.addCor(aaos, tgc); + asm.addElement(aaos); + } + } + } else if (tgc instanceof AvatarSMDSendSignal) { + asmdss = (AvatarSMDSendSignal)tgc; + atas = _ab.getAvatarSignalWithName(asmdss.getSignalName()); + if (atas == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Unknown signal: " + asmdss.getSignalName()); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + aaos = new AvatarActionOnSignal("action_on_signal", atas, tgc); + if (aaos.isReceiving()) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "A sending signal is used for receiving: " + asmdss.getValue()); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } + if (asmdss.getNbOfValues() == -1) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed signal: " + asmdss.getValue()); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + for(i=0; i<asmdss.getNbOfValues(); i++) { + tmp = asmdss.getValue(i); + if (tmp.length() == 0) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed parameter: " + tmp + " in signal expression: " + asmdss.getValue()); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + // Check that tmp is the identifier of an attribute + aa = _ab.getAvatarAttributeWithName(tmp); + if (aa == null) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed parameter: " + tmp + " in signal expression: " + asmdss.getValue()); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + aaos.addValue(tmp); + } + } + } + //adag.setActionValue(makeTIFAction(asmdrs.getValue(), "?")); + listE.addCor(aaos, tgc); + asm.addElement(aaos); + } + } + + // State + } else if (tgc instanceof AvatarSMDState) { + astate = asm.getStateWithName(tgc.getValue()); + if (astate == null) { + astate = new AvatarState(tgc.getValue(), tgc); + asm.addElement(astate); + } + listE.addCor(astate, tgc); + + // Start state + } else if (tgc instanceof AvatarSMDStartState) { + astart = new AvatarStartState("start", tgc); + listE.addCor(astart, tgc); + asm.addElement(astart); + if (tgc.getFather() == null) { + asm.setStartState(astart); + } + + // Stop state + } else if (tgc instanceof AvatarSMDStopState) { + astop = new AvatarStopState("stop", tgc); + listE.addCor(astop, tgc); + asm.addElement(astop); + } + } + + if (checkingErrors.size() != size) { + return; + } + + // Make hierachy between states and elements + iterator = asmdp.getAllComponentList().listIterator(); + AvatarStateMachineElement element1, element2; + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + if ((tgc != null) && (tgc.getFather() != null)) { + element1 = (AvatarStateMachineElement)(listE.getObject(tgc)); + element2 = (AvatarStateMachineElement)(listE.getObject(tgc.getFather())); + if ((element1 != null) && (element2 != null) && (element2 instanceof AvatarState)) { + element1.setState((AvatarState)element2); + } + } + } + + // Make next: handle transitions + iterator = asmdp.getAllComponentList().listIterator(); + AvatarSMDConnector asmdco; + AvatarTransition at; + TGComponent tgc1, tgc2; + int error; + String tmp1, tmp2; + Vector <String> vs; + + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + if (tgc instanceof AvatarSMDConnector) { + asmdco = (AvatarSMDConnector)tgc; + tgc1 = tdp.getComponentToWhichBelongs(asmdco.getTGConnectingPointP1()); + tgc2 = tdp.getComponentToWhichBelongs(asmdco.getTGConnectingPointP2()); + if ((tgc1 == null) || (tgc2 == null)) { + TraceManager.addDev("Tgcs null in Avatar translation"); + } else { + element1 = (AvatarStateMachineElement)(listE.getObject(tgc1)); + element2 = (AvatarStateMachineElement)(listE.getObject(tgc2)); + if ((element1 != null) && (element2 != null)) { + at = new AvatarTransition("avatar transition", tgc); + + // Guard + tmp = asmdco.getGuard(); + error = AvatarSyntaxChecker.isAValidGuard(_as, _ab, tmp); + if (error < 0) { + makeError(error, tdp, _ab, tgc, "transition guard", tmp); + } else { + at.setGuard(tmp); + } + + // Delays + tmp1 = asmdco.getAfterMinDelay(); + error = AvatarSyntaxChecker.isAValidIntExpr(_as, _ab, tmp1); + if (error < 0) { + makeError(error, tdp, _ab, tgc, "after min delay", tmp1); + tmp1 = null; + } + tmp2 = asmdco.getAfterMaxDelay(); + error = AvatarSyntaxChecker.isAValidIntExpr(_as, _ab, tmp2); + if (error < 0) { + makeError(error, tdp, _ab, tgc, "after max delay", tmp2); + tmp2 = null; + } + + if ((tmp1 != null) && (tmp2 != null)) { + at.setDelays(tmp1, tmp2); + } + + // Compute min and max + tmp1 = asmdco.getComputeMinDelay(); + error = AvatarSyntaxChecker.isAValidIntExpr(_as, _ab, tmp1); + if (error < 0) { + makeError(error, tdp, _ab, tgc, "compute min ", tmp1); + tmp1 = null; + } + tmp2 = asmdco.getComputeMaxDelay(); + error = AvatarSyntaxChecker.isAValidIntExpr(_as, _ab, tmp2); + if (error < 0) { + makeError(error, tdp, _ab, tgc, "compute max ", tmp2); + tmp2 = null; + } + + if ((tmp1 != null) && (tmp2 != null)) { + at.setComputes(tmp1, tmp2); + } + + // Actions + vs = asmdco.getActions(); + for(String s: vs) { + if (s.trim().length() > 0) { + s = s.trim(); + // Variable assignation or method call? + error = s.indexOf("="); + if (error == -1) { + // Method call + if(!_ab.isAValidMethodCall(s)) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formed transition method call: " + s); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(tdp); + ce.setTGComponent(tgc); + addCheckingError(ce); + } else { + at.addAction(s); + } + } else { + // Variable assignation + error = AvatarSyntaxChecker.isAValidVariableExpr(_as, _ab, s); + if (error < 0) { + makeError(error, tdp, _ab, tgc, "transition action", s); + } else { + at.addAction(s); + } + } + } + } + + element1.addNext(at); + at.addNext(element2); + listE.addCor(at, tgc); + asm.addElement(at); + } + } + } + } + + } + + private void makeError(int _error, TDiagramPanel _tdp, AvatarBlock _ab, TGComponent _tgc, String _info, String _element) { + if (_error == -3) { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Undeclared variable in " + _info + ": " + _element); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(_tdp); + ce.setTGComponent(_tgc); + addCheckingError(ce); + } else { + CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "Badly formatted " + _info + ": " + _element); + ce.setAvatarBlock(_ab); + ce.setTDiagramPanel(_tdp); + ce.setTGComponent(_tgc); + addCheckingError(ce); + } + } + + // Checks whether all states with internal state machines have at most one start state + private TGComponent checkForStartStateOfCompositeStates(AvatarSMDPanel _panel) { + TGComponent tgc; + ListIterator iterator = _panel.getComponentList().listIterator(); + while(iterator.hasNext()) { + tgc = (TGComponent)(iterator.next()); + if (tgc instanceof AvatarSMDState) { + tgc = (((AvatarSMDState)(tgc)).checkForStartStateOfCompositeStates()); + if (tgc != null) { + return tgc; + } + } + } + return null; + } + + public void createRelationsBetweenBlocks(AvatarSpecification _as, LinkedList<AvatarBDBlock> _blocks) { adp.getAvatarBDPanel().updateAllSignalsOnConnectors(); Iterator iterator = adp.getAvatarBDPanel().getComponentList().listIterator(); diff --git a/src/ui/AvatarSignal.java b/src/ui/AvatarSignal.java index 66234fa72eedd8175438b33dd4083809b49c37c5..bb9e5bd7c4cd51fc99c95d22d97b3805365dbea7 100644 --- a/src/ui/AvatarSignal.java +++ b/src/ui/AvatarSignal.java @@ -205,4 +205,45 @@ public class AvatarSignal extends AvatarMethod { return signal; } + + public static int getNbOfValues(String _value) { + int index = _value.indexOf('('); + if (index == -1) { + return -1; + } + + int index0 = _value.indexOf(')'); + if (index0 == -1) { + return -1; + } + + String val = _value.substring(index+1, index0).trim(); + + if (val.length() == 0) { + return 0; + } + + int nbChar = Conversion.nbChar(_value, ','); + return nbChar+1; + } + + public static String getValue(String _value, int _index) { + int nbOfValues = getNbOfValues(_value); + if (nbOfValues < 1) { + return null; + } + + if (_index >= nbOfValues) { + return null; + } + + int index0 = _value.indexOf('('); + int index1 = _value.indexOf(')'); + + String val = _value.substring(index0+1, index1).trim(); + + String [] vals = val.split(","); + return vals[_index].trim(); + + } } \ No newline at end of file diff --git a/src/ui/CheckingError.java b/src/ui/CheckingError.java index 07bfd19f1157f8eff6d0fb0d5bcba2462be3214b..3cc003a6e5b2e8e6b3804b491e20deddf8d2f582 100755 --- a/src/ui/CheckingError.java +++ b/src/ui/CheckingError.java @@ -45,6 +45,8 @@ knowledge of the CeCILL license and that you accept its terms. package ui; +import avatartranslator.*; + import translator.*; import tmltranslator.*; @@ -62,6 +64,7 @@ public class CheckingError { private TMLTask tmlt; private TDiagramPanel tdp; private TGComponent tgc; + private AvatarBlock ab; public CheckingError(int _type, String _message) { type = _type; @@ -79,6 +82,10 @@ public class CheckingError { public void setTClass(TClass _t) { t = _t; } + + public void setAvatarBlock(AvatarBlock _ab) { + ab = _ab; + } public void setTMLTask(TMLTask _tmlt) { tmlt = _tmlt; @@ -103,6 +110,10 @@ public class CheckingError { public TClass getTClass() { return t; } + + public AvatarBlock getAvatarBlock() { + return ab; + } public TMLTask getTMLTask() { return tmlt; diff --git a/src/ui/CorrespondanceTGElement.java b/src/ui/CorrespondanceTGElement.java index d00a10ad57b7eee7eafcbece56a2002ffab85f99..535d30577069e247ade589946e47cde1edd2dabc 100755 --- a/src/ui/CorrespondanceTGElement.java +++ b/src/ui/CorrespondanceTGElement.java @@ -50,6 +50,7 @@ package ui; import java.awt.*; import java.util.*; +import avatartranslator.*; import req.ebrdd.*; import translator.*; import tmltranslator.*; @@ -101,6 +102,14 @@ public class CorrespondanceTGElement { } return null; } + + public Object getObject(TGComponent tgc) { + int index = tg.indexOf(tgc); + if ((index != -1) && (tg.size() > index)) { + return data.elementAt(index); + } + return null; + } public void addCorInPanel(Object o, TGComponent tgc, String panelName) @@ -154,6 +163,14 @@ public class CorrespondanceTGElement { } return null; } + + public TGComponent getTGFromObject(Object o) { + int index = tg.indexOf(o); + if ((index != -1) && (data.size() > index)) { + return (TGComponent)(data.elementAt(index)); + } + return null; + } public TGComponent getTGAt(int index) { if ((index != -1) && (tg.size() > index)) { @@ -173,6 +190,18 @@ public class CorrespondanceTGElement { } return null; } + + public AvatarBlock getAvatarBlock(TGComponent _tgc) { + int index = tg.indexOf(_tgc); + if ((index != -1) && (tg.size() > index)) { + Object o = data.elementAt(index); + if (o instanceof AvatarBlock) { + return (AvatarBlock)o; + } + return null; + } + return null; + } public HMSCNode getNodeAt(int index) { if ((index != -1) && (data.size() > index)) { diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java index 86c5695e5f2adb3b836f42a1b39ef8612f5f58da..1de7e518bc860d647b7b97e2751fc4b77c3605be 100755 --- a/src/ui/GTURTLEModeling.java +++ b/src/ui/GTURTLEModeling.java @@ -81,6 +81,7 @@ import ui.avatarrd.*; import ui.avatarpd.*; import avatartranslator.*; +import avatartranslator.toturtle.*; import ui.tmlad.*; import ui.tmlcd.*; @@ -1562,7 +1563,7 @@ public class GTURTLEModeling { AvatarDesignPanelTranslator adpt = new AvatarDesignPanelTranslator(adp); avatarspec = adpt.generateAvatarSpecification(blocks); TraceManager.addDev("AvatarSpec:" + avatarspec.toString() + "\n\n"); - tmState = 0; + tmState = 3; listE = adpt.getCorrespondanceTGElement(); checkingErrors = adpt.getErrors(); @@ -1590,6 +1591,25 @@ public class GTURTLEModeling { return true;*/ } + + // From AVATAR to TURTLEModeling + public boolean translateAvatarSpecificationToTIF() { + AVATAR2TURTLE att = new AVATAR2TURTLE(avatarspec); + tm = att.generateTURTLEModeling(); + + TURTLEModelChecker tmc = new TURTLEModelChecker(tm, listE); + + checkingErrors = tmc.syntaxAnalysisChecking(); + warnings.addAll(tmc.getWarnings()); + + if ((checkingErrors != null) && (checkingErrors.size() > 0)){ + analyzeErrors(); + return false; + } else { + return true; + } + + } public Vector getCheckingErrors() { return checkingErrors; diff --git a/src/ui/MainGUI.java b/src/ui/MainGUI.java index 11d47e3f5afca59d3315ffd40d1f516ca2ba704a..c5f8e5700cfe81560ccdc993a1d49a8c398e5a88 100755 --- a/src/ui/MainGUI.java +++ b/src/ui/MainGUI.java @@ -2975,6 +2975,19 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener { TraceManager.addDev("Generating from state 2"); return generateTIFFromTMLModeling(automatic, generator); } + if (state == 3) { + TraceManager.addDev("Generating from state 3 (Avatar)"); + return generateTIFFromAvatarSpecification(automatic, generator); + } + return false; + } + + public boolean generateTIFFromAvatarSpecification(boolean automatic, int generator) { + boolean b = gtm.translateAvatarSpecificationToTIF(); + if (b) { + setMode(MainGUI.MODEL_OK); + return true; + } return false; } diff --git a/src/ui/avatarbd/AvatarBDBlock.java b/src/ui/avatarbd/AvatarBDBlock.java index 4b5186a76cd7721b65d2637d8e035c8d743fc370..c4e0bb992676b14a7d1e7da34448b649fad77a5c 100644 --- a/src/ui/avatarbd/AvatarBDBlock.java +++ b/src/ui/avatarbd/AvatarBDBlock.java @@ -306,7 +306,7 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S break; } am = (AvatarMethod)(myMethods.get(index)); - method = "- " + am.toString(); + method = "# " + am.toString(); w = g.getFontMetrics().stringWidth(method); if ((w + (2 * textX) + 1) < width) { g.drawString(method, x + textX, y + cpt); @@ -356,7 +356,7 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S break; } as = (AvatarSignal)(mySignals.get(index)); - signal = as.toString(); + signal = "# " + as.toString(); w = g.getFontMetrics().stringWidth(signal); if ((w + (2 * textX) + 1) < width) { g.drawString(signal, x + textX, y + cpt); @@ -796,6 +796,28 @@ public class AvatarBDBlock extends TGCScalableWithInternalComponent implements S return mySignals; } + public Vector getAllMethodList() { + if (getFather() == null) { + return myMethods; + } + + Vector v = new Vector(); + v.addAll(myMethods); + v.addAll(((AvatarBDBlock)getFather()).getAllMethodList()); + return v; + } + + public Vector getAllSignalList() { + if (getFather() == null) { + return mySignals; + } + + Vector v = new Vector(); + v.addAll(mySignals); + v.addAll(((AvatarBDBlock)getFather()).getAllSignalList()); + 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 731fb2a0f072c3a33a796487eaa5533a7dc567c1..e8e0271aa236a56f71387e28821669ccaa30d302 100644 --- a/src/ui/avatarbd/AvatarBDPanel.java +++ b/src/ui/avatarbd/AvatarBDPanel.java @@ -573,7 +573,7 @@ public class AvatarBDPanel extends TDiagramPanel { LinkedList<AvatarBDBlock> list = getFullBlockList(); for(AvatarBDBlock block: list) { if (block.getBlockName().compareTo(_name) ==0) { - return block.getMethodList(); + return block.getAllMethodList(); } } return null; @@ -583,7 +583,7 @@ public class AvatarBDPanel extends TDiagramPanel { LinkedList<AvatarBDBlock> list = getFullBlockList(); for(AvatarBDBlock block: list) { if (block.getBlockName().compareTo(_name) ==0) { - return block.getSignalList(); + return block.getAllSignalList(); } } return null; diff --git a/src/ui/avatarsmd/AvatarSMDConnector.java b/src/ui/avatarsmd/AvatarSMDConnector.java index 451711c594e8aceeeb866ed648baf68e5d19841d..17d454bf92949678891398658cfb4b17b69b44da 100644 --- a/src/ui/avatarsmd/AvatarSMDConnector.java +++ b/src/ui/avatarsmd/AvatarSMDConnector.java @@ -122,19 +122,28 @@ public class AvatarSMDConnector extends TGConnector { return TGComponentManager.AVATARSMD_CONNECTOR; } + public AvatarSMDTransitionInfo getAvatarSMDTransitionInfo() { + for(int i=0; i<tgcomponent.length; i++) { + if (tgcomponent[i] instanceof AvatarSMDTransitionInfo) { + return (AvatarSMDTransitionInfo)(tgcomponent[i]); + } + } + return null; + } + public String getGuard() { - return ((AvatarSMDTransitionInfo)getInternalTGComponent(0)).getGuard(); + return getAvatarSMDTransitionInfo().getGuard(); } public String getTotalMinDelay() { - String s1 = ((AvatarSMDTransitionInfo)getInternalTGComponent(0)).getAfterMinDelay(); - String s2 = ((AvatarSMDTransitionInfo)getInternalTGComponent(0)).getComputeMinDelay(); + String s1 = getAvatarSMDTransitionInfo().getAfterMinDelay(); + String s2 = getAvatarSMDTransitionInfo().getComputeMinDelay(); return addedDelays(s1, s2); } public String getTotalMaxDelay() { - String s1 = ((AvatarSMDTransitionInfo)getInternalTGComponent(0)).getAfterMaxDelay(); - String s2 = ((AvatarSMDTransitionInfo)getInternalTGComponent(0)).getComputeMaxDelay(); + String s1 = getAvatarSMDTransitionInfo().getAfterMaxDelay(); + String s2 = getAvatarSMDTransitionInfo().getComputeMaxDelay(); return addedDelays(s1, s2); } @@ -151,7 +160,23 @@ public class AvatarSMDConnector extends TGConnector { } public Vector<String> getActions() { - return ((AvatarSMDTransitionInfo)getInternalTGComponent(0)).getActions(); + return getAvatarSMDTransitionInfo().getActions(); + } + + public String getAfterMinDelay() { + return getAvatarSMDTransitionInfo().getAfterMinDelay(); + } + + public String getAfterMaxDelay() { + return getAvatarSMDTransitionInfo().getAfterMaxDelay(); + } + + public String getComputeMinDelay() { + return getAvatarSMDTransitionInfo().getComputeMinDelay(); + } + + public String getComputeMaxDelay() { + return getAvatarSMDTransitionInfo().getComputeMaxDelay(); } } diff --git a/src/ui/avatarsmd/AvatarSMDReceiveSignal.java b/src/ui/avatarsmd/AvatarSMDReceiveSignal.java index 91a129a048dd85076a5a116ea15806395550e94c..d2043595b23b115e71eaf05cbfc50b7607dc0e64 100644 --- a/src/ui/avatarsmd/AvatarSMDReceiveSignal.java +++ b/src/ui/avatarsmd/AvatarSMDReceiveSignal.java @@ -199,6 +199,16 @@ public class AvatarSMDReceiveSignal extends AvatarSMDBasicComponent implements C } return value.substring(0, index).trim(); } + + // Return -1 in case of error + public int getNbOfValues() { + return AvatarSignal.getNbOfValues(value); + } + + // Return null in case of error + public String getValue(int _index) { + return AvatarSignal.getValue(value, _index); + } /*public String getParamValue(int i) { return params[i]; diff --git a/src/ui/avatarsmd/AvatarSMDSendSignal.java b/src/ui/avatarsmd/AvatarSMDSendSignal.java index 4c7902d613c60d7210ac9984b17f84b0010985d9..b1985d2da8960d05dd94bc90640bf1c98df3ab07 100644 --- a/src/ui/avatarsmd/AvatarSMDSendSignal.java +++ b/src/ui/avatarsmd/AvatarSMDSendSignal.java @@ -207,6 +207,16 @@ public class AvatarSMDSendSignal extends AvatarSMDBasicComponent implements Chec return nParam; }*/ + // Return -1 in case of error + public int getNbOfValues() { + return AvatarSignal.getNbOfValues(value); + } + + // Return null in case of error + public String getValue(int _index) { + return AvatarSignal.getValue(value, _index); + } + public boolean editOndoubleClick(JFrame frame) { Vector signals = tdp.getMGUI().getAllSignals(); diff --git a/src/ui/window/JDialogAvatarSignal.java b/src/ui/window/JDialogAvatarSignal.java index fe1b30841d210ff04c3d0322f617d0303e209da4..a9331510a46a6378d0058fc4b209d09aaaa660fe 100755 --- a/src/ui/window/JDialogAvatarSignal.java +++ b/src/ui/window/JDialogAvatarSignal.java @@ -75,7 +75,6 @@ public class JDialogAvatarSignal extends javax.swing.JDialog implements ActionLi /** Creates new form */ - // arrayDelay: [0] -> minDelay ; [1] -> maxDelay public JDialogAvatarSignal(Frame _f, String _title, String _currentSignal, Vector _signals, boolean _isOut) { super(_f, _title, true);