From 39d74476259d99aecc8bb374fa867b155bfc815f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 5 Dec 2008 15:09:26 +0000 Subject: [PATCH] CSMA tweaks. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@861 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/csma/.autopp | 2 +- prism-examples/csma/.csmaK.pctl.pp | 8 ++-- .../csma/{.csmaNK.nm.pp => .csmaK_N.nm.pp} | 4 +- prism-examples/csma/csma2.pctl | 16 +++---- prism-examples/csma/csma2_2.nm | 6 +-- prism-examples/csma/csma2_3.nm | 6 +-- prism-examples/csma/csma2_4.nm | 6 +-- prism-examples/csma/csma4.pctl | 32 ++++++------- prism-examples/csma/csma4_2.nm | 10 ++-- prism-examples/csma/csma4_3.nm | 10 ++-- prism-examples/csma/csma4_4.nm | 10 ++-- prism-examples/csma/csma6.pctl | 48 +++++++++---------- prism-examples/csma/csma6_2.nm | 14 +++--- prism-examples/csma/csma6_3.nm | 14 +++--- prism-examples/csma/csma6_4.nm | 14 +++--- 15 files changed, 100 insertions(+), 100 deletions(-) rename prism-examples/csma/{.csmaNK.nm.pp => .csmaK_N.nm.pp} (97%) diff --git a/prism-examples/csma/.autopp b/prism-examples/csma/.autopp index 80214aa4..e21af2c2 100755 --- a/prism-examples/csma/.autopp +++ b/prism-examples/csma/.autopp @@ -5,6 +5,6 @@ foreach K ( 2 4 6 ) prismpp .csmaK.pctl.pp $K >! csma$K.pctl foreach N ( 2 3 4 ) echo " and N=$N" - prismpp .csmaNK.nm.pp $N $K >! csma$K"_"$N.nm + prismpp .csmaK_N.nm.pp $N $K >! csma$K"_"$N.nm end end diff --git a/prism-examples/csma/.csmaK.pctl.pp b/prism-examples/csma/.csmaK.pctl.pp index e0023df4..910ad94e 100644 --- a/prism-examples/csma/.csmaK.pctl.pp +++ b/prism-examples/csma/.csmaK.pctl.pp @@ -10,8 +10,8 @@ Rmax=?[ F "one_delivered" ] // message of any station eventually delivered before i backoffs #for i=1:K# -Pmin=?[true U "succes_with_backoff_under_#i#" ] -Pmax=?[true U "succes_with_backoff_under_#i#" ] +Pmin=?[ F "success_with_backoff_under_#i#" ] +Pmax=?[ F "success_with_backoff_under_#i#" ] #end# // probability all sent successfully before a collision with max backoff @@ -20,8 +20,8 @@ Pmax=?[ !"collision_max_backoff" U "all_delivered" ] // probability a station suffers i collisions #for i=1:K# -Pmin=?[true U "collisions_equal_#i#" ] -Pmax=?[true U "collisions_equal_#i#" ] +Pmin=?[ F "collisions_equal_#i#" ] +Pmax=?[ F "collisions_equal_#i#" ] #end# diff --git a/prism-examples/csma/.csmaNK.nm.pp b/prism-examples/csma/.csmaK_N.nm.pp similarity index 97% rename from prism-examples/csma/.csmaNK.nm.pp rename to prism-examples/csma/.csmaK_N.nm.pp index ed84d747..537cd92b 100644 --- a/prism-examples/csma/.csmaNK.nm.pp +++ b/prism-examples/csma/.csmaK_N.nm.pp @@ -1,7 +1,7 @@ // CSMA/CD protocol - probabilistic version of kronos model (3 stations) // gxn/dxp 04/12/01 -nondeterministic +mdp // note made changes since cannot have strict inequalities // in digital clocks approach and suppose a station only sends one message @@ -132,7 +132,7 @@ 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#; #for i=1:K# -label "succes_with_backoff_under_#i#" = #| j=1:N#(cd#j#<=#i# & s#j#=4)#end#; +label "success_with_backoff_under_#i#" = #| j=1:N#(cd#j#<=#i# & s#j#=4)#end#; #end# #for i=1:K# label "collisions_equal_#i#" = #| j=1:N#(cd#j#=#i#)#end#; diff --git a/prism-examples/csma/csma2.pctl b/prism-examples/csma/csma2.pctl index 0f745903..e11b03a5 100644 --- a/prism-examples/csma/csma2.pctl +++ b/prism-examples/csma/csma2.pctl @@ -8,19 +8,19 @@ Rmin=?[ F "one_delivered" ] Rmax=?[ F "one_delivered" ] // message of any station eventually delivered before i backoffs -Pmin=?[true U "succes_with_backoff_under_1" ] -Pmax=?[true U "succes_with_backoff_under_1" ] -Pmin=?[true U "succes_with_backoff_under_2" ] -Pmax=?[true U "succes_with_backoff_under_2" ] +Pmin=?[ F "success_with_backoff_under_1" ] +Pmax=?[ F "success_with_backoff_under_1" ] +Pmin=?[ F "success_with_backoff_under_2" ] +Pmax=?[ F "success_with_backoff_under_2" ] // probability all sent successfully before a collision with max backoff Pmin=?[ !"collision_max_backoff" U "all_delivered" ] Pmax=?[ !"collision_max_backoff" U "all_delivered" ] // probability a station suffers i collisions -Pmin=?[true U "collisions_equal_1" ] -Pmax=?[true U "collisions_equal_1" ] -Pmin=?[true U "collisions_equal_2" ] -Pmax=?[true U "collisions_equal_2" ] +Pmin=?[ F "collisions_equal_1" ] +Pmax=?[ F "collisions_equal_1" ] +Pmin=?[ F "collisions_equal_2" ] +Pmax=?[ F "collisions_equal_2" ] diff --git a/prism-examples/csma/csma2_2.nm b/prism-examples/csma/csma2_2.nm index 3f310749..277cd58e 100644 --- a/prism-examples/csma/csma2_2.nm +++ b/prism-examples/csma/csma2_2.nm @@ -1,7 +1,7 @@ // CSMA/CD protocol - probabilistic version of kronos model (3 stations) // gxn/dxp 04/12/01 -nondeterministic +mdp // note made changes since cannot have strict inequalities // in digital clocks approach and suppose a station only sends one message @@ -121,8 +121,8 @@ endrewards 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); -label "succes_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4); -label "succes_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4); +label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4); +label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4); label "collisions_equal_1" = (cd1=1)|(cd2=1); label "collisions_equal_2" = (cd1=2)|(cd2=2); diff --git a/prism-examples/csma/csma2_3.nm b/prism-examples/csma/csma2_3.nm index a874f09f..514526d1 100644 --- a/prism-examples/csma/csma2_3.nm +++ b/prism-examples/csma/csma2_3.nm @@ -1,7 +1,7 @@ // CSMA/CD protocol - probabilistic version of kronos model (3 stations) // gxn/dxp 04/12/01 -nondeterministic +mdp // note made changes since cannot have strict inequalities // in digital clocks approach and suppose a station only sends one message @@ -126,8 +126,8 @@ endrewards 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); -label "succes_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4); -label "succes_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4); +label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4); +label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4); label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1); label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2); diff --git a/prism-examples/csma/csma2_4.nm b/prism-examples/csma/csma2_4.nm index 5e41a2d7..2bf27a80 100644 --- a/prism-examples/csma/csma2_4.nm +++ b/prism-examples/csma/csma2_4.nm @@ -1,7 +1,7 @@ // CSMA/CD protocol - probabilistic version of kronos model (3 stations) // gxn/dxp 04/12/01 -nondeterministic +mdp // note made changes since cannot have strict inequalities // in digital clocks approach and suppose a station only sends one message @@ -131,8 +131,8 @@ endrewards label "all_delivered" = s1=4&s2=4&s3=4&s4=4; label "one_delivered" = s1=4|s2=4|s3=4|s4=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2)|(cd4=K & s4=1 & b=2); -label "succes_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4)|(cd4<=1 & s4=4); -label "succes_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4)|(cd4<=2 & s4=4); +label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4)|(cd4<=1 & s4=4); +label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4)|(cd4<=2 & s4=4); label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1)|(cd4=1); label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2)|(cd4=2); diff --git a/prism-examples/csma/csma4.pctl b/prism-examples/csma/csma4.pctl index 56efb5e6..ae5ee091 100644 --- a/prism-examples/csma/csma4.pctl +++ b/prism-examples/csma/csma4.pctl @@ -8,27 +8,27 @@ Rmin=?[ F "one_delivered" ] Rmax=?[ F "one_delivered" ] // message of any station eventually delivered before i backoffs -Pmin=?[true U "succes_with_backoff_under_1" ] -Pmax=?[true U "succes_with_backoff_under_1" ] -Pmin=?[true U "succes_with_backoff_under_2" ] -Pmax=?[true U "succes_with_backoff_under_2" ] -Pmin=?[true U "succes_with_backoff_under_3" ] -Pmax=?[true U "succes_with_backoff_under_3" ] -Pmin=?[true U "succes_with_backoff_under_4" ] -Pmax=?[true U "succes_with_backoff_under_4" ] +Pmin=?[ F "success_with_backoff_under_1" ] +Pmax=?[ F "success_with_backoff_under_1" ] +Pmin=?[ F "success_with_backoff_under_2" ] +Pmax=?[ F "success_with_backoff_under_2" ] +Pmin=?[ F "success_with_backoff_under_3" ] +Pmax=?[ F "success_with_backoff_under_3" ] +Pmin=?[ F "success_with_backoff_under_4" ] +Pmax=?[ F "success_with_backoff_under_4" ] // probability all sent successfully before a collision with max backoff Pmin=?[ !"collision_max_backoff" U "all_delivered" ] Pmax=?[ !"collision_max_backoff" U "all_delivered" ] // probability a station suffers i collisions -Pmin=?[true U "collisions_equal_1" ] -Pmax=?[true U "collisions_equal_1" ] -Pmin=?[true U "collisions_equal_2" ] -Pmax=?[true U "collisions_equal_2" ] -Pmin=?[true U "collisions_equal_3" ] -Pmax=?[true U "collisions_equal_3" ] -Pmin=?[true U "collisions_equal_4" ] -Pmax=?[true U "collisions_equal_4" ] +Pmin=?[ F "collisions_equal_1" ] +Pmax=?[ F "collisions_equal_1" ] +Pmin=?[ F "collisions_equal_2" ] +Pmax=?[ F "collisions_equal_2" ] +Pmin=?[ F "collisions_equal_3" ] +Pmax=?[ F "collisions_equal_3" ] +Pmin=?[ F "collisions_equal_4" ] +Pmax=?[ F "collisions_equal_4" ] diff --git a/prism-examples/csma/csma4_2.nm b/prism-examples/csma/csma4_2.nm index 3ca7c82b..8c57cd7e 100644 --- a/prism-examples/csma/csma4_2.nm +++ b/prism-examples/csma/csma4_2.nm @@ -1,7 +1,7 @@ // CSMA/CD protocol - probabilistic version of kronos model (3 stations) // gxn/dxp 04/12/01 -nondeterministic +mdp // note made changes since cannot have strict inequalities // in digital clocks approach and suppose a station only sends one message @@ -123,10 +123,10 @@ endrewards 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); -label "succes_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4); -label "succes_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4); -label "succes_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4); -label "succes_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4); +label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4); +label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4); +label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4); +label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4); label "collisions_equal_1" = (cd1=1)|(cd2=1); label "collisions_equal_2" = (cd1=2)|(cd2=2); label "collisions_equal_3" = (cd1=3)|(cd2=3); diff --git a/prism-examples/csma/csma4_3.nm b/prism-examples/csma/csma4_3.nm index d232ede5..5fa8de32 100644 --- a/prism-examples/csma/csma4_3.nm +++ b/prism-examples/csma/csma4_3.nm @@ -1,7 +1,7 @@ // CSMA/CD protocol - probabilistic version of kronos model (3 stations) // gxn/dxp 04/12/01 -nondeterministic +mdp // note made changes since cannot have strict inequalities // in digital clocks approach and suppose a station only sends one message @@ -128,10 +128,10 @@ endrewards 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); -label "succes_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4); -label "succes_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4); -label "succes_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4); -label "succes_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4); +label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4); +label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4); +label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4); +label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4); label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1); label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2); label "collisions_equal_3" = (cd1=3)|(cd2=3)|(cd3=3); diff --git a/prism-examples/csma/csma4_4.nm b/prism-examples/csma/csma4_4.nm index b150a834..65786dec 100644 --- a/prism-examples/csma/csma4_4.nm +++ b/prism-examples/csma/csma4_4.nm @@ -1,7 +1,7 @@ // CSMA/CD protocol - probabilistic version of kronos model (3 stations) // gxn/dxp 04/12/01 -nondeterministic +mdp // note made changes since cannot have strict inequalities // in digital clocks approach and suppose a station only sends one message @@ -133,10 +133,10 @@ endrewards label "all_delivered" = s1=4&s2=4&s3=4&s4=4; label "one_delivered" = s1=4|s2=4|s3=4|s4=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2)|(cd4=K & s4=1 & b=2); -label "succes_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4)|(cd4<=1 & s4=4); -label "succes_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4)|(cd4<=2 & s4=4); -label "succes_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4)|(cd4<=3 & s4=4); -label "succes_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4)|(cd4<=4 & s4=4); +label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4)|(cd4<=1 & s4=4); +label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4)|(cd4<=2 & s4=4); +label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4)|(cd4<=3 & s4=4); +label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4)|(cd4<=4 & s4=4); label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1)|(cd4=1); label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2)|(cd4=2); label "collisions_equal_3" = (cd1=3)|(cd2=3)|(cd3=3)|(cd4=3); diff --git a/prism-examples/csma/csma6.pctl b/prism-examples/csma/csma6.pctl index 1bec31a9..3b363c69 100644 --- a/prism-examples/csma/csma6.pctl +++ b/prism-examples/csma/csma6.pctl @@ -8,35 +8,35 @@ Rmin=?[ F "one_delivered" ] Rmax=?[ F "one_delivered" ] // message of any station eventually delivered before i backoffs -Pmin=?[true U "succes_with_backoff_under_1" ] -Pmax=?[true U "succes_with_backoff_under_1" ] -Pmin=?[true U "succes_with_backoff_under_2" ] -Pmax=?[true U "succes_with_backoff_under_2" ] -Pmin=?[true U "succes_with_backoff_under_3" ] -Pmax=?[true U "succes_with_backoff_under_3" ] -Pmin=?[true U "succes_with_backoff_under_4" ] -Pmax=?[true U "succes_with_backoff_under_4" ] -Pmin=?[true U "succes_with_backoff_under_5" ] -Pmax=?[true U "succes_with_backoff_under_5" ] -Pmin=?[true U "succes_with_backoff_under_6" ] -Pmax=?[true U "succes_with_backoff_under_6" ] +Pmin=?[ F "success_with_backoff_under_1" ] +Pmax=?[ F "success_with_backoff_under_1" ] +Pmin=?[ F "success_with_backoff_under_2" ] +Pmax=?[ F "success_with_backoff_under_2" ] +Pmin=?[ F "success_with_backoff_under_3" ] +Pmax=?[ F "success_with_backoff_under_3" ] +Pmin=?[ F "success_with_backoff_under_4" ] +Pmax=?[ F "success_with_backoff_under_4" ] +Pmin=?[ F "success_with_backoff_under_5" ] +Pmax=?[ F "success_with_backoff_under_5" ] +Pmin=?[ F "success_with_backoff_under_6" ] +Pmax=?[ F "success_with_backoff_under_6" ] // probability all sent successfully before a collision with max backoff Pmin=?[ !"collision_max_backoff" U "all_delivered" ] Pmax=?[ !"collision_max_backoff" U "all_delivered" ] // probability a station suffers i collisions -Pmin=?[true U "collisions_equal_1" ] -Pmax=?[true U "collisions_equal_1" ] -Pmin=?[true U "collisions_equal_2" ] -Pmax=?[true U "collisions_equal_2" ] -Pmin=?[true U "collisions_equal_3" ] -Pmax=?[true U "collisions_equal_3" ] -Pmin=?[true U "collisions_equal_4" ] -Pmax=?[true U "collisions_equal_4" ] -Pmin=?[true U "collisions_equal_5" ] -Pmax=?[true U "collisions_equal_5" ] -Pmin=?[true U "collisions_equal_6" ] -Pmax=?[true U "collisions_equal_6" ] +Pmin=?[ F "collisions_equal_1" ] +Pmax=?[ F "collisions_equal_1" ] +Pmin=?[ F "collisions_equal_2" ] +Pmax=?[ F "collisions_equal_2" ] +Pmin=?[ F "collisions_equal_3" ] +Pmax=?[ F "collisions_equal_3" ] +Pmin=?[ F "collisions_equal_4" ] +Pmax=?[ F "collisions_equal_4" ] +Pmin=?[ F "collisions_equal_5" ] +Pmax=?[ F "collisions_equal_5" ] +Pmin=?[ F "collisions_equal_6" ] +Pmax=?[ F "collisions_equal_6" ] diff --git a/prism-examples/csma/csma6_2.nm b/prism-examples/csma/csma6_2.nm index 5a34afb2..d189eb4c 100644 --- a/prism-examples/csma/csma6_2.nm +++ b/prism-examples/csma/csma6_2.nm @@ -1,7 +1,7 @@ // CSMA/CD protocol - probabilistic version of kronos model (3 stations) // gxn/dxp 04/12/01 -nondeterministic +mdp // note made changes since cannot have strict inequalities // in digital clocks approach and suppose a station only sends one message @@ -125,12 +125,12 @@ endrewards 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); -label "succes_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4); -label "succes_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4); -label "succes_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4); -label "succes_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4); -label "succes_with_backoff_under_5" = (cd1<=5 & s1=4)|(cd2<=5 & s2=4); -label "succes_with_backoff_under_6" = (cd1<=6 & s1=4)|(cd2<=6 & s2=4); +label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4); +label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4); +label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4); +label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4); +label "success_with_backoff_under_5" = (cd1<=5 & s1=4)|(cd2<=5 & s2=4); +label "success_with_backoff_under_6" = (cd1<=6 & s1=4)|(cd2<=6 & s2=4); label "collisions_equal_1" = (cd1=1)|(cd2=1); label "collisions_equal_2" = (cd1=2)|(cd2=2); label "collisions_equal_3" = (cd1=3)|(cd2=3); diff --git a/prism-examples/csma/csma6_3.nm b/prism-examples/csma/csma6_3.nm index 09ba8e9f..3938f9b9 100644 --- a/prism-examples/csma/csma6_3.nm +++ b/prism-examples/csma/csma6_3.nm @@ -1,7 +1,7 @@ // CSMA/CD protocol - probabilistic version of kronos model (3 stations) // gxn/dxp 04/12/01 -nondeterministic +mdp // note made changes since cannot have strict inequalities // in digital clocks approach and suppose a station only sends one message @@ -130,12 +130,12 @@ endrewards 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); -label "succes_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4); -label "succes_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4); -label "succes_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4); -label "succes_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4); -label "succes_with_backoff_under_5" = (cd1<=5 & s1=4)|(cd2<=5 & s2=4)|(cd3<=5 & s3=4); -label "succes_with_backoff_under_6" = (cd1<=6 & s1=4)|(cd2<=6 & s2=4)|(cd3<=6 & s3=4); +label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4); +label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4); +label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4); +label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4); +label "success_with_backoff_under_5" = (cd1<=5 & s1=4)|(cd2<=5 & s2=4)|(cd3<=5 & s3=4); +label "success_with_backoff_under_6" = (cd1<=6 & s1=4)|(cd2<=6 & s2=4)|(cd3<=6 & s3=4); label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1); label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2); label "collisions_equal_3" = (cd1=3)|(cd2=3)|(cd3=3); diff --git a/prism-examples/csma/csma6_4.nm b/prism-examples/csma/csma6_4.nm index a77dc13c..4de4368e 100644 --- a/prism-examples/csma/csma6_4.nm +++ b/prism-examples/csma/csma6_4.nm @@ -1,7 +1,7 @@ // CSMA/CD protocol - probabilistic version of kronos model (3 stations) // gxn/dxp 04/12/01 -nondeterministic +mdp // note made changes since cannot have strict inequalities // in digital clocks approach and suppose a station only sends one message @@ -135,12 +135,12 @@ endrewards label "all_delivered" = s1=4&s2=4&s3=4&s4=4; label "one_delivered" = s1=4|s2=4|s3=4|s4=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2)|(cd4=K & s4=1 & b=2); -label "succes_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4)|(cd4<=1 & s4=4); -label "succes_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4)|(cd4<=2 & s4=4); -label "succes_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4)|(cd4<=3 & s4=4); -label "succes_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4)|(cd4<=4 & s4=4); -label "succes_with_backoff_under_5" = (cd1<=5 & s1=4)|(cd2<=5 & s2=4)|(cd3<=5 & s3=4)|(cd4<=5 & s4=4); -label "succes_with_backoff_under_6" = (cd1<=6 & s1=4)|(cd2<=6 & s2=4)|(cd3<=6 & s3=4)|(cd4<=6 & s4=4); +label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4)|(cd4<=1 & s4=4); +label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4)|(cd4<=2 & s4=4); +label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4)|(cd4<=3 & s4=4); +label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4)|(cd4<=4 & s4=4); +label "success_with_backoff_under_5" = (cd1<=5 & s1=4)|(cd2<=5 & s2=4)|(cd3<=5 & s3=4)|(cd4<=5 & s4=4); +label "success_with_backoff_under_6" = (cd1<=6 & s1=4)|(cd2<=6 & s2=4)|(cd3<=6 & s3=4)|(cd4<=6 & s4=4); label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1)|(cd4=1); label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2)|(cd4=2); label "collisions_equal_3" = (cd1=3)|(cd2=3)|(cd3=3)|(cd4=3);