From 7ca42448902a05d3b7cae1a579cd6530e9fbaf13 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 16 Jun 2011 06:43:03 +0000 Subject: [PATCH] Few more fixes in examples re new semantics. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3091 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/leader/asynchronous/leader.pctl | 12 +++++++----- prism-examples/leader/synchronous/leader.pctl | 6 +++--- .../self-stabilisation/beauquier/beauquier.pctl | 2 +- prism-examples/self-stabilisation/herman/herman.pctl | 2 +- .../self-stabilisation/israeli-jalfon/ij.pctl | 2 +- 5 files changed, 13 insertions(+), 11 deletions(-) diff --git a/prism-examples/leader/asynchronous/leader.pctl b/prism-examples/leader/asynchronous/leader.pctl index 0152e1a9..26572774 100644 --- a/prism-examples/leader/asynchronous/leader.pctl +++ b/prism-examples/leader/asynchronous/leader.pctl @@ -1,12 +1,14 @@ // only one leader is elected -leaders<=1 +fiter(forall, leaders<=1) // with probability 1 eventually a leader is elected P>=1 [ F "elected" ] + // min/max probability leader is elected within K steps const int K; -Pmin=?[ F<=K "elected" ] -Pmax=?[ F<=K "elected" ] +Pmin=? [ F<=K "elected" ] +Pmax=? [ F<=K "elected" ] + // the min/max expected time to elect a leader -Rmin=?[ F "elected" ] -Rmax=?[ F "elected" ] +Rmin=? [ F "elected" ] +Rmax=? [ F "elected" ] diff --git a/prism-examples/leader/synchronous/leader.pctl b/prism-examples/leader/synchronous/leader.pctl index 4b443da5..d276987a 100644 --- a/prism-examples/leader/synchronous/leader.pctl +++ b/prism-examples/leader/synchronous/leader.pctl @@ -1,10 +1,10 @@ const int L; - + // Probability that a leader is eventually elected -P=? [ F "elected" ] +P=? [ F "elected" ] // Probability that a leader is elected within L rounds P=? [ F<=(L*(N+1)) "elected" ] - + // Expected time (num. rounds) to elect a leader R{"num_rounds"}=? [ F "elected" ] diff --git a/prism-examples/self-stabilisation/beauquier/beauquier.pctl b/prism-examples/self-stabilisation/beauquier/beauquier.pctl index 82f6df27..1269024d 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier.pctl +++ b/prism-examples/self-stabilisation/beauquier/beauquier.pctl @@ -6,7 +6,7 @@ label "k_tokens" = num_tokens=k; // configurations with k tokens label "stable" = num_tokens=1; // stable configurations (1 token) // From any configuration, a stable configuration is reached with probability 1 -filter(forall, P>=1 [ F "stable" ], "init") +filter(forall, "init" => P>=1 [ F "stable" ]) // Maximum expected time to reach a stable configuration (for all configurations) Rmax=? [ F "stable" {"init"}{max} ] diff --git a/prism-examples/self-stabilisation/herman/herman.pctl b/prism-examples/self-stabilisation/herman/herman.pctl index 0873eee8..3c419afb 100644 --- a/prism-examples/self-stabilisation/herman/herman.pctl +++ b/prism-examples/self-stabilisation/herman/herman.pctl @@ -5,7 +5,7 @@ const int K; // number of steps label "k_tokens" = num_tokens=k; // configurations with k tokens // From any configuration, a stable configuration is reached with probability 1 -filter(forall, P>=1 [ F "stable" ], "init") +filter(forall, "init" => P>=1 [ F "stable" ]) // Maximum expected time to reach a stable configuration (for all configurations) R=? [ F "stable" {"init"}{max} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl index 69358e02..76c9ffbb 100644 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl +++ b/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl @@ -5,7 +5,7 @@ const int K; // number of steps label "k_tokens" = num_tokens=k; // configurations with k tokens // From any configuration, a stable configuration is reached with probability 1 -filter(forall, P>=1 [ F "stable" ], "init") +filter(forall, "init" => P>=1 [ F "stable" ]) // Maximum expected time to reach a stable configuration (for all configurations) Rmax=? [ F "stable" {"init"}{max} ]