Browse Source
Removal of explicit/ctmdp examples (moved to qar).
Removal of explicit/ctmdp examples (moved to qar).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2141 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
15 years ago
18 changed files with 0 additions and 2043 deletions
-
9prism/examples/ctmdp/NOTES
-
3prism/examples/ctmdp/Neu10.lab
-
20prism/examples/ctmdp/Neu10.sm
-
7prism/examples/ctmdp/Neu10.tra
-
28prism/examples/ctmdp/erlang.sm
-
1prism/examples/ctmdp/jsp.csl
-
3prism/examples/ctmdp/jsp.lab
-
58prism/examples/ctmdp/jsp.sm
-
42prism/examples/ctmdp/jsp.tra
-
516prism/examples/explicit/NOTES
-
1prism/examples/explicit/wlan/backoff.pctl
-
1prism/examples/explicit/wlan/wlan.pctl
-
270prism/examples/explicit/wlan/wlan2.nm
-
281prism/examples/explicit/wlan/wlan3.nm
-
300prism/examples/explicit/wlan/wlan4.nm
-
336prism/examples/explicit/wlan/wlan5.nm
-
1prism/examples/explicit/zeroconf/zeroconf.pctl
-
166prism/examples/explicit/zeroconf/zeroconfN_M_K.nm.pp
@ -1,9 +0,0 @@ |
|||
prism examples/ctmdp/Neu10.sm -noprobchecks -exporttrans examples/ctmdp/Neu10.tra -exportlabels examples/ctmdp/Neu10.lab |
|||
|
|||
java -cp classes explicit.CTMDPModelChecker examples/ctmdp/Neu10.{tra,lab} target 1 -max |
|||
|
|||
java -cp classes explicit.CTMDPModelChecker examples/ctmdp/jsp.{tra,lab} done 10 -max |
|||
|
|||
|
|||
prism examples/ctmdp/cluster.sm -csl 'const double T; P=? [ true U<=T !"minimum" ]' -const N=4,T=1000 |
|||
prism examples/ctmdp/cluster.sm -csl 'const double T; P=? [ true U<=T !"minimum" {"crit"} ]' -const N=4,T=1000 |
|||
@ -1,3 +0,0 @@ |
|||
0="init" 1="deadlock" 2="target" |
|||
0: 0 |
|||
2: 2 |
|||
@ -1,20 +0,0 @@ |
|||
// Simple CTMP from Neuhausser thesis defence slides (2010) |
|||
|
|||
// For max prob of reaching target within time bound 1, |
|||
// exact answer is 1 + 19/24 e^-3 - 3/2 e^-1 = (approx.) 0.48759 |
|||
// discretisation (k = 4500, tau = 0.0002222...) gives 0.487552953296395 |
|||
|
|||
mdp |
|||
|
|||
module M |
|||
|
|||
s : [0..3]; |
|||
|
|||
[a] s=0 -> 1 : (s'=2) + 2 : (s'=3); |
|||
[b] s=0 -> 3 : (s'=1); |
|||
[b] s=1 -> 1 : (s'=2); |
|||
[c] s>1 -> 1 : true; |
|||
|
|||
endmodule |
|||
|
|||
label "target" = s=2; |
|||
@ -1,7 +0,0 @@ |
|||
4 5 6 |
|||
0 0 1 3 b |
|||
0 1 2 1 a |
|||
0 1 3 2 a |
|||
1 0 2 1 b |
|||
2 0 2 1 c |
|||
3 0 3 1 c |
|||
@ -1,28 +0,0 @@ |
|||
imc |
|||
|
|||
const int k; |
|||
const double mean = 10; |
|||
|
|||
module erlang |
|||
|
|||
s : [0..5]; |
|||
i : [1..k+1]; |
|||
|
|||
[] s=0 -> 1 : (s'=1); |
|||
[a] s=1 -> 1 : (s'=1); |
|||
[] i < k -> k/mean : (i'=i+1); |
|||
[go] i = k -> k/mean : (i'=i+1); |
|||
|
|||
endmodule |
|||
|
|||
module main |
|||
|
|||
x : [0..1]; |
|||
|
|||
[go] x=0 -> (x'=1); |
|||
|
|||
endmodule |
|||
|
|||
rewards "time" |
|||
true : 1; |
|||
endrewards |
|||
@ -1 +0,0 @@ |
|||
"done" |
|||
@ -1,3 +0,0 @@ |
|||
0="init" 1="deadlock" 2="done" |
|||
0: 0 |
|||
14: 2 |
|||
@ -1,58 +0,0 @@ |
|||
mdp |
|||
|
|||
const double lambda1 = 0.25; |
|||
const double lambda2 = 0.33; |
|||
const double lambda3 = 1.25; |
|||
const double lambda4 = 1.50; |
|||
|
|||
formula todo = (job1<2?1:0) + (job2<2?1:0) + (job3<2?1:0) + (job4<2?1:0); |
|||
|
|||
module jsp |
|||
|
|||
job1 : [0..2] init 1; |
|||
job2 : [0..2] init 0; |
|||
job3 : [0..2] init 1; |
|||
job4 : [0..2] init 0; |
|||
|
|||
// 1&3 initially scheduled |
|||
// a_ij_kl: when i (k) finishes, schedule j (l) |
|||
[a_12_32] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job2'=1) + lambda3 : (job3'=2)&(job2'=1); |
|||
[a_12_34] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job2'=1) + lambda3 : (job3'=2)&(job4'=1); |
|||
[a_14_32] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job4'=1) + lambda3 : (job3'=2)&(job2'=1); |
|||
[a_14_34] todo=4 & job1=1 & job3=1 -> lambda1 : (job1'=2)&(job4'=1) + lambda3 : (job3'=2)&(job4'=1); |
|||
|
|||
// 1&2 scheduled (3 done, 4 next) |
|||
[step2] todo=3 & job1=1 & job2=1 -> lambda1 : (job1'=2)&(job4'=1) + lambda2 : (job2'=2)&(job4'=1); |
|||
// 1&4 scheduled (3 done, 2 next) |
|||
[step2] todo=3 & job1=1 & job4=1 -> lambda1 : (job1'=2)&(job2'=1) + lambda4 : (job4'=2)&(job2'=1); |
|||
// 3&2 scheduled (1 done, 4 next) |
|||
[step2] todo=3 & job3=1 & job2=1 -> lambda3 : (job3'=2)&(job4'=1) + lambda2 : (job2'=2)&(job4'=1); |
|||
// 3&4 scheduled (1 done, 2 next) |
|||
[step2] todo=3 & job3=1 & job4=1 -> lambda3 : (job3'=2)&(job2'=1) + lambda4 : (job4'=2)&(job2'=1); |
|||
|
|||
// two scheduled |
|||
[step3] todo=2 & job1=1 & job2=1 -> lambda1 : (job1'=2) + lambda2 : (job2'=2); |
|||
[step3] todo=2 & job1=1 & job3=1 -> lambda1 : (job1'=2) + lambda3 : (job3'=2); |
|||
[step3] todo=2 & job1=1 & job4=1 -> lambda1 : (job1'=2) + lambda4 : (job4'=2); |
|||
[step3] todo=2 & job2=1 & job1=1 -> lambda2 : (job2'=2) + lambda1 : (job1'=2); |
|||
[step3] todo=2 & job2=1 & job3=1 -> lambda2 : (job2'=2) + lambda3 : (job3'=2); |
|||
[step3] todo=2 & job2=1 & job4=1 -> lambda2 : (job2'=2) + lambda4 : (job4'=2); |
|||
[step3] todo=2 & job3=1 & job1=1 -> lambda3 : (job3'=2) + lambda1 : (job1'=2); |
|||
[step3] todo=2 & job3=1 & job2=1 -> lambda3 : (job3'=2) + lambda2 : (job2'=2); |
|||
[step3] todo=2 & job3=1 & job4=1 -> lambda3 : (job3'=2) + lambda4 : (job4'=2); |
|||
[step3] todo=2 & job4=1 & job1=1 -> lambda4 : (job4'=2) + lambda1 : (job1'=2); |
|||
[step3] todo=2 & job4=1 & job2=1 -> lambda4 : (job4'=2) + lambda2 : (job2'=2); |
|||
[step3] todo=2 & job4=1 & job3=1 -> lambda4 : (job4'=2) + lambda3 : (job3'=2); |
|||
|
|||
// one scheduled |
|||
[step4] todo=1 & job1=1 -> lambda1 : (job1'=2); |
|||
[step4] todo=1 & job2=1 -> lambda1 : (job2'=2); |
|||
[step4] todo=1 & job3=1 -> lambda1 : (job3'=2); |
|||
[step4] todo=1 & job4=1 -> lambda1 : (job4'=2); |
|||
|
|||
// done |
|||
[done] todo=0 -> true; |
|||
|
|||
endmodule |
|||
|
|||
label "done" = todo=0; |
|||
@ -1,42 +0,0 @@ |
|||
15 23 41 |
|||
0 0 1 1.25 a_14_34 |
|||
0 0 6 0.25 a_14_34 |
|||
0 1 2 1.25 a_14_32 |
|||
0 1 6 0.25 a_14_32 |
|||
0 2 1 1.25 a_12_34 |
|||
0 2 7 0.25 a_12_34 |
|||
0 3 2 1.25 a_12_32 |
|||
0 3 7 0.25 a_12_32 |
|||
1 0 3 1.5 step2 |
|||
1 0 9 0.25 step2 |
|||
2 0 4 0.33 step2 |
|||
2 0 9 0.25 step2 |
|||
3 0 5 0.33 step3 |
|||
3 0 10 0.25 step3 |
|||
3 1 5 0.33 step3 |
|||
3 1 10 0.25 step3 |
|||
4 0 5 1.5 step3 |
|||
4 0 13 0.25 step3 |
|||
4 1 5 1.5 step3 |
|||
4 1 13 0.25 step3 |
|||
5 0 14 0.25 step4 |
|||
6 0 8 1.5 step2 |
|||
6 0 9 1.25 step2 |
|||
7 0 9 1.25 step2 |
|||
7 0 11 0.33 step2 |
|||
8 0 10 1.25 step3 |
|||
8 0 12 0.33 step3 |
|||
8 1 10 1.25 step3 |
|||
8 1 12 0.33 step3 |
|||
9 0 10 1.5 step3 |
|||
9 0 13 0.33 step3 |
|||
9 1 10 1.5 step3 |
|||
9 1 13 0.33 step3 |
|||
10 0 14 0.25 step4 |
|||
11 0 12 1.5 step3 |
|||
11 0 13 1.25 step3 |
|||
11 1 12 1.5 step3 |
|||
11 1 13 1.25 step3 |
|||
12 0 14 0.25 step4 |
|||
13 0 14 0.25 step4 |
|||
14 0 14 1 done |
|||
@ -1,516 +0,0 @@ |
|||
some notes/conclusions |
|||
|
|||
- precomputation can slow things down (because we can't re-use comp?) |
|||
but can also slow down num comp a lot too - e.g. zeroconf has states that converge v. slowly to 1 |
|||
|
|||
- |
|||
|
|||
#================================================ |
|||
# Simple tests |
|||
#================================================ |
|||
|
|||
prism-ar simple/fmsd-ex4 target -opt -v=10 |
|||
|
|||
#================================================ |
|||
# Zeroconf (untimed) (MDP) |
|||
#================================================ |
|||
|
|||
# Generate model files |
|||
for N in 4 8; do for M in 32 64 128; do |
|||
prismpp zeroconf/zeroconfN_M_K.nm.pp "$N" "$M" 4 >| zeroconf/zeroconf"$N"_"$M"_4.nm |
|||
prism zeroconf/zeroconf"$N"_"$M"_4.nm -exporttrans zeroconf/zeroconf"$N"_"$M"_4.tra -exportlabels zeroconf/zeroconf"$N"_"$M"_4.lab |
|||
done; done |
|||
|
|||
# Model check in PRISM |
|||
for N in 4 8; do for M in 32 64 128; do |
|||
prism zeroconf/zeroconf$N$_$M$_4.nm zeroconf/zeroconf.pctl |
|||
done; done |
|||
|
|||
export PRISM_JAVAMAXMEM=2000m |
|||
# Abstraction refinement |
|||
export N=4 M=32 |
|||
for N in 4 8; do for M in 32 64 128; do |
|||
prism-ar zeroconf/zeroconf"$N"_"$M"_4 done_correct -refine=all |
|||
done; done |
|||
|
|||
#================================================ |
|||
# WLAN (MDP) |
|||
#================================================ |
|||
|
|||
# Generate model files |
|||
prism wlan/wlan2.nm -const TRANS_TIME_MAX=10 -fixdl -exporttrans wlan/wlan2_10.tra -exportlabels wlan/wlan2_10.lab |
|||
prism wlan/wlan3.nm -const TRANS_TIME_MAX=10 -fixdl -exporttrans wlan/wlan3_10.tra -exportlabels wlan/wlan3_10.lab |
|||
prism wlan/wlan4.nm -const TRANS_TIME_MAX=10 -fixdl -exporttrans wlan/wlan4_10.tra -exportlabels wlan/wlan4_10.lab |
|||
prism wlan/wlan5.nm -const TRANS_TIME_MAX=10 -fixdl -exporttrans wlan/wlan5_10.tra -exportlabels wlan/wlan5_10.lab |
|||
# Other value for TRANS_TIME_MAX is 316 |
|||
|
|||
# Model check in PRISM |
|||
prism wlan/wlan2.nm wlan/backoff.pctl -const TRANS_TIME_MAX=10 -m >! wlan/wlan2_10.-1.exactm.log |
|||
prism wlan/wlan3.nm wlan/backoff.pctl -const TRANS_TIME_MAX=10 -m >! wlan/wlan3_10.-1.exactm.log |
|||
prism wlan/wlan4.nm wlan/backoff.pctl -const TRANS_TIME_MAX=10 -m >! wlan/wlan4_10.-1.exactm.log |
|||
prism wlan/wlan5.nm wlan/backoff.pctl -const TRANS_TIME_MAX=10 -m >! wlan/wlan5_10.-1.-exactm.log |
|||
|
|||
# Abstraction refinement |
|||
prism-ar wlan/wlan2_10 bcmax -nopre -opt -refine=all |
|||
prism-ar wlan/wlan3_10 bcmax -nopre -opt -refine=all |
|||
prism-ar wlan/wlan4_10 bcmax -nopre -opt -refine=all |
|||
prism-ar wlan/wlan5_10 bcmax -nopre -opt -refine=all |
|||
|
|||
#================================================ |
|||
# Self-stabilisation (Israeli-Jalfon) (MDP) |
|||
#================================================ |
|||
|
|||
# Generate model files |
|||
foreach N (3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20) |
|||
prism israeli-jalfon/ij$N.nm -exporttrans israeli-jalfon/ij$N.tra -exportlabels israeli-jalfon/ij$N.lab |
|||
end |
|||
|
|||
# Model check in PRISM |
|||
foreach N (3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20) |
|||
prism israeli-jalfon/ij$N.nm israeli-jalfon/ij$N.pctl -prop 2 -const k=40:20:80 >! israeli-jalfon/ij$N.-2.exact.log |
|||
end |
|||
|
|||
# Abstraction refinement |
|||
#bin/prism-ar israeli-jalfon/ij5.tra israeli-jalfon/ij5.lab stable |
|||
prism-ar israeli-jalfon/ij5.tra israeli-jalfon/ij5.lab stable -nopre -opt |
|||
|
|||
#================================================ |
|||
# Self-stabilisation (Herman) (DTMC) |
|||
#================================================ |
|||
|
|||
# Generate model files |
|||
export N=3 k=5 |
|||
for N in 3 5 7 9 11 13 15 17 19; do |
|||
prism herman/herman"$N".pm -exporttrans herman/herman$N.tra -exportlabels herman/herman$N.lab |
|||
done; done |
|||
|
|||
# Model check in PRISM |
|||
for N in 3 5 7 9 11 13 15 17 19; do |
|||
# time-bounded |
|||
prism herman/herman$N.pm -pctl 'const int k; P=?[F<=k "stable"]' -const k=5 |
|||
done; done |
|||
|
|||
# Abstraction refinement |
|||
export N=3 k=5 |
|||
for N in 3 5 7 9 11 13 15 17 19; do |
|||
prism-ar herman/herman"$N" stable -dtmc -probreachbnd="$k" -nopre -noopt |
|||
done; done |
|||
|
|||
|
|||
#================================================ |
|||
# Polling |
|||
#================================================ |
|||
|
|||
prism polling/poll2.sm -csl 'P=?[F "last_polled"]' |
|||
prism polling/poll5.sm -csl 'P=?[F "last_polled"]' |
|||
|
|||
prism polling/poll2.sm -fixdl -exporttrans polling/poll2.tra -exportstates polling/poll2.sta -exportlabels polling/poll2.lab |
|||
prism polling/poll5.sm -fixdl -exporttrans polling/poll5.tra -exportstates polling/poll5.sta -exportlabels polling/poll5.lab |
|||
|
|||
prism-ar polling/poll2 last_polled -ctmc -noopt |
|||
prism-ar polling/poll5 last_polled -ctmc -noopt |
|||
|
|||
prism-ar polling/poll2 last_polled -ctmc -noopt -exactcheck |
|||
|
|||
-ctmc -probreachbnd=1 |
|||
|
|||
#================================================ |
|||
# FGF |
|||
#================================================ |
|||
|
|||
prism fgf/sprouty.sm fgf/deg.ss.csl -s -bgs -epsilon 1e-12 -maxiters 10000000 -fixdl |
|||
|
|||
prism fgf/sprouty.sm -fixdl -exporttrans fgf/sprouty.tra -exportstates fgf/sprouty.sta -exportlabels fgf/sprouty.lab |
|||
|
|||
PRISM_JAVAMAXMEM=2000m prism-ar fgf/sprouty cause1 -ctmc -nopre -noopt |
|||
|
|||
PRISM_JAVAMAXMEM=2000m prism-ar -Xmx2000m fgf/sprouty cause1 -ctmc -noopt -refine=all -epsilon=1e-2 |
|||
|
|||
#================================================ |
|||
# Self-stabilisation (Beauquier) |
|||
#================================================ |
|||
|
|||
# Generate model files |
|||
foreach N (3 5 7 9 11) |
|||
prism beauquier/beauquier$N.nm -exporttrans beauquier/beauquier$N.tra -exportstates beauquier/beauquier$N.sta |
|||
end |
|||
|
|||
# Model check in PRISM |
|||
foreach N (3 5 7 9 11) |
|||
prism beauquier/beauquier$N.nm beauquier/beauquier$N.pctl -m >! beauquier/beauquier$N.-2.exactm.log |
|||
end |
|||
foreach N (3 5 7 9 11) |
|||
prism beauquier/beauquier$N.nm beauquier/beauquier$N.pctl -s >! beauquier/beauquier$N.-2.exacts.log |
|||
end |
|||
|
|||
# Abstraction refinement (value-based) |
|||
foreach N (3 5 7 9) |
|||
java AbstractBeauquierInitial $N,beauquier/beauquier$N -2 21 >! beauquier/beauquier$N.-2.21.log |
|||
end |
|||
java -Xmx1500m AbstractBeauquierInitial 11,beauquier/beauquier11 -2 21 >! beauquier/beauquier11.-2.21.log |
|||
|
|||
# Abstraction refinement (strategy-based) |
|||
foreach N (3 5 7 9) |
|||
java AbstractBeauquierInitial $N,beauquier/beauquier$N -2 20 >! beauquier/beauquier$N.-2.20.log |
|||
end |
|||
java -Xmx1500m AbstractBeauquierInitial 11,beauquier/beauquier11 -2 20 >! beauquier/beauquier11.-2.20.log |
|||
|
|||
|
|||
#================================================ |
|||
# Zeroconf - Until |
|||
#================================================ |
|||
|
|||
# Generate PRISM files |
|||
prismpp zeroconf-until/zeroconfN_M_K.nm.pp 4 32 4 > ! zeroconf-until/zeroconf4_32_4.nm |
|||
prismpp zeroconf-until/zeroconfN_M_K.nm.pp 4 64 4 > ! zeroconf-until/zeroconf4_64_4.nm |
|||
prismpp zeroconf-until/zeroconfN_M_K.nm.pp 4 128 4 > ! zeroconf-until/zeroconf4_128_4.nm |
|||
prismpp zeroconf-until/zeroconfN_M_K.nm.pp 6 32 4 > ! zeroconf-until/zeroconf6_32_4.nm |
|||
prismpp zeroconf-until/zeroconfN_M_K.nm.pp 6 64 4 > ! zeroconf-until/zeroconf6_64_4.nm |
|||
prismpp zeroconf-until/zeroconfN_M_K.nm.pp 6 128 4 > ! zeroconf-until/zeroconf6_128_4.nm |
|||
prismpp zeroconf-until/zeroconfN_M_K.nm.pp 8 32 4 > ! zeroconf-until/zeroconf8_32_4.nm |
|||
prismpp zeroconf-until/zeroconfN_M_K.nm.pp 8 64 4 > ! zeroconf-until/zeroconf8_64_4.nm |
|||
prismpp zeroconf-until/zeroconfN_M_K.nm.pp 8 128 4 > ! zeroconf-until/zeroconf8_128_4.nm |
|||
|
|||
# Generate model files |
|||
prism zeroconf-until/zeroconf4_32_4.nm -exporttrans zeroconf-until/zeroconf4_32_4.tra -exportstates zeroconf-until/zeroconf4_32_4.sta |
|||
prism zeroconf-until/zeroconf4_64_4.nm -exporttrans zeroconf-until/zeroconf4_64_4.tra -exportstates zeroconf-until/zeroconf4_64_4.sta |
|||
prism zeroconf-until/zeroconf4_128_4.nm -exporttrans zeroconf-until/zeroconf4_128_4.tra -exportstates zeroconf-until/zeroconf4_128_4.sta |
|||
prism zeroconf-until/zeroconf6_32_4.nm -exporttrans zeroconf-until/zeroconf6_32_4.tra -exportstates zeroconf-until/zeroconf6_32_4.sta |
|||
prism zeroconf-until/zeroconf6_64_4.nm -exporttrans zeroconf-until/zeroconf6_64_4.tra -exportstates zeroconf-until/zeroconf6_64_4.sta |
|||
prism zeroconf-until/zeroconf6_128_4.nm -exporttrans zeroconf-until/zeroconf6_128_4.tra -exportstates zeroconf-until/zeroconf6_128_4.sta |
|||
prism zeroconf-until/zeroconf8_32_4.nm -exporttrans zeroconf-until/zeroconf8_32_4.tra -exportstates zeroconf-until/zeroconf8_32_4.sta |
|||
prism zeroconf-until/zeroconf8_64_4.nm -exporttrans zeroconf-until/zeroconf8_64_4.tra -exportstates zeroconf-until/zeroconf8_64_4.sta |
|||
prism zeroconf-until/zeroconf8_128_4.nm -exporttrans zeroconf-until/zeroconf8_128_4.tra -exportstates zeroconf-until/zeroconf8_128_4.sta |
|||
|
|||
# Abstraction refinement (value-based, opt) |
|||
java AbstractZeroconfInitial 4,32,4,zeroconf-until/zeroconf4_32_4,until -1 21 -opt >! zeroconf-until/zeroconf4_32.21.opt.log |
|||
java AbstractZeroconfInitial 4,64,4,zeroconf-until/zeroconf4_64_4,until -1 21 -opt >! zeroconf-until/zeroconf4_64.21.opt.log |
|||
java AbstractZeroconfInitial 4,128,4,zeroconf-until/zeroconf4_128_4,until -1 21 -opt >! zeroconf-until/zeroconf4_128.21.opt.log |
|||
java AbstractZeroconfInitial 6,32,4,zeroconf-until/zeroconf6_32_4,until -1 21 -opt >! zeroconf-until/zeroconf6_32.21.opt.log |
|||
java AbstractZeroconfInitial 6,64,4,zeroconf-until/zeroconf6_64_4,until -1 21 -opt >! zeroconf-until/zeroconf6_64.21.opt.log |
|||
java AbstractZeroconfInitial 6,128,4,zeroconf-until/zeroconf6_128_4,until -1 21 -opt >! zeroconf-until/zeroconf6_128.21.opt.log |
|||
java AbstractZeroconfInitial 8,32,4,zeroconf-until/zeroconf8_32_4,until -1 21 -opt >! zeroconf-until/zeroconf8_32.21.opt.log |
|||
java AbstractZeroconfInitial 8,64,4,zeroconf-until/zeroconf8_64_4,until -1 21 -opt >! zeroconf-until/zeroconf8_64.21.opt.log |
|||
java AbstractZeroconfInitial 8,128,4,zeroconf-until/zeroconf8_128_4,until -1 21 -opt >! zeroconf-until/zeroconf8_128.21.opt.log |
|||
|
|||
# Abstraction refinement (value-based, noopt) |
|||
java AbstractZeroconfInitial 4,32,4,zeroconf-until/zeroconf4_32_4,until -1 21 -noopt >! zeroconf-until/zeroconf4_32.21.noopt.log |
|||
java AbstractZeroconfInitial 4,64,4,zeroconf-until/zeroconf4_64_4,until -1 21 -noopt >! zeroconf-until/zeroconf4_64.21.noopt.log |
|||
java AbstractZeroconfInitial 4,128,4,zeroconf-until/zeroconf4_128_4,until -1 21 -noopt >! zeroconf-until/zeroconf4_128.21.noopt.log |
|||
java AbstractZeroconfInitial 6,32,4,zeroconf-until/zeroconf6_32_4,until -1 21 -noopt >! zeroconf-until/zeroconf6_32.21.noopt.log |
|||
java AbstractZeroconfInitial 6,64,4,zeroconf-until/zeroconf6_64_4,until -1 21 -noopt >! zeroconf-until/zeroconf6_64.21.noopt.log |
|||
java AbstractZeroconfInitial 6,128,4,zeroconf-until/zeroconf6_128_4,until -1 21 -noopt >! zeroconf-until/zeroconf6_128.21.noopt.log |
|||
java AbstractZeroconfInitial 8,32,4,zeroconf-until/zeroconf8_32_4,until -1 21 -noopt >! zeroconf-until/zeroconf8_32.21.noopt.log |
|||
java AbstractZeroconfInitial 8,64,4,zeroconf-until/zeroconf8_64_4,until -1 21 -noopt >! zeroconf-until/zeroconf8_64.21.noopt.log |
|||
java AbstractZeroconfInitial 8,128,4,zeroconf-until/zeroconf8_128_4,until -1 21 -noopt >! zeroconf-until/zeroconf8_128.21.noopt.log |
|||
|
|||
# Abstraction refinement (strategy-based, opt) |
|||
java AbstractZeroconfInitial 4,32,4,zeroconf-until/zeroconf4_32_4,until -1 20 -opt >! zeroconf-until/zeroconf4_32.20.opt.log |
|||
java AbstractZeroconfInitial 4,64,4,zeroconf-until/zeroconf4_64_4,until -1 20 -opt >! zeroconf-until/zeroconf4_64.20.opt.log |
|||
java AbstractZeroconfInitial 4,128,4,zeroconf-until/zeroconf4_128_4,until -1 20 -opt >! zeroconf-until/zeroconf4_128.20.opt.log |
|||
java AbstractZeroconfInitial 6,32,4,zeroconf-until/zeroconf6_32_4,until -1 20 -opt >! zeroconf-until/zeroconf6_32.20.opt.log |
|||
java AbstractZeroconfInitial 6,64,4,zeroconf-until/zeroconf6_64_4,until -1 20 -opt >! zeroconf-until/zeroconf6_64.20.opt.log |
|||
java AbstractZeroconfInitial 6,128,4,zeroconf-until/zeroconf6_128_4,until -1 20 -opt >! zeroconf-until/zeroconf6_128.20.opt.log |
|||
java AbstractZeroconfInitial 8,32,4,zeroconf-until/zeroconf8_32_4,until -1 20 -opt >! zeroconf-until/zeroconf8_32.20.opt.log |
|||
java AbstractZeroconfInitial 8,64,4,zeroconf-until/zeroconf8_64_4,until -1 20 -opt >! zeroconf-until/zeroconf8_64.20.opt.log |
|||
java AbstractZeroconfInitial 8,128,4,zeroconf-until/zeroconf8_128_4,until -1 20 -opt >! zeroconf-until/zeroconf8_128.20.opt.log |
|||
|
|||
# Abstraction refinement (strategy-based, noopt) |
|||
java AbstractZeroconfInitial 4,32,4,zeroconf-until/zeroconf4_32_4,until -1 20 -noopt >! zeroconf-until/zeroconf4_32.20.noopt.log |
|||
java AbstractZeroconfInitial 4,64,4,zeroconf-until/zeroconf4_64_4,until -1 20 -noopt >! zeroconf-until/zeroconf4_64.20.noopt.log |
|||
java AbstractZeroconfInitial 4,128,4,zeroconf-until/zeroconf4_128_4,until -1 20 -noopt >! zeroconf-until/zeroconf4_128.20.noopt.log |
|||
java AbstractZeroconfInitial 6,32,4,zeroconf-until/zeroconf6_32_4,until -1 20 -noopt >! zeroconf-until/zeroconf6_32.20.noopt.log |
|||
java AbstractZeroconfInitial 6,64,4,zeroconf-until/zeroconf6_64_4,until -1 20 -noopt >! zeroconf-until/zeroconf6_64.20.noopt.log |
|||
java AbstractZeroconfInitial 6,128,4,zeroconf-until/zeroconf6_128_4,until -1 20 -noopt >! zeroconf-until/zeroconf6_128.20.noopt.log |
|||
java AbstractZeroconfInitial 8,32,4,zeroconf-until/zeroconf8_32_4,until -1 20 -noopt >! zeroconf-until/zeroconf8_32.20.noopt.log |
|||
java AbstractZeroconfInitial 8,64,4,zeroconf-until/zeroconf8_64_4,until -1 20 -noopt >! zeroconf-until/zeroconf8_64.20.noopt.log |
|||
java AbstractZeroconfInitial 8,128,4,zeroconf-until/zeroconf8_128_4,until -1 20 -noopt >! zeroconf-until/zeroconf8_128.20.noopt.log |
|||
|
|||
- to run when i get home (then delete so notes file is correct) |
|||
|
|||
java AbstractZeroconfInitial 4,128,4,zeroconf/until/zeroconf4_128_4,until -1 21 -opt >! zeroconf/until/zeroconf4_128.21.opt.log |
|||
java AbstractZeroconfInitial 4,32,4,zeroconf/until/zeroconf4_32_4,until -1 21 -noopt >! zeroconf/until/zeroconf4_32.21.noopt.log |
|||
java AbstractZeroconfInitial 4,64,4,zeroconf/until/zeroconf4_64_4,until -1 21 -noopt >! zeroconf/until/zeroconf4_64.21.noopt.log |
|||
java AbstractZeroconfInitial 4,128,4,zeroconf/until/zeroconf4_128_4,until -1 21 -noopt >! zeroconf/until/zeroconf4_128.21.noopt.log |
|||
java AbstractZeroconfInitial 6,32,4,zeroconf/until/zeroconf6_32_4,until -1 21 -opt >! zeroconf/until/zeroconf6_32.21.opt.log |
|||
java AbstractZeroconfInitial 6,64,4,zeroconf/until/zeroconf6_64_4,until -1 21 -opt >! zeroconf/until/zeroconf6_64.21.opt.log |
|||
java AbstractZeroconfInitial 6,128,4,zeroconf/until/zeroconf6_128_4,until -1 21 -opt >! zeroconf/until/zeroconf6_128.21.opt.log |
|||
java AbstractZeroconfInitial 6,32,4,zeroconf/until/zeroconf6_32_4,until -1 21 -noopt >! zeroconf/until/zeroconf6_32.21.noopt.log |
|||
java AbstractZeroconfInitial 6,64,4,zeroconf/until/zeroconf6_64_4,until -1 21 -noopt >! zeroconf/until/zeroconf6_64.21.noopt.log |
|||
java AbstractZeroconfInitial 6,128,4,zeroconf/until/zeroconf6_128_4,until -1 21 -noopt >! zeroconf/until/zeroconf6_128.21.noopt.log |
|||
java AbstractZeroconfInitial 6,32,4,zeroconf/until/zeroconf6_32_4,until -1 20 -opt >! zeroconf/until/zeroconf6_32.20.opt.log |
|||
java AbstractZeroconfInitial 6,64,4,zeroconf/until/zeroconf6_64_4,until -1 20 -opt >! zeroconf/until/zeroconf6_64.20.opt.log |
|||
java AbstractZeroconfInitial 6,128,4,zeroconf/until/zeroconf6_128_4,until -1 20 -opt >! zeroconf/until/zeroconf6_128.20.opt.log |
|||
java AbstractZeroconfInitial 6,32,4,zeroconf/until/zeroconf6_32_4,until -1 20 -noopt >! zeroconf/until/zeroconf6_32.20.noopt.log |
|||
java AbstractZeroconfInitial 6,64,4,zeroconf/until/zeroconf6_64_4,until -1 20 -noopt >! zeroconf/until/zeroconf6_64.20.noopt.log |
|||
java AbstractZeroconfInitial 6,128,4,zeroconf/until/zeroconf6_128_4,until -1 20 -noopt >! zeroconf/until/zeroconf6_128.20.noopt.log |
|||
java AbstractZeroconfInitial 8,32,4,zeroconf/until/zeroconf8_32_4,until -1 21 -opt >! zeroconf/until/zeroconf8_32.21.opt.log |
|||
java AbstractZeroconfInitial 8,64,4,zeroconf/until/zeroconf8_64_4,until -1 21 -opt >! zeroconf/until/zeroconf8_64.21.opt.log |
|||
java AbstractZeroconfInitial 8,128,4,zeroconf/until/zeroconf8_128_4,until -1 21 -opt >! zeroconf/until/zeroconf8_128.21.opt.log |
|||
java AbstractZeroconfInitial 8,32,4,zeroconf/until/zeroconf8_32_4,until -1 21 -noopt >! zeroconf/until/zeroconf8_32.21.noopt.log |
|||
java AbstractZeroconfInitial 8,64,4,zeroconf/until/zeroconf8_64_4,until -1 21 -noopt >! zeroconf/until/zeroconf8_64.21.noopt.log |
|||
java AbstractZeroconfInitial 8,128,4,zeroconf/until/zeroconf8_128_4,until -1 21 -noopt >! zeroconf/until/zeroconf8_128.21.noopt.log |
|||
java AbstractZeroconfInitial 8,32,4,zeroconf/until/zeroconf8_32_4,until -1 20 -opt >! zeroconf/until/zeroconf8_32.20.opt.log |
|||
java AbstractZeroconfInitial 8,64,4,zeroconf/until/zeroconf8_64_4,until -1 20 -opt >! zeroconf/until/zeroconf8_64.20.opt.log |
|||
java AbstractZeroconfInitial 8,128,4,zeroconf/until/zeroconf8_128_4,until -1 20 -opt >! zeroconf/until/zeroconf8_128.20.opt.log |
|||
java AbstractZeroconfInitial 8,32,4,zeroconf/until/zeroconf8_32_4,until -1 20 -noopt >! zeroconf/until/zeroconf8_32.20.noopt.log |
|||
java AbstractZeroconfInitial 8,64,4,zeroconf/until/zeroconf8_64_4,until -1 20 -noopt >! zeroconf/until/zeroconf8_64.20.noopt.log |
|||
java AbstractZeroconfInitial 8,128,4,zeroconf/until/zeroconf8_128_4,until -1 20 -noopt >! zeroconf/until/zeroconf8_128.20.noopt.log |
|||
|
|||
#================================================ |
|||
# Zeroconf - Bounded until |
|||
#================================================ |
|||
|
|||
prism zeroconf-bounded_until/zeroconf2_time.nm -const K=4,T=60 -exporttrans zeroconf-bounded_until/zeroconf2_60.tra -exportstates zeroconf-bounded_until/zeroconf2_60.sta |
|||
|
|||
java AbstractZeroconf 2,4,2,zeroconf-bounded_until/zeroconf2_60,buntil -1 |
|||
java AbstractZeroconf 2,4,2,zeroconf-bounded_until/zeroconf2_60,buntil -1 21 |
|||
java AbstractZeroconfInitial 2,4,2,zeroconf-bounded_until/zeroconf2_60,buntil -1 21 |
|||
|
|||
foreach T (60 80) |
|||
prism zeroconf-bounded_until/zeroconf4.nm -const K=4,T=$T -exporttrans zeroconf-bounded_until/zeroconf4_$T.tra -exportstates zeroconf-bounded_until/zeroconf4_$T.sta |
|||
prism zeroconf-bounded_until/zeroconf8.nm -const K=4,T=$T -exporttrans zeroconf-bounded_until/zeroconf8_$T.tra -exportstates zeroconf-bounded_until/zeroconf8_$T.sta |
|||
end |
|||
|
|||
foreach T (60 80) |
|||
java AbstractZeroconfInitial 4,32,4,zeroconf-bounded_until/zeroconf4_$T,buntil,$T -1 21 |
|||
end |
|||
|
|||
java AbstractZeroconf 4,32,4,zeroconf-bounded_until/zeroconf4_80,buntil -1 |
|||
|
|||
exact results for N=4 (min) |
|||
60 0.0 |
|||
65 0.0 |
|||
70 0.0 |
|||
75 0.0 |
|||
80 0.875 |
|||
85 0.875 |
|||
90 0.875 |
|||
95 0.9264677734375 |
|||
100 0.9745415039062499 |
|||
105 0.9745415039062499 |
|||
110 0.9745415039062499 |
|||
115 0.9745415039062499 |
|||
120 0.9745415039062499 |
|||
|
|||
#================================================ |
|||
# Leader election |
|||
#================================================ |
|||
|
|||
foreach N (3 4 5 6 7) |
|||
prism leader-async/leader$N.nm -exportstates leader-async/leader$N.sta -exporttrans leader-async/leader$N.tra |
|||
end |
|||
|
|||
|
|||
foreach N (3 4 5 6 7) |
|||
prism leader-async/leader$N.nm leader-async/leader$N.pctl |
|||
end |
|||
|
|||
|
|||
foreach N (3 4 5 6 7) |
|||
java AbstractLeaderInitial $N,leader-async/leader$N 100 21 >! leader-async/leader$N.100.21.log |
|||
end |
|||
foreach N (3 4 5 6 7) |
|||
java AbstractLeaderInitial $N,leader-async/leader$N 100 20 >! leader-async/leader$N.100.20.log |
|||
end |
|||
|
|||
|
|||
# unbounded |
|||
#java AbstractLeaderInitial $N,leader-async/leader$N -1 20 >! leader-async/leader$N.-1.21.log |
|||
#java AbstractLeaderInitial $N,leader-async/leader$N -1 20 >! leader-async/leader$N.-1.20.log |
|||
|
|||
|
|||
#================================================ |
|||
# Firewire |
|||
#================================================ |
|||
|
|||
# Generate model files |
|||
prism firewire/impl.nm -const delay=3,fast=0.5 -exportstates firewire/impl3.sta -exporttrans firewire/impl3.tra |
|||
prism firewire/impl.nm -const delay=6,fast=0.5 -exportstates firewire/impl6.sta -exporttrans firewire/impl6.tra |
|||
prism firewire/impl.nm -const delay=12,fast=0.5 -exportstates firewire/impl12.sta -exporttrans firewire/impl12.tra |
|||
prism firewire/impl.nm -const delay=24,fast=0.5 -exportstates firewire/impl24.sta -exporttrans firewire/impl24.tra |
|||
prism firewire/impl.nm -const delay=36,fast=0.5 -exportstates firewire/impl36.sta -exporttrans firewire/impl36.tra |
|||
|
|||
# Model check in PRISM (MTBDD) |
|||
prism firewire/impl.nm firewire/impl.pctl -const delay=3,fast=0.5 -prop 3 -m >! firewire/impl3.-2.exactm.log |
|||
prism firewire/impl.nm firewire/impl.pctl -const delay=6,fast=0.5 -prop 3 -m >! firewire/impl6.-2.exactm.log |
|||
prism firewire/impl.nm firewire/impl.pctl -const delay=12,fast=0.5 -prop 3 -m >! firewire/impl12.-2.exactm.log |
|||
prism firewire/impl.nm firewire/impl.pctl -const delay=24,fast=0.5 -prop 3 -m >! firewire/impl24.-2.exactm.log |
|||
prism firewire/impl.nm firewire/impl.pctl -const delay=36,fast=0.5 -prop 3 -m >! firewire/impl36.-2.exactm.log |
|||
|
|||
# Model check in PRISM (sparse) |
|||
prism firewire/impl.nm firewire/impl.pctl -const delay=3,fast=0.5 -prop 3 -s >! firewire/impl3.-2.exacts.log |
|||
prism firewire/impl.nm firewire/impl.pctl -const delay=6,fast=0.5 -prop 3 -s >! firewire/impl6.-2.exacts.log |
|||
prism firewire/impl.nm firewire/impl.pctl -const delay=12,fast=0.5 -prop 3 -s >! firewire/impl12.-2.exacts.log |
|||
prism firewire/impl.nm firewire/impl.pctl -const delay=24,fast=0.5 -prop 3 -s >! firewire/impl24.-2.exacts.log |
|||
prism firewire/impl.nm firewire/impl.pctl -const delay=36,fast=0.5 -prop 3 -s >! firewire/impl36.-2.exacts.log |
|||
|
|||
# Abstraction refinement (value-based, opt) |
|||
java AbstractFirewireInitial firewire/impl3 -2 21 -opt >! firewire/impl3.-2.21.opt.log |
|||
java AbstractFirewireInitial firewire/impl6 -2 21 -opt >! firewire/impl6.-2.21.opt.log |
|||
java AbstractFirewireInitial firewire/impl12 -2 21 -opt >! firewire/impl12.-2.21.opt.log |
|||
java -Xmx1500m AbstractFirewireInitial firewire/impl24 -2 21 -opt >! firewire/impl24.-2.21.opt.log |
|||
java -Xmx1500m AbstractFirewireInitial firewire/impl36 -2 21 -opt >! firewire/impl36.-2.21.opt.log |
|||
|
|||
# Abstraction refinement (value-based, noopt) |
|||
java AbstractFirewireInitial firewire/impl3 -2 21 -noopt >! firewire/impl3.-2.21.noopt.log |
|||
java AbstractFirewireInitial firewire/impl6 -2 21 -noopt >! firewire/impl6.-2.21.noopt.log |
|||
java AbstractFirewireInitial firewire/impl12 -2 21 -noopt >! firewire/impl12.-2.21.noopt.log |
|||
java -Xmx1500m AbstractFirewireInitial firewire/impl24 -2 21 -noopt >! firewire/impl24.-2.21.noopt.log |
|||
java -Xmx1500m AbstractFirewireInitial firewire/impl36 -2 21 -noopt >! firewire/impl36.-2.21.noopt.log |
|||
|
|||
# Abstraction refinement (strategy-based, opt) |
|||
java AbstractFirewireInitial firewire/impl3 -2 20 -opt >! firewire/impl3.-2.20.opt.log |
|||
java AbstractFirewireInitial firewire/impl6 -2 20 -opt >! firewire/impl6.-2.20.opt.log |
|||
java AbstractFirewireInitial firewire/impl12 -2 20 -opt >! firewire/impl12.-2.20.opt.log |
|||
java -Xmx1500m AbstractFirewireInitial firewire/impl24 -2 20 -opt >! firewire/impl24.-2.20.opt.log |
|||
java -Xmx1500m AbstractFirewireInitial firewire/impl36 -2 20 -opt >! firewire/impl36.-2.20.opt.log |
|||
|
|||
# Abstraction refinement (strategy-based, noopt) |
|||
java AbstractFirewireInitial firewire/impl3 -2 20 -noopt >! firewire/impl3.-2.20.noopt.log |
|||
java AbstractFirewireInitial firewire/impl6 -2 20 -noopt >! firewire/impl6.-2.20.noopt.log |
|||
java AbstractFirewireInitial firewire/impl12 -2 20 -noopt >! firewire/impl12.-2.20.noopt.log |
|||
java -Xmx1500m AbstractFirewireInitial firewire/impl24 -2 20 -noopt >! firewire/impl24.-2.20.noopt.log |
|||
java -Xmx1500m AbstractFirewireInitial firewire/impl36 -2 20 -noopt >! firewire/impl36.-2.20.noopt.log |
|||
|
|||
|
|||
#================================================ |
|||
# WLAN |
|||
#================================================ |
|||
|
|||
# Generate model files |
|||
prism wlan/wlan3.nm -const TRANS_TIME_MAX=10 -fixdl -exportstates wlan/wlan3_10.sta -exporttrans wlan/wlan3_10.tra |
|||
prism wlan/wlan5.nm -const TRANS_TIME_MAX=10 -fixdl -exportstates wlan/wlan5_10.sta -exporttrans wlan/wlan5_10.tra |
|||
prism wlan/wlan3.nm -const TRANS_TIME_MAX=316 -fixdl -exportstates wlan/wlan3_316.sta -exporttrans wlan/wlan3_316.tra |
|||
prism wlan/wlan5.nm -const TRANS_TIME_MAX=316 -fixdl -exportstates wlan/wlan5_316.sta -exporttrans wlan/wlan5_316.tra |
|||
|
|||
# Model check in PRISM |
|||
prism wlan/wlan3.nm wlan/backoff.pctl -const TRANS_TIME_MAX=10,K=3 -m >! wlan/wlan3_10.-1.exactm.log |
|||
prism wlan/wlan3.nm wlan/backoff.pctl -const TRANS_TIME_MAX=10,K=5 -m >! wlan/wlan5_10.-1.-exactm.log |
|||
prism wlan/wlan3.nm wlan/backoff.pctl -const TRANS_TIME_MAX=316=3 -m >! wlan/wlan3_316.-1.-exactm.log |
|||
prism wlan/wlan3.nm wlan/backoff.pctl -const TRANS_TIME_MAX=316,K=5 -m >! wlan/wlan5_316.-1.-exactm.log |
|||
|
|||
# Abstraction refinement (value-based, opt) |
|||
java AbstractWlanProbInitial 3,wlan/wlan3_10 -1 21 -opt >! wlan/wlan3_10.-1.21.opt.log |
|||
java AbstractWlanProbInitial 5,wlan/wlan5_10 -1 21 -opt >! wlan/wlan5_10.-1.21.opt.log |
|||
java AbstractWlanProbInitial 3,wlan/wlan3_316 -1 21 -opt >! wlan/wlan3_316.-1.21.opt.log |
|||
java AbstractWlanProbInitial 5,wlan/wlan5_316 -1 21 -opt >! wlan/wlan5_316.-1.21.opt.log |
|||
|
|||
# Abstraction refinement (value-based, noopt) |
|||
java AbstractWlanProbInitial 2,wlan/wlan2_10 -1 21 -noopt >! wlan/wlan2_10.-1.21.noopt.log |
|||
java AbstractWlanProbInitial 3,wlan/wlan3_10 -1 21 -noopt >! wlan/wlan3_10.-1.21.noopt.log |
|||
java AbstractWlanProbInitial 4,wlan/wlan4_10 -1 21 -noopt >! wlan/wlan4_316.-1.21.noopt.log |
|||
java AbstractWlanProbInitial 5,wlan/wlan5_10 -1 21 -noopt >! wlan/wlan5_316.-1.21.noopt.log |
|||
|
|||
# Abstraction refinement (strategy-based) |
|||
java AbstractWlanProbInitial 2,wlan/wlan2_10 -1 20 -noopt >! wlan/wlan2_10.-1.20.noopt.log |
|||
java AbstractWlanProbInitial 3,wlan/wlan3_10 -1 20 -noopt >! wlan/wlan3_10.-1.20.noopt.log |
|||
java AbstractWlanProbInitial 4,wlan/wlan4_10 -1 20 -noopt >! wlan/wlan4_10.-1.20.noopt.log |
|||
java AbstractWlanProbInitial 5,wlan/wlan5_10 -1 20 -noopt >! wlan/wlan5_10.-1.20.noopt.log |
|||
|
|||
|
|||
#================================================ |
|||
# csma |
|||
#================================================ |
|||
|
|||
# Generate model files |
|||
prism csma/csma.nm -const K=2 -exporttrans csma/csma2.tra -exportstates csma/csma2.sta |
|||
prism csma/csma.nm -const K=3 -exporttrans csma/csma3.tra -exportstates csma/csma3.sta |
|||
prism csma/csma.nm -const K=4 -exporttrans csma/csma4.tra -exportstates csma/csma4.sta |
|||
prism csma/csma.nm -const K=5 -exporttrans csma/csma5.tra -exportstates csma/csma5.sta |
|||
prism csma/csma.nm -const K=6 -exporttrans csma/csma6.tra -exportstates csma/csma6.sta |
|||
prism csma/csma.nm -const K=7 -exporttrans csma/csma7.tra -exportstates csma/csma7.sta |
|||
prism csma/csma.nm -const K=8 -exporttrans csma/csma8.tra -exportstates csma/csma8.sta |
|||
|
|||
# Model check in PRISM (sparse) |
|||
prism csma/csma.nm csma/backoff.pctl -const K=2 -s >! csma/csma2.-1.exacts.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=4 -s >! csma/csma4.-1.exacts.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=6 -s >! csma/csma6.-1.exacts.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=7 -s >! csma/csma7.-1.exacts.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=8 -s >! csma/csma8.-1.exacts.log |
|||
|
|||
# Model check in PRISM (MTBDD) |
|||
prism csma/csma.nm csma/backoff.pctl -const K=2 -m >! csma/csma2.-1.exactm.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=4 -m >! csma/csma4.-1.exactm.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=6 -m >! csma/csma6.-1.exactm.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=7 -m >! csma/csma7.-1.exactm.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=8 -m >! csma/csma8.-1.exactm.log |
|||
|
|||
# Model check in PRISM (hybrid) |
|||
prism csma/csma.nm csma/backoff.pctl -const K=2 -h >! csma/csma2.-1.exacth.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=4 -h >! csma/csma4.-1.exacth.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=6 -h >! csma/csma6.-1.exacth.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=7 -h >! csma/csma7.-1.exacth.log |
|||
prism csma/csma.nm csma/backoff.pctl -const K=8 -h >! csma/csma8.-1.exacth.log |
|||
|
|||
# Abstraction refinement (value-based, opt) |
|||
java AbstractCsmaProbInitial 2,csma/csma2 -1 21 -opt >! csma/csma2.-1.21.opt.log |
|||
java AbstractCsmaProbInitial 3,csma/csma3 -1 21 -opt >! csma/csma3.-1.21.opt.log |
|||
java AbstractCsmaProbInitial 4,csma/csma4 -1 21 -opt >! csma/csma4.-1.21.opt.log |
|||
java AbstractCsmaProbInitial 5,csma/csma5 -1 21 -opt >! csma/csma5.-1.21.opt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 6,csma/csma6 -1 21 -opt >! csma/csma6.-1.21.opt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 7,csma/csma7 -1 21 -opt >! csma/csma7.-1.21.opt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 8,csma/csma8 -1 21 -opt >! csma/csma8.-1.21.opt.log |
|||
|
|||
# Abstraction refinement (value-based, noopt) |
|||
java AbstractCsmaProbInitial 2,csma/csma2 -1 21 -noopt >! csma/csma2.-1.21.noopt.log |
|||
java AbstractCsmaProbInitial 3,csma/csma3 -1 21 -noopt >! csma/csma3.-1.21.noopt.log |
|||
java AbstractCsmaProbInitial 4,csma/csma4 -1 21 -noopt >! csma/csma4.-1.21.noopt.log |
|||
java AbstractCsmaProbInitial 5,csma/csma5 -1 21 -noopt >! csma/csma5.-1.21.noopt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 6,csma/csma6 -1 21 -noopt >! csma/csma6.-1.21.noopt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 7,csma/csma7 -1 21 -noopt >! csma/csma7.-1.21.noopt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 8,csma/csma8 -1 21 -noopt >! csma/csma8.-1.21.noopt.log |
|||
|
|||
# Abstraction refinement (strategy-based, opt) |
|||
java AbstractCsmaProbInitial 2,csma/csma2 -1 20 -opt >! csma/csma2.-1.20.opt.log |
|||
java AbstractCsmaProbInitial 3,csma/csma3 -1 20 -opt >! csma/csma3.-1.20.opt.log |
|||
java AbstractCsmaProbInitial 4,csma/csma4 -1 20 -opt >! csma/csma4.-1.20.opt.log |
|||
java AbstractCsmaProbInitial 5,csma/csma5 -1 20 -opt >! csma/csma5.-1.20.opt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 6,csma/csma6 -1 20 -opt >! csma/csma6.-1.20.opt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 7,csma/csma7 -1 20 -opt >! csma/csma7.-1.20.opt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 8,csma/csma8 -1 20 -opt >! csma/csma8.-1.20.opt.log |
|||
|
|||
# Abstraction refinement (strategy-based, noopt) |
|||
java AbstractCsmaProbInitial 2,csma/csma2 -1 20 -noopt >! csma/csma2.-1.20.noopt.log |
|||
java AbstractCsmaProbInitial 3,csma/csma3 -1 20 -noopt >! csma/csma3.-1.20.noopt.log |
|||
java AbstractCsmaProbInitial 4,csma/csma4 -1 20 -noopt >! csma/csma4.-1.20.noopt.log |
|||
java AbstractCsmaProbInitial 5,csma/csma5 -1 20 -noopt >! csma/csma5.-1.20.noopt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 6,csma/csma6 -1 20 -noopt >! csma/csma6.-1.20.noopt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 7,csma/csma7 -1 20 -noopt >! csma/csma7.-1.20.noopt.log |
|||
java -Xmx1500m AbstractCsmaProbInitial 8,csma/csma8 -1 20 -noopt >! csma/csma8.-1.20.noopt.log |
|||
|
|||
|
|||
#================================================ |
|||
# BRP |
|||
#================================================ |
|||
|
|||
foreach N (16 32 64) |
|||
foreach MAX (2 3 4 5) |
|||
prism brp/brp.nm -const N=$N,MAX=$MAX -fixdl -exportstates brp/brp$N_"$MAX".sta -exporttrans brp/brp$N_"$MAX".tra |
|||
end |
|||
end |
|||
|
|||
foreach N (16 32 64) |
|||
foreach MAX (2 3 4 5) |
|||
java AbstractBRPInitial brp/brp$N_"$MAX" -1 21 >! brp/brp$N_"$MAX".-1.21.log |
|||
java AbstractBRPInitial brp/brp$N_"$MAX" -1 20 >! brp/brp$N_"$MAX".-1.20.log |
|||
end |
|||
end |
|||
|
|||
#================================================ |
|||
# Consensus |
|||
#================================================ |
|||
|
|||
java AbstractConsensusInitial 5,2,consensus/consensus5_2 -2 20 >! consensus/consensus5.2.-1.20.log |
|||
java AbstractConsensusInitial 5,4,consensus/consensus5_4 -2 20 >! consensus/consensus5.4.-1.20.log |
|||
java AbstractConsensusInitial 5,8,consensus/consensus5_8 -2 20 >! consensus/consensus5.8.-1.20.log |
|||
java AbstractConsensusInitial 5,16,consensus/consensus5_16 -2 20 >! consensus/consensus5.16.-1.20.log |
|||
java AbstractConsensusInitial 5,2,consensus/consensus5_2 -2 21 -noopt >! consensus/consensus5.2.-1.21.noopt.log |
|||
java AbstractConsensusInitial 5,4,consensus/consensus5_4 -2 21 -noopt >! consensus/consensus5.4.-1.21.noopt.log |
|||
java AbstractConsensusInitial 5,8,consensus/consensus5_8 -2 21 -noopt >! consensus/consensus5.8.-1.21.noopt.log |
|||
java AbstractConsensusInitial 5,16,consensus/consensus5_16 -2 21 -noopt >! consensus/consensus5.16.-1.21.noopt.log |
|||
java AbstractConsensusInitial 5,2,consensus/consensus5_2 -2 20 -noopt >! consensus/consensus5.2.-1.20.noopt.log |
|||
java AbstractConsensusInitial 5,4,consensus/consensus5_4 -2 20 -noopt >! consensus/consensus5.4.-1.20.noopt.log |
|||
java AbstractConsensusInitial 5,8,consensus/consensus5_8 -2 20 -noopt >! consensus/consensus5.8.-1.20.noopt.log |
|||
java AbstractConsensusInitial 5,16,consensus/consensus5_16 -2 20 -noopt >! consensus/consensus5.16.-1.20.noopt.log |
|||
|
|||
@ -1 +0,0 @@ |
|||
Pmax=? [ F "bcmax" ] |
|||
@ -1 +0,0 @@ |
|||
Pmax=? [ F "bcmax" ] |
|||
@ -1,270 +0,0 @@ |
|||
// WLAN PROTOCOL (two stations) |
|||
// discrete time model |
|||
// gxn/jzs 20/02/02 |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// we start with both stations sending a packet at the same time to get a collision |
|||
// then model the backoff procedure of the IEEE 802.11 Wireless LAN |
|||
// note that each station tries to send only one packet |
|||
|
|||
// the the destinations are completely deterministic and have therefore been removed |
|||
|
|||
// we have not included transitions from states in which the ack is corrupted |
|||
// however with the timing constraints used (that is because SIFS<DIFS) this |
|||
// cannot happen, e.g. (s1=11 & c1=2) | (s2=11 & c2=2) does not hold in any state |
|||
|
|||
// the length of packets are non-deterministic: |
|||
// even when the same packet is resent we allow the length to change |
|||
// furthermore the adversary is able to decide on the length of the packet while it is being sent |
|||
|
|||
// in this model we do not model the Timing Synchronization Function (TSF) |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// TIMING CONSTRAINTS |
|||
// we have used the FHSS parameters |
|||
// then scaled by the value of ASLOTTIME |
|||
|
|||
const ASLOTTIME = 1; |
|||
const DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice |
|||
const VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
|||
const TRANS_TIME_MAX; // scaling up |
|||
const TRANS_TIME_MIN = 4; // scaling down |
|||
const ACK_TO = 6; |
|||
const ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice |
|||
const 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 TIME_MAX = TRANS_TIME_MAX+1; |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// CONTENTION WINDOW |
|||
// CWMIN =15 & CWMAX =63 |
|||
// this means that MAX_BACKOFF IS 2 |
|||
const MAX_BACKOFF = 2; |
|||
|
|||
// the probabilistic choices are: |
|||
|
|||
// when backoff counter is 0 uniformly choose backoff from [0..15] |
|||
// when backoff counter is 1 uniformly choose backoff from [0..31] |
|||
// when backoff counter is 2 uniformly choose backoff from [0..63] |
|||
|
|||
// to simplify the probabilistic choices we split the backoff into slots of size [0..15] |
|||
// in each slot backoff is decremented until zero and then the slot is decremented |
|||
// with backoff being set to 15, this then gives the following choices: |
|||
|
|||
// when backoff counter is 0 uniformly choose slot from [0..0] then backoff from [0..15] |
|||
// when backoff counter is 1 uniformly choose slot from [0..1] then backoff from [0..15] |
|||
// when backoff counter is 2 uniformly choose slot from [0..3] then backoff from [0..15] |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// THE MEDIUM/CHANNEL |
|||
module medium |
|||
|
|||
// 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 |
|||
|
|||
[time] true -> (c1'=c1); |
|||
|
|||
// 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); |
|||
[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2); |
|||
|
|||
// finish sending message |
|||
[finish1] c1>0 -> (c1'=0); |
|||
[finish2] c2>0 -> (c2'=0); |
|||
|
|||
endmodule |
|||
|
|||
// FORMULAE FOR THE CHANNEL |
|||
// channel is busy |
|||
formula busy = c1>0 | c2>0; |
|||
// channel is free |
|||
formula free = c1=0 & c2=0; |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// 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..3]; |
|||
backoff1 : [0..15]; |
|||
|
|||
// BACKOFF COUNTER |
|||
bc1 : [0..MAX_BACKOFF]; |
|||
|
|||
// 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)); |
|||
// backoff counter 1 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
|||
// backoff counter 2 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (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); |
|||
// chack channel and free: let time pass |
|||
[time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
|||
// let time pass |
|||
[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 "bcmax" = bc1=MAX_BACKOFF & bc2=MAX_BACKOFF; |
|||
@ -1,281 +0,0 @@ |
|||
// WLAN PROTOCOL (two stations) |
|||
// discrete time model |
|||
// gxn/jzs 20/02/02 |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// we start with both stations sending a packet at the same time to get a collision |
|||
// then model the backoff procedure of the IEEE 802.11 Wireless LAN |
|||
// note that each station tries to send only one packet |
|||
|
|||
// the the destinations are completely deterministic and have therefore been removed |
|||
|
|||
// we have not included transitions from states in which the ack is corrupted |
|||
// however with the timing constraints used (that is because SIFS<DIFS) this |
|||
// cannot happen, e.g. (s1=11 & c1=2) | (s2=11 & c2=2) does not hold in any state |
|||
|
|||
// the length of packets are non-deterministic: |
|||
// even when the same packet is resent we allow the length to change |
|||
// furthermore the adversary is able to decide on the length of the packet while it is being sent |
|||
|
|||
// in this model we do not model the Timing Synchronization Function (TSF) |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// TIMING CONSTRAINTS |
|||
// we have used the FHSS parameters |
|||
// then scaled by the value of ASLOTTIME |
|||
|
|||
const ASLOTTIME = 1; |
|||
const DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice |
|||
const VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
|||
const TRANS_TIME_MAX; // scaling up |
|||
const TRANS_TIME_MIN = 4; // scaling down |
|||
const ACK_TO = 6; |
|||
const ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice |
|||
const 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 TIME_MAX = TRANS_TIME_MAX+1; |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// CONTENTION WINDOW |
|||
// CWMIN =15 & CWMAX =127 |
|||
// this means that MAX_BACKOFF IS 3 |
|||
const MAX_BACKOFF = 3; |
|||
|
|||
// the probabilistic choices are: |
|||
|
|||
// when backoff counter is 0 uniformly choose backoff from [0..15] |
|||
// when backoff counter is 1 uniformly choose backoff from [0..31] |
|||
// when backoff counter is 2 uniformly choose backoff from [0..63] |
|||
// when backoff counter is 3 uniformly choose backoff from [0..127] |
|||
|
|||
// to simplify the probabilistic choices we split the backoff into slots of size [0..15] |
|||
// in each slot backoff is decremented until zero and then the slot is decremented |
|||
// with backoff being set to 15, this then gives the following choices: |
|||
|
|||
// when backoff counter is 0 uniformly choose slot from [0..0] then backoff from [0..15] |
|||
// when backoff counter is 1 uniformly choose slot from [0..1] then backoff from [0..15] |
|||
// when backoff counter is 2 uniformly choose slot from [0..3] then backoff from [0..15] |
|||
// when backoff counter is 3 uniformly choose slot from [0..7] then backoff from [0..15] |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// THE MEDIUM/CHANNEL |
|||
module medium |
|||
|
|||
// 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 |
|||
|
|||
[time] true -> (c1'=c1); |
|||
|
|||
// 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); |
|||
[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2); |
|||
|
|||
// finish sending message |
|||
[finish1] c1>0 -> (c1'=0); |
|||
[finish2] c2>0 -> (c2'=0); |
|||
|
|||
endmodule |
|||
|
|||
// FORMULAE FOR THE CHANNEL |
|||
// channel is busy |
|||
formula busy = c1>0 | c2>0; |
|||
// channel is free |
|||
formula free = c1=0 & c2=0; |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// 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..7]; |
|||
backoff1 : [0..15]; |
|||
|
|||
// BACKOFF COUNTER |
|||
bc1 : [0..MAX_BACKOFF]; |
|||
|
|||
// 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)); |
|||
// backoff counter 1 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
|||
// backoff counter 2 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
|||
// backoff counter 3 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 -> 1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (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); |
|||
// chack channel and free: let time pass |
|||
[time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
|||
// let time pass |
|||
[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 "bcmax" = bc1=MAX_BACKOFF & bc2=MAX_BACKOFF; |
|||
@ -1,300 +0,0 @@ |
|||
// WLAN PROTOCOL (two stations) |
|||
// discrete time model |
|||
// gxn/jzs 20/02/02 |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// we start with both stations sending a packet at the same time to get a collision |
|||
// then model the backoff procedure of the IEEE 802.11 Wireless LAN |
|||
// note that each station tries to send only one packet |
|||
|
|||
// the the destinations are completely deterministic and have therefore been removed |
|||
|
|||
// we have not included transitions from states in which the ack is corrupted |
|||
// however with the timing constraints used (that is because SIFS<DIFS) this |
|||
// cannot happen, e.g. (s1=11 & c1=2) | (s2=11 & c2=2) does not hold in any state |
|||
|
|||
// the length of packets are non-deterministic: |
|||
// even when the same packet is resent we allow the length to change |
|||
// furthermore the adversary is able to decide on the length of the packet while it is being sent |
|||
|
|||
// in this model we do not model the Timing Synchronization Function (TSF) |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// TIMING CONSTRAINTS |
|||
// we have used the FHSS parameters |
|||
// then scaled by the value of ASLOTTIME |
|||
|
|||
const ASLOTTIME = 1; |
|||
const DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice |
|||
const VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
|||
const TRANS_TIME_MAX; // scaling up |
|||
const TRANS_TIME_MIN = 4; // scaling down |
|||
const ACK_TO = 6; |
|||
const ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice |
|||
const 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 TIME_MAX = TRANS_TIME_MAX+1; |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// CONTENTION WINDOW |
|||
// CWMIN =15 & CWMAX =255 |
|||
// this means that MAX_BACKOFF IS 4 |
|||
const MAX_BACKOFF = 4; |
|||
|
|||
// the probabilistic choices are: |
|||
|
|||
// when backoff counter is 0 uniformly choose backoff from [0..15] |
|||
// when backoff counter is 1 uniformly choose backoff from [0..31] |
|||
// when backoff counter is 2 uniformly choose backoff from [0..63] |
|||
// when backoff counter is 3 uniformly choose backoff from [0..127] |
|||
// when backoff counter is 4 uniformly choose backoff from [0..255] |
|||
|
|||
// to simplify the probabilistic choices we split the backoff into slots of size [0..15] |
|||
// in each slot backoff is decremented until zero and then the slot is decremented |
|||
// with backoff being set to 15, this then gives the following choices: |
|||
|
|||
// when backoff counter is 0 uniformly choose slot from [0..0] then backoff from [0..15] |
|||
// when backoff counter is 1 uniformly choose slot from [0..1] then backoff from [0..15] |
|||
// when backoff counter is 2 uniformly choose slot from [0..3] then backoff from [0..15] |
|||
// when backoff counter is 3 uniformly choose slot from [0..7] then backoff from [0..15] |
|||
// when backoff counter is 4 uniformly choose slot from [0..15] then backoff from [0..15] |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// THE MEDIUM/CHANNEL |
|||
module medium |
|||
|
|||
// 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 |
|||
|
|||
[time] true -> (c1'=c1); |
|||
|
|||
// 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); |
|||
[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2); |
|||
|
|||
// finish sending message |
|||
[finish1] c1>0 -> (c1'=0); |
|||
[finish2] c2>0 -> (c2'=0); |
|||
|
|||
endmodule |
|||
|
|||
// FORMULAE FOR THE CHANNEL |
|||
// channel is busy |
|||
formula busy = c1>0 | c2>0; |
|||
// channel is free |
|||
formula free = c1=0 & c2=0; |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// 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..15]; |
|||
backoff1 : [0..15]; |
|||
|
|||
// BACKOFF COUNTER |
|||
bc1 : [0..MAX_BACKOFF]; |
|||
|
|||
// 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)); |
|||
// backoff counter 1 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
|||
// backoff counter 2 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
|||
// backoff counter 3 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 -> 1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
|||
// backoff counter 4 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=4 -> 1/16 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=15) & (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); |
|||
// chack channel and free: let time pass |
|||
[time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
|||
// let time pass |
|||
[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 "bcmax" = bc1=MAX_BACKOFF & bc2=MAX_BACKOFF; |
|||
@ -1,336 +0,0 @@ |
|||
// WLAN PROTOCOL (two stations) |
|||
// discrete time model |
|||
// gxn/jzs 20/02/02 |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// we start with both stations sending a packet at the same time to get a collision |
|||
// then model the backoff procedure of the IEEE 802.11 Wireless LAN |
|||
// note that each station tries to send only one packet |
|||
|
|||
// the the destinations are completely deterministic and have therefore been removed |
|||
|
|||
// we have not included transitions from states in which the ack is corrupted |
|||
// however with the timing constraints used (that is because SIFS<DIFS) this |
|||
// cannot happen, e.g. (s1=11 & c1=2) | (s2=11 & c2=2) does not hold in any state |
|||
|
|||
// the length of packets are non-deterministic: |
|||
// even when the same packet is resent we allow the length to change |
|||
// furthermore the adversary is able to decide on the length of the packet while it is being sent |
|||
|
|||
// in this model we do not model the Timing Synchronization Function (TSF) |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// TIMING CONSTRAINTS |
|||
// we have used the FHSS parameters |
|||
// then scaled by the value of ASLOTTIME |
|||
|
|||
const ASLOTTIME = 1; |
|||
const DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice |
|||
const VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice |
|||
const TRANS_TIME_MAX; // scaling up |
|||
const TRANS_TIME_MIN = 4; // scaling down |
|||
const ACK_TO = 6; |
|||
const ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice |
|||
const 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 TIME_MAX = TRANS_TIME_MAX+1; |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// CONTENTION WINDOW |
|||
// CWMIN =15 & CWMAX =511 |
|||
// this means that MAX_BACKOFF IS 5 |
|||
const MAX_BACKOFF = 5; |
|||
|
|||
// the probabilistic choices are: |
|||
|
|||
// when backoff counter is 0 uniformly choose backoff from [0..15] |
|||
// when backoff counter is 1 uniformly choose backoff from [0..31] |
|||
// when backoff counter is 2 uniformly choose backoff from [0..63] |
|||
// when backoff counter is 3 uniformly choose backoff from [0..127] |
|||
// when backoff counter is 4 uniformly choose backoff from [0..255] |
|||
// when backoff counter is 5 uniformly choose backoff from [0..511] |
|||
|
|||
// to simplify the probabilistic choices we split the backoff into slots of size [0..15] |
|||
// in each slot backoff is decremented until zero and then the slot is decremented |
|||
// with backoff being set to 15, this then gives the following choices: |
|||
|
|||
// when backoff counter is 0 uniformly choose slot from [0..0] then backoff from [0..15] |
|||
// when backoff counter is 1 uniformly choose slot from [0..1] then backoff from [0..15] |
|||
// when backoff counter is 2 uniformly choose slot from [0..3] then backoff from [0..15] |
|||
// when backoff counter is 3 uniformly choose slot from [0..7] then backoff from [0..15] |
|||
// when backoff counter is 4 uniformly choose slot from [0..15] then backoff from [0..15] |
|||
// when backoff counter is 5 uniformly choose slot from [0..31] then backoff from [0..15] |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// THE MEDIUM/CHANNEL |
|||
module medium |
|||
|
|||
// 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 |
|||
|
|||
[time] true -> (c1'=c1); |
|||
|
|||
// 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); |
|||
[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2); |
|||
|
|||
// finish sending message |
|||
[finish1] c1>0 -> (c1'=0); |
|||
[finish2] c2>0 -> (c2'=0); |
|||
|
|||
endmodule |
|||
|
|||
// FORMULAE FOR THE CHANNEL |
|||
// channel is busy |
|||
formula busy = c1>0 | c2>0; |
|||
// channel is free |
|||
formula free = c1=0 & c2=0; |
|||
|
|||
//-----------------------------------------------------------------// |
|||
|
|||
// 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..31]; |
|||
backoff1 : [0..15]; |
|||
|
|||
// BACKOFF COUNTER |
|||
bc1 : [0..MAX_BACKOFF]; |
|||
|
|||
// 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)); |
|||
// backoff counter 1 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
|||
// backoff counter 2 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
|||
// backoff counter 3 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 -> 1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
|||
// backoff counter 4 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=4 -> 1/16 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF)); |
|||
// backoff counter 5 |
|||
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=5 -> 1/32 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=16) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=17) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=18) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=19) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=20) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=21) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=22) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=23) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=24) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=25) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=26) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=27) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=28) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=29) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=30) & (bc1'=min(bc1+1,MAX_BACKOFF)) |
|||
+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=31) & (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); |
|||
// chack channel and free: let time pass |
|||
[time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); |
|||
// let time pass |
|||
[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 "bcmax" = bc1=MAX_BACKOFF & bc2=MAX_BACKOFF; |
|||
@ -1 +0,0 @@ |
|||
Pmin=? [ F "done_correct" ] |
|||
@ -1,166 +0,0 @@ |
|||
#const N# |
|||
#const M# |
|||
#const K# |
|||
// full model of zeroconf protocol |
|||
// dxp/gxn 21/09/06 |
|||
|
|||
mdp |
|||
|
|||
// constants |
|||
const int probe_time = 20; // time to send a probe |
|||
const int N = #N#; // number of existing hosts |
|||
const int M = #M#; // number of possible ip addresses |
|||
const int K = #K#; // number of probes to send |
|||
// host ip addresses |
|||
#for i=1:N# |
|||
const int ip#i# = #i#; |
|||
#end# |
|||
|
|||
// time for messages to be sent and probability of message loss |
|||
const int min_send1 = 2; |
|||
const int max_send1 = 8; |
|||
const double loss1 = 0.01*(min_send1+max_send1)/2; |
|||
|
|||
const int min_send2 = 3; |
|||
const int max_send2 = 6; |
|||
const double loss2 = 0.01*(min_send2+max_send2)/2; |
|||
|
|||
const int min_send3 = 1; |
|||
const int max_send3 = 2; |
|||
const double loss3 = 0.01*(min_send3+max_send3)/2; |
|||
|
|||
const int min_send4 = 6; |
|||
const int max_send4 = 9; |
|||
const double loss4 = 0.01*(min_send4+max_send4)/2; |
|||
|
|||
// formula: true when the channel is free |
|||
formula channel_free = chan=0; |
|||
|
|||
module channel |
|||
|
|||
chan : [0..1]; |
|||
|
|||
[broadcast] true -> (chan'=1); |
|||
|
|||
#for i=1:N# |
|||
[rec0#i#] #+ j=1:N#s0#j##end#=1 -> (chan'=0); |
|||
#end# |
|||
|
|||
#for i=1:N# |
|||
[rec0#i#] #+ j=1:N#s0#j##end#>1 -> true; |
|||
#end# |
|||
|
|||
#for i=1:N# |
|||
[send#i#0] true -> (chan'=1); |
|||
#end# |
|||
|
|||
#for i=1:N# |
|||
[rec#i#0] true -> (chan'=0); |
|||
#end# |
|||
|
|||
endmodule |
|||
|
|||
// host which is trying to configure its ip address |
|||
module host0 |
|||
|
|||
s0 : [0..4]; |
|||
// 0 make random choice |
|||
// 1 send first probe (to buffer) |
|||
// 2 send remaining probes |
|||
// 3 wait before using |
|||
// 4 using |
|||
|
|||
ip0 : [0..M]; // current chosen ip address |
|||
x0 : [0..probe_time]; // local clock |
|||
probes : [0..K]; // number of probes sent |
|||
|
|||
// make choice (rest action used to clear buffer) |
|||
[reset] s0=0 -> #+ i=1:M#1/M : (ip0'=#i#) & (s0'=1)#end#; |
|||
|
|||
// send first probe |
|||
[broadcast] s0=1 & probes=0 -> (s0'=2) & (probes'=probes+1); |
|||
// let time pass before sending next probe |
|||
[time] s0=2 & x0<probe_time -> (x0'=x0+1); |
|||
// send a probe (not last probe) |
|||
[broadcast] s0=2 & x0=probe_time & probes<K-1 -> (s0'=2) & (probes'=probes+1) & (x0'=0); |
|||
// send last probe |
|||
[broadcast] s0=2 & x0=probe_time & probes=K-1 -> (s0'=3) & (probes'=0) & (x0'=0); |
|||
// wait |
|||
[time] s0=3 & x0<probe_time -> (x0'=x0+1); |
|||
// finished waiting |
|||
[done] s0=3 & x0=probe_time -> (s0'=4) & (x0'=0); |
|||
// use ip address (loop) |
|||
[] s0=4 -> true; |
|||
|
|||
// receive an ARP and reconfigure (same IP address) |
|||
#for i=1:N# |
|||
[rec#i#0] s0>0 & s0<4 & ip0=m#i#0 -> (s0'=0) & (probes'=0) & (ip0'=0) & (x0'=0); |
|||
#end# |
|||
// receive an ARP and do nothing (different IP address) |
|||
#for i=1:N# |
|||
[rec#i#0] s0=0 | (s0>0 & s0<4 & !ip0=m#i#0) -> true; |
|||
#end# |
|||
|
|||
endmodule |
|||
|
|||
// messages to host 1 |
|||
module sender01 |
|||
|
|||
s01 : [0..1]; // 0 - no message, 1 - message being sent |
|||
x01 : [0..max_send1]; // local clock |
|||
m01 : [0..M]; // ip address in message |
|||
|
|||
// let time pass if nothing being sent |
|||
[time] s01=0 -> true; |
|||
// receive a message to be sent |
|||
[broadcast] s01=0 -> 1-loss1 : (s01'=1) & (m01'=ip0) + loss1 : (s01'=1) & (m01'=0); |
|||
// message not arrived yet |
|||
[time] s01=1 & x01<max_send1 -> (x01'=x01+1); |
|||
// message arrives |
|||
[rec01] s01=1 & x0>=min_send1 -> (s01'=0) & (x01'=0) & (m01'=0); |
|||
|
|||
endmodule |
|||
|
|||
// messages to host 2 |
|||
#for i=2:N# |
|||
module sender0#i# = sender01 [ s01=s0#i#, ip1=ip#i#, m01=m0#i#, x01=x0#i#, rec01=rec0#i#, min_send1=min_send#func(mod,i-1,4)+1#, max_send1=max_send#func(mod,i-1,4)+1#, loss1=loss#func(mod,i-1,4)+1# ] endmodule |
|||
#end# |
|||
|
|||
// messages from sender 1 (need a buffer) |
|||
module sender10 |
|||
|
|||
s10 : [0..2]; // 0 - no message, 1 - message to be sent 2 sending message |
|||
x10 : [0..max_send1]; // local clock |
|||
m10 : [0..M]; // ip address in message |
|||
|
|||
|
|||
// nothing to send so let time pass |
|||
[time] s10=0 -> true; |
|||
// receive a message and no reply |
|||
[rec01] !m01=ip1 -> true; |
|||
// receive a message and reply (add to buffer) |
|||
[rec01] m01=ip1 -> (s10'=1) & (m10'=m01); |
|||
// cannot reply yet |
|||
[time] s10=1 & !channel_free -> true; |
|||
[send10] s10=1 & channel_free -> 1-loss1 : (s10'=2) & (x10'=0) |
|||
+ loss1 : (s10'=2) & (x10'=0) & (m10'=0); |
|||
// message not arrived yet |
|||
[time] s10=2 & x10<max_send1 -> (x10'=x10+1); |
|||
// deliver message |
|||
[rec10] s10=2 & x10>=min_send1 -> (s10'=0) & (m10'=0) & (x10'=0); |
|||
|
|||
endmodule |
|||
|
|||
// messages from host 2 |
|||
#for i=2:N# |
|||
module sender#i#0 = sender10 [ s10=s#i#0, m10=m#i#0, m01=m0#i#, x10=x#i#0, rec01=rec0#i#, send10=send#i#0, rec10=rec#i#0, ip1=ip#i#, min_send1=min_send#func(mod,i-1,4)+1#, max_send1=max_send#func(mod,i-1,4)+1#, loss1=loss#func(mod,i-1,4)+1# ] endmodule |
|||
#end# |
|||
|
|||
label "done_correct" = s0=4 & ip0<=N; |
|||
|
|||
rewards |
|||
|
|||
[time] true : 0.1; |
|||
[done] ip0=1 | ip0=2 : 1000000; |
|||
|
|||
endrewards |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue