From fc74a45f287373359c1fc68712fbb5c8e320f29f Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Thu, 17 Sep 2020 21:35:33 +0200
Subject: [PATCH] Added BFS/DFS choice, updated deadlock check on DFS
---
.../modelchecker/AvatarModelChecker.java | 31 ++++++++++++++++---
src/main/java/cli/Action.java | 5 +++
.../ui/window/JDialogAvatarModelChecker.java | 16 ++++++++++
3 files changed, 48 insertions(+), 4 deletions(-)
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 801a83fcd8..ccf5f675de 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -81,6 +81,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
// Options
+ private boolean depthSearch;
private boolean ignoreEmptyTransitions;
private boolean ignoreConcurrenceBetweenInternalActions;
private boolean ignoreInternalStates;
@@ -147,6 +148,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
spec = initialSpec.advancedClone();
//TraceManager.addDev("After clone:\n" + spec);
}
+ depthSearch = false;
ignoreEmptyTransitions = true;
ignoreConcurrenceBetweenInternalActions = true;
ignoreInternalStates = true;
@@ -213,6 +215,10 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
public void setFreeIntermediateStateCoding(boolean _b) {
freeIntermediateStateCoding = _b;
}
+
+ public void setSearchType(int searchType) {
+ depthSearch = searchType == 1;
+ }
public void setIgnoreEmptyTransitions(boolean _b) {
ignoreEmptyTransitions = _b;
@@ -459,7 +465,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
public boolean startModelCheckingProperties() {
boolean studyS, studyL, studyR, studyRI, studyAL, genRG, genTrace;
- boolean emptyTr, ignoreConcurrence;
+ boolean depthS, emptyTr, ignoreConcurrence;
long deadlocks = 0;
if (spec == null) {
@@ -477,6 +483,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
stateLimitRG = false;
timeLimitRG = false;
+ depthS = depthSearch;
emptyTr = ignoreEmptyTransitions;
ignoreConcurrence = ignoreConcurrenceBetweenInternalActions;
studyR = studyReachability;
@@ -529,9 +536,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (studyRI) {
studyReinit = true;
+ depthSearch = true;
startModelChecking(nbOfThreads);
deadlocks += nbOfDeadlocks;
resetModelChecking();
+ depthSearch = depthS;
studyReinit = false;
}
@@ -568,6 +577,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
//there is no need to study deadlocks again
if (deadlocks == 0 || genTrace) {
deadlockStop = true;
+ depthSearch = true;
counterexample = genTrace;
ignoreConcurrenceBetweenInternalActions = true;
resetCounterexample();
@@ -577,6 +587,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
resetModelChecking();
ignoreConcurrenceBetweenInternalActions = ignoreConcurrence;
counterexample = false;
+ depthSearch = depthS;
deadlockStop = false;
}
}
@@ -1312,7 +1323,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (studySafety) {
actionOnProperty(newState, i, similar, _ss);
} else {
- pendingStates.add(newState);
+ if (depthSearch && i == 0) {
+ pendingStates.add(0, newState);
+ } else {
+ pendingStates.add(newState);
+ }
if (counterexample && deadlockStop) {
//Register counterexample trace
actionOnProperty(newState, i, similar, _ss);
@@ -1419,7 +1434,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (studySafety) {
actionOnProperty(newState, 0, similar, _ss);
} else {
- pendingStates.add(newState);
+ if (depthSearch) {
+ pendingStates.add(0, newState);
+ } else {
+ pendingStates.add(newState);
+ }
if (counterexample && deadlockStop) {
//Register counterexample trace
actionOnProperty(newState, 0, similar, _ss);
@@ -1512,7 +1531,11 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
if (studySafety) {
actionOnProperty(newState, 0, similar, _ss);
} else {
- pendingStates.add(newState);
+ if (depthSearch) {
+ pendingStates.add(0, newState);
+ } else {
+ pendingStates.add(newState);
+ }
if (counterexample && deadlockStop) {
//Register counterexample trace
actionOnProperty(newState, 0, similar, _ss);
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index 73978e841b..c12ae2b976 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -854,6 +854,7 @@ public class Action extends Command {
+ "-q \"QUERY\"\tquery a safety pragma\n"
+ "-d\tno deadlocks check\n"
+ "-i\ttest model reinitialization\n"
+ + "-dfs\tDFS search preferred over BFS\n"
+ "-a\tno internal actions loops check\n"
+ "-n NUM\tmaximum states created (Only for a non verification study)\n"
+ "-t NUM\tmaximum time (ms) (Only for a non verification study)\n"
@@ -976,6 +977,10 @@ public class Action extends Command {
amc.setReinitAnalysis(true);
reinit = true;
break;
+ case "-dfs":
+ //internal action loops
+ amc.setSearchType(1);
+ break;
case "-a":
//internal action loops
amc.setInternalActionLoopAnalysis(true);
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index b216e4d965..1001eb7107 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -83,6 +83,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
private final static String[] INFOS = {"Not started", "Running", "Stopped by user", "Finished"};
private final static Color[] COLORS = {Color.darkGray, Color.magenta, Color.red, Color.blue};
private final static String[] WORD_BITS = {"32 bits", "16 bits", "8 bits"};
+ private final static String[] SEARCH_TYPE = {"BFS", "DFS"};
public final static int REACHABILITY_ALL = 1;
@@ -116,6 +117,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected static boolean limitTimeSelected = false;
protected static String timeLimitValue;
protected static int wordRepresentationSelected = 1;
+ protected static int searchTypeSelected = 0;
protected MainGUI mgui;
@@ -147,6 +149,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
protected JButton show;
protected JButton display;
protected JComboBox wordRepresentationBox;
+ protected JComboBox searchTypeBox;
//protected JRadioButton exe, exeint;
//protected ButtonGroup exegroup;
@@ -282,6 +285,17 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
ignoreEmptyTransitions.addActionListener(this);
jp01.add(ignoreEmptyTransitions, c01);
+ c01.anchor = GridBagConstraints.EAST;
+ c01.fill = GridBagConstraints.NONE;
+ jp01.add(new JLabel("Search type: "), c01);
+
+ c01.anchor = GridBagConstraints.WEST;
+ c01.fill = GridBagConstraints.HORIZONTAL;
+ searchTypeBox = new JComboBox(SEARCH_TYPE);
+ searchTypeBox.setSelectedIndex(searchTypeSelected);
+ searchTypeBox.addActionListener(this);
+ jp01.add(searchTypeBox, c01);
+
c01.anchor = GridBagConstraints.EAST;
c01.fill = GridBagConstraints.NONE;
jp01.add(new JLabel("Word size: "), c01);
@@ -759,6 +773,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
// Setting options
amc.setCompressionFactor(wordRepresentationSelected << 1);
+ amc.setSearchType(searchTypeSelected);
amc.setIgnoreEmptyTransitions(ignoreEmptyTransitionsSelected);
amc.setIgnoreConcurrenceBetweenInternalActions(ignoreConcurrenceBetweenInternalActionsSelected);
amc.setIgnoreInternalStates(ignoreInternalStatesSelected);
@@ -1145,6 +1160,7 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
checkReinitSelected = reinit.isSelected();
checkActionLoopSelected = actionLoop.isSelected();
wordRepresentationSelected = wordRepresentationBox.getSelectedIndex();
+ searchTypeSelected = searchTypeBox.getSelectedIndex();
if (noReachability.isSelected()) {
reachabilitySelected = REACHABILITY_NONE;
--
GitLab