diff --git a/dfa/bench.py b/dfa/bench.py
index 1e4e1d55ef9a135814d3ef8aa864aa5364babcf2..79bcc178d906d02a8ecf69984f659d31b55ce1ad 100755
--- a/dfa/bench.py
+++ b/dfa/bench.py
@@ -56,13 +56,16 @@ def generate(args):
subprocess.run(cmd)
-def run_one(copar, valmari, n, m, i, final, noopt):
+def run_one(copar, valmari, n, m, i, final, noopt, nofunctrans):
# Run copar on it
copar_args = [copar, 'refine', '--stats-json', coalg_file(n, m, i, final)]
if noopt:
copar_args.append("--disable-optimizations")
+ if nofunctrans:
+ copar_args.append("--no-functor-transforms")
+
out = subprocess.run(copar_args,
stdout=subprocess.DEVNULL,
stderr=subprocess.PIPE)
@@ -152,9 +155,10 @@ def run(args):
m = args.m
final = args.final
noopt = args.noopt
+ nofunctrans = args.nofunctrans
sample_count = samples if args.samples is None else args.samples
- results = [run_one(copar, valmari, n, m, i, final, noopt)
+ results = [run_one(copar, valmari, n, m, i, final, noopt, nofunctrans)
for i in range(0, sample_count)]
# Do some sanity checks on the samles
@@ -220,6 +224,8 @@ if __name__ == "__main__":
metavar="PERCENT")
run_parser.add_argument('--noopt', action='store_true',
help="run copar without --disable-optimizations")
+ run_parser.add_argument('--nofunctrans', action='store_true',
+ help="run copar without --no-functor-transforms")
run_parser.add_argument('--samples', type=int,
help="number of samples to run")
run_parser.set_defaults(func=run)
diff --git a/dfa/benchmark.org b/dfa/benchmark.org
index 74313440157d67be9a90a307e7fc9099fcc3f93f..54da30c5faf44f2cbfc72337623b4bbe625afc75 100644
--- a/dfa/benchmark.org
+++ b/dfa/benchmark.org
@@ -325,7 +325,7 @@ python bench.py run ../../copar/bin/copar ../../valmari_cpp/mdpmin 1000 1000 --i
| 1000 | 1000 | 0 | 1000 | 1000000 | 2 | 1000 | 1000 | 997982 | 3.848351055 | 2.589219225 | 1.2517901 | 0.685918061 | 0.446261266 | 1.041243359 | 1000 |
| 1000 | 1000 | 0 | 1000 | 1000000 | 2 | 1000 | 1000 | 997982 | 3.846534761 | 2.589810158 | 1.249553884 | 0.689444876 | 0.444917202 | 1.037644478 | 1000 |
-**** Without optimizations
+**** Without 1-elem optimization
:PROPERTIES:
:ID: d2559cc7-c179-48cf-aaab-c7f17a29ea1a
:END:
@@ -343,6 +343,25 @@ python bench.py run ../../copar/bin/copar ../../valmari_cpp/mdpmin 1000 1000 --i
| 1000 | 1000 | 0 | 1000 | 1000000 | 2 | 1000 | 1000 | 0 | 47.271392131 | 2.610240776 | 44.653358169 | 0.666528599 | 43.866734415 | 1.043897929 | 1000 |
| 1000 | 1000 | 0 | 1000 | 1000000 | 2 | 1000 | 1000 | 0 | 47.166293115 | 2.590651542 | 44.568110936 | 0.688910081 | 43.76112947 | 1.032940889 | 1000 |
+**** Without functor rewrite
+:PROPERTIES:
+:ID: d17f77cb-9a07-4c9f-8366-533e07075e6b
+:END:
+
+#+begin_src sh :hlines yes :colnames '("N" "M" "i" "States" "Edges" "I" "Q" "Qs1" "Opts" "t (s)" "tp (s)" "ta (s)" "ti (s)" "tr (s)" "tv (s)" "Qv")
+python bench.py run ../../copar/bin/copar ../../valmari_cpp/mdpmin 1000 1000 --indiv --samples 1 --nofunctrans
+python bench.py run ../../copar/bin/copar ../../valmari_cpp/mdpmin 1000 1000 --indiv --samples 1 --nofunctrans
+python bench.py run ../../copar/bin/copar ../../valmari_cpp/mdpmin 1000 1000 --indiv --samples 1 --nofunctrans
+#+end_src
+
+#+RESULTS:
+| N | M | i | States | Edges | I | Q | Qs1 | Opts | t (s) | tp (s) | ta (s) | ti (s) | tr (s) | tv (s) | Qv |
+|------+------+---+--------+---------+---+------+------+---------+-------------+-------------+-------------+-------------+-------------+-------------+------|
+| 1000 | 1000 | 0 | 2000 | 1001000 | 3 | 2000 | 1000 | 1497791 | 3.69951183 | 2.995813312 | 0.696292008 | 0.281623635 | 0.285086162 | 1.011353231 | 1000 |
+| 1000 | 1000 | 0 | 2000 | 1001000 | 3 | 2000 | 1000 | 1497791 | 3.694332219 | 2.994494171 | 0.692652535 | 0.280869596 | 0.280522528 | 1.040548865 | 1000 |
+| 1000 | 1000 | 0 | 2000 | 1001000 | 3 | 2000 | 1000 | 1497791 | 3.674371501 | 2.987738591 | 0.679263792 | 0.280875871 | 0.269943904 | 1.038760097 | 1000 |
+
+
** For m = 10000
#+BEGIN_SRC sh :hlines yes :colnames '("N" "M" "States" "Edges" "I" "Q" "Qs1" "t (s)" "tp (s)" "ta (s)" "ti (s)" "tr (s)" "tv (s)" "Qv")
diff --git a/optimizations/optimizations.org b/optimizations/optimizations.org
index 89a4e201507e989bfcaed6ca61f0d7af4a148c4b..bd487d1e24259323fbf250467fe0af273bff69ae 100644
--- a/optimizations/optimizations.org
+++ b/optimizations/optimizations.org
@@ -34,3 +34,26 @@
| fms | 35.941488 | 1.8943837 |
| dfa | 47.20688 | 0.32612647 |
#+TBLFM: @2$2=remote(one-elem-data, @3$5)::@2$3=10*remote(one-elem-data, @3$6)::@3$2=remote(one-elem-data, @5$5)::@3$3=10*remote(one-elem-data, @5$6)::@4$2=remote(one-elem-data, @7$5)::@4$3=10*remote(one-elem-data, @7$6)
+
+* Functor expression rewriting
+** The Data
+
+#+NAME: func-rewrite-data
+| Benchmark | Time1 | Time2 | Time3 | Mean | Error |
+|------------+-----------+-----------+-----------+-----------+--------------|
+| wlan noopt | 62.322413 | 62.416543 | 62.852129 | 62.530362 | 0.16316227 |
+|------------+-----------+-----------+-----------+-----------+--------------|
+| fms noopt | 21.331782 | 21.307057 | 21.295322 | 21.311387 | 0.010745458 |
+|------------+-----------+-----------+-----------+-----------+--------------|
+| dfa noopt | 3.6995118 | 3.6943322 | 3.6743715 | 3.6894052 | 7.6641028e-3 |
+#+TBLFM: $5=vmean($2..$4)::$6=vsdev($2..$4)/sqrt(3)::@2$2..@2$4=remote(74566779-0749-4bbd-9556-80f857144793, @$#$11)::@3$2..@3$4=remote(7e19eb5e-4009-4bc1-89a3-4e4e5c7f643e, @$#$11)::@4$2..@4$4=remote(d17f77cb-9a07-4c9f-8366-533e07075e6b, @$#$10)
+
+** Making the data easier for pgfplot
+** Noopt
+
+| Benchmark | Time | CI |
+|-----------+-----------+-------------|
+| wlan | 62.530362 | 1.6316227 |
+| fms | 21.311387 | 0.10745458 |
+| dfa | 3.6894052 | 0.076641028 |
+#+TBLFM: $2=remote(func-rewrite-data, @@#$5)::$3=10*remote(func-rewrite-data, @@#$6)
diff --git a/prism/benchmark.org b/prism/benchmark.org
index d7caf7c20d746b62000d219213d7954e590a11c4..a7f0bceb3da662706fa38f0cebb9bf9e207fe39c 100644
--- a/prism/benchmark.org
+++ b/prism/benchmark.org
@@ -186,7 +186,7 @@
model['type'], '--states-file', sta_file,
tra_file, coalgebra_file])
- def partition_model(name, const_assignments, disableopts):
+ def partition_model(name, const_assignments, disableopts, nofunctrans):
model = find_model(name)
path, const_assignments = replace_consts_in_path(model['path'], const_assignments)
path_with_consts = const_base_path(path, const_assignments)
@@ -194,14 +194,16 @@
cmd = [config['copar_cmd'], 'refine', '--stats-json', coalgebra_file]
if disableopts:
cmd.append('--disable-optimizations')
+ if nofunctrans:
+ cmd.append('--no-functor-transforms')
out = subprocess.run(cmd, stdout=subprocess.DEVNULL, stderr=subprocess.PIPE)
print(out.stderr.decode('utf-8'))
return json.loads(out.stderr.decode('utf-8'))
- def run_all(model, const_assignments, initial_partition, disableopts):
+ def run_all(model, const_assignments, initial_partition, disableopts, nofunctrans):
export_model(model, const_assignments)
convert_model(model, const_assignments, initial_partition)
- return partition_model(model, const_assignments, disableopts)
+ return partition_model(model, const_assignments, disableopts, nofunctrans)
#+END_SRC
** Valmari's Implementation
@@ -264,38 +266,44 @@
** Running Benchmarks
- #+BEGIN_SRC python :session :eval never-export :results output silent :exports none
- def run_benchmark(model, const_assignments, initial_partition, disableopts):
- stats = run_all(model, const_assignments, initial_partition, disableopts)
- valmari = run_all_valmari(model, const_assignments, initial_partition)
- return [model, const_assignments, initial_partition,
- stats['states'],
- stats['edges'],
- stats['explicit-states'],
- stats['initial-partition-size'],
- stats['final-partition-size'],
- stats['explicit-final-partition-size'],
- stats['size1-skipped'],
- stats['overall-duration'],
- stats['parse-duration'],
- stats['initialize-duration'],
- stats['refine-duration'],
- stats['algorithm-duration'],
- valmari[0],
- valmari[1]]
- #+END_SRC
+#+BEGIN_SRC python :session :eval never-export :results output silent :exports none
+def run_benchmark(model, const_assignments, initial_partition, disableopts, nofunctrans):
+ stats = run_all(model, const_assignments, initial_partition, disableopts, nofunctrans)
+ valmari = run_all_valmari(model, const_assignments, initial_partition)
+ return [model, const_assignments, initial_partition,
+ stats['states'],
+ stats['edges'],
+ stats['explicit-states'],
+ stats['initial-partition-size'],
+ stats['final-partition-size'],
+ stats['explicit-final-partition-size'],
+ stats['size1-skipped'],
+ stats['overall-duration'],
+ stats['parse-duration'],
+ stats['initialize-duration'],
+ stats['refine-duration'],
+ stats['algorithm-duration'],
+ valmari[0],
+ valmari[1]]
+#+END_SRC
+
+#+NAME: bench
+#+BEGIN_SRC python :session :eval no-export :var table="" :colnames no :hlines yes
+ [['Model', 'Consts', 'Partition', "States", "Edges", "Sort 0", "I", "Q", 'Q_0', 'Opts', 't(s)', 't_p(s)', 't_i(s)', 't_r(s)', 't_a(s)', 't_valmari(s)', 'Q_0v'], None] + \
+ list(map(lambda t: run_benchmark(t[0], t[1], t[2], False, False), table[2:]))
+#+END_SRC
- #+NAME: bench
- #+BEGIN_SRC python :session :eval no-export :var table="" :colnames no :hlines yes
+#+NAME: bench_noopt
+#+BEGIN_SRC python :session :eval no-export :var table="" :colnames no :hlines yes
[['Model', 'Consts', 'Partition', "States", "Edges", "Sort 0", "I", "Q", 'Q_0', 'Opts', 't(s)', 't_p(s)', 't_i(s)', 't_r(s)', 't_a(s)', 't_valmari(s)', 'Q_0v'], None] + \
- list(map(lambda t: run_benchmark(t[0], t[1], t[2], False), table[2:]))
- #+END_SRC
+ list(map(lambda t: run_benchmark(t[0], t[1], t[2], True, False), table[2:]))
+#+END_SRC
- #+NAME: bench_noopt
- #+BEGIN_SRC python :session :eval no-export :var table="" :colnames no :hlines yes
+#+NAME: bench_nofunctrans
+#+BEGIN_SRC python :session :eval no-export :var table="" :colnames no :hlines yes
[['Model', 'Consts', 'Partition', "States", "Edges", "Sort 0", "I", "Q", 'Q_0', 'Opts', 't(s)', 't_p(s)', 't_i(s)', 't_r(s)', 't_a(s)', 't_valmari(s)', 'Q_0v'], None] + \
- list(map(lambda t: run_benchmark(t[0], t[1], t[2], True), table[2:]))
- #+END_SRC
+ list(map(lambda t: run_benchmark(t[0], t[1], t[2], False, True), table[2:]))
+#+END_SRC
* Benchmarks
** Bounded Retransmission Protocol
@@ -712,7 +720,7 @@
| fms | n=6 | | 537768 | 4205670 | 537768 | 1766 | 537768 | 537768 | 4369694 | 21.3837698990 | 9.9432312680 | 2.9128952850 | 5.5583560150 | 9.6761859970 | 5.843124489 | NA |
-*** Comparing with and without 1-elem-optimization
+*** Comparing with and without optimization
We run a single benchmark multiple times. Once with and once without optimizations.
@@ -737,7 +745,7 @@ We run a single benchmark multiple times. Once with and once without optimizatio
| fms | n=6 | | 537768 | 4205670 | 537768 | 1766 | 537768 | 537768 | 4369694 | 20.8703022900 | 9.7372483350 | 2.8314794040 | 5.4073732580 | 9.4311009010 | 5.688309410 | NA |
| fms | n=6 | | 537768 | 4205670 | 537768 | 1766 | 537768 | 537768 | 4369694 | 20.9966534400 | 9.8001559310 | 2.8622791410 | 5.4498891670 | 9.4839336160 | 5.629692038 | NA |
-**** Without optimizations
+**** Without 1-elem optimization
:PROPERTIES:
:ID: 966b0dc7-cf00-4594-88ae-80332696166e
:END:
@@ -751,6 +759,20 @@ We run a single benchmark multiple times. Once with and once without optimizatio
| fms | n=6 | | 537768 | 4205670 | 537768 | 1766 | 537768 | 537768 | 0 | 36.2227431530 | 9.8527793370 | 2.8622964210 | 20.7738557100 | 24.8124665980 | 5.628144954 | NA |
| fms | n=6 | | 537768 | 4205670 | 537768 | 1766 | 537768 | 537768 | 0 | 36.0207062230 | 9.7157072660 | 2.8375580820 | 20.7020294520 | 24.7256647210 | 5.674519115 | NA |
+**** Without functor rewrites
+:PROPERTIES:
+:ID: 7e19eb5e-4009-4bc1-89a3-4e4e5c7f643e
+:END:
+
+#+CALL: bench_nofunctrans(fms_benchmark_single)
+
+#+RESULTS:
+| Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | Opts | t(s) | t_p(s) | t_i(s) | t_r(s) | t_a(s) | t_valmari(s) | Q_0v |
+|-------+--------+-----------+--------+---------+--------+------+--------+--------+---------+---------------+--------------+--------------+--------------+--------------+--------------+------|
+| fms | n=6 | | 537768 | 4205670 | 537768 | 1766 | 537768 | 537768 | 4369694 | 21.3317819830 | 9.9422740590 | 2.9165776070 | 5.5338563370 | 9.6616926620 | 5.676567183 | NA |
+| fms | n=6 | | 537768 | 4205670 | 537768 | 1766 | 537768 | 537768 | 4369694 | 21.3070570780 | 9.9521240360 | 2.9318476720 | 5.5074560910 | 9.6391451150 | 5.714505330 | NA |
+| fms | n=6 | | 537768 | 4205670 | 537768 | 1766 | 537768 | 537768 | 4369694 | 21.2953219580 | 9.9278855310 | 2.8900129830 | 5.5345639560 | 9.6430584370 | 5.873457181 | NA |
+
** Kanban
#+BEGIN_QUOTE
@@ -1394,7 +1416,7 @@ We run a single benchmark multiple times. Once with and once without optimizatio
| wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=0 | c1,c2 | 582327 | 771088 | 248503 | 9 | 236170 | 107865 | 0 | 15.3638788430 | 5.1630418130 | 3.0081672330 | 5.7031240120 | 9.2438828940 | 0.895646868 | 107865 |
| wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=0 | c1,c2 | 582327 | 771088 | 248503 | 9 | 236170 | 107865 | 0 | 15.2745021350 | 5.1306704560 | 3.0418000640 | 5.6621348040 | 9.2231714690 | 0.988643949 | 107865 |
-*** Comparing the 1-elem optimization again
+*** Comparing the optimizations
This time with a different benchmark
@@ -1420,7 +1442,7 @@ This time with a different benchmark
| wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 1408676 | 1963522 | 607727 | 9 | 543056 | 243325 | 271999 | 39.8326298410 | 13.3706358800 | 6.1359063500 | 16.2393612990 | 23.9411712310 | 2.543905222 | 243325 |
| wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 1408676 | 1963522 | 607727 | 9 | 543056 | 243325 | 271999 | 39.7848283170 | 13.3783298480 | 6.1493414580 | 16.2313925350 | 23.8928851990 | 2.586750034 | 243325 |
-**** Without optimizations
+**** Without 1-elem optimization
:PROPERTIES:
:ID: eb6cd726-026c-49ec-974a-1b6285d0fabb
:END:
@@ -1434,6 +1456,19 @@ This time with a different benchmark
| wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 1408676 | 1963522 | 607727 | 9 | 543056 | 243325 | 0 | 40.5545896510 | 13.4405492660 | 6.1304969200 | 16.8959012700 | 24.5962440200 | 2.516830279 | 243325 |
| wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 1408676 | 1963522 | 607727 | 9 | 543056 | 243325 | 0 | 40.8296828650 | 13.4560628920 | 6.1831625030 | 17.1048950840 | 24.8651696430 | 2.539904578 | 243325 |
+**** Without functor rewrite
+:PROPERTIES:
+:ID: 74566779-0749-4bbd-9556-80f857144793
+:END:
+
+#+CALL: bench_nofunctrans(wlan_benchmark_single2)
+
+#+RESULTS:
+| Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | Opts | t(s) | t_p(s) | t_i(s) | t_r(s) | t_a(s) | t_valmari(s) | Q_0v |
+|-------------------+------------------------------------+-----------+---------+---------+--------+----+---------+--------+--------+---------------+---------------+--------------+---------------+---------------+--------------+--------|
+| wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 2817352 | 3372198 | 607727 | 11 | 1038591 | 243325 | 272066 | 62.3224133500 | 24.0014545030 | 8.0163584000 | 22.5763681410 | 33.3185527870 | 2.538228830 | 243325 |
+| wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 2817352 | 3372198 | 607727 | 11 | 1038591 | 243325 | 272066 | 62.4165430840 | 23.9578211250 | 8.0180667980 | 22.6588742730 | 33.4171848350 | 2.526273353 | 243325 |
+| wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 2817352 | 3372198 | 607727 | 11 | 1038591 | 243325 | 272066 | 62.8521293030 | 23.9960135000 | 8.1913510000 | 22.7039631120 | 33.7983183080 | 2.539817679 | 243325 |
** Zeroconf
:PROPERTIES: