diff --git a/prism/benchmark.org b/prism/benchmark.org
index c04c8276dcc5f3ef5ad63dcd40a92743dbc28bf6..fb5b32b7513d3cd50de24bbf018d5c7810d98142 100644
--- a/prism/benchmark.org
+++ b/prism/benchmark.org
@@ -317,18 +317,18 @@
#+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.0209471710 | 0.0109136510 | 0.0089981610 | 0.006649120 |
- | brp | N=16,MAX=3 | s | 1772 | 2041 | 886 | 8 | 882 | 0.0252625480 | 0.0122350360 | 0.0117073170 | 0.002275683 |
- | brp | N=16,MAX=4 | s | 2190 | 2538 | 1095 | 8 | 1108 | 0.0331651640 | 0.0147558910 | 0.0169914490 | 0.002458023 |
- | brp | N=16,MAX=5 | s | 2608 | 3035 | 1304 | 8 | 1334 | 0.0394003400 | 0.0172755360 | 0.0203174490 | 0.002799933 |
- | brp | N=32,MAX=2 | s | 2698 | 3080 | 1349 | 8 | 1296 | 0.0385593240 | 0.0173279330 | 0.0194001910 | 0.002730327 |
- | brp | N=32,MAX=3 | s | 3532 | 4073 | 1766 | 8 | 1746 | 0.0536884640 | 0.0236442470 | 0.0276964150 | 0.003012713 |
- | brp | N=32,MAX=4 | s | 4366 | 5066 | 2183 | 8 | 2196 | 0.0688614540 | 0.0287028950 | 0.0359902280 | 0.003636557 |
- | brp | N=32,MAX=5 | s | 5200 | 6059 | 2600 | 8 | 2646 | 0.0847238970 | 0.0340716350 | 0.0469580390 | 0.003855771 |
- | brp | N=64,MAX=2 | s | 5386 | 6152 | 2693 | 8 | 2576 | 0.0843203740 | 0.0371186270 | 0.0434485360 | 0.003914304 |
- | brp | N=64,MAX=3 | s | 7052 | 8137 | 3526 | 8 | 3474 | 0.1168573180 | 0.0469792130 | 0.0644946360 | 0.004994134 |
- | brp | N=64,MAX=4 | s | 8718 | 10122 | 4359 | 8 | 4372 | 0.1513234340 | 0.0619705450 | 0.0821466690 | 0.005656848 |
- | brp | N=64,MAX=5 | s | 10384 | 12107 | 5192 | 8 | 5270 | 0.1860097840 | 0.0732258280 | 0.1010794740 | 0.006818691 |
+ | brp | N=16,MAX=2 | s | 1354 | 1544 | 677 | 8 | 656 | 0.0183133300 | 0.0092632460 | 0.0079876340 | 0.001792663 |
+ | brp | N=16,MAX=3 | s | 1772 | 2041 | 886 | 8 | 882 | 0.0243576450 | 0.0119258980 | 0.0111986140 | 0.001850050 |
+ | brp | N=16,MAX=4 | s | 2190 | 2538 | 1095 | 8 | 1108 | 0.0313129310 | 0.0144067960 | 0.0154558590 | 0.002142605 |
+ | brp | N=16,MAX=5 | s | 2608 | 3035 | 1304 | 8 | 1334 | 0.0375906170 | 0.0167921660 | 0.0189525830 | 0.002220575 |
+ | brp | N=32,MAX=2 | s | 2698 | 3080 | 1349 | 8 | 1296 | 0.0373192340 | 0.0171126520 | 0.0184061540 | 0.002197632 |
+ | brp | N=32,MAX=3 | s | 3532 | 4073 | 1766 | 8 | 1746 | 0.0516883770 | 0.0236099000 | 0.0256985430 | 0.002611655 |
+ | brp | N=32,MAX=4 | s | 4366 | 5066 | 2183 | 8 | 2196 | 0.0657188100 | 0.0281658170 | 0.0332676790 | 0.003020667 |
+ | brp | N=32,MAX=5 | s | 5200 | 6059 | 2600 | 8 | 2646 | 0.0816464140 | 0.0340161270 | 0.0439713900 | 0.003469654 |
+ | brp | N=64,MAX=2 | s | 5386 | 6152 | 2693 | 8 | 2576 | 0.0823123470 | 0.0384094550 | 0.0402949210 | 0.003361480 |
+ | brp | N=64,MAX=3 | s | 7052 | 8137 | 3526 | 8 | 3474 | 0.1110061720 | 0.0469526190 | 0.0573023420 | 0.004222313 |
+ | brp | N=64,MAX=4 | s | 8718 | 10122 | 4359 | 8 | 4372 | 0.1437197910 | 0.0614879240 | 0.0752228540 | 0.005252320 |
+ | brp | N=64,MAX=5 | s | 10384 | 12107 | 5192 | 8 | 5270 | 0.1794982180 | 0.0725116000 | 0.0971481640 | 0.007470188 |
** Cell in Wireless Communication Network
@@ -360,12 +360,12 @@
#+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.0021642010 | 0.0014539950 | 0.0005021480 | 0.001334944 |
- | cell | N=100,T=0.5 | | 101 | 200 | 101 | 80 | 101 | 0.0018238190 | 0.0012902030 | 0.0004346450 | 0.001246251 |
- | cell | N=200,T=0.5 | | 201 | 400 | 201 | 160 | 201 | 0.0035392020 | 0.0020553230 | 0.0011315590 | 0.001409519 |
- | cell | N=300,T=0.5 | | 301 | 600 | 301 | 251 | 301 | 0.0040798850 | 0.0021953880 | 0.0014557430 | 0.001672196 |
- | cell | N=400,T=0.5 | | 401 | 800 | 401 | 351 | 401 | 0.0055519490 | 0.0027788330 | 0.0022509930 | 0.001700592 |
- | cell | N=500,T=0.5 | | 501 | 1000 | 501 | 451 | 501 | 0.0067999180 | 0.0031769950 | 0.0031048610 | 0.001887522 |
+ | cell | N=50,T=0.5 | | 51 | 100 | 51 | 50 | 51 | 0.0022477340 | 0.0019795950 | 0.0002019030 | 0.001323342 |
+ | cell | N=100,T=0.5 | | 101 | 200 | 101 | 80 | 101 | 0.0017503490 | 0.0012527050 | 0.0004084810 | 0.001249333 |
+ | cell | N=200,T=0.5 | | 201 | 400 | 201 | 160 | 201 | 0.0028871450 | 0.0016577010 | 0.0009160370 | 0.001583382 |
+ | cell | N=300,T=0.5 | | 301 | 600 | 301 | 251 | 301 | 0.0047677180 | 0.0025690420 | 0.0017346540 | 0.001463552 |
+ | cell | N=400,T=0.5 | | 401 | 800 | 401 | 351 | 401 | 0.0051696770 | 0.0025671370 | 0.0021485320 | 0.001644939 |
+ | cell | N=500,T=0.5 | | 501 | 1000 | 501 | 451 | 501 | 0.0066253380 | 0.0030976190 | 0.0030231570 | 0.001800980 |
** Dependable Cluster
@@ -392,10 +392,10 @@
#+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.0298355070 | 0.0137886450 | 0.0147249310 | 0.003478562 |
- | cluster | N=8,T=10 | | 2772 | 12832 | 2772 | 359 | 1917 | 0.0771862720 | 0.0289588370 | 0.0453627970 | 0.008524262 |
- | cluster | N=16,T=10 | | 10132 | 48160 | 10132 | 711 | 7021 | 0.3393682110 | 0.1169745870 | 0.2039435530 | 0.028898241 |
- | cluster | N=32,T=10 | | 38676 | 186400 | 38676 | 1415 | 26829 | 1.5058713060 | 0.4423846110 | 0.9681181190 | 0.120831798 |
+ | cluster | N=4,T=10 | | 820 | 3616 | 820 | 183 | 565 | 0.0180744720 | 0.0083440860 | 0.0089631280 | 0.003003539 |
+ | cluster | N=8,T=10 | | 2772 | 12832 | 2772 | 359 | 1917 | 0.0731653190 | 0.0285537050 | 0.0418818060 | 0.008190769 |
+ | cluster | N=16,T=10 | | 10132 | 48160 | 10132 | 711 | 7021 | 0.3334633290 | 0.1280169100 | 0.1875908420 | 0.028032154 |
+ | cluster | N=32,T=10 | | 38676 | 186400 | 38676 | 1415 | 26829 | 1.4261153720 | 0.4447910060 | 0.8843633530 | 0.111768512 |
** Shared coin protocol
@@ -421,10 +421,10 @@
#+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.0339243940 | 0.0214042700 | 0.0115632400 | 0.001936125 |
- | coin | N=2,K=4,k=10 | pc1,pc2 | 2624 | 3068 | 528 | 20 | 837 | 0.0463473050 | 0.0192713280 | 0.0249119270 | 0.002223486 |
- | coin | N=4,K=2,k=10 | pc1,pc2,pc3,pc4 | 166400 | 218976 | 22656 | 262 | 32860 | 4.3544310730 | 1.2713094710 | 2.9420338860 | 0.085424693 |
- | coin | N=4,K=4,k=10 | pc1,pc2,pc3,pc4 | 317952 | 419168 | 43136 | 262 | 63132 | 8.9700246590 | 2.4618423730 | 6.1038354910 | 0.172734327 |
+ | coin | N=2,K=2,k=10 | pc1,pc2 | 1344 | 1564 | 272 | 20 | 437 | 0.0187914620 | 0.0095398820 | 0.0084577910 | 0.001658171 |
+ | coin | N=2,K=4,k=10 | pc1,pc2 | 2624 | 3068 | 528 | 20 | 837 | 0.0362636050 | 0.0169234580 | 0.0178993270 | 0.002125689 |
+ | coin | N=4,K=2,k=10 | pc1,pc2,pc3,pc4 | 166400 | 218976 | 22656 | 262 | 32860 | 4.0529223640 | 1.2194434780 | 2.6965525900 | 0.081762443 |
+ | coin | N=4,K=4,k=10 | pc1,pc2,pc3,pc4 | 317952 | 419168 | 43136 | 262 | 63132 | 8.2925207780 | 2.3246470810 | 5.6623134960 | 0.166132778 |
** IEEE 802.3 CSMA/CD
@@ -461,11 +461,11 @@
#+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.0602827340 | 0.0296438270 | 0.0281856590 | 0.002571237 |
- | csma | N=2,K=4,k=1 | b | 31892 | 34528 | 7958 | 7 | 3955 | 0.5849368540 | 0.2199502260 | 0.3424232290 | 0.012771149 |
- | csma | N=2,K=6,k=1 | b | 267012 | 293366 | 66718 | 7 | 29575 | 6.6575342930 | 2.0369849420 | 4.3851872190 | 0.117619760 |
- | csma | N=3,K=2,k=1 | b | 150612 | 169624 | 36850 | 8 | 9228 | 3.7054166030 | 1.1050377620 | 2.3561547370 | 0.066355949 |
- | csma | N=4,K=2,k=1 | b | 3174932 | 3740038 | 761962 | 9 | 40920 | 125.8473542140 | 27.9143180180 | 93.7581910370 | 2.140339554 |
+ | csma | N=2,K=2,k=1 | b | 4184 | 4428 | 1038 | 7 | 929 | 0.0590345420 | 0.0275238560 | 0.0285269050 | 0.003041325 |
+ | csma | N=2,K=4,k=1 | b | 31892 | 34528 | 7958 | 7 | 3955 | 0.5513215750 | 0.2182946040 | 0.3110718450 | 0.013088990 |
+ | csma | N=2,K=6,k=1 | b | 267012 | 293366 | 66718 | 7 | 29575 | 6.4105550390 | 2.0424979310 | 4.1367185850 | 0.114354010 |
+ | csma | N=3,K=2,k=1 | b | 150612 | 169624 | 36850 | 8 | 9228 | 3.4994987360 | 1.0762552140 | 2.2180639160 | 0.070182370 |
+ | csma | N=4,K=2,k=1 | b | 3174932 | 3740038 | 761962 | 9 | 40920 | 122.1610020800 | 27.7070354320 | 90.3269129300 | 2.015700499 |
** Dice
@@ -488,11 +488,11 @@
#+CALL: bench(dice_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |----------------+--------+-----------+--------+-------+--------+----+-----+--------------+--------------+--------------|
- | dice | | s | 26 | 33 | 13 | 9 | 14 | 0.0016484700 | 0.0011912350 | 0.0002981260 |
- | two_dice_knuth | | s | 90 | 124 | 45 | 36 | 65 | 0.0021550940 | 0.0014570120 | 0.0006210930 |
- | two_dice | | s1,s2 | 592 | 859 | 169 | 66 | 219 | 0.0083296110 | 0.0050421710 | 0.0028305310 |
+ | 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.0010307540 | 0.0007646180 | 0.0002069160 | 0.001233874 |
+ | two_dice_knuth | | s | 90 | 124 | 45 | 36 | 65 | 0.0017446450 | 0.0011966390 | 0.0004856540 | 0.001231817 |
+ | two_dice | | s1,s2 | 846 | 1113 | 169 | 68 | 316 | 0.0111417980 | 0.0062019170 | 0.0045367490 | 0.001477305 |
** Dining cryptographers
@@ -518,13 +518,13 @@
#+CALL: bench(dining_crypt_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |--------------+--------+-----------+---------+---------+--------+----+----+---------------+---------------+---------------|
- | dining_crypt | N=3 | pay | 1380 | 1776 | 380 | 6 | 12 | 0.0153172760 | 0.0088847950 | 0.0053601590 |
- | dining_crypt | N=4 | pay | 8870 | 12425 | 2165 | 7 | 15 | 0.1058157520 | 0.0529153980 | 0.0488769000 |
- | dining_crypt | N=5 | pay | 54402 | 81324 | 11850 | 8 | 18 | 0.7616123600 | 0.3444833190 | 0.3900184430 |
- | dining_crypt | N=6 | pay | 321412 | 505169 | 63063 | 9 | 21 | 5.2171843840 | 2.0977846730 | 2.9244043600 |
- | dining_crypt | N=7 | pay | 1843560 | 3014272 | 328760 | 10 | 24 | 34.4449497800 | 14.1470112620 | 18.6133679620 |
+ | 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.0314529840 | 0.0191453090 | 0.0115205890 | 0.001822338 |
+ | dining_crypt | N=4 | pay | 13410 | 16965 | 2165 | 11 | 560 | 0.2175989640 | 0.0887223510 | 0.1192107970 | 0.006365550 |
+ | dining_crypt | N=5 | pay | 85104 | 112026 | 11850 | 13 | 1644 | 1.7626679680 | 0.6177125750 | 1.0966332670 | 0.037148995 |
+ | dining_crypt | N=6 | pay | 516698 | 700455 | 63063 | 15 | 4445 | 13.4243863920 | 4.0465883800 | 8.9197053750 | 0.252640876 |
+ | dining_crypt | N=7 | pay | 3029600 | 4200312 | 328760 | 17 | 11384 | 98.6312487290 | 26.6158940420 | 68.9829766530 | 1.742945521 |
** Embedded Control System
@@ -549,11 +549,11 @@
#+CALL: bench(embedded_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |----------+------------------+-----------+--------+-------+--------+----+-----+--------------+--------------+--------------|
- | embedded | MAX_COUNT=2,T=12 | i,a,m | 6956 | 18117 | 3478 | 86 | 252 | 0.1597876630 | 0.0882146950 | 0.0666840940 |
- | embedded | MAX_COUNT=2,T=14 | i,a,m | 6956 | 18117 | 3478 | 86 | 252 | 0.1467784660 | 0.0768221550 | 0.0649901140 |
- | embedded | MAX_COUNT=2,T=0 | i,a,m | 6956 | 18117 | 3478 | 86 | 252 | 0.1478352640 | 0.0783775910 | 0.0642371660 |
+ | 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.1336741270 | 0.0696774430 | 0.0594917330 | 0.014908269 |
+ | embedded | MAX_COUNT=2,T=14 | i,a,m | 6956 | 18117 | 3478 | 86 | 252 | 0.1356532430 | 0.0692266260 | 0.0619485030 | 0.012515015 |
+ | embedded | MAX_COUNT=2,T=0 | i,a,m | 6956 | 18117 | 3478 | 86 | 252 | 0.1340020400 | 0.0693893040 | 0.0597453450 | 0.013081782 |
** Firewire
@@ -606,22 +606,22 @@
#+CALL: bench(firewire_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |------------------------+--------------------------------+-----------+---------+---------+--------+----+--------+---------------+---------------+---------------|
- | firewire_abst_firewire | delay=36,fast=0.5 | s | 2741 | 3376 | 776 | 12 | 2395 | 0.0400200150 | 0.0170720860 | 0.0211536940 |
- | firewire_abst_firewire | delay=3,fast=0.2:0.1:0.8 | s | 1916 | 2023 | 611 | 12 | 1834 | 0.0243190000 | 0.0107229900 | 0.0123831130 |
- | firewire_abst_firewire | delay=36,fast=0.2:0.1:0.8 | s | 2741 | 3376 | 776 | 12 | 2395 | 0.0364160240 | 0.0158612050 | 0.0188617520 |
- | firewire_abst_deadline | deadline=200,delay=36,fast=0.5 | s | 231658 | 277151 | 67901 | 14 | 50971 | 6.0609084650 | 1.6574448420 | 4.0756830210 |
- | firewire_abst_deadline | deadline=300,delay=36,fast=0.5 | s | 494775 | 600858 | 142810 | 14 | 200178 | 15.3814060200 | 3.6826875570 | 10.8453653930 |
- | firewire_abst_deadline | deadline=400,delay=36,fast=0.5 | s | 768875 | 938458 | 220410 | 14 | 338252 | 24.7165903490 | 5.6468136230 | 17.4982826390 |
- | firewire_abst_deadline | deadline=500,delay=36,fast=0.5 | s | 1042975 | 1276058 | 298010 | 14 | 477052 | 34.5024083260 | 7.8380005630 | 24.9620457700 |
- | firewire_abst_deadline | deadline=600,delay=36,fast=0.5 | s | 1317075 | 1613658 | 375610 | 14 | 615852 | 45.7841402450 | 10.0617716280 | 32.7564691280 |
- | firewire_impl_firewire | delay=36,fast=0.5 | w12 | 903292 | 1172816 | 212268 | 7 | 84610 | 22.0220703270 | 6.3157471460 | 14.7304647880 |
- | firewire_impl_firewire | delay=3,fast=0.2:0.1:0.8 | w12 | 13705 | 15197 | 4093 | 7 | 6655 | 0.2110766570 | 0.0787999810 | 0.1183021730 |
- | firewire_impl_firewire | delay=36,fast=0.2:0.1:0.8 | w12 | 903292 | 1172816 | 212268 | 7 | 84610 | 22.1216038000 | 6.3432839570 | 14.7966602820 |
- | firewire_impl_deadline | deadline=200,delay=3,fast=0.5 | w12 | 272996 | 305258 | 80980 | 7 | 4177 | 4.7822075860 | 1.9395076380 | 2.5534351410 |
- | firewire_impl_deadline | deadline=300,delay=3,fast=0.5 | w12 | 711372 | 785821 | 213805 | 7 | 9995 | 13.2433108170 | 5.1315177230 | 7.4526110860 |
- | firewire_impl_deadline | deadline=400,delay=3,fast=0.5 | w12 | 1454775 | 1615298 | 434364 | 7 | 274660 | 34.4772238450 | 11.5118957670 | 21.0848007870 |
+ | 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.0579999360 | 0.0271281610 | 0.0287710190 | 0.011204047 |
+ | firewire_abst_firewire | delay=3,fast=0.2:0.1:0.8 | s | 2610 | 2717 | 611 | 15 | 2450 | 0.0472103650 | 0.0289406500 | 0.0168504270 | 0.002085152 |
+ | firewire_abst_firewire | delay=36,fast=0.2:0.1:0.8 | s | 3930 | 4565 | 776 | 15 | 3242 | 0.0559295240 | 0.0250629500 | 0.0288093630 | 0.002754361 |
+ | firewire_abst_deadline | deadline=200,delay=36,fast=0.5 | s | 327514 | 373007 | 67901 | 17 | 70383 | 9.0142473660 | 2.4680325980 | 6.1962958260 | 0.153781242 |
+ | firewire_abst_deadline | deadline=300,delay=36,fast=0.5 | s | 703930 | 810013 | 142810 | 17 | 273380 | 23.0224128500 | 5.3580252330 | 16.7521692850 | 0.386279360 |
+ | firewire_abst_deadline | deadline=400,delay=36,fast=0.5 | s | 1096930 | 1266513 | 220410 | 17 | 462758 | 37.6847522260 | 8.9898217490 | 27.1851377640 | 0.647646772 |
+ | firewire_abst_deadline | deadline=500,delay=36,fast=0.5 | s | 1489930 | 1723013 | 298010 | 17 | 653158 | 54.0867657590 | 12.3207361000 | 39.2348787200 | 0.944053400 |
+ | firewire_abst_deadline | deadline=600,delay=36,fast=0.5 | s | 1882930 | 2179513 | 375610 | 17 | 843558 | 71.4298740200 | 15.2939004910 | 53.0560072200 | 1.261069111 |
+ | firewire_impl_firewire | delay=36,fast=0.5 | w12 | 1382048 | 1651572 | 212268 | 10 | 256615 | 52.8282913640 | 11.0253984760 | 40.0544668250 | 0.876643644 |
+ | firewire_impl_firewire | delay=3,fast=0.2:0.1:0.8 | w12 | 19224 | 20716 | 4093 | 10 | 14581 | 0.3451744890 | 0.1221639930 | 0.2040304100 | 0.009281872 |
+ | firewire_impl_firewire | delay=36,fast=0.2:0.1:0.8 | w12 | 1382048 | 1651572 | 212268 | 10 | 256615 | 52.4441538770 | 11.0734458920 | 39.6245554390 | 0.894532432 |
+ | firewire_impl_deadline | deadline=200,delay=3,fast=0.5 | w12 | 384032 | 416294 | 80980 | 10 | 7925 | 7.5816849800 | 2.7938790310 | 4.5255920420 | 0.143469737 |
+ | firewire_impl_deadline | deadline=300,delay=3,fast=0.5 | w12 | 995134 | 1069583 | 213805 | 10 | 20640 | 21.0841092730 | 7.5240407240 | 12.7609830580 | 0.378357072 |
+ | firewire_impl_deadline | deadline=400,delay=3,fast=0.5 | w12 | 2040822 | 2201345 | 434364 | 10 | 475841 | 55.6618204630 | 16.7032022820 | 35.9431579500 | 0.956656650 |
** Flexible Manufacturing System
@@ -653,12 +653,12 @@
#+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.0016172580 | 0.0009751920 | 0.0005817690 | 0.001626313 |
- | fms | n=2 | | 810 | 3699 | 810 | 95 | 810 | 0.0255112160 | 0.0109938140 | 0.0133385900 | 0.007168435 |
- | fms | n=3 | | 6520 | 37394 | 6520 | 190 | 6520 | 0.2578682270 | 0.0833142500 | 0.1654538930 | 0.029443027 |
- | fms | n=4 | | 35910 | 237120 | 35910 | 294 | 35910 | 2.0737475910 | 0.5302708630 | 1.4814953620 | 0.207214683 |
- | fms | n=5 | | 152712 | 1111482 | 152712 | 372 | 152712 | 12.2113344620 | 2.6751175980 | 9.1517017740 | 1.184234896 |
- | fms | n=6 | | 537768 | 4205670 | 537768 | 463 | 537768 | 58.2827804620 | 10.6812993050 | 46.0490840600 | 5.357078578 |
+ | fms | n=1 | | 54 | 155 | 54 | 25 | 54 | 0.0018388410 | 0.0011281700 | 0.0006364540 | 0.001331149 |
+ | fms | n=2 | | 810 | 3699 | 810 | 95 | 810 | 0.0189576580 | 0.0086152180 | 0.0094450250 | 0.003700103 |
+ | fms | n=3 | | 6520 | 37394 | 6520 | 190 | 6520 | 0.2424664760 | 0.0814315050 | 0.1519773050 | 0.029144594 |
+ | fms | n=4 | | 35910 | 237120 | 35910 | 294 | 35910 | 1.9962497200 | 0.5290105340 | 1.4053248650 | 0.208487425 |
+ | fms | n=5 | | 152712 | 1111482 | 152712 | 372 | 152712 | 11.8417753190 | 2.7031185630 | 8.7519919900 | 1.171795304 |
+ | fms | n=6 | | 537768 | 4205670 | 537768 | 463 | 537768 | 57.6012079970 | 10.8508265430 | 45.1490399340 | 5.377844887 |
** Kanban
@@ -685,12 +685,12 @@
#+CALL: bench(kanban_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |--------+--------+-----------+--------+---------+--------+----+--------+---------------+---------------+---------------|
- | kanban | t=1 | | 160 | 616 | 160 | 43 | 160 | 0.0038241550 | 0.0022976810 | 0.0011723410 |
- | kanban | t=2 | | 4600 | 28120 | 4600 | 69 | 4600 | 0.1939290190 | 0.0662153880 | 0.1213312170 |
- | kanban | t=3 | | 58400 | 446400 | 58400 | 81 | 58400 | 4.1984053510 | 1.0111610700 | 3.0113522950 |
- | kanban | t=4 | | 454475 | 3979850 | 454475 | 86 | 454475 | 55.0179689960 | 10.4678318240 | 43.1391815640 |
+ | 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.0044386240 | 0.0030013010 | 0.0011616660 | 0.005158281 |
+ | kanban | t=2 | | 4600 | 28120 | 4600 | 69 | 4600 | 0.1933343360 | 0.0870241410 | 0.1009879730 | 0.019504319 |
+ | kanban | t=3 | | 58400 | 446400 | 58400 | 81 | 58400 | 3.9628291280 | 0.9679641260 | 2.8235876360 | 0.350080315 |
+ | kanban | t=4 | | 454475 | 3979850 | 454475 | 86 | 454475 | 53.2478343070 | 9.9061929120 | 41.7320138340 | 4.818514479 |
** Leader Election Protocol
*** Synchronous
@@ -723,17 +723,17 @@
#+CALL: bench(leader_sync_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |-------------+-------------+----------------+--------+-------+--------+---+----+--------------+--------------+--------------|
- | leader_sync | N=3,K=2,L=1 | s1,s2,s3 | 52 | 59 | 26 | 5 | 15 | 0.0012764570 | 0.0010496700 | 0.0001667540 |
- | leader_sync | N=3,K=3,L=1 | s1,s2,s3 | 138 | 164 | 69 | 5 | 15 | 0.0023056190 | 0.0018347410 | 0.0003922980 |
- | leader_sync | N=3,K=4,L=1 | s1,s2,s3 | 294 | 357 | 147 | 5 | 15 | 0.0043560690 | 0.0032755700 | 0.0008732080 |
- | leader_sync | N=4,K=2,L=1 | s1,s2,s3,s4 | 122 | 137 | 61 | 5 | 19 | 0.0030223000 | 0.0023280180 | 0.0005875820 |
- | leader_sync | N=4,K=3,L=1 | s1,s2,s3,s4 | 548 | 628 | 274 | 5 | 19 | 0.0092924760 | 0.0062377630 | 0.0024198320 |
- | leader_sync | N=4,K=4,L=1 | s1,s2,s3,s4 | 1624 | 1879 | 812 | 5 | 19 | 0.0267283050 | 0.0180728780 | 0.0077927720 |
- | leader_sync | N=5,K=2,L=1 | s1,s2,s3,s4,s5 | 282 | 313 | 141 | 5 | 23 | 0.0038073070 | 0.0027439500 | 0.0008015410 |
- | leader_sync | N=5,K=3,L=1 | s1,s2,s3,s4,s5 | 2100 | 2342 | 1050 | 5 | 23 | 0.0292099160 | 0.0159751390 | 0.0119459140 |
- | leader_sync | N=5,K=4,L=1 | s1,s2,s3,s4,s5 | 8488 | 9511 | 4244 | 5 | 23 | 0.1251914660 | 0.0672167660 | 0.0509999760 |
+ | 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.0014491610 | 0.0011924370 | 0.0001978790 | 0.001249239 |
+ | leader_sync | N=3,K=3,L=1 | s1,s2,s3 | 138 | 164 | 69 | 5 | 15 | 0.0021808050 | 0.0017449240 | 0.0003662710 | 0.001184258 |
+ | leader_sync | N=3,K=4,L=1 | s1,s2,s3 | 294 | 357 | 147 | 5 | 15 | 0.0034145700 | 0.0025598250 | 0.0006941640 | 0.001203805 |
+ | leader_sync | N=4,K=2,L=1 | s1,s2,s3,s4 | 122 | 137 | 61 | 5 | 19 | 0.0020448290 | 0.0016326540 | 0.0003468450 | 0.001137715 |
+ | leader_sync | N=4,K=3,L=1 | s1,s2,s3,s4 | 548 | 628 | 274 | 5 | 19 | 0.0064604680 | 0.0042010710 | 0.0018186710 | 0.001334541 |
+ | leader_sync | N=4,K=4,L=1 | s1,s2,s3,s4 | 1624 | 1879 | 812 | 5 | 19 | 0.0178802010 | 0.0111407990 | 0.0055881800 | 0.001719789 |
+ | leader_sync | N=5,K=2,L=1 | s1,s2,s3,s4,s5 | 282 | 313 | 141 | 5 | 23 | 0.0033693180 | 0.0024438400 | 0.0008086740 | 0.001194328 |
+ | leader_sync | N=5,K=3,L=1 | s1,s2,s3,s4,s5 | 2100 | 2342 | 1050 | 5 | 23 | 0.0235098410 | 0.0137206270 | 0.0087004380 | 0.001759321 |
+ | leader_sync | N=5,K=4,L=1 | s1,s2,s3,s4,s5 | 8488 | 9511 | 4244 | 5 | 23 | 0.1060566650 | 0.0566382730 | 0.0443777300 | 0.003793547 |
*** Asynchronous
@@ -759,11 +759,11 @@
#+CALL: bench(leader_async_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |--------------+---------+----------------+--------+--------+--------+-----+-------+--------------+--------------+--------------|
- | leader_async | N=3,K=1 | s1,s2,s3 | 1301 | 1591 | 364 | 56 | 518 | 0.0189675940 | 0.0097637420 | 0.0082665460 |
- | leader_async | N=4,K=1 | s1,s2,s3,s4 | 12596 | 16568 | 3172 | 219 | 3806 | 0.2122865030 | 0.0845087690 | 0.1184230530 |
- | leader_async | N=5,K=1 | s1,s2,s3,s4,s5 | 119583 | 166649 | 27299 | 865 | 27078 | 2.4961700310 | 0.7827652300 | 1.5614750140 |
+ | 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.0279369680 | 0.0130574680 | 0.0135397320 | 0.004130764 |
+ | leader_async | N=4,K=1 | s1,s2,s3,s4 | 18848 | 22820 | 3172 | 223 | 5611 | 0.3436595770 | 0.1287078690 | 0.2020437960 | 0.008791839 |
+ | leader_async | N=5,K=1 | s1,s2,s3,s4,s5 | 184568 | 231634 | 27299 | 870 | 41756 | 4.4770659000 | 1.3426453580 | 2.9605343650 | 0.088709806 |
** Molecules
@@ -802,17 +802,17 @@
#+CALL: bench(molecules_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |-------+---------------------------------------+-----------+--------+-------+--------+----+-----+--------------+--------------+--------------|
- | nacl | N1=10,N2=10,T=0:0.001:0.006,i=4 | na | 22 | 31 | 11 | 22 | 22 | 0.0012944150 | 0.0009634090 | 0.0002411550 |
- | nacl | N1=10,N2=10,T=0:0.001:0.006,i=0 | na | 22 | 31 | 11 | 22 | 22 | 0.0012162310 | 0.0008826650 | 0.0002477660 |
- | nacl | N1=10,N2=10,T=0,i=0 | na | 22 | 31 | 11 | 22 | 22 | 0.0012494110 | 0.0009169500 | 0.0002407770 |
- | knacl | N1=10,N2=10,N3=10,T=0:0.001:0.006,i=4 | na | 132 | 286 | 66 | 76 | 132 | 0.0042323030 | 0.0030404590 | 0.0010718420 |
- | knacl | N1=10,N2=10,N3=10,T=0:0.001:0.006,i=0 | na | 132 | 286 | 66 | 76 | 132 | 0.0042242410 | 0.0029981130 | 0.0010970890 |
- | knacl | N1=10,N2=10,N3=10,T=0,i=0 | na | 132 | 286 | 66 | 76 | 132 | 0.0042726040 | 0.0030445160 | 0.0010900700 |
- | mc | N1=10,N2=10,T=0:0.001:0.006,i=4 | mg | 72 | 146 | 36 | 47 | 72 | 0.0023568160 | 0.0015494180 | 0.0007299610 |
- | mc | N1=10,N2=10,T=0:0.001:0.006,i=0 | mg | 72 | 146 | 36 | 47 | 72 | 0.0020013230 | 0.0013408520 | 0.0005908430 |
- | mc | N1=10,N2=10,T=0i=0 | mg | 72 | 146 | 36 | 47 | 72 | 0.0018785460 | 0.0012647630 | 0.0005537100 |
+ | 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.0010222840 | 0.0007471290 | 0.0002151800 | 0.001213760 |
+ | nacl | N1=10,N2=10,T=0:0.001:0.006,i=0 | na | 22 | 31 | 11 | 22 | 22 | 0.0008372630 | 0.0006145080 | 0.0001728880 | 0.001165764 |
+ | nacl | N1=10,N2=10,T=0,i=0 | na | 22 | 31 | 11 | 22 | 22 | 0.0008533230 | 0.0006302930 | 0.0001737070 | 0.001184578 |
+ | knacl | N1=10,N2=10,N3=10,T=0:0.001:0.006,i=4 | na | 132 | 286 | 66 | 76 | 132 | 0.0027461050 | 0.0019984660 | 0.0006644370 | 0.001339485 |
+ | knacl | N1=10,N2=10,N3=10,T=0:0.001:0.006,i=0 | na | 132 | 286 | 66 | 76 | 132 | 0.0027876270 | 0.0020226200 | 0.0006828300 | 0.001347394 |
+ | knacl | N1=10,N2=10,N3=10,T=0,i=0 | na | 132 | 286 | 66 | 76 | 132 | 0.0027181210 | 0.0019761550 | 0.0006612210 | 0.001289587 |
+ | mc | N1=10,N2=10,T=0:0.001:0.006,i=4 | mg | 72 | 146 | 36 | 47 | 72 | 0.0018041570 | 0.0011872080 | 0.0005564560 | 0.001213348 |
+ | mc | N1=10,N2=10,T=0:0.001:0.006,i=0 | mg | 72 | 146 | 36 | 47 | 72 | 0.0017414820 | 0.0011517000 | 0.0005340830 | 0.001217190 |
+ | mc | N1=10,N2=10,T=0i=0 | mg | 72 | 146 | 36 | 47 | 72 | 0.0017543220 | 0.0011528700 | 0.0005441290 | 0.001193072 |
** Mutual Exclusion
@@ -863,11 +863,11 @@
#+CALL: bench(mutual_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |--------+--------+-----------+---------+---------+--------+----+-------+---------------+---------------+---------------|
- | mutual | N=3 | p1 | 13004 | 19360 | 2368 | 18 | 3779 | 0.2342249750 | 0.0737319720 | 0.1517310010 |
- | mutual | N=4 | p1 | 184784 | 294176 | 27600 | 18 | 17606 | 4.7020056120 | 1.0120345470 | 3.4521555270 |
- | mutual | N=5 | p1 | 2439040 | 4060400 | 308800 | 18 | 63189 | 91.0901674520 | 16.1996346390 | 71.5701971740 |
+ | 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.4740448850 | 0.1488212440 | 0.3085141530 | 0.015498567 |
+ | mutual | N=4 | p1 | 314368 | 423760 | 27600 | 26 | 178996 | 10.6683450390 | 2.3140630390 | 7.9967019650 | 0.222652533 |
+ | mutual | N=5 | p1 | 4260480 | 5881840 | 308800 | 28 | 2320292 | 224.5236245810 | 35.1589327080 | 179.4908187690 | 4.138425003 |
** Peer-to-Peer Protocol
@@ -892,10 +892,10 @@
#+CALL: bench(peer2peer_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |-----------+---------------+-----------------+---------+----------+---------+----+------+----------------+---------------+---------------|
- | peer2peer | N=4,K=4,T=1.1 | b11,b12,b13,b14 | 131072 | 589825 | 65536 | 28 | 5186 | 5.4029228830 | 2.1028815690 | 3.1462962300 |
- | peer2peer | N=5,K=4,T=1.1 | b11,b12,b13,b14 | 2097152 | 11534337 | 1048576 | 47 | 9146 | 126.8734840490 | 43.7285620480 | 79.5732111850 |
+ | 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.9727705090 | 1.9336080480 | 2.8984423040 | 0.261231151 |
+ | peer2peer | N=5,K=4,T=1.1 | b11,b12,b13,b14 | 2097152 | 11534337 | 1048576 | 47 | 9146 | 116.6987245890 | 40.6974802940 | 72.6752300300 | 3.283899994 |
** PEPA
@@ -938,11 +938,11 @@
#+CALL: bench(phil_original_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |---------------+--------+-----------+--------+---------+--------+----+--------+---------------+--------------+---------------|
- | phil_original | N=3 | p1 | 5254 | 7994 | 956 | 14 | 3196 | 0.1064149270 | 0.0308160840 | 0.0690485640 |
- | phil_original | N=4 | p1 | 62880 | 102096 | 9440 | 14 | 32900 | 1.6731439970 | 0.3460310980 | 1.2664375260 |
- | phil_original | N=5 | p1 | 728366 | 1234898 | 93068 | 14 | 336352 | 30.8762339240 | 4.5663775890 | 25.1685231070 |
+ | 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.1715543340 | 0.0563456520 | 0.1076311630 | 0.005861739 |
+ | phil_original | N=4 | p1 | 106880 | 146096 | 9440 | 22 | 65687 | 3.2955146020 | 0.7352457630 | 2.4329047920 | 0.069044309 |
+ | phil_original | N=5 | p1 | 1270596 | 1777128 | 93068 | 24 | 737938 | 57.2339260420 | 9.6288126570 | 45.3471601230 | 1.078908584 |
*** No Fair
@@ -971,10 +971,10 @@
#+CALL: bench(phil_nofair_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |-------------+---------+-----------+--------+-------+--------+----+-------+--------------+--------------+--------------|
- | phil_nofair | N=3,K=1 | p1 | 4606 | 6698 | 956 | 14 | 3178 | 0.0932602170 | 0.0355597460 | 0.0546810820 |
- | phil_nofair | N=4,K=1 | p1 | 54344 | 85024 | 9440 | 14 | 32808 | 1.4521071360 | 0.3227025450 | 1.0796627360 |
+ | 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.1406341460 | 0.0508404880 | 0.0848353530 | 0.004879584 |
+ | phil_nofair | N=4,K=1 | p1 | 89808 | 120488 | 9440 | 20 | 59877 | 2.5496694250 | 0.6356984830 | 1.8102656040 | 0.066967664 |
** Cyclic Server Polling
@@ -1005,16 +1005,16 @@
#+CALL: bench(poll_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |-------+----------+-----------+--------+-------+--------+----+-------+--------------+--------------+--------------|
- | poll | N=2,T=50 | s | 24 | 34 | 12 | 7 | 24 | 0.0010671490 | 0.0007754770 | 0.0002108160 |
- | poll | N=3,T=50 | s | 72 | 120 | 36 | 10 | 72 | 0.0018987980 | 0.0012447010 | 0.0005902550 |
- | poll | N=4,T=50 | s | 192 | 368 | 96 | 13 | 192 | 0.0040551170 | 0.0027627000 | 0.0011657700 |
- | poll | N=5,T=50 | s | 480 | 1040 | 240 | 16 | 480 | 0.0106612640 | 0.0057561260 | 0.0042764790 |
- | poll | N=6,T=50 | s | 1152 | 2784 | 576 | 19 | 1152 | 0.0286362990 | 0.0137992780 | 0.0138493380 |
- | poll | N=7,T=50 | s | 2688 | 7168 | 1344 | 22 | 2688 | 0.0764932780 | 0.0314023640 | 0.0427361450 |
- | poll | N=8,T=50 | s | 6144 | 17920 | 3072 | 25 | 6144 | 0.2000132290 | 0.0755396060 | 0.1156302960 |
- | poll | N=9,T=50 | s | 13824 | 43776 | 6912 | 28 | 13824 | 0.5161052940 | 0.1735822960 | 0.3252389160 |
+ | 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.0021227040 | 0.0018206500 | 0.0002425590 | 0.001402456 |
+ | poll | N=3,T=50 | s | 72 | 120 | 36 | 10 | 72 | 0.0018561590 | 0.0012023310 | 0.0005935680 | 0.001223291 |
+ | poll | N=4,T=50 | s | 192 | 368 | 96 | 13 | 192 | 0.0036577780 | 0.0024758640 | 0.0010588990 | 0.001284740 |
+ | poll | N=5,T=50 | s | 480 | 1040 | 240 | 16 | 480 | 0.0089668140 | 0.0047636110 | 0.0036715520 | 0.001593717 |
+ | poll | N=6,T=50 | s | 1152 | 2784 | 576 | 19 | 1152 | 0.0235332590 | 0.0111201230 | 0.0116040430 | 0.003008100 |
+ | poll | N=7,T=50 | s | 2688 | 7168 | 1344 | 22 | 2688 | 0.0653820210 | 0.0277986240 | 0.0351511720 | 0.006441226 |
+ | poll | N=8,T=50 | s | 6144 | 17920 | 3072 | 25 | 6144 | 0.1781163410 | 0.0652312120 | 0.1068562250 | 0.011917093 |
+ | poll | N=9,T=50 | s | 13824 | 43776 | 6912 | 28 | 13824 | 0.4818925210 | 0.1587100080 | 0.3073108060 | 0.035719632 |
** Mutual Exclusion à la Rabin
@@ -1040,10 +1040,10 @@
#+CALL: bench(rabin_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |-------+--------+-----------+---------+---------+--------+---+-------+----------------+---------------+---------------|
- | rabin | N=3 | p1 | 101168 | 211204 | 27766 | 5 | 8945 | 2.9017581070 | 0.8410896010 | 1.9130689140 |
- | rabin | N=4 | p1 | 2508408 | 5477060 | 668836 | 5 | 66630 | 118.1733361080 | 26.0846764120 | 88.8135763400 |
+ | 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 | 4.7714929120 | 1.2552915580 | 3.3879670760 | 0.147636299 |
+ | rabin | N=4 | p1 | 3679144 | 6647796 | 668836 | 9 | 468698 | 193.4578919920 | 37.9157772430 | 149.7000157640 | 4.270498076 |
** Self Stabilisation
*** Beauquier
@@ -1070,11 +1070,11 @@
#+CALL: bench(beauquier_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |-----------+-------------------+-----------+--------+-------+--------+---+-----+--------------+--------------+--------------|
- | beauquier | N=3,K=0,k=0 | d1,p1 | 224 | 304 | 64 | 6 | 212 | 0.0036527250 | 0.0024545840 | 0.0010864160 |
- | beauquier | N=3,K=0,k=1:2:3 | d1,p1 | 224 | 304 | 64 | 6 | 212 | 0.0034464340 | 0.0021811500 | 0.0011551700 |
- | beauquier | N=3,K=1:1:100,k=3 | d1,p1 | 224 | 304 | 64 | 6 | 212 | 0.0035032960 | 0.0022181370 | 0.0011625630 |
+ | 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.0070665140 | 0.0037813820 | 0.0031371020 | 0.001360574 |
+ | beauquier | N=3,K=0,k=1:2:3 | d1,p1 | 320 | 400 | 64 | 9 | 304 | 0.0047142630 | 0.0029690530 | 0.0016080150 | 0.001318498 |
+ | beauquier | N=3,K=1:1:100,k=3 | d1,p1 | 320 | 400 | 64 | 9 | 304 | 0.0045871890 | 0.0029109880 | 0.0015437340 | 0.001367182 |
*** Herman
@@ -1100,11 +1100,11 @@
#+CALL: bench(herman_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |--------+-------------------+-----------+--------+-------+--------+---+----+--------------+--------------+--------------|
- | herman | N=3,K=0,k=0 | x1 | 16 | 36 | 8 | 3 | 15 | 0.0010250280 | 0.0007443410 | 0.0002196830 |
- | herman | N=3,K=0,k=1:2:7 | x1 | 16 | 36 | 8 | 3 | 15 | 0.0010741930 | 0.0007844720 | 0.0002249140 |
- | herman | N=3,K=1:1:100,k=0 | x1 | 16 | 36 | 8 | 3 | 15 | 0.0012039660 | 0.0008312060 | 0.0002894840 |
+ | 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.0029780360 | 0.0021457350 | 0.0006707370 | 0.004299188 |
+ | herman | N=3,K=0,k=1:2:7 | x1 | 16 | 36 | 8 | 3 | 15 | 0.0028841120 | 0.0020621220 | 0.0006512160 | 0.001205789 |
+ | herman | N=3,K=1:1:100,k=0 | x1 | 16 | 36 | 8 | 3 | 15 | 0.0008583550 | 0.0006391370 | 0.0001766320 | 0.001180447 |
*** Israeli and Jalfon
@@ -1130,11 +1130,11 @@
#+CALL: bench(ij_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |----------------+-------------------+-----------+--------+-------+--------+---+----+--------------+--------------+--------------|
- | israeli-jalfon | N=3,K=0,k=0 | q1 | 26 | 40 | 7 | 4 | 17 | 0.0010139290 | 0.0007265180 | 0.0002092480 |
- | israeli-jalfon | N=3,K=0,k=1:1:3 | q1 | 26 | 40 | 7 | 4 | 17 | 0.0009654130 | 0.0006936970 | 0.0002157220 |
- | israeli-jalfon | N=3,K=1:1:100,k=0 | q1 | 26 | 40 | 7 | 4 | 17 | 0.0009305130 | 0.0006555940 | 0.0002180890 |
+ | 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.0043609660 | 0.0030318040 | 0.0011811690 | 0.001258792 |
+ | israeli-jalfon | N=3,K=0,k=1:1:3 | q1 | 38 | 52 | 7 | 7 | 26 | 0.0011467530 | 0.0007975370 | 0.0003082980 | 0.001241967 |
+ | israeli-jalfon | N=3,K=1:1:100,k=0 | q1 | 38 | 52 | 7 | 7 | 26 | 0.0011922040 | 0.0008536600 | 0.0002978600 | 0.001163322 |
** Tandem Queueing Network
@@ -1164,15 +1164,15 @@
#+CALL: bench(tandem_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |--------+-----------+-----------+--------+--------+--------+-----+--------+--------------+--------------+--------------|
- | tandem | T=1,c=3 | sc | 56 | 99 | 28 | 13 | 56 | 0.0020444530 | 0.0013167840 | 0.0006658560 |
- | tandem | T=1,c=7 | sc | 240 | 483 | 120 | 17 | 240 | 0.0050123350 | 0.0031758280 | 0.0015213880 |
- | tandem | T=1,c=15 | sc | 992 | 2115 | 496 | 25 | 992 | 0.0214330040 | 0.0107751610 | 0.0098780400 |
- | tandem | T=1,c=31 | sc | 4032 | 8835 | 2016 | 41 | 4032 | 0.0897771380 | 0.0423451080 | 0.0442989770 |
- | tandem | T=1,c=63 | sc | 16256 | 36099 | 8128 | 73 | 16256 | 0.4378963350 | 0.1663305730 | 0.2454104440 |
- | tandem | T=1,c=127 | sc | 65280 | 145923 | 32640 | 137 | 65280 | 2.0224284410 | 0.7307604410 | 1.2026261020 |
- | tandem | T=1,c=255 | sc | 261632 | 586755 | 130816 | 265 | 261632 | 9.5187125820 | 3.0532323880 | 5.6603868300 |
+ | 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.0062172490 | 0.0042159800 | 0.0018001740 | 0.001431136 |
+ | tandem | T=1,c=7 | sc | 240 | 483 | 120 | 17 | 240 | 0.0045045450 | 0.0028036560 | 0.0015670110 | 0.001363540 |
+ | tandem | T=1,c=15 | sc | 992 | 2115 | 496 | 25 | 992 | 0.0186471320 | 0.0090645420 | 0.0085897580 | 0.002129946 |
+ | tandem | T=1,c=31 | sc | 4032 | 8835 | 2016 | 41 | 4032 | 0.0818471360 | 0.0363339250 | 0.0422738160 | 0.005628605 |
+ | tandem | T=1,c=63 | sc | 16256 | 36099 | 8128 | 73 | 16256 | 0.3825791800 | 0.1509328770 | 0.2084166330 | 0.021288039 |
+ | tandem | T=1,c=127 | sc | 65280 | 145923 | 32640 | 137 | 65280 | 1.8330856570 | 0.6450710200 | 1.0858111870 | 0.089366251 |
+ | tandem | T=1,c=255 | sc | 261632 | 586755 | 130816 | 265 | 261632 | 8.7376419450 | 2.7555665420 | 5.2639976860 | 0.398082300 |
** WLAN
@@ -1210,16 +1210,16 @@
#+CALL: bench(wlan_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |-------------------+------------------------------------+-----------+---------+---------+--------+---+--------+---------------+---------------+---------------|
- | wlan | TRANS_TIME_MAX=10,k=2,K=0 | c1,c2 | 93942 | 122626 | 28480 | 8 | 66245 | 2.3616887090 | 0.6532304660 | 1.5749287060 |
- | wlan | TRANS_TIME_MAX=10,k=2,K=1 | c1,c2 | 93942 | 122626 | 28480 | 8 | 66245 | 2.3845750970 | 0.6343216450 | 1.6096372230 |
- | wlan | TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 93942 | 122626 | 28480 | 8 | 66245 | 2.3624566260 | 0.6360737690 | 1.5927722160 |
- | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=0 | c1,c2 | 94316 | 123050 | 28598 | 8 | 66245 | 2.3886041070 | 0.6456538030 | 1.6059087230 |
- | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 94316 | 123050 | 28598 | 8 | 66245 | 2.3952365570 | 0.6337526500 | 1.6244512510 |
- | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=3 | c1,c2 | 94316 | 123050 | 28598 | 8 | 66245 | 2.4018029590 | 0.6363316650 | 1.6288217890 |
- | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=0 | c1,c2 | 830830 | 1019591 | 248503 | 8 | 321139 | 24.0904198460 | 6.4635876440 | 16.3805907560 |
- | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 2016403 | 2571249 | 607727 | 8 | 727209 | 62.7162602700 | 16.6871851070 | 41.1353833420 |
+ | 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 | 3.7464944490 | 0.9860575820 | 2.6078309680 | 0.082397685 |
+ | wlan | TRANS_TIME_MAX=10,k=2,K=1 | c1,c2 | 130924 | 159608 | 28480 | 11 | 93978 | 3.7224492950 | 0.9831621610 | 2.5842074110 | 0.092656466 |
+ | wlan | TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 130924 | 159608 | 28480 | 11 | 93978 | 3.7150293520 | 0.9684084560 | 2.5952068950 | 0.080336365 |
+ | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=0 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 3.7206547810 | 0.9653163530 | 2.5999291400 | 0.083302642 |
+ | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 3.7361561010 | 0.9640359550 | 2.6181808800 | 0.083326246 |
+ | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=3 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 3.7325320910 | 0.9727097640 | 2.5871040410 | 0.081009243 |
+ | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=0 | c1,c2 | 1164654 | 1353415 | 248503 | 11 | 453477 | 38.0257833940 | 9.1846114840 | 27.2223471620 | 0.769305967 |
+ | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 2817352 | 3372198 | 607727 | 11 | 1038591 | 103.5838919740 | 24.8761804790 | 73.2835633500 | 2.196273987 |
** Zeroconf
@@ -1260,9 +1260,9 @@
#+CALL: bench(zeroconf_benchmarks)
#+RESULTS:
- | Model | Consts | Partition | States | Edges | Sort 0 | I | Q | t(s) | t_p(s) | t_r(s) |
- |-----------------------+--------------------------------------+-----------+---------+---------+--------+------+--------+---------------+--------------+---------------|
- | zeroconf | N=1000,K=4,err=0,reset=true | n,n0,n1,b | 3531 | 4056 | 1088 | 14 | 1743 | 0.0632904450 | 0.0302867720 | 0.0305903280 |
- | zeroconf | N=1000,K=4,err=0,reset=false | n,n0,n1,b | 1184763 | 1589127 | 307768 | 1717 | 593887 | 34.8158546280 | 8.9907240690 | 23.6549938640 |
- | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=true | n,n0,n1,b | 13737 | 16206 | 4214 | 14 | 6326 | 0.2538107310 | 0.0836276790 | 0.1589075700 |
- | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=false | n,n0,n1,b | 51994 | 66686 | 14834 | 54 | 22774 | 1.2325573030 | 0.3444631290 | 0.8388560040 |
+ | 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.0796394600 | 0.0329309100 | 0.0439400740 | 0.003172273 |
+ | zeroconf | N=1000,K=4,err=0,reset=false | n,n0,n1,b | 1753990 | 2158354 | 307768 | 1721 | 835101 | 57.7927334970 | 14.7249066110 | 40.4476155640 | 1.299638305 |
+ | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=true | n,n0,n1,b | 19046 | 21515 | 4214 | 18 | 8602 | 0.3726282020 | 0.1279469810 | 0.2300872160 | 0.009388841 |
+ | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=false | n,n0,n1,b | 74320 | 89012 | 14834 | 58 | 31671 | 1.8917730410 | 0.5124930110 | 1.2954160320 | 0.042018285 |