diff --git a/prism/benchmark.org b/prism/benchmark.org index 1f10284810be0a886e2ffcceec846547d3858eeb..8b1116bc2dad250e33282ae4cdee99ee3343a866 100644 --- a/prism/benchmark.org +++ b/prism/benchmark.org @@ -61,9 +61,7 @@ | fms | fms/fms.sm | ctmc | n | | kanban | kanban/kanban.sm | ctmc | t | | leader_sync | leader/synchronous/leaderN_K.pm | dtmc | L | - | leader_async3 | leader/asynchronous/leader3.nm | mdp | K | - | leader_async4 | leader/asynchronous/leader4.nm | mdp | K | - | leader_async5 | leader/asynchronous/leader5.nm | mdp | K | + | leader_async | leader/asynchronous/leaderN.nm | mdp | N, K | | nacl | molecules/nacl.sm | ctmc | N1, N2, T, i | | knacl | molecules/knacl.sm | ctmc | N1, N2, N3, T, i | | mc | molecules/mc.sm | ctmc | N1, N2, T, i | @@ -651,6 +649,8 @@ Benchmarks: + We initially partition on the respective local states of all processes. + #+NAME: leader_sync_benchmarks | Model | Constants | Partition | |-------------+-------------+----------------| @@ -691,23 +691,25 @@ Benchmarks: + We initially partition on the respective local states of all processes. + #+NAME: leader_async_benchmarks - | Model | Constants | Partition | - |---------------+-----------+----------------| - | leader_async3 | K=1 | s1,s2,s3 | - | leader_async4 | K=1 | s1,s2,s3,s4 | - | leader_async5 | K=1 | s1,s2,s3,s4,s5 | + | Model | Constants | Partition | + |--------------+-----------+----------------| + | leader_async | N=3,K=1 | s1,s2,s3 | + | leader_async | N=4,K=1 | s1,s2,s3,s4 | + | leader_async | N=5,K=1 | s1,s2,s3,s4,s5 | Results: #+CALL: bench(leader_async_benchmarks) #+RESULTS: - | Model | Constants | Partition | Time(s) | - |---------------+-----------+----------------+-------------| - | leader_async3 | K=1 | s1,s2,s3 | 0.017765507 | - | leader_async4 | K=1 | s1,s2,s3,s4 | 0.202155161 | - | leader_async5 | K=1 | s1,s2,s3,s4,s5 | 2.501104425 | + | 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 | ** Molecules