diff --git a/examples/list.sh b/examples/list.sh new file mode 100755 index 000000000..284215ddc --- /dev/null +++ b/examples/list.sh @@ -0,0 +1,51 @@ +#!/bin/bash +executable="timeout 3600 ../build/src/storm" +arguments="-bisim -i 1000000 --parametric --parametricRegion --region:refinement 0.05 --region:samplemode off" +mkdir results +# pdtmcs +$executable -s ./pdtmc/crowds/crowds.pm -const CrowdSize=10,TotalRuns=5 --prop ./pdtmc/crowds/crowds.prctl --region:regions "0.000010<=PF<=0.999990,0.000010<=badC<=0.999990;" $arguments | tee ./results/pdtmc_crowds.pm-constCrowdSize_10_TotalRuns_5.log & +$executable -s ./pdtmc/crowds/crowds.pm -const CrowdSize=20,TotalRuns=10 --prop ./pdtmc/crowds/crowds.prctl --region:regions "0.000010<=PF<=0.999990,0.000010<=badC<=0.999990;" $arguments | tee ./results/pdtmc_crowds.pm-constCrowdSize_20_TotalRuns_10.log & + + +$executable -s ./pdtmc/nand/nand.pm -const N=10,K=5 --prop ./pdtmc/nand/nand.prctl --region:regions "0.000010<=perr<=0.999990,0.000010<=prob1<=0.999990;" $arguments | tee ./results/pdtmc_nand.pm-constN_10_K_5.log & +$executable -s ./pdtmc/nand/nand.pm -const N=25,K=5 --prop ./pdtmc/nand/nand.prctl --region:regions "0.000010<=perr<=0.999990,0.000010<=prob1<=0.999990;" $arguments | tee ./results/pdtmc_nand.pm-constN_25_K_5.log & + +wait + +$executable -s ./pdtmc/brp_rewards2/brp_rewards2.pm -const N=512,MAX=5 --prop ./pdtmc/brp_rewards2/brp_rewards2.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pK<=0.999990;" $arguments | tee ./results/pdtmc_brp_rewards2.pm-constN_512_MAX_5.log & +$executable -s ./pdtmc/brp_rewards2/brp_rewards2.pm -const N=4096,MAX=5 --prop ./pdtmc/brp_rewards2/brp_rewards2.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pK<=0.999990;" $arguments | tee ./results/pdtmc_brp_rewards2.pm-constN_4096_MAX_5.log & + + +$executable -s ./pdtmc/brp_rewards4/brp_rewards4.pm -const N=256,MAX=5 --prop ./pdtmc/brp_rewards4/brp_rewards4.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pK<=0.999990,0.000010<=TOMsg<=0.999990,0.000010<=TOAck<=0.999990;" $arguments | tee ./results/pdtmc_brp_rewards4.pm-constN_256_MAX_5.log & +$executable -s ./pdtmc/brp_rewards4/brp_rewards4.pm -const N=5012,MAX=5 --prop ./pdtmc/brp_rewards4/brp_rewards4.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pK<=0.999990,0.000010<=TOMsg<=0.999990,0.000010<=TOAck<=0.999990;" $arguments | tee ./results/pdtmc_brp_rewards4.pm-constN_5012_MAX_5.log & + +$executable -s ./pdtmc/brp/brp.pm -const N=256,MAX=5 --prop ./pdtmc/brp/brp.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pK<=0.999990;" $arguments | tee ./results/pdtmc_brp.pm-constN_256_MAX_5.log & +$executable -s ./pdtmc/brp/brp.pm -const N=4096,MAX=5 --prop ./pdtmc/brp/brp.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pK<=0.999990;" $arguments | tee ./results/pdtmc_brp.pm-constN_4096_MAX_5.log & + +wait + +# pmdps +arguments="-i 1000000 --parametric --parametricRegion --region:refinement 0.05 --region:samplemode off" + +$executable -s ./pmdp/brp/brp.pm -const N=256,MAX=5 --prop ./pmdp/brp/brp.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pK<=0.999990;" $arguments | tee ./results/pmdp_brp.pm-constN_256_MAX_5.log & +$executable -s ./pmdp/brp/brp.pm -const N=4096,MAX=5 --prop ./pmdp/brp/brp.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pK<=0.999990;" $arguments | tee ./results/pmdp_brp.pm-constN_4096_MAX_5.log & + +$executable -s ./pmdp/coin2/coin2.pm -const K=2 --prop ./pmdp/coin2/coin2.prctl --region:regions "0.000010<=p1<=0.999990,0.000010<=p2<=0.999990;" $arguments | tee ./results/pmdp_coin2.pm-constK_2.log & +$executable -s ./pmdp/coin2/coin2.pm -const K=32 --prop ./pmdp/coin2/coin2.prctl --region:regions "0.000010<=p1<=0.999990,0.000010<=p2<=0.999990;" $arguments | tee ./results/pmdp_coin2.pm-constK_32.log & + +$executable -s ./pmdp/coin4/coin4.pm -const K=2 --prop ./pmdp/coin4/coin4.prctl --region:regions "0.000010<=p1<=0.999990,0.000010<=p2<=0.999990,0.000010<=p3<=0.999990,0.000010<=p4<=0.999990;" $arguments | tee ./results/pmdp_coin4.pm-constK_2.log & +$executable -s ./pmdp/coin4/coin4.pm -const K=4 --prop ./pmdp/coin4/coin4.prctl --region:regions "0.000010<=p1<=0.999990,0.000010<=p2<=0.999990,0.000010<=p3<=0.999990,0.000010<=p4<=0.999990;" $arguments | tee ./results/pmdp_coin4.pm-constK_4.log & + +wait + +$executable -s ./pmdp/zeroconf/zeroconf.pm -const K=2 --prop ./pmdp/zeroconf/zeroconf.prctl --region:regions "0.000010<=loss<=0.999990,0.000010<=old<=0.999990;" $arguments | tee ./results/pmdp_zeroconf.pm-constK_2.log & +$executable -s ./pmdp/zeroconf/zeroconf.pm -const K=5 --prop ./pmdp/zeroconf/zeroconf.prctl --region:regions "0.000010<=loss<=0.999990,0.000010<=old<=0.999990;" $arguments | tee ./results/pmdp_zeroconf.pm-constK_5.log & + +$executable -s ./pmdp/reporter2/reporter2.pm -const Xsize=6,Ysize=6,MAXTRIES=2,B=2 --prop ./pmdp/reporter2/reporter2.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pH<=0.999990;" $arguments | tee ./results/pmdp_reporter2.pm-constXsize_6_Ysize_6_MAXTRIES_2_B_2.log & +$executable -s ./pmdp/reporter2/reporter2.pm -const Xsize=100,Ysize=100,MAXTRIES=10,B=10 --prop ./pmdp/reporter2/reporter2.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pH<=0.999990;" $arguments | tee ./results/pmdp_reporter2.pm-constXsize_100_Ysize_100_MAXTRIES_10_B_10.log & + +$executable -s ./pmdp/reporter4/reporter4.pm -const Xsize=6,Ysize=6,MAXTRIES=2,B=2 --prop ./pmdp/reporter4/reporter4.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pH<=0.999990,0.000010<=pLDiff<=0.999990,0.000010<=pHDiff<=0.999990;" $arguments | tee ./results/pmdp_reporter4.pm-constXsize_6_Ysize_6_MAXTRIES_2_B_2.log & +$executable -s ./pmdp/reporter4/reporter4.pm -const Xsize=10,Ysize=10,MAXTRIES=3,B=3 --prop ./pmdp/reporter4/reporter4.prctl --region:regions "0.000010<=pL<=0.999990,0.000010<=pH<=0.999990,0.000010<=pLDiff<=0.999990,0.000010<=pHDiff<=0.999990;" $arguments | tee ./results/pmdp_reporter4.pm-constXsize_10_Ysize_10_MAXTRIES_3_B_3.log & + +wait +echo "done!" diff --git a/examples/listBenchmarks.sh b/examples/listBenchmarks.sh new file mode 100755 index 000000000..7bdf33279 --- /dev/null +++ b/examples/listBenchmarks.sh @@ -0,0 +1,54 @@ +#!/bin/bash + +if [ "$#" != 1 ]; +then + echo "Wrong number of arguments! Provide a filename for the results!" +elif [ -a $1 ]; then + echo "File for results already exists!" +else + + +DIR="." + +echo '#!/bin/bash' >> $1 +echo 'executable="timeout 3600 ../build/src/storm"' >> $1 +echo 'arguments="-bisim -i 1000000 --parametric --parametricRegion --region:refinement 0.05 --region:samplemode off"' >> $1 +echo "mkdir results" >> $1 + + +declare -a modeltypes=("pdtmc" "pmdp") + +for modeltype in "${modeltypes[@]}" +do +if [ "$modeltype" == "pdtmc" ]; +then + declare -a models=("crowds" "nand" "brp_rewards2" "brp_rewards4" "brp") + dobisim="-bisim" +else + declare -a models=("brp" "coin2" "coin4" "zeroconf" "reporter2" "reporter4") + dobisim="" +fi + echo "# $modeltype""s" >> $1 + for model in "${models[@]}" + do + modelfolder="$DIR/$modeltype/$model" + suffix="-" + while read instance; + do + + output='$executable ' + output="$output""-s $modelfolder/$instance --prop $modelfolder/$model.prctl --region:regions " + region=$(head -n 1 $modelfolder/$model"_space.txt") + region="$(echo -e "${region}" | tr -d '[[:space:]]')" + output="$output"'"'$region'" $arguments | tee ' + instanceString="$(echo -e "${instance}" | tr -d '[[:space:]]')" + instanceString=${instanceString//[,=]/_} + output="$output""./results/$modeltype""_$instanceString.log &" + echo $output >> $1 + + done < "$modelfolder/models" + + done +done +echo 'wait' >> $1 +fi diff --git a/examples/pdtmc/brp/models b/examples/pdtmc/brp/models index d808cf7e1..b692fffb6 100644 --- a/examples/pdtmc/brp/models +++ b/examples/pdtmc/brp/models @@ -1,4 +1,2 @@ brp.pm -const N=256,MAX=5 -brp.pm -const N=512,MAX=5 -brp.pm -const N=1024,MAX=5 -brp.pm -const N=2048,MAX=5 +brp.pm -const N=4096,MAX=5 diff --git a/examples/pdtmc/brp_rewards2/models b/examples/pdtmc/brp_rewards2/models index 26cd54c78..c4ac2bb5e 100644 --- a/examples/pdtmc/brp_rewards2/models +++ b/examples/pdtmc/brp_rewards2/models @@ -1,3 +1,2 @@ brp_rewards2.pm -const N=512,MAX=5 -brp_rewards2.pm -const N=1024,MAX=5 -brp_rewards2.pm -const N=2048,MAX=5 +brp_rewards2.pm -const N=4096,MAX=5 diff --git a/examples/pdtmc/brp_rewards4/models b/examples/pdtmc/brp_rewards4/models index 3a5274a48..e3656e3a8 100644 --- a/examples/pdtmc/brp_rewards4/models +++ b/examples/pdtmc/brp_rewards4/models @@ -1,3 +1,2 @@ -brp_rewards4.pm -const N=512,MAX=5 -brp_rewards4.pm -const N=1024,MAX=5 -brp_rewards4.pm -const N=2048,MAX=5 +brp_rewards4.pm -const N=256,MAX=5 +brp_rewards4.pm -const N=5012,MAX=5 diff --git a/examples/pdtmc/crowds/models b/examples/pdtmc/crowds/models index b5484e521..fdfc13cee 100644 --- a/examples/pdtmc/crowds/models +++ b/examples/pdtmc/crowds/models @@ -1,3 +1,2 @@ crowds.pm -const CrowdSize=10,TotalRuns=5 -crowds.pm -const CrowdSize=15,TotalRuns=5 -crowds.pm -const CrowdSize=20,TotalRuns=5 +crowds.pm -const CrowdSize=20,TotalRuns=10 diff --git a/examples/pdtmc/nand/models b/examples/pdtmc/nand/models index d4203b0d4..a41532a76 100644 --- a/examples/pdtmc/nand/models +++ b/examples/pdtmc/nand/models @@ -1,4 +1,2 @@ nand.pm -const N=10,K=5 -nand.pm -const N=20,K=5 -nand.pm -const N=30,K=5 -nand.pm -const N=40,K=5 +nand.pm -const N=25,K=5 diff --git a/examples/pmdp/brp/models b/examples/pmdp/brp/models index d808cf7e1..b692fffb6 100644 --- a/examples/pmdp/brp/models +++ b/examples/pmdp/brp/models @@ -1,4 +1,2 @@ brp.pm -const N=256,MAX=5 -brp.pm -const N=512,MAX=5 -brp.pm -const N=1024,MAX=5 -brp.pm -const N=2048,MAX=5 +brp.pm -const N=4096,MAX=5 diff --git a/examples/pmdp/coin2/models b/examples/pmdp/coin2/models index 0650def19..00f6f4cd9 100644 --- a/examples/pmdp/coin2/models +++ b/examples/pmdp/coin2/models @@ -1,5 +1,2 @@ coin2.pm -const K=2 -coin2.pm -const K=8 coin2.pm -const K=32 -coin2.pm -const K=64 -coin2.pm -const K=128 diff --git a/examples/pmdp/coin4/models b/examples/pmdp/coin4/models index 37a8aa0a4..1544a9647 100644 --- a/examples/pmdp/coin4/models +++ b/examples/pmdp/coin4/models @@ -1,5 +1,2 @@ coin4.pm -const K=2 coin4.pm -const K=4 -coin4.pm -const K=6 -coin4.pm -const K=7 -coin4.pm -const K=8 diff --git a/examples/pmdp/reporter2/models b/examples/pmdp/reporter2/models index 4f4828654..167d07df6 100644 --- a/examples/pmdp/reporter2/models +++ b/examples/pmdp/reporter2/models @@ -1,5 +1,2 @@ reporter2.pm -const Xsize=6,Ysize=6,MAXTRIES=2,B=2 -reporter2.pm -const Xsize=25,Ysize=25,MAXTRIES=5,B=5 -reporter2.pm -const Xsize=50,Ysize=50,MAXTRIES=8,B=8 -reporter2.pm -const Xsize=75,Ysize=75,MAXTRIES=10,B=10 reporter2.pm -const Xsize=100,Ysize=100,MAXTRIES=10,B=10 diff --git a/examples/pmdp/reporter4/models b/examples/pmdp/reporter4/models index 86c5e92ac..f9a0e194c 100644 --- a/examples/pmdp/reporter4/models +++ b/examples/pmdp/reporter4/models @@ -1,3 +1,2 @@ reporter4.pm -const Xsize=6,Ysize=6,MAXTRIES=2,B=2 -reporter4.pm -const Xsize=25,Ysize=25,MAXTRIES=5,B=5 -reporter4.pm -const Xsize=50,Ysize=50,MAXTRIES=8,B=8 +reporter4.pm -const Xsize=10,Ysize=10,MAXTRIES=3,B=3 diff --git a/examples/pmdp/zeroconf/models b/examples/pmdp/zeroconf/models index ad243cdcb..07d1fa6b7 100644 --- a/examples/pmdp/zeroconf/models +++ b/examples/pmdp/zeroconf/models @@ -1,5 +1,2 @@ zeroconf.pm -const K=2 -zeroconf.pm -const K=4 -zeroconf.pm -const K=6 -zeroconf.pm -const K=7 -zeroconf.pm -const K=8 +zeroconf.pm -const K=5