From cd5beaac5ecded920ddccbc5cace1b617e6fcb6d Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Tue, 21 Apr 2020 15:34:29 +0200
Subject: [PATCH] Expression Solver for action on signal. Start developing
safety properties on states
---
.../AvatarActionOnSignal.java | 20 +++++
.../modelchecker/AvatarModelChecker.java | 80 ++++++++++++-------
.../modelchecker/SafetyProperty.java | 74 ++++++++---------
.../modelchecker/SpecificationLiveness.java | 2 -
4 files changed, 103 insertions(+), 73 deletions(-)
diff --git a/src/main/java/avatartranslator/AvatarActionOnSignal.java b/src/main/java/avatartranslator/AvatarActionOnSignal.java
index 431bbff681..44109376be 100644
--- a/src/main/java/avatartranslator/AvatarActionOnSignal.java
+++ b/src/main/java/avatartranslator/AvatarActionOnSignal.java
@@ -41,6 +41,7 @@ package avatartranslator;
import myutil.TraceManager;
+import java.util.ArrayList;
import java.util.LinkedList;
import java.util.List;
@@ -55,6 +56,7 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement {
private AvatarSignal signal;
private List<String> values;
private boolean checkLatency;
+ private List<AvatarExpressionAttribute> actionAttr;
public AvatarActionOnSignal(String _name, AvatarSignal _signal, Object _referenceObject ) {
@@ -69,6 +71,7 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement {
signal = _signal;
values = new LinkedList<String>();
+ actionAttr = null;
}
public AvatarSignal getSignal() {
@@ -106,6 +109,23 @@ public class AvatarActionOnSignal extends AvatarStateMachineElement {
public boolean isReceiving() {
return signal.isIn();
}
+
+ public boolean buildActionSolver(AvatarBlock block) {
+ AvatarExpressionAttribute aea;
+ boolean res = true;
+ int i = 0;
+ actionAttr = new ArrayList<AvatarExpressionAttribute>();
+ for (String val : values) {
+ aea = new AvatarExpressionAttribute(block, val);
+ actionAttr.add(aea);
+ res &= aea.hasError();
+ }
+ return res;
+ }
+
+ public AvatarExpressionAttribute getExpressionAttribute(int index) {
+ return actionAttr.get(index);
+ }
public AvatarActionOnSignal basicCloneMe(AvatarStateMachineOwner _block) {
//TraceManager.addDev("I HAVE BEEN CLONED: " + this);
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index ca5d24b9e9..13a480f118 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -434,7 +434,6 @@ 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);
@@ -685,6 +684,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
((AvatarActionAssignment) aa).buildActionSolver(block);
}
}
+ }else if (elt instanceof AvatarActionOnSignal) {
+ ((AvatarActionOnSignal) elt).buildActionSolver(block);
}
}
}
@@ -1407,7 +1408,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private String executeActionTransition(SpecificationState _previousState, SpecificationState _newState, SpecificationTransition _st) {
// We use the attributes value as in the _newState
// Get the attributes value list
- AvatarBlock block = _st.blocks[0];
+// AvatarBlock block = _st.blocks[0];
String retAction = null;
@@ -1458,15 +1459,15 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
private String executeSyncTransition(SpecificationState _previousState, SpecificationState _newState, SpecificationTransition _st) {
- AvatarBlock block0 = _st.blocks[0];
- AvatarBlock block1 = _st.blocks[1];
+// AvatarBlock block0 = _st.blocks[0];
+// AvatarBlock block1 = _st.blocks[1];
AvatarActionOnSignal aaoss, aaosr;
- AvatarAttribute avat;
- String value;
+// AvatarAttribute avat;
+// String value;
int result;
- boolean resultB;
- int indexVar;
- String nameOfVar;
+// boolean resultB;
+// int indexVar;
+// String nameOfVar;
String ret = "";
@@ -1478,29 +1479,38 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
// copy the value of attributes from one block to the other one
+// for (int i = 0; i < aaoss.getNbOfValues(); i++) {
+// value = aaoss.getValue(i);
+// try {
+// avat = aaoss.getSignal().getListOfAttributes().get(i);
+// if (avat.getType() == AvatarType.INTEGER) {
+// //TraceManager.addDev("Evaluating expression, value=" + value);
+// //TraceManager.addDev("Evaluating int expr=" + value);
+// result = evaluateIntExpression(value, block0, _newState.blocks[_st.blocksInt[0]]);
+// } else if (avat.getType() == AvatarType.BOOLEAN) {
+// resultB = evaluateBoolExpression(value, block0, _newState.blocks[_st.blocksInt[0]]);
+// result = resultB ? 1 : 0;
+// } else {
+// result = 0;
+// }
+//
+// // Putting the result to the destination var
+// nameOfVar = aaosr.getValue(i);
+// indexVar = block1.getIndexOfAvatarAttributeWithName(nameOfVar);
+// _newState.blocks[_st.blocksInt[1]].values[SpecificationBlock.ATTR_INDEX + indexVar] = result;
+// ret += "" + result;
+// } catch (Exception e) {
+// TraceManager.addDev("EXCEPTION on adding value " + aaoss);
+// }
+// }
for (int i = 0; i < aaoss.getNbOfValues(); i++) {
- value = aaoss.getValue(i);
- try {
- avat = aaoss.getSignal().getListOfAttributes().get(i);
- if (avat.getType() == AvatarType.INTEGER) {
- //TraceManager.addDev("Evaluating expression, value=" + value);
- //TraceManager.addDev("Evaluating int expr=" + value);
- result = evaluateIntExpression(value, block0, _newState.blocks[_st.blocksInt[0]]);
- } else if (avat.getType() == AvatarType.BOOLEAN) {
- resultB = evaluateBoolExpression(value, block0, _newState.blocks[_st.blocksInt[0]]);
- result = resultB ? 1 : 0;
- } else {
- result = 0;
- }
-
- // Putting the result to the destination var
- nameOfVar = aaosr.getValue(i);
- indexVar = block1.getIndexOfAvatarAttributeWithName(nameOfVar);
- _newState.blocks[_st.blocksInt[1]].values[SpecificationBlock.ATTR_INDEX + indexVar] = result;
+// try {
+ result = aaoss.getExpressionAttribute(i).getValue(_newState.blocks[_st.blocksInt[0]]);
+ aaosr.getExpressionAttribute(i).setValue(_newState.blocks[_st.blocksInt[1]], result);
ret += "" + result;
- } catch (Exception e) {
- TraceManager.addDev("EXCEPTION on adding value " + aaoss);
- }
+// } catch (Exception e) {
+// TraceManager.addDev("EXCEPTION on adding value " + aaoss);
+// }
}
@@ -1538,6 +1548,16 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
_ss.property = true;
}
}
+
+// if (studySafety) {
+// if (safety.propertyType == SafetyProperty.BLOCK_STATE && safety.state == _ase) {
+// if (safety.safetyType == SafetyProperty.ALLTRACES_ALLSTATES || safety.safetyType == SafetyProperty.ONETRACE_ALLSTATES) {
+// _ss.property = false;
+// } else {
+// _ss.property = true;
+// }
+// }
+// }
if (_ase.getNexts().size() != 1) {
return _ase;
diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index a392be7f98..61b0ba8d43 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -52,7 +52,6 @@ public class SafetyProperty {
private String rawProperty;
private String p;
- private AvatarAttribute attribute;
private int errorOnProperty;
private AvatarExpressionSolver safetySolver;
@@ -73,8 +72,9 @@ public class SafetyProperty {
public static final int BOOL_EXPR = 1;
public int safetyType;
+ public int propertyType;
public AvatarBlock block;
- public int blockIndex;
+ public AvatarStateElement state;
public boolean result;
@@ -109,49 +109,33 @@ public class SafetyProperty {
}
p = tmpP.substring(3, tmpP.length()).trim();
-
- safetySolver = new AvatarExpressionSolver(p);
- boolean exprRet = safetySolver.buildExpression(_spec);
-
- if (exprRet == false) {
- errorOnProperty = BAD_PROPERTY_STRUCTURE;
- return false;
- }
-
- /*
- if (p.length() == 0) {
- errorOnProperty = BAD_PROPERTY_STRUCTURE;
- return false;
- }
-
- pFields = p.split(" "); //[0] item, [1] operator, [3] value
-
- if (pFields.length != 3 || pFields[0].split("\\.").length != 2) {
- errorOnProperty = BAD_PROPERTY_STRUCTURE;
- return false;
- }
-
- blockString = pFields[0].split("\\.")[0];
- fieldString = pFields[0].split("\\.")[1];
- block = _spec.getBlockWithName(blockString);
- blockIndex = _spec.getBlockIndex(block);
+ if (!p.matches("^.*[\\+\\-<>=&\\*/].*$")) {
+ propertyType = BLOCK_STATE;
+ pFields = p.split("\\.");
+ blockString = pFields[0];
+ fieldString = pFields[1];
+ block = _spec.getBlockWithName(blockString);
+ if (block == null) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+ state = block.getStateMachine().getStateWithName(fieldString);
+ if (state == null) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
+ } else {
+ propertyType = BOOL_EXPR;
+ safetySolver = new AvatarExpressionSolver(p);
+ boolean exprRet = safetySolver.buildExpression(_spec);
- if (block == null) {
- errorOnProperty = BAD_PROPERTY_STRUCTURE;
- return false;
+ if (exprRet == false) {
+ errorOnProperty = BAD_PROPERTY_STRUCTURE;
+ return false;
+ }
}
- attribute = block.getAvatarAttributeWithName(fieldString);
-
- if (attribute == null) {
- errorOnProperty = BAD_PROPERTY_STRUCTURE;
- return false;
- }
-
- p = fieldString + " " + pFields[1] + " " + pFields[2];
- */
-
return (errorOnProperty == NO_ERROR);
}
@@ -176,6 +160,14 @@ public class SafetyProperty {
return safetySolver.getResult(_ss) != 0;
}
+ public void setBlock(AvatarBlock block) {
+ this.block = block;
+ }
+
+ public void setState(AvatarStateElement ase) {
+ this.state = ase;
+ }
+
public String toString() {
if (result) {
return rawProperty + " -> property is satisfied";
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationLiveness.java b/src/main/java/avatartranslator/modelchecker/SpecificationLiveness.java
index 898573ab7e..db105defea 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationLiveness.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationLiveness.java
@@ -55,13 +55,11 @@ import avatartranslator.AvatarStateMachineElement;
public class SpecificationLiveness {
public Object ref1, ref2; // ref1 must be provided, ref2 might be null
public boolean result;
- public SpecificationState state;
public SpecificationLiveness(Object _ref1, Object _ref2) {
ref1 = _ref1;
ref2 = _ref2;
result = true;
- state = null;
}
public String toString() {
--
GitLab