From bccb3b48f6355f9feb7f8f0399a1e5701ca17a11 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Wed, 24 Jul 2024 07:40:42 +0200
Subject: [PATCH] save error message of TLCError
to provide a useful error message in ProB2-UI
---
src/main/java/de/tlc4b/tlc/TLCResults.java | 17 ++++++++++++-----
1 file changed, 12 insertions(+), 5 deletions(-)
diff --git a/src/main/java/de/tlc4b/tlc/TLCResults.java b/src/main/java/de/tlc4b/tlc/TLCResults.java
index b5f58e3..7ec7edc 100644
--- a/src/main/java/de/tlc4b/tlc/TLCResults.java
+++ b/src/main/java/de/tlc4b/tlc/TLCResults.java
@@ -5,6 +5,7 @@ import de.tlc4b.exceptions.NotSupportedException;
import tla2sany.semantic.*;
import tla2sany.st.Location;
import tlc2.output.EC;
+import tlc2.output.MP;
import tlc2.output.Message;
import tlc2.output.OutputCollector;
import tlc2.tool.BuiltInOPs;
@@ -20,7 +21,7 @@ import static tlc2.output.MP.*;
public class TLCResults implements ToolGlobals {
private TLCResult tlcResult;
- private String violatedDefinition;
+ private String violatedDefinition, tlcErrorMessage;
private Date startTime;
private Date endTime;
private LinkedHashMap<String, Long> operationsCount;
@@ -191,11 +192,14 @@ public class TLCResults implements ToolGlobals {
private void evalAllMessages() {
- ArrayList<Message> messages = OutputCollector.getAllMessages();
+ ArrayList<Message> messages = new ArrayList<>(OutputCollector.getAllMessages());
for (Message m : messages) {
switch (m.getMessageClass()) {
case ERROR:
evalErrorMessage(m);
+ if (tlcResult == null) {
+ tlcErrorMessage = MP.getError(m.getMessageCode(), m.getParameters());
+ }
break;
case TLCBUG:
break;
@@ -212,10 +216,9 @@ public class TLCResults implements ToolGlobals {
}
}
- if (this.tlcResult == null) {
- // this.tlcResult = TLCError;
+ if (this.tlcErrorMessage != null) {
+ this.tlcResult = TLCError;
}
-
}
private void evalStatusMessage(Message m) {
@@ -388,6 +391,10 @@ public class TLCResults implements ToolGlobals {
return tlcResult;
}
+ public String getTLCErrorMessage() {
+ return tlcErrorMessage;
+ }
+
public String getResultString() {
if (tlcResult == TLCResult.InvariantViolation) {
return "Invariant Violation";
--
GitLab