parallel execution of benchmarks and larger models

Former-commit-id: 1abf08d530

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

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

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

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

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

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

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

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

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

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

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

src/modelchecker/region/AbstractSparseRegionModelChecker.cpp

@@ -198,7 +198,7 @@ namespace storm {
             template<typename ParametricSparseModelType, typename ConstantType>
             void AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::refineAndCheckRegion(std::vector<ParameterRegion<ParametricType>>& 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;