Browse Source
Removed extra files.
Removed extra files.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@865 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
17 years ago
5 changed files with 0 additions and 717 deletions
-
142prism-examples/csma/csma2_6.nm
-
135prism-examples/csma/csma3_2.nm
-
141prism-examples/csma/csma3_4.nm
-
147prism-examples/csma/csma3_6.nm
-
152prism-examples/csma/csma4_6.nm
@ -1,142 +0,0 @@ |
|||
// CSMA/CD protocol - probabilistic version of kronos model (3 stations) |
|||
// gxn/dxp 04/12/01 |
|||
|
|||
nondeterministic |
|||
|
|||
// note made changes since cannot have strict inequalities |
|||
// in digital clocks approach and suppose a station only sends one message |
|||
|
|||
// actual parameters |
|||
const int N = 2; // number of processes |
|||
const int K = 6; // exponential backoff limit |
|||
const int slot = 2*sigma; // length of slot |
|||
const int M = floor(pow(2, K))-1 ; // max number of slots to wait |
|||
//const int lambda=782; |
|||
//const int sigma=26; |
|||
|
|||
// simplified parameters scaled |
|||
const int sigma=1; // time for messages to propagate along the bus |
|||
const int lambda=30; // time to send a message |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// the bus |
|||
module bus |
|||
|
|||
b : [0..2]; |
|||
// b=0 - idle |
|||
// b=1 - active |
|||
// b=2 - collision |
|||
|
|||
// clocks of bus |
|||
y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) |
|||
y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) |
|||
|
|||
// a sender sends (ok - no other message being sent) |
|||
[send1] (b=0) -> (b'=1); |
|||
[send2] (b=0) -> (b'=1); |
|||
|
|||
// a sender sends (bus busy - collision) |
|||
[send1] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
[send2] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
|
|||
// finish sending |
|||
[end1] (b=1) -> (b'=0) & (y1'=0); |
|||
[end2] (b=1) -> (b'=0) & (y1'=0); |
|||
|
|||
// bus busy |
|||
[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
|
|||
// collision detected |
|||
[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); |
|||
|
|||
// time passage |
|||
[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 |
|||
[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 |
|||
[time] (b=2) & (y2<sigma) -> (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// model of first sender |
|||
module station1 |
|||
|
|||
// LOCAL STATE |
|||
s1 : [0..5]; |
|||
// s1=0 - initial state |
|||
// s1=1 - transmit |
|||
// s1=2 - collision (set backoff) |
|||
// s1=3 - wait (bus busy) |
|||
// s1=4 - successfully sent |
|||
|
|||
// LOCAL CLOCK |
|||
x1 : [0..max(lambda,slot)]; |
|||
|
|||
// BACKOFF COUNTER (number of slots to wait) |
|||
bc1 : [0..M]; |
|||
|
|||
// COLLISION COUNTER |
|||
cd1 : [0..K]; |
|||
|
|||
// start sending |
|||
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending |
|||
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff |
|||
|
|||
// transmitting |
|||
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass |
|||
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished |
|||
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) |
|||
[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important |
|||
|
|||
// set backoff (no time can pass in this state) |
|||
// probability depends on which transmission this is (cd1) |
|||
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; |
|||
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; |
|||
[] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (bc1'=0) + 1/8 : (s1'=3) & (bc1'=1) + 1/8 : (s1'=3) & (bc1'=2) + 1/8 : (s1'=3) & (bc1'=3) + 1/8 : (s1'=3) & (bc1'=4) + 1/8 : (s1'=3) & (bc1'=5) + 1/8 : (s1'=3) & (bc1'=6) + 1/8 : (s1'=3) & (bc1'=7) ; |
|||
[] s1=2 & cd1=4 -> 1/16 : (s1'=3) & (bc1'=0) + 1/16 : (s1'=3) & (bc1'=1) + 1/16 : (s1'=3) & (bc1'=2) + 1/16 : (s1'=3) & (bc1'=3) + 1/16 : (s1'=3) & (bc1'=4) + 1/16 : (s1'=3) & (bc1'=5) + 1/16 : (s1'=3) & (bc1'=6) + 1/16 : (s1'=3) & (bc1'=7) + 1/16 : (s1'=3) & (bc1'=8) + 1/16 : (s1'=3) & (bc1'=9) + 1/16 : (s1'=3) & (bc1'=10) + 1/16 : (s1'=3) & (bc1'=11) + 1/16 : (s1'=3) & (bc1'=12) + 1/16 : (s1'=3) & (bc1'=13) + 1/16 : (s1'=3) & (bc1'=14) + 1/16 : (s1'=3) & (bc1'=15) ; |
|||
[] s1=2 & cd1=5 -> 1/32 : (s1'=3) & (bc1'=0) + 1/32 : (s1'=3) & (bc1'=1) + 1/32 : (s1'=3) & (bc1'=2) + 1/32 : (s1'=3) & (bc1'=3) + 1/32 : (s1'=3) & (bc1'=4) + 1/32 : (s1'=3) & (bc1'=5) + 1/32 : (s1'=3) & (bc1'=6) + 1/32 : (s1'=3) & (bc1'=7) + 1/32 : (s1'=3) & (bc1'=8) + 1/32 : (s1'=3) & (bc1'=9) + 1/32 : (s1'=3) & (bc1'=10) + 1/32 : (s1'=3) & (bc1'=11) + 1/32 : (s1'=3) & (bc1'=12) + 1/32 : (s1'=3) & (bc1'=13) + 1/32 : (s1'=3) & (bc1'=14) + 1/32 : (s1'=3) & (bc1'=15) + 1/32 : (s1'=3) & (bc1'=16) + 1/32 : (s1'=3) & (bc1'=17) + 1/32 : (s1'=3) & (bc1'=18) + 1/32 : (s1'=3) & (bc1'=19) + 1/32 : (s1'=3) & (bc1'=20) + 1/32 : (s1'=3) & (bc1'=21) + 1/32 : (s1'=3) & (bc1'=22) + 1/32 : (s1'=3) & (bc1'=23) + 1/32 : (s1'=3) & (bc1'=24) + 1/32 : (s1'=3) & (bc1'=25) + 1/32 : (s1'=3) & (bc1'=26) + 1/32 : (s1'=3) & (bc1'=27) + 1/32 : (s1'=3) & (bc1'=28) + 1/32 : (s1'=3) & (bc1'=29) + 1/32 : (s1'=3) & (bc1'=30) + 1/32 : (s1'=3) & (bc1'=31) ; |
|||
[] s1=2 & cd1=6 -> 1/64 : (s1'=3) & (bc1'=0) + 1/64 : (s1'=3) & (bc1'=1) + 1/64 : (s1'=3) & (bc1'=2) + 1/64 : (s1'=3) & (bc1'=3) + 1/64 : (s1'=3) & (bc1'=4) + 1/64 : (s1'=3) & (bc1'=5) + 1/64 : (s1'=3) & (bc1'=6) + 1/64 : (s1'=3) & (bc1'=7) + 1/64 : (s1'=3) & (bc1'=8) + 1/64 : (s1'=3) & (bc1'=9) + 1/64 : (s1'=3) & (bc1'=10) + 1/64 : (s1'=3) & (bc1'=11) + 1/64 : (s1'=3) & (bc1'=12) + 1/64 : (s1'=3) & (bc1'=13) + 1/64 : (s1'=3) & (bc1'=14) + 1/64 : (s1'=3) & (bc1'=15) + 1/64 : (s1'=3) & (bc1'=16) + 1/64 : (s1'=3) & (bc1'=17) + 1/64 : (s1'=3) & (bc1'=18) + 1/64 : (s1'=3) & (bc1'=19) + 1/64 : (s1'=3) & (bc1'=20) + 1/64 : (s1'=3) & (bc1'=21) + 1/64 : (s1'=3) & (bc1'=22) + 1/64 : (s1'=3) & (bc1'=23) + 1/64 : (s1'=3) & (bc1'=24) + 1/64 : (s1'=3) & (bc1'=25) + 1/64 : (s1'=3) & (bc1'=26) + 1/64 : (s1'=3) & (bc1'=27) + 1/64 : (s1'=3) & (bc1'=28) + 1/64 : (s1'=3) & (bc1'=29) + 1/64 : (s1'=3) & (bc1'=30) + 1/64 : (s1'=3) & (bc1'=31) + 1/64 : (s1'=3) & (bc1'=32) + 1/64 : (s1'=3) & (bc1'=33) + 1/64 : (s1'=3) & (bc1'=34) + 1/64 : (s1'=3) & (bc1'=35) + 1/64 : (s1'=3) & (bc1'=36) + 1/64 : (s1'=3) & (bc1'=37) + 1/64 : (s1'=3) & (bc1'=38) + 1/64 : (s1'=3) & (bc1'=39) + 1/64 : (s1'=3) & (bc1'=40) + 1/64 : (s1'=3) & (bc1'=41) + 1/64 : (s1'=3) & (bc1'=42) + 1/64 : (s1'=3) & (bc1'=43) + 1/64 : (s1'=3) & (bc1'=44) + 1/64 : (s1'=3) & (bc1'=45) + 1/64 : (s1'=3) & (bc1'=46) + 1/64 : (s1'=3) & (bc1'=47) + 1/64 : (s1'=3) & (bc1'=48) + 1/64 : (s1'=3) & (bc1'=49) + 1/64 : (s1'=3) & (bc1'=50) + 1/64 : (s1'=3) & (bc1'=51) + 1/64 : (s1'=3) & (bc1'=52) + 1/64 : (s1'=3) & (bc1'=53) + 1/64 : (s1'=3) & (bc1'=54) + 1/64 : (s1'=3) & (bc1'=55) + 1/64 : (s1'=3) & (bc1'=56) + 1/64 : (s1'=3) & (bc1'=57) + 1/64 : (s1'=3) & (bc1'=58) + 1/64 : (s1'=3) & (bc1'=59) + 1/64 : (s1'=3) & (bc1'=60) + 1/64 : (s1'=3) & (bc1'=61) + 1/64 : (s1'=3) & (bc1'=62) + 1/64 : (s1'=3) & (bc1'=63) ; |
|||
|
|||
// wait until backoff counter reaches 0 then send again |
|||
[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot) |
|||
[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) |
|||
[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) |
|||
[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) |
|||
|
|||
// once finished nothing matters |
|||
[time] (s1>=4) -> (x1'=0); |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// construct further stations through renaming |
|||
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// reward structure for expected time |
|||
rewards |
|||
[time] true : 1; |
|||
endrewards |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
label "all_delivered" = s1=4&s2=4; |
|||
label "one_delivered" = s1=4|s2=4; |
|||
label "max_baxkoff_reached" = cd1=K&cd2=K; |
|||
|
|||
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 "collisions_equal_1" = (cd1=1)|(cd2=1); |
|||
label "collisions_equal_2" = (cd1=2)|(cd2=2); |
|||
label "collisions_equal_3" = (cd1=3)|(cd2=3); |
|||
label "collisions_equal_4" = (cd1=4)|(cd2=4); |
|||
label "collisions_equal_5" = (cd1=5)|(cd2=5); |
|||
label "collisions_equal_6" = (cd1=6)|(cd2=6); |
|||
|
|||
|
|||
@ -1,135 +0,0 @@ |
|||
// CSMA/CD protocol - probabilistic version of kronos model (3 stations) |
|||
// gxn/dxp 04/12/01 |
|||
|
|||
nondeterministic |
|||
|
|||
// note made changes since cannot have strict inequalities |
|||
// in digital clocks approach and suppose a station only sends one message |
|||
|
|||
// actual parameters |
|||
const int N = 3; // number of processes |
|||
const int K = 2; // exponential backoff limit |
|||
const int slot = 2*sigma; // length of slot |
|||
const int M = floor(pow(2, K))-1 ; // max number of slots to wait |
|||
//const int lambda=782; |
|||
//const int sigma=26; |
|||
|
|||
// simplified parameters scaled |
|||
const int sigma=1; // time for messages to propagate along the bus |
|||
const int lambda=30; // time to send a message |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// the bus |
|||
module bus |
|||
|
|||
b : [0..2]; |
|||
// b=0 - idle |
|||
// b=1 - active |
|||
// b=2 - collision |
|||
|
|||
// clocks of bus |
|||
y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) |
|||
y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) |
|||
|
|||
// a sender sends (ok - no other message being sent) |
|||
[send1] (b=0) -> (b'=1); |
|||
[send2] (b=0) -> (b'=1); |
|||
[send3] (b=0) -> (b'=1); |
|||
|
|||
// a sender sends (bus busy - collision) |
|||
[send1] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
[send2] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
[send3] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
|
|||
// finish sending |
|||
[end1] (b=1) -> (b'=0) & (y1'=0); |
|||
[end2] (b=1) -> (b'=0) & (y1'=0); |
|||
[end3] (b=1) -> (b'=0) & (y1'=0); |
|||
|
|||
// bus busy |
|||
[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
[busy3] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
|
|||
// collision detected |
|||
[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); |
|||
|
|||
// time passage |
|||
[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 |
|||
[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 |
|||
[time] (b=2) & (y2<sigma) -> (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// model of first sender |
|||
module station1 |
|||
|
|||
// LOCAL STATE |
|||
s1 : [0..5]; |
|||
// s1=0 - initial state |
|||
// s1=1 - transmit |
|||
// s1=2 - collision (set backoff) |
|||
// s1=3 - wait (bus busy) |
|||
// s1=4 - successfully sent |
|||
|
|||
// LOCAL CLOCK |
|||
x1 : [0..max(lambda,slot)]; |
|||
|
|||
// BACKOFF COUNTER (number of slots to wait) |
|||
bc1 : [0..M]; |
|||
|
|||
// COLLISION COUNTER |
|||
cd1 : [0..K]; |
|||
|
|||
// start sending |
|||
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending |
|||
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff |
|||
|
|||
// transmitting |
|||
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass |
|||
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished |
|||
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) |
|||
[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important |
|||
|
|||
// set backoff (no time can pass in this state) |
|||
// probability depends on which transmission this is (cd1) |
|||
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; |
|||
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; |
|||
|
|||
// wait until backoff counter reaches 0 then send again |
|||
[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot) |
|||
[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) |
|||
[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) |
|||
[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) |
|||
|
|||
// once finished nothing matters |
|||
[time] (s1>=4) -> (x1'=0); |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// construct further stations through renaming |
|||
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule |
|||
module station3=station1[s1=s3,x1=x3,cd1=cd3,bc1=bc3,send1=send3,busy1=busy3,end1=end3] endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// reward structure for expected time |
|||
rewards |
|||
[time] true : 1; |
|||
endrewards |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
label "all_delivered" = s1=4&s2=4&s3=4; |
|||
label "one_delivered" = s1=4|s2=4|s3=4; |
|||
label "max_baxkoff_reached" = cd1=K&cd2=K&cd3=K; |
|||
|
|||
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 "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1); |
|||
label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2); |
|||
|
|||
|
|||
@ -1,141 +0,0 @@ |
|||
// CSMA/CD protocol - probabilistic version of kronos model (3 stations) |
|||
// gxn/dxp 04/12/01 |
|||
|
|||
nondeterministic |
|||
|
|||
// note made changes since cannot have strict inequalities |
|||
// in digital clocks approach and suppose a station only sends one message |
|||
|
|||
// actual parameters |
|||
const int N = 3; // number of processes |
|||
const int K = 4; // exponential backoff limit |
|||
const int slot = 2*sigma; // length of slot |
|||
const int M = floor(pow(2, K))-1 ; // max number of slots to wait |
|||
//const int lambda=782; |
|||
//const int sigma=26; |
|||
|
|||
// simplified parameters scaled |
|||
const int sigma=1; // time for messages to propagate along the bus |
|||
const int lambda=30; // time to send a message |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// the bus |
|||
module bus |
|||
|
|||
b : [0..2]; |
|||
// b=0 - idle |
|||
// b=1 - active |
|||
// b=2 - collision |
|||
|
|||
// clocks of bus |
|||
y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) |
|||
y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) |
|||
|
|||
// a sender sends (ok - no other message being sent) |
|||
[send1] (b=0) -> (b'=1); |
|||
[send2] (b=0) -> (b'=1); |
|||
[send3] (b=0) -> (b'=1); |
|||
|
|||
// a sender sends (bus busy - collision) |
|||
[send1] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
[send2] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
[send3] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
|
|||
// finish sending |
|||
[end1] (b=1) -> (b'=0) & (y1'=0); |
|||
[end2] (b=1) -> (b'=0) & (y1'=0); |
|||
[end3] (b=1) -> (b'=0) & (y1'=0); |
|||
|
|||
// bus busy |
|||
[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
[busy3] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
|
|||
// collision detected |
|||
[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); |
|||
|
|||
// time passage |
|||
[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 |
|||
[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 |
|||
[time] (b=2) & (y2<sigma) -> (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// model of first sender |
|||
module station1 |
|||
|
|||
// LOCAL STATE |
|||
s1 : [0..5]; |
|||
// s1=0 - initial state |
|||
// s1=1 - transmit |
|||
// s1=2 - collision (set backoff) |
|||
// s1=3 - wait (bus busy) |
|||
// s1=4 - successfully sent |
|||
|
|||
// LOCAL CLOCK |
|||
x1 : [0..max(lambda,slot)]; |
|||
|
|||
// BACKOFF COUNTER (number of slots to wait) |
|||
bc1 : [0..M]; |
|||
|
|||
// COLLISION COUNTER |
|||
cd1 : [0..K]; |
|||
|
|||
// start sending |
|||
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending |
|||
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff |
|||
|
|||
// transmitting |
|||
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass |
|||
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished |
|||
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) |
|||
[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important |
|||
|
|||
// set backoff (no time can pass in this state) |
|||
// probability depends on which transmission this is (cd1) |
|||
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; |
|||
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; |
|||
[] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (bc1'=0) + 1/8 : (s1'=3) & (bc1'=1) + 1/8 : (s1'=3) & (bc1'=2) + 1/8 : (s1'=3) & (bc1'=3) + 1/8 : (s1'=3) & (bc1'=4) + 1/8 : (s1'=3) & (bc1'=5) + 1/8 : (s1'=3) & (bc1'=6) + 1/8 : (s1'=3) & (bc1'=7) ; |
|||
[] s1=2 & cd1=4 -> 1/16 : (s1'=3) & (bc1'=0) + 1/16 : (s1'=3) & (bc1'=1) + 1/16 : (s1'=3) & (bc1'=2) + 1/16 : (s1'=3) & (bc1'=3) + 1/16 : (s1'=3) & (bc1'=4) + 1/16 : (s1'=3) & (bc1'=5) + 1/16 : (s1'=3) & (bc1'=6) + 1/16 : (s1'=3) & (bc1'=7) + 1/16 : (s1'=3) & (bc1'=8) + 1/16 : (s1'=3) & (bc1'=9) + 1/16 : (s1'=3) & (bc1'=10) + 1/16 : (s1'=3) & (bc1'=11) + 1/16 : (s1'=3) & (bc1'=12) + 1/16 : (s1'=3) & (bc1'=13) + 1/16 : (s1'=3) & (bc1'=14) + 1/16 : (s1'=3) & (bc1'=15) ; |
|||
|
|||
// wait until backoff counter reaches 0 then send again |
|||
[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot) |
|||
[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) |
|||
[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) |
|||
[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) |
|||
|
|||
// once finished nothing matters |
|||
[time] (s1>=4) -> (x1'=0); |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// construct further stations through renaming |
|||
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule |
|||
module station3=station1[s1=s3,x1=x3,cd1=cd3,bc1=bc3,send1=send3,busy1=busy3,end1=end3] endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// reward structure for expected time |
|||
rewards |
|||
[time] true : 1; |
|||
endrewards |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
label "all_delivered" = s1=4&s2=4&s3=4; |
|||
label "one_delivered" = s1=4|s2=4|s3=4; |
|||
label "max_baxkoff_reached" = cd1=K&cd2=K&cd3=K; |
|||
|
|||
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 "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); |
|||
label "collisions_equal_4" = (cd1=4)|(cd2=4)|(cd3=4); |
|||
|
|||
|
|||
@ -1,147 +0,0 @@ |
|||
// CSMA/CD protocol - probabilistic version of kronos model (3 stations) |
|||
// gxn/dxp 04/12/01 |
|||
|
|||
nondeterministic |
|||
|
|||
// note made changes since cannot have strict inequalities |
|||
// in digital clocks approach and suppose a station only sends one message |
|||
|
|||
// actual parameters |
|||
const int N = 3; // number of processes |
|||
const int K = 6; // exponential backoff limit |
|||
const int slot = 2*sigma; // length of slot |
|||
const int M = floor(pow(2, K))-1 ; // max number of slots to wait |
|||
//const int lambda=782; |
|||
//const int sigma=26; |
|||
|
|||
// simplified parameters scaled |
|||
const int sigma=1; // time for messages to propagate along the bus |
|||
const int lambda=30; // time to send a message |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// the bus |
|||
module bus |
|||
|
|||
b : [0..2]; |
|||
// b=0 - idle |
|||
// b=1 - active |
|||
// b=2 - collision |
|||
|
|||
// clocks of bus |
|||
y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) |
|||
y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) |
|||
|
|||
// a sender sends (ok - no other message being sent) |
|||
[send1] (b=0) -> (b'=1); |
|||
[send2] (b=0) -> (b'=1); |
|||
[send3] (b=0) -> (b'=1); |
|||
|
|||
// a sender sends (bus busy - collision) |
|||
[send1] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
[send2] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
[send3] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
|
|||
// finish sending |
|||
[end1] (b=1) -> (b'=0) & (y1'=0); |
|||
[end2] (b=1) -> (b'=0) & (y1'=0); |
|||
[end3] (b=1) -> (b'=0) & (y1'=0); |
|||
|
|||
// bus busy |
|||
[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
[busy3] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
|
|||
// collision detected |
|||
[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); |
|||
|
|||
// time passage |
|||
[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 |
|||
[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 |
|||
[time] (b=2) & (y2<sigma) -> (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// model of first sender |
|||
module station1 |
|||
|
|||
// LOCAL STATE |
|||
s1 : [0..5]; |
|||
// s1=0 - initial state |
|||
// s1=1 - transmit |
|||
// s1=2 - collision (set backoff) |
|||
// s1=3 - wait (bus busy) |
|||
// s1=4 - successfully sent |
|||
|
|||
// LOCAL CLOCK |
|||
x1 : [0..max(lambda,slot)]; |
|||
|
|||
// BACKOFF COUNTER (number of slots to wait) |
|||
bc1 : [0..M]; |
|||
|
|||
// COLLISION COUNTER |
|||
cd1 : [0..K]; |
|||
|
|||
// start sending |
|||
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending |
|||
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff |
|||
|
|||
// transmitting |
|||
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass |
|||
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished |
|||
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) |
|||
[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important |
|||
|
|||
// set backoff (no time can pass in this state) |
|||
// probability depends on which transmission this is (cd1) |
|||
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; |
|||
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; |
|||
[] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (bc1'=0) + 1/8 : (s1'=3) & (bc1'=1) + 1/8 : (s1'=3) & (bc1'=2) + 1/8 : (s1'=3) & (bc1'=3) + 1/8 : (s1'=3) & (bc1'=4) + 1/8 : (s1'=3) & (bc1'=5) + 1/8 : (s1'=3) & (bc1'=6) + 1/8 : (s1'=3) & (bc1'=7) ; |
|||
[] s1=2 & cd1=4 -> 1/16 : (s1'=3) & (bc1'=0) + 1/16 : (s1'=3) & (bc1'=1) + 1/16 : (s1'=3) & (bc1'=2) + 1/16 : (s1'=3) & (bc1'=3) + 1/16 : (s1'=3) & (bc1'=4) + 1/16 : (s1'=3) & (bc1'=5) + 1/16 : (s1'=3) & (bc1'=6) + 1/16 : (s1'=3) & (bc1'=7) + 1/16 : (s1'=3) & (bc1'=8) + 1/16 : (s1'=3) & (bc1'=9) + 1/16 : (s1'=3) & (bc1'=10) + 1/16 : (s1'=3) & (bc1'=11) + 1/16 : (s1'=3) & (bc1'=12) + 1/16 : (s1'=3) & (bc1'=13) + 1/16 : (s1'=3) & (bc1'=14) + 1/16 : (s1'=3) & (bc1'=15) ; |
|||
[] s1=2 & cd1=5 -> 1/32 : (s1'=3) & (bc1'=0) + 1/32 : (s1'=3) & (bc1'=1) + 1/32 : (s1'=3) & (bc1'=2) + 1/32 : (s1'=3) & (bc1'=3) + 1/32 : (s1'=3) & (bc1'=4) + 1/32 : (s1'=3) & (bc1'=5) + 1/32 : (s1'=3) & (bc1'=6) + 1/32 : (s1'=3) & (bc1'=7) + 1/32 : (s1'=3) & (bc1'=8) + 1/32 : (s1'=3) & (bc1'=9) + 1/32 : (s1'=3) & (bc1'=10) + 1/32 : (s1'=3) & (bc1'=11) + 1/32 : (s1'=3) & (bc1'=12) + 1/32 : (s1'=3) & (bc1'=13) + 1/32 : (s1'=3) & (bc1'=14) + 1/32 : (s1'=3) & (bc1'=15) + 1/32 : (s1'=3) & (bc1'=16) + 1/32 : (s1'=3) & (bc1'=17) + 1/32 : (s1'=3) & (bc1'=18) + 1/32 : (s1'=3) & (bc1'=19) + 1/32 : (s1'=3) & (bc1'=20) + 1/32 : (s1'=3) & (bc1'=21) + 1/32 : (s1'=3) & (bc1'=22) + 1/32 : (s1'=3) & (bc1'=23) + 1/32 : (s1'=3) & (bc1'=24) + 1/32 : (s1'=3) & (bc1'=25) + 1/32 : (s1'=3) & (bc1'=26) + 1/32 : (s1'=3) & (bc1'=27) + 1/32 : (s1'=3) & (bc1'=28) + 1/32 : (s1'=3) & (bc1'=29) + 1/32 : (s1'=3) & (bc1'=30) + 1/32 : (s1'=3) & (bc1'=31) ; |
|||
[] s1=2 & cd1=6 -> 1/64 : (s1'=3) & (bc1'=0) + 1/64 : (s1'=3) & (bc1'=1) + 1/64 : (s1'=3) & (bc1'=2) + 1/64 : (s1'=3) & (bc1'=3) + 1/64 : (s1'=3) & (bc1'=4) + 1/64 : (s1'=3) & (bc1'=5) + 1/64 : (s1'=3) & (bc1'=6) + 1/64 : (s1'=3) & (bc1'=7) + 1/64 : (s1'=3) & (bc1'=8) + 1/64 : (s1'=3) & (bc1'=9) + 1/64 : (s1'=3) & (bc1'=10) + 1/64 : (s1'=3) & (bc1'=11) + 1/64 : (s1'=3) & (bc1'=12) + 1/64 : (s1'=3) & (bc1'=13) + 1/64 : (s1'=3) & (bc1'=14) + 1/64 : (s1'=3) & (bc1'=15) + 1/64 : (s1'=3) & (bc1'=16) + 1/64 : (s1'=3) & (bc1'=17) + 1/64 : (s1'=3) & (bc1'=18) + 1/64 : (s1'=3) & (bc1'=19) + 1/64 : (s1'=3) & (bc1'=20) + 1/64 : (s1'=3) & (bc1'=21) + 1/64 : (s1'=3) & (bc1'=22) + 1/64 : (s1'=3) & (bc1'=23) + 1/64 : (s1'=3) & (bc1'=24) + 1/64 : (s1'=3) & (bc1'=25) + 1/64 : (s1'=3) & (bc1'=26) + 1/64 : (s1'=3) & (bc1'=27) + 1/64 : (s1'=3) & (bc1'=28) + 1/64 : (s1'=3) & (bc1'=29) + 1/64 : (s1'=3) & (bc1'=30) + 1/64 : (s1'=3) & (bc1'=31) + 1/64 : (s1'=3) & (bc1'=32) + 1/64 : (s1'=3) & (bc1'=33) + 1/64 : (s1'=3) & (bc1'=34) + 1/64 : (s1'=3) & (bc1'=35) + 1/64 : (s1'=3) & (bc1'=36) + 1/64 : (s1'=3) & (bc1'=37) + 1/64 : (s1'=3) & (bc1'=38) + 1/64 : (s1'=3) & (bc1'=39) + 1/64 : (s1'=3) & (bc1'=40) + 1/64 : (s1'=3) & (bc1'=41) + 1/64 : (s1'=3) & (bc1'=42) + 1/64 : (s1'=3) & (bc1'=43) + 1/64 : (s1'=3) & (bc1'=44) + 1/64 : (s1'=3) & (bc1'=45) + 1/64 : (s1'=3) & (bc1'=46) + 1/64 : (s1'=3) & (bc1'=47) + 1/64 : (s1'=3) & (bc1'=48) + 1/64 : (s1'=3) & (bc1'=49) + 1/64 : (s1'=3) & (bc1'=50) + 1/64 : (s1'=3) & (bc1'=51) + 1/64 : (s1'=3) & (bc1'=52) + 1/64 : (s1'=3) & (bc1'=53) + 1/64 : (s1'=3) & (bc1'=54) + 1/64 : (s1'=3) & (bc1'=55) + 1/64 : (s1'=3) & (bc1'=56) + 1/64 : (s1'=3) & (bc1'=57) + 1/64 : (s1'=3) & (bc1'=58) + 1/64 : (s1'=3) & (bc1'=59) + 1/64 : (s1'=3) & (bc1'=60) + 1/64 : (s1'=3) & (bc1'=61) + 1/64 : (s1'=3) & (bc1'=62) + 1/64 : (s1'=3) & (bc1'=63) ; |
|||
|
|||
// wait until backoff counter reaches 0 then send again |
|||
[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot) |
|||
[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) |
|||
[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) |
|||
[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) |
|||
|
|||
// once finished nothing matters |
|||
[time] (s1>=4) -> (x1'=0); |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// construct further stations through renaming |
|||
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule |
|||
module station3=station1[s1=s3,x1=x3,cd1=cd3,bc1=bc3,send1=send3,busy1=busy3,end1=end3] endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// reward structure for expected time |
|||
rewards |
|||
[time] true : 1; |
|||
endrewards |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
label "all_delivered" = s1=4&s2=4&s3=4; |
|||
label "one_delivered" = s1=4|s2=4|s3=4; |
|||
label "max_baxkoff_reached" = cd1=K&cd2=K&cd3=K; |
|||
|
|||
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 "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); |
|||
label "collisions_equal_4" = (cd1=4)|(cd2=4)|(cd3=4); |
|||
label "collisions_equal_5" = (cd1=5)|(cd2=5)|(cd3=5); |
|||
label "collisions_equal_6" = (cd1=6)|(cd2=6)|(cd3=6); |
|||
|
|||
|
|||
@ -1,152 +0,0 @@ |
|||
// CSMA/CD protocol - probabilistic version of kronos model (3 stations) |
|||
// gxn/dxp 04/12/01 |
|||
|
|||
nondeterministic |
|||
|
|||
// note made changes since cannot have strict inequalities |
|||
// in digital clocks approach and suppose a station only sends one message |
|||
|
|||
// actual parameters |
|||
const int N = 4; // number of processes |
|||
const int K = 6; // exponential backoff limit |
|||
const int slot = 2*sigma; // length of slot |
|||
const int M = floor(pow(2, K))-1 ; // max number of slots to wait |
|||
//const int lambda=782; |
|||
//const int sigma=26; |
|||
|
|||
// simplified parameters scaled |
|||
const int sigma=1; // time for messages to propagate along the bus |
|||
const int lambda=30; // time to send a message |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// the bus |
|||
module bus |
|||
|
|||
b : [0..2]; |
|||
// b=0 - idle |
|||
// b=1 - active |
|||
// b=2 - collision |
|||
|
|||
// clocks of bus |
|||
y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) |
|||
y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) |
|||
|
|||
// a sender sends (ok - no other message being sent) |
|||
[send1] (b=0) -> (b'=1); |
|||
[send2] (b=0) -> (b'=1); |
|||
[send3] (b=0) -> (b'=1); |
|||
[send4] (b=0) -> (b'=1); |
|||
|
|||
// a sender sends (bus busy - collision) |
|||
[send1] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
[send2] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
[send3] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
[send4] (b=1|b=2) & (y1<sigma) -> (b'=2); |
|||
|
|||
// finish sending |
|||
[end1] (b=1) -> (b'=0) & (y1'=0); |
|||
[end2] (b=1) -> (b'=0) & (y1'=0); |
|||
[end3] (b=1) -> (b'=0) & (y1'=0); |
|||
[end4] (b=1) -> (b'=0) & (y1'=0); |
|||
|
|||
// bus busy |
|||
[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
[busy3] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
[busy4] (b=1|b=2) & (y1>=sigma) -> (b'=b); |
|||
|
|||
// collision detected |
|||
[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); |
|||
|
|||
// time passage |
|||
[time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 |
|||
[time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 |
|||
[time] (b=2) & (y2<sigma) -> (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
// model of first sender |
|||
module station1 |
|||
|
|||
// LOCAL STATE |
|||
s1 : [0..5]; |
|||
// s1=0 - initial state |
|||
// s1=1 - transmit |
|||
// s1=2 - collision (set backoff) |
|||
// s1=3 - wait (bus busy) |
|||
// s1=4 - successfully sent |
|||
|
|||
// LOCAL CLOCK |
|||
x1 : [0..max(lambda,slot)]; |
|||
|
|||
// BACKOFF COUNTER (number of slots to wait) |
|||
bc1 : [0..M]; |
|||
|
|||
// COLLISION COUNTER |
|||
cd1 : [0..K]; |
|||
|
|||
// start sending |
|||
[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending |
|||
[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff |
|||
|
|||
// transmitting |
|||
[time] (s1=1) & (x1<lambda) -> (x1'=min(x1+1,lambda)); // let time pass |
|||
[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished |
|||
[cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) |
|||
[cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important |
|||
|
|||
// set backoff (no time can pass in this state) |
|||
// probability depends on which transmission this is (cd1) |
|||
[] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; |
|||
[] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; |
|||
[] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (bc1'=0) + 1/8 : (s1'=3) & (bc1'=1) + 1/8 : (s1'=3) & (bc1'=2) + 1/8 : (s1'=3) & (bc1'=3) + 1/8 : (s1'=3) & (bc1'=4) + 1/8 : (s1'=3) & (bc1'=5) + 1/8 : (s1'=3) & (bc1'=6) + 1/8 : (s1'=3) & (bc1'=7) ; |
|||
[] s1=2 & cd1=4 -> 1/16 : (s1'=3) & (bc1'=0) + 1/16 : (s1'=3) & (bc1'=1) + 1/16 : (s1'=3) & (bc1'=2) + 1/16 : (s1'=3) & (bc1'=3) + 1/16 : (s1'=3) & (bc1'=4) + 1/16 : (s1'=3) & (bc1'=5) + 1/16 : (s1'=3) & (bc1'=6) + 1/16 : (s1'=3) & (bc1'=7) + 1/16 : (s1'=3) & (bc1'=8) + 1/16 : (s1'=3) & (bc1'=9) + 1/16 : (s1'=3) & (bc1'=10) + 1/16 : (s1'=3) & (bc1'=11) + 1/16 : (s1'=3) & (bc1'=12) + 1/16 : (s1'=3) & (bc1'=13) + 1/16 : (s1'=3) & (bc1'=14) + 1/16 : (s1'=3) & (bc1'=15) ; |
|||
[] s1=2 & cd1=5 -> 1/32 : (s1'=3) & (bc1'=0) + 1/32 : (s1'=3) & (bc1'=1) + 1/32 : (s1'=3) & (bc1'=2) + 1/32 : (s1'=3) & (bc1'=3) + 1/32 : (s1'=3) & (bc1'=4) + 1/32 : (s1'=3) & (bc1'=5) + 1/32 : (s1'=3) & (bc1'=6) + 1/32 : (s1'=3) & (bc1'=7) + 1/32 : (s1'=3) & (bc1'=8) + 1/32 : (s1'=3) & (bc1'=9) + 1/32 : (s1'=3) & (bc1'=10) + 1/32 : (s1'=3) & (bc1'=11) + 1/32 : (s1'=3) & (bc1'=12) + 1/32 : (s1'=3) & (bc1'=13) + 1/32 : (s1'=3) & (bc1'=14) + 1/32 : (s1'=3) & (bc1'=15) + 1/32 : (s1'=3) & (bc1'=16) + 1/32 : (s1'=3) & (bc1'=17) + 1/32 : (s1'=3) & (bc1'=18) + 1/32 : (s1'=3) & (bc1'=19) + 1/32 : (s1'=3) & (bc1'=20) + 1/32 : (s1'=3) & (bc1'=21) + 1/32 : (s1'=3) & (bc1'=22) + 1/32 : (s1'=3) & (bc1'=23) + 1/32 : (s1'=3) & (bc1'=24) + 1/32 : (s1'=3) & (bc1'=25) + 1/32 : (s1'=3) & (bc1'=26) + 1/32 : (s1'=3) & (bc1'=27) + 1/32 : (s1'=3) & (bc1'=28) + 1/32 : (s1'=3) & (bc1'=29) + 1/32 : (s1'=3) & (bc1'=30) + 1/32 : (s1'=3) & (bc1'=31) ; |
|||
[] s1=2 & cd1=6 -> 1/64 : (s1'=3) & (bc1'=0) + 1/64 : (s1'=3) & (bc1'=1) + 1/64 : (s1'=3) & (bc1'=2) + 1/64 : (s1'=3) & (bc1'=3) + 1/64 : (s1'=3) & (bc1'=4) + 1/64 : (s1'=3) & (bc1'=5) + 1/64 : (s1'=3) & (bc1'=6) + 1/64 : (s1'=3) & (bc1'=7) + 1/64 : (s1'=3) & (bc1'=8) + 1/64 : (s1'=3) & (bc1'=9) + 1/64 : (s1'=3) & (bc1'=10) + 1/64 : (s1'=3) & (bc1'=11) + 1/64 : (s1'=3) & (bc1'=12) + 1/64 : (s1'=3) & (bc1'=13) + 1/64 : (s1'=3) & (bc1'=14) + 1/64 : (s1'=3) & (bc1'=15) + 1/64 : (s1'=3) & (bc1'=16) + 1/64 : (s1'=3) & (bc1'=17) + 1/64 : (s1'=3) & (bc1'=18) + 1/64 : (s1'=3) & (bc1'=19) + 1/64 : (s1'=3) & (bc1'=20) + 1/64 : (s1'=3) & (bc1'=21) + 1/64 : (s1'=3) & (bc1'=22) + 1/64 : (s1'=3) & (bc1'=23) + 1/64 : (s1'=3) & (bc1'=24) + 1/64 : (s1'=3) & (bc1'=25) + 1/64 : (s1'=3) & (bc1'=26) + 1/64 : (s1'=3) & (bc1'=27) + 1/64 : (s1'=3) & (bc1'=28) + 1/64 : (s1'=3) & (bc1'=29) + 1/64 : (s1'=3) & (bc1'=30) + 1/64 : (s1'=3) & (bc1'=31) + 1/64 : (s1'=3) & (bc1'=32) + 1/64 : (s1'=3) & (bc1'=33) + 1/64 : (s1'=3) & (bc1'=34) + 1/64 : (s1'=3) & (bc1'=35) + 1/64 : (s1'=3) & (bc1'=36) + 1/64 : (s1'=3) & (bc1'=37) + 1/64 : (s1'=3) & (bc1'=38) + 1/64 : (s1'=3) & (bc1'=39) + 1/64 : (s1'=3) & (bc1'=40) + 1/64 : (s1'=3) & (bc1'=41) + 1/64 : (s1'=3) & (bc1'=42) + 1/64 : (s1'=3) & (bc1'=43) + 1/64 : (s1'=3) & (bc1'=44) + 1/64 : (s1'=3) & (bc1'=45) + 1/64 : (s1'=3) & (bc1'=46) + 1/64 : (s1'=3) & (bc1'=47) + 1/64 : (s1'=3) & (bc1'=48) + 1/64 : (s1'=3) & (bc1'=49) + 1/64 : (s1'=3) & (bc1'=50) + 1/64 : (s1'=3) & (bc1'=51) + 1/64 : (s1'=3) & (bc1'=52) + 1/64 : (s1'=3) & (bc1'=53) + 1/64 : (s1'=3) & (bc1'=54) + 1/64 : (s1'=3) & (bc1'=55) + 1/64 : (s1'=3) & (bc1'=56) + 1/64 : (s1'=3) & (bc1'=57) + 1/64 : (s1'=3) & (bc1'=58) + 1/64 : (s1'=3) & (bc1'=59) + 1/64 : (s1'=3) & (bc1'=60) + 1/64 : (s1'=3) & (bc1'=61) + 1/64 : (s1'=3) & (bc1'=62) + 1/64 : (s1'=3) & (bc1'=63) ; |
|||
|
|||
// wait until backoff counter reaches 0 then send again |
|||
[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot) |
|||
[time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) |
|||
[send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) |
|||
[busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) |
|||
|
|||
// once finished nothing matters |
|||
[time] (s1>=4) -> (x1'=0); |
|||
|
|||
endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// construct further stations through renaming |
|||
module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule |
|||
module station3=station1[s1=s3,x1=x3,cd1=cd3,bc1=bc3,send1=send3,busy1=busy3,end1=end3] endmodule |
|||
module station4=station1[s1=s4,x1=x4,cd1=cd4,bc1=bc4,send1=send4,busy1=busy4,end1=end4] endmodule |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
// reward structure for expected time |
|||
rewards |
|||
[time] true : 1; |
|||
endrewards |
|||
|
|||
//---------------------------------------------------------------------------------------------------------------------------- |
|||
|
|||
label "all_delivered" = s1=4&s2=4&s3=4&s4=4; |
|||
label "one_delivered" = s1=4|s2=4|s3=4|s4=4; |
|||
label "max_baxkoff_reached" = cd1=K&cd2=K&cd3=K&cd4=K; |
|||
|
|||
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 "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); |
|||
label "collisions_equal_4" = (cd1=4)|(cd2=4)|(cd3=4)|(cd4=4); |
|||
label "collisions_equal_5" = (cd1=5)|(cd2=5)|(cd3=5)|(cd4=5); |
|||
label "collisions_equal_6" = (cd1=6)|(cd2=6)|(cd3=6)|(cd4=6); |
|||
|
|||
|
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue