From 6d2fb7496912071dfbad13b1c83f99ec1c4599e1 Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Tue, 30 Oct 2007 10:35:24 +0000 Subject: [PATCH] updated herman (rewards) git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@491 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../self-stabilisation/herman/.hermanN.pm.pp | 6 ++--- prism-examples/self-stabilisation/herman/auto | 9 ++++---- .../self-stabilisation/herman/herman.pctl | 23 ++++++++++--------- .../self-stabilisation/herman/herman11.pm | 6 ++--- .../self-stabilisation/herman/herman13.pm | 6 ++--- .../self-stabilisation/herman/herman15.pm | 6 ++--- .../self-stabilisation/herman/herman17.pm | 6 ++--- .../self-stabilisation/herman/herman19.pm | 6 ++--- .../self-stabilisation/herman/herman21.pm | 6 ++--- .../self-stabilisation/herman/herman3.pm | 6 ++--- .../self-stabilisation/herman/herman5.pm | 6 ++--- .../self-stabilisation/herman/herman7.pm | 6 ++--- .../self-stabilisation/herman/herman9.pm | 17 ++++++++++---- 13 files changed, 60 insertions(+), 49 deletions(-) diff --git a/prism-examples/self-stabilisation/herman/.hermanN.pm.pp b/prism-examples/self-stabilisation/herman/.hermanN.pm.pp index 80157436..aa62c7c7 100644 --- a/prism-examples/self-stabilisation/herman/.hermanN.pm.pp +++ b/prism-examples/self-stabilisation/herman/.hermanN.pm.pp @@ -23,13 +23,13 @@ module process#i# = process1 [ x1=x#i#, x#N#=x#i-1# ] endmodule // cost - 1 in each state (expected number of steps) rewards "steps" - true : 1; - endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) -init true endinit +init + true +endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) diff --git a/prism-examples/self-stabilisation/herman/auto b/prism-examples/self-stabilisation/herman/auto index 33e96302..42a538de 100755 --- a/prism-examples/self-stabilisation/herman/auto +++ b/prism-examples/self-stabilisation/herman/auto @@ -1,6 +1,7 @@ #!/bin/csh -prism herman7.pm herman.pctl -prop 1 -const k=0 -prism herman7.pm herman.pctl -prop 2 -const k=0 -prism herman7.pm herman.pctl -prop 3 -const k=1:2:7 -prism herman7.pm herman.pctl -prop 4 -const k=1:2:7 +prism herman7.pm herman.pctl -prop 1 -const k=0,K=0 +prism herman7.pm herman.pctl -prop 2 -const k=0,K=0 +prism herman7.pm herman.pctl -prop 3 -const k=1:2:7,K=0 +prism herman7.pm herman.pctl -prop 4 -const k=1:2:7,K=0 +prism herman7.pm herman.pctl -prop 5 -const k=0,K=1:1:100 diff --git a/prism-examples/self-stabilisation/herman/herman.pctl b/prism-examples/self-stabilisation/herman/herman.pctl index e4321b61..3261167a 100644 --- a/prism-examples/self-stabilisation/herman/herman.pctl +++ b/prism-examples/self-stabilisation/herman/herman.pctl @@ -1,19 +1,20 @@ -const int k; +const int k; // number of tokens +const int K; // number of steps -// States with k tokens -label "k_tokens" = num_tokens=k; +// labels +label "k_tokens" = num_tokens=k; // configurations with k tokens +label "stable" = num_tokens=1; // stable configurations (1 token) -// Stable states - where only one process has a token -label "stable" = num_tokens=1; - -// A stable state is reached with probability 1 +// From any configuration, a stable configuration is reached with probability 1 "init" => P>=1 [ F "stable" ] -// Maximum expected time to reach a stable state (for all configurations) +// Maximum expected time to reach a stable configuration (for all configurations) R=? [ F "stable" {"init"}{max} ] -// Maximum expected time to reach a stable state (for all k-token configurations) +// Maximum/minimum expected time to reach a stable configuration (for all k-token configurations) R=? [ F "stable" {"k_tokens"}{max} ] - -// Minimum expected time to reach a stable state (for all k-token configurations) R=? [ F "stable" {"k_tokens"}{min} ] + +// Minimum probability reached a stable configuration within K steps (for all configurations) +P=? [ F<=K "stable" {"init"}{min} ] + diff --git a/prism-examples/self-stabilisation/herman/herman11.pm b/prism-examples/self-stabilisation/herman/herman11.pm index 0b65b382..f133a8da 100644 --- a/prism-examples/self-stabilisation/herman/herman11.pm +++ b/prism-examples/self-stabilisation/herman/herman11.pm @@ -29,13 +29,13 @@ module process11 = process1 [ x1=x11, x11=x10 ] endmodule // cost - 1 in each state (expected number of steps) rewards "steps" - true : 1; - endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) -init true endinit +init + true +endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) diff --git a/prism-examples/self-stabilisation/herman/herman13.pm b/prism-examples/self-stabilisation/herman/herman13.pm index badc6142..e945cc9e 100644 --- a/prism-examples/self-stabilisation/herman/herman13.pm +++ b/prism-examples/self-stabilisation/herman/herman13.pm @@ -31,13 +31,13 @@ module process13 = process1 [ x1=x13, x13=x12 ] endmodule // cost - 1 in each state (expected number of steps) rewards "steps" - true : 1; - endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) -init true endinit +init + true +endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) diff --git a/prism-examples/self-stabilisation/herman/herman15.pm b/prism-examples/self-stabilisation/herman/herman15.pm index 921aca1b..c75e6d83 100644 --- a/prism-examples/self-stabilisation/herman/herman15.pm +++ b/prism-examples/self-stabilisation/herman/herman15.pm @@ -33,13 +33,13 @@ module process15 = process1 [ x1=x15, x15=x14 ] endmodule // cost - 1 in each state (expected number of steps) rewards "steps" - true : 1; - endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) -init true endinit +init + true +endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) diff --git a/prism-examples/self-stabilisation/herman/herman17.pm b/prism-examples/self-stabilisation/herman/herman17.pm index 6bbdd937..0412a460 100644 --- a/prism-examples/self-stabilisation/herman/herman17.pm +++ b/prism-examples/self-stabilisation/herman/herman17.pm @@ -35,13 +35,13 @@ module process17 = process1 [ x1=x17, x17=x16 ] endmodule // cost - 1 in each state (expected number of steps) rewards "steps" - true : 1; - endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) -init true endinit +init + true +endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) diff --git a/prism-examples/self-stabilisation/herman/herman19.pm b/prism-examples/self-stabilisation/herman/herman19.pm index 8a0dcf6c..4c9c2931 100644 --- a/prism-examples/self-stabilisation/herman/herman19.pm +++ b/prism-examples/self-stabilisation/herman/herman19.pm @@ -37,13 +37,13 @@ module process19 = process1 [ x1=x19, x19=x18 ] endmodule // cost - 1 in each state (expected number of steps) rewards "steps" - true : 1; - endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) -init true endinit +init + true +endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) diff --git a/prism-examples/self-stabilisation/herman/herman21.pm b/prism-examples/self-stabilisation/herman/herman21.pm index 81ace61a..5887db71 100644 --- a/prism-examples/self-stabilisation/herman/herman21.pm +++ b/prism-examples/self-stabilisation/herman/herman21.pm @@ -39,13 +39,13 @@ module process21 = process1 [ x1=x21, x21=x20 ] endmodule // cost - 1 in each state (expected number of steps) rewards "steps" - true : 1; - endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) -init true endinit +init + true +endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) diff --git a/prism-examples/self-stabilisation/herman/herman3.pm b/prism-examples/self-stabilisation/herman/herman3.pm index 9684125d..6a4a06e0 100644 --- a/prism-examples/self-stabilisation/herman/herman3.pm +++ b/prism-examples/self-stabilisation/herman/herman3.pm @@ -21,13 +21,13 @@ module process3 = process1 [ x1=x3, x3=x2 ] endmodule // cost - 1 in each state (expected number of steps) rewards "steps" - true : 1; - endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) -init true endinit +init + true +endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) diff --git a/prism-examples/self-stabilisation/herman/herman5.pm b/prism-examples/self-stabilisation/herman/herman5.pm index 114fc367..e028d98c 100644 --- a/prism-examples/self-stabilisation/herman/herman5.pm +++ b/prism-examples/self-stabilisation/herman/herman5.pm @@ -23,13 +23,13 @@ module process5 = process1 [ x1=x5, x5=x4 ] endmodule // cost - 1 in each state (expected number of steps) rewards "steps" - true : 1; - endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) -init true endinit +init + true +endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) diff --git a/prism-examples/self-stabilisation/herman/herman7.pm b/prism-examples/self-stabilisation/herman/herman7.pm index a18f39ca..1c280e15 100644 --- a/prism-examples/self-stabilisation/herman/herman7.pm +++ b/prism-examples/self-stabilisation/herman/herman7.pm @@ -25,13 +25,13 @@ module process7 = process1 [ x1=x7, x7=x6 ] endmodule // cost - 1 in each state (expected number of steps) rewards "steps" - true : 1; - endrewards // set of initial states: all (i.e. any possible initial configuration of tokens) -init true endinit +init + true +endinit // formula, for use in properties: number of tokens // (i.e. number of processes that have the same value as the process to their left) diff --git a/prism-examples/self-stabilisation/herman/herman9.pm b/prism-examples/self-stabilisation/herman/herman9.pm index 9c36a642..5f207a78 100644 --- a/prism-examples/self-stabilisation/herman/herman9.pm +++ b/prism-examples/self-stabilisation/herman/herman9.pm @@ -27,14 +27,23 @@ module process9 = process1[x1=x9, x9=x8 ] endmodule // cost - 1 in each state (expected steps) rewards - true : 1; - endrewards // any initial state (consider any possible initial configuration of tokens) init - true - endinit +// cost - 1 in each state (expected number of steps) +rewards + true : 1; +endrewards + +// set of initial states: all (i.e. any possible initial configuration of tokens) +init + true +endinit + +// formula for use in properties: number of tokens +// (i.e. number of processes whose variable has the same value as that of the process to their left) +formula num_tokens = (x1=x2?1:0)+(x2=x3?1:0)+(x3=x4?1:0)+(x4=x5?1:0)+(x5=x6?1:0)+(x6=x7?1:0)+(x7=x8?1:0)+(x8=x9?1:0)+(x9=x1?1:0);