From da69f175b4a229ab332a897dff79e137b41eb720 Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Thu, 25 Jun 2020 13:57:51 +0200
Subject: [PATCH] More optimization for memory
---
.../avatartranslator/AvatarSpecification.java | 6 +++
.../avatartranslator/AvatarTransition.java | 42 +++++++++++++---
.../modelchecker/AvatarModelChecker.java | 48 +++++++++++--------
.../modelchecker/SpecificationState.java | 9 +---
.../ui/window/JDialogAvatarModelChecker.java | 1 +
5 files changed, 72 insertions(+), 34 deletions(-)
diff --git a/src/main/java/avatartranslator/AvatarSpecification.java b/src/main/java/avatartranslator/AvatarSpecification.java
index deed36170e..9e5433fbef 100644
--- a/src/main/java/avatartranslator/AvatarSpecification.java
+++ b/src/main/java/avatartranslator/AvatarSpecification.java
@@ -367,6 +367,12 @@ public class AvatarSpecification extends AvatarElement {
errors.add(at);
}
}
+ if (at.hasDelay()) {
+ returnVal = at.buildDelaySolver();
+ if (returnVal == false) {
+ errors.add(at);
+ }
+ }
for (AvatarAction aa : at.getActions()) {
if (aa instanceof AvatarActionAssignment) {
returnVal = ((AvatarActionAssignment) aa).buildActionSolver(block);
diff --git a/src/main/java/avatartranslator/AvatarTransition.java b/src/main/java/avatartranslator/AvatarTransition.java
index 18fc1432d4..935731cda8 100644
--- a/src/main/java/avatartranslator/AvatarTransition.java
+++ b/src/main/java/avatartranslator/AvatarTransition.java
@@ -93,10 +93,9 @@ public class AvatarTransition extends AvatarStateMachineElement {
private String minCompute = "", maxCompute = "";
private AvatarStateMachineOwner block;
-
-
-
private AvatarExpressionSolver guardSolver;
+ private AvatarExpressionSolver minDelaySolver;
+ private AvatarExpressionSolver maxDelaySolver;
private List<AvatarAction> actions; // actions on variable, or method call
@@ -106,6 +105,8 @@ public class AvatarTransition extends AvatarStateMachineElement {
this.guard = new AvatarGuardEmpty();
this.block = _block;
guardSolver = null;
+ minDelaySolver = null;
+ maxDelaySolver = null;
}
public AvatarGuard getGuard() {
@@ -113,15 +114,42 @@ public class AvatarTransition extends AvatarStateMachineElement {
}
public boolean buildGuardSolver() {
- String expr = guard.toString().replaceAll("\\[", "").trim();
- expr = expr.replaceAll("\\]", "");
- guardSolver = new AvatarExpressionSolver(expr);
- return guardSolver.buildExpression((AvatarBlock) block);
+ if (isGuarded()) {
+ String expr = guard.toString().replaceAll("\\[", "").trim();
+ expr = expr.replaceAll("\\]", "");
+ guardSolver = new AvatarExpressionSolver(expr);
+ return guardSolver.buildExpression((AvatarBlock) block);
+ }
+ return true;
+ }
+
+ public boolean buildDelaySolver() {
+ boolean result;
+ if (hasDelay()) {
+ minDelaySolver = new AvatarExpressionSolver(minDelay);
+ result = minDelaySolver.buildExpression((AvatarBlock) block);
+ if (maxDelay.trim().length() != 0) {
+ maxDelaySolver = new AvatarExpressionSolver(maxDelay);
+ result &= maxDelaySolver.buildExpression((AvatarBlock) block);
+ } else {
+ maxDelaySolver = minDelaySolver;
+ }
+ return result;
+ }
+ return true;
}
public AvatarExpressionSolver getGuardSolver() {
return guardSolver;
}
+
+ public AvatarExpressionSolver getMinDelaySolver() {
+ return minDelaySolver;
+ }
+
+ public AvatarExpressionSolver getMaxDelaySolver() {
+ return maxDelaySolver;
+ }
public void setGuard(AvatarGuard _guard) {
this.guard = _guard;
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 744713c9e6..c05d093335 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -85,6 +85,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private boolean ignoreConcurrenceBetweenInternalActions;
private boolean ignoreInternalStates;
private boolean verboseInfo;
+ private int compressionFactor;
// RG
private boolean computeRG;
@@ -152,6 +153,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
counterexample = false;
freeIntermediateStateCoding = true;
verboseInfo = true;
+ compressionFactor = 1;
}
public AvatarSpecification getInitialSpec() {
@@ -213,6 +215,16 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ignoreInternalStates = _b;
}
+ public void setCompressionFactor(int compressionFactor) {
+ if (compressionFactor == 2 || compressionFactor == 4) {
+ this.compressionFactor = compressionFactor;
+ spec.sortAttributes();
+ spec.setAttributeOptRatio(compressionFactor);
+ } else {
+ compressionFactor = 1;
+ }
+ }
+
public void setCheckNoDeadlocks(boolean _checkNoDeadlocks) {
checkNoDeadlocks = _checkNoDeadlocks;
deadlockStop = false;
@@ -736,7 +748,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
prepareStates();
spec.sortAttributes();
- spec.setAttributeOptRatio(2);
+ spec.setAttributeOptRatio(compressionFactor);
initExpressionSolvers();
prepareTransitions();
@@ -966,10 +978,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
- private void prepareTransitionsOfState(SpecificationState _ss) {
+ private ArrayList<SpecificationTransition> prepareTransitionsOfState(SpecificationState _ss) {
int cpt;
- _ss.transitions = new ArrayList<SpecificationTransition>();
+ ArrayList<SpecificationTransition> transitions = new ArrayList<SpecificationTransition>();
//TraceManager.addDev("Preparing transitions of state " + _ss);
@@ -984,12 +996,14 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
for (AvatarStateMachineElement elt : ase.getNexts()) {
if (elt instanceof AvatarTransition) {
- handleAvatarTransition((AvatarTransition) elt, block, sb, cpt, _ss.transitions, ase.getNexts().size() > 1);
+ handleAvatarTransition((AvatarTransition) elt, block, sb, cpt, transitions, ase.getNexts().size() > 1);
}
}
cpt++;
}
+
+ return transitions;
}
@@ -1001,10 +1015,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return;
}
- prepareTransitionsOfState(_ss);
+ ArrayList<SpecificationTransition> transitions = prepareTransitionsOfState(_ss);
- if (_ss.transitions == null) {
+ if (transitions == null) {
TraceManager.addDev("null transitions");
nbOfDeadlocks++;
checkPropertyOnDeadlock(_ss);
@@ -1013,7 +1027,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
//TraceManager.addDev("Possible transitions 1:" + transitions.size());
- ArrayList<SpecificationTransition> transitions = computeValidTransitions(_ss.transitions);
+ transitions = computeValidTransitions(transitions);
//TraceManager.addDev("Possible transitions 3:" + transitions.size());
@@ -1176,8 +1190,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (freeIntermediateStateCoding) {
_ss.freeUselessAllocations();
- } else {
- _ss.finished();
}
mustStop();
@@ -1284,9 +1296,9 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// Compute next transition
//prepareTransitionsOfState(previousState);
- prepareTransitionsOfState(newState);
+ ArrayList<SpecificationTransition> transitions = prepareTransitionsOfState(newState);
- if (newState.transitions == null) {
+ if (transitions == null) {
TraceManager.addDev("null transitions");
nbOfDeadlocks++;
checkPropertyOnDeadlock(_ss);
@@ -1294,7 +1306,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
return;
}
- ArrayList<SpecificationTransition> transitions = computeValidTransitions(newState.transitions);
+ transitions = computeValidTransitions(transitions);
st = null;
if (ignoreConcurrenceBetweenInternalActions) {
@@ -1365,8 +1377,6 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (freeIntermediateStateCoding) {
_ss.freeUselessAllocations();
- } else {
- _ss.finished();
}
mustStop();
@@ -1382,13 +1392,13 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ArrayList<Integer> stackStates = new ArrayList<>(); //keeps track of the block hashes
do {
- prepareTransitionsOfState(prevState);
+ ArrayList<SpecificationTransition> transitions = prepareTransitionsOfState(prevState);
- if (prevState.transitions == null) {
+ if (transitions == null) {
return prevState;
}
- ArrayList<SpecificationTransition> transitions = computeValidTransitions(prevState.transitions);
+ transitions = computeValidTransitions(transitions);
stackStates.add(prevState.hashValue);
found = false;
@@ -1494,13 +1504,13 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if ((minDelay == null) || (minDelay.length() == 0)) {
st.clockMin = 0 - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
} else {
- st.clockMin = evaluateIntExpression(_at.getMinDelay(), _block, _sb) - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
+ st.clockMin = _at.getMinDelaySolver().getResult(_sb) - _sb.values[SpecificationBlock.CLOCKMAX_INDEX];
}
String maxDelay = _at.getMaxDelay().trim();
if ((maxDelay == null) || (maxDelay.length() == 0)) {
st.clockMax = 0 - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
} else {
- int resMax = evaluateIntExpression(_at.getMaxDelay(), _block, _sb);
+ int resMax = _at.getMaxDelaySolver().getResult(_sb);
_sb.maxClock = Math.max(_sb.maxClock, resMax);
st.clockMax = resMax - _sb.values[SpecificationBlock.CLOCKMIN_INDEX];
}
diff --git a/src/main/java/avatartranslator/modelchecker/SpecificationState.java b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
index 51247a4d4c..2d4533bad7 100644
--- a/src/main/java/avatartranslator/modelchecker/SpecificationState.java
+++ b/src/main/java/avatartranslator/modelchecker/SpecificationState.java
@@ -65,9 +65,8 @@ public class SpecificationState implements Comparable<SpecificationState> {
public LinkedList<SpecificationLink> nexts; // The RG is there
public boolean property; //trace the property check at this state
public boolean elaborated; //true only if the elaboration has been completed
- public ArrayList<SpecificationTransition> transitions;
-// public long distance; //max #steps to be reached from S0
+
public SpecificationState() {
hashComputed = false;
property = false;
@@ -193,14 +192,8 @@ public class SpecificationState implements Comparable<SpecificationState> {
return 0;
}
- public void finished() {
- //blocks = null;
- transitions = null;
- }
-
public void freeUselessAllocations() {
blocks = null;
- transitions = null;
}
public int compareTo( SpecificationState _s ) {
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 225f9ee218..0b78621a84 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -729,6 +729,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
timer.scheduleAtFixedRate(mcm, 0, 500);
// Setting options
+ amc.setCompressionFactor(1);
amc.setIgnoreEmptyTransitions(ignoreEmptyTransitionsSelected);
amc.setIgnoreConcurrenceBetweenInternalActions(ignoreConcurrenceBetweenInternalActionsSelected);
amc.setIgnoreInternalStates(ignoreInternalStatesSelected);
--
GitLab