diff --git a/prism/benchmark.org b/prism/benchmark.org index 645317521cb0c23355629d485e980846f267654e..9b40b3d8d7cdc56525609171d8470d1488bba282 100644 --- a/prism/benchmark.org +++ b/prism/benchmark.org @@ -52,11 +52,7 @@ | dice | dice/dice.pm | dtmc | | | two_dice_knuth | dice/two_dice_knuth.pm | dtmc | | | two_dice | dice/two_dice.nm | mdp | | - | dining_crypt3 | dining_crypt/dining_crypt3.nm | mdp | k | - | dining_crypt4 | dining_crypt/dining_crypt4.nm | mdp | k | - | dining_crypt5 | dining_crypt/dining_crypt5.nm | mdp | k | - | dining_crypt6 | dining_crypt/dining_crypt6.nm | mdp | k | - | dining_crypt7 | dining_crypt/dining_crypt7.nm | mdp | k | + | dining_crypt | dining_crypt/dining_cryptN.nm | mdp | N, k | | embedded | embedded/embedded.sm | ctmc | MAX_COUNT, T | | firewire_abst_firewire | firewire/abst/firewire.nm | mdp | delay, fast | | firewire_abst_deadline | firewire/abst/deadline.nm | mdp | deadline, delay, fast | @@ -465,26 +461,26 @@ Benchmarks: #+NAME: dining_crypt_benchmarks - | Model | Constants | Partition | - |---------------+-----------+-----------| - | dining_crypt3 | | pay | - | dining_crypt4 | | pay | - | dining_crypt5 | | pay | - | dining_crypt6 | | pay | - | dining_crypt7 | | pay | + | Model | Constants | Partition | + |--------------+-----------+-----------| + | dining_crypt | N=3 | pay | + | dining_crypt | N=4 | pay | + | dining_crypt | N=5 | pay | + | dining_crypt | N=6 | pay | + | dining_crypt | N=7 | pay | Results: #+CALL: bench(dining_crypt_benchmarks) #+RESULTS: - | Model | Constants | Partition | Time(s) | - |---------------+-----------+-----------+--------------| - | dining_crypt3 | | pay | 0.014666643 | - | dining_crypt4 | | pay | 0.104119122 | - | dining_crypt5 | | pay | 0.731228810 | - | dining_crypt6 | | pay | 5.069027086 | - | dining_crypt7 | | pay | 33.970064235 | + | 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 | ** Embedded Control System