From d308a7a0520b3afa3750c2083fa960144dce519d Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@cs.uni-duesseldorf.de>
Date: Tue, 8 Oct 2019 14:56:50 +0200
Subject: [PATCH] extend messages of some cbc checks
The messages provide more details
explaining the result of the check.
---
.../prob/ui/assertion/AssertionCheckFinishedListener.java | 6 +++---
.../ui/assertion/AssertionDynCheckFinishedListener.java | 6 +++---
.../de/prob/ui/deadlock/DeadlockCheckFinishedListener.java | 4 ++--
3 files changed, 8 insertions(+), 8 deletions(-)
diff --git a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java
index 0843def5..4836aadd 100644
--- a/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java
+++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionCheckFinishedListener.java
@@ -50,17 +50,17 @@ public class AssertionCheckFinishedListener extends ProBJobFinishedListener {
case NO_COUNTER_EXAMPLE_EXISTS:
dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Counter-Example Exists";
- message = "No Counter-Example to the Context Theorems exists.";
+ message = "No Counter-Example to the Context Theorems exists (for current settings of deferred sets).\nIf your model contains deferred sets, there may exist counter-examples for other sizes of these sets.";
break;
case NO_COUNTER_EXAMPLE_FOUND:
dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Counter-Example Found";
- message = "No Counter-Example to the Context Theorems was found.";
+ message = "No Counter-Example to the Context Theorems was found (but one may exist).";
break;
case COUNTER_EXAMPLE:
dialogType = MessageDialog.WARNING;
dialogTitle = "COUNTER-EXAMPLE FOUND!";
- message = "The model contains a Counter-Example state for the Context Theorems, it will be shown in the state view.";
+ message = "A counter-example to the context theorems was found: it will be shown in the state view.\nThis counter-example state satisfies the axioms but not all theorems.";
displayCounterExample(command, animator);
break;
case INTERRUPTED:
diff --git a/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.java b/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.java
index 074c5ae5..f8defdbc 100644
--- a/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.java
+++ b/de.prob.ui/src/de/prob/ui/assertion/AssertionDynCheckFinishedListener.java
@@ -50,17 +50,17 @@ public class AssertionDynCheckFinishedListener extends ProBJobFinishedListener {
case NO_COUNTER_EXAMPLE_EXISTS:
dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Counter-Example Exists";
- message = "No Counter-Example to the Invariant Theorems exists.";
+ message = "No counter-example to the invariant theorems exists (for current settings of deferred sets).\nIf your model contains deferred sets, there may exist counter-examples for other sizes of these sets.";
break;
case NO_COUNTER_EXAMPLE_FOUND:
dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Counter-Example Found";
- message = "No Counter-Example to the Invariant Theorems was found.";
+ message = "No counter-example to the invariant theorems was found (but one may exist).";
break;
case COUNTER_EXAMPLE:
dialogType = MessageDialog.WARNING;
dialogTitle = "COUNTER-EXAMPLE FOUND!";
- message = "The model contains a Counter-Example state to the Invariant Theorems, it will be shown in the state view.";
+ message = "A counter-example to the invariant theorems was found: it will be shown in the state view.\nThis counter-example state satisfies the invariants but may not be reachable from the initialisation.";
displayCounterExample(command, animator);
break;
case INTERRUPTED:
diff --git a/de.prob.ui/src/de/prob/ui/deadlock/DeadlockCheckFinishedListener.java b/de.prob.ui/src/de/prob/ui/deadlock/DeadlockCheckFinishedListener.java
index e49a3296..5cda9e47 100644
--- a/de.prob.ui/src/de/prob/ui/deadlock/DeadlockCheckFinishedListener.java
+++ b/de.prob.ui/src/de/prob/ui/deadlock/DeadlockCheckFinishedListener.java
@@ -49,7 +49,7 @@ public class DeadlockCheckFinishedListener extends ProBJobFinishedListener {
case NO_DEADLOCK:
dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Deadlock Found";
- message = "The model does not contain any deadlock.";
+ message = "The model does not contain any deadlock (for current settings of deferred sets).\nIf your model contains deferred sets, there may exist counter-examples for other sizes of these sets.";
break;
case ERROR:
dialogType = MessageDialog.ERROR;
@@ -59,7 +59,7 @@ public class DeadlockCheckFinishedListener extends ProBJobFinishedListener {
case DEADLOCK_FOUND:
dialogType = MessageDialog.WARNING;
dialogTitle = "DEADLOCK FOUND!";
- message = "The model contains a deadlocking state satisfying the invariant, it will be shown in the state view.";
+ message = "The model contains a deadlocking state satisfying the invariant, it will be shown in the state view.\nThe state may not be reachable from the initialisation.";
displayDeadlock(command, animator);
break;
case INTERRUPTED:
--
GitLab