From 43e030d2f9d9429afa58332e59b9e73c9a158ccc Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Fri, 24 Apr 2020 14:14:36 +0200
Subject: [PATCH] Model-checker: improved heap memory footprint of about 60%
---
.../modelchecker/AvatarModelChecker.java | 17 ++++---
.../modelchecker/SafetyProperty.java | 4 +-
.../modelchecker/SpecificationTransition.java | 49 ++++++-------------
3 files changed, 29 insertions(+), 41 deletions(-)
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index c2a5c24651..5f8ac57c61 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -209,7 +209,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//TraceManager.addDev("null elt in state machine of block=" + block.getName());
//if (elt.canBeVerified() && elt.isChecked()) {
if (elt.isChecked()) {
- SafetyProperty sp = new SafetyProperty(block, elt);
+ SafetyProperty sp = new SafetyProperty(block, elt, SafetyProperty.ALLTRACES_ONESTATE);
livenesses.add(sp);
}
}
@@ -223,7 +223,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
for (AvatarBlock block : spec.getListOfBlocks()) {
for (AvatarStateMachineElement elt : block.getStateMachine().getListOfElements()) {
if (((elt instanceof AvatarStateElement) && (elt.canBeVerified())) || (elt.isCheckable())) {
- SafetyProperty sp = new SafetyProperty(block, elt);
+ SafetyProperty sp = new SafetyProperty(block, elt, SafetyProperty.ALLTRACES_ONESTATE);
livenesses.add(sp);
}
}
@@ -549,7 +549,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
public void stopModelChecking() {
emptyPendingStates();
stoppedBeforeEnd = true;
- safety.result = false;
+ if (studySafety) {
+ safety.result = false;
+ }
TraceManager.addDev("Model checking stopped");
}
@@ -770,7 +772,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
((AvatarActionAssignment) aa).buildActionSolver(block);
}
}
- }else if (elt instanceof AvatarActionOnSignal) {
+ } else if (elt instanceof AvatarActionOnSignal) {
((AvatarActionOnSignal) elt).buildActionSolver(block);
}
}
@@ -1423,7 +1425,8 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ase = getNextState(_st.transitions[i], _newState, 10);
if (ase != null) {
checkElement(ase, _newState);
- int index = _st.blocks[i].getStateMachine().getIndexOfState(ase);
+ //int index = _st.blocks[i].getStateMachine().getIndexOfState(ase);
+ int index = _st.transitions[i].getBlock().getStateMachine().getIndexOfState(ase);
if (index > -1) {
_newState.blocks[_st.blocksInt[i]].values[SpecificationBlock.STATE_INDEX] = index;
}
@@ -1507,7 +1510,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
retAction = "";
}
- return "i(" + _st.blocks[0].getName() + "/" + retAction + ")";
+ //return "i(" + _st.blocks[0].getName() + "/" + retAction + ")";
+ return "i(" + _st.transitions[0].getBlock().getName() + "/" + retAction + ")";
+
}
private String executeSyncTransition(SpecificationState _previousState, SpecificationState _newState, SpecificationTransition _st) {
diff --git a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
index 651b555382..9f599f5554 100644
--- a/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
+++ b/src/main/java/avatartranslator/modelchecker/SafetyProperty.java
@@ -88,7 +88,7 @@ public class SafetyProperty {
analyzeProperty(_spec);
}
- public SafetyProperty(AvatarBlock block, AvatarStateMachineElement state) {
+ public SafetyProperty(AvatarBlock block, AvatarStateMachineElement state, int _safetyType) {
//create liveness safety
this.block = block;
this.state = state;
@@ -96,7 +96,7 @@ public class SafetyProperty {
safetySolver = new AvatarExpressionSolver();
safetySolver.builExpression(attribute);
propertyType = BLOCK_STATE;
- safetyType = ALLTRACES_ONESTATE;
+ safetyType = _safetyType;
result = true;
}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationTransition.java b/src/main/java/avatartranslator/modelchecker/SpecificationTransition.java
index d375c7f9cf..a44e68f79b 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationTransition.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationTransition.java
@@ -57,8 +57,6 @@ public class SpecificationTransition {
public boolean fromStateWithMoreThanOneTransition;
- public AvatarBlock[] blocks;
- public SpecificationBlock[] specBlocks;
public int[] blocksInt;
public AvatarTransition[] transitions;
@@ -71,13 +69,7 @@ public class SpecificationTransition {
public void init(int _nbOfElements, AvatarTransition _at, AvatarBlock _ab, SpecificationBlock _sb, int _blockIndex) {
transitions = new AvatarTransition[_nbOfElements];
- transitions[0] = _at;
-
- blocks = new AvatarBlock[_nbOfElements];
- blocks[0] = _ab;
-
- specBlocks = new SpecificationBlock[_nbOfElements];
- specBlocks[0] = _sb;
+ transitions[0] = _at;
blocksInt = new int[_nbOfElements];
blocksInt[0] = _blockIndex;
@@ -97,14 +89,6 @@ public class SpecificationTransition {
transitions[0] = _tr1.transitions[0];
transitions[1] = _tr2.transitions[0];
- blocks = new AvatarBlock[nbOfElements];
- blocks[0] = _tr1.blocks[0];
- blocks[1] = _tr2.blocks[0];
-
- specBlocks = new SpecificationBlock[nbOfElements];
- specBlocks[0] = _tr1.specBlocks[0];
- specBlocks[1] = _tr2.specBlocks[0];
-
blocksInt = new int[nbOfElements];
blocksInt[0] = _tr1.blocksInt[0];
blocksInt[1] = _tr2.blocksInt[0];
@@ -115,17 +99,17 @@ public class SpecificationTransition {
}
public boolean hasBlockOf(SpecificationTransition _tr) {
- if (blocks == null) {
+ if (transitions == null) {
return false;
}
- if (_tr.blocks == null) {
+ if (_tr.transitions == null) {
return false;
}
- for (int i=0; i<blocks.length; i++) {
- for(int j=0; j<_tr.blocks.length; j++) {
- if (blocks[i] == _tr.blocks[j]) {
+ for (int i=0; i<transitions.length; i++) {
+ for(int j=0; j<_tr.transitions.length; j++) {
+ if (transitions[i].getBlock() == _tr.transitions[j].getBlock()) {
return true;
}
}
@@ -134,6 +118,7 @@ public class SpecificationTransition {
return false;
}
+
public boolean hasBlockIndex(int _index) {
if (blocksInt == null) {
return false;
@@ -151,19 +136,17 @@ public class SpecificationTransition {
public String toString() {
String ret = "Trans: ";
- if (blocks != null) {
- for (int i=0; i<blocks.length; i++) {
- ret += "/ Block" + i + ": " + blocks[i].getName();
- }
+// if (blocks != null) {
+// for (int i=0; i<blocks.length; i++) {
+// ret += "/ Block" + i + ": " + blocks[i].getName();
+// }
+// }
+ if (transitions != null) {
+ for (int i = 0; i < transitions.length; i++) {
+ ret += "/ Block" + i + ": " + transitions[i].getBlock().getName() + "/" + transitions[i];
+ }
}
-
-
- if (transitions != null) {
- for (int i=0; i<transitions.length; i++) {
- ret += "/" + transitions[i];
- }
- }
return ret;
}
--
GitLab