s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Removed fairness info. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@868 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 17 years ago
parent
ff749eb06e
commit
dd3a53f34b
1 changed files with 0 additions and 3 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 3
      prism-examples/consensus/coin.pctl

3
prism-examples/consensus/coin.pctl
View File

@ -1,18 +1,15 @@
const int k; const int k;
// C1 (with probability 1, all N processes finish the protocol) // C1 (with probability 1, all N processes finish the protocol)
// (needs fairness)
P>=1 [ F "finished" ] P>=1 [ F "finished" ]
// C2 (minimum probability that the protocol finishes with all coins equal to v) (v=1,2) // C2 (minimum probability that the protocol finishes with all coins equal to v) (v=1,2)
// (needs fairness)
// Results are same for v=1 and v=2 by symmetry // Results are same for v=1 and v=2 by symmetry
// Analytic bound is (K-1)/(2*K) // Analytic bound is (K-1)/(2*K)
Pmin=? [ F "finished"&"all_coins_equal_0" ] Pmin=? [ F "finished"&"all_coins_equal_0" ]
Pmin=? [ F "finished"&"all_coins_equal_1" ] Pmin=? [ F "finished"&"all_coins_equal_1" ]
// Max probability of finishing protocol with coins not all equal // Max probability of finishing protocol with coins not all equal
// (no fairness needed since max. probabilities)
Pmax=? [ F "finished"&!"agree" ] Pmax=? [ F "finished"&!"agree" ]
// Min/max probability of finishing within k steps // Min/max probability of finishing within k steps

Write Preview
Loading…
Cancel
Save