From a11a6457ac681724fc9f3b2ceb0ff7d7160641fc Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Wed, 3 Dec 2008 16:52:04 +0000 Subject: [PATCH] minor fixes git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@842 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/rabin/modified/.autopp | 2 +- .../rabin/modified/.mod_rabinN.nm.pp | 2 +- prism-examples/rabin/modified/.rabinN.nm.pp | 71 ------------------- 3 files changed, 2 insertions(+), 73 deletions(-) delete mode 100644 prism-examples/rabin/modified/.rabinN.nm.pp diff --git a/prism-examples/rabin/modified/.autopp b/prism-examples/rabin/modified/.autopp index ca9b6c18..a130c69e 100755 --- a/prism-examples/rabin/modified/.autopp +++ b/prism-examples/rabin/modified/.autopp @@ -1,6 +1,6 @@ #!/bin/csh -foreach N ( 3 4 5 6 7 8) +foreach N ( 3 4 5 6 7 8 9 10 ) echo "Generating for N=$N" prismpp .mod_rabinN.nm.pp $N >! mod_rabin$N.nm unix2dos mod_rabin$N.nm diff --git a/prism-examples/rabin/modified/.mod_rabinN.nm.pp b/prism-examples/rabin/modified/.mod_rabinN.nm.pp index 49c79f24..96129a6b 100644 --- a/prism-examples/rabin/modified/.mod_rabinN.nm.pp +++ b/prism-examples/rabin/modified/.mod_rabinN.nm.pp @@ -86,4 +86,4 @@ label "one_trying" = #| i=1:N#p#i#=1#end#; label "one_critical" = #| i=1:N#p#i#=2#end#; // maximum value of the bi's -formula maxb = max(b1#for i=2:N#,b#i# #end#); +formula maxb = max(b1#for i=2:N#,b#i##end#); diff --git a/prism-examples/rabin/modified/.rabinN.nm.pp b/prism-examples/rabin/modified/.rabinN.nm.pp deleted file mode 100644 index 0341e44c..00000000 --- a/prism-examples/rabin/modified/.rabinN.nm.pp +++ /dev/null @@ -1,71 +0,0 @@ -#const N# -#const K=4+func(ceil,func(log,N,2))# -// N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization -// gxn/dxp 02/02/00 - -mdp - -// size of shared counter -const int K = #K#; // 4+ceil(log_2 N) - -// global variables (all modules can read and write) -// c=0 critical section free -// c=1 critical section not free -// b current highest draw -// r current round - -global c : [0..1]; -global b : [0..K]; -global r : [1..2]; - -// local variables: process i -// state: pi -// 0 remainder -// 1 trying -// 2 critical section -// current draw: bi -// current round: ri - -// atomic formula for process 1 drawing -formula draw = p1=1 & (b (p1'=0); - // enter trying - [] p1=0 -> (p1'=1); - // make a draw - [] draw ->#+ i=1:K-1# #1/func(floor,func(pow,2,i))# : (b1'=#i#) & (r1'=r) & (b'=max(b,#i#)) - #end#+ #1/func(floor,func(pow,2,K-1))# : (b1'=#K#) & (r1'=r) & (b'=max(b,#K#)); - // enter critical section and randomly set r to 1 or 2 - [] p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) - + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); - // loop when trying and cannot make a draw or enter critical section - [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); - // leave crictical section - [] p1=2 -> (p1'=0) & (c'=0); - // stay in critical section - [] p1=2 -> (p1'=2); - -endmodule - -// construct further modules through renaming -#for i=2:N# -module process#i# = process1 [p1=p#i#, b1=b#i#, r1=r#i#] endmodule #end# - -// formulas/labels for use in properties: - -// number of processes in critical section -formula num_procs_in_crit = #+ i=1:N#(p#i#=2?1:0)#end#; - -// one of the processes is trying -label "one_trying" = #| i=1:N#p#i#=1#end#; - -// one of the processes is in the critical section -label "one_critical" = #| i=1:N#p#i#=2#end#;