diff --git a/prism-examples/dice/dice.pctl b/prism-examples/dice/dice.pctl index 05df91a1..ed5d699e 100644 --- a/prism-examples/dice/dice.pctl +++ b/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 ] diff --git a/prism-examples/dining_crypt/correctness.pctl b/prism-examples/dining_crypt/correctness.pctl index d6667b87..dc9e79b5 100644 --- a/prism-examples/dining_crypt/correctness.pctl +++ b/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) ]) diff --git a/prism-examples/firewire/abst/liveness.pctl b/prism-examples/firewire/abst/liveness.pctl index 8c832230..312c837f 100644 --- a/prism-examples/firewire/abst/liveness.pctl +++ b/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) ] diff --git a/prism-examples/firewire/impl/liveness.pctl b/prism-examples/firewire/impl/liveness.pctl index a901c83f..6b271db9 100644 --- a/prism-examples/firewire/impl/liveness.pctl +++ b/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)) ] diff --git a/prism-examples/mutual/mutual.pctl b/prism-examples/mutual/mutual.pctl index 5baa9265..fcd9964d 100644 --- a/prism-examples/mutual/mutual.pctl +++ b/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 ]) diff --git a/prism-examples/phil/nofair/phil.pctl b/prism-examples/phil/nofair/phil.pctl index 0ad052c0..f480fb0d 100644 --- a/prism-examples/phil/nofair/phil.pctl +++ b/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} ] diff --git a/prism-examples/phil/original/phil.pctl b/prism-examples/phil/original/phil.pctl index f1370a9c..2943dffc 100644 --- a/prism-examples/phil/original/phil.pctl +++ b/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" ]) diff --git a/prism-examples/phil_lss/phil_lss3.pctl b/prism-examples/phil_lss/phil_lss3.pctl index 4230929b..e88ad573 100644 --- a/prism-examples/phil_lss/phil_lss3.pctl +++ b/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} ] diff --git a/prism-examples/phil_lss/phil_lss4.pctl b/prism-examples/phil_lss/phil_lss4.pctl index a87e7d9a..09f8f6db 100644 --- a/prism-examples/phil_lss/phil_lss4.pctl +++ b/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} ] diff --git a/prism-examples/rabin/rabin.pctl b/prism-examples/rabin/rabin.pctl index 3db25f61..f275cc71 100644 --- a/prism-examples/rabin/rabin.pctl +++ b/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 diff --git a/prism-examples/self-stabilisation/beauquier/beauquier.pctl b/prism-examples/self-stabilisation/beauquier/beauquier.pctl index 69c0b591..82f6df27 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier.pctl +++ b/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} ] diff --git a/prism-examples/self-stabilisation/herman/herman.pctl b/prism-examples/self-stabilisation/herman/herman.pctl index a9501003..0873eee8 100644 --- a/prism-examples/self-stabilisation/herman/herman.pctl +++ b/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} ] diff --git a/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl b/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl index f88a5731..69358e02 100644 --- a/prism-examples/self-stabilisation/israeli-jalfon/ij.pctl +++ b/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} ]