From 43fd084221add1167dcd4fbe71f0cf75c3c39cc9 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 26 Feb 2010 22:03:47 +0000 Subject: [PATCH] Some abstraction examples. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1774 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/NOTES-ABSTR | 1 - prism/examples/explicit/NOTES | 514 ++++++++++++++++++ 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 ++++++ 10 files changed, 1870 insertions(+), 1 deletion(-) create mode 100644 prism/examples/explicit/NOTES create mode 100644 prism/examples/explicit/wlan/backoff.pctl create mode 100644 prism/examples/explicit/wlan/wlan.pctl create mode 100644 prism/examples/explicit/wlan/wlan2.nm create mode 100644 prism/examples/explicit/wlan/wlan3.nm create mode 100644 prism/examples/explicit/wlan/wlan4.nm create mode 100644 prism/examples/explicit/wlan/wlan5.nm create mode 100644 prism/examples/explicit/zeroconf/zeroconf.pctl create mode 100644 prism/examples/explicit/zeroconf/zeroconfN_M_K.nm.pp diff --git a/prism/NOTES-ABSTR b/prism/NOTES-ABSTR index 8deb3797..0f54c96f 100644 --- a/prism/NOTES-ABSTR +++ b/prism/NOTES-ABSTR @@ -5,7 +5,6 @@ TODO: exp reach for games -remove src/abstraction dir other notes/ideas: diff --git a/prism/examples/explicit/NOTES b/prism/examples/explicit/NOTES new file mode 100644 index 00000000..967d53da --- /dev/null +++ b/prism/examples/explicit/NOTES @@ -0,0 +1,514 @@ +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 + +# 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 +foreach N (3 5 7 9 11 13 15 17 19) + prism herman/herman$N.pm -exporttrans herman/herman$N.tra -exportlabels herman/herman$N.lab +end + +# Model check in PRISM +foreach N (3 5 7 9 11 13 15 17 19) + # time-bounded + prism herman/herman$N.pm -pctl 'const int k; P=?[F<=k "stable"]' -const k=5 +end + +# Abstraction refinement + # time-bounded + prism-ar herman/herman5 stable -dtmc -probreachbnd=5 -nopre -noopt + +prism herman/herman5.pm herman/herman.pctl -prop 2 + + prism-ar herman/herman5 stable -dtmc -nopre -noopt + + +#================================================ +# 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 + +-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-ar fgf/sprouty cause1 -ctmc -nopre -noopt + + prism-ar 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 new file mode 100644 index 00000000..ccc67871 --- /dev/null +++ b/prism/examples/explicit/wlan/backoff.pctl @@ -0,0 +1 @@ +Pmax=? [ F "bcmax" ] diff --git a/prism/examples/explicit/wlan/wlan.pctl b/prism/examples/explicit/wlan/wlan.pctl new file mode 100644 index 00000000..215441de --- /dev/null +++ b/prism/examples/explicit/wlan/wlan.pctl @@ -0,0 +1 @@ +Pmax=? [ F "bcmax" ] diff --git a/prism/examples/explicit/wlan/wlan2.nm b/prism/examples/explicit/wlan/wlan2.nm new file mode 100644 index 00000000..b95b0527 --- /dev/null +++ b/prism/examples/explicit/wlan/wlan2.nm @@ -0,0 +1,270 @@ +// 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 new file mode 100644 index 00000000..90cd6d8a --- /dev/null +++ b/prism/examples/explicit/wlan/wlan3.nm @@ -0,0 +1,281 @@ +// 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 new file mode 100644 index 00000000..696426de --- /dev/null +++ b/prism/examples/explicit/wlan/wlan4.nm @@ -0,0 +1,300 @@ +// 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 new file mode 100644 index 00000000..c584847d --- /dev/null +++ b/prism/examples/explicit/wlan/wlan5.nm @@ -0,0 +1,336 @@ +// 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 new file mode 100644 index 00000000..5717735c --- /dev/null +++ b/prism/examples/explicit/zeroconf/zeroconf.pctl @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..4f06baae --- /dev/null +++ b/prism/examples/explicit/zeroconf/zeroconfN_M_K.nm.pp @@ -0,0 +1,166 @@ +#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