From fdb1c7f8673898f62ed93952e97860a761b7a276 Mon Sep 17 00:00:00 2001 From: rensink Date: Tue, 23 Jul 2024 18:34:14 +0200 Subject: [PATCH] Exploration report no longer contains all result states, just a count --- .../java/nl/utwente/groove/explore/ExploreResult.java | 6 ++++++ .../java/nl/utwente/groove/explore/result/Acceptor.java | 8 +------- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/main/java/nl/utwente/groove/explore/ExploreResult.java b/src/main/java/nl/utwente/groove/explore/ExploreResult.java index ca9fecd6f..b86f12d4c 100644 --- a/src/main/java/nl/utwente/groove/explore/ExploreResult.java +++ b/src/main/java/nl/utwente/groove/explore/ExploreResult.java @@ -120,6 +120,12 @@ public GTSFragment toFragment(boolean internal) { return result; } + /** Returns the number of states and transitions found during exploration. */ + public String getStatistics() { + return "Exploration result: %s states, %s transitions" + .formatted(this.states.size(), this.transitions.size()); + } + @Override public String toString() { return "Result [states=" + this.states + ", " + "transitions=" + this.transitions diff --git a/src/main/java/nl/utwente/groove/explore/result/Acceptor.java b/src/main/java/nl/utwente/groove/explore/result/Acceptor.java index 9aca2504e..66e0981c3 100644 --- a/src/main/java/nl/utwente/groove/explore/result/Acceptor.java +++ b/src/main/java/nl/utwente/groove/explore/result/Acceptor.java @@ -114,12 +114,6 @@ public ExploreResult getResult() { /** Returns a message describing the accepted result. */ public String getMessage() { - String result; - if (this.result.isEmpty()) { - result = "No result states found"; - } else { - result = this.result.size() + " result states found: " + this.result; - } - return result; + return this.result.getStatistics(); } }