From 0663831b5ee908ab0006413003a089b889f1dc8f Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Mon, 20 Apr 2020 18:03:26 +0200
Subject: [PATCH] Assigment Action using the new expression evaluator
---
.../AvatarActionAssignment.java | 23 ++++++
.../AvatarExpressionAttribute.java | 24 ++++++
.../modelchecker/AvatarModelChecker.java | 73 +++++++++++--------
3 files changed, 89 insertions(+), 31 deletions(-)
diff --git a/src/main/java/avatartranslator/AvatarActionAssignment.java b/src/main/java/avatartranslator/AvatarActionAssignment.java
index 8a558a16bb..40d0c911d5 100644
--- a/src/main/java/avatartranslator/AvatarActionAssignment.java
+++ b/src/main/java/avatartranslator/AvatarActionAssignment.java
@@ -42,6 +42,8 @@ import myutil.TraceManager;
import java.util.Map;
+import avatartranslator.modelchecker.SpecificationBlock;
+
/**
* Class AvatarActionAssignment
* Creation: 16/09/2015
@@ -51,10 +53,14 @@ import java.util.Map;
public class AvatarActionAssignment implements AvatarAction {
AvatarLeftHand leftHand;
AvatarTerm rightHand;
+ AvatarExpressionSolver actionSolver;
+ private AvatarExpressionAttribute leftAttribute;
public AvatarActionAssignment (AvatarLeftHand _leftHand, AvatarTerm _rightHand) {
this.leftHand = _leftHand;
this.rightHand = _rightHand;
+ this.actionSolver = null;
+ this.leftAttribute = null;
}
public boolean isAVariableSetting () {
@@ -72,6 +78,10 @@ public class AvatarActionAssignment implements AvatarAction {
public AvatarTerm getRightHand () {
return this.rightHand;
}
+
+ public AvatarExpressionSolver getActionSolver() {
+ return actionSolver;
+ }
public boolean isABasicVariableSetting () {
return (this.leftHand instanceof AvatarAttribute || this.leftHand instanceof AvatarTuple) &&
@@ -85,6 +95,19 @@ public class AvatarActionAssignment implements AvatarAction {
public String toString () {
return this.leftHand.getName() + " = " + this.rightHand.getName();
}
+
+ public boolean buildActionSolver(AvatarBlock block) {
+ boolean res;
+ actionSolver = new AvatarExpressionSolver(rightHand.getName());
+ res = actionSolver.buildExpression((AvatarBlock) block);
+ leftAttribute = new AvatarExpressionAttribute(block, leftHand.getName());
+ res &= !leftAttribute.hasError();
+ return res;
+ }
+
+ public void executeActionSolver(SpecificationBlock sb) {
+ leftAttribute.setValue(sb, actionSolver.getResult(sb));
+ }
@Override
public boolean containsAMethodCall () {
diff --git a/src/main/java/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
index 264eef134b..5f8ccad448 100644
--- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java
+++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
@@ -190,6 +190,30 @@ public class AvatarExpressionAttribute {
return value;
}
+ public void setValue(SpecificationState ss, int value) {
+ int v = value;
+
+ if (isNot) {
+ v = (value == 0) ? 1 : 0;
+ } else if (isNegated) {
+ v = -value;
+ }
+
+ ss.blocks[blockIndex].values[accessIndex] = v;
+ }
+
+ public void setValue(SpecificationBlock sb, int value) {
+ int v = value;
+
+ if (isNot) {
+ v = (value == 0) ? 1 : 0;
+ } else if (isNegated) {
+ v = -value;
+ }
+
+ sb.values[accessIndex] = v;
+ }
+
public String toString() {
String res = "";
if (isNot) {
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index b90ea40fba..ca5d24b9e9 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -159,20 +159,6 @@ 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) {
@@ -448,6 +434,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
nbOfThreads = Runtime.getRuntime().availableProcessors();
+ nbOfThreads = 1;
TraceManager.addDev("Starting the model checking with " + nbOfThreads + " threads");
TraceManager.addDev("Ignore internal state:" + ignoreInternalStates);
startModelChecking(nbOfThreads);
@@ -680,6 +667,28 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
nbOfCurrentComputations = 0;
}
+
+ private void initExpressionSolvers() {
+ AvatarTransition at;
+
+ for (AvatarBlock block : spec.getListOfBlocks()) {
+ AvatarStateMachine asm = block.getStateMachine();
+
+ for (AvatarStateMachineElement elt : asm.getListOfElements()) {
+ if (elt instanceof AvatarTransition) {
+ at = (AvatarTransition) elt;
+ if (at.isGuarded()) {
+ at.buildGuardSolver();
+ }
+ for (AvatarAction aa : at.getActions()) {
+ if (aa instanceof AvatarActionAssignment) {
+ ((AvatarActionAssignment) aa).buildActionSolver(block);
+ }
+ }
+ }
+ }
+ }
+ }
private void prepareTransitionsOfState(SpecificationState _ss) {
@@ -1419,23 +1428,25 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (retAction == null) {
retAction = nameOfVar + "=" + act;
}
-
- int indexVar = block.getIndexOfAvatarAttributeWithName(nameOfVar);
- AvatarType type = block.getAttribute(indexVar).getType();
- if (indexVar != -1) {
- if (type == AvatarType.INTEGER) {
- //TraceManager.addDev("Evaluating int expr=" + act);
- int result = evaluateIntExpression(act, _st.blocks[0], _newState.blocks[_st.blocksInt[0]]);
- _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = result;
- } else if (type == AvatarType.BOOLEAN) {
- boolean bool = evaluateBoolExpression(act, _st.blocks[0], _newState.blocks[_st.blocksInt[0]]);
- if (bool) {
- _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = 1;
- } else {
- _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = 0;
- }
- }
- }
+
+ ((AvatarActionAssignment) aAction).executeActionSolver(_newState.blocks[_st.blocksInt[0]]);
+
+// int indexVar = block.getIndexOfAvatarAttributeWithName(nameOfVar);
+// AvatarType type = block.getAttribute(indexVar).getType();
+// if (indexVar != -1) {
+// if (type == AvatarType.INTEGER) {
+// //TraceManager.addDev("Evaluating int expr=" + act);
+// int result = evaluateIntExpression(act, _st.blocks[0], _newState.blocks[_st.blocksInt[0]]);
+// _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = result;
+// } else if (type == AvatarType.BOOLEAN) {
+// boolean bool = evaluateBoolExpression(act, _st.blocks[0], _newState.blocks[_st.blocksInt[0]]);
+// if (bool) {
+// _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = 1;
+// } else {
+// _newState.blocks[_st.blocksInt[0]].values[SpecificationBlock.ATTR_INDEX + indexVar] = 0;
+// }
+// }
+// }
}
}
--
GitLab