Commit 14535a6e authored by Michael Leuschel's avatar Michael Leuschel
Browse files

rename nodes to states in model checking results

parent b8e610c0
......@@ -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:"
......
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment