From cd74c9a5e8c6dbaa205a0345ad0b16ccc579ba45 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 10 Dec 2008 12:32:02 +0000 Subject: [PATCH] Fix(es) for previous commit. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@890 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/csma/.csmaN_K.nm.pp | 4 ++-- prism-examples/csma/auto | 18 +++++++++--------- prism-examples/csma/csma.pctl | 2 +- prism-examples/csma/csma2_2.nm | 4 ++-- prism-examples/csma/csma2_4.nm | 4 ++-- prism-examples/csma/csma2_6.nm | 4 ++-- prism-examples/csma/csma3_2.nm | 4 ++-- prism-examples/csma/csma3_4.nm | 4 ++-- prism-examples/csma/csma3_6.nm | 4 ++-- 9 files changed, 24 insertions(+), 24 deletions(-) diff --git a/prism-examples/csma/.csmaN_K.nm.pp b/prism-examples/csma/.csmaN_K.nm.pp index 3d37a73e..678031d6 100644 --- a/prism-examples/csma/.csmaN_K.nm.pp +++ b/prism-examples/csma/.csmaN_K.nm.pp @@ -133,6 +133,6 @@ label "all_delivered" = #& i=1:N#s#i#=4#end#; label "one_delivered" = #| i=1:N#s#i#=4#end#; label "collision_max_backoff" = #| i=1:N#(cd#i#=K & s#i#=1 & b=2)#end#; formula min_backoff_after_success = min(#, i=1:N#s#i#=4?cd#i#:K+1#end#); -formula min_collisions = min(cd1,cd2,cd3,cd4); -formula max_collisions = max(cd1,cd2,cd3,cd4); +formula min_collisions = min(#, i=1:N#cd#i##end#); +formula max_collisions = max(#, i=1:N#cd#i##end#); diff --git a/prism-examples/csma/auto b/prism-examples/csma/auto index d2717178..119969ac 100755 --- a/prism-examples/csma/auto +++ b/prism-examples/csma/auto @@ -1,12 +1,12 @@ #!/bin/csh -prism csma2_2.nm csma.pctl -s -prism csma2_4.nm csma.pctl -s -prism csma2_6.nm csma.pctl -s -prism csma3_2.nm csma.pctl -s -prism csma3_4.nm csma.pctl -s -prism csma3_6.nm csma.pctl -s -prism csma4_2.nm csma.pctl -s -#prism csma4_4.nm csma.pctl -s -#prism csma4_6.nm csma.pctl -s +prism csma2_2.nm csma.pctl -const k=1 -s +prism csma2_4.nm csma.pctl -const k=1 -s +prism csma2_6.nm csma.pctl -const k=1 -s +prism csma3_2.nm csma.pctl -const k=1 -s +prism csma3_4.nm csma.pctl -const k=1 -s +prism csma3_6.nm csma.pctl -const k=1 -s +prism csma4_2.nm csma.pctl -const k=1 -s +#prism csma4_4.nm csma.pctl -const k=1 -s +#prism csma4_6.nm csma.pctl -const k=1 -s diff --git a/prism-examples/csma/csma.pctl b/prism-examples/csma/csma.pctl index bc4e6906..0f861493 100644 --- a/prism-examples/csma/csma.pctl +++ b/prism-examples/csma/csma.pctl @@ -8,7 +8,7 @@ R{"time"}max=?[ F "all_delivered" ] Rmin=?[ F "one_delivered" ] Rmax=?[ F "one_delivered" ] -// message of any station eventually delivered before k backoffs +// message of some station eventually delivered before k backoffs Pmin=?[ F min_backoff_after_success<=k ] Pmax=?[ F min_backoff_after_success<=k ] diff --git a/prism-examples/csma/csma2_2.nm b/prism-examples/csma/csma2_2.nm index 09a0a9a7..affff106 100644 --- a/prism-examples/csma/csma2_2.nm +++ b/prism-examples/csma/csma2_2.nm @@ -123,6 +123,6 @@ label "all_delivered" = s1=4&s2=4; label "one_delivered" = s1=4|s2=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2); formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1); -formula min_collisions = min(cd1,cd2,cd3,cd4); -formula max_collisions = max(cd1,cd2,cd3,cd4); +formula min_collisions = min(cd1,cd2); +formula max_collisions = max(cd1,cd2); diff --git a/prism-examples/csma/csma2_4.nm b/prism-examples/csma/csma2_4.nm index 30d5ee7a..0f880613 100644 --- a/prism-examples/csma/csma2_4.nm +++ b/prism-examples/csma/csma2_4.nm @@ -125,6 +125,6 @@ label "all_delivered" = s1=4&s2=4; label "one_delivered" = s1=4|s2=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2); formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1); -formula min_collisions = min(cd1,cd2,cd3,cd4); -formula max_collisions = max(cd1,cd2,cd3,cd4); +formula min_collisions = min(cd1,cd2); +formula max_collisions = max(cd1,cd2); diff --git a/prism-examples/csma/csma2_6.nm b/prism-examples/csma/csma2_6.nm index 10a51d81..a40dcc37 100644 --- a/prism-examples/csma/csma2_6.nm +++ b/prism-examples/csma/csma2_6.nm @@ -127,6 +127,6 @@ label "all_delivered" = s1=4&s2=4; label "one_delivered" = s1=4|s2=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2); formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1); -formula min_collisions = min(cd1,cd2,cd3,cd4); -formula max_collisions = max(cd1,cd2,cd3,cd4); +formula min_collisions = min(cd1,cd2); +formula max_collisions = max(cd1,cd2); diff --git a/prism-examples/csma/csma3_2.nm b/prism-examples/csma/csma3_2.nm index 9bd6cde5..32c00740 100644 --- a/prism-examples/csma/csma3_2.nm +++ b/prism-examples/csma/csma3_2.nm @@ -128,6 +128,6 @@ label "all_delivered" = s1=4&s2=4&s3=4; label "one_delivered" = s1=4|s2=4|s3=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2); formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1); -formula min_collisions = min(cd1,cd2,cd3,cd4); -formula max_collisions = max(cd1,cd2,cd3,cd4); +formula min_collisions = min(cd1,cd2,cd3); +formula max_collisions = max(cd1,cd2,cd3); diff --git a/prism-examples/csma/csma3_4.nm b/prism-examples/csma/csma3_4.nm index 8387752a..62b76ac9 100644 --- a/prism-examples/csma/csma3_4.nm +++ b/prism-examples/csma/csma3_4.nm @@ -130,6 +130,6 @@ label "all_delivered" = s1=4&s2=4&s3=4; label "one_delivered" = s1=4|s2=4|s3=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2); formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1); -formula min_collisions = min(cd1,cd2,cd3,cd4); -formula max_collisions = max(cd1,cd2,cd3,cd4); +formula min_collisions = min(cd1,cd2,cd3); +formula max_collisions = max(cd1,cd2,cd3); diff --git a/prism-examples/csma/csma3_6.nm b/prism-examples/csma/csma3_6.nm index 73d93172..5ce0a071 100644 --- a/prism-examples/csma/csma3_6.nm +++ b/prism-examples/csma/csma3_6.nm @@ -132,6 +132,6 @@ label "all_delivered" = s1=4&s2=4&s3=4; label "one_delivered" = s1=4|s2=4|s3=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2); formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1); -formula min_collisions = min(cd1,cd2,cd3,cd4); -formula max_collisions = max(cd1,cd2,cd3,cd4); +formula min_collisions = min(cd1,cd2,cd3); +formula max_collisions = max(cd1,cd2,cd3);