From c5b02346671337582b915c28d934a3cb83107f05 Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Tue, 26 May 2020 17:03:39 +0200
Subject: [PATCH] More precise and correct behaviour in pragmas verification;
Added better management of Expression Solvers with states
---
.../AvatarExpressionAttribute.java | 40 ++++++++++++++--
.../AvatarExpressionSolver.java | 11 +++++
.../modelchecker/AvatarModelChecker.java | 48 +++++++++++--------
.../modelchecker/SafetyProperty.java | 11 +++++
4 files changed, 84 insertions(+), 26 deletions(-)
diff --git a/src/main/java/avatartranslator/AvatarExpressionAttribute.java b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
index 0ca60b084d..bcf8ffe035 100644
--- a/src/main/java/avatartranslator/AvatarExpressionAttribute.java
+++ b/src/main/java/avatartranslator/AvatarExpressionAttribute.java
@@ -78,6 +78,8 @@ public class AvatarExpressionAttribute {
isState = true;
state = asme;
error = false;
+ accessIndex = -1;
+ block = null;
}
@@ -116,8 +118,10 @@ public class AvatarExpressionAttribute {
return false;
}
isState = true;
+ accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
+ } else {
+ accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
}
- accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
return true;
}
@@ -139,9 +143,10 @@ public class AvatarExpressionAttribute {
return false;
}
isState = true;
+ accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
+ } else {
+ accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
}
-
- accessIndex = attributeIndex + SpecificationBlock.ATTR_INDEX;
return true;
}
@@ -153,7 +158,14 @@ public class AvatarExpressionAttribute {
int value;
if (isState) {
- return 0;
+ if (ss.blocks == null || accessIndex == -1) {
+ return 0;
+ }
+ if (ss.blocks[blockIndex].values[SpecificationBlock.STATE_INDEX] == accessIndex) {
+ return 1;
+ } else {
+ return 0;
+ }
}
value = ss.blocks[blockIndex].values[accessIndex];
@@ -177,7 +189,14 @@ public class AvatarExpressionAttribute {
int value;
if (isState) {
- return 0;
+ if (sb == null || accessIndex == -1) {
+ return 0;
+ }
+ if (sb.values[SpecificationBlock.STATE_INDEX] == accessIndex) {
+ return 1;
+ } else {
+ return 0;
+ }
}
value = sb.values[accessIndex];
@@ -209,6 +228,17 @@ public class AvatarExpressionAttribute {
sb.values[accessIndex] = v;
}
+ //Link state to access index in the state machine
+ public void linkState() {
+ if (isState) {
+ if (block != null) {
+ accessIndex = block.getStateMachine().getIndexOfState((AvatarStateElement) state);
+ } else {
+ accessIndex = -1;
+ }
+ }
+ }
+
public boolean isState() {
return isState;
}
diff --git a/src/main/java/avatartranslator/AvatarExpressionSolver.java b/src/main/java/avatartranslator/AvatarExpressionSolver.java
index bc7ee7060e..e73a5c237c 100644
--- a/src/main/java/avatartranslator/AvatarExpressionSolver.java
+++ b/src/main/java/avatartranslator/AvatarExpressionSolver.java
@@ -635,6 +635,17 @@ public class AvatarExpressionSolver {
}
}
+ public void linkStates() {
+ if (isLeaf) {
+ if (isImmediateValue == IMMEDIATE_NO) {
+ leaf.linkState();
+ }
+ } else {
+ left.linkStates();
+ right.linkStates();
+ }
+ }
+
private void removeUselessBrackets() {
while (expression.startsWith("(") && expression.endsWith(")")) {
if (getClosingBracket(1) == expression.length() - 1) {
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 58121c23ab..e85496731c 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -590,15 +590,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
int cpt = 0;
- for (AvatarBlock block : spec.getListOfBlocks()) {
- AvatarStateMachine asm = block.getStateMachine();
- SpecificationBlock sb = initialState.blocks[cpt];
- AvatarStateMachineElement asme = asm.allStates[sb.values[SpecificationBlock.STATE_INDEX]];
- if (studySafety && safety.propertyType == SafetyProperty.BLOCK_STATE) {
- initialState.property |= safety.getSolverResult(initialState, asme);
- }
- cpt++;
- }
+
+ initialState.property |= safety.getSolverResult(initialState);
+
if (studySafety && safety.propertyType == SafetyProperty.BLOCK_STATE) {
if (safety.safetyType == SafetyProperty.ALLTRACES_ALLSTATES || safety.safetyType == SafetyProperty.ONETRACE_ALLSTATES) {
initialState.property = !initialState.property;
@@ -662,11 +656,12 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (ignoreEmptyTransitions) {
spec.removeEmptyTransitions(!(studyReachability || studyLiveness || studySafety));
}
-
- initExpressionSolvers();
//TraceManager.addDev("Preparing Avatar specification :" + spec.toString());
prepareStates();
+
+ initExpressionSolvers();
+
prepareTransitions();
prepareBlocks();
@@ -866,6 +861,13 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
}
}
+
+ //To have all the leadsTo functionalities allStates in stateMachines must be filled with states
+ if (studySafety && safeties != null) {
+ for (SafetyProperty sp : safeties) {
+ sp.linkSolverStates();
+ }
+ }
}
private void prepareTransitionsOfState(SpecificationState _ss) {
@@ -1800,19 +1802,23 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private boolean evaluateSafetyOfProperty(SpecificationState newState, SpecificationTransition tr, boolean precProperty) {
AvatarStateMachineElement asme;
- boolean result = false;
+ boolean result;
if (safety.propertyType == SafetyProperty.BLOCK_STATE) {
- for (int i = 0; i < tr.transitions.length; i++) {
- int k = 10;
- asme = tr.transitions[i].getNext(0);
- while (k > 0) {
- result |= safety.getSolverResult(newState, asme);
- if (asme instanceof AvatarStateElement || result == true) {
- break;
+ result = safety.getSolverResult(newState);
+
+ if (!result) {
+ for (int i = 0; i < tr.transitions.length; i++) {
+ int k = 10;
+ asme = tr.transitions[i].getNext(0);
+ while (k > 0) {
+ result |= safety.getSolverResult(newState, asme);
+ if (asme instanceof AvatarStateElement || result == true) {
+ break;
+ }
+ asme = asme.getNext(0);
+ k--;
}
- asme = asme.getNext(0);
- k--;
}
}
} else {
diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index 0fff8d9062..9c5c086387 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -193,6 +193,17 @@ public class SafetyProperty {
}
+ public void linkSolverStates() {
+ //linking to states so that normal bool elaborations are possible
+ if (safetySolver != null) {
+ safetySolver.linkStates();
+ }
+ if (safetySolverLead != null) {
+ safetySolverLead.linkStates();
+ }
+ }
+
+
public String toString() {
String ret = rawProperty;
switch(phase) {
--
GitLab