From 40621839df4483d58d29f040ca3a3e4f20bbb6ae Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hpd@hpdeifel.de>
Date: Wed, 31 Oct 2018 00:18:50 +0100
Subject: [PATCH] prism: Update benchmarks
---
prism/benchmark.org | 374 ++++++++++++++++++++++----------------------
1 file changed, 187 insertions(+), 187 deletions(-)
diff --git a/prism/benchmark.org b/prism/benchmark.org
index edc4d63..7c4f191 100644
--- a/prism/benchmark.org
+++ b/prism/benchmark.org
@@ -321,20 +321,20 @@
#+CALL: bench(brp_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-------+------------+-----------+--------+-------+--------+---+------+--------------+--------------+--------------+--------------|
- | brp | N=16,MAX=2 | s | 1354 | 1544 | 677 | 8 | 656 | 0.0202596730 | 0.0102995080 | 0.0083154340 | 0.002149536 |
- | brp | N=16,MAX=3 | s | 1772 | 2041 | 886 | 8 | 882 | 0.0214338710 | 0.0114332150 | 0.0085533570 | 0.002309430 |
- | brp | N=16,MAX=4 | s | 2190 | 2538 | 1095 | 8 | 1108 | 0.0283669860 | 0.0142651890 | 0.0125192220 | 0.002415548 |
- | brp | N=16,MAX=5 | s | 2608 | 3035 | 1304 | 8 | 1334 | 0.0320771210 | 0.0157281450 | 0.0142112560 | 0.002694890 |
- | brp | N=32,MAX=2 | s | 2698 | 3080 | 1349 | 8 | 1296 | 0.0325095100 | 0.0164302290 | 0.0139967900 | 0.002473492 |
- | brp | N=32,MAX=3 | s | 3532 | 4073 | 1766 | 8 | 1746 | 0.0437944950 | 0.0227312760 | 0.0190372900 | 0.003091343 |
- | brp | N=32,MAX=4 | s | 4366 | 5066 | 2183 | 8 | 2196 | 0.0550229100 | 0.0262486600 | 0.0261296720 | 0.003421692 |
- | brp | N=32,MAX=5 | s | 5200 | 6059 | 2600 | 8 | 2646 | 0.0658214110 | 0.0309070490 | 0.0314822830 | 0.004007015 |
- | brp | N=64,MAX=2 | s | 5386 | 6152 | 2693 | 8 | 2576 | 0.0658823780 | 0.0318694270 | 0.0287925920 | 0.003965890 |
- | brp | N=64,MAX=3 | s | 7052 | 8137 | 3526 | 8 | 3474 | 0.0919075860 | 0.0429443210 | 0.0444544850 | 0.004779758 |
- | brp | N=64,MAX=4 | s | 8718 | 10122 | 4359 | 8 | 4372 | 0.1196455480 | 0.0590531820 | 0.0543136790 | 0.005763311 |
- | brp | N=64,MAX=5 | s | 10384 | 12107 | 5192 | 8 | 5270 | 0.1670934010 | 0.0694743910 | 0.0891515340 | 0.006285228 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-------+------------+-----------+--------+-------+--------+---+------+------+--------------+--------------+--------------+--------------+------|
+ | brp | N=16,MAX=2 | s | 677 | 867 | 677 | 7 | 329 | 329 | 0.0373774390 | 0.0204458250 | 0.0152257340 | 0.001804035 | NA |
+ | brp | N=16,MAX=3 | s | 886 | 1155 | 886 | 7 | 442 | 442 | 0.0140537720 | 0.0057085550 | 0.0075240620 | 0.002026017 | NA |
+ | brp | N=16,MAX=4 | s | 1095 | 1443 | 1095 | 7 | 555 | 555 | 0.0183529520 | 0.0077354930 | 0.0093098840 | 0.002122708 | NA |
+ | brp | N=16,MAX=5 | s | 1304 | 1731 | 1304 | 7 | 668 | 668 | 0.0224552320 | 0.0087925450 | 0.0123908730 | 0.002480143 | NA |
+ | brp | N=32,MAX=2 | s | 1349 | 1731 | 1349 | 7 | 649 | 649 | 0.0219726340 | 0.0092532590 | 0.0114435580 | 0.002309687 | NA |
+ | brp | N=32,MAX=3 | s | 1766 | 2307 | 1766 | 7 | 874 | 874 | 0.0289253810 | 0.0113399820 | 0.0159887690 | 0.002788109 | NA |
+ | brp | N=32,MAX=4 | s | 2183 | 2883 | 2183 | 7 | 1099 | 1099 | 0.0378952270 | 0.0147304250 | 0.0213006090 | 0.003144004 | NA |
+ | brp | N=32,MAX=5 | s | 2600 | 3459 | 2600 | 7 | 1324 | 1324 | 0.0518128080 | 0.0217227650 | 0.0268356920 | 0.003886458 | NA |
+ | brp | N=64,MAX=2 | s | 2693 | 3459 | 2693 | 7 | 1289 | 1289 | 0.0448249680 | 0.0175989510 | 0.0248925890 | 0.003431631 | NA |
+ | brp | N=64,MAX=3 | s | 3526 | 4611 | 3526 | 7 | 1738 | 1738 | 0.0628191330 | 0.0229192590 | 0.0366669400 | 0.004610478 | NA |
+ | brp | N=64,MAX=4 | s | 4359 | 5763 | 4359 | 7 | 2187 | 2187 | 0.0800126010 | 0.0299000880 | 0.0460105110 | 0.005266248 | NA |
+ | brp | N=64,MAX=5 | s | 5192 | 6915 | 5192 | 7 | 2636 | 2636 | 0.1005523030 | 0.0351439820 | 0.0597582860 | 0.141978185 | NA |
** Cell in Wireless Communication Network
@@ -364,14 +364,14 @@
#+CALL: bench(cell_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-------+-------------+-----------+--------+-------+--------+-----+-----+--------------+--------------+--------------+--------------|
- | cell | N=50,T=0.5 | | 51 | 100 | 51 | 50 | 51 | 0.0011328470 | 0.0009498470 | 0.0001199340 | 0.001504079 |
- | cell | N=100,T=0.5 | | 101 | 200 | 101 | 80 | 101 | 0.0015420070 | 0.0009972660 | 0.0004575140 | 0.001502876 |
- | cell | N=200,T=0.5 | | 201 | 400 | 201 | 160 | 201 | 0.0022662020 | 0.0015966990 | 0.0004524780 | 0.001555440 |
- | cell | N=300,T=0.5 | | 301 | 600 | 301 | 251 | 301 | 0.0030290910 | 0.0019992860 | 0.0006535950 | 0.001803425 |
- | cell | N=400,T=0.5 | | 401 | 800 | 401 | 351 | 401 | 0.0039414910 | 0.0025291110 | 0.0011076590 | 0.001867502 |
- | cell | N=500,T=0.5 | | 501 | 1000 | 501 | 451 | 501 | 0.0045357650 | 0.0028279120 | 0.0012763760 | 0.002091393 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-------+-------------+-----------+--------+-------+--------+-----+-----+-----+--------------+--------------+--------------+--------------+------|
+ | cell | N=50,T=0.5 | | 51 | 100 | 51 | 50 | 51 | 51 | 0.0011676780 | 0.0009303200 | 0.0001433640 | 0.001362867 | NA |
+ | cell | N=100,T=0.5 | | 101 | 200 | 101 | 80 | 101 | 101 | 0.0014387010 | 0.0009194470 | 0.0004346910 | 0.001281246 | NA |
+ | cell | N=200,T=0.5 | | 201 | 400 | 201 | 160 | 201 | 201 | 0.0024421880 | 0.0017179640 | 0.0005000630 | 0.003504114 | NA |
+ | cell | N=300,T=0.5 | | 301 | 600 | 301 | 251 | 301 | 301 | 0.0031271730 | 0.0020915020 | 0.0007124940 | 0.002171734 | NA |
+ | cell | N=400,T=0.5 | | 401 | 800 | 401 | 351 | 401 | 401 | 0.0037854340 | 0.0024571330 | 0.0010355270 | 0.001671380 | NA |
+ | cell | N=500,T=0.5 | | 501 | 1000 | 501 | 451 | 501 | 501 | 0.0044740830 | 0.0028285420 | 0.0012152600 | 0.001830942 | NA |
** Dependable Cluster
@@ -396,12 +396,12 @@
#+CALL: bench(cluster_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |---------+-----------+-----------+--------+--------+--------+------+-------+--------------+--------------+--------------+--------------|
- | cluster | N=4,T=10 | | 820 | 3616 | 820 | 183 | 565 | 0.0169006920 | 0.0078237790 | 0.0082840800 | 0.003284676 |
- | cluster | N=8,T=10 | | 2772 | 12832 | 2772 | 359 | 1917 | 0.0613999710 | 0.0261539960 | 0.0324123900 | 0.008421882 |
- | cluster | N=16,T=10 | | 10132 | 48160 | 10132 | 711 | 7021 | 0.2702806220 | 0.1053783250 | 0.1510995340 | 0.028009609 |
- | cluster | N=32,T=10 | | 38676 | 186400 | 38676 | 1415 | 26829 | 1.1740824720 | 0.3990564290 | 0.6802306580 | 0.117198263 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |---------+-----------+-----------+--------+--------+--------+------+-------+-------+--------------+--------------+--------------+--------------+------|
+ | cluster | N=4,T=10 | | 820 | 3616 | 820 | 183 | 565 | 565 | 0.0193714380 | 0.0088562680 | 0.0095646740 | 0.003312910 | NA |
+ | cluster | N=8,T=10 | | 2772 | 12832 | 2772 | 359 | 1917 | 1917 | 0.0599859040 | 0.0251998340 | 0.0309856360 | 0.008382883 | NA |
+ | cluster | N=16,T=10 | | 10132 | 48160 | 10132 | 711 | 7021 | 7021 | 0.2673604280 | 0.1035486140 | 0.1501898910 | 0.217959900 | NA |
+ | cluster | N=32,T=10 | | 38676 | 186400 | 38676 | 1415 | 26829 | 26829 | 1.2315221770 | 0.4716808680 | 0.6643042390 | 0.141528757 | NA |
** Shared coin protocol
@@ -425,12 +425,12 @@
#+CALL: bench(consensus_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-------+--------------+-----------------+--------+--------+--------+-----+-------+--------------+--------------+--------------+--------------|
- | coin | N=2,K=2,k=10 | pc1,pc2 | 1344 | 1564 | 272 | 20 | 437 | 0.0166496940 | 0.0092504160 | 0.0069378580 | 0.001774161 |
- | coin | N=2,K=4,k=10 | pc1,pc2 | 2624 | 3068 | 528 | 20 | 837 | 0.0322432680 | 0.0166440640 | 0.0144193950 | 0.002107052 |
- | coin | N=4,K=2,k=10 | pc1,pc2,pc3,pc4 | 166400 | 218976 | 22656 | 262 | 32860 | 3.1329518880 | 1.1488851980 | 1.8658573580 | 0.086255911 |
- | coin | N=4,K=4,k=10 | pc1,pc2,pc3,pc4 | 317952 | 419168 | 43136 | 262 | 63132 | 6.4697686060 | 2.1805455820 | 3.9879320210 | 0.172912059 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-------+--------------+-----------------+--------+--------+--------+-----+-------+-------+--------------+--------------+--------------+--------------+-------|
+ | coin | N=2,K=2,k=10 | pc1,pc2 | 672 | 892 | 272 | 18 | 231 | 95 | 0.0124291850 | 0.0060656990 | 0.0059153700 | 0.001786334 | 95 |
+ | coin | N=2,K=4,k=10 | pc1,pc2 | 1312 | 1756 | 528 | 18 | 439 | 183 | 0.0209580860 | 0.0070945080 | 0.0123054790 | 0.002097912 | 183 |
+ | coin | N=4,K=2,k=10 | pc1,pc2,pc3,pc4 | 83200 | 135776 | 22656 | 260 | 18522 | 5392 | 2.3250785960 | 0.5819388980 | 1.6748731840 | 0.118400836 | 5392 |
+ | coin | N=4,K=4,k=10 | pc1,pc2,pc3,pc4 | 158976 | 260192 | 43136 | 260 | 35482 | 10352 | 4.5686613180 | 1.1145849630 | 3.2476925690 | 0.193811507 | 10352 |
** IEEE 802.3 CSMA/CD
@@ -465,13 +465,13 @@
#+CALL: bench(csma_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-------+-------------+-----------+---------+---------+--------+---+-------+---------------+---------------+---------------+--------------|
- | csma | N=2,K=2,k=1 | b | 4184 | 4428 | 1038 | 7 | 929 | 0.0494152380 | 0.0283352880 | 0.0192856740 | 0.002761276 |
- | csma | N=2,K=4,k=1 | b | 31892 | 34528 | 7958 | 7 | 3955 | 0.4126711850 | 0.1982495930 | 0.1968982030 | 0.013688714 |
- | csma | N=2,K=6,k=1 | b | 267012 | 293366 | 66718 | 7 | 29575 | 4.8421286430 | 1.8968389470 | 2.6847511070 | 0.118215164 |
- | csma | N=3,K=2,k=1 | b | 150612 | 169624 | 36850 | 8 | 9228 | 2.8152048920 | 1.0343917820 | 1.5463293940 | 0.063031481 |
- | csma | N=4,K=2,k=1 | b | 3174932 | 3740038 | 761962 | 9 | 40920 | 83.9797209220 | 25.9414732210 | 54.6122784800 | 2.042126831 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-------+-------------+-----------+---------+---------+--------+---+-------+------+---------------+---------------+---------------+--------------+------|
+ | csma | N=2,K=2,k=1 | b | 2092 | 2336 | 1038 | 5 | 470 | 233 | 0.0343206830 | 0.0139484280 | 0.0187489780 | 0.002635600 | 233 |
+ | csma | N=2,K=4,k=1 | b | 15946 | 18582 | 7958 | 5 | 1992 | 997 | 0.2982624200 | 0.1155415110 | 0.1665479790 | 0.013442486 | 997 |
+ | csma | N=2,K=6,k=1 | b | 133506 | 159860 | 66718 | 5 | 14829 | 7436 | 3.1429969940 | 0.8405545260 | 2.0722624040 | 0.133832368 | 7436 |
+ | csma | N=3,K=2,k=1 | b | 75306 | 94318 | 36850 | 6 | 4686 | 2281 | 1.6440409950 | 0.4906179150 | 1.0833934760 | 0.090110651 | 2281 |
+ | csma | N=4,K=2,k=1 | b | 1587466 | 2152572 | 761962 | 7 | 21024 | 9830 | 55.3879561460 | 14.2149838970 | 38.5313801010 | 2.026345765 | 9830 |
** Dice
@@ -494,11 +494,11 @@
#+CALL: bench(dice_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |----------------+--------+-----------+--------+-------+--------+----+-----+--------------+--------------+--------------+--------------|
- | dice | | s | 26 | 33 | 13 | 9 | 14 | 0.0013463390 | 0.0011487930 | 0.0001454540 | 0.001353259 |
- | two_dice_knuth | | s | 90 | 124 | 45 | 36 | 65 | 0.0017951110 | 0.0012336440 | 0.0005021370 | 0.001354521 |
- | two_dice | | s1,s2 | 846 | 1113 | 169 | 68 | 316 | 0.0095234110 | 0.0059030030 | 0.0033710280 | 0.001774375 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |----------------+--------+-----------+--------+-------+--------+----+-----+-----+--------------+--------------+--------------+--------------+------|
+ | dice | | s | 13 | 20 | 13 | 8 | 8 | 8 | 0.0009058700 | 0.0006924430 | 0.0001552390 | 0.001260493 | NA |
+ | two_dice_knuth | | s | 45 | 79 | 45 | 35 | 35 | 35 | 0.0012327070 | 0.0010378750 | 0.0001362100 | 0.001199256 | NA |
+ | two_dice | | s1,s2 | 423 | 690 | 169 | 66 | 160 | 64 | 0.0085937680 | 0.0050529530 | 0.0033376730 | 0.001537383 | 64 |
** Dining cryptographers
@@ -524,13 +524,13 @@
#+CALL: bench(dining_crypt_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |--------------+--------+-----------+---------+---------+--------+----+-------+---------------+---------------+---------------+--------------|
- | dining_crypt | N=3 | pay | 2000 | 2396 | 380 | 9 | 164 | 0.0234645930 | 0.0132989050 | 0.0085936890 | 0.002175370 |
- | dining_crypt | N=4 | pay | 13410 | 16965 | 2165 | 11 | 560 | 0.1795917050 | 0.0840534430 | 0.0882113680 | 0.006376125 |
- | dining_crypt | N=5 | pay | 85104 | 112026 | 11850 | 13 | 1644 | 1.4277203340 | 0.5802520010 | 0.8102711210 | 0.038009236 |
- | dining_crypt | N=6 | pay | 516698 | 700455 | 63063 | 15 | 4445 | 10.7725457330 | 3.7978662670 | 6.6046398470 | 0.254485920 |
- | dining_crypt | N=7 | pay | 3029600 | 4200312 | 328760 | 17 | 11384 | 77.1360998520 | 25.1148376700 | 49.6569179400 | 1.683909862 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |--------------+--------+-----------+---------+---------+--------+----+------+------+---------------+---------------+---------------+--------------+------|
+ | dining_crypt | N=3 | pay | 1000 | 1396 | 380 | 7 | 96 | 36 | 0.0161892200 | 0.0079901050 | 0.0077348570 | 0.001928556 | 36 |
+ | dining_crypt | N=4 | pay | 6705 | 10260 | 2165 | 9 | 335 | 115 | 0.1127357880 | 0.0402905120 | 0.0690622510 | 0.006093009 | 115 |
+ | dining_crypt | N=5 | pay | 42552 | 69474 | 11850 | 11 | 1014 | 318 | 0.9264858650 | 0.2666935890 | 0.6054998160 | 0.040335534 | 318 |
+ | dining_crypt | N=6 | pay | 258349 | 442106 | 63063 | 13 | 2842 | 805 | 6.6041376030 | 1.8525384900 | 4.5724769850 | 0.255761754 | 805 |
+ | dining_crypt | N=7 | pay | 1514800 | 2685512 | 328760 | 15 | 7536 | 1928 | 45.2948491710 | 12.5502440290 | 31.5424213600 | 1.679455502 | 1928 |
** Embedded Control System
@@ -555,11 +555,11 @@
#+CALL: bench(embedded_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |----------+------------------+-----------+--------+-------+--------+----+-----+--------------+--------------+--------------+--------------|
- | embedded | MAX_COUNT=2,T=12 | i,a,m | 6956 | 18117 | 3478 | 86 | 252 | 0.1118336670 | 0.0670545140 | 0.0406941350 | 0.013228961 |
- | embedded | MAX_COUNT=2,T=14 | i,a,m | 6956 | 18117 | 3478 | 86 | 252 | 0.1281870580 | 0.0697041020 | 0.0497916980 | 0.013421337 |
- | embedded | MAX_COUNT=2,T=0 | i,a,m | 6956 | 18117 | 3478 | 86 | 252 | 0.1085432620 | 0.0634605300 | 0.0410748420 | 0.012998660 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |----------+------------------+-----------+--------+-------+--------+-----+-----+-----+--------------+--------------+--------------+--------------+------|
+ | embedded | MAX_COUNT=2,T=12 | i,a,m | 3478 | 14639 | 3478 | 152 | 560 | 560 | 0.1158639350 | 0.0483491360 | 0.0645445580 | 0.013104902 | NA |
+ | embedded | MAX_COUNT=2,T=14 | i,a,m | 3478 | 14639 | 3478 | 152 | 560 | 560 | 0.1082902710 | 0.0416334620 | 0.0637769040 | 0.013742779 | NA |
+ | embedded | MAX_COUNT=2,T=0 | i,a,m | 3478 | 14639 | 3478 | 152 | 560 | 560 | 0.1094423070 | 0.0420950640 | 0.0643464660 | 0.013086958 | NA |
** Firewire
@@ -612,22 +612,22 @@
#+CALL: bench(firewire_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |------------------------+--------------------------------+-----------+---------+---------+--------+----+--------+---------------+---------------+---------------+--------------|
- | firewire_abst_firewire | delay=36,fast=0.5 | s | 3930 | 4565 | 776 | 15 | 3242 | 0.0530911930 | 0.0292487850 | 0.0219630440 | 0.003014310 |
- | firewire_abst_firewire | delay=3,fast=0.2:0.1:0.8 | s | 2610 | 2717 | 611 | 15 | 2450 | 0.0298428020 | 0.0151824090 | 0.0134062910 | 0.002358096 |
- | firewire_abst_firewire | delay=36,fast=0.2:0.1:0.8 | s | 3930 | 4565 | 776 | 15 | 3242 | 0.0467456700 | 0.0236742070 | 0.0212447830 | 0.003015546 |
- | firewire_abst_deadline | deadline=200,delay=36,fast=0.5 | s | 327514 | 373007 | 67901 | 17 | 70383 | 6.7777738240 | 2.2877971300 | 4.2027125650 | 0.162179300 |
- | firewire_abst_deadline | deadline=300,delay=36,fast=0.5 | s | 703930 | 810013 | 142810 | 17 | 273380 | 16.5917206760 | 4.9626792550 | 10.5475405420 | 0.416113801 |
- | firewire_abst_deadline | deadline=400,delay=36,fast=0.5 | s | 1096930 | 1266513 | 220410 | 17 | 462758 | 27.2058529830 | 8.3210653120 | 17.5561356870 | 0.675145289 |
- | firewire_abst_deadline | deadline=500,delay=36,fast=0.5 | s | 1489930 | 1723013 | 298010 | 17 | 653158 | 38.2232837950 | 11.4491819320 | 24.5965126400 | 0.936638134 |
- | firewire_abst_deadline | deadline=600,delay=36,fast=0.5 | s | 1882930 | 2179513 | 375610 | 17 | 843558 | 49.8061531330 | 14.2242202320 | 32.0929149970 | 1.282804713 |
- | firewire_impl_firewire | delay=36,fast=0.5 | w12 | 1382048 | 1651572 | 212268 | 10 | 256615 | 37.0318118280 | 10.4577420250 | 24.8537176890 | 0.894251068 |
- | firewire_impl_firewire | delay=3,fast=0.2:0.1:0.8 | w12 | 19224 | 20716 | 4093 | 10 | 14581 | 0.2672704380 | 0.1153124960 | 0.1357688810 | 0.009006543 |
- | firewire_impl_firewire | delay=36,fast=0.2:0.1:0.8 | w12 | 1382048 | 1651572 | 212268 | 10 | 256615 | 36.5008171890 | 10.2690859140 | 24.5284158720 | 0.897536961 |
- | firewire_impl_deadline | deadline=200,delay=3,fast=0.5 | w12 | 384032 | 416294 | 80980 | 10 | 7925 | 5.8752263940 | 2.6159971650 | 3.0166369380 | 0.138102826 |
- | firewire_impl_deadline | deadline=300,delay=3,fast=0.5 | w12 | 995134 | 1069583 | 213805 | 10 | 20640 | 16.2066158490 | 7.0883824850 | 8.4395501270 | 0.388696986 |
- | firewire_impl_deadline | deadline=400,delay=3,fast=0.5 | w12 | 2040822 | 2201345 | 434364 | 10 | 475841 | 41.3992261300 | 15.6562968780 | 23.1548002740 | 1.014870145 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |------------------------+--------------------------------+-----------+---------+---------+--------+----+--------+--------+---------------+--------------+---------------+--------------+--------|
+ | firewire_abst_firewire | delay=36,fast=0.5 | s | 1965 | 2600 | 776 | 13 | 1623 | 776 | 0.0384609120 | 0.0135733880 | 0.0233808050 | 0.002941471 | 776 |
+ | firewire_abst_firewire | delay=3,fast=0.2:0.1:0.8 | s | 1305 | 1412 | 611 | 13 | 1227 | 611 | 0.0182079700 | 0.0063022380 | 0.0108083100 | 0.002220293 | 611 |
+ | firewire_abst_firewire | delay=36,fast=0.2:0.1:0.8 | s | 1965 | 2600 | 776 | 13 | 1623 | 776 | 0.0295681120 | 0.0106359100 | 0.0178537030 | 0.003005253 | 776 |
+ | firewire_abst_deadline | deadline=200,delay=36,fast=0.5 | s | 163757 | 209250 | 67901 | 15 | 35260 | 15848 | 4.2821563640 | 1.1393089320 | 2.9786258460 | 0.190295118 | 15848 |
+ | firewire_abst_deadline | deadline=300,delay=36,fast=0.5 | s | 351965 | 458048 | 142810 | 15 | 136910 | 63708 | 10.5084312020 | 2.5634628710 | 7.4930864910 | 0.502950189 | 63708 |
+ | firewire_abst_deadline | deadline=400,delay=36,fast=0.5 | s | 548465 | 718048 | 220410 | 15 | 231876 | 107370 | 16.9113232150 | 4.0496925950 | 12.0911771220 | 0.804662446 | 107370 |
+ | firewire_abst_deadline | deadline=500,delay=36,fast=0.5 | s | 744965 | 978048 | 298010 | 15 | 327376 | 151270 | 23.4279473190 | 5.4956145690 | 16.8394684980 | 1.167988726 | 151270 |
+ | firewire_abst_deadline | deadline=600,delay=36,fast=0.5 | s | 941465 | 1238048 | 375610 | 15 | 422876 | 195170 | 30.8133933470 | 7.3875186570 | 21.9758213760 | 1.496577306 | 195170 |
+ | firewire_impl_firewire | delay=36,fast=0.5 | w12 | 691024 | 960548 | 212268 | 8 | 131382 | 62836 | 23.6471015010 | 4.9016731180 | 17.8979509550 | 0.988364671 | 62836 |
+ | firewire_impl_firewire | delay=3,fast=0.2:0.1:0.8 | w12 | 9612 | 11104 | 4093 | 8 | 7362 | 3631 | 0.1795763780 | 0.0534055310 | 0.1182857070 | 0.125829353 | 3631 |
+ | firewire_impl_firewire | delay=36,fast=0.2:0.1:0.8 | w12 | 691024 | 960548 | 212268 | 8 | 131382 | 62836 | 23.5915041120 | 4.9392515940 | 17.8103947040 | 0.982834687 | 62836 |
+ | firewire_impl_deadline | deadline=200,delay=3,fast=0.5 | w12 | 192016 | 224278 | 80980 | 8 | 4021 | 1967 | 3.4135964830 | 1.2760307090 | 1.9222134620 | 0.146304165 | 1967 |
+ | firewire_impl_deadline | deadline=300,delay=3,fast=0.5 | w12 | 497567 | 572016 | 213805 | 8 | 10432 | 5133 | 10.4063802620 | 3.6262297710 | 6.3183020130 | 0.393506709 | 5133 |
+ | firewire_impl_deadline | deadline=400,delay=3,fast=0.5 | w12 | 1020411 | 1180934 | 434364 | 8 | 240169 | 118151 | 24.9434744920 | 7.4574397270 | 16.0661705990 | 1.195568660 | 118151 |
** Flexible Manufacturing System
@@ -657,14 +657,14 @@
#+CALL: bench(fms_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-------+--------+-----------+--------+---------+--------+-----+--------+---------------+--------------+---------------+--------------|
- | fms | n=1 | | 54 | 155 | 54 | 25 | 54 | 0.0011827400 | 0.0009253590 | 0.0001802780 | 0.001571953 |
- | fms | n=2 | | 810 | 3699 | 810 | 95 | 810 | 0.0142572690 | 0.0075303740 | 0.0057155820 | 0.003826568 |
- | fms | n=3 | | 6520 | 37394 | 6520 | 190 | 6520 | 0.1542268220 | 0.0730456090 | 0.0726066830 | 0.029094708 |
- | fms | n=4 | | 35910 | 237120 | 35910 | 294 | 35910 | 1.0856177700 | 0.4666757000 | 0.5577012290 | 0.198376081 |
- | fms | n=5 | | 152712 | 1111482 | 152712 | 372 | 152712 | 6.0818450290 | 2.4388620660 | 3.2654031390 | 1.160481592 |
- | fms | n=6 | | 537768 | 4205670 | 537768 | 463 | 537768 | 25.8463488400 | 9.7678142610 | 14.5281689380 | 5.385258385 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-------+--------+-----------+--------+---------+--------+-----+--------+--------+---------------+--------------+---------------+--------------+------|
+ | fms | n=1 | | 54 | 155 | 54 | 25 | 54 | 54 | 0.0027695680 | 0.0020326750 | 0.0005347760 | 0.001302236 | NA |
+ | fms | n=2 | | 810 | 3699 | 810 | 95 | 810 | 810 | 0.0137363510 | 0.0075075570 | 0.0049695810 | 0.003743593 | NA |
+ | fms | n=3 | | 6520 | 37394 | 6520 | 190 | 6520 | 6520 | 0.1535406920 | 0.0762844330 | 0.0685589050 | 0.148513659 | NA |
+ | fms | n=4 | | 35910 | 237120 | 35910 | 294 | 35910 | 35910 | 1.1035074370 | 0.5012303600 | 0.5353624030 | 0.211326362 | NA |
+ | fms | n=5 | | 152712 | 1111482 | 152712 | 372 | 152712 | 152712 | 5.8206713820 | 2.4356896450 | 3.0083955470 | 1.196443773 | NA |
+ | fms | n=6 | | 537768 | 4205670 | 537768 | 463 | 537768 | 537768 | 25.2295242230 | 9.7541697760 | 13.9126260830 | 5.642700833 | NA |
** Kanban
@@ -691,12 +691,12 @@
#+CALL: bench(kanban_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |--------+--------+-----------+--------+---------+--------+----+--------+---------------+--------------+---------------+--------------|
- | kanban | t=1 | | 160 | 616 | 160 | 43 | 160 | 0.0028181150 | 0.0020233060 | 0.0005745400 | 0.001435628 |
- | kanban | t=2 | | 4600 | 28120 | 4600 | 69 | 4600 | 0.0995035240 | 0.0526479650 | 0.0413604970 | 0.018956863 |
- | kanban | t=3 | | 58400 | 446400 | 58400 | 81 | 58400 | 2.1778529960 | 0.8510330230 | 1.1186015150 | 0.349015574 |
- | kanban | t=4 | | 454475 | 3979850 | 454475 | 86 | 454475 | 24.7147020410 | 8.9672916140 | 14.4873543830 | 4.784644693 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |--------+--------+-----------+--------+---------+--------+----+--------+--------+---------------+--------------+---------------+--------------+------|
+ | kanban | t=1 | | 160 | 616 | 160 | 43 | 160 | 160 | 0.0043981930 | 0.0036662350 | 0.0005347790 | 0.001630305 | NA |
+ | kanban | t=2 | | 4600 | 28120 | 4600 | 69 | 4600 | 4600 | 0.1017988090 | 0.0529543130 | 0.0412840410 | 0.153109183 | NA |
+ | kanban | t=3 | | 58400 | 446400 | 58400 | 81 | 58400 | 58400 | 2.1177241660 | 0.8688213570 | 1.0524390480 | 0.374841061 | NA |
+ | kanban | t=4 | | 454475 | 3979850 | 454475 | 86 | 454475 | 454475 | 23.8471982380 | 8.9731928780 | 13.6251115360 | 5.183629876 | NA |
** Leader Election Protocol
*** Synchronous
@@ -729,17 +729,17 @@
#+CALL: bench(leader_sync_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-------------+-------------+----------------+--------+-------+--------+---+----+--------------+--------------+--------------+--------------|
- | leader_sync | N=3,K=2,L=1 | s1,s2,s3 | 52 | 59 | 26 | 5 | 15 | 0.0020590370 | 0.0013447340 | 0.0005368510 | 0.001170329 |
- | leader_sync | N=3,K=3,L=1 | s1,s2,s3 | 138 | 164 | 69 | 5 | 15 | 0.0020689240 | 0.0016545460 | 0.0003482500 | 0.001210456 |
- | leader_sync | N=3,K=4,L=1 | s1,s2,s3 | 294 | 357 | 147 | 5 | 15 | 0.0032101670 | 0.0023880870 | 0.0007183870 | 0.001291121 |
- | leader_sync | N=4,K=2,L=1 | s1,s2,s3,s4 | 122 | 137 | 61 | 5 | 19 | 0.0019183680 | 0.0015397180 | 0.0002775180 | 0.001184142 |
- | leader_sync | N=4,K=3,L=1 | s1,s2,s3,s4 | 548 | 628 | 274 | 5 | 19 | 0.0056185720 | 0.0038216310 | 0.0015942050 | 0.001351651 |
- | leader_sync | N=4,K=4,L=1 | s1,s2,s3,s4 | 1624 | 1879 | 812 | 5 | 19 | 0.0155145470 | 0.0100154920 | 0.0048928820 | 0.001689804 |
- | leader_sync | N=5,K=2,L=1 | s1,s2,s3,s4,s5 | 282 | 313 | 141 | 5 | 23 | 0.0031412440 | 0.0023037270 | 0.0007313390 | 0.001236276 |
- | leader_sync | N=5,K=3,L=1 | s1,s2,s3,s4,s5 | 2100 | 2342 | 1050 | 5 | 23 | 0.0198006790 | 0.0124331450 | 0.0064562300 | 0.001838288 |
- | leader_sync | N=5,K=4,L=1 | s1,s2,s3,s4,s5 | 8488 | 9511 | 4244 | 5 | 23 | 0.0908090200 | 0.0522178840 | 0.0325702690 | 0.004049696 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-------------+-------------+----------------+--------+-------+--------+---+----+-----+--------------+--------------+--------------+--------------+------|
+ | leader_sync | N=3,K=2,L=1 | s1,s2,s3 | 26 | 33 | 26 | 4 | 8 | 8 | 0.0012051610 | 0.0008919190 | 0.0002296060 | 0.001514285 | NA |
+ | leader_sync | N=3,K=3,L=1 | s1,s2,s3 | 69 | 95 | 69 | 4 | 8 | 8 | 0.0015021590 | 0.0009763670 | 0.0004741170 | 0.001258788 | NA |
+ | leader_sync | N=3,K=4,L=1 | s1,s2,s3 | 147 | 210 | 147 | 4 | 8 | 8 | 0.0021806760 | 0.0015907640 | 0.0003543110 | 0.001239725 | NA |
+ | leader_sync | N=4,K=2,L=1 | s1,s2,s3,s4 | 61 | 76 | 61 | 4 | 10 | 10 | 0.0012497620 | 0.0010005990 | 0.0001921400 | 0.001293489 | NA |
+ | leader_sync | N=4,K=3,L=1 | s1,s2,s3,s4 | 274 | 354 | 274 | 4 | 10 | 10 | 0.0036157460 | 0.0025247210 | 0.0009583470 | 0.001405601 | NA |
+ | leader_sync | N=4,K=4,L=1 | s1,s2,s3,s4 | 812 | 1067 | 812 | 4 | 10 | 10 | 0.0096473780 | 0.0054189810 | 0.0036687170 | 0.001867704 | NA |
+ | leader_sync | N=5,K=2,L=1 | s1,s2,s3,s4,s5 | 141 | 172 | 141 | 4 | 12 | 12 | 0.0022099400 | 0.0016510960 | 0.0004331620 | 0.001324117 | NA |
+ | leader_sync | N=5,K=3,L=1 | s1,s2,s3,s4,s5 | 1050 | 1292 | 1050 | 4 | 12 | 12 | 0.0131144340 | 0.0073943540 | 0.0048857200 | 0.002051182 | NA |
+ | leader_sync | N=5,K=4,L=1 | s1,s2,s3,s4,s5 | 4244 | 5267 | 4244 | 4 | 12 | 12 | 0.0534547100 | 0.0274600550 | 0.0226146050 | 0.004176759 | NA |
*** Asynchronous
@@ -765,11 +765,11 @@
#+CALL: bench(leader_async_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |--------------+---------+----------------+--------+--------+--------+-----+-------+--------------+--------------+--------------+--------------|
- | leader_async | N=3,K=1 | s1,s2,s3 | 1874 | 2164 | 364 | 59 | 732 | 0.0240404010 | 0.0132842680 | 0.0098047740 | 0.001966300 |
- | leader_async | N=4,K=1 | s1,s2,s3,s4 | 18848 | 22820 | 3172 | 223 | 5611 | 0.2916478960 | 0.1391586730 | 0.1419070690 | 0.013835285 |
- | leader_async | N=5,K=1 | s1,s2,s3,s4,s5 | 184568 | 231634 | 27299 | 870 | 41756 | 3.5905053640 | 1.2768928910 | 2.1808222650 | 0.097230589 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |--------------+---------+----------------+--------+--------+--------+-----+-------+------+--------------+--------------+--------------+--------------+------|
+ | leader_async | N=3,K=1 | s1,s2,s3 | 937 | 1227 | 364 | 57 | 385 | 171 | 0.0164843340 | 0.0081200900 | 0.0076695220 | 0.001907752 | 171 |
+ | leader_async | N=4,K=1 | s1,s2,s3,s4 | 9424 | 13396 | 3172 | 221 | 2974 | 1169 | 0.1954432560 | 0.0627651930 | 0.1232613580 | 0.009560667 | 1169 |
+ | leader_async | N=5,K=1 | s1,s2,s3,s4,s5 | 92284 | 139350 | 27299 | 868 | 22626 | 7948 | 2.3265634720 | 0.6525356730 | 1.5961905890 | 0.114070581 | 7948 |
** Molecules
@@ -808,17 +808,17 @@
#+CALL: bench(molecules_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-------+---------------------------------------+-----------+--------+-------+--------+----+-----+--------------+--------------+--------------+--------------|
- | nacl | N1=10,N2=10,T=0:0.001:0.006,i=4 | na | 22 | 31 | 11 | 22 | 22 | 0.0007961260 | 0.0005686150 | 0.0001787610 | 0.001234372 |
- | nacl | N1=10,N2=10,T=0:0.001:0.006,i=0 | na | 22 | 31 | 11 | 22 | 22 | 0.0007806050 | 0.0005755910 | 0.0001006150 | 0.001166277 |
- | nacl | N1=10,N2=10,T=0,i=0 | na | 22 | 31 | 11 | 22 | 22 | 0.0007561780 | 0.0005992040 | 0.0001041540 | 0.001187662 |
- | knacl | N1=10,N2=10,N3=10,T=0:0.001:0.006,i=4 | na | 132 | 286 | 66 | 76 | 132 | 0.0022448360 | 0.0018103490 | 0.0003525870 | 0.001376522 |
- | knacl | N1=10,N2=10,N3=10,T=0:0.001:0.006,i=0 | na | 132 | 286 | 66 | 76 | 132 | 0.0022776530 | 0.0018280460 | 0.0003666330 | 0.001285510 |
- | knacl | N1=10,N2=10,N3=10,T=0,i=0 | na | 132 | 286 | 66 | 76 | 132 | 0.0022601980 | 0.0018272380 | 0.0003495470 | 0.001268068 |
- | mc | N1=10,N2=10,T=0:0.001:0.006,i=4 | mg | 72 | 146 | 36 | 47 | 72 | 0.0016914570 | 0.0011755080 | 0.0004527470 | 0.001230690 |
- | mc | N1=10,N2=10,T=0:0.001:0.006,i=0 | mg | 72 | 146 | 36 | 47 | 72 | 0.0015948330 | 0.0011008890 | 0.0004396060 | 0.001222564 |
- | mc | N1=10,N2=10,T=0i=0 | mg | 72 | 146 | 36 | 47 | 72 | 0.0016406260 | 0.0011483810 | 0.0004374580 | 0.001252315 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-------+---------------------------------------+-----------+--------+-------+--------+----+----+-----+--------------+--------------+--------------+--------------+------|
+ | nacl | N1=10,N2=10,T=0:0.001:0.006,i=4 | na | 11 | 20 | 11 | 11 | 11 | 11 | 0.0009441510 | 0.0007848570 | 0.0001018140 | 0.001348267 | NA |
+ | nacl | N1=10,N2=10,T=0:0.001:0.006,i=0 | na | 11 | 20 | 11 | 11 | 11 | 11 | 0.0007495060 | 0.0006365920 | 0.0000709000 | 0.001174548 | NA |
+ | nacl | N1=10,N2=10,T=0,i=0 | na | 11 | 20 | 11 | 11 | 11 | 11 | 0.0006624600 | 0.0005476220 | 0.0000725790 | 0.001208477 | NA |
+ | knacl | N1=10,N2=10,N3=10,T=0:0.001:0.006,i=4 | na | 66 | 220 | 66 | 66 | 66 | 66 | 0.0017893470 | 0.0015809280 | 0.0001433970 | 0.001330679 | NA |
+ | knacl | N1=10,N2=10,N3=10,T=0:0.001:0.006,i=0 | na | 66 | 220 | 66 | 66 | 66 | 66 | 0.0017992330 | 0.0015818900 | 0.0001500450 | 0.001255018 | NA |
+ | knacl | N1=10,N2=10,N3=10,T=0,i=0 | na | 66 | 220 | 66 | 66 | 66 | 66 | 0.0017566360 | 0.0015493320 | 0.0001428110 | 0.001218437 | NA |
+ | mc | N1=10,N2=10,T=0:0.001:0.006,i=4 | mg | 36 | 110 | 36 | 36 | 36 | 36 | 0.0011984690 | 0.0010461900 | 0.0000964790 | 0.001384311 | NA |
+ | mc | N1=10,N2=10,T=0:0.001:0.006,i=0 | mg | 36 | 110 | 36 | 36 | 36 | 36 | 0.0011476870 | 0.0009940860 | 0.0000965050 | 0.001289684 | NA |
+ | mc | N1=10,N2=10,T=0i=0 | mg | 36 | 110 | 36 | 36 | 36 | 36 | 0.0012536670 | 0.0010887060 | 0.0000967990 | 0.001375207 | NA |
** Mutual Exclusion
@@ -869,11 +869,11 @@
#+CALL: bench(mutual_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |--------+--------+-----------+---------+---------+--------+----+---------+----------------+---------------+----------------+--------------|
- | mutual | N=3 | p1 | 21272 | 27628 | 2368 | 24 | 12874 | 0.3562959450 | 0.1326003510 | 0.2104688670 | 0.012258514 |
- | mutual | N=4 | p1 | 314368 | 423760 | 27600 | 26 | 178996 | 7.8024324260 | 2.1878985260 | 5.2989352130 | 0.218172462 |
- | mutual | N=5 | p1 | 4260480 | 5881840 | 308800 | 28 | 2320292 | 153.7128500830 | 32.9383896050 | 111.6750890410 | 4.125266199 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |--------+--------+-----------+---------+---------+--------+----+---------+--------+----------------+---------------+---------------+--------------+--------|
+ | mutual | N=3 | p1 | 10636 | 16992 | 2368 | 22 | 7978 | 2220 | 0.2615949580 | 0.0743777510 | 0.1795910880 | 0.091549925 | 2220 |
+ | mutual | N=4 | p1 | 157184 | 266576 | 27600 | 24 | 118224 | 26682 | 5.4447735440 | 1.0114744670 | 4.1979780290 | 0.302474220 | 26682 |
+ | mutual | N=5 | p1 | 2130240 | 3751600 | 308800 | 26 | 1604356 | 303608 | 102.6024451740 | 16.5370636420 | 81.7407906190 | 4.890839340 | 303608 |
** Peer-to-Peer Protocol
@@ -898,10 +898,10 @@
#+CALL: bench(peer2peer_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-----------+---------------+-----------------+---------+----------+---------+----+------+----------------+---------------+---------------+--------------|
- | peer2peer | N=4,K=4,T=1.1 | b11,b12,b13,b14 | 131072 | 589825 | 65536 | 28 | 5186 | 4.4678272080 | 1.7100144590 | 2.6163745380 | 0.270053699 |
- | peer2peer | N=5,K=4,T=1.1 | b11,b12,b13,b14 | 2097152 | 11534337 | 1048576 | 47 | 9146 | 101.6835119460 | 36.8182229940 | 61.7547327180 | 3.363654870 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-----------+---------------+-----------------+---------+----------+---------+-----+------+------+---------------+---------------+---------------+--------------+------|
+ | peer2peer | N=4,K=4,T=1.1 | b11,b12,b13,b14 | 65536 | 524289 | 65536 | 143 | 2595 | 2595 | 4.1838889430 | 1.4857622000 | 2.6068418540 | 0.270712644 | NA |
+ | peer2peer | N=5,K=4,T=1.1 | b11,b12,b13,b14 | 1048576 | 10485761 | 1048576 | 416 | 4575 | 4575 | 92.9116019660 | 31.5700511360 | 59.0466742390 | 5.993993306 | NA |
** PEPA
@@ -944,11 +944,11 @@
#+CALL: bench(phil_original_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |---------------+--------+-----------+---------+---------+--------+----+--------+---------------+--------------+---------------+--------------|
- | phil_original | N=3 | p1 | 8596 | 11336 | 956 | 20 | 5716 | 0.1323389700 | 0.0540117720 | 0.0736364480 | 0.006022200 |
- | phil_original | N=4 | p1 | 106880 | 146096 | 9440 | 22 | 65687 | 2.4639530770 | 0.6871754240 | 1.6944727410 | 0.073798335 |
- | phil_original | N=5 | p1 | 1270596 | 1777128 | 93068 | 24 | 737938 | 41.0224361500 | 8.9896192460 | 30.2331595520 | 1.088851768 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |---------------+--------+-----------+--------+---------+--------+----+--------+-------+---------------+--------------+---------------+--------------+-------|
+ | phil_original | N=3 | p1 | 4298 | 7038 | 956 | 18 | 3476 | 956 | 0.0991513130 | 0.0285057980 | 0.0671398950 | 0.005910168 | 956 |
+ | phil_original | N=4 | p1 | 53440 | 92656 | 9440 | 20 | 42227 | 9440 | 1.7436439550 | 0.3729716410 | 1.3266761870 | 0.134535511 | 9440 |
+ | phil_original | N=5 | p1 | 635298 | 1141830 | 93068 | 22 | 494654 | 93068 | 27.6253272650 | 4.7922973930 | 21.9391580220 | 1.340808085 | 93068 |
*** No Fair
@@ -977,10 +977,10 @@
#+CALL: bench(phil_nofair_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-------------+---------+-----------+--------+--------+--------+----+-------+--------------+--------------+--------------+--------------|
- | phil_nofair | N=3,K=1 | p1 | 7300 | 9392 | 956 | 18 | 5245 | 0.1081048670 | 0.0498680450 | 0.0532069150 | 0.005267348 |
- | phil_nofair | N=4,K=1 | p1 | 89808 | 120488 | 9440 | 20 | 59877 | 1.9435177250 | 0.6136654360 | 1.2620874860 | 0.057043773 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-------------+---------+-----------+--------+-------+--------+----+-------+------+--------------+--------------+--------------+--------------+------|
+ | phil_nofair | N=3,K=1 | p1 | 3650 | 5742 | 956 | 16 | 3023 | 956 | 0.0814082860 | 0.0293376010 | 0.0499600120 | 0.005302261 | 956 |
+ | phil_nofair | N=4,K=1 | p1 | 44904 | 75584 | 9440 | 18 | 36509 | 9440 | 1.4168774340 | 0.3053214300 | 1.0686104900 | 0.131420308 | 9440 |
** Cyclic Server Polling
@@ -1011,16 +1011,16 @@
#+CALL: bench(poll_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-------+----------+-----------+--------+-------+--------+----+-------+--------------+--------------+--------------+--------------|
- | poll | N=2,T=50 | s | 24 | 34 | 12 | 7 | 24 | 0.0019461820 | 0.0014940950 | 0.0003399830 | 0.001432169 |
- | poll | N=3,T=50 | s | 72 | 120 | 36 | 10 | 72 | 0.0017074010 | 0.0011435970 | 0.0005032420 | 0.001505192 |
- | poll | N=4,T=50 | s | 192 | 368 | 96 | 13 | 192 | 0.0031334600 | 0.0022405420 | 0.0007880370 | 0.001481561 |
- | poll | N=5,T=50 | s | 480 | 1040 | 240 | 16 | 480 | 0.0073217160 | 0.0045210700 | 0.0025369050 | 0.002187779 |
- | poll | N=6,T=50 | s | 1152 | 2784 | 576 | 19 | 1152 | 0.0187852920 | 0.0100396800 | 0.0080074890 | 0.003221514 |
- | poll | N=7,T=50 | s | 2688 | 7168 | 1344 | 22 | 2688 | 0.0497332080 | 0.0245368360 | 0.0231752230 | 0.006416140 |
- | poll | N=8,T=50 | s | 6144 | 17920 | 3072 | 25 | 6144 | 0.1350377530 | 0.0573634460 | 0.0725547710 | 0.011949279 |
- | poll | N=9,T=50 | s | 13824 | 43776 | 6912 | 28 | 13824 | 0.3570237990 | 0.1413092260 | 0.1977489020 | 0.035072746 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-------+----------+-----------+--------+-------+--------+-----+------+------+--------------+--------------+--------------+--------------+------|
+ | poll | N=2,T=50 | s | 12 | 22 | 12 | 10 | 12 | 12 | 0.0008910090 | 0.0007066880 | 0.0001298040 | 0.001327407 | NA |
+ | poll | N=3,T=50 | s | 36 | 84 | 36 | 21 | 36 | 36 | 0.0012657850 | 0.0010364200 | 0.0001748600 | 0.001361599 | NA |
+ | poll | N=4,T=50 | s | 96 | 272 | 96 | 36 | 96 | 96 | 0.0023831820 | 0.0016814210 | 0.0006161430 | 0.001624606 | NA |
+ | poll | N=5,T=50 | s | 240 | 800 | 240 | 69 | 240 | 240 | 0.0051083390 | 0.0031624390 | 0.0015928920 | 0.001916775 | NA |
+ | poll | N=6,T=50 | s | 576 | 2208 | 576 | 78 | 576 | 576 | 0.0151479820 | 0.0071269240 | 0.0074199210 | 0.003032829 | NA |
+ | poll | N=7,T=50 | s | 1344 | 5824 | 1344 | 117 | 1344 | 1344 | 0.0467666580 | 0.0227359860 | 0.0226693750 | 0.134917099 | NA |
+ | poll | N=8,T=50 | s | 3072 | 14848 | 3072 | 136 | 3072 | 3072 | 0.1182813750 | 0.0424620610 | 0.0723774770 | 0.158348731 | NA |
+ | poll | N=9,T=50 | s | 6912 | 36864 | 6912 | 171 | 6912 | 6912 | 0.3183194150 | 0.1082939610 | 0.1957532170 | 0.173080736 | NA |
** Mutual Exclusion à la Rabin
@@ -1046,10 +1046,10 @@
#+CALL: bench(rabin_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-------+--------+-----------+---------+---------+--------+---+--------+----------------+---------------+---------------+--------------|
- | rabin | N=3 | p1 | 146804 | 256840 | 27766 | 8 | 22275 | 3.5765650560 | 1.1790803120 | 2.2444284600 | 0.115869639 |
- | rabin | N=4 | p1 | 3679144 | 6647796 | 668836 | 9 | 468698 | 137.7622148050 | 38.5853359130 | 94.1964029790 | 4.227659734 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-------+--------+-----------+---------+---------+--------+---+--------+--------+----------------+---------------+---------------+--------------+--------|
+ | rabin | N=3 | p1 | 73402 | 183438 | 27766 | 6 | 11348 | 6389 | 2.8423379660 | 0.6502151130 | 2.1266318030 | 0.129058069 | 6389 |
+ | rabin | N=4 | p1 | 1839572 | 4808224 | 668836 | 7 | 240744 | 126402 | 104.9218090710 | 19.3309383670 | 80.7231135260 | 4.480593622 | 126402 |
** Self Stabilisation
*** Beauquier
@@ -1076,11 +1076,11 @@
#+CALL: bench(beauquier_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-----------+-------------------+-----------+--------+-------+--------+---+-----+--------------+--------------+--------------+--------------|
- | beauquier | N=3,K=0,k=0 | d1,p1 | 320 | 400 | 64 | 9 | 304 | 0.0043127660 | 0.0027450860 | 0.0014498480 | 0.001494351 |
- | beauquier | N=3,K=0,k=1:2:3 | d1,p1 | 320 | 400 | 64 | 9 | 304 | 0.0042613870 | 0.0026900940 | 0.0014534710 | 0.001482036 |
- | beauquier | N=3,K=1:1:100,k=3 | d1,p1 | 320 | 400 | 64 | 9 | 304 | 0.0042725350 | 0.0027533610 | 0.0013997510 | 0.001556610 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-----------+-------------------+-----------+--------+-------+--------+---+-----+-----+--------------+--------------+--------------+--------------+------|
+ | beauquier | N=3,K=0,k=0 | d1,p1 | 160 | 240 | 64 | 7 | 156 | 64 | 0.0062942290 | 0.0031537420 | 0.0029998830 | 0.001448451 | 64 |
+ | beauquier | N=3,K=0,k=1:2:3 | d1,p1 | 160 | 240 | 64 | 7 | 156 | 64 | 0.0063430930 | 0.0035986510 | 0.0025616250 | 0.001343983 | 64 |
+ | beauquier | N=3,K=1:1:100,k=3 | d1,p1 | 160 | 240 | 64 | 7 | 156 | 64 | 0.0034279250 | 0.0021093160 | 0.0012242850 | 0.001436485 | 64 |
*** Herman
@@ -1106,11 +1106,11 @@
#+CALL: bench(herman_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |--------+-------------------+-----------+--------+-------+--------+---+----+--------------+--------------+--------------+--------------|
- | herman | N=3,K=0,k=0 | x1 | 16 | 36 | 8 | 3 | 15 | 0.0007419490 | 0.0005406320 | 0.0001626820 | 0.001368507 |
- | herman | N=3,K=0,k=1:2:7 | x1 | 16 | 36 | 8 | 3 | 15 | 0.0007305800 | 0.0005338040 | 0.0001589180 | 0.001337646 |
- | herman | N=3,K=1:1:100,k=0 | x1 | 16 | 36 | 8 | 3 | 15 | 0.0007522640 | 0.0005440680 | 0.0001678600 | 0.001259825 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |--------+-------------------+-----------+--------+-------+--------+---+---+-----+--------------+--------------+--------------+--------------+------|
+ | herman | N=3,K=0,k=0 | x1 | 8 | 28 | 8 | 2 | 8 | 8 | 0.0011958170 | 0.0009452440 | 0.0001836330 | 0.001307534 | NA |
+ | herman | N=3,K=0,k=1:2:7 | x1 | 8 | 28 | 8 | 2 | 8 | 8 | 0.0006995140 | 0.0005423030 | 0.0001221320 | 0.001344269 | NA |
+ | herman | N=3,K=1:1:100,k=0 | x1 | 8 | 28 | 8 | 2 | 8 | 8 | 0.0007458310 | 0.0005802510 | 0.0001284360 | 0.001369970 | NA |
*** Israeli and Jalfon
@@ -1136,11 +1136,11 @@
#+CALL: bench(ij_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |----------------+-------------------+-----------+--------+-------+--------+---+----+--------------+--------------+--------------+--------------|
- | israeli-jalfon | N=3,K=0,k=0 | q1 | 38 | 52 | 7 | 7 | 26 | 0.0010639840 | 0.0007484040 | 0.0002801020 | 0.001331625 |
- | israeli-jalfon | N=3,K=0,k=1:1:3 | q1 | 38 | 52 | 7 | 7 | 26 | 0.0011277800 | 0.0008020610 | 0.0002879750 | 0.001514973 |
- | israeli-jalfon | N=3,K=1:1:100,k=0 | q1 | 38 | 52 | 7 | 7 | 26 | 0.0011946810 | 0.0008500820 | 0.0003068540 | 0.001331800 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |----------------+-------------------+-----------+--------+-------+--------+---+----+-----+--------------+--------------+--------------+--------------+------|
+ | israeli-jalfon | N=3,K=0,k=0 | q1 | 19 | 33 | 7 | 5 | 14 | 5 | 0.0011091940 | 0.0008037810 | 0.0002497640 | 0.001330080 | 5 |
+ | israeli-jalfon | N=3,K=0,k=1:1:3 | q1 | 19 | 33 | 7 | 5 | 14 | 5 | 0.0009298120 | 0.0007077380 | 0.0001832360 | 0.001361262 | 5 |
+ | israeli-jalfon | N=3,K=1:1:100,k=0 | q1 | 19 | 33 | 7 | 5 | 14 | 5 | 0.0008726910 | 0.0006402390 | 0.0001894150 | 0.001430738 | 5 |
** Tandem Queueing Network
@@ -1170,15 +1170,15 @@
#+CALL: bench(tandem_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |--------+-----------+-----------+--------+--------+--------+-----+--------+--------------+--------------+--------------+--------------|
- | tandem | T=1,c=3 | sc | 56 | 99 | 28 | 13 | 56 | 0.0012627910 | 0.0010033670 | 0.0002041720 | 0.002930771 |
- | tandem | T=1,c=7 | sc | 240 | 483 | 120 | 17 | 240 | 0.0040184010 | 0.0027907440 | 0.0010636400 | 0.001692385 |
- | tandem | T=1,c=15 | sc | 992 | 2115 | 496 | 25 | 992 | 0.0146707330 | 0.0080388200 | 0.0058302650 | 0.002499379 |
- | tandem | T=1,c=31 | sc | 4032 | 8835 | 2016 | 41 | 4032 | 0.0643002630 | 0.0314884760 | 0.0288534760 | 0.005989609 |
- | tandem | T=1,c=63 | sc | 16256 | 36099 | 8128 | 73 | 16256 | 0.2938911520 | 0.1320939200 | 0.1458865470 | 0.021436435 |
- | tandem | T=1,c=127 | sc | 65280 | 145923 | 32640 | 137 | 65280 | 1.3598630290 | 0.5752202270 | 0.6970814290 | 0.090911982 |
- | tandem | T=1,c=255 | sc | 261632 | 586755 | 130816 | 265 | 261632 | 6.4663487130 | 2.3844438290 | 3.4512245100 | 0.422799297 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |--------+-----------+-----------+--------+--------+--------+------+--------+--------+--------------+--------------+--------------+--------------+------|
+ | tandem | T=1,c=3 | sc | 28 | 71 | 28 | 14 | 28 | 28 | 0.0017086680 | 0.0011059290 | 0.0005132400 | 0.001287729 | NA |
+ | tandem | T=1,c=7 | sc | 120 | 363 | 120 | 30 | 120 | 120 | 0.0028268260 | 0.0018785560 | 0.0008513960 | 0.001664509 | NA |
+ | tandem | T=1,c=15 | sc | 496 | 1619 | 496 | 62 | 496 | 496 | 0.0124606510 | 0.0054529810 | 0.0064661740 | 0.002466569 | NA |
+ | tandem | T=1,c=31 | sc | 2016 | 6819 | 2016 | 126 | 2016 | 2016 | 0.0544782370 | 0.0214374920 | 0.0294120970 | 0.146817774 | NA |
+ | tandem | T=1,c=63 | sc | 8128 | 27971 | 8128 | 254 | 8128 | 8128 | 0.2465705900 | 0.0939794700 | 0.1412541940 | 0.129191465 | NA |
+ | tandem | T=1,c=127 | sc | 32640 | 113283 | 32640 | 510 | 32640 | 32640 | 1.1397291790 | 0.3947242670 | 0.6921939540 | 0.167059434 | NA |
+ | tandem | T=1,c=255 | sc | 130816 | 455939 | 130816 | 1022 | 130816 | 130816 | 5.1715710130 | 1.7897675410 | 3.1015734600 | 0.433634037 | NA |
** WLAN
@@ -1216,16 +1216,16 @@
#+CALL: bench(wlan_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-------------------+------------------------------------+-----------+---------+---------+--------+----+---------+---------------+---------------+---------------+--------------|
- | wlan | TRANS_TIME_MAX=10,k=2,K=0 | c1,c2 | 130924 | 159608 | 28480 | 11 | 93978 | 2.5908570580 | 0.9249179730 | 1.5016590850 | 0.093078634 |
- | wlan | TRANS_TIME_MAX=10,k=2,K=1 | c1,c2 | 130924 | 159608 | 28480 | 11 | 93978 | 2.5753110480 | 0.9395872720 | 1.4612171740 | 0.088714052 |
- | wlan | TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 130924 | 159608 | 28480 | 11 | 93978 | 2.5341541370 | 0.9207595380 | 1.4575034320 | 0.081334169 |
- | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=0 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 2.5907287140 | 0.9454512560 | 1.4836718780 | 0.082597288 |
- | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 2.5355523980 | 0.9009553080 | 1.4735462300 | 0.081611174 |
- | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=3 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 2.5361680950 | 0.8973794470 | 1.4780346470 | 0.081681599 |
- | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=0 | c1,c2 | 1164654 | 1353415 | 248503 | 11 | 453477 | 26.3056340660 | 8.7312956210 | 15.5047473050 | 0.762718008 |
- | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 2817352 | 3372198 | 607727 | 11 | 1038591 | 69.8417826180 | 23.4097774980 | 42.1173267720 | 2.250720532 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-------------------+------------------------------------+-----------+---------+---------+--------+---+--------+--------+---------------+---------------+---------------+--------------+--------|
+ | wlan | TRANS_TIME_MAX=10,k=2,K=0 | c1,c2 | 65462 | 94146 | 28480 | 9 | 49602 | 21869 | 1.7558618230 | 0.4390517930 | 1.2454266760 | 0.126421844 | 21869 |
+ | wlan | TRANS_TIME_MAX=10,k=2,K=1 | c1,c2 | 65462 | 94146 | 28480 | 9 | 49602 | 21869 | 1.7543553850 | 0.4361156320 | 1.2482959920 | 0.158908273 | 21869 |
+ | wlan | TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 65462 | 94146 | 28480 | 9 | 49602 | 21869 | 1.7711672650 | 0.4566827060 | 1.2441302510 | 0.145084650 | 21869 |
+ | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=0 | c1,c2 | 65718 | 94452 | 28598 | 9 | 49602 | 21869 | 1.7843243230 | 0.4392616130 | 1.2723777120 | 0.162618919 | 21869 |
+ | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 65718 | 94452 | 28598 | 9 | 49602 | 21869 | 1.8235408620 | 0.4620862550 | 1.2886523420 | 0.150338646 | 21869 |
+ | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=3 | c1,c2 | 65718 | 94452 | 28598 | 9 | 49602 | 21869 | 1.8411782350 | 0.4359194410 | 1.3328821700 | 0.127593711 | 21869 |
+ | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=0 | c1,c2 | 582327 | 771088 | 248503 | 9 | 236170 | 107865 | 16.9908837680 | 4.3799129560 | 11.7960952010 | 0.944234783 | 107865 |
+ | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 1408676 | 1963522 | 607727 | 9 | 543056 | 243325 | 45.4369958910 | 11.4752167380 | 31.4161619510 | 2.489094019 | 243325 |
** Zeroconf
@@ -1266,9 +1266,9 @@
#+CALL: bench(zeroconf_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) | t_valmari(s) |
- |-----------------------+--------------------------------------+-----------+---------+---------+--------+------+--------+---------------+---------------+---------------+--------------|
- | zeroconf | N=1000,K=4,err=0,reset=true | n,n0,n1,b | 4886 | 5411 | 1088 | 17 | 2366 | 0.0613427780 | 0.0291644460 | 0.0299064440 | 0.003344225 |
- | zeroconf | N=1000,K=4,err=0,reset=false | n,n0,n1,b | 1753990 | 2158354 | 307768 | 1721 | 835101 | 41.5351746540 | 13.3675275650 | 25.7048396630 | 1.277922856 |
- | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=true | n,n0,n1,b | 19046 | 21515 | 4214 | 18 | 8602 | 0.2668741390 | 0.1188995240 | 0.1335954910 | 0.009975180 |
- | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=false | n,n0,n1,b | 74320 | 89012 | 14834 | 58 | 31671 | 1.3478339080 | 0.4705650060 | 0.8260892900 | 0.039518822 |
+ | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | Q_0 | t(s) | t_p(s) | t_r(s) | t_valmari(s) | Q_0v |
+ |-----------------------+--------------------------------------+-----------+--------+---------+--------+------+--------+--------+---------------+--------------+---------------+--------------+--------|
+ | zeroconf | N=1000,K=4,err=0,reset=true | n,n0,n1,b | 2443 | 2968 | 1088 | 15 | 1201 | 578 | 0.0525785820 | 0.0204689620 | 0.0305502270 | 0.003272353 | 578 |
+ | zeroconf | N=1000,K=4,err=0,reset=false | n,n0,n1,b | 876995 | 1281359 | 307768 | 1722 | 435504 | 194290 | 28.1256166850 | 6.4696528370 | 20.3058384180 | 1.585585508 | 194290 |
+ | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=true | n,n0,n1,b | 9523 | 11992 | 4214 | 16 | 4375 | 2102 | 0.1846794510 | 0.0557492630 | 0.1222555780 | 0.117496914 | 2102 |
+ | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=false | n,n0,n1,b | 37160 | 51852 | 14834 | 59 | 16412 | 7525 | 0.9179981490 | 0.2309559160 | 0.6545364810 | 0.114226051 | 7525 |
--
GitLab