Commit 1dc35a12 authored by Ludovic Apvrille's avatar Ludovic Apvrille
Browse files

Resolving bug on complex int expression. Thanks to Florian Lugou

parent 7c73bffa
/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille /* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
* *
* ludovic.apvrille AT enst.fr * ludovic.apvrille AT enst.fr
* *
* This software is a computer program whose purpose is to allow the * This software is a computer program whose purpose is to allow the
* edition of TURTLE analysis, design and deployment diagrams, to * edition of TURTLE analysis, design and deployment diagrams, to
* allow the generation of RT-LOTOS or Java code from this diagram, * allow the generation of RT-LOTOS or Java code from this diagram,
* and at last to allow the analysis of formal validation traces * and at last to allow the analysis of formal validation traces
* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
* from INRIA Rhone-Alpes. * from INRIA Rhone-Alpes.
* *
* This software is governed by the CeCILL license under French law and * This software is governed by the CeCILL license under French law and
* abiding by the rules of distribution of free software. You can use, * abiding by the rules of distribution of free software. You can use,
* modify and/ or redistribute the software under the terms of the CeCILL * modify and/ or redistribute the software under the terms of the CeCILL
* license as circulated by CEA, CNRS and INRIA at the following URL * license as circulated by CEA, CNRS and INRIA at the following URL
* "http://www.cecill.info". * "http://www.cecill.info".
* *
* As a counterpart to the access to the source code and rights to copy, * 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 * modify and redistribute granted by the license, users are provided only
* with a limited warranty and the software's author, the holder of the * with a limited warranty and the software's author, the holder of the
* economic rights, and the successive licensors have only limited * economic rights, and the successive licensors have only limited
* liability. * liability.
* *
* In this respect, the user's attention is drawn to the risks associated * In this respect, the user's attention is drawn to the risks associated
* with loading, using, modifying and/or developing or reproducing the * with loading, using, modifying and/or developing or reproducing the
* software by the user in light of its specific status of free software, * software by the user in light of its specific status of free software,
...@@ -31,174 +31,183 @@ ...@@ -31,174 +31,183 @@
* requirements in conditions enabling the security of their systems and/or * 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 * data to be ensured and, more generally, to use and operate it in the
* same conditions as regards security. * same conditions as regards security.
* *
* The fact that you are presently reading this means that you have had * The fact that you are presently reading this means that you have had
* knowledge of the CeCILL license and that you accept its terms. * knowledge of the CeCILL license and that you accept its terms.
*/ */
package avatartranslator; package avatartranslator;
import java.util.Map;
import myutil.Conversion; import myutil.Conversion;
import myutil.TraceManager; import myutil.TraceManager;
import java.util.Map;
/** /**
* Class AvatarGuard * Class AvatarGuard
* Creation: 16/09/2015 * Creation: 16/09/2015
* @version 1.0 16/09/2015 *
* @author Florian LUGOU * @author Florian LUGOU
* @version 1.0 16/09/2015
*/ */
public abstract class AvatarGuard { public abstract class AvatarGuard {
public static int getMatchingRParen (String s, int indexLParen) { public static int getMatchingRParen(String s, int indexLParen) {
int index, n; int index, n;
n = 1; n = 1;
for (index = indexLParen+1; index < s.length (); index++) { for (index = indexLParen + 1; index < s.length(); index++) {
if (s.charAt (index) == '(') if (s.charAt(index) == '(')
n ++; n++;
else if (s.charAt (index) == ')') else if (s.charAt(index) == ')')
n--; n--;
if (n == 0) if (n == 0)
break; return index;
} }
return index; return -1;
} }
public static AvatarGuard createFromString (AvatarStateMachineOwner block, String _guard) { public static AvatarGuard createFromString(AvatarStateMachineOwner block, String _guard) {
if (_guard == null) if (_guard == null)
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
String sane = AvatarGuard.sanitizeString (_guard); String sane = AvatarGuard.sanitizeString(_guard);
if (sane.isEmpty ()) if (sane.isEmpty())
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
if (sane.toLowerCase ().equals ("else")) if (sane.toLowerCase().equals("else"))
return new AvatarGuardElse (); return new AvatarGuardElse();
int indexRParen = 0; int indexRParen = 0;
AvatarTuple tuple = null; AvatarTuple tuple = null;
AvatarGuard first = null; AvatarGuard first = null;
if (sane.startsWith ("not(")) { if (sane.startsWith("not(")) {
indexRParen = AvatarGuard.getMatchingRParen (sane, 3); indexRParen = AvatarGuard.getMatchingRParen(sane, 3);
first = AvatarGuard.createFromString (block, sane.substring (4, indexRParen)); if (indexRParen < 0) {
TraceManager.addDev("Invalid guard expression with tuple " + sane);
return new AvatarGuardEmpty();
}
first = AvatarGuard.createFromString(block, sane.substring(4, indexRParen));
if (indexRParen >= sane.length ()-1) { if (indexRParen >= sane.length() - 1) {
if (first instanceof AvatarComposedGuard) if (first instanceof AvatarComposedGuard)
return new AvatarUnaryGuard ("not", "(", ")", (AvatarComposedGuard) first); return new AvatarUnaryGuard("not", "(", ")", (AvatarComposedGuard) first);
else { else {
TraceManager.addDev("Could not create unary guard "+ sane); TraceManager.addDev("Could not create unary guard " + sane);
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
} }
} }
} }
if (sane.startsWith ("(")) { if (sane.startsWith("(")) {
indexRParen = AvatarGuard.getMatchingRParen (sane, 0); indexRParen = AvatarGuard.getMatchingRParen(sane, 0);
tuple = AvatarTuple.createFromString (block, sane.substring (0, indexRParen)); if (indexRParen < 0) {
TraceManager.addDev("Invalid guard expression with tuple " + sane);
return new AvatarGuardEmpty();
}
tuple = AvatarTuple.createFromString(block, sane.substring(0, indexRParen));
if (tuple == null) { if (tuple == null) {
first = AvatarGuard.createFromString (block, sane.substring (1, indexRParen)); first = AvatarGuard.createFromString(block, sane.substring(1, indexRParen));
if (indexRParen == sane.length ()-1) { if (indexRParen == sane.length() - 1) {
if (first instanceof AvatarComposedGuard) if (first instanceof AvatarComposedGuard)
return new AvatarUnaryGuard ("", "(", ")", (AvatarComposedGuard) first); return new AvatarUnaryGuard("", "(", ")", (AvatarComposedGuard) first);
else { else {
TraceManager.addDev("Unary guard "+ sane + " does not contain guard"); TraceManager.addDev("Unary guard " + sane + " does not contain guard");
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
} }
} else { } else {
int indexLParen = sane.indexOf ("(", indexRParen); int indexLParen = sane.indexOf("(", indexRParen);
if (indexLParen == -1) if (indexLParen == -1)
indexLParen = indexRParen; indexLParen = indexRParen;
for (String delim: new String[] {"and", "or"}) { for (String delim : new String[]{"and", "or"}) {
int indexBinaryOp = sane.substring (0, indexLParen).indexOf (delim, indexRParen+1); int indexBinaryOp = sane.substring(0, indexLParen).indexOf(delim, indexRParen + 1);
if (indexBinaryOp != -1) { if (indexBinaryOp != -1) {
first = AvatarGuard.createFromString (block, sane.substring (0, indexBinaryOp)); first = AvatarGuard.createFromString(block, sane.substring(0, indexBinaryOp));
AvatarGuard second = AvatarGuard.createFromString (block, sane.substring (indexBinaryOp + delim.length ())); AvatarGuard second = AvatarGuard.createFromString(block, sane.substring(indexBinaryOp + delim.length()));
if (first instanceof AvatarComposedGuard && second instanceof AvatarComposedGuard) if (first instanceof AvatarComposedGuard && second instanceof AvatarComposedGuard)
return new AvatarBinaryGuard ((AvatarComposedGuard) first, (AvatarComposedGuard) second, delim); return new AvatarBinaryGuard((AvatarComposedGuard) first, (AvatarComposedGuard) second, delim);
TraceManager.addDev("Binary guard "+ sane + "does not contain 2 guards"); TraceManager.addDev("Binary guard " + sane + "does not contain 2 guards");
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
} }
} }
TraceManager.addDev("Invalid guard "+ sane); TraceManager.addDev("Invalid guard " + sane);
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
} }
} else if (tuple.getComponents().size()==1){ } else if (tuple.getComponents().size() == 1) {
first = AvatarGuard.createFromString (block, sane.substring (1, indexRParen)); first = AvatarGuard.createFromString(block, sane.substring(1, indexRParen));
if (indexRParen == sane.length ()-1) { if (indexRParen == sane.length() - 1) {
if (first instanceof AvatarComposedGuard) if (first instanceof AvatarComposedGuard)
return new AvatarUnaryGuard ("", "(", ")", (AvatarComposedGuard) first); return new AvatarUnaryGuard("", "(", ")", (AvatarComposedGuard) first);
else { else {
TraceManager.addDev("Unary guard "+ sane + " does not contain guard"); TraceManager.addDev("Unary guard " + sane + " does not contain guard");
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
} }
} }
int indexLParen = sane.indexOf ("(", indexRParen); int indexLParen = sane.indexOf("(", indexRParen);
if (indexLParen == -1) if (indexLParen == -1)
indexLParen = indexRParen; indexLParen = indexRParen;
for (String delim: new String[] {"and", "or", "&&", "||"}) { for (String delim : new String[]{"and", "or", "&&", "||"}) {
int indexBinaryOp = sane.substring (0, indexLParen).indexOf (delim, indexRParen+1); int indexBinaryOp = sane.substring(0, indexLParen).indexOf(delim, indexRParen + 1);
if (indexBinaryOp != -1) { if (indexBinaryOp != -1) {
first = AvatarGuard.createFromString (block, sane.substring (0, indexBinaryOp)); first = AvatarGuard.createFromString(block, sane.substring(0, indexBinaryOp));
AvatarGuard second = AvatarGuard.createFromString (block, sane.substring (indexBinaryOp + delim.length ())); AvatarGuard second = AvatarGuard.createFromString(block, sane.substring(indexBinaryOp + delim.length()));
if (first instanceof AvatarComposedGuard && second instanceof AvatarComposedGuard) if (first instanceof AvatarComposedGuard && second instanceof AvatarComposedGuard)
return new AvatarBinaryGuard ((AvatarComposedGuard) first, (AvatarComposedGuard) second, delim); return new AvatarBinaryGuard((AvatarComposedGuard) first, (AvatarComposedGuard) second, delim);
TraceManager.addDev("Binary guard "+ sane + "does not contain 2 guards"); TraceManager.addDev("Binary guard " + sane + "does not contain 2 guards");
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
} }
} }
TraceManager.addDev("Invalid guard "+ sane); TraceManager.addDev("Invalid guard " + sane);
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
} else { } else {
int indexLParen = sane.indexOf ("(", indexRParen); int indexLParen = sane.indexOf("(", indexRParen);
if (indexLParen == -1) if (indexLParen == -1)
indexLParen = indexRParen; indexLParen = indexRParen;
for (String delim: new String[] {"==", "!="}) { for (String delim : new String[]{"==", "!="}) {
int indexBinaryOp = sane.substring (0, indexLParen).indexOf (delim, indexRParen+1); int indexBinaryOp = sane.substring(0, indexLParen).indexOf(delim, indexRParen + 1);
if (indexBinaryOp != -1) { if (indexBinaryOp != -1) {
AvatarTerm secondTerm = AvatarTerm.createFromString (block, sane.substring (indexBinaryOp + delim.length ())); AvatarTerm secondTerm = AvatarTerm.createFromString(block, sane.substring(indexBinaryOp + delim.length()));
if (secondTerm != null) if (secondTerm != null)
return new AvatarSimpleGuardDuo (tuple, secondTerm, delim); return new AvatarSimpleGuardDuo(tuple, secondTerm, delim);
TraceManager.addDev("Could not find term in guard "+ sane); TraceManager.addDev("Could not find term in guard " + sane);
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
} }
} }
TraceManager.addDev("Invalid guard expression with tuple "+ sane); TraceManager.addDev("Invalid guard expression with tuple " + sane);
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
} }
} }
for (String delim: new String[] {"==", "!=", "<=", ">=", "<", ">"}) { for (String delim : new String[]{"==", "!=", "<=", ">=", "<", ">"}) {
int indexBinaryOp = sane.indexOf (delim); int indexBinaryOp = sane.indexOf(delim);
if (indexBinaryOp != -1) { if (indexBinaryOp != -1) {
AvatarTerm firstTerm = AvatarTerm.createFromString (block, sane.substring (0, indexBinaryOp)); AvatarTerm firstTerm = AvatarTerm.createFromString(block, sane.substring(0, indexBinaryOp));
AvatarTerm secondTerm = AvatarTerm.createFromString (block, sane.substring (indexBinaryOp + delim.length ())); AvatarTerm secondTerm = AvatarTerm.createFromString(block, sane.substring(indexBinaryOp + delim.length()));
if (secondTerm != null && firstTerm != null) if (secondTerm != null && firstTerm != null)
return new AvatarSimpleGuardDuo (firstTerm, secondTerm, delim); return new AvatarSimpleGuardDuo(firstTerm, secondTerm, delim);
// TraceManager.addDev("Term in guard does not exist " +sane.substring (0, indexBinaryOp) + " "+ sane.substring (indexBinaryOp + delim.length ())); // TraceManager.addDev("Term in guard does not exist " +sane.substring (0, indexBinaryOp) + " "+ sane.substring (indexBinaryOp + delim.length ()));
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
} }
} }
AvatarTerm term = AvatarTerm.createFromString (block, sane); AvatarTerm term = AvatarTerm.createFromString(block, sane);
if (term != null) if (term != null)
return new AvatarSimpleGuardMono (term); return new AvatarSimpleGuardMono(term);
// TODO: add warning // TODO: add warning
TraceManager.addDev("Could not parse guard '" + sane + "'. Replacing by an empty guard."); TraceManager.addDev("Could not parse guard '" + sane + "'. Replacing by an empty guard.");
return new AvatarGuardEmpty (); return new AvatarGuardEmpty();
} }
private static String sanitizeString (String s) { private static String sanitizeString(String s) {
String result = Conversion.replaceAllChar(s, ' ', "").trim(); String result = Conversion.replaceAllChar(s, ' ', "").trim();
result = Conversion.replaceAllChar(result, '[', ""); result = Conversion.replaceAllChar(result, '[', "");
result = Conversion.replaceAllChar(result, ']', ""); result = Conversion.replaceAllChar(result, ']', "");
...@@ -207,31 +216,31 @@ public abstract class AvatarGuard { ...@@ -207,31 +216,31 @@ public abstract class AvatarGuard {
} }
public static AvatarGuard addGuard(AvatarGuard _guard, AvatarGuard _g, String _binaryOp) { public static AvatarGuard addGuard(AvatarGuard _guard, AvatarGuard _g, String _binaryOp) {
if (_g == null || ! (_g instanceof AvatarComposedGuard) || ! (_guard instanceof AvatarComposedGuard)) if (_g == null || !(_g instanceof AvatarComposedGuard) || !(_guard instanceof AvatarComposedGuard))
return _guard; return _guard;
return new AvatarBinaryGuard (new AvatarUnaryGuard ("", "(", ")", (AvatarComposedGuard) _guard), return new AvatarBinaryGuard(new AvatarUnaryGuard("", "(", ")", (AvatarComposedGuard) _guard),
new AvatarUnaryGuard ("", "(", ")", (AvatarComposedGuard) _g), new AvatarUnaryGuard("", "(", ")", (AvatarComposedGuard) _g),
_binaryOp); _binaryOp);
} }
public AvatarGuard getRealGuard (AvatarStateMachineElement precedent) { public AvatarGuard getRealGuard(AvatarStateMachineElement precedent) {
return this; return this;
} }
public boolean isElseGuard () { public boolean isElseGuard() {
return false; return false;
} }
public boolean isGuarded () { public boolean isGuarded() {
return true; return true;
} }
public abstract String getAsString (AvatarSyntaxTranslator translator); public abstract String getAsString(AvatarSyntaxTranslator translator);
@Override @Override
public String toString () { public String toString() {
return this.getAsString (new AvatarSyntaxTranslator ()); return this.getAsString(new AvatarSyntaxTranslator());
} }
/** /**
...@@ -239,13 +248,12 @@ public abstract class AvatarGuard { ...@@ -239,13 +248,12 @@ public abstract class AvatarGuard {
* *
* @return A clone of the guard. * @return A clone of the guard.
*/ */
public abstract AvatarGuard clone (); public abstract AvatarGuard clone();
/** /**
* Replaces attributes in this guard according to the provided mapping. * Replaces attributes in this guard according to the provided mapping.
* *
* @param attributesMapping * @param attributesMapping The mapping used to replace the attributes of the guard. All the attributes of the block should be present as keys.
* The mapping used to replace the attributes of the guard. All the attributes of the block should be present as keys.
*/ */
public abstract void replaceAttributes( Map<AvatarAttribute, AvatarAttribute> attributesMapping); public abstract void replaceAttributes(Map<AvatarAttribute, AvatarAttribute> attributesMapping);
} }
...@@ -64,12 +64,14 @@ public class AvatarTuple extends AvatarLeftHand { ...@@ -64,12 +64,14 @@ public class AvatarTuple extends AvatarLeftHand {
if (toParse.trim().startsWith("(")) { if (toParse.trim().startsWith("(")) {
int indexLParen = toParse.indexOf ("("); int indexLParen = toParse.indexOf ("(");
int indexRParen = AvatarGuard.getMatchingRParen (toParse, indexLParen); int indexRParen = AvatarGuard.getMatchingRParen (toParse, indexLParen);
if (indexRParen < 0)
return null;
String[] components = toParse.substring (indexLParen+1, indexRParen).trim().split (","); String[] components = toParse.substring (indexLParen+1, indexRParen).trim().split (",");
boolean illFormed = false; boolean illFormed = false;
AvatarTuple argsTuple = new AvatarTuple (block); AvatarTuple argsTuple = new AvatarTuple (block);
for (String arg: components) { for (String arg: components) {
if (!arg.isEmpty()) { if (!arg.isEmpty()) {
TraceManager.addDev("In for with arg=" + arg+"|"); //TraceManager.addDev("In for with arg=" + arg+"|");
AvatarTerm t = AvatarTerm.createFromString (block, arg); AvatarTerm t = AvatarTerm.createFromString (block, arg);
if (t == null) { if (t == null) {
// Term couldn't be parsed // Term couldn't be parsed
......
...@@ -41,6 +41,7 @@ package cli; ...@@ -41,6 +41,7 @@ package cli;
import common.ConfigurationTTool; import common.ConfigurationTTool;
import launcher.RTLLauncher; import launcher.RTLLauncher;
import myutil.Conversion;
import myutil.IntExpressionEvaluator; import myutil.IntExpressionEvaluator;
import myutil.PluginManager; import myutil.PluginManager;
import myutil.TraceManager; import myutil.TraceManager;
...@@ -108,11 +109,26 @@ public class TestSpecific extends Command { ...@@ -108,11 +109,26 @@ public class TestSpecific extends Command {
at.addAction(command); at.addAction(command);
IntExpressionEvaluator iee = new IntExpressionEvaluator(); IntExpressionEvaluator iee = new IntExpressionEvaluator();
iee.getResultOf(at.getAction(0).toString());
double result = iee.getResultOf(command);
System.out.println("Value of x=" + x.getInitialValue() + " y=" + y.getInitialValue() + " z=" +z.getInitialValue()); System.out.println("Value of x=" + x.getInitialValue() + " y=" + y.getInitialValue() + " z=" +z.getInitialValue());
System.out.println("Result =" + result); String expr = at.getAction(0).toString();
int index = expr.indexOf('=');
if (index == -1) {
System.out.println("Invalid expr");
return "Test failed no '=' in assignation";
}
expr = expr.substring(index+1, expr.length()).trim();
System.out.println("Evaluating: " + expr);
for(AvatarAttribute aa: block.getAttributes()) {
expr = Conversion.putVariableValueInString(AvatarSpecification.ops, expr, aa.getName(), aa.getInitialValue());
}
System.out.println("Evaluating: " + expr);
double result = iee.getResultOf(expr);
System.out.println("Result = " + result);
return null; return null;
} catch (Exception e) { } catch (Exception e) {
......
...@@ -84,15 +84,14 @@ public class IntExpressionEvaluator { ...@@ -84,15 +84,14 @@ public class IntExpressionEvaluator {
double d = parseExpression(); double d = parseExpression();
if ((errorMessage == null) && (nbOpen!=0)) { if ((errorMessage == null) && (nbOpen!=0)) {
errorMessage = "Badly placed parenthesis"; errorMessage = "Badly placed parenthesis";
} }
if (errorMessage != null) { if (errorMessage != null) {
TraceManager.addDev("Expr contains an error:" + errorMessage + " expr=" + _expr); TraceManager.addDev("Expr contains an error: " + errorMessage + " for expr:" + _expr);
} else { } else {
//TraceManager.addDev("Expr is correct"); TraceManager.addDev("Expr is correct");
} }
return d; return d;
...@@ -221,7 +220,7 @@ public class IntExpressionEvaluator { ...@@ -221,7 +220,7 @@ public class IntExpressionEvaluator {
// <rootexp> ::= number // <rootexp> ::= number
else if (currentType==NUMBER_TOKEN){ else if (currentType == NUMBER_TOKEN){
result = currentValue; result = currentValue;
if (errorMessage != null) return result; if (errorMessage != null) return result;
match(NUMBER_TOKEN); match(NUMBER_TOKEN);
...@@ -230,7 +229,7 @@ public class IntExpressionEvaluator { ...@@ -230,7 +229,7 @@ public class IntExpressionEvaluator {
else { else {
errorMessage = errorMessage =
"Expected a number or a parenthesis."; "Expected a number or a parenthesis for currentType = " + currentType;
} }
return result; return result;
...@@ -255,7 +254,7 @@ public class IntExpressionEvaluator { ...@@ -255,7 +254,7 @@ public class IntExpressionEvaluator {
char c1 = s.charAt(0); char c1 = s.charAt(0);