s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Out of date file in phil-nofair. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1919 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 16 years ago
parent
ddcb377e8c
commit
211be9eb3c
1 changed files with 57 additions and 54 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 111
      prism-examples/phil/nofair/phil-nofair10.nm

111
prism-examples/phil/nofair/phil-nofair10.nm
View File

@ -1,54 +1,57 @@
// randomized dining philosophers [LR81]
// dxp/gxn 23/01/02
// model which does not require fairness
// remove the possibility of loops:
// (1) cannot stay in thinking
// (2) if first fork not free then cannot move (another philosopher must more)
mdp
// atomic formulae
// left fork free and right fork free resp.
formula lfree = p2=0..4,6,10;
formula rfree = p10=0..3,5,7,11;
module phil1
p1: [0..11];
[] p1=0 -> (p1'=1); // trying
[] p1=1 -> 0.5 : (p1'=2) + 0.5 : (p1'=3); // draw randomly
[] p1=2 & lfree -> (p1'=4); // pick up left
[] p1=3 & rfree -> (p1'=5); // pick up right
[] p1=4 & rfree -> (p1'=8); // pick up right (got left)
[] p1=4 & !rfree -> (p1'=6); // right not free (got left)
[] p1=5 & lfree -> (p1'=8); // pick up left (got right)
[] p1=5 & !lfree -> (p1'=7); // left not free (got right)
[] p1=6 -> (p1'=1); // put down left
[] p1=7 -> (p1'=1); // put down right
[] p1=8 -> (p1'=9); // move to eating (got forks)
[] p1=9 -> (p1'=10); // finished eating and put down left
[] p1=9 -> (p1'=11); // finished eating and put down right
[] p1=10 -> (p1'=0); // put down right and return to think
[] p1=11 -> (p1'=0); // put down left and return to think
endmodule
// construct further modules through renaming
module phil2 = phil1 [p1=p2, p2=p3, p10=p1] endmodule
module phil3 = phil1 [p1=p3, p2=p4, p10=p2] endmodule
module phil4 = phil1 [p1=p4, p2=p5, p10=p3] endmodule
module phil5 = phil1 [p1=p5, p2=p6, p10=p4] endmodule
module phil6 = phil1 [p1=p6, p2=p7, p10=p5] endmodule
module phil7 = phil1 [p1=p7, p2=p8, p10=p6] endmodule
module phil8 = phil1 [p1=p8, p2=p9, p10=p7] endmodule
module phil9 = phil1 [p1=p9, p2=p10, p10=p8] endmodule
module phil10 = phil1 [p1=p10, p2=p1, p10=p9] endmodule
// rewards (number of steps)
rewards
[] true : 1;
endrewards
// randomized dining philosophers [LR81]
// dxp/gxn 23/01/02
// model which does not require fairness
// remove the possibility of loops:
// (1) cannot stay in thinking
// (2) if first fork not free then cannot move (another philosopher must more)
mdp
// atomic formulae
// left fork free and right fork free resp.
formula lfree = (p2>=0&p2<=4)|p2=6|p2=10;
formula rfree = (p10>=0&p10<=3)|p10=5|p10=7|p10=11;
module phil1
p1: [0..11];
[] p1=0 -> (p1'=1); // trying
[] p1=1 -> 0.5 : (p1'=2) + 0.5 : (p1'=3); // draw randomly
[] p1=2 & lfree -> (p1'=4); // pick up left
[] p1=3 & rfree -> (p1'=5); // pick up right
[] p1=4 & rfree -> (p1'=8); // pick up right (got left)
[] p1=4 & !rfree -> (p1'=6); // right not free (got left)
[] p1=5 & lfree -> (p1'=8); // pick up left (got right)
[] p1=5 & !lfree -> (p1'=7); // left not free (got right)
[] p1=6 -> (p1'=1); // put down left
[] p1=7 -> (p1'=1); // put down right
[] p1=8 -> (p1'=9); // move to eating (got forks)
[] p1=9 -> (p1'=10); // finished eating and put down left
[] p1=9 -> (p1'=11); // finished eating and put down right
[] p1=10 -> (p1'=0); // put down right and return to think
[] p1=11 -> (p1'=0); // put down left and return to think
endmodule
// construct further modules through renaming
module phil2 = phil1 [ p1=p2, p2=p3, p10=p1 ] endmodule
module phil3 = phil1 [ p1=p3, p2=p4, p10=p2 ] endmodule
module phil4 = phil1 [ p1=p4, p2=p5, p10=p3 ] endmodule
module phil5 = phil1 [ p1=p5, p2=p6, p10=p4 ] endmodule
module phil6 = phil1 [ p1=p6, p2=p7, p10=p5 ] endmodule
module phil7 = phil1 [ p1=p7, p2=p8, p10=p6 ] endmodule
module phil8 = phil1 [ p1=p8, p2=p9, p10=p7 ] endmodule
module phil9 = phil1 [ p1=p9, p2=p10, p10=p8 ] endmodule
module phil10 = phil1 [ p1=p10, p2=p1, p10=p9 ] endmodule
// rewards (number of steps)
rewards "num_steps"
[] true : 1;
endrewards
// labels
label "hungry" = ((p1>0)&(p1<8))|((p2>0)&(p2<8))|((p3>0)&(p3<8))|((p4>0)&(p4<8))|((p5>0)&(p5<8))|((p6>0)&(p6<8))|((p7>0)&(p7<8))|((p8>0)&(p8<8))|((p9>0)&(p9<8))|((p10>0)&(p10<8));
label "eat" = ((p1>=8)&(p1<=9))|((p2>=8)&(p2<=9))|((p3>=8)&(p3<=9))|((p4>=8)&(p4<=9))|((p5>=8)&(p5<=9))|((p6>=8)&(p6<=9))|((p7>=8)&(p7<=9))|((p8>=8)&(p8<=9))|((p9>=8)&(p9<=9))|((p10>=8)&(p10<=9));
Write Preview
Loading…
Cancel
Save