TODO: * Get PrismSTPGAsbtractRefine working better on more examples * When PrismSTPGAsbtractRefine can reproduce QEST results, delete abstraction package exp reach for games remove src/abstraction dir other notes/ideas: refine opt: don't add ubsets of player1 choices #================================================ # Self-stabilisation (Israeli-Jalfon) #================================================ # Generate model files foreach N (3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20) prism examples/explicit/israeli-jalfon/ij$N.nm -exporttrans examples/explicit/israeli-jalfon/ij$N.tra -exportstates examples/explicit/israeli-jalfon/ij$N.sta -exportlabels examples/explicit/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 examples/explicit/israeli-jalfon/ij5.tra examples/explicit/israeli-jalfon/ij5.lab stable bin/prism-ar examples/explicit/israeli-jalfon/ij5.tra examples/explicit/israeli-jalfon/ij5.lab stable -nopre -opt # Abstraction refinement (value-based) #java AbstractIJInitial 10,examples/explicit/israeli-jalfon/ij10 -2 21 >! israeli-jalfon/ij10.-2.21.log #java AbstractIJInitial 12,examples/explicit/israeli-jalfon/ij12 -2 21 >! israeli-jalfon/ij12.-2.21.log java AbstractIJInitial 14,examples/explicit/israeli-jalfon/ij14 -2 21 >! israeli-jalfon/ij14.-2.21.log java AbstractIJInitial 16,examples/explicit/israeli-jalfon/ij16 -2 21 >! israeli-jalfon/ij16.-2.21.log java AbstractIJInitial 18,examples/explicit/israeli-jalfon/ij18 -2 21 >! israeli-jalfon/ij18.-2.21.log java -Xmx1500m AbstractIJInitial 20,examples/explicit/israeli-jalfon/ij20 -2 21 > israeli-jalfon/ij20.-2.21.log # Abstraction refinement (strategy-based) #java AbstractIJInitial 10,examples/explicit/israeli-jalfon/ij10 -2 20 >! israeli-jalfon/ij10.-2.20.log #java AbstractIJInitial 12,examples/explicit/israeli-jalfon/ij12 -2 20 >! israeli-jalfon/ij12.-2.20.log java AbstractIJInitial 14,examples/explicit/israeli-jalfon/ij14 -2 20 >! israeli-jalfon/ij14.-2.20.log java AbstractIJInitial 16,examples/explicit/israeli-jalfon/ij16 -2 20 >! israeli-jalfon/ij16.-2.20.log java AbstractIJInitial 18,examples/explicit/israeli-jalfon/ij18 -2 20 >! israeli-jalfon/ij18.-2.20.log java -Xmx1500m AbstractIJInitial 20,examples/explicit/israeli-jalfon/ij20 -2 20 > israeli-jalfon/ij20.-2.20.log #================================================ # Self-stabilisation (Beauquier) #================================================ # Generate model files foreach N (3 5 7 9 11) prism beauquier/beauquier$N.nm -exporttrans examples/explicit/beauquier/beauquier$N.tra -exportstates examples/explicit/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,examples/explicit/beauquier/beauquier$N -2 21 >! beauquier/beauquier$N.-2.21.log end java -Xmx1500m AbstractBeauquierInitial 11,examples/explicit/beauquier/beauquier11 -2 21 >! beauquier/beauquier11.-2.21.log # Abstraction refinement (strategy-based) foreach N (3 5 7 9) java AbstractBeauquierInitial $N,examples/explicit/beauquier/beauquier$N -2 20 >! beauquier/beauquier$N.-2.20.log end java -Xmx1500m AbstractBeauquierInitial 11,examples/explicit/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 examples/explicit/zeroconf-until/zeroconf4_32_4.tra -exportstates examples/explicit/zeroconf-until/zeroconf4_32_4.sta prism zeroconf-until/zeroconf4_64_4.nm -exporttrans examples/explicit/zeroconf-until/zeroconf4_64_4.tra -exportstates examples/explicit/zeroconf-until/zeroconf4_64_4.sta prism zeroconf-until/zeroconf4_128_4.nm -exporttrans examples/explicit/zeroconf-until/zeroconf4_128_4.tra -exportstates examples/explicit/zeroconf-until/zeroconf4_128_4.sta prism zeroconf-until/zeroconf6_32_4.nm -exporttrans examples/explicit/zeroconf-until/zeroconf6_32_4.tra -exportstates examples/explicit/zeroconf-until/zeroconf6_32_4.sta prism zeroconf-until/zeroconf6_64_4.nm -exporttrans examples/explicit/zeroconf-until/zeroconf6_64_4.tra -exportstates examples/explicit/zeroconf-until/zeroconf6_64_4.sta prism zeroconf-until/zeroconf6_128_4.nm -exporttrans examples/explicit/zeroconf-until/zeroconf6_128_4.tra -exportstates examples/explicit/zeroconf-until/zeroconf6_128_4.sta prism zeroconf-until/zeroconf8_32_4.nm -exporttrans examples/explicit/zeroconf-until/zeroconf8_32_4.tra -exportstates examples/explicit/zeroconf-until/zeroconf8_32_4.sta prism zeroconf-until/zeroconf8_64_4.nm -exporttrans examples/explicit/zeroconf-until/zeroconf8_64_4.tra -exportstates examples/explicit/zeroconf-until/zeroconf8_64_4.sta prism zeroconf-until/zeroconf8_128_4.nm -exporttrans examples/explicit/zeroconf-until/zeroconf8_128_4.tra -exportstates examples/explicit/zeroconf-until/zeroconf8_128_4.sta # Abstraction refinement (value-based, opt) java AbstractZeroconfInitial 4,32,4,examples/explicit/zeroconf-until/zeroconf4_32_4,until -1 21 -opt >! zeroconf-until/zeroconf4_32.21.opt.log java AbstractZeroconfInitial 4,64,4,examples/explicit/zeroconf-until/zeroconf4_64_4,until -1 21 -opt >! zeroconf-until/zeroconf4_64.21.opt.log java AbstractZeroconfInitial 4,128,4,examples/explicit/zeroconf-until/zeroconf4_128_4,until -1 21 -opt >! zeroconf-until/zeroconf4_128.21.opt.log java AbstractZeroconfInitial 6,32,4,examples/explicit/zeroconf-until/zeroconf6_32_4,until -1 21 -opt >! zeroconf-until/zeroconf6_32.21.opt.log java AbstractZeroconfInitial 6,64,4,examples/explicit/zeroconf-until/zeroconf6_64_4,until -1 21 -opt >! zeroconf-until/zeroconf6_64.21.opt.log java AbstractZeroconfInitial 6,128,4,examples/explicit/zeroconf-until/zeroconf6_128_4,until -1 21 -opt >! zeroconf-until/zeroconf6_128.21.opt.log java AbstractZeroconfInitial 8,32,4,examples/explicit/zeroconf-until/zeroconf8_32_4,until -1 21 -opt >! zeroconf-until/zeroconf8_32.21.opt.log java AbstractZeroconfInitial 8,64,4,examples/explicit/zeroconf-until/zeroconf8_64_4,until -1 21 -opt >! zeroconf-until/zeroconf8_64.21.opt.log java AbstractZeroconfInitial 8,128,4,examples/explicit/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,examples/explicit/zeroconf-until/zeroconf4_32_4,until -1 21 -noopt >! zeroconf-until/zeroconf4_32.21.noopt.log java AbstractZeroconfInitial 4,64,4,examples/explicit/zeroconf-until/zeroconf4_64_4,until -1 21 -noopt >! zeroconf-until/zeroconf4_64.21.noopt.log java AbstractZeroconfInitial 4,128,4,examples/explicit/zeroconf-until/zeroconf4_128_4,until -1 21 -noopt >! zeroconf-until/zeroconf4_128.21.noopt.log java AbstractZeroconfInitial 6,32,4,examples/explicit/zeroconf-until/zeroconf6_32_4,until -1 21 -noopt >! zeroconf-until/zeroconf6_32.21.noopt.log java AbstractZeroconfInitial 6,64,4,examples/explicit/zeroconf-until/zeroconf6_64_4,until -1 21 -noopt >! zeroconf-until/zeroconf6_64.21.noopt.log java AbstractZeroconfInitial 6,128,4,examples/explicit/zeroconf-until/zeroconf6_128_4,until -1 21 -noopt >! zeroconf-until/zeroconf6_128.21.noopt.log java AbstractZeroconfInitial 8,32,4,examples/explicit/zeroconf-until/zeroconf8_32_4,until -1 21 -noopt >! zeroconf-until/zeroconf8_32.21.noopt.log java AbstractZeroconfInitial 8,64,4,examples/explicit/zeroconf-until/zeroconf8_64_4,until -1 21 -noopt >! zeroconf-until/zeroconf8_64.21.noopt.log java AbstractZeroconfInitial 8,128,4,examples/explicit/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,examples/explicit/zeroconf-until/zeroconf4_32_4,until -1 20 -opt >! zeroconf-until/zeroconf4_32.20.opt.log java AbstractZeroconfInitial 4,64,4,examples/explicit/zeroconf-until/zeroconf4_64_4,until -1 20 -opt >! zeroconf-until/zeroconf4_64.20.opt.log java AbstractZeroconfInitial 4,128,4,examples/explicit/zeroconf-until/zeroconf4_128_4,until -1 20 -opt >! zeroconf-until/zeroconf4_128.20.opt.log java AbstractZeroconfInitial 6,32,4,examples/explicit/zeroconf-until/zeroconf6_32_4,until -1 20 -opt >! zeroconf-until/zeroconf6_32.20.opt.log java AbstractZeroconfInitial 6,64,4,examples/explicit/zeroconf-until/zeroconf6_64_4,until -1 20 -opt >! zeroconf-until/zeroconf6_64.20.opt.log java AbstractZeroconfInitial 6,128,4,examples/explicit/zeroconf-until/zeroconf6_128_4,until -1 20 -opt >! zeroconf-until/zeroconf6_128.20.opt.log java AbstractZeroconfInitial 8,32,4,examples/explicit/zeroconf-until/zeroconf8_32_4,until -1 20 -opt >! zeroconf-until/zeroconf8_32.20.opt.log java AbstractZeroconfInitial 8,64,4,examples/explicit/zeroconf-until/zeroconf8_64_4,until -1 20 -opt >! zeroconf-until/zeroconf8_64.20.opt.log java AbstractZeroconfInitial 8,128,4,examples/explicit/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,examples/explicit/zeroconf-until/zeroconf4_32_4,until -1 20 -noopt >! zeroconf-until/zeroconf4_32.20.noopt.log java AbstractZeroconfInitial 4,64,4,examples/explicit/zeroconf-until/zeroconf4_64_4,until -1 20 -noopt >! zeroconf-until/zeroconf4_64.20.noopt.log java AbstractZeroconfInitial 4,128,4,examples/explicit/zeroconf-until/zeroconf4_128_4,until -1 20 -noopt >! zeroconf-until/zeroconf4_128.20.noopt.log java AbstractZeroconfInitial 6,32,4,examples/explicit/zeroconf-until/zeroconf6_32_4,until -1 20 -noopt >! zeroconf-until/zeroconf6_32.20.noopt.log java AbstractZeroconfInitial 6,64,4,examples/explicit/zeroconf-until/zeroconf6_64_4,until -1 20 -noopt >! zeroconf-until/zeroconf6_64.20.noopt.log java AbstractZeroconfInitial 6,128,4,examples/explicit/zeroconf-until/zeroconf6_128_4,until -1 20 -noopt >! zeroconf-until/zeroconf6_128.20.noopt.log java AbstractZeroconfInitial 8,32,4,examples/explicit/zeroconf-until/zeroconf8_32_4,until -1 20 -noopt >! zeroconf-until/zeroconf8_32.20.noopt.log java AbstractZeroconfInitial 8,64,4,examples/explicit/zeroconf-until/zeroconf8_64_4,until -1 20 -noopt >! zeroconf-until/zeroconf8_64.20.noopt.log java AbstractZeroconfInitial 8,128,4,examples/explicit/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/examples/explicit/until/zeroconf4_128_4,until -1 21 -opt >! zeroconf/until/zeroconf4_128.21.opt.log java AbstractZeroconfInitial 4,32,4,zeroconf/examples/explicit/until/zeroconf4_32_4,until -1 21 -noopt >! zeroconf/until/zeroconf4_32.21.noopt.log java AbstractZeroconfInitial 4,64,4,zeroconf/examples/explicit/until/zeroconf4_64_4,until -1 21 -noopt >! zeroconf/until/zeroconf4_64.21.noopt.log java AbstractZeroconfInitial 4,128,4,zeroconf/examples/explicit/until/zeroconf4_128_4,until -1 21 -noopt >! zeroconf/until/zeroconf4_128.21.noopt.log java AbstractZeroconfInitial 6,32,4,zeroconf/examples/explicit/until/zeroconf6_32_4,until -1 21 -opt >! zeroconf/until/zeroconf6_32.21.opt.log java AbstractZeroconfInitial 6,64,4,zeroconf/examples/explicit/until/zeroconf6_64_4,until -1 21 -opt >! zeroconf/until/zeroconf6_64.21.opt.log java AbstractZeroconfInitial 6,128,4,zeroconf/examples/explicit/until/zeroconf6_128_4,until -1 21 -opt >! zeroconf/until/zeroconf6_128.21.opt.log java AbstractZeroconfInitial 6,32,4,zeroconf/examples/explicit/until/zeroconf6_32_4,until -1 21 -noopt >! zeroconf/until/zeroconf6_32.21.noopt.log java AbstractZeroconfInitial 6,64,4,zeroconf/examples/explicit/until/zeroconf6_64_4,until -1 21 -noopt >! zeroconf/until/zeroconf6_64.21.noopt.log java AbstractZeroconfInitial 6,128,4,zeroconf/examples/explicit/until/zeroconf6_128_4,until -1 21 -noopt >! zeroconf/until/zeroconf6_128.21.noopt.log java AbstractZeroconfInitial 6,32,4,zeroconf/examples/explicit/until/zeroconf6_32_4,until -1 20 -opt >! zeroconf/until/zeroconf6_32.20.opt.log java AbstractZeroconfInitial 6,64,4,zeroconf/examples/explicit/until/zeroconf6_64_4,until -1 20 -opt >! zeroconf/until/zeroconf6_64.20.opt.log java AbstractZeroconfInitial 6,128,4,zeroconf/examples/explicit/until/zeroconf6_128_4,until -1 20 -opt >! zeroconf/until/zeroconf6_128.20.opt.log java AbstractZeroconfInitial 6,32,4,zeroconf/examples/explicit/until/zeroconf6_32_4,until -1 20 -noopt >! zeroconf/until/zeroconf6_32.20.noopt.log java AbstractZeroconfInitial 6,64,4,zeroconf/examples/explicit/until/zeroconf6_64_4,until -1 20 -noopt >! zeroconf/until/zeroconf6_64.20.noopt.log java AbstractZeroconfInitial 6,128,4,zeroconf/examples/explicit/until/zeroconf6_128_4,until -1 20 -noopt >! zeroconf/until/zeroconf6_128.20.noopt.log java AbstractZeroconfInitial 8,32,4,zeroconf/examples/explicit/until/zeroconf8_32_4,until -1 21 -opt >! zeroconf/until/zeroconf8_32.21.opt.log java AbstractZeroconfInitial 8,64,4,zeroconf/examples/explicit/until/zeroconf8_64_4,until -1 21 -opt >! zeroconf/until/zeroconf8_64.21.opt.log java AbstractZeroconfInitial 8,128,4,zeroconf/examples/explicit/until/zeroconf8_128_4,until -1 21 -opt >! zeroconf/until/zeroconf8_128.21.opt.log java AbstractZeroconfInitial 8,32,4,zeroconf/examples/explicit/until/zeroconf8_32_4,until -1 21 -noopt >! zeroconf/until/zeroconf8_32.21.noopt.log java AbstractZeroconfInitial 8,64,4,zeroconf/examples/explicit/until/zeroconf8_64_4,until -1 21 -noopt >! zeroconf/until/zeroconf8_64.21.noopt.log java AbstractZeroconfInitial 8,128,4,zeroconf/examples/explicit/until/zeroconf8_128_4,until -1 21 -noopt >! zeroconf/until/zeroconf8_128.21.noopt.log java AbstractZeroconfInitial 8,32,4,zeroconf/examples/explicit/until/zeroconf8_32_4,until -1 20 -opt >! zeroconf/until/zeroconf8_32.20.opt.log java AbstractZeroconfInitial 8,64,4,zeroconf/examples/explicit/until/zeroconf8_64_4,until -1 20 -opt >! zeroconf/until/zeroconf8_64.20.opt.log java AbstractZeroconfInitial 8,128,4,zeroconf/examples/explicit/until/zeroconf8_128_4,until -1 20 -opt >! zeroconf/until/zeroconf8_128.20.opt.log java AbstractZeroconfInitial 8,32,4,zeroconf/examples/explicit/until/zeroconf8_32_4,until -1 20 -noopt >! zeroconf/until/zeroconf8_32.20.noopt.log java AbstractZeroconfInitial 8,64,4,zeroconf/examples/explicit/until/zeroconf8_64_4,until -1 20 -noopt >! zeroconf/until/zeroconf8_64.20.noopt.log java AbstractZeroconfInitial 8,128,4,zeroconf/examples/explicit/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 examples/explicit/zeroconf-bounded_until/zeroconf4_$T.tra -exportstates examples/explicit/zeroconf-bounded_until/zeroconf4_$T.sta prism zeroconf-bounded_until/zeroconf8.nm -const K=4,T=$T -exporttrans examples/explicit/zeroconf-bounded_until/zeroconf8_$T.tra -exportstates examples/explicit/zeroconf-bounded_until/zeroconf8_$T.sta end foreach T (60 80) java AbstractZeroconfInitial 4,32,4,examples/explicit/zeroconf-bounded_until/zeroconf4_$T,buntil,$T -1 21 end java AbstractZeroconf 4,32,4,examples/explicit/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 examples/explicit/leader-async/leader$N.sta -exporttrans examples/explicit/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,examples/explicit/leader-async/leader$N 100 21 >! leader-async/leader$N.100.21.log end foreach N (3 4 5 6 7) java AbstractLeaderInitial $N,examples/explicit/leader-async/leader$N 100 20 >! leader-async/leader$N.100.20.log end # unbounded #java AbstractLeaderInitial $N,examples/explicit/leader-async/leader$N -1 20 >! leader-async/leader$N.-1.21.log #java AbstractLeaderInitial $N,examples/explicit/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 examples/explicit/firewire/impl3.sta -exporttrans examples/explicit/firewire/impl3.tra prism firewire/impl.nm -const delay=6,fast=0.5 -exportstates examples/explicit/firewire/impl6.sta -exporttrans examples/explicit/firewire/impl6.tra prism firewire/impl.nm -const delay=12,fast=0.5 -exportstates examples/explicit/firewire/impl12.sta -exporttrans examples/explicit/firewire/impl12.tra prism firewire/impl.nm -const delay=24,fast=0.5 -exportstates examples/explicit/firewire/impl24.sta -exporttrans examples/explicit/firewire/impl24.tra prism firewire/impl.nm -const delay=36,fast=0.5 -exportstates examples/explicit/firewire/impl36.sta -exporttrans examples/explicit/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 examples/explicit/firewire/impl3 -2 21 -opt >! firewire/impl3.-2.21.opt.log java AbstractFirewireInitial examples/explicit/firewire/impl6 -2 21 -opt >! firewire/impl6.-2.21.opt.log java AbstractFirewireInitial examples/explicit/firewire/impl12 -2 21 -opt >! firewire/impl12.-2.21.opt.log java -Xmx1500m AbstractFirewireInitial examples/explicit/firewire/impl24 -2 21 -opt >! firewire/impl24.-2.21.opt.log java -Xmx1500m AbstractFirewireInitial examples/explicit/firewire/impl36 -2 21 -opt >! firewire/impl36.-2.21.opt.log # Abstraction refinement (value-based, noopt) java AbstractFirewireInitial examples/explicit/firewire/impl3 -2 21 -noopt >! firewire/impl3.-2.21.noopt.log java AbstractFirewireInitial examples/explicit/firewire/impl6 -2 21 -noopt >! firewire/impl6.-2.21.noopt.log java AbstractFirewireInitial examples/explicit/firewire/impl12 -2 21 -noopt >! firewire/impl12.-2.21.noopt.log java -Xmx1500m AbstractFirewireInitial examples/explicit/firewire/impl24 -2 21 -noopt >! firewire/impl24.-2.21.noopt.log java -Xmx1500m AbstractFirewireInitial examples/explicit/firewire/impl36 -2 21 -noopt >! firewire/impl36.-2.21.noopt.log # Abstraction refinement (strategy-based, opt) java AbstractFirewireInitial examples/explicit/firewire/impl3 -2 20 -opt >! firewire/impl3.-2.20.opt.log java AbstractFirewireInitial examples/explicit/firewire/impl6 -2 20 -opt >! firewire/impl6.-2.20.opt.log java AbstractFirewireInitial examples/explicit/firewire/impl12 -2 20 -opt >! firewire/impl12.-2.20.opt.log java -Xmx1500m AbstractFirewireInitial examples/explicit/firewire/impl24 -2 20 -opt >! firewire/impl24.-2.20.opt.log java -Xmx1500m AbstractFirewireInitial examples/explicit/firewire/impl36 -2 20 -opt >! firewire/impl36.-2.20.opt.log # Abstraction refinement (strategy-based, noopt) java AbstractFirewireInitial examples/explicit/firewire/impl3 -2 20 -noopt >! firewire/impl3.-2.20.noopt.log java AbstractFirewireInitial examples/explicit/firewire/impl6 -2 20 -noopt >! firewire/impl6.-2.20.noopt.log java AbstractFirewireInitial examples/explicit/firewire/impl12 -2 20 -noopt >! firewire/impl12.-2.20.noopt.log java -Xmx1500m AbstractFirewireInitial examples/explicit/firewire/impl24 -2 20 -noopt >! firewire/impl24.-2.20.noopt.log java -Xmx1500m AbstractFirewireInitial examples/explicit/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 examples/explicit/wlan/wlan3_10.sta -exporttrans examples/explicit/wlan/wlan3_10.tra prism wlan/wlan5.nm -const TRANS_TIME_MAX=10 -fixdl -exportstates examples/explicit/wlan/wlan5_10.sta -exporttrans examples/explicit/wlan/wlan5_10.tra prism wlan/wlan3.nm -const TRANS_TIME_MAX=316 -fixdl -exportstates examples/explicit/wlan/wlan3_316.sta -exporttrans examples/explicit/wlan/wlan3_316.tra prism wlan/wlan5.nm -const TRANS_TIME_MAX=316 -fixdl -exportstates examples/explicit/wlan/wlan5_316.sta -exporttrans examples/explicit/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,examples/explicit/wlan/wlan3_10 -1 21 -opt >! wlan/wlan3_10.-1.21.opt.log java AbstractWlanProbInitial 5,examples/explicit/wlan/wlan5_10 -1 21 -opt >! wlan/wlan5_10.-1.21.opt.log java AbstractWlanProbInitial 3,examples/explicit/wlan/wlan3_316 -1 21 -opt >! wlan/wlan3_316.-1.21.opt.log java AbstractWlanProbInitial 5,examples/explicit/wlan/wlan5_316 -1 21 -opt >! wlan/wlan5_316.-1.21.opt.log # Abstraction refinement (value-based, noopt) java AbstractWlanProbInitial 2,examples/explicit/wlan/wlan2_10 -1 21 -noopt >! wlan/wlan2_10.-1.21.noopt.log java AbstractWlanProbInitial 3,examples/explicit/wlan/wlan3_10 -1 21 -noopt >! wlan/wlan3_10.-1.21.noopt.log java AbstractWlanProbInitial 4,examples/explicit/wlan/wlan4_10 -1 21 -noopt >! wlan/wlan4_316.-1.21.noopt.log java AbstractWlanProbInitial 5,examples/explicit/wlan/wlan5_10 -1 21 -noopt >! wlan/wlan5_316.-1.21.noopt.log # Abstraction refinement (strategy-based) java AbstractWlanProbInitial 2,examples/explicit/wlan/wlan2_10 -1 20 -noopt >! wlan/wlan2_10.-1.20.noopt.log java AbstractWlanProbInitial 3,examples/explicit/wlan/wlan3_10 -1 20 -noopt >! wlan/wlan3_10.-1.20.noopt.log java AbstractWlanProbInitial 4,examples/explicit/wlan/wlan4_10 -1 20 -noopt >! wlan/wlan4_10.-1.20.noopt.log java AbstractWlanProbInitial 5,examples/explicit/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 examples/explicit/csma/csma2.tra -exportstates examples/explicit/csma/csma2.sta prism csma/csma.nm -const K=3 -exporttrans examples/explicit/csma/csma3.tra -exportstates examples/explicit/csma/csma3.sta prism csma/csma.nm -const K=4 -exporttrans examples/explicit/csma/csma4.tra -exportstates examples/explicit/csma/csma4.sta prism csma/csma.nm -const K=5 -exporttrans examples/explicit/csma/csma5.tra -exportstates examples/explicit/csma/csma5.sta prism csma/csma.nm -const K=6 -exporttrans examples/explicit/csma/csma6.tra -exportstates examples/explicit/csma/csma6.sta prism csma/csma.nm -const K=7 -exporttrans examples/explicit/csma/csma7.tra -exportstates examples/explicit/csma/csma7.sta prism csma/csma.nm -const K=8 -exporttrans examples/explicit/csma/csma8.tra -exportstates examples/explicit/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,examples/explicit/csma/csma2 -1 21 -opt >! csma/csma2.-1.21.opt.log java AbstractCsmaProbInitial 3,examples/explicit/csma/csma3 -1 21 -opt >! csma/csma3.-1.21.opt.log java AbstractCsmaProbInitial 4,examples/explicit/csma/csma4 -1 21 -opt >! csma/csma4.-1.21.opt.log java AbstractCsmaProbInitial 5,examples/explicit/csma/csma5 -1 21 -opt >! csma/csma5.-1.21.opt.log java -Xmx1500m AbstractCsmaProbInitial 6,examples/explicit/csma/csma6 -1 21 -opt >! csma/csma6.-1.21.opt.log java -Xmx1500m AbstractCsmaProbInitial 7,examples/explicit/csma/csma7 -1 21 -opt >! csma/csma7.-1.21.opt.log java -Xmx1500m AbstractCsmaProbInitial 8,examples/explicit/csma/csma8 -1 21 -opt >! csma/csma8.-1.21.opt.log # Abstraction refinement (value-based, noopt) java AbstractCsmaProbInitial 2,examples/explicit/csma/csma2 -1 21 -noopt >! csma/csma2.-1.21.noopt.log java AbstractCsmaProbInitial 3,examples/explicit/csma/csma3 -1 21 -noopt >! csma/csma3.-1.21.noopt.log java AbstractCsmaProbInitial 4,examples/explicit/csma/csma4 -1 21 -noopt >! csma/csma4.-1.21.noopt.log java AbstractCsmaProbInitial 5,examples/explicit/csma/csma5 -1 21 -noopt >! csma/csma5.-1.21.noopt.log java -Xmx1500m AbstractCsmaProbInitial 6,examples/explicit/csma/csma6 -1 21 -noopt >! csma/csma6.-1.21.noopt.log java -Xmx1500m AbstractCsmaProbInitial 7,examples/explicit/csma/csma7 -1 21 -noopt >! csma/csma7.-1.21.noopt.log java -Xmx1500m AbstractCsmaProbInitial 8,examples/explicit/csma/csma8 -1 21 -noopt >! csma/csma8.-1.21.noopt.log # Abstraction refinement (strategy-based, opt) java AbstractCsmaProbInitial 2,examples/explicit/csma/csma2 -1 20 -opt >! csma/csma2.-1.20.opt.log java AbstractCsmaProbInitial 3,examples/explicit/csma/csma3 -1 20 -opt >! csma/csma3.-1.20.opt.log java AbstractCsmaProbInitial 4,examples/explicit/csma/csma4 -1 20 -opt >! csma/csma4.-1.20.opt.log java AbstractCsmaProbInitial 5,examples/explicit/csma/csma5 -1 20 -opt >! csma/csma5.-1.20.opt.log java -Xmx1500m AbstractCsmaProbInitial 6,examples/explicit/csma/csma6 -1 20 -opt >! csma/csma6.-1.20.opt.log java -Xmx1500m AbstractCsmaProbInitial 7,examples/explicit/csma/csma7 -1 20 -opt >! csma/csma7.-1.20.opt.log java -Xmx1500m AbstractCsmaProbInitial 8,examples/explicit/csma/csma8 -1 20 -opt >! csma/csma8.-1.20.opt.log # Abstraction refinement (strategy-based, noopt) java AbstractCsmaProbInitial 2,examples/explicit/csma/csma2 -1 20 -noopt >! csma/csma2.-1.20.noopt.log java AbstractCsmaProbInitial 3,examples/explicit/csma/csma3 -1 20 -noopt >! csma/csma3.-1.20.noopt.log java AbstractCsmaProbInitial 4,examples/explicit/csma/csma4 -1 20 -noopt >! csma/csma4.-1.20.noopt.log java AbstractCsmaProbInitial 5,examples/explicit/csma/csma5 -1 20 -noopt >! csma/csma5.-1.20.noopt.log java -Xmx1500m AbstractCsmaProbInitial 6,examples/explicit/csma/csma6 -1 20 -noopt >! csma/csma6.-1.20.noopt.log java -Xmx1500m AbstractCsmaProbInitial 7,examples/explicit/csma/csma7 -1 20 -noopt >! csma/csma7.-1.20.noopt.log java -Xmx1500m AbstractCsmaProbInitial 8,examples/explicit/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 examples/explicit/brp/brp$N_"$MAX".sta -exporttrans examples/explicit/brp/brp$N_"$MAX".tra end end foreach N (16 32 64) foreach MAX (2 3 4 5) java AbstractBRPInitial examples/explicit/brp/brp$N_"$MAX" -1 21 >! brp/brp$N_"$MAX".-1.21.log java AbstractBRPInitial examples/explicit/brp/brp$N_"$MAX" -1 20 >! brp/brp$N_"$MAX".-1.20.log end end #================================================ # Consensus #================================================ java AbstractConsensusInitial 5,2,examples/explicit/consensus/consensus5_2 -2 20 >! consensus/consensus5.2.-1.20.log java AbstractConsensusInitial 5,4,examples/explicit/consensus/consensus5_4 -2 20 >! consensus/consensus5.4.-1.20.log java AbstractConsensusInitial 5,8,examples/explicit/consensus/consensus5_8 -2 20 >! consensus/consensus5.8.-1.20.log java AbstractConsensusInitial 5,16,examples/explicit/consensus/consensus5_16 -2 20 >! consensus/consensus5.16.-1.20.log java AbstractConsensusInitial 5,2,examples/explicit/consensus/consensus5_2 -2 21 -noopt >! consensus/consensus5.2.-1.21.noopt.log java AbstractConsensusInitial 5,4,examples/explicit/consensus/consensus5_4 -2 21 -noopt >! consensus/consensus5.4.-1.21.noopt.log java AbstractConsensusInitial 5,8,examples/explicit/consensus/consensus5_8 -2 21 -noopt >! consensus/consensus5.8.-1.21.noopt.log java AbstractConsensusInitial 5,16,examples/explicit/consensus/consensus5_16 -2 21 -noopt >! consensus/consensus5.16.-1.21.noopt.log java AbstractConsensusInitial 5,2,examples/explicit/consensus/consensus5_2 -2 20 -noopt >! consensus/consensus5.2.-1.20.noopt.log java AbstractConsensusInitial 5,4,examples/explicit/consensus/consensus5_4 -2 20 -noopt >! consensus/consensus5.4.-1.20.noopt.log java AbstractConsensusInitial 5,8,examples/explicit/consensus/consensus5_8 -2 20 -noopt >! consensus/consensus5.8.-1.20.noopt.log java AbstractConsensusInitial 5,16,examples/explicit/consensus/consensus5_16 -2 20 -noopt >! consensus/consensus5.16.-1.20.noopt.log