Skip to content
Snippets Groups Projects
Commit 4bb94c12 authored by tempiaa's avatar tempiaa
Browse files

New guard evaluator, using precomputing and the optimized expression solver... 

New guard evaluator, using precomputing and the optimized expression solver ~80x speedup in modelchecker
parent 7eeb3c34
No related branches found
No related tags found
1 merge request!325Avatar model-checker improvements
Hide whitespace changes
Inline Side-by-side
src/main/java/avatartranslator/AvatarExpressionAttribute.java
+ 67
− 1
View file @ 4bb94c12
......@@ -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;
}
}
src/main/java/avatartranslator/AvatarExpressionSolver.java
+ 199
− 9
View file @ 4bb94c12
......@@ -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;
}
}
src/main/java/avatartranslator/AvatarTransition.java
+ 15
− 0
View file @ 4bb94c12
......@@ -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;
......
src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+ 21
− 4
View file @ 4bb94c12
......@@ -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) {
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment