From 121715d1ed0408af7641e58a3dcc4805443693dc Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Fri, 30 Apr 2010 09:33:38 +0000 Subject: [PATCH] Removed (old) abstraction package. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1861 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/Makefile | 6 +- prism/NOTES-ABSTR | 435 --------------- prism/src/abstraction/AbstractMDP.java | 351 ------------ prism/src/abstraction/AbstractRefine.java | 553 ------------------- prism/src/abstraction/AbstractState.java | 73 --- prism/src/abstraction/Makefile | 34 -- prism/src/abstraction/PRISMAbstraction.java | 71 --- prism/src/abstraction/examples/Firewire.java | 82 --- prism/src/abstraction/examples/IJ.java | 80 --- prism/src/abstraction/examples/IJManual.java | 130 ----- 10 files changed, 5 insertions(+), 1810 deletions(-) delete mode 100644 prism/NOTES-ABSTR delete mode 100644 prism/src/abstraction/AbstractMDP.java delete mode 100644 prism/src/abstraction/AbstractRefine.java delete mode 100644 prism/src/abstraction/AbstractState.java delete mode 100644 prism/src/abstraction/Makefile delete mode 100644 prism/src/abstraction/PRISMAbstraction.java delete mode 100644 prism/src/abstraction/examples/Firewire.java delete mode 100644 prism/src/abstraction/examples/IJ.java delete mode 100644 prism/src/abstraction/examples/IJManual.java diff --git a/prism/Makefile b/prism/Makefile index f3ddf590..b0b43d0b 100644 --- a/prism/Makefile +++ b/prism/Makefile @@ -245,7 +245,7 @@ JAVA_INCLUDES = -I $(JAVA_JNI_H_DIR) -I $(JAVA_JNI_MD_H_DIR) # Main part of Makefile # ######################### -MAKE_DIRS = dd jdd odd dv prism mtbdd sparse hybrid parser settings userinterface pepa/compiler simulator jltl2ba jltl2dstar explicit pta abstraction +MAKE_DIRS = dd jdd odd dv prism mtbdd sparse hybrid parser settings userinterface pepa/compiler simulator jltl2ba jltl2dstar explicit pta ifeq ($(OSTYPE),linux) BIN_PRISM=bin/prism @@ -471,6 +471,10 @@ clean_jltl2ba: checks @(cd src/jltl2ba && $(MAKE) -s SRC_DIR="$(SRC_DIR)" CLASSES_DIR="$(CLASSES_DIR)" OBJ_DIR="$(OBJ_DIR)" LIB_DIR="$(LIB_DIR)" EXE="$(EXE)" LIBPREFIX="$(LIBPREFIX)" LIBSUFFIX="$(LIBSUFFIX)" clean) clean_jltl2dstar: checks @(cd src/jltl2dstar && $(MAKE) -s SRC_DIR="$(SRC_DIR)" CLASSES_DIR="$(CLASSES_DIR)" OBJ_DIR="$(OBJ_DIR)" LIB_DIR="$(LIB_DIR)" EXE="$(EXE)" LIBPREFIX="$(LIBPREFIX)" LIBSUFFIX="$(LIBSUFFIX)" clean) +clean_explicit: checks + @(cd src/explicit && $(MAKE) -s SRC_DIR="$(SRC_DIR)" CLASSES_DIR="$(CLASSES_DIR)" OBJ_DIR="$(OBJ_DIR)" LIB_DIR="$(LIB_DIR)" EXE="$(EXE)" LIBPREFIX="$(LIBPREFIX)" LIBSUFFIX="$(LIBSUFFIX)" clean) +clean_pta: checks + @(cd src/pta && $(MAKE) -s SRC_DIR="$(SRC_DIR)" CLASSES_DIR="$(CLASSES_DIR)" OBJ_DIR="$(OBJ_DIR)" LIB_DIR="$(LIB_DIR)" EXE="$(EXE)" LIBPREFIX="$(LIBPREFIX)" LIBSUFFIX="$(LIBSUFFIX)" clean) checks: @(if [ "$(OSTYPE)" != "linux" -a "$(OSTYPE)" != "solaris" -a "$(OSTYPE)" != "cygwin" -a "$(OSTYPE)" != "darwin" ]; then \ diff --git a/prism/NOTES-ABSTR b/prism/NOTES-ABSTR deleted file mode 100644 index 0f54c96f..00000000 --- a/prism/NOTES-ABSTR +++ /dev/null @@ -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 - diff --git a/prism/src/abstraction/AbstractMDP.java b/prism/src/abstraction/AbstractMDP.java deleted file mode 100644 index 2103bc95..00000000 --- a/prism/src/abstraction/AbstractMDP.java +++ /dev/null @@ -1,351 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Dave Parker (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 mdp; - public ArrayList 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(); - 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(); - set.add(iLast); - mdpTmp[mapping[iLast]].put(distrs, set); - in.close(); - - // build MDP (convert (sets to lists) - mdp = new ArrayList(nAbstract); - mdpStates = new ArrayList(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); - } - } -} diff --git a/prism/src/abstraction/AbstractRefine.java b/prism/src/abstraction/AbstractRefine.java deleted file mode 100644 index 9894e931..00000000 --- a/prism/src/abstraction/AbstractRefine.java +++ /dev/null @@ -1,553 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Dave Parker (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 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()+" "; - } - - 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); - } - - -} diff --git a/prism/src/abstraction/AbstractState.java b/prism/src/abstraction/AbstractState.java deleted file mode 100644 index 122aacec..00000000 --- a/prism/src/abstraction/AbstractState.java +++ /dev/null @@ -1,73 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Dave Parker (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; - } -} diff --git a/prism/src/abstraction/Makefile b/prism/src/abstraction/Makefile deleted file mode 100644 index 6a89592e..00000000 --- a/prism/src/abstraction/Makefile +++ /dev/null @@ -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 - -################################################# diff --git a/prism/src/abstraction/PRISMAbstraction.java b/prism/src/abstraction/PRISMAbstraction.java deleted file mode 100644 index b590ffe3..00000000 --- a/prism/src/abstraction/PRISMAbstraction.java +++ /dev/null @@ -1,71 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Dave Parker (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; - } -} diff --git a/prism/src/abstraction/examples/Firewire.java b/prism/src/abstraction/examples/Firewire.java deleted file mode 100644 index 987fe780..00000000 --- a/prism/src/abstraction/examples/Firewire.java +++ /dev/null @@ -1,82 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Dave Parker (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; - } -} diff --git a/prism/src/abstraction/examples/IJ.java b/prism/src/abstraction/examples/IJ.java deleted file mode 100644 index 975fa19f..00000000 --- a/prism/src/abstraction/examples/IJ.java +++ /dev/null @@ -1,80 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Dave Parker (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; - } -} diff --git a/prism/src/abstraction/examples/IJManual.java b/prism/src/abstraction/examples/IJManual.java deleted file mode 100644 index 458dc233..00000000 --- a/prism/src/abstraction/examples/IJManual.java +++ /dev/null @@ -1,130 +0,0 @@ -//============================================================================== -// -// Copyright (c) 2002- -// Authors: -// * Dave Parker (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; - } -}