Browse Source
Removed (old) abstraction package.
Removed (old) abstraction package.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1861 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Dave Parker
17 years ago
10 changed files with 5 additions and 1810 deletions
-
6prism/Makefile
-
435prism/NOTES-ABSTR
-
351prism/src/abstraction/AbstractMDP.java
-
553prism/src/abstraction/AbstractRefine.java
-
73prism/src/abstraction/AbstractState.java
-
34prism/src/abstraction/Makefile
-
71prism/src/abstraction/PRISMAbstraction.java
-
82prism/src/abstraction/examples/Firewire.java
-
80prism/src/abstraction/examples/IJ.java
-
130prism/src/abstraction/examples/IJManual.java
@ -1,435 +0,0 @@ |
|||||
TODO: |
|
||||
|
|
||||
* Get PrismSTPGAsbtractRefine working better on more examples |
|
||||
* When PrismSTPGAsbtractRefine can reproduce QEST results, delete abstraction package |
|
||||
|
|
||||
|
|
||||
exp reach for games |
|
||||
|
|
||||
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 |
|
||||
|
|
||||
@ -1,351 +0,0 @@ |
|||||
//============================================================================== |
|
||||
// |
|
||||
// Copyright (c) 2002- |
|
||||
// Authors: |
|
||||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford) |
|
||||
// |
|
||||
//------------------------------------------------------------------------------ |
|
||||
// |
|
||||
// This file is part of PRISM. |
|
||||
// |
|
||||
// PRISM is free software; you can redistribute it and/or modify |
|
||||
// it under the terms of the GNU General Public License as published by |
|
||||
// the Free Software Foundation; either version 2 of the License, or |
|
||||
// (at your option) any later version. |
|
||||
// |
|
||||
// PRISM is distributed in the hope that it will be useful, |
|
||||
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
|
||||
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
|
||||
// GNU General Public License for more details. |
|
||||
// |
|
||||
// You should have received a copy of the GNU General Public License |
|
||||
// along with PRISM; if not, write to the Free Software Foundation, |
|
||||
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
|
||||
// |
|
||||
//============================================================================== |
|
||||
|
|
||||
package abstraction; |
|
||||
|
|
||||
import java.io.BufferedReader; |
|
||||
import java.io.File; |
|
||||
import java.io.FileReader; |
|
||||
import java.io.FileWriter; |
|
||||
import java.io.IOException; |
|
||||
import java.util.ArrayList; |
|
||||
import java.util.Arrays; |
|
||||
import java.util.HashMap; |
|
||||
import java.util.HashSet; |
|
||||
import java.util.Iterator; |
|
||||
import java.util.List; |
|
||||
import java.util.Set; |
|
||||
import java.util.TreeSet; |
|
||||
import explicit.*; |
|
||||
|
|
||||
public class AbstractMDP |
|
||||
{ |
|
||||
public int nConcrete; |
|
||||
public int nAbstract; |
|
||||
public int nnzConcrete; |
|
||||
public int nnzAbstract; |
|
||||
public int mapping[] = null; |
|
||||
public int initialConcreteState; |
|
||||
public int initialAbstractState; |
|
||||
public boolean target[]; |
|
||||
public TreeSet states; |
|
||||
public List statesList; |
|
||||
public ArrayList<List> mdp; |
|
||||
public ArrayList<List> mdpStates; |
|
||||
|
|
||||
protected long timer; |
|
||||
|
|
||||
public long getLastTimer() |
|
||||
{ |
|
||||
return timer; |
|
||||
} |
|
||||
|
|
||||
/* Build the abstract state space */ |
|
||||
|
|
||||
public void buildAbstractStateSpace(PRISMAbstraction abstr) |
|
||||
{ |
|
||||
BufferedReader in; |
|
||||
FileWriter out; |
|
||||
String s, ss[]; |
|
||||
int i, j, numVars = 0, vars[]; |
|
||||
AbstractState state; |
|
||||
|
|
||||
// start timer |
|
||||
timer = System.currentTimeMillis(); |
|
||||
|
|
||||
try { |
|
||||
states = new TreeSet(); |
|
||||
nConcrete = 0; |
|
||||
|
|
||||
// first pass of states file - build abstract state space |
|
||||
|
|
||||
System.out.println("Computing abstract states..."); |
|
||||
in = new BufferedReader(new FileReader(new File(abstr.filename + ".sta"))); |
|
||||
s = in.readLine(); |
|
||||
if (s != null) { |
|
||||
s = s.substring(1, s.length() - 1); |
|
||||
ss = s.split(","); |
|
||||
numVars = ss.length; |
|
||||
} |
|
||||
s = in.readLine(); |
|
||||
while (s != null) { |
|
||||
s = s.substring(s.indexOf(":") + 2, s.indexOf(")")); |
|
||||
ss = s.split(","); |
|
||||
vars = new int[numVars]; |
|
||||
for (j = 0; j < numVars; j++) { |
|
||||
try { |
|
||||
vars[j] = Integer.parseInt(ss[j]); |
|
||||
} catch (NumberFormatException e) { |
|
||||
if (ss[j].equals("false")) |
|
||||
vars[j] = 0; |
|
||||
else { |
|
||||
if (ss[j].equals("true")) |
|
||||
vars[j] = 1; |
|
||||
else |
|
||||
throw e; |
|
||||
} |
|
||||
} |
|
||||
} |
|
||||
state = abstr.concreteToAbstract(vars); |
|
||||
states.add(state); |
|
||||
nConcrete++; |
|
||||
s = in.readLine(); |
|
||||
} |
|
||||
in.close(); |
|
||||
nAbstract = states.size(); |
|
||||
|
|
||||
System.out.println("Concrete states: " + nConcrete); |
|
||||
System.out.println("Abstract states: " + nAbstract); |
|
||||
|
|
||||
// Convert states list to array |
|
||||
statesList = Arrays.asList(states.toArray()); |
|
||||
|
|
||||
// output abstract state space to file |
|
||||
/* |
|
||||
* System.out.println("Sending abstract state space to file..."); out = new FileWriter(new |
|
||||
* File(filename+".abs.sta")); s = "(" + abstractVarsString() + ")\n"; out.write(s, 0, s.length()); for (i = |
|
||||
* 0; i < nAbstract; i++) { s = ""+i+":"+statesList.get(i)+" \n"; out.write(s, 0, s.length()); } |
|
||||
* out.close(); |
|
||||
*/ |
|
||||
|
|
||||
// second pass - build mapping from concrete to abstract states and build array of target states |
|
||||
System.out.println("Building mapping..."); |
|
||||
mapping = new int[nConcrete]; |
|
||||
target = new boolean[nConcrete]; |
|
||||
in = new BufferedReader(new FileReader(new File(abstr.filename + ".sta"))); |
|
||||
s = in.readLine(); |
|
||||
s = in.readLine(); |
|
||||
while (s != null) { |
|
||||
i = Integer.parseInt(s.substring(0, s.indexOf(":"))); |
|
||||
s = s.substring(s.indexOf(":") + 2, s.indexOf(")")); |
|
||||
ss = s.split(","); |
|
||||
vars = new int[numVars]; |
|
||||
for (j = 0; j < numVars; j++) { |
|
||||
try { |
|
||||
vars[j] = Integer.parseInt(ss[j]); |
|
||||
} catch (NumberFormatException e) { |
|
||||
if (ss[j].equals("false")) |
|
||||
vars[j] = 0; |
|
||||
else { |
|
||||
if (ss[j].equals("true")) |
|
||||
vars[j] = 1; |
|
||||
else |
|
||||
throw e; |
|
||||
} |
|
||||
} |
|
||||
} |
|
||||
state = abstr.concreteToAbstract(vars); |
|
||||
j = statesList.indexOf(state); |
|
||||
mapping[i] = j; |
|
||||
if (abstr.isInitialConcreteState(vars)) { |
|
||||
initialConcreteState = i; |
|
||||
initialAbstractState = j; |
|
||||
} |
|
||||
target[i] = abstr.isTargetConcreteState(vars); |
|
||||
s = in.readLine(); |
|
||||
} |
|
||||
in.close(); |
|
||||
} catch (IOException e) { |
|
||||
System.out.println(e); |
|
||||
System.exit(1); |
|
||||
} |
|
||||
|
|
||||
// stop timer |
|
||||
timer = System.currentTimeMillis() - timer; |
|
||||
System.out.println("Abstract state space built in " + timer / 1000.0 + " seconds."); |
|
||||
} |
|
||||
|
|
||||
public void buildAbstractMDP(PRISMAbstraction abstr) |
|
||||
{ |
|
||||
BufferedReader in; |
|
||||
String s, ss[]; |
|
||||
int i = 0, j, k, n, iLast, kLast; |
|
||||
double prob; |
|
||||
Distribution distr; |
|
||||
HashSet distrs = null; |
|
||||
Iterator it1, it2, it3; |
|
||||
HashMap mdpTmp[]; |
|
||||
Set set; |
|
||||
List list, list2; |
|
||||
|
|
||||
long timer; |
|
||||
|
|
||||
// start timer |
|
||||
timer = System.currentTimeMillis(); |
|
||||
|
|
||||
try { |
|
||||
// read transitions file - build mdp |
|
||||
mdpTmp = new HashMap[nAbstract]; |
|
||||
for (i = 0; i < nAbstract; i++) mdpTmp[i] = new HashMap(); |
|
||||
in = new BufferedReader(new FileReader(new File(abstr.filename+".tra"))); |
|
||||
s = in.readLine(); |
|
||||
nnzConcrete = 0; |
|
||||
if (s != null) { |
|
||||
s = s.substring(1,s.length()-1); |
|
||||
ss = s.split(","); |
|
||||
} |
|
||||
iLast = -1; |
|
||||
kLast = -1; |
|
||||
distr = null; |
|
||||
s = in.readLine(); |
|
||||
while (s != null) { |
|
||||
ss = s.split(" "); |
|
||||
i = Integer.parseInt(ss[0]); |
|
||||
k = Integer.parseInt(ss[1]); |
|
||||
j = Integer.parseInt(ss[2]); |
|
||||
prob = Double.parseDouble(ss[3]); |
|
||||
nnzConcrete++; |
|
||||
if (i != iLast) { |
|
||||
if (distr != null) { |
|
||||
distrs.add(distr); |
|
||||
set = (HashSet)mdpTmp[mapping[iLast]].get(distrs); |
|
||||
if (set == null) set = new HashSet<Integer>(); |
|
||||
set.add(iLast); |
|
||||
mdpTmp[mapping[iLast]].put(distrs, set); |
|
||||
} |
|
||||
distrs = new HashSet(); |
|
||||
distr = new Distribution(); |
|
||||
} |
|
||||
else if (k != kLast) { |
|
||||
if (distr != null) distrs.add(distr); |
|
||||
distr = new Distribution(); |
|
||||
} |
|
||||
distr.add(mapping[j], prob); |
|
||||
iLast = i; |
|
||||
kLast = k; |
|
||||
s = in.readLine(); |
|
||||
} |
|
||||
distrs.add(distr); |
|
||||
set = (HashSet)mdpTmp[mapping[iLast]].get(distrs); |
|
||||
if (set == null) set = new HashSet<Integer>(); |
|
||||
set.add(iLast); |
|
||||
mdpTmp[mapping[iLast]].put(distrs, set); |
|
||||
in.close(); |
|
||||
|
|
||||
// build MDP (convert (sets to lists) |
|
||||
mdp = new ArrayList<List>(nAbstract); |
|
||||
mdpStates = new ArrayList<List>(nAbstract); |
|
||||
for (i = 0; i < nAbstract; i++) { |
|
||||
list = new ArrayList(); |
|
||||
list2 = new ArrayList(); |
|
||||
set = mdpTmp[i].keySet(); |
|
||||
it1 = set.iterator(); |
|
||||
while (it1.hasNext()) { |
|
||||
distrs = (HashSet)it1.next(); |
|
||||
list.add(distrs); |
|
||||
list2.add(mdpTmp[i].get(distrs)); |
|
||||
} |
|
||||
mdp.add(list); |
|
||||
mdpStates.add(list2); |
|
||||
} |
|
||||
|
|
||||
// for (i = 0; i < nAbstract; i++) { |
|
||||
// System.out.println(i+": "+mdp.get(i)); |
|
||||
// } |
|
||||
} |
|
||||
catch (IOException e) { |
|
||||
System.out.println(e); |
|
||||
System.exit(1); |
|
||||
} |
|
||||
|
|
||||
System.out.println("Concrete MDP: n = " + nConcrete + ", nnz = " + nnzConcrete); |
|
||||
System.out.println("Initial state: "+initialConcreteState+" (concrete) "+initialAbstractState+" (abstract)"); |
|
||||
|
|
||||
// check size of abstract mdp |
|
||||
nnzAbstract = 0; |
|
||||
j = 0; k = 0; |
|
||||
for (i = 0; i < nAbstract; i++) { |
|
||||
list = mdp.get(i); |
|
||||
n = list.size(); if (n > j) j = n; |
|
||||
it1 = list.iterator(); |
|
||||
while (it1.hasNext()) { |
|
||||
distrs = (HashSet)it1.next(); |
|
||||
n = distrs.size(); if (n > k) k = n; |
|
||||
it2 = distrs.iterator(); |
|
||||
while (it2.hasNext()) { |
|
||||
distr = (Distribution)it2.next(); |
|
||||
it3 = distr.iterator(); |
|
||||
while (it3.hasNext()) { |
|
||||
nnzAbstract++; |
|
||||
it3.next(); |
|
||||
} |
|
||||
} |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
System.out.print("Abstract MDP: n = " + nAbstract + ", nnz = " + nnzAbstract); |
|
||||
System.out.println(", maxk1 = " + j + ", maxk2 = " + k); |
|
||||
|
|
||||
// stop timer |
|
||||
timer = System.currentTimeMillis() - timer; |
|
||||
System.out.println("Abstract MDP built in " + timer/1000.0 + " seconds."); |
|
||||
} |
|
||||
|
|
||||
public void printMapping(PRISMAbstraction abstr) |
|
||||
{ |
|
||||
BufferedReader in; |
|
||||
String s, ss[]; |
|
||||
int i, j, numVars = 0, vars[]; |
|
||||
|
|
||||
try { |
|
||||
in = new BufferedReader(new FileReader(new File(abstr.filename + ".sta"))); |
|
||||
s = in.readLine(); |
|
||||
if (s != null) { |
|
||||
s = s.substring(1, s.length() - 1); |
|
||||
ss = s.split(","); |
|
||||
numVars = ss.length; |
|
||||
} |
|
||||
s = in.readLine(); |
|
||||
i = 0; |
|
||||
while (s != null) { |
|
||||
s = s.substring(s.indexOf(":") + 2, s.indexOf(")")); |
|
||||
ss = s.split(","); |
|
||||
vars = new int[numVars]; |
|
||||
for (j = 0; j < numVars; j++) { |
|
||||
try { |
|
||||
vars[j] = Integer.parseInt(ss[j]); |
|
||||
} catch (NumberFormatException e) { |
|
||||
if (ss[j].equals("false")) |
|
||||
vars[j] = 0; |
|
||||
else { |
|
||||
if (ss[j].equals("true")) |
|
||||
vars[j] = 1; |
|
||||
else |
|
||||
throw e; |
|
||||
} |
|
||||
} |
|
||||
} |
|
||||
System.out.println(mapping[i] + "\t" + s); |
|
||||
s = in.readLine(); |
|
||||
i++; |
|
||||
} |
|
||||
in.close(); |
|
||||
} catch (IOException e) { |
|
||||
System.out.println(e); |
|
||||
System.exit(1); |
|
||||
} |
|
||||
} |
|
||||
} |
|
||||
@ -1,553 +0,0 @@ |
|||||
//============================================================================== |
|
||||
// |
|
||||
// Copyright (c) 2002- |
|
||||
// Authors: |
|
||||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford) |
|
||||
// |
|
||||
//------------------------------------------------------------------------------ |
|
||||
// |
|
||||
// This file is part of PRISM. |
|
||||
// |
|
||||
// PRISM is free software; you can redistribute it and/or modify |
|
||||
// it under the terms of the GNU General Public License as published by |
|
||||
// the Free Software Foundation; either version 2 of the License, or |
|
||||
// (at your option) any later version. |
|
||||
// |
|
||||
// PRISM is distributed in the hope that it will be useful, |
|
||||
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
|
||||
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
|
||||
// GNU General Public License for more details. |
|
||||
// |
|
||||
// You should have received a copy of the GNU General Public License |
|
||||
// along with PRISM; if not, write to the Free Software Foundation, |
|
||||
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
|
||||
// |
|
||||
//============================================================================== |
|
||||
|
|
||||
package abstraction; |
|
||||
|
|
||||
import java.util.*; |
|
||||
import explicit.*; |
|
||||
|
|
||||
public class AbstractRefine |
|
||||
{ |
|
||||
protected double epsilonRefine = 1e-4; // abs |
|
||||
protected double epsilonSolve = 1e-6; // rel |
|
||||
protected double epsilonDouble = 1e-12; // abs |
|
||||
|
|
||||
protected PRISMAbstraction abstr = null; |
|
||||
protected AbstractMDP amdp = null; |
|
||||
protected GameModelChecker gmc = null; |
|
||||
|
|
||||
// Flags/parameters |
|
||||
protected boolean optimise; |
|
||||
protected String refinementMethod; |
|
||||
|
|
||||
public boolean phi2[]; |
|
||||
|
|
||||
public int totalIters; |
|
||||
|
|
||||
protected int property = -1; // -2 = expected reachability, -1 = probabilistic reachability, >=0 = bounded |
|
||||
// reachability |
|
||||
protected int refinementMapping[]; |
|
||||
|
|
||||
/* Main method - create a class instance and call run() */ |
|
||||
|
|
||||
public static void main(String args[]) |
|
||||
{ |
|
||||
new AbstractRefine().run(args); |
|
||||
} |
|
||||
|
|
||||
/* Run method - do abstraction refinement loop */ |
|
||||
|
|
||||
public void run(String args[]) |
|
||||
{ |
|
||||
int i, j; |
|
||||
boolean done; |
|
||||
String s; |
|
||||
long totalTimer; |
|
||||
long initTime, buildTime, solnTime, refineTime; |
|
||||
|
|
||||
// start timer |
|
||||
totalTimer = System.currentTimeMillis(); |
|
||||
|
|
||||
initTime = 0; |
|
||||
buildTime = 0; |
|
||||
solnTime = 0; |
|
||||
refineTime = 0; |
|
||||
|
|
||||
// Locate and construct abstraction class from name in args[0] |
|
||||
Class<?> abstrClass; |
|
||||
try { |
|
||||
abstrClass = Class.forName(args[0].replace("/", ".")); |
|
||||
abstr = (PRISMAbstraction)abstrClass.newInstance(); |
|
||||
} catch (ClassNotFoundException e) { |
|
||||
System.err.println(e); |
|
||||
System.exit(1); |
|
||||
} catch (IllegalAccessException e) { |
|
||||
System.err.println(e); |
|
||||
System.exit(1); |
|
||||
} catch (InstantiationException e) { |
|
||||
System.err.println(e); |
|
||||
System.exit(1); |
|
||||
} |
|
||||
|
|
||||
// Configure abstraction class using model details in args[1] |
|
||||
s = abstr.modelArgs(args[1]); |
|
||||
if (s != null) { |
|
||||
System.out.println(usage()); |
|
||||
System.out.println("where <model_details> are: " + s); |
|
||||
System.exit(1); |
|
||||
} |
|
||||
|
|
||||
// Create game model checker |
|
||||
gmc = new GameModelChecker(); |
|
||||
|
|
||||
// Parse command-line arguments |
|
||||
args(args); |
|
||||
|
|
||||
// Build initial abstract MDP |
|
||||
amdp = new AbstractMDP(); |
|
||||
amdp.buildAbstractStateSpace(abstr); |
|
||||
initTime = amdp.getLastTimer(); |
|
||||
|
|
||||
i = 0; |
|
||||
done = false; |
|
||||
totalIters = 0; |
|
||||
|
|
||||
while (!done) { |
|
||||
|
|
||||
System.out.println("\nBuilding abstract MDP (#" + i + ")..."); |
|
||||
amdp.buildAbstractMDP(abstr); |
|
||||
buildTime += amdp.getLastTimer(); |
|
||||
buildPhi2(); |
|
||||
System.out.println("\nModel checking (#" + i + ")..."); |
|
||||
gmc.lbStrat = new HashSet[amdp.nAbstract]; |
|
||||
gmc.ubStrat = new HashSet[amdp.nAbstract]; |
|
||||
for (j = 0; j < amdp.nAbstract; j++) { |
|
||||
gmc.lbStrat[j] = new HashSet(); |
|
||||
gmc.ubStrat[j] = new HashSet(); |
|
||||
} |
|
||||
if (property == -2) { |
|
||||
gmc.expectedReachability(amdp, phi2, true, abstr.computeMinExp(), refinementMapping); // min max (default) |
|
||||
solnTime += gmc.getLastTimer(); |
|
||||
totalIters += gmc.getLastIters(); |
|
||||
gmc.expectedReachability(amdp, phi2, false, abstr.computeMinExp(), refinementMapping); // max max (default) |
|
||||
solnTime += gmc.getLastTimer(); |
|
||||
totalIters += gmc.getLastIters(); |
|
||||
} else { |
|
||||
gmc.probabilisticReachability(amdp, phi2, true, abstr.computeMinProbs(), refinementMapping); // min min (default) |
|
||||
solnTime += gmc.getLastTimer(); |
|
||||
totalIters += gmc.getLastIters(); |
|
||||
gmc.probabilisticReachability(amdp, phi2, false, abstr.computeMinProbs(), refinementMapping); // max min (default) |
|
||||
solnTime += gmc.getLastTimer(); |
|
||||
totalIters += gmc.getLastIters(); |
|
||||
} |
|
||||
// System.out.print("lb:"); for (j = 0; j < nAbstract; j++) System.out.print(" "+gmc.lbSoln[j]); |
|
||||
// System.out.println(); |
|
||||
// System.out.print("ub:"); for (j = 0; j < nAbstract; j++) System.out.print(" "+gmc.ubSoln[j]); |
|
||||
// System.out.println(); |
|
||||
// System.out.print("gmc.lbStrat:"); for (j = 0; j < nAbstract; j++) System.out.print(" "+gmc.lbStrat[j]); |
|
||||
// System.out.println(); |
|
||||
// System.out.print("gmc.ubStrat:"); for (j = 0; j < nAbstract; j++) System.out.print(" "+gmc.ubStrat[j]); |
|
||||
// System.out.println(); |
|
||||
System.out.print("Result interval for initial state: " |
|
||||
+ abstr.processResult(property, gmc.lbSoln[amdp.initialAbstractState]) + "," |
|
||||
+ abstr.processResult(property, gmc.ubSoln[amdp.initialAbstractState])); |
|
||||
System.out.println(" (diff = " |
|
||||
+ Math.abs(abstr.processResult(property, gmc.lbSoln[amdp.initialAbstractState]) |
|
||||
- abstr.processResult(property, gmc.ubSoln[amdp.initialAbstractState])) + ")"); |
|
||||
|
|
||||
if (!veryCloseRel(gmc.ubSoln[amdp.initialAbstractState], gmc.lbSoln[amdp.initialAbstractState], epsilonRefine)) { |
|
||||
// if (!veryCloseAbs(gmc.ubSoln[amdp.initialAbstractState], gmc.lbSoln[amdp.initialAbstractState], |
|
||||
// epsilonRefine)) { |
|
||||
i++; |
|
||||
System.out.println("\nRefining (#" + i + ")..."); |
|
||||
boolean res = refine(refinementMethod); |
|
||||
refineTime += gmc.getLastTimer(); |
|
||||
if (!res) { |
|
||||
done = true; |
|
||||
i--; |
|
||||
} |
|
||||
} else { |
|
||||
done = true; |
|
||||
} |
|
||||
|
|
||||
} |
|
||||
|
|
||||
// stop timer |
|
||||
totalTimer = System.currentTimeMillis() - totalTimer; |
|
||||
|
|
||||
System.out.println("\nTotal of " + i + " refinements"); |
|
||||
System.out.println("\nFinal abstract MDP has " + amdp.nAbstract + " states and " + amdp.nnzAbstract |
|
||||
+ " transitions"); |
|
||||
System.out.println("\nFinal result interval for initial state: " |
|
||||
+ abstr.processResult(property, gmc.lbSoln[amdp.initialAbstractState]) + "," |
|
||||
+ abstr.processResult(property, gmc.ubSoln[amdp.initialAbstractState])); |
|
||||
System.out.println("\nTotal time for whole process: " + totalTimer / 1000.0 + " seconds."); |
|
||||
System.out.println("\nTime breakdown: init " + initTime / 1000.0 + " seconds, build " + buildTime / 1000.0 |
|
||||
+ " seconds, soln " + solnTime / 1000.0 + " seconds, refine " + refineTime / 1000.0 + " seconds."); |
|
||||
System.out.println("\nTotal iterations for whole process: " + totalIters); |
|
||||
|
|
||||
//amdp.printMapping(abstr); |
|
||||
} |
|
||||
|
|
||||
/* Parse command-line args */ |
|
||||
|
|
||||
public void args(String args[]) |
|
||||
{ |
|
||||
if (args.length < 3) { |
|
||||
System.out.println(usage()); |
|
||||
System.exit(1); |
|
||||
} |
|
||||
property = Integer.parseInt(args[2]); |
|
||||
refinementMethod = (args.length > 3) ? args[3] : null; |
|
||||
for (int i = 3; i < args.length; i++) { |
|
||||
if (args[i].equals("-opt")) |
|
||||
optimise = gmc.optimise = true; |
|
||||
else if (args[i].equals("-noopt")) |
|
||||
optimise = gmc.optimise = false; |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
/* Usage string */ |
|
||||
|
|
||||
public String usage() |
|
||||
{ |
|
||||
return "Usage: java "+getClass().getName()+" <abstr_class> <model_details> <property>"; |
|
||||
} |
|
||||
|
|
||||
public void buildPhi2() |
|
||||
{ |
|
||||
int i; |
|
||||
phi2 = new boolean[amdp.nAbstract]; |
|
||||
for (i = 0; i < amdp.nAbstract; i++) |
|
||||
phi2[i] = false; |
|
||||
for (i = 0; i < amdp.nConcrete; i++) |
|
||||
if (amdp.target[i]) |
|
||||
phi2[amdp.mapping[i]] = true; |
|
||||
} |
|
||||
|
|
||||
// Perform refinement, return true if refined successfully |
|
||||
|
|
||||
public boolean refine(String refinementMethod) |
|
||||
{ |
|
||||
if (refinementMethod == null) |
|
||||
return false; |
|
||||
if (refinementMethod.equals("10")) |
|
||||
return refine(1, 0); |
|
||||
else if (refinementMethod.equals("11")) |
|
||||
return refine(1, 1); |
|
||||
else if (refinementMethod.equals("20")) |
|
||||
return refine(2, 0); |
|
||||
else if (refinementMethod.equals("21")) |
|
||||
return refine(2, 1); |
|
||||
return false; |
|
||||
} |
|
||||
|
|
||||
// whichStates: 0 = single max diff, 1 = all max diff, 2 = all where diff > 0 |
|
||||
// howSplit: 0 = choose single lower/upper bound strategies, 1 = ... |
|
||||
|
|
||||
public boolean refine(int whichStates, int howSplit) |
|
||||
{ |
|
||||
HashSet set, splitStates, strategySets, inter, l_minus, u_minus; |
|
||||
Iterator it1, it2; |
|
||||
int i, n, r, r_lb, r_ub, newStates = 0; |
|
||||
double maxDiff; |
|
||||
Integer ii; |
|
||||
List list; |
|
||||
long timer; |
|
||||
|
|
||||
// Start timer |
|
||||
timer = System.currentTimeMillis(); |
|
||||
|
|
||||
// If necessary, find find max diff amongst potential split states |
|
||||
maxDiff = 0.0; |
|
||||
r = -1; |
|
||||
if (whichStates <= 1) { |
|
||||
System.out.print("Potential split states:"); |
|
||||
for (i = 0; i < amdp.nAbstract; i++) { |
|
||||
if (gmc.ubSoln[i] - gmc.lbSoln[i] < maxDiff) |
|
||||
continue; |
|
||||
set = new HashSet(); |
|
||||
set.addAll(gmc.lbStrat[i]); |
|
||||
set.addAll(gmc.ubStrat[i]); |
|
||||
if (set.size() > 1) { |
|
||||
maxDiff = gmc.ubSoln[i] - gmc.lbSoln[i]; |
|
||||
r = i; |
|
||||
System.out.print(" " + i); |
|
||||
} |
|
||||
} |
|
||||
System.out.println(); |
|
||||
if (r > -1) |
|
||||
System.out.println("Potential split state max diff: " + maxDiff); |
|
||||
else { |
|
||||
System.out.println("No potential split states."); |
|
||||
return false; |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
// Choose states to split |
|
||||
splitStates = new HashSet(); |
|
||||
switch (whichStates) { |
|
||||
case 0: |
|
||||
splitStates.add(r); |
|
||||
break; |
|
||||
case 1: |
|
||||
for (i = 0; i < amdp.nAbstract; i++) { |
|
||||
// set = new HashSet(); |
|
||||
// set.addAll(gmc.lbStrat[i]); |
|
||||
// set.addAll(gmc.ubStrat[i]); |
|
||||
// if (set.size() > 1) splitStates.add(i); |
|
||||
|
|
||||
// If there's only one choice in this player 1 state, can't be split |
|
||||
if (amdp.mdp.get(i).size() == 1 || !veryCloseAbs(gmc.ubSoln[i] - gmc.lbSoln[i], maxDiff, epsilonDouble)) { |
|
||||
if (optimise) |
|
||||
gmc.status[i] = 2; |
|
||||
continue; |
|
||||
} |
|
||||
|
|
||||
splitStates.add(i); |
|
||||
} |
|
||||
break; |
|
||||
case 2: |
|
||||
for (i = 0; i < amdp.nAbstract; i++) { |
|
||||
// set = new HashSet(); |
|
||||
// set.addAll(gmc.lbStrat[i]); |
|
||||
// set.addAll(gmc.ubStrat[i]); |
|
||||
// if (set.size() > 1 && !veryClose(gmc.ubSoln[i], gmc.lbSoln[i], epsilonDouble)) splitStates.add(i); |
|
||||
|
|
||||
// If there's only one choice in this player 1 state, can't be split |
|
||||
if (amdp.mdp.get(i).size() == 1) |
|
||||
continue; |
|
||||
if (veryClose(gmc.ubSoln[i], gmc.lbSoln[i], epsilonDouble)) { |
|
||||
if (optimise) |
|
||||
gmc.status[i] = 2; |
|
||||
continue; |
|
||||
} |
|
||||
|
|
||||
splitStates.add(i); |
|
||||
} |
|
||||
break; |
|
||||
} |
|
||||
// System.out.println("Split states: "+splitStates); |
|
||||
|
|
||||
// Split the states; this is done in 2 passes: |
|
||||
// - one which just counts the number of new abstract states |
|
||||
// - the second which actually does the split |
|
||||
strategySets = new HashSet(); |
|
||||
for (int round = 1; round <= 2; round++) { |
|
||||
|
|
||||
// create array to store (backwards) refinement map |
|
||||
if (round == 2) { |
|
||||
refinementMapping = new int[amdp.nAbstract + newStates]; |
|
||||
for (i = 0; i < amdp.nAbstract + newStates; i++) |
|
||||
refinementMapping[i] = i; |
|
||||
} |
|
||||
|
|
||||
newStates = 0; |
|
||||
it1 = splitStates.iterator(); |
|
||||
while (it1.hasNext()) { |
|
||||
// Which state (r) to be split |
|
||||
r = (Integer) it1.next(); |
|
||||
// Start with empty set of stratedy sets |
|
||||
strategySets.clear(); |
|
||||
if (howSplit == 0) { |
|
||||
// Remove interection of lb/ub strategy sets from larger |
|
||||
// If sets were identical, move one element across to ensure both non-empty |
|
||||
if (gmc.lbStrat[r].size() > gmc.ubStrat[r].size()) { |
|
||||
gmc.lbStrat[r].removeAll(gmc.ubStrat[r]); |
|
||||
if (gmc.lbStrat[r].size() == 0) { |
|
||||
ii = (Integer) gmc.ubStrat[r].iterator().next(); |
|
||||
gmc.lbStrat[r].add(ii); |
|
||||
gmc.ubStrat[r].remove(ii); |
|
||||
} |
|
||||
} else { |
|
||||
gmc.ubStrat[r].removeAll(gmc.lbStrat[r]); |
|
||||
if (gmc.ubStrat[r].size() == 0) { |
|
||||
ii = (Integer) gmc.lbStrat[r].iterator().next(); |
|
||||
gmc.ubStrat[r].add(ii); |
|
||||
gmc.lbStrat[r].remove(ii); |
|
||||
} |
|
||||
} |
|
||||
// Pick first of each set |
|
||||
r_lb = (!gmc.lbStrat[r].isEmpty()) ? (Integer) gmc.lbStrat[r].iterator().next() : -1; |
|
||||
r_ub = (!gmc.ubStrat[r].isEmpty()) ? (Integer) gmc.ubStrat[r].iterator().next() : -1; |
|
||||
if (r_ub != -1) { |
|
||||
set = new HashSet(); |
|
||||
set.add(r_ub); |
|
||||
strategySets.add(set); |
|
||||
} |
|
||||
if (r_lb != -1) { |
|
||||
set = new HashSet(); |
|
||||
set.add(r_lb); |
|
||||
strategySets.add(set); |
|
||||
} |
|
||||
} else { |
|
||||
inter = new HashSet(); |
|
||||
l_minus = new HashSet(); |
|
||||
u_minus = new HashSet(); |
|
||||
it2 = gmc.lbStrat[r].iterator(); |
|
||||
while (it2.hasNext()) { |
|
||||
i = (Integer) it2.next(); |
|
||||
if (gmc.ubStrat[r].contains(i)) |
|
||||
inter.add(i); |
|
||||
else |
|
||||
l_minus.add(i); |
|
||||
} |
|
||||
it2 = gmc.ubStrat[r].iterator(); |
|
||||
while (it2.hasNext()) { |
|
||||
i = (Integer) it2.next(); |
|
||||
if (gmc.lbStrat[r].contains(i)) |
|
||||
inter.add(i); |
|
||||
else |
|
||||
u_minus.add(i); |
|
||||
} |
|
||||
// System.out.println("lb: "+gmc.lbStrat[r]+" ub: "+gmc.ubStrat[r]+" inter: "+inter+" |
|
||||
// interval="+gmc.lbSoln[r]+"-"+gmc.ubSoln[r]); |
|
||||
if (inter.size() > 0) |
|
||||
strategySets.add(inter); |
|
||||
if (l_minus.size() > 0) |
|
||||
strategySets.add(l_minus); |
|
||||
if (u_minus.size() > 0) |
|
||||
strategySets.add(u_minus); |
|
||||
} |
|
||||
// Split (or not) |
|
||||
if (round == 1) { |
|
||||
newStates += splitCount(r, strategySets); |
|
||||
} else { |
|
||||
newStates += split(r, strategySets); |
|
||||
} |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
// Stop timer |
|
||||
timer = System.currentTimeMillis() - timer; |
|
||||
System.out.println("Refinement completed in " + timer / 1000.0 + " seconds (" + newStates + " states added)"); |
|
||||
|
|
||||
return true; |
|
||||
} |
|
||||
|
|
||||
// Return number of new states that would be added on a split |
|
||||
|
|
||||
public int splitCount(int r, HashSet strategySets) |
|
||||
{ |
|
||||
List state; |
|
||||
Iterator it1; |
|
||||
boolean reuse; |
|
||||
int i, n, count, newStates; |
|
||||
|
|
||||
state = amdp.mdp.get(r); |
|
||||
it1 = strategySets.iterator(); |
|
||||
n = strategySets.size(); |
|
||||
i = 0; |
|
||||
count = 0; |
|
||||
newStates = 0; |
|
||||
reuse = false; |
|
||||
while (it1.hasNext()) { |
|
||||
count += ((HashSet) it1.next()).size(); |
|
||||
if (i == n - 1 && count == state.size()) |
|
||||
reuse = true; |
|
||||
if (!reuse) |
|
||||
newStates++; |
|
||||
i++; |
|
||||
} |
|
||||
return newStates; |
|
||||
} |
|
||||
|
|
||||
// Split a state, return number of new states added |
|
||||
|
|
||||
public int split(int r, HashSet strategySets) |
|
||||
{ |
|
||||
HashSet set, oneStrategySet; |
|
||||
List state, states; |
|
||||
Iterator it1, it2, it3; |
|
||||
int i, j, k, n, count, newStates; |
|
||||
boolean reuse; |
|
||||
List list; |
|
||||
|
|
||||
int r_lb = -1; |
|
||||
int r_ub = 1; |
|
||||
|
|
||||
// System.out.println("Splitting state "+r+" (strats="+strategySets+")"); |
|
||||
|
|
||||
state = amdp.mdp.get(r); |
|
||||
states = amdp.mdpStates.get(r); |
|
||||
|
|
||||
// Go through each set of strategies (i.e. each new partition of state r) |
|
||||
it1 = strategySets.iterator(); |
|
||||
n = strategySets.size(); |
|
||||
i = 0; |
|
||||
count = 0; |
|
||||
newStates = 0; |
|
||||
reuse = false; |
|
||||
while (it1.hasNext()) { |
|
||||
oneStrategySet = (HashSet) it1.next(); |
|
||||
// Keep running count of number of strategies and, on the last set, |
|
||||
// work out if we will reuse state r |
|
||||
count += oneStrategySet.size(); |
|
||||
// System.out.println("# "+i+"/"+n+": "+count+" (="+state.size()+"?)"); |
|
||||
if (i == n - 1 && count == state.size()) |
|
||||
reuse = true; |
|
||||
if (!reuse) { |
|
||||
// System.out.print("New state "+amdp.nAbstract+": "); |
|
||||
refinementMapping[amdp.nAbstract] = r; |
|
||||
// System.out.print("* "+amdp.nAbstract+" - > "+r); |
|
||||
newStates++; |
|
||||
// For each strategy (i.e. element of player 1 state) in the set |
|
||||
it2 = oneStrategySet.iterator(); |
|
||||
while (it2.hasNext()) { |
|
||||
j = (Integer) it2.next(); |
|
||||
// For each concrete state corresponding to that strategy |
|
||||
it3 = ((HashSet) states.get(j)).iterator(); |
|
||||
while (it3.hasNext()) { |
|
||||
k = ((Integer) it3.next()).intValue(); |
|
||||
// System.out.print(" "+k); |
|
||||
amdp.mapping[k] = amdp.nAbstract; |
|
||||
if (k == amdp.initialConcreteState) |
|
||||
amdp.initialAbstractState = amdp.nAbstract; |
|
||||
} |
|
||||
} |
|
||||
// System.out.println(); |
|
||||
amdp.nAbstract++; |
|
||||
} |
|
||||
i++; |
|
||||
} |
|
||||
|
|
||||
return newStates; |
|
||||
} |
|
||||
|
|
||||
public static boolean veryClose(double d1, double d2, double epsilon) |
|
||||
{ |
|
||||
return veryCloseAbs(d1, d2, epsilon); |
|
||||
} |
|
||||
|
|
||||
public static boolean veryCloseAbs(double d1, double d2, double epsilon) |
|
||||
{ |
|
||||
if (Double.isInfinite(d1)) { |
|
||||
if (Double.isInfinite(d2)) |
|
||||
return (d1 > 0) == (d2 > 0); |
|
||||
else |
|
||||
return false; |
|
||||
} |
|
||||
double diff = Math.abs(d1 - d2); |
|
||||
return (diff < epsilon); |
|
||||
} |
|
||||
|
|
||||
public static boolean veryCloseRel(double d1, double d2, double epsilon) |
|
||||
{ |
|
||||
if (Double.isInfinite(d1)) { |
|
||||
if (Double.isInfinite(d2)) |
|
||||
return (d1 > 0) == (d2 > 0); |
|
||||
else |
|
||||
return false; |
|
||||
} |
|
||||
double diff = Math.abs(d1 - d2); |
|
||||
double min = Math.min(d1, d2); |
|
||||
if (min != 0) |
|
||||
return (diff / min < epsilon); |
|
||||
return (diff < epsilon); |
|
||||
} |
|
||||
|
|
||||
|
|
||||
} |
|
||||
@ -1,73 +0,0 @@ |
|||||
//============================================================================== |
|
||||
// |
|
||||
// Copyright (c) 2002- |
|
||||
// Authors: |
|
||||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford) |
|
||||
// |
|
||||
//------------------------------------------------------------------------------ |
|
||||
// |
|
||||
// This file is part of PRISM. |
|
||||
// |
|
||||
// PRISM is free software; you can redistribute it and/or modify |
|
||||
// it under the terms of the GNU General Public License as published by |
|
||||
// the Free Software Foundation; either version 2 of the License, or |
|
||||
// (at your option) any later version. |
|
||||
// |
|
||||
// PRISM is distributed in the hope that it will be useful, |
|
||||
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
|
||||
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
|
||||
// GNU General Public License for more details. |
|
||||
// |
|
||||
// You should have received a copy of the GNU General Public License |
|
||||
// along with PRISM; if not, write to the Free Software Foundation, |
|
||||
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
|
||||
// |
|
||||
//============================================================================== |
|
||||
|
|
||||
package abstraction; |
|
||||
|
|
||||
public class AbstractState implements Comparable |
|
||||
{ |
|
||||
private int n; |
|
||||
private int vars[]; |
|
||||
|
|
||||
public AbstractState(int n) |
|
||||
{ |
|
||||
this.n = n; |
|
||||
vars = new int[n]; |
|
||||
} |
|
||||
|
|
||||
public void set(int i, int v) |
|
||||
{ |
|
||||
vars[i] = v; |
|
||||
} |
|
||||
|
|
||||
public int compareTo(Object o) |
|
||||
{ |
|
||||
AbstractState s = (AbstractState) o; |
|
||||
for (int i = 0; i < n; i++) { |
|
||||
if (vars[i] < s.vars[i]) |
|
||||
return -1; |
|
||||
if (vars[i] > s.vars[i]) |
|
||||
return 1; |
|
||||
} |
|
||||
return 0; |
|
||||
} |
|
||||
|
|
||||
public boolean equals(Object o) |
|
||||
{ |
|
||||
return compareTo(o) == 0; |
|
||||
} |
|
||||
|
|
||||
public String toString() |
|
||||
{ |
|
||||
String s = "("; |
|
||||
for (int i = 0; i < n; i++) { |
|
||||
s += "" + vars[i]; |
|
||||
if (i < n - 1) |
|
||||
s += ","; |
|
||||
} |
|
||||
s += ")"; |
|
||||
return s; |
|
||||
} |
|
||||
} |
|
||||
@ -1,34 +0,0 @@ |
|||||
################################################
|
|
||||
# NB: This Makefile is designed to be called #
|
|
||||
# from the main PRISM Makefile. It won't #
|
|
||||
# work on its own because it needs #
|
|
||||
# various options to be passed in #
|
|
||||
################################################
|
|
||||
|
|
||||
# Reminder: $@ = target, $* = target without extension, $< = dependency
|
|
||||
|
|
||||
THIS_DIR = abstraction |
|
||||
PRISM_DIR_REL = ../.. |
|
||||
|
|
||||
JAVA_FILES = $(wildcard *.java) |
|
||||
CLASS_FILES = $(JAVA_FILES:%.java=$(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/%.class) |
|
||||
|
|
||||
default: all |
|
||||
|
|
||||
all: checks $(CLASS_FILES) |
|
||||
|
|
||||
# Try and prevent accidental makes (i.e. called manually, not from top-level Makefile)
|
|
||||
checks: |
|
||||
@if [ "$(SRC_DIR)" = "" ]; then \
|
|
||||
(echo "Error: This Makefile is designed to be called from the main PRISM Makefile"; exit 1) \
|
|
||||
fi; |
|
||||
|
|
||||
$(PRISM_DIR_REL)/$(CLASSES_DIR)/$(THIS_DIR)/%.class: %.java |
|
||||
(cd ..; $(JAVAC) -sourcepath $(THIS_DIR)/$(PRISM_DIR_REL)/$(SRC_DIR) -classpath $(THIS_DIR)/$(PRISM_DIR_REL)/$(CLASSES_DIR) -d $(THIS_DIR)/$(PRISM_DIR_REL)/$(CLASSES_DIR) $(THIS_DIR)/$<) |
|
||||
|
|
||||
clean: checks |
|
||||
@rm -f $(CLASS_FILES) |
|
||||
|
|
||||
celan: clean |
|
||||
|
|
||||
#################################################
|
|
||||
@ -1,71 +0,0 @@ |
|||||
//============================================================================== |
|
||||
// |
|
||||
// Copyright (c) 2002- |
|
||||
// Authors: |
|
||||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford) |
|
||||
// |
|
||||
//------------------------------------------------------------------------------ |
|
||||
// |
|
||||
// This file is part of PRISM. |
|
||||
// |
|
||||
// PRISM is free software; you can redistribute it and/or modify |
|
||||
// it under the terms of the GNU General Public License as published by |
|
||||
// the Free Software Foundation; either version 2 of the License, or |
|
||||
// (at your option) any later version. |
|
||||
// |
|
||||
// PRISM is distributed in the hope that it will be useful, |
|
||||
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
|
||||
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
|
||||
// GNU General Public License for more details. |
|
||||
// |
|
||||
// You should have received a copy of the GNU General Public License |
|
||||
// along with PRISM; if not, write to the Free Software Foundation, |
|
||||
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
|
||||
// |
|
||||
//============================================================================== |
|
||||
|
|
||||
package abstraction; |
|
||||
|
|
||||
public abstract class PRISMAbstraction |
|
||||
{ |
|
||||
public String filename; |
|
||||
|
|
||||
/* Configure based on command-line arguments */ |
|
||||
abstract public String modelArgs(String arg); |
|
||||
|
|
||||
/* Return string listing abstract variable names */ |
|
||||
abstract protected String abstractVarsString(); |
|
||||
|
|
||||
/* Convert concrete to concrete state to abstract state */ |
|
||||
abstract protected AbstractState concreteToAbstract(int vars[]); |
|
||||
|
|
||||
/* Identifies (concrete) target states for reachability */ |
|
||||
abstract protected boolean isTargetConcreteState(int vars[]); |
|
||||
|
|
||||
/* Identifies (single) (concrete) initial state */ |
|
||||
abstract protected boolean isInitialConcreteState(int vars[]); |
|
||||
|
|
||||
/* Identifies (abstract) initial state (for which results will be shown) */ |
|
||||
abstract protected AbstractState getInitialAbstractState(); |
|
||||
|
|
||||
/* If required, process result (e.g. to subtract from one) */ |
|
||||
|
|
||||
public double processResult(int property, double res) |
|
||||
{ |
|
||||
return res; |
|
||||
} |
|
||||
|
|
||||
/* Compute min probs? (default is "yes", i.e. true) */ |
|
||||
|
|
||||
public boolean computeMinProbs() |
|
||||
{ |
|
||||
return true; |
|
||||
} |
|
||||
|
|
||||
/* Compute min expected costs? (default is "no", i.e. false) */ |
|
||||
|
|
||||
public boolean computeMinExp() |
|
||||
{ |
|
||||
return false; |
|
||||
} |
|
||||
} |
|
||||
@ -1,82 +0,0 @@ |
|||||
//============================================================================== |
|
||||
// |
|
||||
// Copyright (c) 2002- |
|
||||
// Authors: |
|
||||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford) |
|
||||
// |
|
||||
//------------------------------------------------------------------------------ |
|
||||
// |
|
||||
// This file is part of PRISM. |
|
||||
// |
|
||||
// PRISM is free software; you can redistribute it and/or modify |
|
||||
// it under the terms of the GNU General Public License as published by |
|
||||
// the Free Software Foundation; either version 2 of the License, or |
|
||||
// (at your option) any later version. |
|
||||
// |
|
||||
// PRISM is distributed in the hope that it will be useful, |
|
||||
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
|
||||
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
|
||||
// GNU General Public License for more details. |
|
||||
// |
|
||||
// You should have received a copy of the GNU General Public License |
|
||||
// along with PRISM; if not, write to the Free Software Foundation, |
|
||||
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
|
||||
// |
|
||||
//============================================================================== |
|
||||
|
|
||||
package abstraction.examples; |
|
||||
|
|
||||
import abstraction.*; |
|
||||
|
|
||||
public class Firewire extends PRISMAbstraction |
|
||||
{ |
|
||||
/* Parse comma-separated command-line argument with model details |
|
||||
Returns null if OK, correct format string if not */ |
|
||||
|
|
||||
public String modelArgs(String arg) |
|
||||
{ |
|
||||
filename = "data/firewire/impl"+arg; |
|
||||
return null; |
|
||||
} |
|
||||
|
|
||||
/* Comma-separated list of names of variables in abstraction */ |
|
||||
|
|
||||
protected String abstractVarsString() |
|
||||
{ |
|
||||
return "x"; |
|
||||
} |
|
||||
|
|
||||
/* Abstraction: conversion of concrete to abstract state */ |
|
||||
|
|
||||
protected AbstractState concreteToAbstract(int vars[]) |
|
||||
{ |
|
||||
AbstractState state; |
|
||||
int i; |
|
||||
|
|
||||
state = new AbstractState(1); |
|
||||
if (isInitialConcreteState(vars)) i = 0; |
|
||||
else if (isTargetConcreteState(vars)) i = 1; |
|
||||
else i = 2; |
|
||||
state.set(0, i); |
|
||||
|
|
||||
return state; |
|
||||
} |
|
||||
|
|
||||
protected boolean isTargetConcreteState(int vars[]) |
|
||||
{ |
|
||||
return ((vars[4] == 7 && vars[9] == 8) || (vars[4] == 8 && vars[9] == 7)); |
|
||||
} |
|
||||
|
|
||||
protected boolean isInitialConcreteState(int vars[]) |
|
||||
{ |
|
||||
int i; |
|
||||
for (i = 0; i < 10; i++) if (vars[i] != 0) return false; |
|
||||
return true; |
|
||||
} |
|
||||
|
|
||||
protected AbstractState getInitialAbstractState() |
|
||||
{ |
|
||||
// not currently used? |
|
||||
return null; |
|
||||
} |
|
||||
} |
|
||||
@ -1,80 +0,0 @@ |
|||||
//============================================================================== |
|
||||
// |
|
||||
// Copyright (c) 2002- |
|
||||
// Authors: |
|
||||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford) |
|
||||
// |
|
||||
//------------------------------------------------------------------------------ |
|
||||
// |
|
||||
// This file is part of PRISM. |
|
||||
// |
|
||||
// PRISM is free software; you can redistribute it and/or modify |
|
||||
// it under the terms of the GNU General Public License as published by |
|
||||
// the Free Software Foundation; either version 2 of the License, or |
|
||||
// (at your option) any later version. |
|
||||
// |
|
||||
// PRISM is distributed in the hope that it will be useful, |
|
||||
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
|
||||
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
|
||||
// GNU General Public License for more details. |
|
||||
// |
|
||||
// You should have received a copy of the GNU General Public License |
|
||||
// along with PRISM; if not, write to the Free Software Foundation, |
|
||||
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
|
||||
// |
|
||||
//============================================================================== |
|
||||
|
|
||||
package abstraction.examples; |
|
||||
|
|
||||
import abstraction.*; |
|
||||
|
|
||||
public class IJ extends IJManual |
|
||||
{ |
|
||||
protected String abstractVarsString() |
|
||||
{ |
|
||||
return "final"; |
|
||||
} |
|
||||
|
|
||||
protected AbstractState concreteToAbstract(int vars[]) |
|
||||
{ |
|
||||
AbstractState state; |
|
||||
int i, j, d, count; |
|
||||
|
|
||||
state = new AbstractState(1); |
|
||||
|
|
||||
count = 0; |
|
||||
for (i = 0; i < N; i++) { |
|
||||
if (vars[i] == 1) count++; |
|
||||
} |
|
||||
|
|
||||
if (count == 1) state.set(0, 0); |
|
||||
//else if (count == N) state.set(0, 0); |
|
||||
else state.set(0, 1); |
|
||||
|
|
||||
return state; |
|
||||
} |
|
||||
|
|
||||
protected boolean isTargetConcreteState(int vars[]) |
|
||||
{ |
|
||||
int i, count = 0; |
|
||||
for (i = 0; i < N; i++) if (vars[i] == 1) count ++; |
|
||||
return (count == 1); |
|
||||
} |
|
||||
|
|
||||
protected boolean isInitialConcreteState(int vars[]) |
|
||||
{ |
|
||||
int i; |
|
||||
for (i = 0; i < N; i++) if (vars[i] == 0) return false; |
|
||||
return true; |
|
||||
} |
|
||||
|
|
||||
protected AbstractState getInitialAbstractState() |
|
||||
{ |
|
||||
AbstractState init; |
|
||||
|
|
||||
init = new AbstractState(1); |
|
||||
init.set(0, 0); |
|
||||
|
|
||||
return init; |
|
||||
} |
|
||||
} |
|
||||
@ -1,130 +0,0 @@ |
|||||
//============================================================================== |
|
||||
// |
|
||||
// Copyright (c) 2002- |
|
||||
// Authors: |
|
||||
// * Dave Parker <david.parker@comlab.ox.ac.uk> (University of Oxford) |
|
||||
// |
|
||||
//------------------------------------------------------------------------------ |
|
||||
// |
|
||||
// This file is part of PRISM. |
|
||||
// |
|
||||
// PRISM is free software; you can redistribute it and/or modify |
|
||||
// it under the terms of the GNU General Public License as published by |
|
||||
// the Free Software Foundation; either version 2 of the License, or |
|
||||
// (at your option) any later version. |
|
||||
// |
|
||||
// PRISM is distributed in the hope that it will be useful, |
|
||||
// but WITHOUT ANY WARRANTY; without even the implied warranty of |
|
||||
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
|
||||
// GNU General Public License for more details. |
|
||||
// |
|
||||
// You should have received a copy of the GNU General Public License |
|
||||
// along with PRISM; if not, write to the Free Software Foundation, |
|
||||
// Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA |
|
||||
// |
|
||||
//============================================================================== |
|
||||
|
|
||||
package abstraction.examples; |
|
||||
|
|
||||
import abstraction.*; |
|
||||
|
|
||||
public class IJManual extends PRISMAbstraction |
|
||||
{ |
|
||||
protected int N; |
|
||||
|
|
||||
/* |
|
||||
* Parse comma-separated command-line argument with model details Returns null if OK, correct format string if not |
|
||||
*/ |
|
||||
|
|
||||
public String modelArgs(String arg) |
|
||||
{ |
|
||||
N = Integer.parseInt(arg); |
|
||||
filename = "data/israeli-jalfon/ij"+arg; |
|
||||
return null; |
|
||||
} |
|
||||
|
|
||||
/* Comma-separated list of names of variables in abstraction */ |
|
||||
|
|
||||
protected String abstractVarsString() |
|
||||
{ |
|
||||
String s = ""; |
|
||||
for (int i = 0; i < N; i++) { |
|
||||
if (i > 0) |
|
||||
s += ","; |
|
||||
s += "d" + i; |
|
||||
} |
|
||||
return s; |
|
||||
} |
|
||||
|
|
||||
/* Abstraction: conversion of concrete to abstract state */ |
|
||||
|
|
||||
protected AbstractState concreteToAbstract(int vars[]) |
|
||||
{ |
|
||||
AbstractState state; |
|
||||
int i, j, d, first, tmp[]; |
|
||||
|
|
||||
state = new AbstractState(N); |
|
||||
|
|
||||
// Temp storage for abstract state |
|
||||
tmp = new int[N]; |
|
||||
for (i = 0; i < N; i++) |
|
||||
tmp[i] = 0; |
|
||||
|
|
||||
// Find first token |
|
||||
first = -1; |
|
||||
for (i = 0; i < N; i++) |
|
||||
if (vars[i] == 1) { |
|
||||
first = i; |
|
||||
break; |
|
||||
} |
|
||||
|
|
||||
// Count distances |
|
||||
if (first > -1) { |
|
||||
d = 0; // current distance |
|
||||
for (i = 0; i < N; i++) { |
|
||||
j = (i + first + 1) % N; |
|
||||
if (vars[j] == 1) { |
|
||||
tmp[d]++; |
|
||||
d = 0; |
|
||||
} else |
|
||||
d++; |
|
||||
} |
|
||||
} |
|
||||
|
|
||||
// Build/return abstract state |
|
||||
for (i = 0; i < N; i++) |
|
||||
state.set(i, tmp[i]); |
|
||||
return state; |
|
||||
} |
|
||||
|
|
||||
protected boolean isTargetConcreteState(int vars[]) |
|
||||
{ |
|
||||
int i, count = 0; |
|
||||
for (i = 0; i < N; i++) |
|
||||
if (vars[i] == 1) |
|
||||
count++; |
|
||||
return (count == 1); |
|
||||
} |
|
||||
|
|
||||
protected boolean isInitialConcreteState(int vars[]) |
|
||||
{ |
|
||||
int i; |
|
||||
for (i = 0; i < N; i++) |
|
||||
if (vars[i] == 0) |
|
||||
return false; |
|
||||
return true; |
|
||||
} |
|
||||
|
|
||||
protected AbstractState getInitialAbstractState() |
|
||||
{ |
|
||||
AbstractState init; |
|
||||
int i; |
|
||||
|
|
||||
init = new AbstractState(N); |
|
||||
init.set(0, N); |
|
||||
for (i = 1; i < N; i++) |
|
||||
init.set(i, 0); |
|
||||
|
|
||||
return init; |
|
||||
} |
|
||||
} |
|
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue