From 9d47781cb6b43ed401c6541353f125d084edf1a8 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 15 Oct 2010 15:25:13 +0000 Subject: [PATCH] Removal of explicit/ctmdp examples (moved to qar). git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2141 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/examples/ctmdp/NOTES | 9 - prism/examples/ctmdp/Neu10.lab | 3 - prism/examples/ctmdp/Neu10.sm | 20 - prism/examples/ctmdp/Neu10.tra | 7 - prism/examples/ctmdp/erlang.sm | 28 - prism/examples/ctmdp/jsp.csl | 1 - prism/examples/ctmdp/jsp.lab | 3 - prism/examples/ctmdp/jsp.sm | 58 -- prism/examples/ctmdp/jsp.tra | 42 -- prism/examples/explicit/NOTES | 516 ------------------ prism/examples/explicit/wlan/backoff.pctl | 1 - prism/examples/explicit/wlan/wlan.pctl | 1 - prism/examples/explicit/wlan/wlan2.nm | 270 --------- prism/examples/explicit/wlan/wlan3.nm | 281 ---------- prism/examples/explicit/wlan/wlan4.nm | 300 ---------- prism/examples/explicit/wlan/wlan5.nm | 336 ------------ .../examples/explicit/zeroconf/zeroconf.pctl | 1 - .../explicit/zeroconf/zeroconfN_M_K.nm.pp | 166 ------ 18 files changed, 2043 deletions(-) delete mode 100644 prism/examples/ctmdp/NOTES delete mode 100644 prism/examples/ctmdp/Neu10.lab delete mode 100644 prism/examples/ctmdp/Neu10.sm delete mode 100644 prism/examples/ctmdp/Neu10.tra delete mode 100644 prism/examples/ctmdp/erlang.sm delete mode 100644 prism/examples/ctmdp/jsp.csl delete mode 100644 prism/examples/ctmdp/jsp.lab delete mode 100644 prism/examples/ctmdp/jsp.sm delete mode 100644 prism/examples/ctmdp/jsp.tra delete mode 100644 prism/examples/explicit/NOTES delete mode 100644 prism/examples/explicit/wlan/backoff.pctl delete mode 100644 prism/examples/explicit/wlan/wlan.pctl delete mode 100644 prism/examples/explicit/wlan/wlan2.nm delete mode 100644 prism/examples/explicit/wlan/wlan3.nm delete mode 100644 prism/examples/explicit/wlan/wlan4.nm delete mode 100644 prism/examples/explicit/wlan/wlan5.nm delete mode 100644 prism/examples/explicit/zeroconf/zeroconf.pctl delete mode 100644 prism/examples/explicit/zeroconf/zeroconfN_M_K.nm.pp diff --git a/prism/examples/ctmdp/NOTES b/prism/examples/ctmdp/NOTES deleted file mode 100644 index 59d6821b..00000000 --- a/prism/examples/ctmdp/NOTES +++ /dev/null @@ -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 diff --git a/prism/examples/ctmdp/Neu10.lab b/prism/examples/ctmdp/Neu10.lab deleted file mode 100644 index 140f2c5a..00000000 --- a/prism/examples/ctmdp/Neu10.lab +++ /dev/null @@ -1,3 +0,0 @@ -0="init" 1="deadlock" 2="target" -0: 0 -2: 2 diff --git a/prism/examples/ctmdp/Neu10.sm b/prism/examples/ctmdp/Neu10.sm deleted file mode 100644 index a4b23c29..00000000 --- a/prism/examples/ctmdp/Neu10.sm +++ /dev/null @@ -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; diff --git a/prism/examples/ctmdp/Neu10.tra b/prism/examples/ctmdp/Neu10.tra deleted file mode 100644 index 22983c8e..00000000 --- a/prism/examples/ctmdp/Neu10.tra +++ /dev/null @@ -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 diff --git a/prism/examples/ctmdp/erlang.sm b/prism/examples/ctmdp/erlang.sm deleted file mode 100644 index 1840fa75..00000000 --- a/prism/examples/ctmdp/erlang.sm +++ /dev/null @@ -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 diff --git a/prism/examples/ctmdp/jsp.csl b/prism/examples/ctmdp/jsp.csl deleted file mode 100644 index 1c1e8c91..00000000 --- a/prism/examples/ctmdp/jsp.csl +++ /dev/null @@ -1 +0,0 @@ -"done" diff --git a/prism/examples/ctmdp/jsp.lab b/prism/examples/ctmdp/jsp.lab deleted file mode 100644 index 233d7f1d..00000000 --- a/prism/examples/ctmdp/jsp.lab +++ /dev/null @@ -1,3 +0,0 @@ -0="init" 1="deadlock" 2="done" -0: 0 -14: 2 diff --git a/prism/examples/ctmdp/jsp.sm b/prism/examples/ctmdp/jsp.sm deleted file mode 100644 index 8055fe8f..00000000 --- a/prism/examples/ctmdp/jsp.sm +++ /dev/null @@ -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; diff --git a/prism/examples/ctmdp/jsp.tra b/prism/examples/ctmdp/jsp.tra deleted file mode 100644 index 97ae218a..00000000 --- a/prism/examples/ctmdp/jsp.tra +++ /dev/null @@ -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 diff --git a/prism/examples/explicit/NOTES b/prism/examples/explicit/NOTES deleted file mode 100644 index a9cd3f37..00000000 --- a/prism/examples/explicit/NOTES +++ /dev/null @@ -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 - diff --git a/prism/examples/explicit/wlan/backoff.pctl b/prism/examples/explicit/wlan/backoff.pctl deleted file mode 100644 index ccc67871..00000000 --- a/prism/examples/explicit/wlan/backoff.pctl +++ /dev/null @@ -1 +0,0 @@ -Pmax=? [ F "bcmax" ] diff --git a/prism/examples/explicit/wlan/wlan.pctl b/prism/examples/explicit/wlan/wlan.pctl deleted file mode 100644 index 215441de..00000000 --- a/prism/examples/explicit/wlan/wlan.pctl +++ /dev/null @@ -1 +0,0 @@ -Pmax=? [ F "bcmax" ] diff --git a/prism/examples/explicit/wlan/wlan2.nm b/prism/examples/explicit/wlan/wlan2.nm deleted file mode 100644 index b95b0527..00000000 --- a/prism/examples/explicit/wlan/wlan2.nm +++ /dev/null @@ -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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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; diff --git a/prism/examples/explicit/wlan/wlan3.nm b/prism/examples/explicit/wlan/wlan3.nm deleted file mode 100644 index 90cd6d8a..00000000 --- a/prism/examples/explicit/wlan/wlan3.nm +++ /dev/null @@ -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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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; diff --git a/prism/examples/explicit/wlan/wlan4.nm b/prism/examples/explicit/wlan/wlan4.nm deleted file mode 100644 index 696426de..00000000 --- a/prism/examples/explicit/wlan/wlan4.nm +++ /dev/null @@ -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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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; diff --git a/prism/examples/explicit/wlan/wlan5.nm b/prism/examples/explicit/wlan/wlan5.nm deleted file mode 100644 index c584847d..00000000 --- a/prism/examples/explicit/wlan/wlan5.nm +++ /dev/null @@ -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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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; diff --git a/prism/examples/explicit/zeroconf/zeroconf.pctl b/prism/examples/explicit/zeroconf/zeroconf.pctl deleted file mode 100644 index 5717735c..00000000 --- a/prism/examples/explicit/zeroconf/zeroconf.pctl +++ /dev/null @@ -1 +0,0 @@ -Pmin=? [ F "done_correct" ] diff --git a/prism/examples/explicit/zeroconf/zeroconfN_M_K.nm.pp b/prism/examples/explicit/zeroconf/zeroconfN_M_K.nm.pp deleted file mode 100644 index 4f06baae..00000000 --- a/prism/examples/explicit/zeroconf/zeroconfN_M_K.nm.pp +++ /dev/null @@ -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 (x0'=x0+1); - // send a probe (not last probe) - [broadcast] s0=2 & x0=probe_time & probes (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 (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 (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 (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