From 79d5ff124be9673b79b69c7a33716a103e9c931c Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Mon, 26 Nov 2007 11:23:33 +0000 Subject: [PATCH] updated properties and rewards in phil (no fair) git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@533 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/phil/nofair/phil-nofair10.nm | 4 ++-- prism-examples/phil/nofair/phil-nofair3.nm | 8 +++----- prism-examples/phil/nofair/phil-nofair4.nm | 4 ++-- prism-examples/phil/nofair/phil-nofair5.nm | 4 ++-- prism-examples/phil/nofair/phil-nofair6.nm | 4 ++-- prism-examples/phil/nofair/phil-nofair7.nm | 4 ++-- prism-examples/phil/nofair/phil-nofair8.nm | 4 ++-- prism-examples/phil/nofair/phil-nofair9.nm | 7 ++++++- prism-examples/phil/nofair/phil3.pctl | 8 ++++++-- prism-examples/phil/nofair/phil4.pctl | 6 +++++- prism-examples/phil/nofair/phil5.pctl | 6 +++++- prism-examples/phil/nofair/phil6.pctl | 6 +++++- prism-examples/phil/nofair/phil7.pctl | 6 +++++- prism-examples/phil/nofair/phil8.pctl | 6 +++++- prism-examples/phil/nofair/phil9.pctl | 6 +++++- 15 files changed, 57 insertions(+), 26 deletions(-) diff --git a/prism-examples/phil/nofair/phil-nofair10.nm b/prism-examples/phil/nofair/phil-nofair10.nm index f87ad031..f4c918b4 100644 --- a/prism-examples/phil/nofair/phil-nofair10.nm +++ b/prism-examples/phil/nofair/phil-nofair10.nm @@ -1,11 +1,11 @@ // 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) -// dxp/gxn 23/01/02 - nondeterministic // atomic formulae diff --git a/prism-examples/phil/nofair/phil-nofair3.nm b/prism-examples/phil/nofair/phil-nofair3.nm index 0ec17866..ae71ccbc 100644 --- a/prism-examples/phil/nofair/phil-nofair3.nm +++ b/prism-examples/phil/nofair/phil-nofair3.nm @@ -1,11 +1,11 @@ // 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) -// dxp/gxn 23/01/02 - nondeterministic // atomic formulae @@ -40,8 +40,6 @@ module phil2 = phil1 [p1=p2, p2=p3, p3=p1] endmodule module phil3 = phil1 [p1=p3, p2=p1, p3=p2] endmodule // rewards (number of steps) -rewards - +rewards "steps" [] true : 1; - endrewards diff --git a/prism-examples/phil/nofair/phil-nofair4.nm b/prism-examples/phil/nofair/phil-nofair4.nm index 523c4ea7..70c0718c 100644 --- a/prism-examples/phil/nofair/phil-nofair4.nm +++ b/prism-examples/phil/nofair/phil-nofair4.nm @@ -1,11 +1,11 @@ // 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) -// dxp/gxn 23/01/02 - nondeterministic // atomic formulae diff --git a/prism-examples/phil/nofair/phil-nofair5.nm b/prism-examples/phil/nofair/phil-nofair5.nm index 4f7ea8b9..5f4653d7 100644 --- a/prism-examples/phil/nofair/phil-nofair5.nm +++ b/prism-examples/phil/nofair/phil-nofair5.nm @@ -1,11 +1,11 @@ // 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) -// dxp/gxn 23/01/02 - nondeterministic // atomic formulae diff --git a/prism-examples/phil/nofair/phil-nofair6.nm b/prism-examples/phil/nofair/phil-nofair6.nm index e8c637ea..17cc7f33 100644 --- a/prism-examples/phil/nofair/phil-nofair6.nm +++ b/prism-examples/phil/nofair/phil-nofair6.nm @@ -1,11 +1,11 @@ // 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) -// dxp/gxn 23/01/02 - nondeterministic // atomic formulae diff --git a/prism-examples/phil/nofair/phil-nofair7.nm b/prism-examples/phil/nofair/phil-nofair7.nm index 8b2dac40..e246ca65 100644 --- a/prism-examples/phil/nofair/phil-nofair7.nm +++ b/prism-examples/phil/nofair/phil-nofair7.nm @@ -1,11 +1,11 @@ // 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) -// dxp/gxn 23/01/02 - nondeterministic // atomic formulae diff --git a/prism-examples/phil/nofair/phil-nofair8.nm b/prism-examples/phil/nofair/phil-nofair8.nm index f428e503..8b4086ab 100644 --- a/prism-examples/phil/nofair/phil-nofair8.nm +++ b/prism-examples/phil/nofair/phil-nofair8.nm @@ -1,11 +1,11 @@ // 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) -// dxp/gxn 23/01/02 - nondeterministic // atomic formulae diff --git a/prism-examples/phil/nofair/phil-nofair9.nm b/prism-examples/phil/nofair/phil-nofair9.nm index 600d9b77..f59d1aa3 100644 --- a/prism-examples/phil/nofair/phil-nofair9.nm +++ b/prism-examples/phil/nofair/phil-nofair9.nm @@ -1,5 +1,10 @@ // randomized dining philosophers [LR81] -// dxp/gxn 12/12/99 +// 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) nondeterministic diff --git a/prism-examples/phil/nofair/phil3.pctl b/prism-examples/phil/nofair/phil3.pctl index d4102109..2bd8e2f6 100644 --- a/prism-examples/phil/nofair/phil3.pctl +++ b/prism-examples/phil/nofair/phil3.pctl @@ -1,9 +1,13 @@ +const int K; // discrete time bound + label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)); label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9); + // liveness (if a philosopher is hungry then eventually some philosopher eats) "hungry" => P>=1 [ true U "eat"] + // bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -const int K; Pmin=?[true U<=K "eat" {"hungry"}{min}] + // expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) -Rmax=?[F "eat" {"hungry"}{max}] +Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil4.pctl b/prism-examples/phil/nofair/phil4.pctl index da08449b..6bd3cfdd 100644 --- a/prism-examples/phil/nofair/phil4.pctl +++ b/prism-examples/phil/nofair/phil4.pctl @@ -1,9 +1,13 @@ +const int K; // discrete time bound + label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)); label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9); + // liveness (if a philosopher is hungry then eventually some philosopher eats) "hungry" => P>=1 [ true U "eat"] + // bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -const int K; Pmin=?[true U<=K "eat" {"hungry"}{min}] + // expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil5.pctl b/prism-examples/phil/nofair/phil5.pctl index 601d645e..9e9c134a 100644 --- a/prism-examples/phil/nofair/phil5.pctl +++ b/prism-examples/phil/nofair/phil5.pctl @@ -1,9 +1,13 @@ +const int K; // discrete time bound + label "hungry" = ((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)) | ((p5>0) & (p5<8)); label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9); + // liveness (if a philosopher is hungry then eventually some philosopher eats) "hungry" => P>=1 [ true U "eat"] + // bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -const int K; Pmin=?[true U<=K "eat" {"hungry"}{min}] + // expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil6.pctl b/prism-examples/phil/nofair/phil6.pctl index 061f5f13..f490a4d0 100644 --- a/prism-examples/phil/nofair/phil6.pctl +++ b/prism-examples/phil/nofair/phil6.pctl @@ -1,9 +1,13 @@ +const int K; // discrete time bound + 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)); label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9); + // liveness (if a philosopher is hungry then eventually some philosopher eats) "hungry" => P>=1 [ true U "eat"] + // bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -const int K; Pmin=?[true U<=K "eat" {"hungry"}{min}] + // expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil7.pctl b/prism-examples/phil/nofair/phil7.pctl index f066e390..3697d135 100644 --- a/prism-examples/phil/nofair/phil7.pctl +++ b/prism-examples/phil/nofair/phil7.pctl @@ -1,9 +1,13 @@ +const int K; // discrete time bound + 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)); label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9); + // liveness (if a philosopher is hungry then eventually some philosopher eats) "hungry" => P>=1 [ true U "eat"] + // bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -const int K; Pmin=?[true U<=K "eat" {"hungry"}{min}] + // expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil8.pctl b/prism-examples/phil/nofair/phil8.pctl index 2ae5a24b..1c0eee27 100644 --- a/prism-examples/phil/nofair/phil8.pctl +++ b/prism-examples/phil/nofair/phil8.pctl @@ -1,9 +1,13 @@ +const int K; // discrete time bound + 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)); label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9) | (p8=8..9); + // liveness (if a philosopher is hungry then eventually some philosopher eats) "hungry" => P>=1 [ true U "eat"] + // bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -const int K; Pmin=?[true U<=K "eat" {"hungry"}{min}] + // expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) Rmax=?[F "eat" {"hungry"}{max}] diff --git a/prism-examples/phil/nofair/phil9.pctl b/prism-examples/phil/nofair/phil9.pctl index effe602f..6190fb92 100644 --- a/prism-examples/phil/nofair/phil9.pctl +++ b/prism-examples/phil/nofair/phil9.pctl @@ -1,9 +1,13 @@ +const int K; // discrete time bound + 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)); label "eat" = (p1=8..9) | (p2=8..9) | (p3=8..9) | (p4=8..9) | (p5=8..9) | (p6=8..9) | (p7=8..9) | (p8=8..9) | (p9=8..9); + // liveness (if a philosopher is hungry then eventually some philosopher eats) "hungry" => P>=1 [ true U "eat"] + // bounded until (minimum probability, from a state where someone is hungry, that a philosopher will eat within K steps) -const int K; Pmin=?[true U<=K "eat" {"hungry"}{min}] + // expected time (from a state where someone is hungry the maximum exapected number of steps until a philosopher eats) Rmax=?[F "eat" {"hungry"}{max}]