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 282871b34d7911d6e3acb80711ada8e6c7ace6ad..6a3b4744a75fa558a81e4f407442c2aa074d469c 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 0955c190d3d5e03cdaf7d64e51f20046ea3ef198..bee6c416eef80dc7cba829f2ccc85d9de0e9fce2 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