From be73f6d7b98b3c33ed4f17df68142f1d0858a94e Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 1 Nov 2007 14:33:43 +0000 Subject: [PATCH] Added pp files to Beauquier. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@501 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../self-stabilisation/beauquier/.autopp | 7 +++ .../beauquier/.beauquierN.nm.pp | 35 +++++++++++++ .../beauquier/beauquier11.nm | 50 +++++++++---------- .../beauquier/beauquier3.nm | 30 +++++------ .../beauquier/beauquier5.nm | 38 +++++++------- .../beauquier/beauquier7.nm | 42 ++++++++-------- .../beauquier/beauquier9.nm | 46 ++++++++--------- 7 files changed, 145 insertions(+), 103 deletions(-) create mode 100755 prism-examples/self-stabilisation/beauquier/.autopp create mode 100644 prism-examples/self-stabilisation/beauquier/.beauquierN.nm.pp diff --git a/prism-examples/self-stabilisation/beauquier/.autopp b/prism-examples/self-stabilisation/beauquier/.autopp new file mode 100755 index 00000000..430fd250 --- /dev/null +++ b/prism-examples/self-stabilisation/beauquier/.autopp @@ -0,0 +1,7 @@ +#!/bin/csh + +foreach N ( 3 5 7 9 11 ) + echo "Generating for N=$N" + prismpp .beauquierN.nm.pp $N >! beauquier$N.nm + unix2dos beauquier$N.nm +end diff --git a/prism-examples/self-stabilisation/beauquier/.beauquierN.nm.pp b/prism-examples/self-stabilisation/beauquier/.beauquierN.nm.pp new file mode 100644 index 00000000..5cb01d63 --- /dev/null +++ b/prism-examples/self-stabilisation/beauquier/.beauquierN.nm.pp @@ -0,0 +1,35 @@ +#const N# +// self stabilisation algorithm Beauquier, Gradinariu and Johnen +// gxn/dxp 18/07/02 + +mdp + +// module of process 1 +module process1 + + d1 : bool; // probabilistic variable + p1 : bool; // deterministic variable + + [] d1=d#N# & p1=p#N# -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1); + [] d1=d#N# & !p1=p#N# -> (d1'=!d1); + +endmodule + +// add further processes through renaming +#for i=2:N# +module process#i# = process1 [ p1=p#i#, p#N#=p#i-1#, d1=d#i#, d#N#=d#i-1# ] endmodule +#end# + +// cost - 1 in each state (expected steps) +rewards "steps" + true : 1; +endrewards + +// initial states - any state with more than 1 token, that is all states +init + true +endinit + +// formula, for use in properties: number of tokens +formula num_tokens = #+ i=1:N#(p#i#=p#func(mod, i, N)+1#?1:0)#end#; + diff --git a/prism-examples/self-stabilisation/beauquier/beauquier11.nm b/prism-examples/self-stabilisation/beauquier/beauquier11.nm index 677549d6..f692f705 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier11.nm +++ b/prism-examples/self-stabilisation/beauquier/beauquier11.nm @@ -1,8 +1,7 @@ // self stabilisation algorithm Beauquier, Gradinariu and Johnen // gxn/dxp 18/07/02 -// model is an mdp -nondeterministic +mdp // module of process 1 module process1 @@ -10,32 +9,33 @@ module process1 d1 : bool; // probabilistic variable p1 : bool; // deterministic variable - [] (d1=d11) & (p1=p11) -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1); - [] (d1=d11) & !(p1=p11) -> (d1'=!d1); + [] d1=d11 & p1=p11 -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1); + [] d1=d11 & !p1=p11 -> (d1'=!d1); endmodule // add further processes through renaming -module process2 =process1[p1=p2 ,p11=p1, d1=d2 ,d11=d1] endmodule -module process3 =process1[p1=p3 ,p11=p2, d1=d3 ,d11=d2] endmodule -module process4 =process1[p1=p4 ,p11=p3, d1=d4 ,d11=d3] endmodule -module process5 =process1[p1=p5 ,p11=p4, d1=d5 ,d11=d4] endmodule -module process6 =process1[p1=p6 ,p11=p5, d1=d6 ,d11=d5] endmodule -module process7 =process1[p1=p7 ,p11=p6, d1=d7 ,d11=d6] endmodule -module process8 =process1[p1=p8 ,p11=p7, d1=d8 ,d11=d7] endmodule -module process9 =process1[p1=p9 ,p11=p8, d1=d9 ,d11=d8] endmodule -module process10=process1[p1=p10,p11=p9, d1=d10,d11=d9] endmodule -module process11=process1[p1=p11,p11=p10,d1=d11,d11=d10] endmodule +module process2 = process1 [ p1=p2, p11=p1, d1=d2, d11=d1 ] endmodule +module process3 = process1 [ p1=p3, p11=p2, d1=d3, d11=d2 ] endmodule +module process4 = process1 [ p1=p4, p11=p3, d1=d4, d11=d3 ] endmodule +module process5 = process1 [ p1=p5, p11=p4, d1=d5, d11=d4 ] endmodule +module process6 = process1 [ p1=p6, p11=p5, d1=d6, d11=d5 ] endmodule +module process7 = process1 [ p1=p7, p11=p6, d1=d7, d11=d6 ] endmodule +module process8 = process1 [ p1=p8, p11=p7, d1=d8, d11=d7 ] endmodule +module process9 = process1 [ p1=p9, p11=p8, d1=d9, d11=d8 ] endmodule +module process10 = process1 [ p1=p10, p11=p9, d1=d10, d11=d9 ] endmodule +module process11 = process1 [ p1=p11, p11=p10, d1=d11, d11=d10 ] endmodule + +// cost - 1 in each state (expected steps) +rewards "steps" + true : 1; +endrewards -// cost - 1 in each state (expected steps) -rewards - true : 1; -endrewards - // initial states - any state with more than 1 token, that is all states -init - true -endinit - -// formula, for use in properties: number of tokens -formula num_tokens = (p11=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0); +init + true +endinit + +// formula, for use in properties: number of tokens +formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p10?1:0)+(p10=p11?1:0)+(p11=p1?1:0); + diff --git a/prism-examples/self-stabilisation/beauquier/beauquier3.nm b/prism-examples/self-stabilisation/beauquier/beauquier3.nm index afc6c3f8..6bb8ce61 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier3.nm +++ b/prism-examples/self-stabilisation/beauquier/beauquier3.nm @@ -1,8 +1,7 @@ // self stabilisation algorithm Beauquier, Gradinariu and Johnen // gxn/dxp 18/07/02 -// model is an mdp -nondeterministic +mdp // module of process 1 module process1 @@ -16,18 +15,19 @@ module process1 endmodule // add further processes through renaming -module process2 =process1[p1=p2 ,p3=p1, d1=d2 ,d3=d1] endmodule -module process3 =process1[p1=p3 ,p3=p2, d1=d3 ,d3=d2] endmodule +module process2 = process1 [ p1=p2, p3=p1, d1=d2, d3=d1 ] endmodule +module process3 = process1 [ p1=p3, p3=p2, d1=d3, d3=d2 ] endmodule + +// cost - 1 in each state (expected steps) +rewards "steps" + true : 1; +endrewards -// cost - 1 in each state (expected steps) -rewards - true : 1; -endrewards - // initial states - any state with more than 1 token, that is all states -init - true -endinit - -// formula for use in properties: number of tokens -formula num_tokens = (p3=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0); +init + true +endinit + +// formula, for use in properties: number of tokens +formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p1?1:0); + diff --git a/prism-examples/self-stabilisation/beauquier/beauquier5.nm b/prism-examples/self-stabilisation/beauquier/beauquier5.nm index 5f74632d..46d21849 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier5.nm +++ b/prism-examples/self-stabilisation/beauquier/beauquier5.nm @@ -1,8 +1,7 @@ // self stabilisation algorithm Beauquier, Gradinariu and Johnen // gxn/dxp 18/07/02 -// model is an mdp -nondeterministic +mdp // module of process 1 module process1 @@ -10,26 +9,27 @@ module process1 d1 : bool; // probabilistic variable p1 : bool; // deterministic variable - [] (d1=d5) & (p1=p5) -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1); - [] (d1=d5) & !(p1=p5) -> (d1'=!d1); + [] d1=d5 & p1=p5 -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1); + [] d1=d5 & !p1=p5 -> (d1'=!d1); endmodule // add further processes through renaming -module process2 =process1[p1=p2 ,p5=p1, d1=d2 ,d5=d1] endmodule -module process3 =process1[p1=p3 ,p5=p2, d1=d3 ,d5=d2] endmodule -module process4 =process1[p1=p4 ,p5=p3, d1=d4 ,d5=d3] endmodule -module process5 =process1[p1=p5 ,p5=p4, d1=d5 ,d5=d4] endmodule +module process2 = process1 [ p1=p2, p5=p1, d1=d2, d5=d1 ] endmodule +module process3 = process1 [ p1=p3, p5=p2, d1=d3, d5=d2 ] endmodule +module process4 = process1 [ p1=p4, p5=p3, d1=d4, d5=d3 ] endmodule +module process5 = process1 [ p1=p5, p5=p4, d1=d5, d5=d4 ] endmodule + +// cost - 1 in each state (expected steps) +rewards "steps" + true : 1; +endrewards -// cost - 1 in each state (expected steps) -rewards - true : 1; -endrewards - // initial states - any state with more than 1 token, that is all states -init - true -endinit - -// formula, for use in properties: number of tokens -formula num_tokens = (p5=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0); +init + true +endinit + +// formula, for use in properties: number of tokens +formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p1?1:0); + diff --git a/prism-examples/self-stabilisation/beauquier/beauquier7.nm b/prism-examples/self-stabilisation/beauquier/beauquier7.nm index 16b11020..dfc7903c 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier7.nm +++ b/prism-examples/self-stabilisation/beauquier/beauquier7.nm @@ -1,8 +1,7 @@ // self stabilisation algorithm Beauquier, Gradinariu and Johnen // gxn/dxp 18/07/02 -// model is an mdp -nondeterministic +mdp // module of process 1 module process1 @@ -10,28 +9,29 @@ module process1 d1 : bool; // probabilistic variable p1 : bool; // deterministic variable - [] (d1=d7) & (p1=p7) -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1); - [] (d1=d7) & !(p1=p7) -> (d1'=!d1); + [] d1=d7 & p1=p7 -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1); + [] d1=d7 & !p1=p7 -> (d1'=!d1); endmodule // add further processes through renaming -module process2 =process1[p1=p2 ,p7=p1, d1=d2 ,d7=d1] endmodule -module process3 =process1[p1=p3 ,p7=p2, d1=d3 ,d7=d2] endmodule -module process4 =process1[p1=p4 ,p7=p3, d1=d4 ,d7=d3] endmodule -module process5 =process1[p1=p5 ,p7=p4, d1=d5 ,d7=d4] endmodule -module process6 =process1[p1=p6 ,p7=p5, d1=d6 ,d7=d5] endmodule -module process7 =process1[p1=p7 ,p7=p6, d1=d7 ,d7=d6] endmodule +module process2 = process1 [ p1=p2, p7=p1, d1=d2, d7=d1 ] endmodule +module process3 = process1 [ p1=p3, p7=p2, d1=d3, d7=d2 ] endmodule +module process4 = process1 [ p1=p4, p7=p3, d1=d4, d7=d3 ] endmodule +module process5 = process1 [ p1=p5, p7=p4, d1=d5, d7=d4 ] endmodule +module process6 = process1 [ p1=p6, p7=p5, d1=d6, d7=d5 ] endmodule +module process7 = process1 [ p1=p7, p7=p6, d1=d7, d7=d6 ] endmodule + +// cost - 1 in each state (expected steps) +rewards "steps" + true : 1; +endrewards -// cost - 1 in each state (expected steps) -rewards - true : 1; -endrewards - // initial states - any state with more than 1 token, that is all states -init - true -endinit - -// formula, for use in properties: number of tokens -formula num_tokens = (p7=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0); +init + true +endinit + +// formula, for use in properties: number of tokens +formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p1?1:0); + diff --git a/prism-examples/self-stabilisation/beauquier/beauquier9.nm b/prism-examples/self-stabilisation/beauquier/beauquier9.nm index d7fc4df0..bcba98a3 100644 --- a/prism-examples/self-stabilisation/beauquier/beauquier9.nm +++ b/prism-examples/self-stabilisation/beauquier/beauquier9.nm @@ -1,8 +1,7 @@ // self stabilisation algorithm Beauquier, Gradinariu and Johnen // gxn/dxp 18/07/02 -// model is an mdp -nondeterministic +mdp // module of process 1 module process1 @@ -10,30 +9,31 @@ module process1 d1 : bool; // probabilistic variable p1 : bool; // deterministic variable - [] (d1=d9) & (p1=p9) -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1); - [] (d1=d9) & !(p1=p9) -> (d1'=!d1); + [] d1=d9 & p1=p9 -> 0.5 : (d1'=!d1) & (p1'=p1) + 0.5 : (d1'=!d1) & (p1'=!p1); + [] d1=d9 & !p1=p9 -> (d1'=!d1); endmodule // add further processes through renaming -module process2 =process1[p1=p2 ,p9=p1, d1=d2 ,d9=d1] endmodule -module process3 =process1[p1=p3 ,p9=p2, d1=d3 ,d9=d2] endmodule -module process4 =process1[p1=p4 ,p9=p3, d1=d4 ,d9=d3] endmodule -module process5 =process1[p1=p5 ,p9=p4, d1=d5 ,d9=d4] endmodule -module process6 =process1[p1=p6 ,p9=p5, d1=d6 ,d9=d5] endmodule -module process7 =process1[p1=p7 ,p9=p6, d1=d7 ,d9=d6] endmodule -module process8 =process1[p1=p8 ,p9=p7, d1=d8 ,d9=d7] endmodule -module process9 =process1[p1=p9 ,p9=p8, d1=d9 ,d9=d8] endmodule +module process2 = process1 [ p1=p2, p9=p1, d1=d2, d9=d1 ] endmodule +module process3 = process1 [ p1=p3, p9=p2, d1=d3, d9=d2 ] endmodule +module process4 = process1 [ p1=p4, p9=p3, d1=d4, d9=d3 ] endmodule +module process5 = process1 [ p1=p5, p9=p4, d1=d5, d9=d4 ] endmodule +module process6 = process1 [ p1=p6, p9=p5, d1=d6, d9=d5 ] endmodule +module process7 = process1 [ p1=p7, p9=p6, d1=d7, d9=d6 ] endmodule +module process8 = process1 [ p1=p8, p9=p7, d1=d8, d9=d7 ] endmodule +module process9 = process1 [ p1=p9, p9=p8, d1=d9, d9=d8 ] endmodule + +// cost - 1 in each state (expected steps) +rewards "steps" + true : 1; +endrewards -// cost - 1 in each state (expected steps) -rewards - true : 1; -endrewards - // initial states - any state with more than 1 token, that is all states -init - true -endinit - -// formula, for use in properties: number of tokens -formula num_tokens = (p9=p1?1:0)+(p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0); +init + true +endinit + +// formula, for use in properties: number of tokens +formula num_tokens = (p1=p2?1:0)+(p2=p3?1:0)+(p3=p4?1:0)+(p4=p5?1:0)+(p5=p6?1:0)+(p6=p7?1:0)+(p7=p8?1:0)+(p8=p9?1:0)+(p9=p1?1:0); +