diff --git a/prism-examples/csma/csma2_6.nm b/prism-examples/csma/csma2_6.nm deleted file mode 100644 index e98b4261..00000000 --- a/prism-examples/csma/csma2_6.nm +++ /dev/null @@ -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 (b'=2); - [send2] (b=1|b=2) & (y1 (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 (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 (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 (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); - - diff --git a/prism-examples/csma/csma3_2.nm b/prism-examples/csma/csma3_2.nm deleted file mode 100644 index b7afbef5..00000000 --- a/prism-examples/csma/csma3_2.nm +++ /dev/null @@ -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 (b'=2); - [send2] (b=1|b=2) & (y1 (b'=2); - [send3] (b=1|b=2) & (y1 (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 (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 (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 (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); - - diff --git a/prism-examples/csma/csma3_4.nm b/prism-examples/csma/csma3_4.nm deleted file mode 100644 index d489c871..00000000 --- a/prism-examples/csma/csma3_4.nm +++ /dev/null @@ -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 (b'=2); - [send2] (b=1|b=2) & (y1 (b'=2); - [send3] (b=1|b=2) & (y1 (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 (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 (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 (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); - - diff --git a/prism-examples/csma/csma3_6.nm b/prism-examples/csma/csma3_6.nm deleted file mode 100644 index 7dad29b0..00000000 --- a/prism-examples/csma/csma3_6.nm +++ /dev/null @@ -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 (b'=2); - [send2] (b=1|b=2) & (y1 (b'=2); - [send3] (b=1|b=2) & (y1 (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 (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 (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 (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); - - diff --git a/prism-examples/csma/csma4_6.nm b/prism-examples/csma/csma4_6.nm deleted file mode 100644 index 615d0756..00000000 --- a/prism-examples/csma/csma4_6.nm +++ /dev/null @@ -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 (b'=2); - [send2] (b=1|b=2) & (y1 (b'=2); - [send3] (b=1|b=2) & (y1 (b'=2); - [send4] (b=1|b=2) & (y1 (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 (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 (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 (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); - -