From 0f545630ebffcab8df1b45417a1aec5d7519375d Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Wed, 8 May 2013 14:56:48 +0200 Subject: [PATCH] Adapted the pctl files according to our format. --- examples/dtmc/crowds/crowds.pctl | 6 ++--- examples/dtmc/die/die.pctl | 8 +++---- examples/dtmc/synchronous_leader/leader.pctl | 6 ++--- examples/mdp/asynchronous_leader/leader.pctl | 10 ++++---- examples/mdp/consensus/coin.pctl | 16 ++++++------- examples/mdp/two_dice/two_dice.pctl | 24 ++++++++++---------- 6 files changed, 35 insertions(+), 35 deletions(-) diff --git a/examples/dtmc/crowds/crowds.pctl b/examples/dtmc/crowds/crowds.pctl index a7c83e667..653da5713 100644 --- a/examples/dtmc/crowds/crowds.pctl +++ b/examples/dtmc/crowds/crowds.pctl @@ -1,3 +1,3 @@ -P=? [ F "observe0Greater1" ] -P=? [ F "observeIGreater1" ] -P=? [ F "observeOnlyTrueSender" ] +P=? [ F observe0Greater1 ] +P=? [ F observeIGreater1 ] +P=? [ F observeOnlyTrueSender ] diff --git a/examples/dtmc/die/die.pctl b/examples/dtmc/die/die.pctl index b0eb88dcd..8deea6c43 100644 --- a/examples/dtmc/die/die.pctl +++ b/examples/dtmc/die/die.pctl @@ -1,4 +1,4 @@ -P=? [ F "one" ] -P=? [ F "two" ] -P=? [ F "three" ] -R=? [ F "done" ] +P=? [ F one ] +P=? [ F two ] +P=? [ F three ] +R=? [ F done ] diff --git a/examples/dtmc/synchronous_leader/leader.pctl b/examples/dtmc/synchronous_leader/leader.pctl index e8b1899e6..b14536d80 100644 --- a/examples/dtmc/synchronous_leader/leader.pctl +++ b/examples/dtmc/synchronous_leader/leader.pctl @@ -1,3 +1,3 @@ -P=? [ F "elected" ] -P=? [ F<=(4*(N+1)) "elected" ] -R=? [ F "elected" ] +P=? [ F elected ] +P=? [ F<=(4*(N+1)) elected ] +R=? [ F elected ] diff --git a/examples/mdp/asynchronous_leader/leader.pctl b/examples/mdp/asynchronous_leader/leader.pctl index 49e4dbeaa..bb8fb1b82 100644 --- a/examples/mdp/asynchronous_leader/leader.pctl +++ b/examples/mdp/asynchronous_leader/leader.pctl @@ -1,8 +1,8 @@ -Pmin=? [ F "elected" ] +Pmin=? [ F elected ] const int K = 25; -Pmin=? [ F<=K "elected" ] -Pmax=? [ F<=K "elected" ] +Pmin=? [ F<=K elected ] +Pmax=? [ F<=K elected ] -Rmin=? [ F "elected" ] -Rmax=? [ F "elected" ] +Rmin=? [ F elected ] +Rmax=? [ F elected ] diff --git a/examples/mdp/consensus/coin.pctl b/examples/mdp/consensus/coin.pctl index 52a308559..aa371d50b 100644 --- a/examples/mdp/consensus/coin.pctl +++ b/examples/mdp/consensus/coin.pctl @@ -1,20 +1,20 @@ // C1 (with probability 1, all N processes finish the protocol) -Pmin=? [ F "finished" ] +Pmin=? [ F finished ] // C2 (minimum probability that the protocol finishes with all coins equal to v) (v=1,2) // Results are same for v=1 and v=2 by symmetry // Analytic bound is (K-1)/(2*K) -Pmin=? [ F "finished"&"all_coins_equal_0" ] -Pmin=? [ F "finished"&"all_coins_equal_1" ] +Pmin=? [ F finished & all_coins_equal_0 ] +Pmin=? [ F finished & all_coins_equal_1 ] // Max probability of finishing protocol with coins not all equal -Pmax=? [ F "finished"&!"agree" ] +Pmax=? [ F finished & !agree ] // Min/max probability of finishing within k steps -Pmin=? [ F<=k "finished" ] -Pmax=? [ F<=k "finished" ] +Pmin=? [ F<=k finished ] +Pmax=? [ F<=k finished ] // Min/max expected steps to finish -Rmin=? [ F "finished" ] -Rmax=? [ F "finished" ] +Rmin=? [ F finished ] +Rmax=? [ F finished ] diff --git a/examples/mdp/two_dice/two_dice.pctl b/examples/mdp/two_dice/two_dice.pctl index 10cdff821..4ad376feb 100644 --- a/examples/mdp/two_dice/two_dice.pctl +++ b/examples/mdp/two_dice/two_dice.pctl @@ -1,13 +1,13 @@ -Pmin=? [ F "two" ] -Pmax=? [ F "two" ] -Pmin=? [ F "three" ] -Pmax=? [ F "three" ] -Pmin=? [ F "four" ] -Pmax=? [ F "four" ] -Pmin=? [ F "five" ] -Pmax=? [ F "five" ] -Pmin=? [ F "six" ] -Pmax=? [ F "six" ] +Pmin=? [ F two ] +Pmax=? [ F two ] +Pmin=? [ F three ] +Pmax=? [ F three ] +Pmin=? [ F four ] +Pmax=? [ F four ] +Pmin=? [ F five ] +Pmax=? [ F five ] +Pmin=? [ F six ] +Pmax=? [ F six ] -Rmin=? [ F "done" ] -Rmax=? [ F "done" ] +Rmin=? [ F done ] +Rmax=? [ F done ]