Browse Source

Re-tidy csma.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@892 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 17 years ago
parent
commit
c9c0b1176d
  1. 27
      prism-examples/csma/.csmaK.pctl.pp

27
prism-examples/csma/.csmaK.pctl.pp

@ -1,27 +0,0 @@
#const K#
// expected time for all messages to be sent
R{"time"}min=?[ F "all_delivered" ]
R{"time"}max=?[ F "all_delivered" ]
// expected time for one message to be sent
Rmin=?[ F "one_delivered" ]
Rmax=?[ F "one_delivered" ]
// message of any station eventually delivered before i backoffs
#for i=1:K#
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
Pmin=?[ !"collision_max_backoff" U "all_delivered" ]
Pmax=?[ !"collision_max_backoff" U "all_delivered" ]
// probability a station suffers i collisions
#for i=1:K#
Pmin=?[ F "collisions_equal_#i#" ]
Pmax=?[ F "collisions_equal_#i#" ]
#end#
Loading…
Cancel
Save