From 6bd499220ee960baa85874e8ae352d91e46e7cad Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Mon, 8 Dec 2008 09:52:21 +0000 Subject: [PATCH] update to auto file git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@877 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/rabin/.rabinN.nm.pp | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/prism-examples/rabin/.rabinN.nm.pp b/prism-examples/rabin/.rabinN.nm.pp index 2ea483d7..8e357b64 100644 --- a/prism-examples/rabin/.rabinN.nm.pp +++ b/prism-examples/rabin/.rabinN.nm.pp @@ -3,18 +3,15 @@ // N-processor mutual exclusion [Rab82] // gxn/dxp 03/12/08 -// modified version to analyse the bounded waiting property -// more precisely we analyse the waeker property: -// "the minimum probability a process enters the critical section given the process tries" - -// we modify the model by dividing the step corresponding to a process making a draw into two steps -// this allows one to identify states where a process will draw without knowing -// what value the process will randomly pick -// these two steps are atomic (i.e. no other process can move one the first step has been made) -// as otherwise the adversary can prevent the process from actually drawing in the current round -// by not scheduling it after it has performed the first step - // to remove the need for fairness constraints we have also removed the self loops from the model + +// the step corresponding to a process making a draw has been split into two steps +// to allow us to identify states where a process will draw without knowing the value +// randomly drawn +// to correctly model the protocol and prevent erroneous behaviour, the two steps are atomic +// (i.e. no other process can move one the first step has been made) +// as for example otherwise an adversary can prevent the process from actually drawing +// in the current round by not scheduling it after it has performed the first step mdp