From 14535a6eab6100e7e9141dfea9d9ce6cf8f18515 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 12 Nov 2020 13:09:36 +0100
Subject: [PATCH] rename nodes to states in model checking results
---
.../de/prob/ui/eventb/ModelCheckingFinishedListener.java | 6 +++---
de.prob.ui/src/de/prob/ui/ltl/LtlStrings.properties | 4 ++--
2 files changed, 5 insertions(+), 5 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 282871b3..6a3b4744 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java
@@ -193,12 +193,12 @@ public class ModelCheckingFinishedListener extends JobChangeAdapter {
private String createOkButNotFinishedResult() {
return "No errors found, but not all possible "
- + "nodes have been visited (Due to animation parameter restrictions).";
+ + "states have been visited (Due to animation parameter restrictions).";
}
private String createOkResult() {
return "No errors found\n"
- + "Model Checking finished, all nodes visited.\n";
+ + "Model Checking finished, all states visited.\n";
}
private void replayErrorTrace() throws ProBException {
@@ -222,7 +222,7 @@ public class ModelCheckingFinishedListener extends JobChangeAdapter {
private void appendCoverageStatistics(final ComputeCoverageResult coverage,
final String PID, final MultiStatus info) {
info.add(new Status(IStatus.INFO, PID, 1, "Coverage statistics:", null));
- info.add(new Status(IStatus.INFO, PID, 1, "Total Number of Nodes:"
+ info.add(new Status(IStatus.INFO, PID, 1, "Total Number of States:"
+ coverage.getTotalNumberOfNodes(), null));
info.add(new Status(IStatus.INFO, PID, 1,
"Total Number of Transitions:"
diff --git a/de.prob.ui/src/de/prob/ui/ltl/LtlStrings.properties b/de.prob.ui/src/de/prob/ui/ltl/LtlStrings.properties
index 0955c190..bee6c416 100644
--- a/de.prob.ui/src/de/prob/ui/ltl/LtlStrings.properties
+++ b/de.prob.ui/src/de/prob/ui/ltl/LtlStrings.properties
@@ -12,9 +12,9 @@ ltlHelpText=About LTL Checking\n\nLTL Syntax:\n\
-use WEF or SEF to search for paths that are weakly or strongly fair w.r.t. all transitions.
ltlResultIncompleteTitle=Modelchecking not completed
-ltlResultIncompleteMessage=No counterexample has been found, but not all possible nodes have been visited (Due to animation parameter restrictions).
+ltlResultIncompleteMessage=No counterexample has been found, but not all possible states have been visited (Due to animation parameter restrictions).
ltlResultOkTitle=Modelchecking successfully finished
-ltlResultOkMessage=No counterexample has been found, all nodes have been visited.
+ltlResultOkMessage=No counterexample has been found, all states have been visited.
ltlResultCounterexampleTitle=Counterexample found
ltlResultCounterexampleMessage=A counterexample has been found. It will be shown in the LTL view.
ltlResultNoStartTitle=No initialisation found
--
GitLab