Skip to content
Snippets Groups Projects
Commit d308a7a0 authored by Michael Leuschel's avatar Michael Leuschel
Browse files

extend messages of some cbc checks

The messages provide more details
explaining the result of the check.
parent dfcd10bf
No related branches found
No related tags found
No related merge requests found
...@@ -50,17 +50,17 @@ public class AssertionCheckFinishedListener extends ProBJobFinishedListener { ...@@ -50,17 +50,17 @@ public class AssertionCheckFinishedListener extends ProBJobFinishedListener {
case NO_COUNTER_EXAMPLE_EXISTS: case NO_COUNTER_EXAMPLE_EXISTS:
dialogType = MessageDialog.INFORMATION; dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Counter-Example Exists"; 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; break;
case NO_COUNTER_EXAMPLE_FOUND: case NO_COUNTER_EXAMPLE_FOUND:
dialogType = MessageDialog.INFORMATION; dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Counter-Example Found"; 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; break;
case COUNTER_EXAMPLE: case COUNTER_EXAMPLE:
dialogType = MessageDialog.WARNING; dialogType = MessageDialog.WARNING;
dialogTitle = "COUNTER-EXAMPLE FOUND!"; 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); displayCounterExample(command, animator);
break; break;
case INTERRUPTED: case INTERRUPTED:
......
...@@ -50,17 +50,17 @@ public class AssertionDynCheckFinishedListener extends ProBJobFinishedListener { ...@@ -50,17 +50,17 @@ public class AssertionDynCheckFinishedListener extends ProBJobFinishedListener {
case NO_COUNTER_EXAMPLE_EXISTS: case NO_COUNTER_EXAMPLE_EXISTS:
dialogType = MessageDialog.INFORMATION; dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Counter-Example Exists"; 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; break;
case NO_COUNTER_EXAMPLE_FOUND: case NO_COUNTER_EXAMPLE_FOUND:
dialogType = MessageDialog.INFORMATION; dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Counter-Example Found"; 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; break;
case COUNTER_EXAMPLE: case COUNTER_EXAMPLE:
dialogType = MessageDialog.WARNING; dialogType = MessageDialog.WARNING;
dialogTitle = "COUNTER-EXAMPLE FOUND!"; 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); displayCounterExample(command, animator);
break; break;
case INTERRUPTED: case INTERRUPTED:
......
...@@ -49,7 +49,7 @@ public class DeadlockCheckFinishedListener extends ProBJobFinishedListener { ...@@ -49,7 +49,7 @@ public class DeadlockCheckFinishedListener extends ProBJobFinishedListener {
case NO_DEADLOCK: case NO_DEADLOCK:
dialogType = MessageDialog.INFORMATION; dialogType = MessageDialog.INFORMATION;
dialogTitle = "No Deadlock Found"; 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; break;
case ERROR: case ERROR:
dialogType = MessageDialog.ERROR; dialogType = MessageDialog.ERROR;
...@@ -59,7 +59,7 @@ public class DeadlockCheckFinishedListener extends ProBJobFinishedListener { ...@@ -59,7 +59,7 @@ public class DeadlockCheckFinishedListener extends ProBJobFinishedListener {
case DEADLOCK_FOUND: case DEADLOCK_FOUND:
dialogType = MessageDialog.WARNING; dialogType = MessageDialog.WARNING;
dialogTitle = "DEADLOCK FOUND!"; 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); displayDeadlock(command, animator);
break; break;
case INTERRUPTED: case INTERRUPTED:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment