From 933194c155f946803204e846d768c79da4029240 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Thu, 4 Feb 2016 14:16:46 +0100
Subject: [PATCH] Added debuglevel to benchmark script

Former-commit-id: 79040662612db50bce0fe7bb2b4db7593cfe26d9
---
 benchmark_dft.py        | 14 ++++++++++----
 examples/dft/spare7.dft |  5 +++++
 2 files changed, 15 insertions(+), 4 deletions(-)
 create mode 100644 examples/dft/spare7.dft

diff --git a/benchmark_dft.py b/benchmark_dft.py
index 425d8ae80..b12d4f185 100644
--- a/benchmark_dft.py
+++ b/benchmark_dft.py
@@ -4,6 +4,7 @@ import subprocess
 import re
 import time
 import math
+import argparse
 
 STORM_PATH= "/Users/mvolk/develop/storm/build/src/storm-dft"
 EXAMPLE_DIR= "/Users/mvolk/develop/storm/examples/dft/"
@@ -28,6 +29,7 @@ benchmarks = [
     ("spare4", False, [4.8459, 1]),
     ("spare5", False, [2.66667, 1]), # We discard the result 2.16667 from DFTCalc
     ("spare6", False, [1.4, 1]),
+    ("spare7", False, [3.67333, 1]),
     ("tripple_and1", False, [4.16667, 1]),
     ("tripple_and2", False, [3.66667, 1]),
     ("tripple_and2_c", False, [3.6667, 1]),
@@ -81,6 +83,9 @@ def run_tool(args, quiet=False):
     return result
 
 if __name__ == "__main__":
+    parser = argparse.ArgumentParser(description='Benchmarking DFTs via Storm')
+    parser.add_argument('--debuglevel', type=int, default=0, help='the debug level (0=silent, 1=print benchmarks, 2=print output from storm')
+    args = parser.parse_args()
     count = 0
     correct = 0
     properties = ["ET=? [F \"failed\"]", "P=? [F \"failed\"]"]
@@ -90,19 +95,20 @@ if __name__ == "__main__":
             expected_result = result_original[index]
             # Run benchmark and check result
             count += 1;
-            print("Running '{}' with property '{}'".format(benchmark, prop))
-            result = run_storm_dft(benchmark, prop, parametric, True)
+            if args.debuglevel > 0:
+                print("Running '{}' with property '{}'".format(benchmark, prop))
+            result = run_storm_dft(benchmark, prop, parametric, args.debuglevel<2)
             if not parametric:
                 # Float
                 result = float(result)
                 if not math.isclose(result, float(expected_result), rel_tol=1e-05):
-                    print("!!! File '{}': result: {}, Expected: {}".format(benchmark, result, expected_result))
+                    print("Wrong result on example '{}' with property '{}': result: {}, Expected: {}".format(benchmark, prop, result, expected_result))
                 else:
                     correct += 1
             else:
                 # Parametric
                 if result != expected_result:
-                    print("!!! File {}: result: {}, Expected: {}".format(benchmark, result, expected_result))
+                    print("Wrong result on example '{}' with property '{}': result: {}, Expected: {}".format(benchmark, prop, result, expected_result))
                 else:
                     correct += 1
     end = time.time()
diff --git a/examples/dft/spare7.dft b/examples/dft/spare7.dft
new file mode 100644
index 000000000..a16429e6f
--- /dev/null
+++ b/examples/dft/spare7.dft
@@ -0,0 +1,5 @@
+toplevel "A";
+"A" wsp "K" "J" "I";
+"I" lambda=0.5 dorm=0.5;
+"J" lambda=1 dorm=0.5;
+"K" lambda=0.5 dorm=0.5;