From f120be9f35a93d5c52b19d67f65768e19d4f8b7d Mon Sep 17 00:00:00 2001 From: Hans-Peter Deifel <hpd@hpdeifel.de> Date: Fri, 5 Oct 2018 00:19:21 +0200 Subject: [PATCH] Update prism benchmarks --- prism/benchmark.org | 270 ++++++++++++++++++++++---------------------- 1 file changed, 135 insertions(+), 135 deletions(-) diff --git a/prism/benchmark.org b/prism/benchmark.org index a89b714..4a5e404 100644 --- a/prism/benchmark.org +++ b/prism/benchmark.org @@ -318,18 +318,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.0188950360 | 0.0098092270 | 0.0076425390 | 0.002146178 | - | brp | N=16,MAX=3 | s | 1772 | 2041 | 886 | 8 | 882 | 0.0304527650 | 0.0156660330 | 0.0127367270 | 0.002410077 | - | brp | N=16,MAX=4 | s | 2190 | 2538 | 1095 | 8 | 1108 | 0.0269560230 | 0.0136345220 | 0.0118421960 | 0.002389365 | - | brp | N=16,MAX=5 | s | 2608 | 3035 | 1304 | 8 | 1334 | 0.0332567440 | 0.0162388570 | 0.0148080690 | 0.002676431 | - | brp | N=32,MAX=2 | s | 2698 | 3080 | 1349 | 8 | 1296 | 0.0322524490 | 0.0162090300 | 0.0139492290 | 0.002331856 | - | brp | N=32,MAX=3 | s | 3532 | 4073 | 1766 | 8 | 1746 | 0.0440965050 | 0.0222288100 | 0.0198487370 | 0.003230717 | - | brp | N=32,MAX=4 | s | 4366 | 5066 | 2183 | 8 | 2196 | 0.0556214930 | 0.0264696080 | 0.0265295730 | 0.003670085 | - | brp | N=32,MAX=5 | s | 5200 | 6059 | 2600 | 8 | 2646 | 0.0695928030 | 0.0329448630 | 0.0320962750 | 0.003937146 | - | brp | N=64,MAX=2 | s | 5386 | 6152 | 2693 | 8 | 2576 | 0.0680201300 | 0.0333708410 | 0.0295354600 | 0.003989285 | - | brp | N=64,MAX=3 | s | 7052 | 8137 | 3526 | 8 | 3474 | 0.0939140690 | 0.0443968700 | 0.0450378270 | 0.004797144 | - | brp | N=64,MAX=4 | s | 8718 | 10122 | 4359 | 8 | 4372 | 0.1198332050 | 0.0578635050 | 0.0555599790 | 0.005731700 | - | brp | N=64,MAX=5 | s | 10384 | 12107 | 5192 | 8 | 5270 | 0.1484909690 | 0.0677984730 | 0.0728306520 | 0.006421111 | + | 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 | ** Cell in Wireless Communication Network @@ -361,12 +361,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.0011894620 | 0.0008788470 | 0.0002462850 | 0.001401349 | - | cell | N=100,T=0.5 | | 101 | 200 | 101 | 80 | 101 | 0.0016633860 | 0.0009933760 | 0.0005557070 | 0.001454158 | - | cell | N=200,T=0.5 | | 201 | 400 | 201 | 160 | 201 | 0.0026713560 | 0.0016791780 | 0.0008379350 | 0.001628887 | - | cell | N=300,T=0.5 | | 301 | 600 | 301 | 251 | 301 | 0.0036202190 | 0.0020721700 | 0.0012313100 | 0.001783353 | - | cell | N=400,T=0.5 | | 401 | 800 | 401 | 351 | 401 | 0.0049426580 | 0.0027046720 | 0.0017427840 | 0.001882094 | - | cell | N=500,T=0.5 | | 501 | 1000 | 501 | 451 | 501 | 0.0055804840 | 0.0029686370 | 0.0020414390 | 0.001978327 | + | 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 | ** Dependable Cluster @@ -393,10 +393,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.0182412610 | 0.0085451460 | 0.0088147900 | 0.003163900 | - | cluster | N=8,T=10 | | 2772 | 12832 | 2772 | 359 | 1917 | 0.0651362330 | 0.0256683430 | 0.0368183740 | 0.008481651 | - | cluster | N=16,T=10 | | 10132 | 48160 | 10132 | 711 | 7021 | 0.2851114870 | 0.1048529180 | 0.1668840730 | 0.027820578 | - | cluster | N=32,T=10 | | 38676 | 186400 | 38676 | 1415 | 26829 | 1.2521929310 | 0.4053136910 | 0.7520738080 | 0.127231512 | + | 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 | ** Shared coin protocol @@ -422,10 +422,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.0163994120 | 0.0086990680 | 0.0071874150 | 0.001855358 | - | coin | N=2,K=4,k=10 | pc1,pc2 | 2624 | 3068 | 528 | 20 | 837 | 0.0311953930 | 0.0162076340 | 0.0139152760 | 0.002594711 | - | coin | N=4,K=2,k=10 | pc1,pc2,pc3,pc4 | 166400 | 218976 | 22656 | 262 | 32860 | 3.3047407230 | 1.1673807350 | 2.0192748310 | 0.082545026 | - | coin | N=4,K=4,k=10 | pc1,pc2,pc3,pc4 | 317952 | 419168 | 43136 | 262 | 63132 | 6.6214747270 | 2.2195561030 | 4.0914969870 | 0.169557882 | + | coin | N=2,K=2,k=10 | pc1,pc2 | 1344 | 1564 | 272 | 20 | 437 | 0.0171049230 | 0.0093142880 | 0.0072575380 | 0.001804668 | + | coin | N=2,K=4,k=10 | pc1,pc2 | 2624 | 3068 | 528 | 20 | 837 | 0.0311217670 | 0.0161397530 | 0.0139169040 | 0.002401901 | + | coin | N=4,K=2,k=10 | pc1,pc2,pc3,pc4 | 166400 | 218976 | 22656 | 262 | 32860 | 3.3746632030 | 1.1837290750 | 2.0716036590 | 0.097529010 | + | coin | N=4,K=4,k=10 | pc1,pc2,pc3,pc4 | 317952 | 419168 | 43136 | 262 | 63132 | 6.6321609420 | 2.1929385640 | 4.1228524830 | 0.169530354 | ** IEEE 802.3 CSMA/CD @@ -462,11 +462,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.0476302400 | 0.0263560700 | 0.0194732830 | 0.002887048 | - | csma | N=2,K=4,k=1 | b | 31892 | 34528 | 7958 | 7 | 3955 | 0.4185876040 | 0.2030995700 | 0.1979958370 | 0.013156199 | - | csma | N=2,K=6,k=1 | b | 267012 | 293366 | 66718 | 7 | 29575 | 4.8254152400 | 1.8920757130 | 2.6817095170 | 0.121755517 | - | csma | N=3,K=2,k=1 | b | 150612 | 169624 | 36850 | 8 | 9228 | 2.6504964620 | 1.0151165680 | 1.4600879550 | 0.062983945 | - | csma | N=4,K=2,k=1 | b | 3174932 | 3740038 | 761962 | 9 | 40920 | 84.4799675000 | 26.0543066790 | 54.8930418350 | 2.106186147 | + | 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 | ** Dice @@ -491,9 +491,9 @@ #+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.0027397180 | 0.0019604890 | 0.0006027410 | 0.001454446 | - | two_dice_knuth | | s | 90 | 124 | 45 | 36 | 65 | 0.0017874860 | 0.0011955980 | 0.0005269940 | 0.001388099 | - | two_dice | | s1,s2 | 846 | 1113 | 169 | 68 | 316 | 0.0100751720 | 0.0060373370 | 0.0036686880 | 0.001694433 | + | 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 | ** Dining cryptographers @@ -521,11 +521,11 @@ #+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.0230494130 | 0.0127772160 | 0.0085923400 | 0.002202896 | - | dining_crypt | N=4 | pay | 13410 | 16965 | 2165 | 11 | 560 | 0.1812904460 | 0.0868927480 | 0.0872490690 | 0.007217677 | - | dining_crypt | N=5 | pay | 85104 | 112026 | 11850 | 13 | 1644 | 1.4520456140 | 0.5920173400 | 0.8222563360 | 0.042030725 | - | dining_crypt | N=6 | pay | 516698 | 700455 | 63063 | 15 | 4445 | 10.8023676790 | 3.8273971080 | 6.6041024110 | 0.257029574 | - | dining_crypt | N=7 | pay | 3029600 | 4200312 | 328760 | 17 | 11384 | 76.9138726350 | 25.0527085750 | 49.4994786660 | 1.671568953 | + | 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 | ** Embedded Control System @@ -552,9 +552,9 @@ #+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.1100440610 | 0.0646915790 | 0.0412657370 | 0.012709559 | - | embedded | MAX_COUNT=2,T=14 | i,a,m | 6956 | 18117 | 3478 | 86 | 252 | 0.1109864620 | 0.0653588060 | 0.0415045250 | 0.015237451 | - | embedded | MAX_COUNT=2,T=0 | i,a,m | 6956 | 18117 | 3478 | 86 | 252 | 0.1097881480 | 0.0644046900 | 0.0413261700 | 0.013154117 | + | 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 | ** Firewire @@ -609,20 +609,20 @@ #+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.0494186720 | 0.0257453310 | 0.0218591030 | 0.003022763 | - | firewire_abst_firewire | delay=3,fast=0.2:0.1:0.8 | s | 2610 | 2717 | 611 | 15 | 2450 | 0.0298752630 | 0.0153000670 | 0.0133244590 | 0.002511750 | - | firewire_abst_firewire | delay=36,fast=0.2:0.1:0.8 | s | 3930 | 4565 | 776 | 15 | 3242 | 0.0492653910 | 0.0253711350 | 0.0220726070 | 0.002906351 | - | firewire_abst_deadline | deadline=200,delay=36,fast=0.5 | s | 327514 | 373007 | 67901 | 17 | 70383 | 6.8125534080 | 2.3039300550 | 4.2174788310 | 0.161257427 | - | firewire_abst_deadline | deadline=300,delay=36,fast=0.5 | s | 703930 | 810013 | 142810 | 17 | 273380 | 16.6322833480 | 4.9967263510 | 10.5505602590 | 0.389238511 | - | firewire_abst_deadline | deadline=400,delay=36,fast=0.5 | s | 1096930 | 1266513 | 220410 | 17 | 462758 | 27.3392666710 | 8.3952436700 | 17.6091180250 | 0.677216999 | - | firewire_abst_deadline | deadline=500,delay=36,fast=0.5 | s | 1489930 | 1723013 | 298010 | 17 | 653158 | 38.8698501590 | 11.6639097350 | 25.0697188800 | 0.985507254 | - | firewire_abst_deadline | deadline=600,delay=36,fast=0.5 | s | 1882930 | 2179513 | 375610 | 17 | 843558 | 49.8337730880 | 14.3954997030 | 31.9074757530 | 1.269223500 | - | firewire_impl_firewire | delay=36,fast=0.5 | w12 | 1382048 | 1651572 | 212268 | 10 | 256615 | 37.2488858380 | 10.8166382590 | 24.7305268030 | 0.908223813 | - | firewire_impl_firewire | delay=3,fast=0.2:0.1:0.8 | w12 | 19224 | 20716 | 4093 | 10 | 14581 | 0.2727050040 | 0.1174786780 | 0.1390329030 | 0.009668480 | - | firewire_impl_firewire | delay=36,fast=0.2:0.1:0.8 | w12 | 1382048 | 1651572 | 212268 | 10 | 256615 | 36.5249287240 | 10.3680540760 | 24.4643583470 | 0.892992872 | - | firewire_impl_deadline | deadline=200,delay=3,fast=0.5 | w12 | 384032 | 416294 | 80980 | 10 | 7925 | 5.8788569030 | 2.6241322130 | 3.0244084240 | 0.141427104 | - | firewire_impl_deadline | deadline=300,delay=3,fast=0.5 | w12 | 995134 | 1069583 | 213805 | 10 | 20640 | 16.2098460610 | 7.1057442250 | 8.4122592500 | 0.397433871 | - | firewire_impl_deadline | deadline=400,delay=3,fast=0.5 | w12 | 2040822 | 2201345 | 434364 | 10 | 475841 | 41.7396024340 | 15.8261203680 | 23.2245395020 | 0.992461145 | + | 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 | ** Flexible Manufacturing System @@ -654,12 +654,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.0016589520 | 0.0010199620 | 0.0005822890 | 0.001296463 | - | fms | n=2 | | 810 | 3699 | 810 | 95 | 810 | 0.0181915520 | 0.0079072300 | 0.0093955000 | 0.003774613 | - | fms | n=3 | | 6520 | 37394 | 6520 | 190 | 6520 | 0.2265589320 | 0.0739326040 | 0.1439085330 | 0.029541573 | - | fms | n=4 | | 35910 | 237120 | 35910 | 294 | 35910 | 1.7562615800 | 0.4952735860 | 1.1980477340 | 0.204527004 | - | fms | n=5 | | 152712 | 1111482 | 152712 | 372 | 152712 | 9.8220047470 | 2.4682988850 | 6.9644375610 | 1.160547092 | - | fms | n=6 | | 537768 | 4205670 | 537768 | 463 | 537768 | 42.2731691720 | 9.6807067850 | 31.0679153790 | 5.332736467 | + | 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 | ** Kanban @@ -688,10 +688,10 @@ #+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.0033925270 | 0.0021004710 | 0.0010204130 | 0.001783636 | - | kanban | t=2 | | 4600 | 28120 | 4600 | 69 | 4600 | 0.1492719920 | 0.0537122170 | 0.0876977220 | 0.020728106 | - | kanban | t=3 | | 58400 | 446400 | 58400 | 81 | 58400 | 3.4850200380 | 0.8539087910 | 2.4595447090 | 0.351481823 | - | kanban | t=4 | | 454475 | 3979850 | 454475 | 86 | 454475 | 40.0881567210 | 8.9440957260 | 29.8893517990 | 4.732188670 | + | 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 | ** Leader Election Protocol *** Synchronous @@ -726,15 +726,15 @@ #+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.0012455620 | 0.0010357300 | 0.0001660650 | 0.001580897 | - | leader_sync | N=3,K=3,L=1 | s1,s2,s3 | 138 | 164 | 69 | 5 | 15 | 0.0021297550 | 0.0016815460 | 0.0003816110 | 0.001530016 | - | leader_sync | N=3,K=4,L=1 | s1,s2,s3 | 294 | 357 | 147 | 5 | 15 | 0.0032029720 | 0.0023936790 | 0.0007066800 | 0.001468995 | - | leader_sync | N=4,K=2,L=1 | s1,s2,s3,s4 | 122 | 137 | 61 | 5 | 19 | 0.0021298570 | 0.0017019130 | 0.0003240700 | 0.001485295 | - | leader_sync | N=4,K=3,L=1 | s1,s2,s3,s4 | 548 | 628 | 274 | 5 | 19 | 0.0054733350 | 0.0037655810 | 0.0015253770 | 0.001695948 | - | leader_sync | N=4,K=4,L=1 | s1,s2,s3,s4 | 1624 | 1879 | 812 | 5 | 19 | 0.0161193470 | 0.0104516400 | 0.0050446030 | 0.002082084 | - | leader_sync | N=5,K=2,L=1 | s1,s2,s3,s4,s5 | 282 | 313 | 141 | 5 | 23 | 0.0033329840 | 0.0024485710 | 0.0007740910 | 0.001564871 | - | leader_sync | N=5,K=3,L=1 | s1,s2,s3,s4,s5 | 2100 | 2342 | 1050 | 5 | 23 | 0.0206586440 | 0.0129294410 | 0.0068270380 | 0.002177223 | - | leader_sync | N=5,K=4,L=1 | s1,s2,s3,s4,s5 | 8488 | 9511 | 4244 | 5 | 23 | 0.0910144150 | 0.0525467830 | 0.0324466550 | 0.004438275 | + | 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 | *** Asynchronous @@ -762,9 +762,9 @@ #+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.0224499980 | 0.0116675460 | 0.0098302840 | 0.002160238 | - | leader_async | N=4,K=1 | s1,s2,s3,s4 | 18848 | 22820 | 3172 | 223 | 5611 | 0.2766182730 | 0.1228863100 | 0.1433195320 | 0.008872060 | - | leader_async | N=5,K=1 | s1,s2,s3,s4,s5 | 184568 | 231634 | 27299 | 870 | 41756 | 3.5497851540 | 1.2774373690 | 2.1403442240 | 0.088139541 | + | 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 | ** Molecules @@ -805,15 +805,15 @@ #+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.0008443860 | 0.0006118490 | 0.0001735270 | 0.001378318 | - | nacl | N1=10,N2=10,T=0:0.001:0.006,i=0 | na | 22 | 31 | 11 | 22 | 22 | 0.0008306220 | 0.0006133590 | 0.0001661960 | 0.001426326 | - | nacl | N1=10,N2=10,T=0,i=0 | na | 22 | 31 | 11 | 22 | 22 | 0.0009913170 | 0.0007715850 | 0.0001699910 | 0.001290936 | - | knacl | N1=10,N2=10,N3=10,T=0:0.001:0.006,i=4 | na | 132 | 286 | 66 | 76 | 132 | 0.0026645840 | 0.0019819240 | 0.0005980100 | 0.001535300 | - | knacl | N1=10,N2=10,N3=10,T=0:0.001:0.006,i=0 | na | 132 | 286 | 66 | 76 | 132 | 0.0025841620 | 0.0019225880 | 0.0005803290 | 0.001427382 | - | knacl | N1=10,N2=10,N3=10,T=0,i=0 | na | 132 | 286 | 66 | 76 | 132 | 0.0025980660 | 0.0019369310 | 0.0005820160 | 0.001474482 | - | mc | N1=10,N2=10,T=0:0.001:0.006,i=4 | mg | 72 | 146 | 36 | 47 | 72 | 0.0017686360 | 0.0011994120 | 0.0005109210 | 0.001497097 | - | mc | N1=10,N2=10,T=0:0.001:0.006,i=0 | mg | 72 | 146 | 36 | 47 | 72 | 0.0017970850 | 0.0012216930 | 0.0005207130 | 0.001438862 | - | mc | N1=10,N2=10,T=0i=0 | mg | 72 | 146 | 36 | 47 | 72 | 0.0017843320 | 0.0012051610 | 0.0005271200 | 0.001407019 | + | 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 | ** Mutual Exclusion @@ -866,9 +866,9 @@ #+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.3694790620 | 0.1323802260 | 0.2234964700 | 0.012388897 | - | mutual | N=4 | p1 | 314368 | 423760 | 27600 | 26 | 178996 | 8.0228840090 | 2.1777250550 | 5.4691608570 | 0.220155250 | - | mutual | N=5 | p1 | 4260480 | 5881840 | 308800 | 28 | 2320292 | 157.0285429100 | 33.0592370560 | 115.2237349140 | 4.114433922 | + | 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 | ** Peer-to-Peer Protocol @@ -895,8 +895,8 @@ #+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.4684696300 | 1.7074202030 | 2.6221442800 | 0.295253462 | - | peer2peer | N=5,K=4,T=1.1 | b11,b12,b13,b14 | 2097152 | 11534337 | 1048576 | 47 | 9146 | 101.2148887470 | 36.7977000240 | 61.3423567040 | 3.339991652 | + | 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 | ** PEPA @@ -941,9 +941,9 @@ #+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.1348028980 | 0.0534504140 | 0.0766576930 | 0.006007028 | - | phil_original | N=4 | p1 | 106880 | 146096 | 9440 | 22 | 65687 | 2.5052405480 | 0.6879468700 | 1.7382986730 | 0.072883812 | - | phil_original | N=5 | p1 | 1270596 | 1777128 | 93068 | 24 | 737938 | 42.5007280010 | 8.9768393670 | 31.8995922180 | 1.124525879 | + | 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 | *** No Fair @@ -974,8 +974,8 @@ #+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.1140704260 | 0.0486332970 | 0.0615730220 | 0.005067395 | - | phil_nofair | N=4,K=1 | p1 | 89808 | 120488 | 9440 | 20 | 59877 | 2.0014410900 | 0.5981093440 | 1.3362608580 | 0.056992915 | + | 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 | ** Cyclic Server Polling @@ -1008,14 +1008,14 @@ #+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.0018727460 | 0.0014765100 | 0.0002866820 | 0.001406508 | - | poll | N=3,T=50 | s | 72 | 120 | 36 | 10 | 72 | 0.0017936850 | 0.0011660510 | 0.0005724820 | 0.001413147 | - | poll | N=4,T=50 | s | 192 | 368 | 96 | 13 | 192 | 0.0033036170 | 0.0022367790 | 0.0009658030 | 0.001560300 | - | poll | N=5,T=50 | s | 480 | 1040 | 240 | 16 | 480 | 0.0077280800 | 0.0044219660 | 0.0030579600 | 0.001854376 | - | poll | N=6,T=50 | s | 1152 | 2784 | 576 | 19 | 1152 | 0.0200765060 | 0.0099330340 | 0.0092926580 | 0.003252963 | - | poll | N=7,T=50 | s | 2688 | 7168 | 1344 | 22 | 2688 | 0.0547510590 | 0.0255323740 | 0.0271718120 | 0.006263860 | - | poll | N=8,T=50 | s | 6144 | 17920 | 3072 | 25 | 6144 | 0.1471080040 | 0.0570083080 | 0.0848655010 | 0.011877615 | - | poll | N=9,T=50 | s | 13824 | 43776 | 6912 | 28 | 13824 | 0.4038697710 | 0.1408657310 | 0.2477647120 | 0.035613908 | + | 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 | ** Mutual Exclusion à la Rabin @@ -1043,8 +1043,8 @@ #+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.5366239430 | 1.1626325160 | 2.2389496670 | 0.118025275 | - | rabin | N=4 | p1 | 3679144 | 6647796 | 668836 | 9 | 468698 | 137.9010502200 | 35.1524329990 | 97.6223431620 | 4.240369669 | + | 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 | ** Self Stabilisation *** Beauquier @@ -1073,9 +1073,9 @@ #+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.0046853890 | 0.0030033350 | 0.0015608240 | 0.001563627 | - | beauquier | N=3,K=0,k=1:2:3 | d1,p1 | 320 | 400 | 64 | 9 | 304 | 0.0043421760 | 0.0027671980 | 0.0014575940 | 0.001502174 | - | beauquier | N=3,K=1:1:100,k=3 | d1,p1 | 320 | 400 | 64 | 9 | 304 | 0.0045126660 | 0.0029127010 | 0.0014801840 | 0.001393170 | + | 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 | *** Herman @@ -1103,9 +1103,9 @@ #+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.0008104630 | 0.0005986420 | 0.0001736520 | 0.001358830 | - | herman | N=3,K=0,k=1:2:7 | x1 | 16 | 36 | 8 | 3 | 15 | 0.0008579220 | 0.0006450260 | 0.0001748980 | 0.001301007 | - | herman | N=3,K=1:1:100,k=0 | x1 | 16 | 36 | 8 | 3 | 15 | 0.0008028760 | 0.0005896810 | 0.0001739130 | 0.001366661 | + | 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 | *** Israeli and Jalfon @@ -1133,9 +1133,9 @@ #+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.0011529370 | 0.0008155630 | 0.0003009700 | 0.001338530 | - | israeli-jalfon | N=3,K=0,k=1:1:3 | q1 | 38 | 52 | 7 | 7 | 26 | 0.0011120980 | 0.0007771280 | 0.0002978090 | 0.001376369 | - | israeli-jalfon | N=3,K=1:1:100,k=0 | q1 | 38 | 52 | 7 | 7 | 26 | 0.0011415460 | 0.0007963930 | 0.0002953980 | 0.001286816 | + | 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 | ** Tandem Queueing Network @@ -1167,13 +1167,13 @@ #+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.0014820900 | 0.0011315000 | 0.0002904420 | 0.001431661 | - | tandem | T=1,c=7 | sc | 240 | 483 | 120 | 17 | 240 | 0.0041254950 | 0.0026239090 | 0.0013077780 | 0.001756718 | - | tandem | T=1,c=15 | sc | 992 | 2115 | 496 | 25 | 992 | 0.0169052150 | 0.0081456600 | 0.0079959590 | 0.002552562 | - | tandem | T=1,c=31 | sc | 4032 | 8835 | 2016 | 41 | 4032 | 0.0726668500 | 0.0325795640 | 0.0371850770 | 0.006219019 | - | tandem | T=1,c=63 | sc | 16256 | 36099 | 8128 | 73 | 16256 | 0.3287744450 | 0.1331997120 | 0.1794725280 | 0.021913007 | - | tandem | T=1,c=127 | sc | 65280 | 145923 | 32640 | 137 | 65280 | 1.6548456180 | 0.6044918960 | 0.9749148050 | 0.099776383 | - | tandem | T=1,c=255 | sc | 261632 | 586755 | 130816 | 265 | 261632 | 7.1984889890 | 2.4235422100 | 4.2074060010 | 0.414266407 | + | 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 | ** WLAN @@ -1213,14 +1213,14 @@ #+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 | 3.5839339150 | 0.9110962170 | 2.4584573070 | 0.099914037 | - | wlan | TRANS_TIME_MAX=10,k=2,K=1 | c1,c2 | 130924 | 159608 | 28480 | 11 | 93978 | 2.7943990100 | 0.9932372370 | 1.6429902310 | 0.086112979 | - | wlan | TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 130924 | 159608 | 28480 | 11 | 93978 | 2.7085619200 | 0.9071012910 | 1.6434265670 | 0.093285420 | - | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=0 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 2.7354142090 | 0.9069037080 | 1.6668874220 | 0.097207219 | - | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 2.7219018230 | 0.9001929150 | 1.6572252480 | 0.081757576 | - | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=3 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 2.7326067240 | 0.9081559580 | 1.6618832380 | 0.098859321 | - | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=0 | c1,c2 | 1164654 | 1353415 | 248503 | 11 | 453477 | 26.6775090080 | 8.5827093630 | 16.0744046520 | 0.777281090 | - | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 2817352 | 3372198 | 607727 | 11 | 1038591 | 72.6440292420 | 23.2892330420 | 45.3142019650 | 2.207380531 | + | wlan | TRANS_TIME_MAX=10,k=2,K=0 | c1,c2 | 130924 | 159608 | 28480 | 11 | 93978 | 2.5795851610 | 0.8756316910 | 1.5495106960 | 0.080312674 | + | wlan | TRANS_TIME_MAX=10,k=2,K=1 | c1,c2 | 130924 | 159608 | 28480 | 11 | 93978 | 2.7299784310 | 0.9664400010 | 1.6044077410 | 0.096319025 | + | wlan | TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 130924 | 159608 | 28480 | 11 | 93978 | 2.6733091280 | 0.8947473770 | 1.6191451950 | 0.080323906 | + | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=0 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 2.6728393770 | 0.8901755260 | 1.6134748050 | 0.087877106 | + | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=2 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 2.6658679510 | 0.8946790950 | 1.6079022800 | 0.084412667 | + | wlan_collide | COL=2,TRANS_TIME_MAX=10,k=2,K=3 | c1,c2 | 131436 | 160170 | 28598 | 11 | 93978 | 2.6687942280 | 0.8975846390 | 1.6050872500 | 0.079983295 | + | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=0 | c1,c2 | 1164654 | 1353415 | 248503 | 11 | 453477 | 25.9879118920 | 8.5385552270 | 15.4460330920 | 0.735166115 | + | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2 | 2817352 | 3372198 | 607727 | 11 | 1038591 | 70.6483613060 | 22.6843832900 | 43.8991528170 | 2.128643841 | ** Zeroconf @@ -1263,7 +1263,7 @@ #+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.0644922620 | 0.0308532900 | 0.0313861540 | 0.003329406 | - | zeroconf | N=1000,K=4,err=0,reset=false | n,n0,n1,b | 1753990 | 2158354 | 307768 | 1721 | 835101 | 43.0012910080 | 13.6607244320 | 26.7934068730 | 1.296812405 | - | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=true | n,n0,n1,b | 19046 | 21515 | 4214 | 18 | 8602 | 0.2754106730 | 0.1225439420 | 0.1384951790 | 0.010186214 | - | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=false | n,n0,n1,b | 74320 | 89012 | 14834 | 58 | 31671 | 1.4049972150 | 0.4923834490 | 0.8606184700 | 0.049947670 | + | 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 | -- GitLab