From ba194b167a205213c0f3b9bcffd55bae72375c07 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paris.fr>
Date: Mon, 12 Jun 2023 21:01:31 +0200
Subject: [PATCH] Adding test for deadlock modelchecker
---
.../modelchecker/AvatarModelChecker.java | 8 +--
src/main/java/cli/Action.java | 39 ++++++++++++
.../java/cli/CLIAvatarModelCheckerTest.java | 61 +++++++++++++++++++
.../cli/input/scriptmodelcheckerrandom | 2 +-
4 files changed, 105 insertions(+), 5 deletions(-)
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index dbcd351d1d..7e95f090c8 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -2469,16 +2469,16 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
}
for (SpecificationState state : states.values()) {
- TraceManager.addDev("Parsing states");
+ //TraceManager.addDev("Parsing states");
if ((state.nexts == null) || (state.nexts != null) && (state.nexts.size() == 0)) {
- TraceManager.addDev("Deadlock state identified");
+ //TraceManager.addDev("Deadlock state identified");
// Deadlock state
// Must add all states of blocks
for (int i = 0; i < spec.getListOfBlocks().size(); i++) {
AvatarBlock ab = spec.getListOfBlocks().get(i);
- TraceManager.addDev("avatar block: " + ab.getName());
+ //TraceManager.addDev("avatar block: " + ab.getName());
if (state.blocks != null) {
- TraceManager.addDev("Non null blocks of state");
+ //TraceManager.addDev("Non null blocks of state");
SpecificationBlock sb = state.blocks[i];
HashSet<AvatarStateElement> listOfStates;
listOfStates = map.get(ab);
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index d080923920..b16d4eb57a 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -1392,6 +1392,7 @@ public class Action extends Command implements ProVerifOutputListener {
+ "-s\tsafety pragmas verification\n"
+ "-q \"QUERY\"\tquery a safety pragma\n"
+ "-d\tno deadlocks check\n"
+ + "-adv\tadvanced deadlock check: provide a path to a text file"
+ "-i\ttest model reinitialization\n"
+ "-dfs\tDFS search preferred over BFS\n"
+ "-a\tno internal actions loops check\n"
@@ -1453,6 +1454,8 @@ public class Action extends Command implements ProVerifOutputListener {
boolean livenessAnalysis = false;
boolean safetyAnalysis = false;
boolean noDeadlocks = false;
+ String deadlockPaths = "";
+ boolean advancedDeadlock = false;
boolean reinit = false;
boolean actionLoop = false;
for (int i = 0; i < commands.length; i++) {
@@ -1524,6 +1527,16 @@ public class Action extends Command implements ProVerifOutputListener {
amc.setCheckNoDeadlocks(true);
noDeadlocks = true;
break;
+ case "-adv":
+ // Advanced deadlock
+ if (i != commands.length - 1) {
+ amc.setCheckNoDeadlocks(true);
+ advancedDeadlock = true;
+ deadlockPaths = commands[++i];
+ } else {
+ return Interpreter.BAD;
+ }
+ break;
case "-i":
//reinitialization
amc.setReinitAnalysis(true);
@@ -1587,11 +1600,17 @@ public class Action extends Command implements ProVerifOutputListener {
TraceManager.addDev("Starting model checking");
amc.setCounterExampleTrace(counterTraces, counterTracesAUT);
+ if (advancedDeadlock) {
+ amc.setFreeIntermediateStateCoding(false);
+ }
+
if (livenessAnalysis || safetyAnalysis || noDeadlocks) {
amc.startModelCheckingProperties();
} else {
amc.startModelChecking();
}
+
+
System.out.println("Model checking done\nGraph: states:" + amc.getNbOfStates() +
" links:" + amc.getNbOfLinks() + "\n");
@@ -1716,6 +1735,26 @@ public class Action extends Command implements ProVerifOutputListener {
}
}
+ if (advancedDeadlock && deadlockPaths != null) {
+ try {
+ File f = new File(deadlockPaths);
+ StringBuffer sb = new StringBuffer("");
+ HashMap<AvatarBlock, HashSet<AvatarStateElement>> mapOfDeadlockStates = amc.getMapOfDeadlockStates();
+ for (AvatarBlock ab : mapOfDeadlockStates.keySet()) {
+ interpreter.print("deadlock state for " + ab.getName() + ":");
+ sb.append("#" + ab.getName() + "\n");
+ for (AvatarStateElement ase : mapOfDeadlockStates.get(ab)) {
+ interpreter.print("\t- state \"" + ase.getName() + "\"");
+ sb.append("-" + ase.getName() + "\n");
+ }
+ }
+ FileUtils.saveFile(f, sb.toString());
+ } catch (Exception e) {
+ return Interpreter.BAD;
+ }
+
+ }
+
return null;
}
};
diff --git a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
index a1822cdfdb..ed46e6c1d6 100644
--- a/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
+++ b/ttool/src/test/java/cli/CLIAvatarModelCheckerTest.java
@@ -47,7 +47,11 @@ package cli;
import static org.junit.Assert.assertEquals;
import static org.junit.Assert.assertTrue;
+
+import java.io.BufferedReader;
import java.io.File;
+import java.io.FileReader;
+import java.io.IOException;
import java.util.ArrayList;
import common.ConfigurationTTool;
@@ -55,6 +59,7 @@ import common.SpecConfigTTool;
import graph.AUTGraph;
import graph.AUTTransition;
import myutil.Conversion;
+import myutil.TraceManager;
import org.junit.Test;
import test.AbstractTest;
@@ -64,6 +69,8 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
final static String PATH_TO_TEST_FILE = "cli/input/";
final static String PATH_TO_EXPECTED_FILE = "cli/expected/";
private StringBuilder outputResult;
+
+ private static final String DEADLOCKS [] = {"#MainBlock", "-stop", "#Receiver", "-stopCreated", "-MainChoice"};
public CLIAvatarModelCheckerTest() {
//
@@ -485,7 +492,61 @@ public class CLIAvatarModelCheckerTest extends AbstractTest implements Interpret
assertTrue(graph.getNbOfStates() == 49);
assertTrue(graph.getNbOfTransitions() == 48);
+ filePath = "deadlockmodel.txt";
+ f = new File(filePath);
+ assertTrue(myutil.FileUtils.checkFileForOpen(f));
+
+ BufferedReader reader;
+ String block = "";
+ String state = "";
+ try {
+ reader = new BufferedReader(new FileReader("deadlockmodel.txt"));
+ String line = "";
+ while (line != null) {
+ // read next line
+ line = reader.readLine();
+ if (line == null) {
+ break;
+ }
+ TraceManager.addDev("line of file=" + line);
+ if (line.startsWith("#")) {
+ block = line.trim();
+ TraceManager.addDev("Block=" + block);
+ }
+ if (line.startsWith("-")) {
+ state = line.trim();
+ assertTrue(checkNames(block, state));
+ }
+
+ }
+ reader.close();
+ } catch (IOException e) {
+ assertTrue(false);
+ }
+
+
+ }
+
+ private boolean checkNames(String blockName, String stateName) {
+ TraceManager.addDev("Checking for block=" + blockName + " state=" + stateName);
+ boolean blockFound = false;
+ for(String s: DEADLOCKS) {
+ TraceManager.addDev("s=" + s);
+ if (s.compareTo(blockName) == 0) {
+ blockFound = true;
+ TraceManager.addDev("Found block");
+ } else if (blockFound) {
+ if (s.startsWith("#")) {
+ return false;
+ }
+ if (s.compareTo(stateName) == 0) {
+ TraceManager.addDev("s found");
+ return true;
+ }
+ }
+ }
+ return false;
}
}
diff --git a/ttool/src/test/resources/cli/input/scriptmodelcheckerrandom b/ttool/src/test/resources/cli/input/scriptmodelcheckerrandom
index 86695fe2be..bebbec4837 100644
--- a/ttool/src/test/resources/cli/input/scriptmodelcheckerrandom
+++ b/ttool/src/test/resources/cli/input/scriptmodelcheckerrandom
@@ -7,5 +7,5 @@ wait 2
action open $model
wait 4
action check-syntax
-action avatar-rg -g rgmodelcheckerrandom.aut
+action avatar-rg -adv deadlockmodel.txt -g rgmodelcheckerrandom.aut
action quit
--
GitLab