From bbe4e2133ac38d134fdfc27278513ff6da7d8267 Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Wed, 1 Jul 2020 15:13:01 +0200
Subject: [PATCH] Patch, exaustive loop search inserted for non trivial
counterexamples
---
.../modelchecker/AvatarModelChecker.java | 2 +-
.../modelchecker/CounterexampleTrace.java | 104 +++++++++++++++++-
src/main/java/cli/Action.java | 50 +++++++--
3 files changed, 147 insertions(+), 9 deletions(-)
diff --git a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
index 33626e9137..abf79a425a 100644
--- a/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
+++ b/src/main/java/avatartranslator/modelchecker/AvatarModelChecker.java
@@ -959,7 +959,7 @@ public class AvatarModelChecker implements Runnable, myutil.Graph {
private void generateCounterexample() {
if (counterexample && counterTrace.hasCounterexample()) {
- counterTrace.buildTrace();
+ counterTrace.buildTrace(states, traceStates);
if (studySafety) {
counterTraceReport.append("Trace for " + safety.getRawProperty() + "\n");
counterTraceReport.append(counterTrace.generateSimpleTrace(states) + "\n\n");
diff --git a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
index 1cec7d0368..1450e65a8b 100644
--- a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
+++ b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
@@ -2,9 +2,13 @@ package avatartranslator.modelchecker;
import java.util.ArrayList;
import java.util.HashMap;
+import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
+import java.util.Set;
+
+import com.sun.net.httpserver.Authenticator.Result;
import avatartranslator.AvatarBlock;
import avatartranslator.AvatarSpecification;
@@ -78,6 +82,70 @@ public class CounterexampleTrace {
}
+ public boolean buildTrace(Map<Integer, SpecificationState> states, Map<Integer, CounterexampleTraceState> counterstates) {
+ if (counterexampleState == null) {
+ return false;
+ }
+
+ trace = new LinkedList<CounterexampleTraceState>();
+
+ CounterexampleTraceState cs = counterexampleState;
+ CounterexampleTraceState loopPoint = counterstates.get(counterexampleState.hash);
+
+ if (loopPoint != null) {
+ //search for a loop
+ boolean loop = false;
+ while (cs.father != null) {
+ cs = cs.father;
+ if (cs == loopPoint) {
+ loop = true;
+ }
+ }
+ if (loop == true) {
+ //registered path contains a loop
+ cs = counterexampleState;
+ trace.add(cs);
+ while (cs.father != null) {
+ cs = cs.father;
+ trace.add(0, cs);
+ }
+ } else {
+ //registered path does not contain a loop
+ cs = loopPoint;
+ trace.add(cs);
+ while (cs.father != null) {
+ cs = cs.father;
+ trace.add(0, cs);
+ }
+ List<SpecificationState> loopTrace = findLoopTrace(states.get(loopPoint.hash));
+ if (loopTrace != null) {
+ //integrate
+ for (SpecificationState ss : loopTrace) {
+ trace.add(counterstates.get(ss.hashValue));
+ }
+ } else {
+ //continue normally
+ int pos = trace.size();
+ cs = counterexampleState;
+ while (cs.father != loopPoint) {
+ cs = cs.father;
+ trace.add(pos, cs);
+ }
+ }
+ }
+ } else {
+ //normal trace
+ trace.add(cs);
+ while (cs.father != null) {
+ cs = cs.father;
+ trace.add(0, cs);
+ }
+ }
+
+ return true;
+ }
+
+
public String toString() {
if (trace == null) {
return "";
@@ -138,7 +206,7 @@ public class CounterexampleTrace {
int id = 0;
SpecificationState state = null;
for (CounterexampleTraceState cs : trace) {
- if (state != null) {
+ if (state != null && state.nexts != null) {
for (SpecificationLink sl : state.nexts) {
if (sl.destinationState.hashValue == cs.hash) {
s.append("Transition " + sl.action + "\n");
@@ -203,5 +271,39 @@ public class CounterexampleTrace {
CounterexampleQueryReport cr = new CounterexampleQueryReport(null, query, s.toString());
autTraces.add(cr);
}
+
+ private List<SpecificationState> findLoopTrace(SpecificationState start) {
+ Set<Long> visited= new HashSet<Long>();
+ List<SpecificationState> loopTrace = new ArrayList<>();
+
+ if (!(start.getNextsSize() == 0 || visited.contains(start.id))) {
+ for (SpecificationLink i : start.nexts) {
+ if(findLoopTraceRec(i.destinationState, start, visited, loopTrace, 0)) {
+ return loopTrace;
+ }
+ }
+ }
+
+ return null;
+ }
+
+ private boolean findLoopTraceRec(SpecificationState start, SpecificationState arrival, Set<Long> visited, List<SpecificationState> loopTrace, int depth) {
+ loopTrace.add(depth, start);
+
+ if (start == arrival) {
+ return true;
+ } else if (start.getNextsSize() == 0 || visited.contains(start.id)) {
+ return false;
+ }
+
+ visited.add(start.id);
+ for (SpecificationLink i : start.nexts) {
+ if (findLoopTraceRec(i.destinationState, arrival, visited, loopTrace, depth + 1)) {
+ return true;
+ }
+ }
+ loopTrace.remove(depth);
+ return false;
+ }
}
diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java
index 9517a5e392..ebee80e5eb 100644
--- a/src/main/java/cli/Action.java
+++ b/src/main/java/cli/Action.java
@@ -41,6 +41,7 @@ package cli;
import avatartranslator.AvatarSpecification;
import avatartranslator.modelchecker.AvatarModelChecker;
+import avatartranslator.modelchecker.CounterexampleQueryReport;
import avatartranslator.modelcheckervalidator.ModelCheckerValidator;
import common.ConfigurationTTool;
import common.SpecConfigTTool;
@@ -854,7 +855,8 @@ public class Action extends Command {
+ "-n NUM\tmaximum states created (Only for a non verification study)\n"
+ "-t NUM\tmaximum time (ms) (Only for a non verification study)\n"
+ "-c\tconsider full concurrency between actions\n"
- + "-v FILE\tsave counterexample traces for pragmas in FILE";
+ + "-v FILE\tsave counterexample traces for pragmas in FILE"
+ + "-va FILE\tsave counterexample traces and AUT graph for pragmas in FILE";
}
public String getExample() {
@@ -889,6 +891,7 @@ public class Action extends Command {
amc.setComputeRG(false);
boolean rgGraph = false;
boolean counterTraces = false;
+ boolean counterTracesAUT = false;
boolean reachabilityAnalysis = false;
boolean livenessAnalysis = false;
boolean safetyAnalysis = false;
@@ -997,6 +1000,16 @@ public class Action extends Command {
return Interpreter.BAD;
}
break;
+ case "-va":
+ if (i != commands.length - 1) {
+ counterPath = commands[++i];
+ amc.setCounterExampleTrace(true, true);
+ counterTraces = true;
+ counterTracesAUT = true;
+ } else {
+ return Interpreter.BAD;
+ }
+ break;
default:
return Interpreter.BAD;
}
@@ -1031,17 +1044,40 @@ public class Action extends Command {
if (counterTraces) {
String trace = amc.getCounterTrace();
- String autfile;
+ String file;
if (counterPath.indexOf("$") != -1) {
- autfile = Conversion.replaceAllChar(counterPath, '$', dateAndTime);
+ file = Conversion.replaceAllChar(counterPath, '$', dateAndTime);
} else {
- autfile = counterPath;
+ file = counterPath;
}
try {
- FileUtils.saveFile(autfile, trace);
- System.out.println("\nCounterexample trace saved in " + autfile + "\n");
+ File f = new File(file);
+ FileUtils.saveFile(file, trace);
+ System.out.println("\nCounterexample trace saved in " + file + "\n");
} catch (Exception e) {
- System.out.println("\nCounterexample trace could not be saved in " + autfile + "\n");
+ System.out.println("\nCounterexample trace could not be saved in " + file + "\n");
+ }
+
+ List<CounterexampleQueryReport> autTraces = amc.getAUTTraces();
+ if (autTraces != null) {
+ int i = 0;
+ String autfile = FileUtils.removeFileExtension(file);
+ for (CounterexampleQueryReport tr : autTraces) {
+ String filename = autfile + "_" + i + ".aut";
+ try {
+ RG rg = new RG(file);
+ rg.data = tr.getReport();
+ rg.fileName = filename;
+ rg.name = tr.getQuery();
+ interpreter.mgui.addRG(rg);
+ File f = new File(filename);
+ FileUtils.saveFile(filename, tr.getReport());
+ System.out.println("Counterexample graph trace " + tr.getQuery() + " saved in " + filename + "\n");
+ } catch (Exception e) {
+ System.out.println("Counterexample graph trace "+ tr.getQuery() + " could not be saved in " + filename + "\n");
+ }
+ i++;
+ }
}
}
--
GitLab