diff --git a/plugins/howto b/plugins/howto
index 3f86dcbff002bed8f8a39a031ebf16b05ba3dba9..014bf968ed5543e6d7a12637ba927fc52e786078 100644
--- a/plugins/howto
+++ b/plugins/howto
@@ -6,7 +6,7 @@ $make
Then, edit the configuration file of TTool (default: TTool/bin/config.xml) and add:
<PLUGIN_PATH data="../plugins" />
<PLUGIN file="CustomizerAvatarJavaCodeGeneration.jar" package = "."/>
-PLUGIN file="CustomizerGraphicalComponent.jar" package="."/>
+<PLUGIN file="CustomizerGraphicalComponent.jar" package="."/>
Then, start TTool, and generate Java code from an avatar design model.
diff --git a/src/main/java/avatartranslator/AvatarBlock.java b/src/main/java/avatartranslator/AvatarBlock.java
index 511d0ebf1ca40d3fe58a75f48cbe676b00894a11..596ac54083a08ec0e6786702d2a72d638798901b 100644
--- a/src/main/java/avatartranslator/AvatarBlock.java
+++ b/src/main/java/avatartranslator/AvatarBlock.java
@@ -1,26 +1,26 @@
/* 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,
@@ -31,7 +31,7 @@
* 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.
*/
@@ -46,8 +46,9 @@ import java.util.List;
/**
* Class AvatarBlock
* Creation: 20/05/2010
- * @version 1.1 01/07/2014
+ *
* @author Ludovic APVRILLE, Raja GATGOUT
+ * @version 1.1 01/07/2014
*/
public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwner {
@@ -128,39 +129,39 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
public List<AvatarSignal> getSignals() {
- return signals ;
+ return signals;
}
public AvatarSignal getSignalByName(String _name) {
- for(AvatarSignal sig: signals) {
- if (sig.getName().compareTo(_name) == 0) {
- return sig;
- }
- }
+ for (AvatarSignal sig : signals) {
+ if (sig.getName().compareTo(_name) == 0) {
+ return sig;
+ }
+ }
- if (father != null) {
- return father.getSignalByName(_name);
- }
-
- return null;
+ if (father != null) {
+ return father.getSignalByName(_name);
+ }
+
+ return null;
}
public int getNbOfASMGraphicalElements() {
- if (asm == null) {
- return 0;
- }
+ if (asm == null) {
+ return 0;
+ }
- return asm.getNbOfASMGraphicalElements();
+ return asm.getNbOfASMGraphicalElements();
}
- public AvatarSpecification getAvatarSpecification () {
+ public AvatarSpecification getAvatarSpecification() {
return this.avspec;
}
public void addAttribute(AvatarAttribute _aa) {
- if (getAvatarAttributeWithName(_aa.getName()) == null) {
- attributes.add(_aa);
- }
+ if (getAvatarAttributeWithName(_aa.getName()) == null) {
+ attributes.add(_aa);
+ }
}
public void addIntAttributeIfApplicable(String _name) {
@@ -174,17 +175,17 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
//Thread.currentThread().dumpStack();
StringBuffer sb = new StringBuffer("block:" + getName() + " ID=" + getID() + " \n");
if (getFather() != null) {
- sb.append(" subblock of: " + getFather().getName() + " ID=" + getFather().getID()+ "\n");
+ sb.append(" subblock of: " + getFather().getName() + " ID=" + getFather().getID() + "\n");
} else {
sb.append(" top level block\n");
}
- for(AvatarAttribute attribute: attributes) {
+ for (AvatarAttribute attribute : attributes) {
sb.append(" attribute: " + attribute.toString() + " ID=" + attribute.getID() + "\n");
}
- for(AvatarMethod method: methods) {
+ for (AvatarMethod method : methods) {
sb.append(" method: " + method.toString() + " ID=" + method.getID() + "\n");
}
- for(AvatarSignal signal: signals) {
+ for (AvatarSignal signal : signals) {
sb.append(" signal: " + signal.toString() + " ID=" + signal.getID() + "\n");
}
if (asm != null) {
@@ -200,17 +201,17 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
//Thread.currentThread().dumpStack();
StringBuffer sb = new StringBuffer("block:" + getName() + " ID=" + getID() + " \n");
if (getFather() != null) {
- sb.append(" subblock of: " + getFather().getName() + " ID=" + getFather().getID()+ "\n");
+ sb.append(" subblock of: " + getFather().getName() + " ID=" + getFather().getID() + "\n");
} else {
sb.append(" top level block\n");
}
- for(AvatarAttribute attribute: attributes) {
+ for (AvatarAttribute attribute : attributes) {
sb.append(" attribute: " + attribute.toString() + " ID=" + attribute.getID() + "\n");
}
- for(AvatarMethod method: methods) {
+ for (AvatarMethod method : methods) {
sb.append(" method: " + method.toString() + " ID=" + method.getID() + "\n");
}
- for(AvatarSignal signal: signals) {
+ for (AvatarSignal signal : signals) {
sb.append(" signal: " + signal.toString() + " ID=" + signal.getID() + "\n");
}
@@ -227,11 +228,11 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
}
public AvatarState getState(int index) {
- return asm.getState(index);
+ return asm.getState(index);
}
public void putAllTimers(ArrayList<AvatarAttribute> timers) {
- for(AvatarAttribute attribute: attributes) {
+ for (AvatarAttribute attribute : attributes) {
if (attribute.getType() == AvatarType.TIMER) {
timers.add(attribute);
}
@@ -239,7 +240,7 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
}
public boolean hasTimer(String _name) {
- for(AvatarAttribute attribute: attributes) {
+ for (AvatarAttribute attribute : attributes) {
if (attribute.getType() == AvatarType.TIMER) {
if (attribute.getName().compareTo(_name) == 0) {
return true;
@@ -254,11 +255,11 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
public AvatarAttribute getAttribute(int _index) {
return attributes.get(_index);
}
-
+
public int getBlockIndex() {
return blockIndex;
}
-
+
public void setBlockIndex(int _blockIndex) {
blockIndex = _blockIndex;
}
@@ -274,11 +275,11 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
public int getIndexOfAvatarAttributeWithName(String _name) {
int cpt = 0;
- for(AvatarAttribute attribute: attributes) {
- if (attribute.getName().compareTo(_name)== 0) {
+ for (AvatarAttribute attribute : attributes) {
+ if (attribute.getName().compareTo(_name) == 0) {
return cpt;
}
- cpt ++;
+ cpt++;
}
return -1;
}
@@ -286,14 +287,12 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
/**
* Look for an attribute with the provided name.
*
- * @param _name
- * The name of the attribute to look for.
- *
+ * @param _name The name of the attribute to look for.
* @return The attribute if found, or null otherwise
*/
public AvatarAttribute getAvatarAttributeWithName(String _name) {
- for(AvatarAttribute attribute: attributes) {
- if (attribute.getName().compareTo(_name)== 0) {
+ for (AvatarAttribute attribute : attributes) {
+ if (attribute.getName().compareTo(_name) == 0) {
return attribute;
}
}
@@ -301,8 +300,8 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
}
public AvatarMethod getAvatarMethodWithName(String _name) {
- for(AvatarMethod method: methods) {
- if (method.getName().compareTo(_name)== 0) {
+ for (AvatarMethod method : methods) {
+ if (method.getName().compareTo(_name) == 0) {
return method;
}
}
@@ -324,8 +323,8 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
}
public AvatarBlock getBlockOfMethodWithName(String _name) {
- for(AvatarMethod method: methods) {
- if (method.getName().compareTo(_name)== 0) {
+ for (AvatarMethod method : methods) {
+ if (method.getName().compareTo(_name) == 0) {
return this;
}
}
@@ -338,8 +337,8 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
}
public AvatarSignal getAvatarSignalWithName(String _name) {
- for(AvatarSignal signal: signals) {
- if (signal.getName().compareTo(_name)== 0) {
+ for (AvatarSignal signal : signals) {
+ if (signal.getName().compareTo(_name) == 0) {
return signal;
}
}
@@ -351,7 +350,7 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
return null;
}
- public static boolean isAValidMethodCall (AvatarStateMachineOwner owner, String _s) {
+ public static boolean isAValidMethodCall(AvatarStateMachineOwner owner, String _s) {
int i;
//TraceManager.addDev("****** method=" + _s);
@@ -379,19 +378,19 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
return false;
}
- String params = _s.substring(index0+1, index1).trim();
+ String params = _s.substring(index0 + 1, index1).trim();
//TraceManager.addDev("params=" + params);
if (params.length() == 0) {
return am.getListOfAttributes().size() == 0;
}
//TraceManager.addDev("params=" + params);
- String [] actions = params.split(",");
+ String[] actions = params.split(",");
if (am.getListOfAttributes().size() != actions.length) {
return false;
}
AvatarAttribute aa;
- for(i=0; i<actions.length; i++) {
+ for (i = 0; i < actions.length; i++) {
//TraceManager.addDev("params=" + params + " actions=" + actions[i]);
// Must check tha validity of this action
@@ -420,20 +419,20 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
//TraceManager.addDev("Retparam=" + retparams);
// multiple params
- if (retparams.length()>0) {
+ if (retparams.length() > 0) {
if (retparams.charAt(0) == '(') {
- if (retparams.charAt(retparams.length()-1) != ')') {
+ if (retparams.charAt(retparams.length() - 1) != ')') {
//TraceManager.addDev("Bad format for return params: " + retparams);
return false;
}
- retparams = retparams.substring(1, retparams.length()-1).trim();
+ retparams = retparams.substring(1, retparams.length() - 1).trim();
actions = retparams.split(",");
if (am.getListOfReturnAttributes().size() != actions.length) {
return false;
}
- for(i=0; i<actions.length; i++) {
+ for (i = 0; i < actions.length; i++) {
//TraceManager.addDev("params=" + retparams + " actions=" + actions[i]);
aa = owner.getAvatarAttributeWithName(actions[i].trim());
if (aa == null) {
@@ -477,7 +476,7 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
AvatarAttribute value;
// Add new timer signals
- for (AvatarAttribute aa: attributes) {
+ for (AvatarAttribute aa : attributes) {
if (aa.getType() == AvatarType.TIMER) {
as = new AvatarSignal("set__" + aa.getName(), AvatarSignal.OUT, aa.getReferenceObject());
value = new AvatarAttribute("__myvalue", AvatarType.INTEGER, this, aa.getReferenceObject());
@@ -487,10 +486,10 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
addSignal(new AvatarSignal("expire__" + aa.getName(), AvatarSignal.IN, aa.getReferenceObject()));
// Create a timer block, and connect signals
- String blockName = "Timer__" + aa.getName() + "__" + getName();
- while( _spec.getBlockWithName(blockName) != null) {
- blockName += "_";
- }
+ String blockName = "Timer__" + aa.getName() + "__" + getName();
+ while (_spec.getBlockWithName(blockName) != null) {
+ blockName += "_";
+ }
AvatarBlock ab = AvatarBlockTemplate.getTimerBlock(blockName, _spec, getReferenceObject(), null, null, null);
_addedBlocks.add(ab);
@@ -514,25 +513,25 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
}
// Remove Timer attribute
- //boolean hasTimerAttribute = false;
+ //boolean hasTimerAttribute = false;
List<AvatarAttribute> tmps = attributes;
attributes = new LinkedList<AvatarAttribute>();
- for (AvatarAttribute aa: tmps) {
+ for (AvatarAttribute aa : tmps) {
if (aa.getType() != AvatarType.TIMER) {
attributes.add(aa);
} else {
- //hasTimerAttribute = true;
+ //hasTimerAttribute = true;
}
}
}
public boolean hasTimerAttribute() {
- for(AvatarAttribute attr: attributes) {
- if (attr.isTimer()) {
- return true;
- }
- }
- return false;
+ for (AvatarAttribute attr : attributes) {
+ if (attr.isTimer()) {
+ return true;
+ }
+ }
+ return false;
}
public AvatarAttribute addTimerAttribute(String _name) {
@@ -540,14 +539,14 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
AvatarAttribute aa;
int cpt;
- for(cpt=0; cpt<50000; cpt++) {
+ for (cpt = 0; cpt < 50000; cpt++) {
aa = getAvatarAttributeWithName(_name + cpt);
if (aa == null) {
break;
}
}
- aa = new AvatarAttribute(_name+cpt, AvatarType.TIMER, this, getReferenceObject());
+ aa = new AvatarAttribute(_name + cpt, AvatarType.TIMER, this, getReferenceObject());
addAttribute(aa);
return aa;
@@ -557,14 +556,14 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
AvatarAttribute aa;
int cpt;
- for(cpt=0; cpt<50000; cpt++) {
+ for (cpt = 0; cpt < 50000; cpt++) {
aa = getAvatarAttributeWithName(_name + cpt);
if (aa == null) {
break;
}
}
- aa = new AvatarAttribute(_name+cpt, AvatarType.INTEGER, this, getReferenceObject());
+ aa = new AvatarAttribute(_name + cpt, AvatarType.INTEGER, this, getReferenceObject());
addAttribute(aa);
return aa;
@@ -587,7 +586,7 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
}
if (asme instanceof AvatarTransition) {
- AvatarTransition at = (AvatarTransition)asme;
+ AvatarTransition at = (AvatarTransition) asme;
if (at.hasDelay() || at.hasCompute() || at.hasActions()) {
return true;
}
@@ -607,9 +606,9 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
int cpt = 0;
- for(AvatarStateMachineElement asme :asm.getListOfElements()) {
+ for (AvatarStateMachineElement asme : asm.getListOfElements()) {
if (asme instanceof AvatarActionOnSignal) {
- cpt = Math.max(cpt, ((AvatarActionOnSignal)asme).getNbOfValues());
+ cpt = Math.max(cpt, ((AvatarActionOnSignal) asme).getNbOfValues());
}
}
return cpt;
@@ -622,7 +621,7 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
int cpt = 1;
- for(AvatarStateMachineElement asme :asm.getListOfElements()) {
+ for (AvatarStateMachineElement asme : asm.getListOfElements()) {
if (asme instanceof AvatarState) {
cpt = Math.max(cpt, asme.nbOfNexts());
}
@@ -632,75 +631,95 @@ public class AvatarBlock extends AvatarElement implements AvatarStateMachineOwne
public int getIndexOfStartState() {
- if (asm == null) {
- return -1;
- }
+ if (asm == null) {
+ return -1;
+ }
+
+ return asm.getIndexOfStartState();
- return asm.getIndexOfStartState();
-
}
public int getIndexOfRealStartState() {
- if (asm == null) {
- return -1;
- }
+ if (asm == null) {
+ return -1;
+ }
- int cpt = 0;
- AvatarStateElement ase = asm.getStartState();
-
- while((ase != null) && (cpt<50)) {
- if (ase.getNexts().size() != 1) {
- break;
- }
+ int cpt = 0;
+ AvatarStateElement ase = asm.getStartState();
- AvatarTransition at = (AvatarTransition)(ase.getNext(0));
- if (!(at.isEmpty())) {
- break;
- }
+ while ((ase != null) && (cpt < 50)) {
+ if (ase.getNexts().size() != 1) {
+ break;
+ }
- if (ase.getNexts().size() != 1) {
- break;
- }
+ AvatarTransition at = (AvatarTransition) (ase.getNext(0));
+ if (!(at.isEmpty())) {
+ break;
+ }
+
+ if (ase.getNexts().size() != 1) {
+ break;
+ }
+
+ AvatarStateMachineElement next = at.getNext(0);
+ if (!(next instanceof AvatarStateElement)) {
+ break;
+ }
- AvatarStateMachineElement next = at.getNext(0);
- if (!(next instanceof AvatarStateElement)) {
- break;
- }
+ ase = (AvatarStateElement) next;
- ase = (AvatarStateElement) next;
+ cpt++;
+ }
+
+ if (ase != null) {
+ return asm.getIndexOfState(ase);
+ }
- cpt ++;
- }
+ return -1;
- if (ase != null) {
- return asm.getIndexOfState(ase);
- }
-
- return -1;
-
}
+ public ArrayList<AvatarElement> getAttributesOverMax(int maxV) {
+ ArrayList<AvatarElement> outside = new ArrayList<>();
+ for(AvatarAttribute aa: attributes) {
+ if (aa.isInt()) {
+ if (aa.hasInitialValue()) {
+ try {
+ int initialVal = Math.abs(Integer.decode(aa.getInitialValue()));
+ if (initialVal > maxV) {
+ outside.add(aa);
+ }
+ } catch (Exception e) {
+ outside.add(aa);
+ }
+ }
+ }
+ }
+ return outside;
+ }
+
+
@Override
public AvatarBlock advancedClone(AvatarSpecification avspec) {
- AvatarBlock av = new AvatarBlock(this.getName(), this.getAvatarSpecification(), this.getReferenceObject());
-
- cloneLinkToReferenceObjects(av);
-
-
- //Attributes, methods and signals
- for(AvatarAttribute aa: attributes) {
- av.addAttribute(aa.advancedClone(av));
- }
- for(AvatarMethod am: methods) {
- av.addMethod(am.advancedClone(av));
- }
- for(AvatarSignal as: signals) {
- av.addSignal(as.advancedClone(av));
- }
-
- // global code
- av.addGlobalCode(getGlobalCode());
-
- return av;
+ AvatarBlock av = new AvatarBlock(this.getName(), this.getAvatarSpecification(), this.getReferenceObject());
+
+ cloneLinkToReferenceObjects(av);
+
+
+ //Attributes, methods and signals
+ for (AvatarAttribute aa : attributes) {
+ av.addAttribute(aa.advancedClone(av));
+ }
+ for (AvatarMethod am : methods) {
+ av.addMethod(am.advancedClone(av));
+ }
+ for (AvatarSignal as : signals) {
+ av.addSignal(as.advancedClone(av));
+ }
+
+ // global code
+ av.addGlobalCode(getGlobalCode());
+
+ return av;
}
}
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index 91e39b0555af133e2a8a405ad419063873b03f34..3c0d34b11455419625845251b7863cdbbe5f169a 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -54,6 +54,8 @@ import java.util.ArrayList;
* @author Ludovic APVRILLE
*/
public class AvatarSpecification extends AvatarElement {
+
+ public final static int UPPAAL_MAX_INT = 32767;
public static String[] ops = {">", "<", "+", "-", "*", "/", "[", "]", "(", ")", ":", "=", "==", ",", "!", "?", "{", "}", "|", "&"};
diff --git a/src/main/java/avatartranslator/AvatarStateMachine.java b/src/main/java/avatartranslator/AvatarStateMachine.java
index b1130ebdb1bb51a9b61dda1d7bbf19a192484ff4..222c90d1f3f4c729bc3555a29cf64ac8c710f019 100644
--- a/src/main/java/avatartranslator/AvatarStateMachine.java
+++ b/src/main/java/avatartranslator/AvatarStateMachine.java
@@ -38,6 +38,7 @@
package avatartranslator;
+import myutil.MyMath;
import myutil.TraceManager;
import java.util.*;
@@ -1735,4 +1736,88 @@ public class AvatarStateMachine extends AvatarElement {
}
}
}
+
+ /**
+ * Looks for all numerical values over
+ * the provided max
+ *
+ * @param maxV Maximum value.
+ */
+ public ArrayList<AvatarElement> elementsWithNumericalValueOver(int maxV) {
+ String val;
+
+ ArrayList<AvatarElement> invalids = new ArrayList<AvatarElement>();
+
+ for(AvatarStateMachineElement asme: elements) {
+
+ // Action on signals
+ if (asme instanceof AvatarActionOnSignal) {
+ AvatarActionOnSignal aaos = (AvatarActionOnSignal)asme;
+ for(int i=0; i<aaos.getNbOfValues(); i++) {
+ val = aaos.getValue(i);
+ if (MyMath.hasIntegerValueOverMax(val, maxV)) {
+ invalids.add(this);
+ break;
+ }
+ }
+
+ }
+
+ if (asme instanceof AvatarRandom) {
+ AvatarRandom arand = (AvatarRandom)asme;
+ val = arand.getMinValue();
+ if (MyMath.hasIntegerValueOverMax(val, maxV)) {
+ invalids.add(this);
+ } else {
+ val = arand.getMaxValue();
+ if (MyMath.hasIntegerValueOverMax(val, maxV)) {
+ invalids.add(this);
+ }
+ }
+ }
+
+ if (asme instanceof AvatarSetTimer) {
+ AvatarSetTimer atop = (AvatarSetTimer)asme;
+ val = atop.getTimerValue();
+ if (MyMath.hasIntegerValueOverMax(val, maxV)) {
+ invalids.add(this);
+ }
+ }
+
+ if (asme instanceof AvatarTransition) {
+ AvatarTransition at = (AvatarTransition)asme;
+
+ // Guard
+ val = at.getGuard().toString();
+ if (MyMath.hasIntegerValueOverMax(val, maxV)) {
+ invalids.add(this);
+ }
+
+ // Delays
+ val = at.getMinDelay();
+ if (MyMath.hasIntegerValueOverMax(val, maxV)) {
+ invalids.add(this);
+ }
+ val = at.getMaxDelay();
+ if (MyMath.hasIntegerValueOverMax(val, maxV)) {
+ invalids.add(this);
+ }
+
+ // Actions
+ for(AvatarAction aa: at.getActions()) {
+ val = aa.toString();
+ if (MyMath.hasIntegerValueOverMax(val, maxV)) {
+ invalids.add(this);
+ }
+ }
+
+ }
+
+
+
+ }
+
+ return invalids;
+ }
+
}
diff --git a/src/main/java/avatartranslator/AvatarSyntaxChecker.java b/src/main/java/avatartranslator/AvatarSyntaxChecker.java
index a0b88ce198e8f79b923f8658d127b0819296115a..fcecce47da7b4fd06acd633c84980b6148b8f492 100644
--- a/src/main/java/avatartranslator/AvatarSyntaxChecker.java
+++ b/src/main/java/avatartranslator/AvatarSyntaxChecker.java
@@ -39,6 +39,7 @@
package avatartranslator;
import java.io.StringReader;
+import java.util.ArrayList;
import java.util.List;
import compiler.tmlparser.ParseException;
@@ -95,7 +96,14 @@ public class AvatarSyntaxChecker {
//return parse(_as, _ab, "guard", _guard);
}
+ /*
+ * @return 0 if ok, -1 if failure
+ */
public static int isAValidIntExpr(AvatarSpecification _as, AvatarStateMachineOwner _ab, String _expr) {
+
+ /*AvatarExpressionSolver e1 = new AvatarExpressionSolver("x + y");
+ e1.buildExpression(_ab);*/
+
if (_expr.trim().length() == 0) {
return 0;
}
@@ -117,8 +125,7 @@ public class AvatarSyntaxChecker {
}
return 0;
- // OLD return parse(_as, _ab, "actionnat", _expr);*/
-
+ // OLD return parse(_as, _ab, "actionnat", _expr);
}
@@ -277,4 +284,23 @@ public class AvatarSyntaxChecker {
return 0;
}
+
+
+ // Searches for numerical values over max
+ // @return list of AvatarElement not respecting this interval
+ public static ArrayList<AvatarElement> useOfInvalidUPPAALNumericalValues(AvatarSpecification _as, int maxV) {
+ ArrayList<AvatarElement> invalids = new ArrayList<AvatarElement>();
+
+ for(AvatarBlock ab: _as.getListOfBlocks()) {
+ // Check for attribute initial value
+ invalids.addAll(ab.getAttributesOverMax(maxV));
+
+ // Check operators of State machine
+ invalids.addAll(ab.getStateMachine().elementsWithNumericalValueOver(maxV));
+ }
+
+
+ return invalids;
+ }
+
}
diff --git a/src/main/java/avatartranslator/AvatarTimerOperator.java b/src/main/java/avatartranslator/AvatarTimerOperator.java
index 97db22c911f5eb3c56281599944974ca52be5973..4960eee9de32a01479edbfc8b1b97ca43064fbe3 100644
--- a/src/main/java/avatartranslator/AvatarTimerOperator.java
+++ b/src/main/java/avatartranslator/AvatarTimerOperator.java
@@ -1,26 +1,26 @@
/* 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,
@@ -31,46 +31,45 @@
* 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.
*/
-
-
package avatartranslator;
/**
* Class AvatarTimerOperator
* Creation: 15/07/2010
- * @version 1.0 15/07/2010
+ *
* @author Ludovic APVRILLE
+ * @version 1.0 15/07/2010
*/
public abstract class AvatarTimerOperator extends AvatarStateMachineElement {
- protected AvatarAttribute timer;
-
+ protected AvatarAttribute timer;
+
public AvatarTimerOperator(String _name, Object _referenceObject) {
super(_name, _referenceObject);
}
-
- public void setTimer(AvatarAttribute _timer) {
- timer = _timer;
- }
-
- public AvatarAttribute getTimer() {
- return timer;
- }
-
- public String specificToString() {
- if (timer != null) {
- return "\n timer: " + timer.getName();
- }
-
- return "";
- }
- public void translate (AvatarTranslator translator, Object arg) {
- translator.translateTimerOperator (this, arg);
+ public void setTimer(AvatarAttribute _timer) {
+ timer = _timer;
+ }
+
+ public AvatarAttribute getTimer() {
+ return timer;
+ }
+
+ public String specificToString() {
+ if (timer != null) {
+ return "\n timer: " + timer.getName();
}
+
+ return "";
+ }
+
+ public void translate(AvatarTranslator translator, Object arg) {
+ translator.translateTimerOperator(this, arg);
+ }
}
diff --git a/src/main/java/avatartranslator/directsimulation/AvatarSimulationBlock.java b/src/main/java/avatartranslator/directsimulation/AvatarSimulationBlock.java
index 1b2c58e0ea834d933587cfa8ebc9e6e069c073e0..f49bf322515f71106d5fd968586bf3c5b1a75a5b 100644
--- a/src/main/java/avatartranslator/directsimulation/AvatarSimulationBlock.java
+++ b/src/main/java/avatartranslator/directsimulation/AvatarSimulationBlock.java
@@ -40,6 +40,7 @@
package avatartranslator.directsimulation;
import avatartranslator.*;
+import avatartranslator.modelchecker.SpecificationBlock;
import myutil.*;
import java.util.Vector;
@@ -223,11 +224,11 @@ public class AvatarSimulationBlock {
AvatarTransition trans = (AvatarTransition) (aspt.elementToExecute);
aspt.probability = trans.getProbability();
if (trans.hasDelay()) {
- aspt.myMinDelay = evaluateIntExpression(trans.getMinDelay(), lastTransaction.attributeValues);
- aspt.myMaxDelay = evaluateIntExpression(trans.getMaxDelay(), lastTransaction.attributeValues);
+ aspt.myMinDelay = newEvaluateIntExpression(trans.getMinDelay(), lastTransaction.attributeValues);
+ aspt.myMaxDelay = newEvaluateIntExpression(trans.getMaxDelay(), lastTransaction.attributeValues);
aspt.hasDelay = true;
- aspt.extraParam1 = evaluateIntExpression(trans.getDelayExtra1(), lastTransaction.attributeValues);
- aspt.extraParam2 = evaluateIntExpression(trans.getDelayExtra2(), lastTransaction.attributeValues);
+ aspt.extraParam1 = newEvaluateIntExpression(trans.getDelayExtra1(), lastTransaction.attributeValues);
+ aspt.extraParam2 = newEvaluateIntExpression(trans.getDelayExtra2(), lastTransaction.attributeValues);
aspt.delayDistributionLaw = trans.getDelayDistributionLaw();
if (lastTransaction != null) {
if (lastTransaction.clockValueWhenFinished < _clockValue) {
@@ -240,8 +241,8 @@ public class AvatarSimulationBlock {
} else if (aspt.involvedElement instanceof AvatarTransition) {
AvatarTransition trans = (AvatarTransition) (aspt.involvedElement);
if (trans.hasDelay()) {
- aspt.myMinDelay = evaluateIntExpression(trans.getMinDelay(), lastTransaction.attributeValues);
- aspt.myMaxDelay = evaluateIntExpression(trans.getMaxDelay(), lastTransaction.attributeValues);
+ aspt.myMinDelay = newEvaluateIntExpression(trans.getMinDelay(), lastTransaction.attributeValues);
+ aspt.myMaxDelay = newEvaluateIntExpression(trans.getMaxDelay(), lastTransaction.attributeValues);
aspt.hasDelay = true;
aspt.extraParam1 = evaluateDoubleExpression(trans.getDelayExtra1(), lastTransaction.attributeValues);
aspt.extraParam2 = evaluateDoubleExpression(trans.getDelayExtra2(), lastTransaction.attributeValues);
@@ -394,8 +395,8 @@ public class AvatarSimulationBlock {
AvatarRandom random = (AvatarRandom) (_elt);
index = block.getIndexOfAvatarAttributeWithName(random.getVariable());
if (index > -1) {
- int valMin = evaluateIntExpression(random.getMinValue(), attributeValues);
- int valMax = evaluateIntExpression(random.getMaxValue(), attributeValues);
+ int valMin = newEvaluateIntExpression(random.getMinValue(), attributeValues);
+ int valMax = newEvaluateIntExpression(random.getMaxValue(), attributeValues);
double extra1;
try {
@@ -450,7 +451,7 @@ public class AvatarSimulationBlock {
result = "";
if (avat.getType() == AvatarType.INTEGER) {
//TraceManager.addDev("Evaluating expression, value=" + value);
- result += evaluateIntExpression(value, lastTransaction.attributeValues);
+ result += newEvaluateIntExpression(value, lastTransaction.attributeValues);
} else if (avat.getType() == AvatarType.BOOLEAN) {
result += evaluateBoolExpression(value, lastTransaction.attributeValues);
}
@@ -514,7 +515,7 @@ public class AvatarSimulationBlock {
avat = aaos.getSignal().getListOfAttributes().get(i);
result = "";
if (avat.getType() == AvatarType.INTEGER) {
- result += evaluateIntExpression(value, lastTransaction.attributeValues);
+ result += newEvaluateIntExpression(value, lastTransaction.attributeValues);
} else if (avat.getType() == AvatarType.BOOLEAN) {
result += evaluateBoolExpression(value, lastTransaction.attributeValues);
}
@@ -650,7 +651,7 @@ public class AvatarSimulationBlock {
// int or bool???
AvatarType type = block.getAttribute(indexVar).getType();
if (type == AvatarType.INTEGER) {
- int result = evaluateIntExpression(act, _attributeValues);
+ int result = newEvaluateIntExpression(act, _attributeValues);
_actions.add(nameOfVar + " = " + result);
_attributeValues.remove(indexVar);
_attributeValues.add(indexVar, "" + result);
@@ -705,6 +706,14 @@ public class AvatarSimulationBlock {
}
}
+ public int newEvaluateIntExpression(String _expr, Vector<String> _attributeValues) {
+ AvatarExpressionSolver e1 = new AvatarExpressionSolver(_expr);
+ SpecificationBlock sb = new SpecificationBlock(_attributeValues);
+ e1.buildExpression(block);
+ return e1.getResult(sb);
+
+ }
+
public int evaluateIntExpression(String _expr, Vector<String> _attributeValues) {
String act = _expr;
int cpt = 0;
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java b/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
index 517040496fd1d7b60ea3d17c01c1b5245ea7373c..e632831482d6ae0c184f2c506da4497c00c09a2e 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationBlock.java
@@ -40,6 +40,7 @@ package avatartranslator.modelchecker;
import java.util.Arrays;
import java.util.List;
+import java.util.Vector;
import avatartranslator.AvatarAttribute;
import avatartranslator.AvatarBlock;
@@ -69,6 +70,16 @@ public class SpecificationBlock {
public SpecificationBlock() {
}
+ public SpecificationBlock(Vector<String> _valuesOfVariables) {
+ values = new int[_valuesOfVariables.size()+3];
+ for(int i=0; i<_valuesOfVariables.size(); i++) {
+ try {
+ values[i + 3] = Integer.decode(_valuesOfVariables.get(i));
+ } catch (Exception e) {
+ }
+ }
+ }
+
public int getHash() {
return Arrays.hashCode(values);
}
diff --git a/src/main/java/myutil/MyMath.java b/src/main/java/myutil/MyMath.java
index da0def5cb4ce6d996b2245f8bf4c1a9cd392780f..1459a722350850bf091862d77eecf0504dc985e3 100644
--- a/src/main/java/myutil/MyMath.java
+++ b/src/main/java/myutil/MyMath.java
@@ -41,7 +41,12 @@
package myutil;
+import java.util.ArrayList;
+import java.util.List;
import java.util.Random;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
import org.apache.commons.math3.distribution.*;
/**
@@ -162,6 +167,46 @@ public class MyMath {
return val;
}
+ /**
+ * Extract the positive or negative int values from a String
+ *"-" is considered only as an unary operator
+ *
+ *
+ * @param s Input String
+ */
+ public static List<Integer> extractIntegerValues(String s) {
+ ArrayList<Integer> retList = new ArrayList<>();
+
+ Pattern p = Pattern.compile("-?\\d+");
+ Matcher m = p.matcher(s);
+ while (m.find()) {
+ try {
+ retList.add(Integer.decode(m.group()));
+ } catch (Exception e) {
+
+ }
+ }
+ return retList;
+ }
+
+ /**
+ * @param s Input String
+ * @param maxV Maximum of the interval. Expected to be higher than minV
+ * @return whether the provided String contains
+ * positive or negative int values outside
+ * of the input interval
+ */
+ public static boolean hasIntegerValueOverMax(String s, int maxV) {
+ List<Integer> listOfInt = extractIntegerValues(s);
+ for(Integer i: listOfInt) {
+ int v = Math.abs(i.intValue());
+ if (v > maxV) {
+ return true;
+ }
+ }
+ return false;
+ }
+
diff --git a/src/main/java/ui/AvatarDesignPanelTranslator.java b/src/main/java/ui/AvatarDesignPanelTranslator.java
index 85e2adfac41d7a6f4c97ed2dc47a814e0f544a6b..7e842ccf9ee45bbf1c0176dfffb10ad20940e12e 100644
--- a/src/main/java/ui/AvatarDesignPanelTranslator.java
+++ b/src/main/java/ui/AvatarDesignPanelTranslator.java
@@ -120,6 +120,22 @@ public class AvatarDesignPanelTranslator {
//TraceManager.addDev("Removing else guards");
as.removeElseGuards();
+
+
+ // Checking integer values
+ ArrayList<AvatarElement> listOfBadInt = AvatarSyntaxChecker.useOfInvalidUPPAALNumericalValues(as, AvatarSpecification.UPPAAL_MAX_INT);
+ // Adding warnings for each element
+ for(AvatarElement ae: listOfBadInt) {
+ UICheckingError ce = new UICheckingError(CheckingError.STRUCTURE_ERROR, "Integer expression outside UPPAAL range: " +
+ ae.toString() +
+ "-> UPPAAL verification may fail");
+ ce.setTDiagramPanel(adp.getAvatarBDPanel());
+ if (ae.getReferenceObject() instanceof TGComponent) {
+ ce.setTGComponent((TGComponent)ae.getReferenceObject());
+ }
+ addWarning(ce);
+ }
+
//TraceManager.addDev("Removing else guards ... done");
//System.out.println(as.toString());
adp.abdp.repaint();
diff --git a/src/main/java/ui/TAttribute.java b/src/main/java/ui/TAttribute.java
index 498e4155be691e320989b578552300a0e91bba2e..cc6abeba995ca3b5342fe869bdec7671bc4102f8 100644
--- a/src/main/java/ui/TAttribute.java
+++ b/src/main/java/ui/TAttribute.java
@@ -277,7 +277,8 @@ public class TAttribute {
}
return val > 0;
case INTEGER:
- return value.matches("\\d*");
+ //return value.matches("-?\\d+");
+ return value.matches("\\d+");
case TIMER:
return ((value == null) || (value.equals("")));
default:
diff --git a/src/main/java/ui/window/JDialogAvatarBlock.java b/src/main/java/ui/window/JDialogAvatarBlock.java
index b43fa830d448a79c2d3622daca0b8c588af22c50..9eb142d2b754a561b1b8d4de73c957d3713259f4 100644
--- a/src/main/java/ui/window/JDialogAvatarBlock.java
+++ b/src/main/java/ui/window/JDialogAvatarBlock.java
@@ -41,6 +41,7 @@ package ui.window;
import myutil.Conversion;
import myutil.GraphicLib;
+import myutil.TraceManager;
import ui.AvatarMethod;
import ui.AvatarSignal;
import ui.TAttribute;
@@ -751,6 +752,8 @@ public class JDialogAvatarBlock extends JDialogBase implements ActionListener, L
int i = TAttribute.getAccess(o1.toString());
int j = TAttribute.getAvatarType(o2.toString());
+ TraceManager.addDev("Type=" + o2.toString());
+
if ((j == TAttribute.ARRAY_NAT) && (value.length() < 1)) {
value = "2";
}