Blame view
prism-4.3-linux64/examples/wlan/wlan.pctl
757 Bytes
8146dcf82 first commit |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 |
// with probability 1, eventually both stations have sent their packet correctly P>=1 [ true U s1=12 & s2=12 ]; // maximum probability that either station's backoff counter reaches k const int k; Pmax=? [ true U bc1=k | bc2=k ]; // maximum expected number of collisions R{"collisions"}max=? [ F s1=12 & s2=12 ]; // both send correctly // maximum expected time R{"time"}max=? [ F s1=12 & s2=12 ]; // both send correctly R{"time"}max=? [ F s1=12 | s2=12 ]; // either sends correctly R{"time"}max=? [ F s1=12 ]; // station 1 sends correctly // maximum expected cost R{"cost"}max=? [ F s1=12 & s2=12 ]; // both send correctly R{"cost"}max=? [ F s1=12 | s2=12 ]; // either sends R{"cost"}max=? [ F s1=12 ]; // station 1 sends correctly |