From 5f678f96ae9a9d4cb85e8bad505585b7b6144a67 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 20 Jan 2016 14:42:04 +0100 Subject: [PATCH] parallel execution of benchmarks and larger models Former-commit-id: 1abf08d530c7afcca9d8878ef82dfa3b3c5db481 --- examples/benchmarkRegions.sh | 25 ++++++++++++------- examples/benchmarkRegionsRefinement.sh | 24 +++++++++++------- examples/pdtmc/brp/models | 1 + examples/pdtmc/brp_rewards2/models | 1 + examples/pdtmc/brp_rewards4/models | 1 + examples/pdtmc/crowds/models | 1 + examples/pdtmc/nand/models | 1 + examples/pmdp/brp/models | 1 + examples/pmdp/coin4/models | 2 ++ examples/pmdp/reporter2/models | 1 + examples/pmdp/zeroconf/models | 1 + .../AbstractSparseRegionModelChecker.cpp | 2 +- 12 files changed, 42 insertions(+), 19 deletions(-) diff --git a/examples/benchmarkRegions.sh b/examples/benchmarkRegions.sh index 568d96ef8..136ffeee1 100755 --- a/examples/benchmarkRegions.sh +++ b/examples/benchmarkRegions.sh @@ -24,23 +24,30 @@ then dobisim="-bisim" else declare -a models=("brp" "coin2" "coin4" "zeroconf" "reporter2" "reporter4") -# declare -a models=( "zeroconf" "reporter2" "reporter4") dobisim="" fi for model in "${models[@]}" do modelfolder="$DIR/$modeltype/$model" + suffix="-" while read instance; do - - echo "Working on $modelfolder/$instance" - echo >> $1 - echo "-------------------------------------------------------------" >> $1 - echo "---- WORKING ON: $modelfolder/$instance ----" >>$1 - echo "-------------------------------------------------------------" >> $1 - $timeout "$executable" -s $modelfolder/$instance $dobisim --prop $modelfolder/$model.prctl --parametric --parametricRegion --region:regionfile $modelfolder/$model"_regions.txt" >> $1 + suffix="1$suffix" + echo "Working on $modelfolder/$instance" + echo "___WORKING ON: $modelfolder/$instance""____________" >>$1$suffix + echo "_________________________________________________________________________________" >> $1$suffix + $timeout "$executable" -s $modelfolder/$instance $dobisim --prop $modelfolder/$model.prctl --parametric --parametricRegion --region:regionfile $modelfolder/$model"_regions.txt" >> $1$suffix & + done < "$modelfolder/models" + done < "$modelfolder/models" + wait + # write logs into result file + suffix="-" + while read instance; + do + suffix="1$suffix" + cat $1$suffix >> $1 + rm $1$suffix done < "$modelfolder/models" - done done fi diff --git a/examples/benchmarkRegionsRefinement.sh b/examples/benchmarkRegionsRefinement.sh index 55bcaf9bf..01229bbb3 100755 --- a/examples/benchmarkRegionsRefinement.sh +++ b/examples/benchmarkRegionsRefinement.sh @@ -24,23 +24,29 @@ then dobisim="-bisim" else declare -a models=("brp" "coin2" "coin4" "zeroconf" "reporter2" "reporter4") - #declare -a models=( "zeroconf" "reporter2" "reporter4") dobisim="" fi for model in "${models[@]}" do modelfolder="$DIR/$modeltype/$model" + suffix="-" while read instance; do - - echo "Working on $modelfolder/$instance" - echo >> $1 - echo "-------------------------------------------------------------" >> $1 - echo "---- WORKING ON: $modelfolder/$instance ----" >>$1 - echo "-------------------------------------------------------------" >> $1 - $timeout "$executable" -s $modelfolder/$instance $dobisim --prop $modelfolder/$model.prctl --parametric --parametricRegion --region:regionfile $modelfolder/$model"_space.txt" --region:refinement 0.05 --region:samplemode off >> $1 + suffix="1$suffix" + echo "Working on $modelfolder/$instance" + echo "___WORKING ON: $modelfolder/$instance""____________" >>$1$suffix + echo "_________________________________________________________________________________" >> $1$suffix + $timeout "$executable" -s $modelfolder/$instance $dobisim --prop $modelfolder/$model.prctl --parametric --parametricRegion --region:regionfile $modelfolder/$model"_space.txt" --region:refinement 0.05 --region:samplemode off >> "$1$suffix" & + done < "$modelfolder/models" + wait + # write logs into result file + suffix="-" + while read instance; + do + suffix="1$suffix" + cat $1$suffix >> $1 + rm $1$suffix done < "$modelfolder/models" - done done fi diff --git a/examples/pdtmc/brp/models b/examples/pdtmc/brp/models index afe9c2e13..d808cf7e1 100644 --- a/examples/pdtmc/brp/models +++ b/examples/pdtmc/brp/models @@ -1,3 +1,4 @@ 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 diff --git a/examples/pdtmc/brp_rewards2/models b/examples/pdtmc/brp_rewards2/models index b12533a0b..26cd54c78 100644 --- a/examples/pdtmc/brp_rewards2/models +++ b/examples/pdtmc/brp_rewards2/models @@ -1,2 +1,3 @@ brp_rewards2.pm -const N=512,MAX=5 brp_rewards2.pm -const N=1024,MAX=5 +brp_rewards2.pm -const N=2048,MAX=5 diff --git a/examples/pdtmc/brp_rewards4/models b/examples/pdtmc/brp_rewards4/models index 13a317bf0..3a5274a48 100644 --- a/examples/pdtmc/brp_rewards4/models +++ b/examples/pdtmc/brp_rewards4/models @@ -1,2 +1,3 @@ brp_rewards4.pm -const N=512,MAX=5 brp_rewards4.pm -const N=1024,MAX=5 +brp_rewards4.pm -const N=2048,MAX=5 diff --git a/examples/pdtmc/crowds/models b/examples/pdtmc/crowds/models index 1ae914ac9..b5484e521 100644 --- a/examples/pdtmc/crowds/models +++ b/examples/pdtmc/crowds/models @@ -1,2 +1,3 @@ crowds.pm -const CrowdSize=10,TotalRuns=5 crowds.pm -const CrowdSize=15,TotalRuns=5 +crowds.pm -const CrowdSize=20,TotalRuns=5 diff --git a/examples/pdtmc/nand/models b/examples/pdtmc/nand/models index 4337d6baa..d4203b0d4 100644 --- a/examples/pdtmc/nand/models +++ b/examples/pdtmc/nand/models @@ -1,3 +1,4 @@ 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 diff --git a/examples/pmdp/brp/models b/examples/pmdp/brp/models index afe9c2e13..d808cf7e1 100644 --- a/examples/pmdp/brp/models +++ b/examples/pmdp/brp/models @@ -1,3 +1,4 @@ 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 diff --git a/examples/pmdp/coin4/models b/examples/pmdp/coin4/models index 3083a6829..37a8aa0a4 100644 --- a/examples/pmdp/coin4/models +++ b/examples/pmdp/coin4/models @@ -1,3 +1,5 @@ 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 5683a5758..4f4828654 100644 --- a/examples/pmdp/reporter2/models +++ b/examples/pmdp/reporter2/models @@ -2,3 +2,4 @@ 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/zeroconf/models b/examples/pmdp/zeroconf/models index ae90eae00..ad243cdcb 100644 --- a/examples/pmdp/zeroconf/models +++ b/examples/pmdp/zeroconf/models @@ -2,3 +2,4 @@ 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 diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp index 9311882d5..dcb3d213b 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp @@ -198,7 +198,7 @@ namespace storm { template void AbstractSparseRegionModelChecker::refineAndCheckRegion(std::vector>& regions, double const& refinementThreshold) { STORM_LOG_DEBUG("Applying refinement on region: " << regions.front().toString() << "."); - std::cout << "Applying refinement on region: " << regions.front().toString(); + std::cout << "Applying refinement on region: " << regions.front().toString() << std::endl; std::cout.flush(); CoefficientType areaOfParameterSpace = regions.front().area(); uint_fast64_t indexOfCurrentRegion=0;