sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

modified selection of benchmarks 

Former-commit-id: a0a00e7383
tempestpy_adaptions
TimQu 9 years ago
parent
5cd8254263
commit
6484e431f5
13 changed files with 114 additions and 31 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 51
      examples/list.sh
  2. 54
      examples/listBenchmarks.sh
  3. 4
      examples/pdtmc/brp/models
  4. 3
      examples/pdtmc/brp_rewards2/models
  5. 5
      examples/pdtmc/brp_rewards4/models
  6. 3
      examples/pdtmc/crowds/models
  7. 4
      examples/pdtmc/nand/models
  8. 4
      examples/pmdp/brp/models
  9. 3
      examples/pmdp/coin2/models
  10. 3
      examples/pmdp/coin4/models
  11. 3
      examples/pmdp/reporter2/models
  12. 3
      examples/pmdp/reporter4/models
  13. 5
      examples/pmdp/zeroconf/models

51
examples/list.sh
View File

@ -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!"

54
examples/listBenchmarks.sh
View File

@ -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

4
examples/pdtmc/brp/models
View File

@ -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

3
examples/pdtmc/brp_rewards2/models
View File

@ -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

5
examples/pdtmc/brp_rewards4/models
View File

@ -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

3
examples/pdtmc/crowds/models
View File

@ -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

4
examples/pdtmc/nand/models
View File

@ -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

4
examples/pmdp/brp/models
View File

@ -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

3
examples/pmdp/coin2/models
View File

@ -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

3
examples/pmdp/coin4/models
View File

@ -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

3
examples/pmdp/reporter2/models
View File

@ -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

3
examples/pmdp/reporter4/models
View File

@ -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

5
examples/pmdp/zeroconf/models
View File

@ -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
Write Preview
Loading…
Cancel
Save