From 2c969eff3b1d60a19c95f93ab71d6c217b98fae7 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Wed, 3 Feb 2016 18:04:45 +0100
Subject: [PATCH] Updated benchmark script for reachability probabilities

Former-commit-id: 717c099ae1cdc4fcd81afcd4a3201fc7a4a4d062
---
 benchmark_dft.py | 106 ++++++++++++++++++++++++-----------------------
 1 file changed, 54 insertions(+), 52 deletions(-)

diff --git a/benchmark_dft.py b/benchmark_dft.py
index 54fb06593..a6109ff45 100644
--- a/benchmark_dft.py
+++ b/benchmark_dft.py
@@ -10,43 +10,42 @@ EXAMPLE_DIR= "/Users/mvolk/develop/storm/examples/dft/"
 
 
 benchmarks = [ 
-    ("and", False, 3),
-    ("and_param", True, "(4*x^2+2*x+1)/((x) * (2*x+1))"),
-    ("cm2", False, 0.256272),
-    #("cm4", False, 0),
-    ("cps", False, "inf"),
-    #("fdep", False, 0),
-    ("mdcs", False, 2.85414),
-    ("mdcs2", False, 2.85414),
-    ("mp", False, 1.66667),
-    ("or", False, 1),
-    ("pand", False, "inf"),
-    ("pand_param", True, "-1"),
-    ("spare", False, 3.53846),
-    ("spare2", False, 1.86957),
-    ("spare3", False, 1.27273),
-    ("spare4", False, 4.8459),
-    ("spare5", False, 2.16667),
-    ("spare6", False, 1.4),
-    ("tripple_and1", False, 4.16667),
-    ("tripple_and2", False, 3.66667),
-    ("tripple_and2_c", False, 3.6667),
-    ("tripple_and_c", False, 4.16667),
-    ("tripple_or", False, 0.5),
-    ("tripple_or2", False, 0.666667),
-    ("tripple_or2_c", False, 0.66667),
-    ("tripple_or_c", False, 0.5),
-    ("tripple_pand", False, "inf"),
-    ("tripple_pand2", False, "inf"),
-    ("tripple_pand2_c", False, "inf"),
-    ("tripple_pand_c", False, "inf"),
-    ("voting", False, 1.66667),
-    ("voting2", False, 0.588235)
+    ("and", False, [3, 1]),
+    ("and_param", True, ["(4*x^2+2*x+1)/((x) * (2*x+1))", "1"]),
+    ("cm2", False, [0.256272, 1]),
+    #("cm4", False, [0, 1]),
+    ("cps", False, ["inf", 0.333333]),
+    #("fdep", False, [0, 1]),
+    ("mdcs", False, [2.85414, 1]),
+    ("mdcs2", False, [2.85414, 1]),
+    ("mp", False, [1.66667, 1]),
+    ("or", False, [1, 1]),
+    ("pand", False, ["inf", 0.666667]),
+    ("pand_param", True, ["-1", "(x)/(y+x)"]),
+    ("spare", False, [3.53846, 1]),
+    ("spare2", False, [1.86957, 1]),
+    ("spare3", False, [1.27273, 1]),
+    ("spare4", False, [4.8459, 1]),
+    ("spare5", False, [2.16667, 1]),
+    ("spare6", False, [1.4, 1]),
+    ("tripple_and1", False, [4.16667, 1]),
+    ("tripple_and2", False, [3.66667, 1]),
+    ("tripple_and2_c", False, [3.6667, 1]),
+    ("tripple_and_c", False, [4.16667, 1]),
+    ("tripple_or", False, [0.5, 1]),
+    ("tripple_or2", False, [0.666667, 1]),
+    ("tripple_or2_c", False, [0.66667, 1]),
+    ("tripple_or_c", False, [0.5, 1]),
+    ("tripple_pand", False, ["inf", 0.0416667]),
+    ("tripple_pand2", False, ["inf", 0.166667]),
+    ("tripple_pand2_c", False, ["inf", 0.166667]),
+    ("tripple_pand_c", False, ["inf", 0.0416667]),
+    ("voting", False, [1.66667, 1]),
+    ("voting2", False, [0.588235, 1])
 ]
 
-def run_storm_dft(filename, parametric, quiet):
+def run_storm_dft(filename, prop, parametric, quiet):
     # Run storm-dft on filename and return result
-    prop = "ET=? [F \"failed\"]"
     dft_file = os.path.join(EXAMPLE_DIR, filename + ".dft")
     args = [STORM_PATH,
             dft_file,
@@ -84,24 +83,27 @@ def run_tool(args, quiet=False):
 if __name__ == "__main__":
     count = 0
     correct = 0
+    properties = ["ET=? [F \"failed\"]", "P=? [F \"failed\"]"]
     start = time.time()
-    for (benchmark, parametric, result_original) in benchmarks:
-        # Run benchmark and check result
-        count += 1;
-        print("Running '{}'".format(benchmark))
-        result = run_storm_dft(benchmark, parametric, True)
-        if not parametric:
-            # Float
-            result = float(result)
-            if not math.isclose(result, float(result_original), rel_tol=1e-05):
-                print("!!! File '{}': result: {}, Expected: {}".format(benchmark, result, result_original))
+    for index, prop in enumerate(properties):
+        for (benchmark, parametric, result_original) in benchmarks:
+            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 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))
+                else:
+                    correct += 1
             else:
-                correct += 1
-        else:
-            # Parametric
-            if result != result_original:
-                print("!!! File {}: result: {}, Expected: {}".format(benchmark, result, result_original))
-            else:
-                correct += 1
+                # Parametric
+                if result != expected_result:
+                    print("!!! File {}: result: {}, Expected: {}".format(benchmark, result, expected_result))
+                else:
+                    correct += 1
     end = time.time()
-    print("Correct results for {} of {} DFTs in {}s".format(correct, count, end-start))
+    print("Correct results for {} of {} DFT checks in {}s".format(correct, count, end-start))