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

Added getResult() of expression from array of int attribute values

parent b16111ad
No related branches found
No related tags found
1 merge request!336Fixes, documentation, and a first implementation of counterexamples for safety pragmas (txt)
...@@ -38,6 +38,8 @@ ...@@ -38,6 +38,8 @@
package avatartranslator; package avatartranslator;
import java.util.List;
import avatartranslator.modelchecker.SpecificationBlock; import avatartranslator.modelchecker.SpecificationBlock;
import avatartranslator.modelchecker.SpecificationState; import avatartranslator.modelchecker.SpecificationState;
...@@ -204,6 +206,19 @@ public class AvatarExpressionAttribute { ...@@ -204,6 +206,19 @@ public class AvatarExpressionAttribute {
return value; return value;
} }
public int getValue(int[] attributesValues) {
int value;
if (isState) {
return 0;
}
//Cancel offset based on Specification Blocks
value = attributesValues[accessIndex - SpecificationBlock.ATTR_INDEX];
return value;
}
public void setValue(SpecificationState ss, int value) { public void setValue(SpecificationState ss, int value) {
int v; int v;
......
...@@ -557,6 +557,26 @@ public class AvatarExpressionSolver { ...@@ -557,6 +557,26 @@ public class AvatarExpressionSolver {
return res; return res;
} }
public int getResult(int[] attributesValues) {
int res;
if (isLeaf) {
if (isImmediateValue != IMMEDIATE_NO) {
res = intValue;
} else {
res = leaf.getValue(attributesValues);
}
} else {
res = getChildrenResult(left.getResult(attributesValues), right.getResult(attributesValues));
}
if (isNot) {
res = (res == 0) ? 1 : 0;
} else if (isNegated) {
res = -res;
}
return res;
}
private int getChildrenResult(int leftV, int rightV) { private int getChildrenResult(int leftV, int rightV) {
int result; int result;
......
...@@ -135,6 +135,7 @@ public class AvatarExpressionTest { ...@@ -135,6 +135,7 @@ public class AvatarExpressionTest {
public void testBlock() { public void testBlock() {
SpecificationBlock specBlock = new SpecificationBlock(); SpecificationBlock specBlock = new SpecificationBlock();
specBlock.init(block1, false); specBlock.init(block1, false);
int[] attributes = {2, 3, 7, 0, 1};
AvatarExpressionSolver e1 = new AvatarExpressionSolver("x + y"); AvatarExpressionSolver e1 = new AvatarExpressionSolver("x + y");
assertTrue(e1.buildExpression(block1)); assertTrue(e1.buildExpression(block1));
...@@ -156,6 +157,12 @@ public class AvatarExpressionTest { ...@@ -156,6 +157,12 @@ public class AvatarExpressionTest {
assertTrue(e9.buildExpression(block1)); assertTrue(e9.buildExpression(block1));
AvatarExpressionSolver e10 = new AvatarExpressionSolver("x*((x + y)*z + (x+z)/z)/x"); AvatarExpressionSolver e10 = new AvatarExpressionSolver("x*((x + y)*z + (x+z)/z)/x");
assertTrue(e10.buildExpression(block1)); assertTrue(e10.buildExpression(block1));
AvatarExpressionSolver e11 = new AvatarExpressionSolver("x + y");
assertTrue(e11.buildExpression(block1));
AvatarExpressionSolver e12 = new AvatarExpressionSolver("x*((x + y)*z + (x+z)/z)/x");
assertTrue(e12.buildExpression(block1));
AvatarExpressionSolver e13 = new AvatarExpressionSolver("(key1==false) and (key2==true)");
assertTrue(e13.buildExpression(block1));
assertTrue(e1.getResult(specBlock) == 15); assertTrue(e1.getResult(specBlock) == 15);
assertTrue(e2.getResult(specBlock) == 1); assertTrue(e2.getResult(specBlock) == 1);
assertTrue(e3.getResult(specBlock) == 0); assertTrue(e3.getResult(specBlock) == 0);
...@@ -166,6 +173,9 @@ public class AvatarExpressionTest { ...@@ -166,6 +173,9 @@ public class AvatarExpressionTest {
assertTrue(e8.getResult(specBlock) == 45); assertTrue(e8.getResult(specBlock) == 45);
assertTrue(e9.getResult(specBlock) == 570); assertTrue(e9.getResult(specBlock) == 570);
assertTrue(e10.getResult(specBlock) == 36); assertTrue(e10.getResult(specBlock) == 36);
assertTrue(e11.getResult(attributes) == 5);
assertTrue(e12.getResult(attributes) == 36);
assertTrue(e13.getResult(attributes) == 1);
} }
@Test @Test
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment