s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

CSMA tweaks. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@861 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
85f53564c9
commit
39d7447625
15 changed files with 100 additions and 100 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      prism-examples/csma/.autopp
  2. 8
      prism-examples/csma/.csmaK.pctl.pp
  3. 4
      prism-examples/csma/.csmaK_N.nm.pp
  4. 16
      prism-examples/csma/csma2.pctl
  5. 6
      prism-examples/csma/csma2_2.nm
  6. 6
      prism-examples/csma/csma2_3.nm
  7. 6
      prism-examples/csma/csma2_4.nm
  8. 32
      prism-examples/csma/csma4.pctl
  9. 10
      prism-examples/csma/csma4_2.nm
  10. 10
      prism-examples/csma/csma4_3.nm
  11. 10
      prism-examples/csma/csma4_4.nm
  12. 48
      prism-examples/csma/csma6.pctl
  13. 14
      prism-examples/csma/csma6_2.nm
  14. 14
      prism-examples/csma/csma6_3.nm
  15. 14
      prism-examples/csma/csma6_4.nm

2
prism-examples/csma/.autopp
View File

@ -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

8
prism-examples/csma/.csmaK.pctl.pp
View File

@ -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#

4
prism-examples/csma/.csmaNK.nm.pp → prism-examples/csma/.csmaK_N.nm.pp
View File

@ -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#;

16
prism-examples/csma/csma2.pctl
View File

@ -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" ]

6
prism-examples/csma/csma2_2.nm
View File

@ -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);

6
prism-examples/csma/csma2_3.nm
View File

@ -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);

6
prism-examples/csma/csma2_4.nm
View File

@ -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);

32
prism-examples/csma/csma4.pctl
View File

@ -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" ]

10
prism-examples/csma/csma4_2.nm
View File

@ -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);

10
prism-examples/csma/csma4_3.nm
View File

@ -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);

10
prism-examples/csma/csma4_4.nm
View File

@ -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);

48
prism-examples/csma/csma6.pctl
View File

@ -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" ]

14
prism-examples/csma/csma6_2.nm
View File

@ -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);

14
prism-examples/csma/csma6_3.nm
View File

@ -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);

14
prism-examples/csma/csma6_4.nm
View File

@ -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);

Write Preview
Loading…
Cancel
Save