diff --git a/prism/bench.py b/prism/bench.py
new file mode 100755
index 0000000000000000000000000000000000000000..57b123adbe8a7c3c90ed923de12c23074ddb84c9
--- /dev/null
+++ b/prism/bench.py
@@ -0,0 +1,54 @@
+#!/usr/bin/python
+
+import subprocess
+import os
+import sys
+import re
+
+
+def extract_time(perf_output):
+ "returns the measured time from the perf output in seconds"
+ m = re.search(r'(\d+.\d+)\W+seconds time elapsed', str(perf_output))
+ return m[1]
+
+
+def run_ma(ma, input_file):
+ process = subprocess.run(
+ ['perf', 'stat', ma],
+ stdin=input_file,
+ stdout=subprocess.DEVNULL,
+ stderr=subprocess.PIPE,
+ env={'LC_ALL': 'C'})
+
+ try:
+ process.check_returncode()
+ except subprocess.CalledProcessError as e:
+ err = os.fdopen(sys.stderr.fileno(), 'wb')
+ err.write(process.stderr)
+ err.flush()
+ raise e
+
+ return extract_time(process.stderr)
+
+
+def run_bench(ma, name, filename):
+ with open(filename) as model_file:
+ time = run_ma(ma, model_file)
+
+ print("%s" % time)
+
+
+def main(args):
+ if len(args) != 4:
+ print("Usage: %s EXECUTABLE MODEL_NAME MODEL_FILE" % args[0])
+ sys.exit(1)
+
+ ma_binary = args[1]
+ model_name = args[2]
+ model_file = args[3]
+
+ run_bench(ma_binary, model_name, model_file)
+
+
+if __name__ == "__main__":
+ main(sys.argv)
diff --git a/prism/benchmark.org b/prism/benchmark.org
index 2eec320cccfc890a1d70042222d791ec04b6f352..b614979ab7eafda972f6ceeb95543b4d421e88bc 100644
--- a/prism/benchmark.org
+++ b/prism/benchmark.org
@@ -47,7 +47,13 @@
| brp | brp/brp.pm | dtmc | N, MAX |
| dice | dice/dice.pm | dtmc | |
| two_dice_knuth | dice/two_dice_knuth.pm | dtmc | |
- | two_dice | dice/two_dice.pm | | |
+ | two_dice | dice/two_dice.nm | mdp | |
+
+ #+BEGIN_SRC python :session :var models_table=models :results none
+ models = []
+ for t in models_table:
+ models.append({'name': t[0], 'path': t[1], 'type': t[2], 'constants': t[3]})
+ #+END_SRC
** Tooling
@@ -55,6 +61,7 @@
#+BEGIN_SRC python :session :results none
import os
+ import subprocess
#+END_SRC
The following environment definitions probably need to be adapted for
@@ -63,67 +70,125 @@
#+BEGIN_SRC python :session :results none
config = {'prism_cmd': '../../prism-4.4/prism/bin/prism',
'prism_examples': '../../prism-4.4/prism-examples',
- 'ma_cmd': '../../masterarbeit/bin/ma',
- 'prism_converter_cmd': '../../masterarbeit/bin/prism-converter',
+ 'ma_cmd': '../../ma/bin/ma',
+ 'prism_converter_cmd': '../../ma/bin/prism-converter',
}
#+END_SRC
We need to define a few python functions and variables to use later:
- #+BEGIN_SRC python :session :var models_table=models :results none
- models = []
- for t in models_table:
- models.append({'name': t[0], 'path': t[1], 'type': t[2], 'constants': t[3]})
-
+ #+BEGIN_SRC python :session :results none
def const_base_path(path, const_assignments):
- return "%s_%s" % (path, const_assignments) \
- if const_assignments else path
+ return "bench/%s_%s" % (path, const_assignments) \
+ if const_assignments else ("bench/%s" % path)
def export_model_impl(path, const_assignments):
path_with_consts = const_base_path(path, const_assignments)
tra_file = "%s.tra" % path_with_consts
sta_file = "%s.sta" % path_with_consts
- print("making directory %s" % (os.path.dirname(path)))
- os.makedirs(os.path.dirname(path), exist_ok=True)
+ if os.path.isfile(tra_file):
+ return
+ os.makedirs(os.path.dirname(tra_file), exist_ok=True)
model_path = "%s/%s" % (config['prism_examples'], path)
- subprocess.call([config['prism_cmd'],
- '-exporttrans', tra_file,
- '-exportstates', sta_file,
- '-const', const_assignments,
- model_path])
+ subprocess.run([config['prism_cmd'],
+ '-exporttrans', tra_file,
+ '-exportstates', sta_file,
+ '-const', const_assignments,
+ model_path])
- def export_model(name, const_assignments):
+ def find_model(name):
for m in models:
if m['name'] == name:
- return export_model_impl(m['path'], const_assignments)
+ return m
raise Exception("Model %s not found" % name)
+
+
+ def export_model(name, const_assignments):
+ m = find_model(name)
+ return export_model_impl(m['path'], const_assignments)
+
+ def convert_model(name, const_assignments):
+ model = find_model(name)
+ path_with_consts = const_base_path(model['path'], const_assignments)
+ tra_file = "%s.tra" % path_with_consts
+ sta_file = "%s.sta" % path_with_consts
+ coalgebra_file = path_with_consts + ".coalgebra"
+ if os.path.isfile(coalgebra_file):
+ return
+ subprocess.run([config['prism_converter_cmd'], '--model-type',
+ model['type'], '--states-file', sta_file, tra_file,
+ coalgebra_file])
+
+ def partition_model(name, const_assignments):
+ model = find_model(name)
+ path_with_consts = const_base_path(model['path'], const_assignments)
+ coalgebra_file = path_with_consts + ".coalgebra"
+ out = subprocess.run(['./bench.py', config['ma_cmd'], model['name'],
+ coalgebra_file], capture_output=True)
+ return out.stdout.decode('utf-8').strip()
+
+ def run_benchmark(model, const_assignments):
+ export_model(model, const_assignments)
+ convert_model(model, const_assignments)
+ return partition_model(model, const_assignments)
#+END_SRC
-* Benchmarks
+ #+NAME: bench
+ #+BEGIN_SRC python :session :eval no-export :var table="" :colnames no :hlines yes
+ [['Model', 'Constants', 'Time(s)'], None] + list(map(lambda t: [t[0], t[1], run_benchmark(t[0], t[1])], table[2:]))
+ #+END_SRC
+* Benchmarks
** brp
- Constants:
-
- | N | MAX |
- |----+-----|
- | 16 | 2 |
- | 32 | 2 |
- | 64 | 2 |
- | 16 | 3 |
- | 32 | 3 |
- | 64 | 3 |
- | 16 | 4 |
- | 32 | 4 |
- | 64 | 4 |
- | 16 | 5 |
- | 32 | 5 |
- | 64 | 5 |
+ #+NAME: brp_benchmarks
+ | Model | Constants |
+ |-------+------------|
+ | brp | N=16,MAX=2 |
+ | brp | N=16,MAX=3 |
+ | brp | N=16,MAX=4 |
+ | brp | N=16,MAX=5 |
+ | brp | N=32,MAX=2 |
+ | brp | N=32,MAX=3 |
+ | brp | N=32,MAX=4 |
+ | brp | N=32,MAX=5 |
+ | brp | N=64,MAX=2 |
+ | brp | N=64,MAX=3 |
+ | brp | N=64,MAX=4 |
+ | brp | N=64,MAX=5 |
+
+ #+CALL: bench(brp_benchmarks)
+
+ #+RESULTS:
+ | Model | Constants | Time(s) |
+ |-------+------------+-------------|
+ | brp | N=16,MAX=2 | 0.006715844 |
+ | brp | N=16,MAX=3 | 0.008666313 |
+ | brp | N=16,MAX=4 | 0.010352513 |
+ | brp | N=16,MAX=5 | 0.011620392 |
+ | brp | N=32,MAX=2 | 0.011925145 |
+ | brp | N=32,MAX=3 | 0.016233265 |
+ | brp | N=32,MAX=4 | 0.018848666 |
+ | brp | N=32,MAX=5 | 0.022940769 |
+ | brp | N=64,MAX=2 | 0.023586786 |
+ | brp | N=64,MAX=3 | 0.032067215 |
+ | brp | N=64,MAX=4 | 0.038755864 |
+ | brp | N=64,MAX=5 | 0.049498514 |
** dice
- #+BEGIN_SRC python :session
- export_model('dice', '')
- #+END_SRC
+ #+NAME: dice_benchmarks
+ | Model | Constants |
+ |----------------+-----------|
+ | dice | |
+ | two_dice_knuth | |
+ | two_dice | |
+
+ #+CALL: bench(dice_benchmarks)
#+RESULTS:
+ | Model | Constants | Time(s) |
+ |----------------+-----------+-------------|
+ | dice | | 0.001887141 |
+ | two_dice_knuth | | 0.002188563 |
+ | two_dice | | 0.004425725 |