From dd3a53f34b6bbaa7adcc74a009972112b93157d8 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 5 Dec 2008 15:45:23 +0000 Subject: [PATCH] Removed fairness info. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@868 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/consensus/coin.pctl | 3 --- 1 file changed, 3 deletions(-) diff --git a/prism-examples/consensus/coin.pctl b/prism-examples/consensus/coin.pctl index e26c623e..c85f10f4 100644 --- a/prism-examples/consensus/coin.pctl +++ b/prism-examples/consensus/coin.pctl @@ -1,18 +1,15 @@ const int k; // C1 (with probability 1, all N processes finish the protocol) -// (needs fairness) P>=1 [ F "finished" ] // 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 // Analytic bound is (K-1)/(2*K) Pmin=? [ F "finished"&"all_coins_equal_0" ] Pmin=? [ F "finished"&"all_coins_equal_1" ] // Max probability of finishing protocol with coins not all equal -// (no fairness needed since max. probabilities) Pmax=? [ F "finished"&!"agree" ] // Min/max probability of finishing within k steps