Browse Source
Extended DD-based model building to also build the MDP models of our benchmark suite. Added (MDP) tests for DD-based model building and explicit model building.
Extended DD-based model building to also build the MDP models of our benchmark suite. Added (MDP) tests for DD-based model building and explicit model building.
Former-commit-id: 4e18f98ee6
main
dehnert
10 years ago
10 changed files with 652 additions and 77 deletions
-
90src/builder/DdPrismModelBuilder.cpp
-
5test/functional/builder/DdPrismModelBuilderTest.cpp
-
5test/functional/builder/ExplicitPrismModelBuilderTest.cpp
-
136test/functional/builder/brp-16-2.pm
-
69test/functional/builder/crowds-5-5.pm
-
31test/functional/builder/die.pm
-
85test/functional/builder/leader-3-5.pm
-
76test/functional/builder/nand-5-2.pm
-
219test/functional/builder/wlan0-2-2.nm
-
13wlan0_collide.nm
@ -0,0 +1,136 @@ |
|||||
|
// bounded retransmission protocol [D'AJJL01] |
||||
|
// gxn/dxp 23/05/2001 |
||||
|
|
||||
|
dtmc |
||||
|
|
||||
|
// number of chunks |
||||
|
const int N = 16; |
||||
|
// maximum number of retransmissions |
||||
|
const int MAX = 2; |
||||
|
|
||||
|
module sender |
||||
|
|
||||
|
s : [0..6]; |
||||
|
// 0 idle |
||||
|
// 1 next_frame |
||||
|
// 2 wait_ack |
||||
|
// 3 retransmit |
||||
|
// 4 success |
||||
|
// 5 error |
||||
|
// 6 wait sync |
||||
|
srep : [0..3]; |
||||
|
// 0 bottom |
||||
|
// 1 not ok (nok) |
||||
|
// 2 do not know (dk) |
||||
|
// 3 ok (ok) |
||||
|
nrtr : [0..MAX]; |
||||
|
i : [0..N]; |
||||
|
bs : bool; |
||||
|
s_ab : bool; |
||||
|
fs : bool; |
||||
|
ls : bool; |
||||
|
|
||||
|
// idle |
||||
|
[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); |
||||
|
// next_frame |
||||
|
[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); |
||||
|
// wait_ack |
||||
|
[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); |
||||
|
[TO_Msg] (s=2) -> (s'=3); |
||||
|
[TO_Ack] (s=2) -> (s'=3); |
||||
|
// retransmit |
||||
|
[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); |
||||
|
[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); |
||||
|
[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); |
||||
|
// success |
||||
|
[] (s=4) & (i<N) -> (s'=1) & (i'=i+1); |
||||
|
[] (s=4) & (i=N) -> (s'=0) & (srep'=3); |
||||
|
// error |
||||
|
[SyncWait] (s=5) -> (s'=6); |
||||
|
// wait sync |
||||
|
[SyncWait] (s=6) -> (s'=0) & (s_ab'=false); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module receiver |
||||
|
|
||||
|
r : [0..5]; |
||||
|
// 0 new_file |
||||
|
// 1 fst_safe |
||||
|
// 2 frame_received |
||||
|
// 3 frame_reported |
||||
|
// 4 idle |
||||
|
// 5 resync |
||||
|
rrep : [0..4]; |
||||
|
// 0 bottom |
||||
|
// 1 fst |
||||
|
// 2 inc |
||||
|
// 3 ok |
||||
|
// 4 nok |
||||
|
fr : bool; |
||||
|
lr : bool; |
||||
|
br : bool; |
||||
|
r_ab : bool; |
||||
|
recv : bool; |
||||
|
|
||||
|
|
||||
|
// new_file |
||||
|
[SyncWait] (r=0) -> (r'=0); |
||||
|
[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); |
||||
|
// fst_safe_frame |
||||
|
[] (r=1) -> (r'=2) & (r_ab'=br); |
||||
|
// frame_received |
||||
|
[] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); |
||||
|
[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); |
||||
|
[] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); |
||||
|
[aA] (r=2) & !(r_ab=br) -> (r'=4); |
||||
|
// frame_reported |
||||
|
[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); |
||||
|
// idle |
||||
|
[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); |
||||
|
[SyncWait] (r=4) & (ls=true) -> (r'=5); |
||||
|
[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); |
||||
|
// resync |
||||
|
[SyncWait] (r=5) -> (r'=0) & (rrep'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module checker // prevents more than one frame being set |
||||
|
|
||||
|
T : bool; |
||||
|
|
||||
|
[NewFile] (T=false) -> (T'=true); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module channelK |
||||
|
|
||||
|
k : [0..2]; |
||||
|
|
||||
|
// idle |
||||
|
[aF] (k=0) -> 0.98 : (k'=1) + 0.02 : (k'=2); |
||||
|
// sending |
||||
|
[aG] (k=1) -> (k'=0); |
||||
|
// lost |
||||
|
[TO_Msg] (k=2) -> (k'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
module channelL |
||||
|
|
||||
|
l : [0..2]; |
||||
|
|
||||
|
// idle |
||||
|
[aA] (l=0) -> 0.99 : (l'=1) + 0.01 : (l'=2); |
||||
|
// sending |
||||
|
[aB] (l=1) -> (l'=0); |
||||
|
// lost |
||||
|
[TO_Ack] (l=2) -> (l'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
rewards |
||||
|
[aF] i=1 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "target" = s=5; |
||||
@ -0,0 +1,69 @@ |
|||||
|
dtmc |
||||
|
|
||||
|
// probability of forwarding |
||||
|
const double PF = 0.8; |
||||
|
const double notPF = .2; // must be 1-PF |
||||
|
// probability that a crowd member is bad |
||||
|
const double badC = .167; |
||||
|
// probability that a crowd member is good |
||||
|
const double goodC = 0.833; |
||||
|
// Total number of protocol runs to analyze |
||||
|
const int TotalRuns = 5; |
||||
|
// size of the crowd |
||||
|
const int CrowdSize = 5; |
||||
|
|
||||
|
module crowds |
||||
|
// protocol phase |
||||
|
phase: [0..4] init 0; |
||||
|
|
||||
|
// crowd member good (or bad) |
||||
|
good: bool init false; |
||||
|
|
||||
|
// number of protocol runs |
||||
|
runCount: [0..TotalRuns] init 0; |
||||
|
|
||||
|
// observe_i is the number of times the attacker observed crowd member i |
||||
|
observe0: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe1: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe2: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe3: [0..TotalRuns] init 0; |
||||
|
|
||||
|
observe4: [0..TotalRuns] init 0; |
||||
|
|
||||
|
// the last seen crowd member |
||||
|
lastSeen: [0..CrowdSize - 1] init 0; |
||||
|
|
||||
|
// get the protocol started |
||||
|
[] phase=0 & runCount<TotalRuns -> 1: (phase'=1) & (runCount'=runCount+1) & (lastSeen'=0); |
||||
|
|
||||
|
// decide whether crowd member is good or bad according to given probabilities |
||||
|
[] phase=1 -> goodC : (phase'=2) & (good'=true) + badC : (phase'=2) & (good'=false); |
||||
|
|
||||
|
// if the current member is a good member, update the last seen index (chosen uniformly) |
||||
|
[] phase=2 & good -> 1/5 : (lastSeen'=0) & (phase'=3) + 1/5 : (lastSeen'=1) & (phase'=3) + 1/5 : (lastSeen'=2) & (phase'=3) + 1/5 : (lastSeen'=3) & (phase'=3) + 1/5 : (lastSeen'=4) & (phase'=3); |
||||
|
|
||||
|
// if the current member is a bad member, record the most recently seen index |
||||
|
[] phase=2 & !good & lastSeen=0 & observe0 < TotalRuns -> 1: (observe0'=observe0+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=1 & observe1 < TotalRuns -> 1: (observe1'=observe1+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=2 & observe2 < TotalRuns -> 1: (observe2'=observe2+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=3 & observe3 < TotalRuns -> 1: (observe3'=observe3+1) & (phase'=4); |
||||
|
[] phase=2 & !good & lastSeen=4 & observe4 < TotalRuns -> 1: (observe4'=observe4+1) & (phase'=4); |
||||
|
|
||||
|
// good crowd members forward with probability PF and deliver otherwise |
||||
|
[] phase=3 -> PF : (phase'=1) + notPF : (phase'=4); |
||||
|
|
||||
|
// deliver the message and start over |
||||
|
[] phase=4 -> 1: (phase'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
label "observe0Greater1" = observe0>1; |
||||
|
label "observe1Greater1" = observe1>1; |
||||
|
label "observe2Greater1" = observe2>1; |
||||
|
label "observe3Greater1" = observe3>1; |
||||
|
label "observe4Greater1" = observe4>1; |
||||
|
label "observeIGreater1" = observe1>1|observe2>1|observe3>1|observe4>1; |
||||
|
label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1 & observe3<=1 & observe4<=1; |
||||
@ -0,0 +1,31 @@ |
|||||
|
// Knuth's model of a fair die using only fair coins |
||||
|
dtmc |
||||
|
|
||||
|
module die |
||||
|
|
||||
|
// local state |
||||
|
s : [0..7] init 0; |
||||
|
// value of the dice |
||||
|
d : [0..6] init 0; |
||||
|
|
||||
|
[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); |
||||
|
[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); |
||||
|
[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); |
||||
|
[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); |
||||
|
[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); |
||||
|
[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); |
||||
|
[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); |
||||
|
[] s=7 -> 1: (s'=7); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
rewards "coin_flips" |
||||
|
[] s<7 : 1; |
||||
|
endrewards |
||||
|
|
||||
|
label "one" = s=7&d=1; |
||||
|
label "two" = s=7&d=2; |
||||
|
label "three" = s=7&d=3; |
||||
|
label "four" = s=7&d=4; |
||||
|
label "five" = s=7&d=5; |
||||
|
label "six" = s=7&d=6; |
||||
@ -0,0 +1,85 @@ |
|||||
|
// synchronous leader election protocol (itai & Rodeh) |
||||
|
// dxp/gxn 25/01/01 |
||||
|
|
||||
|
dtmc |
||||
|
|
||||
|
// CONSTANTS |
||||
|
const int N = 3; // number of processes |
||||
|
const int K = 5; // range of probabilistic choice |
||||
|
|
||||
|
// counter module used to count the number of processes that have been read |
||||
|
// and to know when a process has decided |
||||
|
module counter |
||||
|
|
||||
|
// counter (c=i means process j reading process (i-1)+j next) |
||||
|
c : [1..N-1]; |
||||
|
|
||||
|
// reading |
||||
|
[read] c<N-1 -> 1:(c'=c+1); |
||||
|
// finished reading |
||||
|
[read] c=N-1 -> 1:(c'=c); |
||||
|
//decide |
||||
|
[done] u1|u2|u3 -> 1:(c'=c); |
||||
|
// pick again reset counter |
||||
|
[retry] !(u1|u2|u3) -> 1:(c'=1); |
||||
|
// loop (when finished to avoid deadlocks) |
||||
|
[loop] s1=3 -> 1:(c'=c); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// processes form a ring and suppose: |
||||
|
// process 1 reads process 2 |
||||
|
// process 2 reads process 3 |
||||
|
// process 3 reads process 1 |
||||
|
module process1 |
||||
|
|
||||
|
// local state |
||||
|
s1 : [0..3]; |
||||
|
// s1=0 make random choice |
||||
|
// s1=1 reading |
||||
|
// s1=2 deciding |
||||
|
// s1=3 finished |
||||
|
|
||||
|
// has a unique id so far (initially true) |
||||
|
u1 : bool; |
||||
|
|
||||
|
// value to be sent to next process in the ring (initially sets this to its own value) |
||||
|
v1 : [0..K-1]; |
||||
|
|
||||
|
// random choice |
||||
|
p1 : [0..K-1]; |
||||
|
|
||||
|
// pick value |
||||
|
[pick] s1=0 -> 1/K : (s1'=1) & (p1'=0) & (v1'=0) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=1) & (v1'=1) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=2) & (v1'=2) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) |
||||
|
+ 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true); |
||||
|
// read |
||||
|
[read] s1=1 & u1 & c<N-1 -> 1:(u1'=(p1!=v2)) & (v1'=v2); |
||||
|
[read] s1=1 & !u1 & c<N-1 -> 1:(u1'=false) & (v1'=v2) & (p1'=0); |
||||
|
// read and move to decide |
||||
|
[read] s1=1 & u1 & c=N-1 -> 1:(s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); |
||||
|
[read] s1=1 & !u1 & c=N-1 -> 1:(s1'=2) & (u1'=false) & (v1'=0); |
||||
|
// deciding |
||||
|
// done |
||||
|
[done] s1=2 -> 1:(s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); |
||||
|
//retry |
||||
|
[retry] s1=2 -> 1:(s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); |
||||
|
// loop (when finished to avoid deadlocks) |
||||
|
[loop] s1=3 -> 1:(s1'=3); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// construct remaining processes through renaming |
||||
|
module process2 = process1 [ s1=s2,p1=p2,v1=v2,u1=u2,v2=v3 ] endmodule |
||||
|
module process3 = process1 [ s1=s3,p1=p3,v1=v3,u1=u3,v2=v1 ] endmodule |
||||
|
|
||||
|
// expected number of rounds |
||||
|
rewards "num_rounds" |
||||
|
[pick] true : 1; |
||||
|
endrewards |
||||
|
|
||||
|
// labels |
||||
|
label "elected" = s1=3&s2=3&s3=3; |
||||
|
|
||||
@ -0,0 +1,76 @@ |
|||||
|
// nand multiplex system |
||||
|
// gxn/dxp 20/03/03 |
||||
|
|
||||
|
// U (correctly) performs a random permutation of the outputs of the previous stage |
||||
|
|
||||
|
dtmc |
||||
|
|
||||
|
const int N = 5; // number of inputs in each bundle |
||||
|
const int K = 2; // number of restorative stages |
||||
|
|
||||
|
const int M = 2*K+1; // total number of multiplexing units |
||||
|
|
||||
|
// parameters taken from the following paper |
||||
|
// A system architecture solution for unreliable nanoelectric devices |
||||
|
// J. Han & P. Jonker |
||||
|
// IEEEE trans. on nanotechnology vol 1(4) 2002 |
||||
|
|
||||
|
const double perr = 0.02; // probability nand works correctly |
||||
|
const double prob1 = 0.9; // probability initial inputs are stimulated |
||||
|
|
||||
|
// model whole system as a single module by resuing variables |
||||
|
// to decrease the state space |
||||
|
module multiplex |
||||
|
|
||||
|
u : [1..M]; // number of stages |
||||
|
c : [0..N]; // counter (number of copies of the nand done) |
||||
|
|
||||
|
s : [0..4]; // local state |
||||
|
// 0 - initial state |
||||
|
// 1 - set x inputs |
||||
|
// 2 - set y inputs |
||||
|
// 3 - set outputs |
||||
|
// 4 - done |
||||
|
|
||||
|
z : [0..N]; // number of new outputs equal to 1 |
||||
|
zx : [0..N]; // number of old outputs equal to 1 |
||||
|
zy : [0..N]; // need second copy for y |
||||
|
// initially 9 since initially probability of stimulated state is 0.9 |
||||
|
|
||||
|
x : [0..1]; // value of first input |
||||
|
y : [0..1]; // value of second input |
||||
|
|
||||
|
[] s=0 & (c<N) -> (s'=1); // do next nand if have not done N yet |
||||
|
[] s=0 & (c=N) & (u<M) -> (s'=1) & (zx'=z) & (zy'=z) & (z'=0) & (u'=u+1) & (c'=0); // move on to next u if not finished |
||||
|
[] s=0 & (c=N) & (u=M) -> (s'=4) & (zx'=0) & (zy'=0) & (x'=0) & (y'=0); // finished (so reset variables not needed to reduce state space) |
||||
|
|
||||
|
// choose x permute selection (have zx stimulated inputs) |
||||
|
// note only need y to be random |
||||
|
[] s=1 & u=1 -> prob1 : (x'=1) & (s'=2) + (1-prob1) : (x'=0) & (s'=2); // initially random |
||||
|
[] s=1 & u>1 & zx>0 -> (x'=1) & (s'=2) & (zx'=zx-1); |
||||
|
[] s=1 & u>1 & zx=0 -> (x'=0) & (s'=2); |
||||
|
|
||||
|
// choose x randomly from selection (have zy stimulated inputs) |
||||
|
[] s=2 & u=1 -> prob1 : (y'=1) & (s'=3) + (1-prob1) : (y'=0) & (s'=3); // initially random |
||||
|
[] s=2 & u>1 & zy<(N-c) & zy>0 -> zy/(N-c) : (y'=1) & (s'=3) & (zy'=zy-1) + 1-(zy/(N-c)) : (y'=0) & (s'=3); |
||||
|
[] s=2 & u>1 & zy=(N-c) & c<N -> 1 : (y'=1) & (s'=3) & (zy'=zy-1); |
||||
|
[] s=2 & u>1 & zy=0 -> 1 : (y'=0) & (s'=3); |
||||
|
|
||||
|
// use nand gate |
||||
|
[] s=3 & z<N & c<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty |
||||
|
+ perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault |
||||
|
// [] s=3 & z<N -> (1-perr) : (z'=z+(1-x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0) // not faulty |
||||
|
// + perr : (z'=z+(x*y)) & (s'=0) & (c'=c+1) & (x'=0) & (y'=0); // von neumann fault |
||||
|
|
||||
|
[] s=4 -> (s'=s); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// rewards: final value of gate |
||||
|
rewards |
||||
|
// [] s=0 & (c=N) & (u=M) : z/N; |
||||
|
s=0 & (c=N) & (u=M) : z/N; |
||||
|
endrewards |
||||
|
|
||||
|
label "target" = s=4 & z/N<0.1; |
||||
|
label "end" = s=4; |
||||
@ -0,0 +1,219 @@ |
|||||
|
// WLAN PROTOCOL (two stations) |
||||
|
// discrete time model |
||||
|
// gxn/jzs 20/02/02 |
||||
|
|
||||
|
mdp |
||||
|
|
||||
|
// COLLISIONS |
||||
|
const int COL = 2; // maximum number of collisions |
||||
|
|
||||
|
// TIMING CONSTRAINTS |
||||
|
// we have used the FHSS parameters |
||||
|
// then scaled by the value of ASLOTTIME |
||||
|
const int ASLOTTIME = 1; |
||||
|
const int DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice |
||||
|
const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
||||
|
const int TRANS_TIME_MAX = 2; // scaling up |
||||
|
const int TRANS_TIME_MIN = 4; // scaling down |
||||
|
const int ACK_TO = 6; |
||||
|
const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice |
||||
|
const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
||||
|
// maximum constant used in timing constraints + 1 |
||||
|
const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; |
||||
|
|
||||
|
// CONTENTION WINDOW |
||||
|
// CWMIN =15 & CWMAX =16 |
||||
|
// this means that MAX_BACKOFF IS 2 |
||||
|
const int MAX_BACKOFF = 0; |
||||
|
|
||||
|
//-----------------------------------------------------------------// |
||||
|
// THE MEDIUM/CHANNEL |
||||
|
|
||||
|
// FORMULAE FOR THE CHANNEL |
||||
|
// channel is busy |
||||
|
formula busy = c1>0 | c2>0; |
||||
|
// channel is free |
||||
|
formula free = c1=0 & c2=0; |
||||
|
|
||||
|
module medium |
||||
|
|
||||
|
// number of collisions |
||||
|
col : [0..COL]; |
||||
|
|
||||
|
// medium status |
||||
|
c1 : [0..2]; |
||||
|
c2 : [0..2]; |
||||
|
// ci corresponds to messages associated with station i |
||||
|
// 0 nothing being sent |
||||
|
// 1 being sent correctly |
||||
|
// 2 being sent garbled |
||||
|
|
||||
|
// begin sending message and nothing else currently being sent |
||||
|
[send1] c1=0 & c2=0 -> (c1'=1); |
||||
|
[send2] c2=0 & c1=0 -> (c2'=1); |
||||
|
|
||||
|
// begin sending message and something is already being sent |
||||
|
// in this case both messages become garbled |
||||
|
[send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); |
||||
|
[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); |
||||
|
|
||||
|
// finish sending message |
||||
|
[finish1] c1>0 -> (c1'=0); |
||||
|
[finish2] c2>0 -> (c2'=0); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
//-----------------------------------------------------------------// |
||||
|
// STATION 1 |
||||
|
module station1 |
||||
|
// clock for station 1 |
||||
|
x1 : [0..TIME_MAX]; |
||||
|
|
||||
|
// local state |
||||
|
s1 : [1..12]; |
||||
|
// 1 sense |
||||
|
// 2 wait until free before setting backoff |
||||
|
// 3 wait for DIFS then set slot |
||||
|
// 4 set backoff |
||||
|
// 5 backoff |
||||
|
// 6 wait until free in backoff |
||||
|
// 7 wait for DIFS then resume backoff |
||||
|
// 8 vulnerable |
||||
|
// 9 transmit |
||||
|
// 11 wait for SIFS and then ACK |
||||
|
// 10 wait for ACT_TO |
||||
|
// 12 done |
||||
|
// BACKOFF |
||||
|
// separate into slots |
||||
|
slot1 : [0..1]; |
||||
|
backoff1 : [0..15]; |
||||
|
|
||||
|
// BACKOFF COUNTER |
||||
|
bc1 : [0..1]; |
||||
|
// SENSE |
||||
|
// let time pass |
||||
|
[time] s1=1 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// ready to transmit |
||||
|
[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0); |
||||
|
// found channel busy so wait until free |
||||
|
[] s1=1 & busy -> (s1'=2) & (x1'=0); |
||||
|
// WAIT UNTIL FREE BEFORE SETTING BACKOFF |
||||
|
// let time pass (no need for the clock x1 to change) |
||||
|
[time] s1=2 & busy -> (s1'=2); |
||||
|
// find that channel is free so check its free for DIFS before setting backoff |
||||
|
[] s1=2 & free -> (s1'=3); |
||||
|
// WAIT FOR DIFS THEN SET BACKOFF |
||||
|
// let time pass |
||||
|
[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// found channel busy so wait until free |
||||
|
[] s1=3 & busy -> (s1'=2) & (x1'=0); |
||||
|
// start backoff first uniformly choose slot |
||||
|
// backoff counter 0 |
||||
|
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
||||
|
// SET BACKOFF (no time can pass) |
||||
|
// chosen slot now set backoff |
||||
|
[] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=1 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=2 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=3 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=4 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=5 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=6 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=7 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=8 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=9 ) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=10) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=11) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=12) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=13) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=14) |
||||
|
+ 1/16 : (s1'=5) & (backoff1'=15); |
||||
|
// BACKOFF |
||||
|
// let time pass |
||||
|
[time] s1=5 & x1<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// decrement backoff |
||||
|
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1); |
||||
|
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1); |
||||
|
// finish backoff |
||||
|
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0); |
||||
|
// found channel busy |
||||
|
[] s1=5 & busy -> (s1'=6) & (x1'=0); |
||||
|
// WAIT UNTIL FREE IN BACKOFF |
||||
|
// let time pass (no need for the clock x1 to change) |
||||
|
[time] s1=6 & busy -> (s1'=6); |
||||
|
// find that channel is free |
||||
|
[] s1=6 & free -> (s1'=7); |
||||
|
|
||||
|
// WAIT FOR DIFS THEN RESUME BACKOFF |
||||
|
// let time pass |
||||
|
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// resume backoff (start again from previous backoff) |
||||
|
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0); |
||||
|
// found channel busy |
||||
|
[] s1=7 & busy -> (s1'=6) & (x1'=0); |
||||
|
|
||||
|
// VULNERABLE |
||||
|
// let time pass |
||||
|
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// move to transmit |
||||
|
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0); |
||||
|
// TRANSMIT |
||||
|
// let time pass |
||||
|
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// finish transmission successful |
||||
|
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0); |
||||
|
// finish transmission garbled |
||||
|
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0); |
||||
|
// WAIT FOR SIFS THEN WAIT FOR ACK |
||||
|
|
||||
|
// WAIT FOR SIFS i.e. c1=0 |
||||
|
// check channel and busy: go into backoff |
||||
|
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2); |
||||
|
// check channel and free: let time pass |
||||
|
[time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// let time pass |
||||
|
// following guard is always false as SIFS=1 |
||||
|
// [time] s1=10 & c1=0 & x1>0 & x1<SIFS -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free) |
||||
|
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0); |
||||
|
|
||||
|
// WAIT FOR ACK i.e. c1=1 |
||||
|
// let time pass |
||||
|
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// get acknowledgement so packet sent correctly and move to done |
||||
|
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0); |
||||
|
|
||||
|
// WAIT FOR ACK_TO |
||||
|
// check channel and busy: go into backoff |
||||
|
[] s1=11 & x1=0 & busy -> (s1'=2); |
||||
|
// check channel and free: let time pass |
||||
|
[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// let time pass |
||||
|
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX)); |
||||
|
// no acknowledgement (go to backoff waiting DIFS first) |
||||
|
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0); |
||||
|
|
||||
|
// DONE |
||||
|
[time] s1=12 -> (s1'=12); |
||||
|
|
||||
|
endmodule |
||||
|
|
||||
|
// ---------------------------------------------------------------------------- // |
||||
|
// STATION 2 (rename STATION 1) |
||||
|
module |
||||
|
station2=station1[x1=x2, |
||||
|
s1=s2, |
||||
|
s2=s1, |
||||
|
c1=c2, |
||||
|
c2=c1, |
||||
|
slot1=slot2, |
||||
|
backoff1=backoff2, |
||||
|
bc1=bc2, |
||||
|
send1=send2, |
||||
|
finish1=finish2] |
||||
|
endmodule |
||||
|
// ---------------------------------------------------------------------------- // |
||||
|
|
||||
|
label "twoCollisions" = col=2; |
||||
|
label "fourCollisions" = col=4; |
||||
|
label "sixCollisions" = col=6; |
||||
@ -1,13 +0,0 @@ |
|||||
mdp |
|
||||
|
|
||||
module station1 |
|
||||
s1 : [0..12] init 0; |
|
||||
|
|
||||
// [] s1=0 -> (s1'=8) ; |
|
||||
|
|
||||
[] s1=1 -> (s1'=1); |
|
||||
[] s1=1 -> (s1'=1); |
|
||||
|
|
||||
//[] s1=8 -> (s1'=8); |
|
||||
|
|
||||
endmodule |
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue