Example fixes re new semantics (result reported for initial state by default) - need more filters.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3036 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism-examples/dice/dice.pctl

@@ -1,13 +1,13 @@
-const int x;
-
-// Is probability of throwing x > 0.1?
-"init" => P>0.1 [ true U s=7 & d=x ]
-
-// Probability of throwing 6?
-P=? [ true U s=7 & d=6 ]
-
-// Probability of throwing x?
-P=? [ true U s=7 & d=x ]
-
-// Expected number of coin flips to complete?
-R=? [ F s=7 ]
+const int x;
+
+// Is probability of throwing x > 0.1?
+P>0.1 [ true U s=7 & d=x ]
+
+// Probability of throwing 6?
+P=? [ true U s=7 & d=6 ]
+
+// Probability of throwing x?
+P=? [ true U s=7 & d=x ]
+
+// Expected number of coin flips to complete?
+R=? [ F s=7 ]

prism-examples/dining_crypt/correctness.pctl

@@ -1,7 +1,7 @@
 // Correctness for the case where the master pays
-// (final parity of number of number of "agrees"s matches that of N)
-(pay=0) => P>=1 [ F "done" & parity=func(mod, N, 2) ]
-
-// Correctness for the case where a cryptographer pays
-// (final parity of number of number of "agrees"s does not match that of N)
-(pay>0) => P>=1 [ F "done" & parity!=func(mod, N, 2) ]
+// (final parity of number of number of "agrees"s matches that of N)
+filter(forall, (pay=0) => P>=1 [ F "done" & parity=func(mod, N, 2) ])
+
+// Correctness for the case where a cryptographer pays
+// (final parity of number of number of "agrees"s does not match that of N)
+filter(forall, (pay>0) => P>=1 [ F "done" & parity!=func(mod, N, 2) ])

prism-examples/firewire/abst/liveness.pctl

@@ -1,2 +1,2 @@
 // liveness property (eventually a process is made the leader)
-"init" => P>=1[ true U (s=9) ]
+P>=1 [ F (s=9) ]

prism-examples/firewire/impl/liveness.pctl

@@ -1,2 +1,2 @@
 // liveness
-"init" => P>=1 [ true U ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)) ]
+P>=1 [ F ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)) ]

prism-examples/mutual/mutual.pctl

@@ -1,18 +1,18 @@
-// Theorem 1 (mutual exclusion)
-
-num_crit <= 1
-
-// Lemma C
-// If the crical section is occupied then eventually it becomes clear
-
-num_crit > 0 => P>=1 [ F num_crit = 0 ]
-
-// Lemma D
-// If a process is between 4 and 13 (in our version) then eventually some process gets to 14
-
-"some_4_13" => P>=1 [ F "some_14" ]
-
-// Theorem 2 (liveness)
-// If process 1 tries then eventually it enters the critical section
-
-p1=1 => P>=1 [ F p1=10 ]
+// Theorem 1 (mutual exclusion)
+
+filter(forall, num_crit <= 1)
+
+// Lemma C
+// If the crical section is occupied then eventually it becomes clear
+
+filter(forall, num_crit > 0 => P>=1 [ F num_crit = 0 ])
+
+// Lemma D
+// If a process is between 4 and 13 (in our version) then eventually some process gets to 14
+
+filter(forall, "some_4_13" => P>=1 [ F "some_14" ])
+
+// Theorem 2 (liveness)
+// If process 1 tries then eventually it enters the critical section
+
+filter(forall, p1=1 => P>=1 [ F p1=10 ])

prism-examples/phil/nofair/phil.pctl

@@ -1,12 +1,17 @@
 const int K;
 
-// Liveness (if a philosopher is hungry then eventually some philosopher eats)
-"hungry" => P>=1 [ F "eat"]
+// Liveness (if a philosopher is hungry then eventually some philosopher eats)
+
+filter(forall, "hungry" => P>=1 [ F "eat"])
+
 
 // Bounded until (minimum probability, from a state where someone
-// is hungry, that a philosopher will eat within K steps)
-Pmin=? [ F<=K "eat" {"hungry"}{min} ]
+// is hungry, that a philosopher will eat within K steps)
+
+Pmin=? [ F<=K "eat" {"hungry"}{min} ]
+
 
 // Expected time (from a state where someone is hungry, the maximum
-// expected number of steps until a philosopher eats)
-R{"num_steps"}max=? [F "eat" {"hungry"}{max} ]
+// expected number of steps until a philosopher eats)
+
+R{"num_steps"}max=? [ F "eat" {"hungry"}{max} ]

prism-examples/phil/original/phil.pctl

@@ -1,3 +1,2 @@
 // Liveness (if a philosopher is hungry then eventually some philosopher eats)
-
-"hungry" => P>=1 [ F "eat"]
+filter(forall, "hungry" => P>=1 [ F "eat" ])

prism-examples/phil_lss/phil_lss3.pctl

@@ -1,13 +1,13 @@
-const int L; // discrete time bound
+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" ]
+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
 
-// 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
-Pmin=? [ true U<=L "entered" {"trying"}{min} ]
+// lockout free
+filter(forall, "trying" =>  P>=1 [ true U "entered" ])
 
-// 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} ]
+// 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
+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} ]

prism-examples/phil_lss/phil_lss4.pctl

@@ -1,13 +1,13 @@
-const int L; // discrete time bound
+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" ]
+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
 
-// 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
-Pmin=? [ true U<=L "entered" {"trying"}{min} ]
+// lockout free
+filter(forall, "trying" =>  P>=1 [ true U "entered" ])
 
-// 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} ]
+// 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
+Pmin=? [ F<=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} ]

prism-examples/rabin/rabin.pctl

@@ -1,8 +1,8 @@
 // Mutual exclusion: at any time t there is at most one process in its critical section phase
-num_procs_in_crit <= 1
+filter(forall, num_procs_in_crit <= 1)
 
 // Liveness: if a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ F "one_critical" ]
+filter(forall, "one_trying" => P>=1 [ F "one_critical" ])
 
 
 // weaker version of k-bounded waiting: minimum probability process enters the criticial section given it draws

prism-examples/self-stabilisation/beauquier/beauquier.pctl

@@ -6,7 +6,7 @@ label "k_tokens" = num_tokens=k; // configurations with k tokens
 label "stable" = num_tokens=1;   // stable configurations (1 token)
 
 // From any configuration, a stable configuration is reached with probability 1
-"init" => P>=1 [ F "stable" ]
+filter(forall, P>=1 [ F "stable" ], "init")
 
 // Maximum expected time to reach a stable configuration (for all configurations)
 Rmax=? [ F "stable" {"init"}{max} ]

prism-examples/self-stabilisation/herman/herman.pctl

@@ -5,7 +5,7 @@ const int K; // number of steps
 label "k_tokens" = num_tokens=k; // configurations with k tokens
 
 // From any configuration, a stable configuration is reached with probability 1
-"init" => P>=1 [ F "stable" ]
+filter(forall, P>=1 [ F "stable" ], "init")
 
 // Maximum expected time to reach a stable configuration (for all configurations)
 R=? [ F "stable" {"init"}{max} ]

prism-examples/self-stabilisation/israeli-jalfon/ij.pctl

@@ -5,7 +5,7 @@ const int K; // number of steps
 label "k_tokens" = num_tokens=k; // configurations with k tokens
 
 // From any configuration, a stable configuration is reached with probability 1
-"init" => P>=1 [ F "stable" ]
+filter(forall, P>=1 [ F "stable" ], "init")
 
 // Maximum expected time to reach a stable configuration (for all configurations)
 Rmax=? [ F "stable" {"init"}{max} ]