From a48e12befe7a727519bbfc7d722b05a6c253ffc5 Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Mon, 26 Nov 2007 11:20:09 +0000 Subject: [PATCH] updated reward structures in phil_lss files git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@531 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/phil_lss/phil_lss3.nm | 8 +++----- prism-examples/phil_lss/phil_lss3.pctl | 11 ++++++----- prism-examples/phil_lss/phil_lss4.nm | 8 +++----- prism-examples/phil_lss/phil_lss4.pctl | 11 ++++++----- 4 files changed, 18 insertions(+), 20 deletions(-) diff --git a/prism-examples/phil_lss/phil_lss3.nm b/prism-examples/phil_lss/phil_lss3.nm index b43aab7f..ff56d849 100644 --- a/prism-examples/phil_lss/phil_lss3.nm +++ b/prism-examples/phil_lss/phil_lss3.nm @@ -91,11 +91,9 @@ endmodule module phil2=phil1 [p1=p2, p2=p3, p3=p1, s1=s2] endmodule module phil3=phil1 [p1=p3, p2=p1, p3=p2, s1=s3] endmodule -// rewards - expected number of steps -rewards - +// reward structure - number of steps +rewards "steps" [s1] true : 1; [s2] true : 1; [s3] true : 1; - -endrewards +endrewards diff --git a/prism-examples/phil_lss/phil_lss3.pctl b/prism-examples/phil_lss/phil_lss3.pctl index 261c9fcc..4230929b 100644 --- a/prism-examples/phil_lss/phil_lss3.pctl +++ b/prism-examples/phil_lss/phil_lss3.pctl @@ -1,12 +1,13 @@ -// philosopher in its trying region -label "trying" =((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)); -// philosopher in its critical section -label "entered" =((p1>7) & (p1<13)) | ((p2>7) & (p2<13)) | ((p3>7) & (p3<13)); +const int L; // discrete time bound + +label "trying" =((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)); // philosopher in its trying region +label "entered" =((p1>7) & (p1<13)) | ((p2>7) & (p2<13)) | ((p3>7) & (p3<13)); // philosopher in its critical section // lockout free "trying" => P>=1 [ true U "entered" ] + // bounded until: minimum probability (from a state where a process is in its trying region) that some process enters its critical section within k steps -const int L; Pmin=? [ true U<=L "entered" {"trying"}{min} ] + // expected time: maximum expected time (from a state where a process is in its trying region) that some process enters its critical section Rmax=? [ F "entered" {"trying"}{max} ] diff --git a/prism-examples/phil_lss/phil_lss4.nm b/prism-examples/phil_lss/phil_lss4.nm index c2b2a0d9..3326c901 100644 --- a/prism-examples/phil_lss/phil_lss4.nm +++ b/prism-examples/phil_lss/phil_lss4.nm @@ -119,12 +119,10 @@ module phil2=phil1 [p1=p2, p2=p3, p3=p4, p4=p1, s1=s2] endmodule module phil3=phil1 [p1=p3, p2=p4, p3=p1, p4=p2, s1=s3] endmodule module phil4=phil1 [p1=p4, p2=p1, p3=p2, p4=p3, s1=s4] endmodule -// rewards - expected number of steps -rewards - +// reward structure - number of steps +rewards "steps" [s1] true : 1; [s2] true : 1; [s3] true : 1; [s4] true : 1; - -endrewards +endrewards diff --git a/prism-examples/phil_lss/phil_lss4.pctl b/prism-examples/phil_lss/phil_lss4.pctl index 4ce228e6..a87e7d9a 100644 --- a/prism-examples/phil_lss/phil_lss4.pctl +++ b/prism-examples/phil_lss/phil_lss4.pctl @@ -1,12 +1,13 @@ -// philosopher in its trying region -label "trying" =((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)); -// philosopher in its critical section -label "entered" =((p1>7) & (p1<13)) | ((p2>7) & (p2<13)) | ((p3>7) & (p3<13)) | ((p4>7) & (p4<13)); +const int L; // discrete time bound + +label "trying" =((p1>0) & (p1<8)) | ((p2>0) & (p2<8)) | ((p3>0) & (p3<8)) | ((p4>0) & (p4<8)); // philosopher in its trying region +label "entered" =((p1>7) & (p1<13)) | ((p2>7) & (p2<13)) | ((p3>7) & (p3<13)) | ((p4>7) & (p4<13)); // philosopher in its critical section // lockout free "trying" => P>=1 [ true U "entered" ] + // bounded until: minimum probability (from a state where a process is in its trying region) that some process enters its critical section within k steps -const int L; Pmin=? [ true U<=L "entered" {"trying"}{min} ] + // expected time: maximum expected time (from a state where a process is in its trying region) that some process enters its critical section Rmax=? [ F "entered" {"trying"}{max} ]