From 25adf30f265970da7155ba022909bb96e12535cd Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Sun, 30 May 2010 20:53:46 +0000 Subject: [PATCH] Line endings. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1922 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/phil/nofair/.phil-nofairN.nm.pp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/prism-examples/phil/nofair/.phil-nofairN.nm.pp b/prism-examples/phil/nofair/.phil-nofairN.nm.pp index 91189524..3595908a 100644 --- a/prism-examples/phil/nofair/.phil-nofairN.nm.pp +++ b/prism-examples/phil/nofair/.phil-nofairN.nm.pp @@ -1,4 +1,4 @@ -#const N# +#const N# // randomized dining philosophers [LR81] // dxp/gxn 23/01/02 @@ -11,8 +11,8 @@ mdp // atomic formulae // left fork free and right fork free resp. -formula lfree = (p2>=0&p2<=4)|p2=6|p2=10; -formula rfree = (p#N#>=0&p#N#<=3)|p#N#=5|p#N#=7|p#N#=11; +formula lfree = (p2>=0&p2<=4)|p2=6|p2=10; +formula rfree = (p#N#>=0&p#N#<=3)|p#N#=5|p#N#=7|p#N#=11; module phil1 @@ -36,17 +36,17 @@ module phil1 endmodule -// construct further modules through renaming +// construct further modules through renaming #for i=2:N# module phil#i# = phil1 [ p1=p#i#, p2=p#mod(i,N)+1#, p#N#=p#mod(i-2,N)+1# ] endmodule -#end# - +#end# + // rewards (number of steps) rewards "num_steps" [] true : 1; endrewards -// labels +// labels label "hungry" = #| i=1:N#((p#i#>0)&(p#i#<8))#end#; label "eat" = #| i=1:N#((p#i#>=8)&(p#i#<=9))#end#; - +