diff --git a/prism/benchmark.org b/prism/benchmark.org index a5b3a6bef68c63778a934284c3d8304c670d2910..671196df80a52e5d17739541492ddf1de51446f2 100644 --- a/prism/benchmark.org +++ b/prism/benchmark.org @@ -947,16 +947,16 @@ #+CALL: bench(poll_benchmarks) #+RESULTS: - | Model | Constants | Partition | Time(s) | - |-------+-----------+-----------+-------------| - | poll | N=2,T=50 | s | 0.002390337 | - | poll | N=3,T=50 | s | 0.003281045 | - | poll | N=4,T=50 | s | 0.005657634 | - | poll | N=5,T=50 | s | 0.010797578 | - | poll | N=6,T=50 | s | 0.027570597 | - | poll | N=7,T=50 | s | 0.079170932 | - | poll | N=8,T=50 | s | 0.196261201 | - | poll | N=9,T=50 | s | 0.508719703 | + | 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 | ** Mutual Exclusion à la Rabin