diff --git a/src/main/java/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
index a406a782e33d909676b7d2f191aeac896015957e..264eef134bcdbf1805e5568c6e870334d9c11b4e 100644
--- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java
+++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
@@ -82,6 +82,31 @@ public class AvatarExpressionAttribute {
error = !initAttributes(spec);
}
+ public AvatarExpressionAttribute(AvatarBlock block, String s) {
+ this.s = s;
+ isNegated = false;
+ isNot = 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);
+ }
+
private boolean initAttributes(AvatarSpecification spec) {
//Extract Block and Attribute
@@ -118,6 +143,25 @@ public class AvatarExpressionAttribute {
return true;
}
+ private boolean initAttributes(AvatarBlock block) {
+ //Extract Attribute
+ if (block == null) {
+ return false;
+ }
+
+ this.block = block;
+ this.blockIndex = -1; //not initialized
+
+ attributeIndex = block.getIndexOfAvatarAttributeWithName(s);
+
+ if (attributeIndex == -1) {
+ return false;
+ }
+
+ accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
+ return true;
+ }
+
public boolean hasError() {
return error == true;
}
@@ -134,7 +178,29 @@ public class AvatarExpressionAttribute {
return value;
}
+ public int getValue(SpecificationBlock sb) {
+ int value = sb.values[accessIndex];
+
+ if (isNot) {
+ value = (value == 0) ? 1 : 0;
+ } else if (isNegated) {
+ value = -value;
+ }
+
+ return value;
+ }
+
public String toString() {
- return this.s;
+ String res = "";
+ if (isNot) {
+ res = "not(" + this.s + ")";
+ } else if (isNegated) {
+ res += "-" + this.s;
+ } else {
+ res = s;
+ }
+
+ return res;
}
+
}
diff --git a/src/main/java/avatartranslator/AvatarExpressionSolver.java b/src/main/java/avatartranslator/AvatarExpressionSolver.java
index 51ed3a75d05280c8788880739141522c4d58db4b..b50dc67d1260b1aea226400ee197c3c4841140a0 100644
--- a/src/main/java/avatartranslator/AvatarExpressionSolver.java
+++ b/src/main/java/avatartranslator/AvatarExpressionSolver.java
@@ -38,6 +38,7 @@
package avatartranslator;
+import avatartranslator.modelchecker.SpecificationBlock;
import avatartranslator.modelchecker.SpecificationState;
/**
@@ -56,6 +57,8 @@ public class AvatarExpressionSolver {
private char operator;
private String expression;
private boolean isLeaf; //variable
+ private boolean isNot;
+ private boolean isNegated;
private int isImmediateValue; //0: No; 1: Boolean; 2: Int
private int intValue;
private AvatarExpressionAttribute leaf;
@@ -77,6 +80,8 @@ public class AvatarExpressionSolver {
isLeaf = true;
isImmediateValue = IMMEDIATE_NO;
intValue = 0;
+ isNot = false;
+ isNegated = false;
}
public void setExpression(String expression) {
@@ -87,7 +92,9 @@ public class AvatarExpressionSolver {
public boolean buildExpression(AvatarSpecification spec) {
boolean returnVal;
- if (!expression.matches("^.+[\\+\\-<>=&\\*\\\\].*$")) {
+ removeUselessBrackets();
+
+ if (!expression.matches("^.+[\\+\\-<>=&\\*/].*$")) {
// leaf
isLeaf = true;
if (expression.equals("true")) {
@@ -111,7 +118,34 @@ public class AvatarExpressionSolver {
}
isLeaf = false;
- // to single character operation
+
+ 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();
+ }
+ }
+
+ 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();
+ }
+ }
int index = getOperatorIndex();
@@ -134,6 +168,85 @@ public class AvatarExpressionSolver {
return returnVal;
}
+ public boolean buildExpression(AvatarBlock block) {
+ boolean returnVal;
+
+ removeUselessBrackets();
+
+ if (!expression.matches("^.+[\\+\\-<>=&\\*/].*$")) {
+ // leaf
+ isLeaf = true;
+ if (expression.equals("true")) {
+ intValue = 1;
+ isImmediateValue = IMMEDIATE_INT;
+ returnVal = true;
+ } else if (expression.equals("false")) {
+ intValue = 0;
+ isImmediateValue = IMMEDIATE_INT;
+ returnVal = true;
+ } else if (expression.matches("-?\\d+")) {
+ intValue = Integer.parseInt(expression);
+ isImmediateValue = IMMEDIATE_INT;
+ returnVal = true;
+ } else {
+ leaf = new AvatarExpressionAttribute(block, expression);
+ returnVal = !leaf.hasError();
+ }
+ //System.out.println("Variable " + expression + "\n");
+ return returnVal;
+ }
+
+ 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();
+ }
+ }
+
+ 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();
+ }
+ }
+
+ int index = getOperatorIndex();
+
+ if (index == -1) {
+ return false;
+ }
+
+ operator = expression.charAt(index);
+
+ //split and recur
+ String leftExpression = expression.substring(0, index).strip();
+ String rightExpression = expression.substring(index + 1, expression.length()).strip();
+
+ left = new AvatarExpressionSolver(leftExpression);
+ right = new AvatarExpressionSolver(rightExpression);
+ //System.out.println("Expression " + expression + " ; " + leftExpression + " ; " + rightExpression + "\n");
+ returnVal = left.buildExpression(block);
+ returnVal &= right.buildExpression(block);
+
+ return returnVal;
+ }
+
private void replaceOperators() {
expression = expression.replaceAll("\\|\\|", "\\|").trim();
expression = expression.replaceAll("&&", "&").trim();
@@ -150,9 +263,6 @@ public class AvatarExpressionSolver {
private int getOperatorIndex() {
int index;
// find the last executed operator
- while (expression.startsWith("(") && expression.endsWith(")")) {
- expression = expression.substring(1, expression.length() - 1);
- }
// if (expression.matches("^.+[=\\$:;<>].*$")) {
// // boolean operator found
// if (expression.indexOf('=') != -1) {
@@ -285,15 +395,43 @@ public class AvatarExpressionSolver {
}
public int getResult(SpecificationState ss) {
+ int res;
if (isLeaf) {
if (isImmediateValue == IMMEDIATE_INT) {
- return intValue;
+ res = intValue;
} else {
- return leaf.getValue(ss);
+ res = leaf.getValue(ss);
}
+ } else {
+ res = getChildrenResult(left.getResult(ss), right.getResult(ss));
}
- return getChildrenResult(left.getResult(ss), right.getResult(ss));
+ if (isNot) {
+ res = (res == 0) ? 1 : 0;
+ } else if (isNegated) {
+ res = -res;
+ }
+ return res;
+ }
+
+ public int getResult(SpecificationBlock sb) {
+ int res;
+ if (isLeaf) {
+ if (isImmediateValue == IMMEDIATE_INT) {
+ res = intValue;
+ } else {
+ res = leaf.getValue(sb);
+ }
+ } else {
+ res = getChildrenResult(left.getResult(sb), right.getResult(sb));
+ }
+
+ if (isNot) {
+ res = (res == 0) ? 1 : 0;
+ } else if (isNegated) {
+ res = -res;
+ }
+ return res;
}
private int getChildrenResult(int leftV, int rightV) {
@@ -354,8 +492,60 @@ public class AvatarExpressionSolver {
} else {
String leftString = left.toString();
String rightString = right.toString();
- return "(" + leftString + " " + operator + " " + rightString + ")";
+ String opString;
+ switch (operator) {
+ case '=':
+ opString = "==";
+ break;
+ case '$':
+ opString = "!=";
+ break;
+ case ':':
+ opString = ">=";
+ break;
+ case ';':
+ opString = "<=";
+ break;
+ case '|':
+ opString = "||";
+ break;
+ case '&':
+ opString = "&&";
+ break;
+ default:
+ opString = "" + operator;
+ break;
+ }
+ return "(" + leftString + " " + opString + " " + rightString + ")";
+ }
+ }
+
+ private void removeUselessBrackets() {
+ while (expression.startsWith("(") && expression.endsWith(")")) {
+ if (getClosingBracket(1) == expression.length() - 1) {
+ expression = expression.substring(1, expression.length() - 1).trim();
+ } else {
+ break;
+ }
+ }
+ }
+
+ private int getClosingBracket(int startChar) {
+ int level = 0;
+ char a;
+ for (int i = startChar; i < expression.length(); i++) {
+ a = expression.charAt(i);
+ if (a == ')') {
+ if (level == 0) {
+ return i;
+ } else {
+ level--;
+ }
+ } else if (a == '(') {
+ level++;
+ }
}
+ return -1;
}
}
diff --git a/src/main/java/avatartranslator/AvatarTransition.java b/src/main/java/avatartranslator/AvatarTransition.java
index 2455bc46c89c51e50bc5e005d4fa7eb8fd286de8..eb1864d1b20395f0ae199929f4e45e208dacfe91 100644
--- a/src/main/java/avatartranslator/AvatarTransition.java
+++ b/src/main/java/avatartranslator/AvatarTransition.java
@@ -44,6 +44,7 @@ import java.util.Iterator;
import java.util.LinkedList;
import java.util.List;
+
/**
* Class AvatarTransition
* Creation: 20/05/2010
@@ -73,6 +74,8 @@ public class AvatarTransition extends AvatarStateMachineElement {
private String minDelay = "", maxDelay = "";
private String minCompute = "", maxCompute = "";
private AvatarStateMachineOwner block;
+
+ private AvatarExpressionSolver guardSolver;
private List<AvatarAction> actions; // actions on variable, or method call
@@ -81,11 +84,23 @@ public class AvatarTransition extends AvatarStateMachineElement {
actions = new LinkedList<AvatarAction>();
this.guard = new AvatarGuardEmpty();
this.block = _block;
+ guardSolver = null;
}
public AvatarGuard getGuard() {
return guard;
}
+
+ public boolean buildGuardSolver() {
+ String expr = guard.toString().replaceAll("\\[", "").trim();
+ expr = expr.replaceAll("\\]", "");
+ guardSolver = new AvatarExpressionSolver(expr);
+ return guardSolver.buildExpression((AvatarBlock) block);
+ }
+
+ public AvatarExpressionSolver getGuardSolver() {
+ return guardSolver;
+ }
public void setGuard(AvatarGuard _guard) {
this.guard = _guard;
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 6a525575764fb3250adc4608fa4b0b9c75fec21a..b90ea40fbada911b2b7980c6e66174b1953dc1aa 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -159,6 +159,20 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
public AvatarSpecification getReworkedAvatarSpecification() {
return spec;
}
+
+ private void initExpressionSolvers() {
+ for (AvatarBlock block : spec.getListOfBlocks()) {
+ AvatarStateMachine asm = block.getStateMachine();
+
+ for (AvatarStateMachineElement elt : asm.getListOfElements()) {
+ if (elt instanceof AvatarTransition) {
+ if (((AvatarTransition) elt).isGuarded()) {
+ ((AvatarTransition) elt).buildGuardSolver();
+ }
+ }
+ }
+ }
+ }
public int getNbOfStates() {
if (states == null) {
@@ -425,6 +439,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (ignoreEmptyTransitions) {
spec.removeEmptyTransitions((nbOfRemainingReachabilities == 0) || studyLiveness || studySafety);
}
+
+ initExpressionSolvers();
//TraceManager.addDev("Preparing Avatar specification :" + spec.toString());
prepareStates();
@@ -1083,10 +1099,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
// Must evaluate the guard
- String guard = _at.getGuard().toString();
- String s = Conversion.replaceAllString(guard, "[", "").trim();
- s = Conversion.replaceAllString(s, "]", "").trim();
- return evaluateBoolExpression(s, _block, _sb);
+ //String guard = _at.getGuard().toString();
+ //String s = Conversion.replaceAllString(guard, "[", "").trim();
+ //s = Conversion.replaceAllString(s, "]", "").trim();
+ return (_at.getGuardSolver().getResult(_sb) == 0) ? false : true;
+ //return evaluateBoolExpression(s, _block, _sb);
}
private void handleAvatarTransition(AvatarTransition _at, AvatarBlock _block, SpecificationBlock _sb, int _indexOfBlock, ArrayList<SpecificationTransition> _transitionsToAdd, boolean _fromStateWithMoreThanOneTransition) {