From 59960744f3530dc0a097f4d55662b7f9d302bccf Mon Sep 17 00:00:00 2001
From: tempiaa <tempiaa@eurecom.fr>
Date: Thu, 23 Jul 2020 09:55:17 +0200
Subject: [PATCH] Added states and transition information in the verification
trace name
---
.../CounterexampleQueryReport.java | 19 +++++++++++++++++++
.../modelchecker/CounterexampleTrace.java | 2 ++
.../ui/window/JDialogAvatarModelChecker.java | 2 ++
3 files changed, 23 insertions(+)
diff --git a/src/main/java/avatartranslator/modelchecker/CounterexampleQueryReport.java b/src/main/java/avatartranslator/modelchecker/CounterexampleQueryReport.java
index 260d420485..b7e719384a 100644
--- a/src/main/java/avatartranslator/modelchecker/CounterexampleQueryReport.java
+++ b/src/main/java/avatartranslator/modelchecker/CounterexampleQueryReport.java
@@ -4,6 +4,8 @@ public class CounterexampleQueryReport {
private String name;
private String query;
private String report;
+ private int nbOfStates;
+ private int nbOfTransitions;
public CounterexampleQueryReport(String name) {
this.name = name;
@@ -36,4 +38,21 @@ public class CounterexampleQueryReport {
this.report = report;
}
+ public int getNbOfStates() {
+ return nbOfStates;
+ }
+
+ public void setNbOfStates(int nbOfStates) {
+ this.nbOfStates = nbOfStates;
+ }
+
+ public int getNbOfTransitions() {
+ return nbOfTransitions;
+ }
+
+ public void setNbOfTransitions(int nbOfTransitions) {
+ this.nbOfTransitions = nbOfTransitions;
+ }
+
+
}
diff --git a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
index d6f104efc1..18843e2400 100644
--- a/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
+++ b/src/main/java/avatartranslator/modelchecker/CounterexampleTrace.java
@@ -266,6 +266,8 @@ public class CounterexampleTrace {
s.insert(0 ,"des(0," + (trace.size() - 1) + "," + statesID.size() + ")\n");
CounterexampleQueryReport cr = new CounterexampleQueryReport(null, query, s.toString());
+ cr.setNbOfStates(statesID.size());
+ cr.setNbOfTransitions(trace.size() - 1);
autTraces.add(cr);
}
diff --git a/src/main/java/ui/window/JDialogAvatarModelChecker.java b/src/main/java/ui/window/JDialogAvatarModelChecker.java
index 5dd270d582..072177cd17 100644
--- a/src/main/java/ui/window/JDialogAvatarModelChecker.java
+++ b/src/main/java/ui/window/JDialogAvatarModelChecker.java
@@ -978,6 +978,8 @@ public class JDialogAvatarModelChecker extends javax.swing.JFrame implements Act
RG rg = new RG(file);
rg.data = tr.getReport();
rg.fileName = filename;
+ rg.nbOfStates = tr.getNbOfStates();
+ rg.nbOfTransitions = tr.getNbOfTransitions();
rg.name = tr.getQuery() + "_" + dateAndTime;
mgui.addRG(rg);
File f = new File(filename);
--
GitLab