From 62fe0f11618a73c7bf1ee45885f3305e9eb9e7ce Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Thu, 19 Feb 2015 10:34:34 +0100
Subject: [PATCH] remove more trace outputs in Model Checking result dialog
---
.../eventb/ModelCheckingFinishedListener.java | 21 ++++++++++---------
1 file changed, 11 insertions(+), 10 deletions(-)
diff --git a/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java b/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java
index 3cde356c..0383d34e 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java
@@ -144,24 +144,25 @@ public class ModelCheckingFinishedListener extends JobChangeAdapter {
StringBuffer sb = new StringBuffer();
sb.append("Theorem violation found.\n");
sb.append("ProB has detected a state that violates the theorems.\n");
- sb.append("The following is the trace that led to the violation:\n");
- appendTrace(trace, sb);
+ // no longer show trace of state ids to user; not very useful
+ //sb.append("The following is the trace that led to the violation:\n");
+ //appendTrace(trace, sb);
return sb.toString();
}
private String createStateErrorResult(final List<String> trace) {
StringBuffer sb = new StringBuffer();
sb.append("ProB has detected an erroneous state (e.g., witness error, guard strengthening error).\n");
- sb.append("The following is the trace that led to the error:\n");
- appendTrace(trace, sb);
+ //sb.append("The following is the trace that led to the error:\n");
+ //appendTrace(trace, sb);
return sb.toString();
}
private String createWDErrorResult(final List<String> trace) {
StringBuffer sb = new StringBuffer();
sb.append("ProB has detected a state which caused a well-definedness error(e.g., division by zero).\n");
- sb.append("The following is the trace that led to the error:\n");
- appendTrace(trace, sb);
+ //sb.append("The following is the trace that led to the error:\n");
+ //appendTrace(trace, sb);
return sb.toString();
}
@@ -169,8 +170,8 @@ public class ModelCheckingFinishedListener extends JobChangeAdapter {
StringBuffer sb = new StringBuffer();
sb.append("ProB has detected a state which caused an internal error.\n");
sb.append("This is probably a bug (please report).\n");
- sb.append("The following is the trace that led to the error:\n");
- appendTrace(trace, sb);
+ //sb.append("The following is the trace that led to the error:\n");
+ //appendTrace(trace, sb);
return sb.toString();
}
@@ -178,8 +179,8 @@ public class ModelCheckingFinishedListener extends JobChangeAdapter {
StringBuffer sb = new StringBuffer();
sb.append("Deadlock found.\n");
sb.append("ProB has detected a state where all guards are false.\n");
- sb.append("The following is the trace that led to the deadlock:\n");
- appendTrace(trace, sb);
+ //sb.append("The following is the trace that led to the deadlock:\n");
+ //appendTrace(trace, sb);
return sb.toString();
}
--
GitLab