From 9ed1fa19e20c74aaee1915b2db049849096c8e52 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 15 May 2013 18:25:20 +0200 Subject: [PATCH] Added some example files. --- examples/dtmc/synchronous_leader/leader.pctl | 3 ++- examples/mdp/consensus/coin.pctl | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/examples/dtmc/synchronous_leader/leader.pctl b/examples/dtmc/synchronous_leader/leader.pctl index b14536d80..c4eb53408 100644 --- a/examples/dtmc/synchronous_leader/leader.pctl +++ b/examples/dtmc/synchronous_leader/leader.pctl @@ -1,3 +1,4 @@ P=? [ F elected ] -P=? [ F<=(4*(N+1)) elected ] +// P=? [ F<=(4*(N+1)) elected ] +P=? [ F<=28 elected ] R=? [ F elected ] diff --git a/examples/mdp/consensus/coin.pctl b/examples/mdp/consensus/coin.pctl index aa371d50b..edd87a453 100644 --- a/examples/mdp/consensus/coin.pctl +++ b/examples/mdp/consensus/coin.pctl @@ -11,8 +11,8 @@ Pmin=? [ F finished & all_coins_equal_1 ] Pmax=? [ F finished & !agree ] // Min/max probability of finishing within k steps -Pmin=? [ F<=k finished ] -Pmax=? [ F<=k finished ] +Pmin=? [ F<=50 finished ] +Pmax=? [ F<=50 finished ] // Min/max expected steps to finish Rmin=? [ F finished ]