Add MddAnalysisStatistics

RipplB · Jul 12, 2024 · 0a0b2dd · 0a0b2dd
1 parent 20af0a6
commit 0a0b2dd
Show file tree

Hide file tree

Showing 4 changed files with 77 additions and 11 deletions.
diff --git a/...analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddAnalysisStatistics.java b/...analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddAnalysisStatistics.java
@@ -0,0 +1,62 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.algorithm.mdd;
+
+import hu.bme.mit.theta.analysis.algorithm.Statistics;
+
+public class MddAnalysisStatistics extends Statistics {
+
+    private final Long violatingSize;
+    private final Long stateSpaceSize;
+    private final Long hitCount;
+    private final Long queryCount;
+    private final Long cacheSize;
+
+
+    public MddAnalysisStatistics(Long violatingSize, Long stateSpaceSize, Long hitCount, Long queryCount, Long cacheSize) {
+        this.violatingSize = violatingSize;
+        this.stateSpaceSize = stateSpaceSize;
+        this.hitCount = hitCount;
+        this.queryCount = queryCount;
+        this.cacheSize = cacheSize;
+
+        addStat("ViolatingSize", this::getViolatingSize);
+        addStat("StateSpaceSize", this::getStateSpaceSize);
+        addStat("HitCount", this::getHitCount);
+        addStat("QueryCount", this::getQueryCount);
+        addStat("CacheSize", this::getCacheSize);
+    }
+
+    public Long getViolatingSize() {
+        return violatingSize;
+    }
+
+    public Long getStateSpaceSize() {
+        return stateSpaceSize;
+    }
+
+    public Long getHitCount() {
+        return hitCount;
+    }
+
+    public Long getQueryCount() {
+        return queryCount;
+    }
+
+    public Long getCacheSize() {
+        return cacheSize;
+    }
+}
diff --git a/...cts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java b/...cts/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mdd/MddChecker.java
@@ -170,16 +170,13 @@ public SafetyResult<MddWitness, MddCex> check(Void input) {
         final Long stateSpaceSize = MddInterpreter.calculateNonzeroCount(stateSpace);
         logger.write(Level.DETAIL, "State space size: " + stateSpaceSize);
 
-
-        logger.write(Level.DETAIL, "Hit count: " + cache.getHitCount());
-        logger.write(Level.DETAIL, "Query count: " + cache.getQueryCount());
-        logger.write(Level.DETAIL, "Cache size: " + cache.getCacheSize());
+        final MddAnalysisStatistics statistics = new MddAnalysisStatistics(violatingSize, stateSpaceSize, cache.getHitCount(), cache.getQueryCount(), cache.getCacheSize());
 
         final SafetyResult<MddWitness, MddCex> result;
         if (violatingSize != 0) {
-            result = SafetyResult.unsafe(MddCex.of(propViolating), MddWitness.of(stateSpace));
+            result = SafetyResult.unsafe(MddCex.of(propViolating), MddWitness.of(stateSpace), statistics);
         } else {
-            result = SafetyResult.safe(MddWitness.of(stateSpace));
+            result = SafetyResult.safe(MddWitness.of(stateSpace), statistics);
         }
         logger.write(Level.RESULT, "%s%n", result);
         return result;

diff --git a/...s/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java b/...s/xsts/xsts-analysis/src/main/java/hu/bme/mit/theta/xsts/analysis/mdd/XstsMddChecker.java
@@ -22,6 +22,7 @@
 import hu.bme.mit.delta.mdd.MddVariableDescriptor;
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
 import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
+import hu.bme.mit.theta.analysis.algorithm.mdd.MddAnalysisStatistics;
 import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex;
 import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker.IterationStrategy;
 import hu.bme.mit.theta.analysis.algorithm.mdd.MddWitness;
@@ -189,15 +190,13 @@ public SafetyResult<MddWitness, MddCex> check(Void input) {
         final Long stateSpaceSize = MddInterpreter.calculateNonzeroCount(stateSpace);
         logger.write(Level.DETAIL, "State space size: " + stateSpaceSize);
 
-        logger.write(Level.DETAIL, "Hit count: " + cache.getHitCount());
-        logger.write(Level.DETAIL, "Query count: " + cache.getQueryCount());
-        logger.write(Level.DETAIL, "Cache size: " + cache.getCacheSize());
+        final MddAnalysisStatistics statistics = new MddAnalysisStatistics(violatingSize, stateSpaceSize, cache.getHitCount(), cache.getQueryCount(), cache.getCacheSize());
 
         final SafetyResult<MddWitness, MddCex> result;
         if (violatingSize != 0) {
-            result = SafetyResult.unsafe(MddCex.of(propViolating), MddWitness.of(stateSpace));
+            result = SafetyResult.unsafe(MddCex.of(propViolating), MddWitness.of(stateSpace), statistics);
         } else {
-            result = SafetyResult.safe(MddWitness.of(stateSpace));
+            result = SafetyResult.safe(MddWitness.of(stateSpace), statistics);
         }
         logger.write(Level.RESULT, "%s%n", result);
         return result;

diff --git a/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java b/subprojects/xsts/xsts-cli/src/main/java/hu/bme/mit/theta/xsts/cli/XstsCli.java
@@ -33,6 +33,7 @@
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
 import hu.bme.mit.theta.analysis.algorithm.cegar.CegarStatistics;
+import hu.bme.mit.theta.analysis.algorithm.mdd.MddAnalysisStatistics;
 import hu.bme.mit.theta.analysis.algorithm.mdd.MddCex;
 import hu.bme.mit.theta.analysis.algorithm.mdd.MddChecker;
 import hu.bme.mit.theta.analysis.algorithm.mdd.MddWitness;
@@ -603,10 +604,17 @@ private void printCegarResult(final SafetyResult<? extends ARG<?, ?>, ? extends
     }
 
     private void printSymbolicResult(final SafetyResult<MddWitness, MddCex> status, final XSTS sts, final long totalTimeMs) {
+        final MddAnalysisStatistics stats = (MddAnalysisStatistics)
+                status.getStats().orElse(new MddAnalysisStatistics(0L, 0L, 0L, 0L, 0L));
         if (benchmarkMode) {
             writer.cell(status.isSafe());
             writer.cell(totalTimeMs);
             writer.cell(status.getWitness().size());
+            writer.cell(stats.getViolatingSize());
+            writer.cell(stats.getStateSpaceSize());
+            writer.cell(stats.getHitCount());
+            writer.cell(stats.getQueryCount());
+            writer.cell(stats.getCacheSize());
             if (status.isUnsafe()) {
                 writer.cell(status.asUnsafe().getCex().length() + "");
             } else {