From c8134e3a37a03ac0a791190b8c8d2b9493e76373 Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Thu, 30 Apr 2020 11:20:54 +0200
Subject: [PATCH] Optimized synchronization of signals for better performance
---
.../modelchecker/AvatarModelChecker.java | 63 ++++++++++++++-----
1 file changed, 48 insertions(+), 15 deletions(-)
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index b50c1bba22..d5ed7b9073 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -72,6 +72,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private Map<Long, SpecificationState> statesByID;
private List<SpecificationState> pendingStates;
private List<SpecificationState> safetyLeadStates;
+ private Map<AvatarTransition, Set<AvatarTransition>> signalRelation;
//private List<SpecificationLink> links;
private int nbOfLinks;
private long stateID = 0;
@@ -1244,7 +1245,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// Compute the id of each transition
// Assumes the allStates list has been computed in AvatarStateMachine
// Assumes that it is only after states that transitions have non empty
-
+ signalRelation = new HashMap<AvatarTransition, Set<AvatarTransition>>();
for (AvatarBlock block : spec.getListOfBlocks()) {
AvatarStateMachine asm = block.getStateMachine();
@@ -1263,6 +1264,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
at.type = AvatarTransition.TYPE_RECV_SYNC;
} else {
at.type = AvatarTransition.TYPE_SEND_SYNC;
+ synchronizeSignalRelation(at, sig);
}
}
} else {
@@ -1294,6 +1296,31 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
ab.setBlockIndex(i++);
}
}
+
+ private void synchronizeSignalRelation(AvatarTransition sender, AvatarSignal sig) {
+ HashSet<AvatarTransition> set = new HashSet<>();
+
+ for (AvatarBlock block : spec.getListOfBlocks()) {
+ AvatarStateMachine asm = block.getStateMachine();
+ if (asm != null) {
+ for (int i = 0; i < asm.allStates.length; i++) {
+ for (int j = 0; j < asm.allStates[i].nbOfNexts(); j++) {
+ AvatarStateMachineElement e = asm.allStates[i].getNext(j);
+ if (e instanceof AvatarTransition) {
+ AvatarStateMachineElement n = e.getNext(0);
+ if (n != null && n instanceof AvatarActionOnSignal) {
+ AvatarSignal asr = ((AvatarActionOnSignal) n).getSignal();
+ if (asr.isIn() && spec.areSynchronized(sig, asr)) {
+ set.add((AvatarTransition) e);
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ signalRelation.put(sender, set);
+ }
public boolean oldEvaluateBoolExpression(String _expr, AvatarBlock _block, SpecificationBlock _sb) {
String act = _expr;
@@ -1395,20 +1422,26 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
private SpecificationTransition computeSynchronousTransition(SpecificationTransition sender, SpecificationTransition receiver) {
- AvatarTransition trs = sender.transitions[0];
- AvatarTransition trr = receiver.transitions[0];
-
- AvatarStateMachineElement asmes, asmer;
- asmes = trs.getNext(0);
- asmer = trr.getNext(0);
- if ((asmes == null) || (asmer == null)) return null;
- if (!(asmes instanceof AvatarActionOnSignal)) return null;
- if (!(asmer instanceof AvatarActionOnSignal)) return null;
-
- AvatarSignal ass = ((AvatarActionOnSignal) asmes).getSignal();
- AvatarSignal asr = ((AvatarActionOnSignal) asmer).getSignal();
-
- if (spec.areSynchronized(ass, asr)) {
+// AvatarTransition trs = sender.transitions[0];
+// AvatarTransition trr = receiver.transitions[0];
+//
+// AvatarStateMachineElement asmes, asmer;
+// asmes = trs.getNext(0);
+// asmer = trr.getNext(0);
+// if ((asmes == null) || (asmer == null)) return null;
+// if (!(asmes instanceof AvatarActionOnSignal)) return null;
+// if (!(asmer instanceof AvatarActionOnSignal)) return null;
+//
+// AvatarSignal ass = ((AvatarActionOnSignal) asmes).getSignal();
+// AvatarSignal asr = ((AvatarActionOnSignal) asmer).getSignal();
+//
+// if (spec.areSynchronized(ass, asr)) {
+// SpecificationTransition st = new SpecificationTransition();
+// st.makeFromTwoSynchronous(sender, receiver);
+// return st;
+// }
+
+ if (signalRelation.get(sender.transitions[0]).contains(receiver.transitions[0])) {
SpecificationTransition st = new SpecificationTransition();
st.makeFromTwoSynchronous(sender, receiver);
return st;
--
GitLab