diff --git a/src/main/java/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java index 8be746878a4f9676f2f3cd9139efca6f312dd3eb..5fb16200dc1d823acdb393184d270d7f1bfde9fa 100644 --- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java +++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java @@ -55,65 +55,26 @@ public class AvatarExpressionAttribute { private int accessIndex; private AvatarStateMachineElement state; private String s; - private boolean isNegated; - private boolean isNot; private boolean isState; private boolean error; public AvatarExpressionAttribute(AvatarSpecification spec, String s) { this.s = s; - isNegated = false; - isNot = false; isState = false; - if (s.startsWith("not(")) { - //not(variable) - isNot = true; - this.s = s.substring(3).trim(); - while (this.s.startsWith("(") && this.s.endsWith(")")){ - this.s = this.s.substring(1, this.s.length() - 1); - } - } - if (s.startsWith("-")) { - //not(variable) - isNegated = true; - this.s = s.substring(1).trim(); - } - error = !initAttributes(spec); } public AvatarExpressionAttribute(AvatarBlock block, String s) { this.s = s; - isNegated = false; - isNot = false; isState = false; - if (s.startsWith("not(")) { - //not(variable) - isNot = true; - this.s = s.substring(3).trim(); - while (this.s.startsWith("(") && this.s.endsWith(")")){ - this.s = this.s.substring(1, this.s.length() - 1); - } - } - if (s.startsWith("-")) { - //not(variable) - isNegated = true; - this.s = s.substring(1).trim(); - while (this.s.startsWith("(") && this.s.endsWith(")")){ - this.s = this.s.substring(1, this.s.length() - 1); - } - } - error = !initAttributes(block); } public AvatarExpressionAttribute(AvatarBlock block, AvatarStateMachineElement asme) { this.s = asme.name; - isNegated = false; - isNot = false; isState = true; state = asme; error = false; @@ -197,12 +158,6 @@ public class AvatarExpressionAttribute { value = ss.blocks[blockIndex].values[accessIndex]; - if (isNot) { - value = (value == 0) ? 1 : 0; - } else if (isNegated) { - value = -value; - } - return value; } @@ -215,12 +170,6 @@ public class AvatarExpressionAttribute { value = ss.blocks[blockIndex].values[accessIndex]; - if (isNot) { - value = (value == 0) ? 1 : 0; - } else if (isNegated) { - value = -value; - } - return value; } @@ -233,12 +182,6 @@ public class AvatarExpressionAttribute { value = sb.values[accessIndex]; - if (isNot) { - value = (value == 0) ? 1 : 0; - } else if (isNegated) { - value = -value; - } - return value; } @@ -251,12 +194,6 @@ public class AvatarExpressionAttribute { v = value; - if (isNot) { - v = (value == 0) ? 1 : 0; - } else if (isNegated) { - v = -value; - } - ss.blocks[blockIndex].values[accessIndex] = v; } @@ -269,12 +206,6 @@ public class AvatarExpressionAttribute { v = value; - if (isNot) { - v = (value == 0) ? 1 : 0; - } else if (isNegated) { - v = -value; - } - sb.values[accessIndex] = v; } @@ -283,16 +214,7 @@ public class AvatarExpressionAttribute { } public String toString() { - String res = ""; - if (isNot) { - res = "not(" + this.s + ")"; - } else if (isNegated) { - res += "-" + this.s; - } else { - res = s; - } - - return res; + return s; } } diff --git a/src/main/java/avatartranslator/AvatarExpressionSolver.java b/src/main/java/avatartranslator/AvatarExpressionSolver.java index 3d65f749cedf9fa500e6b3730220d3b05172e9e2..9867e120d65c9289402f92679ef1616f43df4f48 100644 --- a/src/main/java/avatartranslator/AvatarExpressionSolver.java +++ b/src/main/java/avatartranslator/AvatarExpressionSolver.java @@ -95,9 +95,12 @@ public class AvatarExpressionSolver { removeUselessBrackets(); - if (!expression.matches("^.+[\\+\\-<>=&\\|\\*/].*$")) { + if (!expression.matches("^.+[\\+\\-<>=:;\\$&\\|\\*/].*$")) { // leaf isLeaf = true; + checkNot(); + checkNegated(); + checkNegatedNoBrackets(); if (expression.equals("true")) { intValue = 1; isImmediateValue = IMMEDIATE_INT; @@ -120,32 +123,11 @@ public class AvatarExpressionSolver { isLeaf = false; - if (expression.startsWith("not(")) { - //not bracket must be closed in the last char - int closingIndex = getClosingBracket(4); - - if (closingIndex == -1) { - return false; - } - if (closingIndex == expression.length() - 1) { - //not(expression) - isNot = true; - expression = expression.substring(4, expression.length() - 1).trim(); - } - } + returnVal = checkNot(); + returnVal &= checkNegated(); - if (expression.startsWith("-(")) { - //not bracket must be closed in the last char - int closingIndex = getClosingBracket(4); - - if (closingIndex == -1) { - return false; - } - if (closingIndex == expression.length() - 1) { - //not(expression) - isNot = true; - expression = expression.substring(2, expression.length() - 1).trim(); - } + if (!returnVal) { + return false; } int index = getOperatorIndex(); @@ -174,9 +156,12 @@ public class AvatarExpressionSolver { removeUselessBrackets(); - if (!expression.matches("^.+[\\+\\-<>=&\\*/].*$")) { + if (!expression.matches("^.+[\\+\\-<>=:;\\$&\\|\\*/].*$")) { // leaf isLeaf = true; + checkNot(); + checkNegated(); + checkNegatedNoBrackets(); if (expression.equals("true")) { intValue = 1; isImmediateValue = IMMEDIATE_INT; @@ -199,32 +184,11 @@ public class AvatarExpressionSolver { isLeaf = false; - if (expression.startsWith("not(")) { - //not bracket must be closed in the last char - int closingIndex = getClosingBracket(4); - - if (closingIndex == -1) { - return false; - } - if (closingIndex == expression.length() - 1) { - //not(expression) - isNot = true; - expression = expression.substring(4, expression.length() - 1).trim(); - } - } + returnVal = checkNot(); + returnVal &= checkNegated(); - if (expression.startsWith("-(")) { - //not bracket must be closed in the last char - int closingIndex = getClosingBracket(4); - - if (closingIndex == -1) { - return false; - } - if (closingIndex == expression.length() - 1) { - //not(expression) - isNot = true; - expression = expression.substring(2, expression.length() - 1).trim(); - } + if (!returnVal) { + return false; } int index = getOperatorIndex(); @@ -261,9 +225,12 @@ public class AvatarExpressionSolver { removeUselessBrackets(); - if (!expression.matches("^.+[\\+\\-<>=&\\*/].*$")) { + if (!expression.matches("^.+[\\+\\-<>=:;\\$&\\|\\*/].*$")) { // leaf isLeaf = true; + checkNot(); + checkNegated(); + checkNegatedNoBrackets(); if (expression.equals("true")) { intValue = 1; isImmediateValue = IMMEDIATE_INT; @@ -285,32 +252,11 @@ public class AvatarExpressionSolver { isLeaf = false; - if (expression.startsWith("not(")) { - //not bracket must be closed in the last char - int closingIndex = getClosingBracket(4); - - if (closingIndex == -1) { - return false; - } - if (closingIndex == expression.length() - 1) { - //not(expression) - isNot = true; - expression = expression.substring(4, expression.length() - 1).trim(); - } - } + returnVal = checkNot(); + returnVal &= checkNegated(); - if (expression.startsWith("-(")) { - //not bracket must be closed in the last char - int closingIndex = getClosingBracket(4); - - if (closingIndex == -1) { - return false; - } - if (closingIndex == expression.length() - 1) { - //not(expression) - isNot = true; - expression = expression.substring(2, expression.length() - 1).trim(); - } + if (!returnVal) { + return false; } int index = getOperatorIndex(); @@ -347,6 +293,48 @@ public class AvatarExpressionSolver { //expression.replaceAll("\\bfalse\\b", "f").trim(); } + private boolean checkNot() { + if (expression.startsWith("not(")) { + //not bracket must be closed in the last char + int closingIndex = getClosingBracket(4); + + if (closingIndex == -1) { + return false; + } + if (closingIndex == expression.length() - 1) { + //not(expression) + isNot = true; + expression = expression.substring(4, expression.length() - 1).trim(); + } + } + return true; + } + + private boolean checkNegated() { + if (expression.startsWith("-(")) { + //not bracket must be closed in the last char + int closingIndex = getClosingBracket(2); + + if (closingIndex == -1) { + return false; + } + if (closingIndex == expression.length() - 1) { + //-(expression) + isNegated = true; + expression = expression.substring(2, expression.length() - 1).trim(); + } + } + return true; + } + + private boolean checkNegatedNoBrackets() { + if (expression.startsWith("-")) { + isNegated = true; + expression = expression.substring(1, expression.length()).trim(); + } + return true; + } + private int getOperatorIndex() { int index; // find the last executed operator @@ -452,15 +440,23 @@ public class AvatarExpressionSolver { } public int getResult() { + int res; if (isLeaf) { - if (isImmediateValue == IMMEDIATE_NO) { - return 0; + if (isImmediateValue == IMMEDIATE_INT) { + res = intValue; } else { - return intValue; + return 0; } + } else { + res = getChildrenResult(left.getResult(), right.getResult()); } - return getChildrenResult(left.getResult(), right.getResult()); + if (isNot) { + res = (res == 0) ? 1 : 0; + } else if (isNegated) { + res = -res; + } + return res; } public int getResult(SpecificationState ss) { @@ -552,7 +548,7 @@ public class AvatarExpressionSolver { result = leftV + rightV; break; case '|': - result = ((leftV + rightV) > 0) ? 1 : 0; + result = (leftV == 0 && rightV == 0) ? 0 : 1; break; case '/': result = leftV / rightV; @@ -561,7 +557,7 @@ public class AvatarExpressionSolver { result = leftV * rightV; break; case '&': - result = ((leftV + rightV - 2) == 0) ? 1 : 0; + result = (leftV == 0 || rightV == 0) ? 0 : 1; break; default: //System.out.println("Error in EquationSolver::getResult"); @@ -573,12 +569,19 @@ public class AvatarExpressionSolver { } public String toString() { + String retS; if (isLeaf) { if (isImmediateValue == IMMEDIATE_NO) { - return leaf.toString(); + retS = leaf.toString(); } else { - return String.valueOf(intValue); - } + retS = String.valueOf(intValue); + } + if (isNegated) { + retS = "-(" + retS + ")"; + } + if (isNot) { + retS = "not(" + retS + ")"; + } } else { String leftString = left.toString(); String rightString = right.toString(); @@ -606,8 +609,15 @@ public class AvatarExpressionSolver { opString = "" + operator; break; } - return "(" + leftString + " " + opString + " " + rightString + ")"; + retS = "(" + leftString + " " + opString + " " + rightString + ")"; + if (isNegated) { + retS = "-" + retS; + } + if (isNot) { + retS = "not" + retS; + } } + return retS; } public boolean hasState() { diff --git a/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java new file mode 100644 index 0000000000000000000000000000000000000000..ba108657358d41b7f5c37ed5fc345b6ff52b283e --- /dev/null +++ b/ttool/src/test/java/avatartranslator/AvatarExpressionTest.java @@ -0,0 +1,126 @@ +/**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 AvatarExpressionTest + * Creation: 29/04/2020 + * @version 1.0 29/04/2020 + * @author Alessandro TEMPIA CALVINO + * @see + */ + + +package avatartranslator; + +import static org.junit.Assert.*; +import static org.junit.Assert.assertFalse; +import static org.junit.Assert.assertTrue; + +import org.junit.Before; +import org.junit.Test; + +import avatartranslator.*; +import avatartranslator.modelchecker.SpecificationBlock; + +public class AvatarExpressionTest { + + private AvatarGuard res; + private AvatarBlock block; + private SpecificationBlock specBlock; + + public AvatarExpressionTest() { + + } + + @Before + public void test () { + AvatarSpecification as = new AvatarSpecification("avatarspecification", null); + + block = new AvatarBlock("myblock", as, null); + as.addBlock(block); + AvatarAttribute x = new AvatarAttribute("x", AvatarType.INTEGER, block, null); + block.addAttribute(x); + AvatarAttribute y = new AvatarAttribute("y", AvatarType.INTEGER, block, null); + block.addAttribute(y); + AvatarAttribute z = new AvatarAttribute("z", AvatarType.INTEGER, block, null); + block.addAttribute(z); + AvatarAttribute w = new AvatarAttribute("w", AvatarType.BOOLEAN, block, null); + block.addAttribute(w); + + x.setInitialValue("10"); + y.setInitialValue("5"); + z.setInitialValue("2"); + + specBlock = new SpecificationBlock(); + specBlock.init(block, false); + } + + @Test + public void testImmediate() { + AvatarExpressionSolver e1 = new AvatarExpressionSolver("10 + 15 >= 20"); + e1.buildExpression(); + AvatarExpressionSolver e2 = new AvatarExpressionSolver("-10 / 2 - 15 * 2 + 1 == -30 -4"); + e2.buildExpression(); + AvatarExpressionSolver e3 = new AvatarExpressionSolver("not(-10 / 2 - 15 * 2 + 1 == -(60 - 26))"); + e3.buildExpression(); + AvatarExpressionSolver e4 = new AvatarExpressionSolver("1 && 0 >= 1 || 0"); + e4.buildExpression(); + AvatarExpressionSolver e5 = new AvatarExpressionSolver("true and not(false) == not(false or false)"); + e5.buildExpression(); + AvatarExpressionSolver e6 = new AvatarExpressionSolver("10 -Cabin.match"); + assertTrue(e1.getResult() == 1); + assertTrue(e2.getResult() == 1); + assertTrue(e3.getResult() == 0); + assertTrue(e4.getResult() == 0); + assertTrue(e5.getResult() == 1); + assertTrue(e6.buildExpression() == false); + } + + @Test + public void testBlock() { + AvatarExpressionSolver e1 = new AvatarExpressionSolver("x + y"); + e1.buildExpression(block); + AvatarExpressionSolver e2 = new AvatarExpressionSolver("-x / y - 15 * z + 1 == -31"); + e2.buildExpression(block); + AvatarExpressionSolver e3 = new AvatarExpressionSolver("not(-x / z - (x + y) * 2 + 1 == -(60 - 26))"); + e3.buildExpression(block); + assertTrue(e1.getResult(specBlock) == 15); + assertTrue(e2.getResult(specBlock) == 1); + assertTrue(e3.getResult(specBlock) == 0); + } + +}