|
|
|
@ -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#; |
|
|
|
|
|
|
|
|
|
|
|
|