diff --git a/examples/benchmarkRegions.sh b/examples/benchmarkRegions.sh
index 0cc0d7a62..568d96ef8 100755
--- a/examples/benchmarkRegions.sh
+++ b/examples/benchmarkRegions.sh
@@ -6,20 +6,25 @@ then
elif [ -a $1 ]; then
echo "File for results already exists!"
else
+
+
DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+
executable=$DIR/../build/src/storm
+timeout="timeout 3600"
+
declare -a modeltypes=("pdtmc" "pmdp")
for modeltype in "${modeltypes[@]}"
do
if [ "$modeltype" == "pdtmc" ];
then
-# declare -a models=("crowds" "nand" "brp_rewards2" "brp_rewards4" "brp")
+ declare -a models=("crowds" "nand" "brp_rewards2" "brp_rewards4" "brp")
dobisim="-bisim"
else
-# declare -a models=("brp" "coin2" "coin4" "zeroconf" "reporter2" "reporter4")
- declare -a models=( "zeroconf" "reporter2" "reporter4")
+ declare -a models=("brp" "coin2" "coin4" "zeroconf" "reporter2" "reporter4")
+# declare -a models=( "zeroconf" "reporter2" "reporter4")
dobisim=""
fi
for model in "${models[@]}"
@@ -33,7 +38,7 @@ fi
echo "-------------------------------------------------------------" >> $1
echo "---- WORKING ON: $modelfolder/$instance ----" >>$1
echo "-------------------------------------------------------------" >> $1
- "$executable" -s $modelfolder/$instance $dobisim --prop $modelfolder/$model.prctl --parametric --parametricRegion --region:regionfile $modelfolder/$model"_regions.txt" >> $1
+ $timeout "$executable" -s $modelfolder/$instance $dobisim --prop $modelfolder/$model.prctl --parametric --parametricRegion --region:regionfile $modelfolder/$model"_regions.txt" >> $1
done < "$modelfolder/models"
done
diff --git a/examples/benchmarkRegionsRefinement.sh b/examples/benchmarkRegionsRefinement.sh
new file mode 100755
index 000000000..55bcaf9bf
--- /dev/null
+++ b/examples/benchmarkRegionsRefinement.sh
@@ -0,0 +1,46 @@
+#!/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="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+
+executable=$DIR/../build/src/storm
+
+timeout="timeout 3600"
+
+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")
+ #declare -a models=( "zeroconf" "reporter2" "reporter4")
+ dobisim=""
+fi
+ for model in "${models[@]}"
+ do
+ modelfolder="$DIR/$modeltype/$model"
+ 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
+ done < "$modelfolder/models"
+
+ done
+done
+fi
diff --git a/examples/pdtmc/brp/brp_space.txt b/examples/pdtmc/brp/brp_space.txt
new file mode 100644
index 000000000..444b98e90
--- /dev/null
+++ b/examples/pdtmc/brp/brp_space.txt
@@ -0,0 +1,2 @@
+0.000010<=pL<=0.999990, 0.000010<=pK<=0.999990;
+
diff --git a/examples/pdtmc/brp/models b/examples/pdtmc/brp/models
index 15dc2b545..afe9c2e13 100644
--- a/examples/pdtmc/brp/models
+++ b/examples/pdtmc/brp/models
@@ -1,5 +1,3 @@
brp.pm -const N=256,MAX=5
brp.pm -const N=512,MAX=5
brp.pm -const N=1024,MAX=5
-
-
diff --git a/examples/pdtmc/brp_rewards2/brp_rewards2_regions.txt b/examples/pdtmc/brp_rewards2/brp_rewards2_regions.txt
deleted file mode 100644
index c1c19ee3b..000000000
--- a/examples/pdtmc/brp_rewards2/brp_rewards2_regions.txt
+++ /dev/null
@@ -1,625 +0,0 @@
-0.000010<=pL<=0.040000, 0.000010<=pK<=0.040000;
-0.000010<=pL<=0.040000, 0.040000<=pK<=0.080000;
-0.000010<=pL<=0.040000, 0.080000<=pK<=0.120000;
-0.000010<=pL<=0.040000, 0.120000<=pK<=0.160000;
-0.000010<=pL<=0.040000, 0.160000<=pK<=0.200000;
-0.000010<=pL<=0.040000, 0.200000<=pK<=0.240000;
-0.000010<=pL<=0.040000, 0.240000<=pK<=0.280000;
-0.000010<=pL<=0.040000, 0.280000<=pK<=0.320000;
-0.000010<=pL<=0.040000, 0.320000<=pK<=0.360000;
-0.000010<=pL<=0.040000, 0.360000<=pK<=0.400000;
-0.000010<=pL<=0.040000, 0.400000<=pK<=0.440000;
-0.000010<=pL<=0.040000, 0.440000<=pK<=0.480000;
-0.000010<=pL<=0.040000, 0.480000<=pK<=0.520000;
-0.000010<=pL<=0.040000, 0.520000<=pK<=0.560000;
-0.000010<=pL<=0.040000, 0.560000<=pK<=0.600000;
-0.000010<=pL<=0.040000, 0.600000<=pK<=0.640000;
-0.000010<=pL<=0.040000, 0.640000<=pK<=0.680000;
-0.000010<=pL<=0.040000, 0.680000<=pK<=0.720000;
-0.000010<=pL<=0.040000, 0.720000<=pK<=0.760000;
-0.000010<=pL<=0.040000, 0.760000<=pK<=0.800000;
-0.000010<=pL<=0.040000, 0.800000<=pK<=0.840000;
-0.000010<=pL<=0.040000, 0.840000<=pK<=0.880000;
-0.000010<=pL<=0.040000, 0.880000<=pK<=0.920000;
-0.000010<=pL<=0.040000, 0.920000<=pK<=0.960000;
-0.000010<=pL<=0.040000, 0.960000<=pK<=0.999990;
-0.040000<=pL<=0.080000, 0.000010<=pK<=0.040000;
-0.040000<=pL<=0.080000, 0.040000<=pK<=0.080000;
-0.040000<=pL<=0.080000, 0.080000<=pK<=0.120000;
-0.040000<=pL<=0.080000, 0.120000<=pK<=0.160000;
-0.040000<=pL<=0.080000, 0.160000<=pK<=0.200000;
-0.040000<=pL<=0.080000, 0.200000<=pK<=0.240000;
-0.040000<=pL<=0.080000, 0.240000<=pK<=0.280000;
-0.040000<=pL<=0.080000, 0.280000<=pK<=0.320000;
-0.040000<=pL<=0.080000, 0.320000<=pK<=0.360000;
-0.040000<=pL<=0.080000, 0.360000<=pK<=0.400000;
-0.040000<=pL<=0.080000, 0.400000<=pK<=0.440000;
-0.040000<=pL<=0.080000, 0.440000<=pK<=0.480000;
-0.040000<=pL<=0.080000, 0.480000<=pK<=0.520000;
-0.040000<=pL<=0.080000, 0.520000<=pK<=0.560000;
-0.040000<=pL<=0.080000, 0.560000<=pK<=0.600000;
-0.040000<=pL<=0.080000, 0.600000<=pK<=0.640000;
-0.040000<=pL<=0.080000, 0.640000<=pK<=0.680000;
-0.040000<=pL<=0.080000, 0.680000<=pK<=0.720000;
-0.040000<=pL<=0.080000, 0.720000<=pK<=0.760000;
-0.040000<=pL<=0.080000, 0.760000<=pK<=0.800000;
-0.040000<=pL<=0.080000, 0.800000<=pK<=0.840000;
-0.040000<=pL<=0.080000, 0.840000<=pK<=0.880000;
-0.040000<=pL<=0.080000, 0.880000<=pK<=0.920000;
-0.040000<=pL<=0.080000, 0.920000<=pK<=0.960000;
-0.040000<=pL<=0.080000, 0.960000<=pK<=0.999990;
-0.080000<=pL<=0.120000, 0.000010<=pK<=0.040000;
-0.080000<=pL<=0.120000, 0.040000<=pK<=0.080000;
-0.080000<=pL<=0.120000, 0.080000<=pK<=0.120000;
-0.080000<=pL<=0.120000, 0.120000<=pK<=0.160000;
-0.080000<=pL<=0.120000, 0.160000<=pK<=0.200000;
-0.080000<=pL<=0.120000, 0.200000<=pK<=0.240000;
-0.080000<=pL<=0.120000, 0.240000<=pK<=0.280000;
-0.080000<=pL<=0.120000, 0.280000<=pK<=0.320000;
-0.080000<=pL<=0.120000, 0.320000<=pK<=0.360000;
-0.080000<=pL<=0.120000, 0.360000<=pK<=0.400000;
-0.080000<=pL<=0.120000, 0.400000<=pK<=0.440000;
-0.080000<=pL<=0.120000, 0.440000<=pK<=0.480000;
-0.080000<=pL<=0.120000, 0.480000<=pK<=0.520000;
-0.080000<=pL<=0.120000, 0.520000<=pK<=0.560000;
-0.080000<=pL<=0.120000, 0.560000<=pK<=0.600000;
-0.080000<=pL<=0.120000, 0.600000<=pK<=0.640000;
-0.080000<=pL<=0.120000, 0.640000<=pK<=0.680000;
-0.080000<=pL<=0.120000, 0.680000<=pK<=0.720000;
-0.080000<=pL<=0.120000, 0.720000<=pK<=0.760000;
-0.080000<=pL<=0.120000, 0.760000<=pK<=0.800000;
-0.080000<=pL<=0.120000, 0.800000<=pK<=0.840000;
-0.080000<=pL<=0.120000, 0.840000<=pK<=0.880000;
-0.080000<=pL<=0.120000, 0.880000<=pK<=0.920000;
-0.080000<=pL<=0.120000, 0.920000<=pK<=0.960000;
-0.080000<=pL<=0.120000, 0.960000<=pK<=0.999990;
-0.120000<=pL<=0.160000, 0.000010<=pK<=0.040000;
-0.120000<=pL<=0.160000, 0.040000<=pK<=0.080000;
-0.120000<=pL<=0.160000, 0.080000<=pK<=0.120000;
-0.120000<=pL<=0.160000, 0.120000<=pK<=0.160000;
-0.120000<=pL<=0.160000, 0.160000<=pK<=0.200000;
-0.120000<=pL<=0.160000, 0.200000<=pK<=0.240000;
-0.120000<=pL<=0.160000, 0.240000<=pK<=0.280000;
-0.120000<=pL<=0.160000, 0.280000<=pK<=0.320000;
-0.120000<=pL<=0.160000, 0.320000<=pK<=0.360000;
-0.120000<=pL<=0.160000, 0.360000<=pK<=0.400000;
-0.120000<=pL<=0.160000, 0.400000<=pK<=0.440000;
-0.120000<=pL<=0.160000, 0.440000<=pK<=0.480000;
-0.120000<=pL<=0.160000, 0.480000<=pK<=0.520000;
-0.120000<=pL<=0.160000, 0.520000<=pK<=0.560000;
-0.120000<=pL<=0.160000, 0.560000<=pK<=0.600000;
-0.120000<=pL<=0.160000, 0.600000<=pK<=0.640000;
-0.120000<=pL<=0.160000, 0.640000<=pK<=0.680000;
-0.120000<=pL<=0.160000, 0.680000<=pK<=0.720000;
-0.120000<=pL<=0.160000, 0.720000<=pK<=0.760000;
-0.120000<=pL<=0.160000, 0.760000<=pK<=0.800000;
-0.120000<=pL<=0.160000, 0.800000<=pK<=0.840000;
-0.120000<=pL<=0.160000, 0.840000<=pK<=0.880000;
-0.120000<=pL<=0.160000, 0.880000<=pK<=0.920000;
-0.120000<=pL<=0.160000, 0.920000<=pK<=0.960000;
-0.120000<=pL<=0.160000, 0.960000<=pK<=0.999990;
-0.160000<=pL<=0.200000, 0.000010<=pK<=0.040000;
-0.160000<=pL<=0.200000, 0.040000<=pK<=0.080000;
-0.160000<=pL<=0.200000, 0.080000<=pK<=0.120000;
-0.160000<=pL<=0.200000, 0.120000<=pK<=0.160000;
-0.160000<=pL<=0.200000, 0.160000<=pK<=0.200000;
-0.160000<=pL<=0.200000, 0.200000<=pK<=0.240000;
-0.160000<=pL<=0.200000, 0.240000<=pK<=0.280000;
-0.160000<=pL<=0.200000, 0.280000<=pK<=0.320000;
-0.160000<=pL<=0.200000, 0.320000<=pK<=0.360000;
-0.160000<=pL<=0.200000, 0.360000<=pK<=0.400000;
-0.160000<=pL<=0.200000, 0.400000<=pK<=0.440000;
-0.160000<=pL<=0.200000, 0.440000<=pK<=0.480000;
-0.160000<=pL<=0.200000, 0.480000<=pK<=0.520000;
-0.160000<=pL<=0.200000, 0.520000<=pK<=0.560000;
-0.160000<=pL<=0.200000, 0.560000<=pK<=0.600000;
-0.160000<=pL<=0.200000, 0.600000<=pK<=0.640000;
-0.160000<=pL<=0.200000, 0.640000<=pK<=0.680000;
-0.160000<=pL<=0.200000, 0.680000<=pK<=0.720000;
-0.160000<=pL<=0.200000, 0.720000<=pK<=0.760000;
-0.160000<=pL<=0.200000, 0.760000<=pK<=0.800000;
-0.160000<=pL<=0.200000, 0.800000<=pK<=0.840000;
-0.160000<=pL<=0.200000, 0.840000<=pK<=0.880000;
-0.160000<=pL<=0.200000, 0.880000<=pK<=0.920000;
-0.160000<=pL<=0.200000, 0.920000<=pK<=0.960000;
-0.160000<=pL<=0.200000, 0.960000<=pK<=0.999990;
-0.200000<=pL<=0.240000, 0.000010<=pK<=0.040000;
-0.200000<=pL<=0.240000, 0.040000<=pK<=0.080000;
-0.200000<=pL<=0.240000, 0.080000<=pK<=0.120000;
-0.200000<=pL<=0.240000, 0.120000<=pK<=0.160000;
-0.200000<=pL<=0.240000, 0.160000<=pK<=0.200000;
-0.200000<=pL<=0.240000, 0.200000<=pK<=0.240000;
-0.200000<=pL<=0.240000, 0.240000<=pK<=0.280000;
-0.200000<=pL<=0.240000, 0.280000<=pK<=0.320000;
-0.200000<=pL<=0.240000, 0.320000<=pK<=0.360000;
-0.200000<=pL<=0.240000, 0.360000<=pK<=0.400000;
-0.200000<=pL<=0.240000, 0.400000<=pK<=0.440000;
-0.200000<=pL<=0.240000, 0.440000<=pK<=0.480000;
-0.200000<=pL<=0.240000, 0.480000<=pK<=0.520000;
-0.200000<=pL<=0.240000, 0.520000<=pK<=0.560000;
-0.200000<=pL<=0.240000, 0.560000<=pK<=0.600000;
-0.200000<=pL<=0.240000, 0.600000<=pK<=0.640000;
-0.200000<=pL<=0.240000, 0.640000<=pK<=0.680000;
-0.200000<=pL<=0.240000, 0.680000<=pK<=0.720000;
-0.200000<=pL<=0.240000, 0.720000<=pK<=0.760000;
-0.200000<=pL<=0.240000, 0.760000<=pK<=0.800000;
-0.200000<=pL<=0.240000, 0.800000<=pK<=0.840000;
-0.200000<=pL<=0.240000, 0.840000<=pK<=0.880000;
-0.200000<=pL<=0.240000, 0.880000<=pK<=0.920000;
-0.200000<=pL<=0.240000, 0.920000<=pK<=0.960000;
-0.200000<=pL<=0.240000, 0.960000<=pK<=0.999990;
-0.240000<=pL<=0.280000, 0.000010<=pK<=0.040000;
-0.240000<=pL<=0.280000, 0.040000<=pK<=0.080000;
-0.240000<=pL<=0.280000, 0.080000<=pK<=0.120000;
-0.240000<=pL<=0.280000, 0.120000<=pK<=0.160000;
-0.240000<=pL<=0.280000, 0.160000<=pK<=0.200000;
-0.240000<=pL<=0.280000, 0.200000<=pK<=0.240000;
-0.240000<=pL<=0.280000, 0.240000<=pK<=0.280000;
-0.240000<=pL<=0.280000, 0.280000<=pK<=0.320000;
-0.240000<=pL<=0.280000, 0.320000<=pK<=0.360000;
-0.240000<=pL<=0.280000, 0.360000<=pK<=0.400000;
-0.240000<=pL<=0.280000, 0.400000<=pK<=0.440000;
-0.240000<=pL<=0.280000, 0.440000<=pK<=0.480000;
-0.240000<=pL<=0.280000, 0.480000<=pK<=0.520000;
-0.240000<=pL<=0.280000, 0.520000<=pK<=0.560000;
-0.240000<=pL<=0.280000, 0.560000<=pK<=0.600000;
-0.240000<=pL<=0.280000, 0.600000<=pK<=0.640000;
-0.240000<=pL<=0.280000, 0.640000<=pK<=0.680000;
-0.240000<=pL<=0.280000, 0.680000<=pK<=0.720000;
-0.240000<=pL<=0.280000, 0.720000<=pK<=0.760000;
-0.240000<=pL<=0.280000, 0.760000<=pK<=0.800000;
-0.240000<=pL<=0.280000, 0.800000<=pK<=0.840000;
-0.240000<=pL<=0.280000, 0.840000<=pK<=0.880000;
-0.240000<=pL<=0.280000, 0.880000<=pK<=0.920000;
-0.240000<=pL<=0.280000, 0.920000<=pK<=0.960000;
-0.240000<=pL<=0.280000, 0.960000<=pK<=0.999990;
-0.280000<=pL<=0.320000, 0.000010<=pK<=0.040000;
-0.280000<=pL<=0.320000, 0.040000<=pK<=0.080000;
-0.280000<=pL<=0.320000, 0.080000<=pK<=0.120000;
-0.280000<=pL<=0.320000, 0.120000<=pK<=0.160000;
-0.280000<=pL<=0.320000, 0.160000<=pK<=0.200000;
-0.280000<=pL<=0.320000, 0.200000<=pK<=0.240000;
-0.280000<=pL<=0.320000, 0.240000<=pK<=0.280000;
-0.280000<=pL<=0.320000, 0.280000<=pK<=0.320000;
-0.280000<=pL<=0.320000, 0.320000<=pK<=0.360000;
-0.280000<=pL<=0.320000, 0.360000<=pK<=0.400000;
-0.280000<=pL<=0.320000, 0.400000<=pK<=0.440000;
-0.280000<=pL<=0.320000, 0.440000<=pK<=0.480000;
-0.280000<=pL<=0.320000, 0.480000<=pK<=0.520000;
-0.280000<=pL<=0.320000, 0.520000<=pK<=0.560000;
-0.280000<=pL<=0.320000, 0.560000<=pK<=0.600000;
-0.280000<=pL<=0.320000, 0.600000<=pK<=0.640000;
-0.280000<=pL<=0.320000, 0.640000<=pK<=0.680000;
-0.280000<=pL<=0.320000, 0.680000<=pK<=0.720000;
-0.280000<=pL<=0.320000, 0.720000<=pK<=0.760000;
-0.280000<=pL<=0.320000, 0.760000<=pK<=0.800000;
-0.280000<=pL<=0.320000, 0.800000<=pK<=0.840000;
-0.280000<=pL<=0.320000, 0.840000<=pK<=0.880000;
-0.280000<=pL<=0.320000, 0.880000<=pK<=0.920000;
-0.280000<=pL<=0.320000, 0.920000<=pK<=0.960000;
-0.280000<=pL<=0.320000, 0.960000<=pK<=0.999990;
-0.320000<=pL<=0.360000, 0.000010<=pK<=0.040000;
-0.320000<=pL<=0.360000, 0.040000<=pK<=0.080000;
-0.320000<=pL<=0.360000, 0.080000<=pK<=0.120000;
-0.320000<=pL<=0.360000, 0.120000<=pK<=0.160000;
-0.320000<=pL<=0.360000, 0.160000<=pK<=0.200000;
-0.320000<=pL<=0.360000, 0.200000<=pK<=0.240000;
-0.320000<=pL<=0.360000, 0.240000<=pK<=0.280000;
-0.320000<=pL<=0.360000, 0.280000<=pK<=0.320000;
-0.320000<=pL<=0.360000, 0.320000<=pK<=0.360000;
-0.320000<=pL<=0.360000, 0.360000<=pK<=0.400000;
-0.320000<=pL<=0.360000, 0.400000<=pK<=0.440000;
-0.320000<=pL<=0.360000, 0.440000<=pK<=0.480000;
-0.320000<=pL<=0.360000, 0.480000<=pK<=0.520000;
-0.320000<=pL<=0.360000, 0.520000<=pK<=0.560000;
-0.320000<=pL<=0.360000, 0.560000<=pK<=0.600000;
-0.320000<=pL<=0.360000, 0.600000<=pK<=0.640000;
-0.320000<=pL<=0.360000, 0.640000<=pK<=0.680000;
-0.320000<=pL<=0.360000, 0.680000<=pK<=0.720000;
-0.320000<=pL<=0.360000, 0.720000<=pK<=0.760000;
-0.320000<=pL<=0.360000, 0.760000<=pK<=0.800000;
-0.320000<=pL<=0.360000, 0.800000<=pK<=0.840000;
-0.320000<=pL<=0.360000, 0.840000<=pK<=0.880000;
-0.320000<=pL<=0.360000, 0.880000<=pK<=0.920000;
-0.320000<=pL<=0.360000, 0.920000<=pK<=0.960000;
-0.320000<=pL<=0.360000, 0.960000<=pK<=0.999990;
-0.360000<=pL<=0.400000, 0.000010<=pK<=0.040000;
-0.360000<=pL<=0.400000, 0.040000<=pK<=0.080000;
-0.360000<=pL<=0.400000, 0.080000<=pK<=0.120000;
-0.360000<=pL<=0.400000, 0.120000<=pK<=0.160000;
-0.360000<=pL<=0.400000, 0.160000<=pK<=0.200000;
-0.360000<=pL<=0.400000, 0.200000<=pK<=0.240000;
-0.360000<=pL<=0.400000, 0.240000<=pK<=0.280000;
-0.360000<=pL<=0.400000, 0.280000<=pK<=0.320000;
-0.360000<=pL<=0.400000, 0.320000<=pK<=0.360000;
-0.360000<=pL<=0.400000, 0.360000<=pK<=0.400000;
-0.360000<=pL<=0.400000, 0.400000<=pK<=0.440000;
-0.360000<=pL<=0.400000, 0.440000<=pK<=0.480000;
-0.360000<=pL<=0.400000, 0.480000<=pK<=0.520000;
-0.360000<=pL<=0.400000, 0.520000<=pK<=0.560000;
-0.360000<=pL<=0.400000, 0.560000<=pK<=0.600000;
-0.360000<=pL<=0.400000, 0.600000<=pK<=0.640000;
-0.360000<=pL<=0.400000, 0.640000<=pK<=0.680000;
-0.360000<=pL<=0.400000, 0.680000<=pK<=0.720000;
-0.360000<=pL<=0.400000, 0.720000<=pK<=0.760000;
-0.360000<=pL<=0.400000, 0.760000<=pK<=0.800000;
-0.360000<=pL<=0.400000, 0.800000<=pK<=0.840000;
-0.360000<=pL<=0.400000, 0.840000<=pK<=0.880000;
-0.360000<=pL<=0.400000, 0.880000<=pK<=0.920000;
-0.360000<=pL<=0.400000, 0.920000<=pK<=0.960000;
-0.360000<=pL<=0.400000, 0.960000<=pK<=0.999990;
-0.400000<=pL<=0.440000, 0.000010<=pK<=0.040000;
-0.400000<=pL<=0.440000, 0.040000<=pK<=0.080000;
-0.400000<=pL<=0.440000, 0.080000<=pK<=0.120000;
-0.400000<=pL<=0.440000, 0.120000<=pK<=0.160000;
-0.400000<=pL<=0.440000, 0.160000<=pK<=0.200000;
-0.400000<=pL<=0.440000, 0.200000<=pK<=0.240000;
-0.400000<=pL<=0.440000, 0.240000<=pK<=0.280000;
-0.400000<=pL<=0.440000, 0.280000<=pK<=0.320000;
-0.400000<=pL<=0.440000, 0.320000<=pK<=0.360000;
-0.400000<=pL<=0.440000, 0.360000<=pK<=0.400000;
-0.400000<=pL<=0.440000, 0.400000<=pK<=0.440000;
-0.400000<=pL<=0.440000, 0.440000<=pK<=0.480000;
-0.400000<=pL<=0.440000, 0.480000<=pK<=0.520000;
-0.400000<=pL<=0.440000, 0.520000<=pK<=0.560000;
-0.400000<=pL<=0.440000, 0.560000<=pK<=0.600000;
-0.400000<=pL<=0.440000, 0.600000<=pK<=0.640000;
-0.400000<=pL<=0.440000, 0.640000<=pK<=0.680000;
-0.400000<=pL<=0.440000, 0.680000<=pK<=0.720000;
-0.400000<=pL<=0.440000, 0.720000<=pK<=0.760000;
-0.400000<=pL<=0.440000, 0.760000<=pK<=0.800000;
-0.400000<=pL<=0.440000, 0.800000<=pK<=0.840000;
-0.400000<=pL<=0.440000, 0.840000<=pK<=0.880000;
-0.400000<=pL<=0.440000, 0.880000<=pK<=0.920000;
-0.400000<=pL<=0.440000, 0.920000<=pK<=0.960000;
-0.400000<=pL<=0.440000, 0.960000<=pK<=0.999990;
-0.440000<=pL<=0.480000, 0.000010<=pK<=0.040000;
-0.440000<=pL<=0.480000, 0.040000<=pK<=0.080000;
-0.440000<=pL<=0.480000, 0.080000<=pK<=0.120000;
-0.440000<=pL<=0.480000, 0.120000<=pK<=0.160000;
-0.440000<=pL<=0.480000, 0.160000<=pK<=0.200000;
-0.440000<=pL<=0.480000, 0.200000<=pK<=0.240000;
-0.440000<=pL<=0.480000, 0.240000<=pK<=0.280000;
-0.440000<=pL<=0.480000, 0.280000<=pK<=0.320000;
-0.440000<=pL<=0.480000, 0.320000<=pK<=0.360000;
-0.440000<=pL<=0.480000, 0.360000<=pK<=0.400000;
-0.440000<=pL<=0.480000, 0.400000<=pK<=0.440000;
-0.440000<=pL<=0.480000, 0.440000<=pK<=0.480000;
-0.440000<=pL<=0.480000, 0.480000<=pK<=0.520000;
-0.440000<=pL<=0.480000, 0.520000<=pK<=0.560000;
-0.440000<=pL<=0.480000, 0.560000<=pK<=0.600000;
-0.440000<=pL<=0.480000, 0.600000<=pK<=0.640000;
-0.440000<=pL<=0.480000, 0.640000<=pK<=0.680000;
-0.440000<=pL<=0.480000, 0.680000<=pK<=0.720000;
-0.440000<=pL<=0.480000, 0.720000<=pK<=0.760000;
-0.440000<=pL<=0.480000, 0.760000<=pK<=0.800000;
-0.440000<=pL<=0.480000, 0.800000<=pK<=0.840000;
-0.440000<=pL<=0.480000, 0.840000<=pK<=0.880000;
-0.440000<=pL<=0.480000, 0.880000<=pK<=0.920000;
-0.440000<=pL<=0.480000, 0.920000<=pK<=0.960000;
-0.440000<=pL<=0.480000, 0.960000<=pK<=0.999990;
-0.480000<=pL<=0.520000, 0.000010<=pK<=0.040000;
-0.480000<=pL<=0.520000, 0.040000<=pK<=0.080000;
-0.480000<=pL<=0.520000, 0.080000<=pK<=0.120000;
-0.480000<=pL<=0.520000, 0.120000<=pK<=0.160000;
-0.480000<=pL<=0.520000, 0.160000<=pK<=0.200000;
-0.480000<=pL<=0.520000, 0.200000<=pK<=0.240000;
-0.480000<=pL<=0.520000, 0.240000<=pK<=0.280000;
-0.480000<=pL<=0.520000, 0.280000<=pK<=0.320000;
-0.480000<=pL<=0.520000, 0.320000<=pK<=0.360000;
-0.480000<=pL<=0.520000, 0.360000<=pK<=0.400000;
-0.480000<=pL<=0.520000, 0.400000<=pK<=0.440000;
-0.480000<=pL<=0.520000, 0.440000<=pK<=0.480000;
-0.480000<=pL<=0.520000, 0.480000<=pK<=0.520000;
-0.480000<=pL<=0.520000, 0.520000<=pK<=0.560000;
-0.480000<=pL<=0.520000, 0.560000<=pK<=0.600000;
-0.480000<=pL<=0.520000, 0.600000<=pK<=0.640000;
-0.480000<=pL<=0.520000, 0.640000<=pK<=0.680000;
-0.480000<=pL<=0.520000, 0.680000<=pK<=0.720000;
-0.480000<=pL<=0.520000, 0.720000<=pK<=0.760000;
-0.480000<=pL<=0.520000, 0.760000<=pK<=0.800000;
-0.480000<=pL<=0.520000, 0.800000<=pK<=0.840000;
-0.480000<=pL<=0.520000, 0.840000<=pK<=0.880000;
-0.480000<=pL<=0.520000, 0.880000<=pK<=0.920000;
-0.480000<=pL<=0.520000, 0.920000<=pK<=0.960000;
-0.480000<=pL<=0.520000, 0.960000<=pK<=0.999990;
-0.520000<=pL<=0.560000, 0.000010<=pK<=0.040000;
-0.520000<=pL<=0.560000, 0.040000<=pK<=0.080000;
-0.520000<=pL<=0.560000, 0.080000<=pK<=0.120000;
-0.520000<=pL<=0.560000, 0.120000<=pK<=0.160000;
-0.520000<=pL<=0.560000, 0.160000<=pK<=0.200000;
-0.520000<=pL<=0.560000, 0.200000<=pK<=0.240000;
-0.520000<=pL<=0.560000, 0.240000<=pK<=0.280000;
-0.520000<=pL<=0.560000, 0.280000<=pK<=0.320000;
-0.520000<=pL<=0.560000, 0.320000<=pK<=0.360000;
-0.520000<=pL<=0.560000, 0.360000<=pK<=0.400000;
-0.520000<=pL<=0.560000, 0.400000<=pK<=0.440000;
-0.520000<=pL<=0.560000, 0.440000<=pK<=0.480000;
-0.520000<=pL<=0.560000, 0.480000<=pK<=0.520000;
-0.520000<=pL<=0.560000, 0.520000<=pK<=0.560000;
-0.520000<=pL<=0.560000, 0.560000<=pK<=0.600000;
-0.520000<=pL<=0.560000, 0.600000<=pK<=0.640000;
-0.520000<=pL<=0.560000, 0.640000<=pK<=0.680000;
-0.520000<=pL<=0.560000, 0.680000<=pK<=0.720000;
-0.520000<=pL<=0.560000, 0.720000<=pK<=0.760000;
-0.520000<=pL<=0.560000, 0.760000<=pK<=0.800000;
-0.520000<=pL<=0.560000, 0.800000<=pK<=0.840000;
-0.520000<=pL<=0.560000, 0.840000<=pK<=0.880000;
-0.520000<=pL<=0.560000, 0.880000<=pK<=0.920000;
-0.520000<=pL<=0.560000, 0.920000<=pK<=0.960000;
-0.520000<=pL<=0.560000, 0.960000<=pK<=0.999990;
-0.560000<=pL<=0.600000, 0.000010<=pK<=0.040000;
-0.560000<=pL<=0.600000, 0.040000<=pK<=0.080000;
-0.560000<=pL<=0.600000, 0.080000<=pK<=0.120000;
-0.560000<=pL<=0.600000, 0.120000<=pK<=0.160000;
-0.560000<=pL<=0.600000, 0.160000<=pK<=0.200000;
-0.560000<=pL<=0.600000, 0.200000<=pK<=0.240000;
-0.560000<=pL<=0.600000, 0.240000<=pK<=0.280000;
-0.560000<=pL<=0.600000, 0.280000<=pK<=0.320000;
-0.560000<=pL<=0.600000, 0.320000<=pK<=0.360000;
-0.560000<=pL<=0.600000, 0.360000<=pK<=0.400000;
-0.560000<=pL<=0.600000, 0.400000<=pK<=0.440000;
-0.560000<=pL<=0.600000, 0.440000<=pK<=0.480000;
-0.560000<=pL<=0.600000, 0.480000<=pK<=0.520000;
-0.560000<=pL<=0.600000, 0.520000<=pK<=0.560000;
-0.560000<=pL<=0.600000, 0.560000<=pK<=0.600000;
-0.560000<=pL<=0.600000, 0.600000<=pK<=0.640000;
-0.560000<=pL<=0.600000, 0.640000<=pK<=0.680000;
-0.560000<=pL<=0.600000, 0.680000<=pK<=0.720000;
-0.560000<=pL<=0.600000, 0.720000<=pK<=0.760000;
-0.560000<=pL<=0.600000, 0.760000<=pK<=0.800000;
-0.560000<=pL<=0.600000, 0.800000<=pK<=0.840000;
-0.560000<=pL<=0.600000, 0.840000<=pK<=0.880000;
-0.560000<=pL<=0.600000, 0.880000<=pK<=0.920000;
-0.560000<=pL<=0.600000, 0.920000<=pK<=0.960000;
-0.560000<=pL<=0.600000, 0.960000<=pK<=0.999990;
-0.600000<=pL<=0.640000, 0.000010<=pK<=0.040000;
-0.600000<=pL<=0.640000, 0.040000<=pK<=0.080000;
-0.600000<=pL<=0.640000, 0.080000<=pK<=0.120000;
-0.600000<=pL<=0.640000, 0.120000<=pK<=0.160000;
-0.600000<=pL<=0.640000, 0.160000<=pK<=0.200000;
-0.600000<=pL<=0.640000, 0.200000<=pK<=0.240000;
-0.600000<=pL<=0.640000, 0.240000<=pK<=0.280000;
-0.600000<=pL<=0.640000, 0.280000<=pK<=0.320000;
-0.600000<=pL<=0.640000, 0.320000<=pK<=0.360000;
-0.600000<=pL<=0.640000, 0.360000<=pK<=0.400000;
-0.600000<=pL<=0.640000, 0.400000<=pK<=0.440000;
-0.600000<=pL<=0.640000, 0.440000<=pK<=0.480000;
-0.600000<=pL<=0.640000, 0.480000<=pK<=0.520000;
-0.600000<=pL<=0.640000, 0.520000<=pK<=0.560000;
-0.600000<=pL<=0.640000, 0.560000<=pK<=0.600000;
-0.600000<=pL<=0.640000, 0.600000<=pK<=0.640000;
-0.600000<=pL<=0.640000, 0.640000<=pK<=0.680000;
-0.600000<=pL<=0.640000, 0.680000<=pK<=0.720000;
-0.600000<=pL<=0.640000, 0.720000<=pK<=0.760000;
-0.600000<=pL<=0.640000, 0.760000<=pK<=0.800000;
-0.600000<=pL<=0.640000, 0.800000<=pK<=0.840000;
-0.600000<=pL<=0.640000, 0.840000<=pK<=0.880000;
-0.600000<=pL<=0.640000, 0.880000<=pK<=0.920000;
-0.600000<=pL<=0.640000, 0.920000<=pK<=0.960000;
-0.600000<=pL<=0.640000, 0.960000<=pK<=0.999990;
-0.640000<=pL<=0.680000, 0.000010<=pK<=0.040000;
-0.640000<=pL<=0.680000, 0.040000<=pK<=0.080000;
-0.640000<=pL<=0.680000, 0.080000<=pK<=0.120000;
-0.640000<=pL<=0.680000, 0.120000<=pK<=0.160000;
-0.640000<=pL<=0.680000, 0.160000<=pK<=0.200000;
-0.640000<=pL<=0.680000, 0.200000<=pK<=0.240000;
-0.640000<=pL<=0.680000, 0.240000<=pK<=0.280000;
-0.640000<=pL<=0.680000, 0.280000<=pK<=0.320000;
-0.640000<=pL<=0.680000, 0.320000<=pK<=0.360000;
-0.640000<=pL<=0.680000, 0.360000<=pK<=0.400000;
-0.640000<=pL<=0.680000, 0.400000<=pK<=0.440000;
-0.640000<=pL<=0.680000, 0.440000<=pK<=0.480000;
-0.640000<=pL<=0.680000, 0.480000<=pK<=0.520000;
-0.640000<=pL<=0.680000, 0.520000<=pK<=0.560000;
-0.640000<=pL<=0.680000, 0.560000<=pK<=0.600000;
-0.640000<=pL<=0.680000, 0.600000<=pK<=0.640000;
-0.640000<=pL<=0.680000, 0.640000<=pK<=0.680000;
-0.640000<=pL<=0.680000, 0.680000<=pK<=0.720000;
-0.640000<=pL<=0.680000, 0.720000<=pK<=0.760000;
-0.640000<=pL<=0.680000, 0.760000<=pK<=0.800000;
-0.640000<=pL<=0.680000, 0.800000<=pK<=0.840000;
-0.640000<=pL<=0.680000, 0.840000<=pK<=0.880000;
-0.640000<=pL<=0.680000, 0.880000<=pK<=0.920000;
-0.640000<=pL<=0.680000, 0.920000<=pK<=0.960000;
-0.640000<=pL<=0.680000, 0.960000<=pK<=0.999990;
-0.680000<=pL<=0.720000, 0.000010<=pK<=0.040000;
-0.680000<=pL<=0.720000, 0.040000<=pK<=0.080000;
-0.680000<=pL<=0.720000, 0.080000<=pK<=0.120000;
-0.680000<=pL<=0.720000, 0.120000<=pK<=0.160000;
-0.680000<=pL<=0.720000, 0.160000<=pK<=0.200000;
-0.680000<=pL<=0.720000, 0.200000<=pK<=0.240000;
-0.680000<=pL<=0.720000, 0.240000<=pK<=0.280000;
-0.680000<=pL<=0.720000, 0.280000<=pK<=0.320000;
-0.680000<=pL<=0.720000, 0.320000<=pK<=0.360000;
-0.680000<=pL<=0.720000, 0.360000<=pK<=0.400000;
-0.680000<=pL<=0.720000, 0.400000<=pK<=0.440000;
-0.680000<=pL<=0.720000, 0.440000<=pK<=0.480000;
-0.680000<=pL<=0.720000, 0.480000<=pK<=0.520000;
-0.680000<=pL<=0.720000, 0.520000<=pK<=0.560000;
-0.680000<=pL<=0.720000, 0.560000<=pK<=0.600000;
-0.680000<=pL<=0.720000, 0.600000<=pK<=0.640000;
-0.680000<=pL<=0.720000, 0.640000<=pK<=0.680000;
-0.680000<=pL<=0.720000, 0.680000<=pK<=0.720000;
-0.680000<=pL<=0.720000, 0.720000<=pK<=0.760000;
-0.680000<=pL<=0.720000, 0.760000<=pK<=0.800000;
-0.680000<=pL<=0.720000, 0.800000<=pK<=0.840000;
-0.680000<=pL<=0.720000, 0.840000<=pK<=0.880000;
-0.680000<=pL<=0.720000, 0.880000<=pK<=0.920000;
-0.680000<=pL<=0.720000, 0.920000<=pK<=0.960000;
-0.680000<=pL<=0.720000, 0.960000<=pK<=0.999990;
-0.720000<=pL<=0.760000, 0.000010<=pK<=0.040000;
-0.720000<=pL<=0.760000, 0.040000<=pK<=0.080000;
-0.720000<=pL<=0.760000, 0.080000<=pK<=0.120000;
-0.720000<=pL<=0.760000, 0.120000<=pK<=0.160000;
-0.720000<=pL<=0.760000, 0.160000<=pK<=0.200000;
-0.720000<=pL<=0.760000, 0.200000<=pK<=0.240000;
-0.720000<=pL<=0.760000, 0.240000<=pK<=0.280000;
-0.720000<=pL<=0.760000, 0.280000<=pK<=0.320000;
-0.720000<=pL<=0.760000, 0.320000<=pK<=0.360000;
-0.720000<=pL<=0.760000, 0.360000<=pK<=0.400000;
-0.720000<=pL<=0.760000, 0.400000<=pK<=0.440000;
-0.720000<=pL<=0.760000, 0.440000<=pK<=0.480000;
-0.720000<=pL<=0.760000, 0.480000<=pK<=0.520000;
-0.720000<=pL<=0.760000, 0.520000<=pK<=0.560000;
-0.720000<=pL<=0.760000, 0.560000<=pK<=0.600000;
-0.720000<=pL<=0.760000, 0.600000<=pK<=0.640000;
-0.720000<=pL<=0.760000, 0.640000<=pK<=0.680000;
-0.720000<=pL<=0.760000, 0.680000<=pK<=0.720000;
-0.720000<=pL<=0.760000, 0.720000<=pK<=0.760000;
-0.720000<=pL<=0.760000, 0.760000<=pK<=0.800000;
-0.720000<=pL<=0.760000, 0.800000<=pK<=0.840000;
-0.720000<=pL<=0.760000, 0.840000<=pK<=0.880000;
-0.720000<=pL<=0.760000, 0.880000<=pK<=0.920000;
-0.720000<=pL<=0.760000, 0.920000<=pK<=0.960000;
-0.720000<=pL<=0.760000, 0.960000<=pK<=0.999990;
-0.760000<=pL<=0.800000, 0.000010<=pK<=0.040000;
-0.760000<=pL<=0.800000, 0.040000<=pK<=0.080000;
-0.760000<=pL<=0.800000, 0.080000<=pK<=0.120000;
-0.760000<=pL<=0.800000, 0.120000<=pK<=0.160000;
-0.760000<=pL<=0.800000, 0.160000<=pK<=0.200000;
-0.760000<=pL<=0.800000, 0.200000<=pK<=0.240000;
-0.760000<=pL<=0.800000, 0.240000<=pK<=0.280000;
-0.760000<=pL<=0.800000, 0.280000<=pK<=0.320000;
-0.760000<=pL<=0.800000, 0.320000<=pK<=0.360000;
-0.760000<=pL<=0.800000, 0.360000<=pK<=0.400000;
-0.760000<=pL<=0.800000, 0.400000<=pK<=0.440000;
-0.760000<=pL<=0.800000, 0.440000<=pK<=0.480000;
-0.760000<=pL<=0.800000, 0.480000<=pK<=0.520000;
-0.760000<=pL<=0.800000, 0.520000<=pK<=0.560000;
-0.760000<=pL<=0.800000, 0.560000<=pK<=0.600000;
-0.760000<=pL<=0.800000, 0.600000<=pK<=0.640000;
-0.760000<=pL<=0.800000, 0.640000<=pK<=0.680000;
-0.760000<=pL<=0.800000, 0.680000<=pK<=0.720000;
-0.760000<=pL<=0.800000, 0.720000<=pK<=0.760000;
-0.760000<=pL<=0.800000, 0.760000<=pK<=0.800000;
-0.760000<=pL<=0.800000, 0.800000<=pK<=0.840000;
-0.760000<=pL<=0.800000, 0.840000<=pK<=0.880000;
-0.760000<=pL<=0.800000, 0.880000<=pK<=0.920000;
-0.760000<=pL<=0.800000, 0.920000<=pK<=0.960000;
-0.760000<=pL<=0.800000, 0.960000<=pK<=0.999990;
-0.800000<=pL<=0.840000, 0.000010<=pK<=0.040000;
-0.800000<=pL<=0.840000, 0.040000<=pK<=0.080000;
-0.800000<=pL<=0.840000, 0.080000<=pK<=0.120000;
-0.800000<=pL<=0.840000, 0.120000<=pK<=0.160000;
-0.800000<=pL<=0.840000, 0.160000<=pK<=0.200000;
-0.800000<=pL<=0.840000, 0.200000<=pK<=0.240000;
-0.800000<=pL<=0.840000, 0.240000<=pK<=0.280000;
-0.800000<=pL<=0.840000, 0.280000<=pK<=0.320000;
-0.800000<=pL<=0.840000, 0.320000<=pK<=0.360000;
-0.800000<=pL<=0.840000, 0.360000<=pK<=0.400000;
-0.800000<=pL<=0.840000, 0.400000<=pK<=0.440000;
-0.800000<=pL<=0.840000, 0.440000<=pK<=0.480000;
-0.800000<=pL<=0.840000, 0.480000<=pK<=0.520000;
-0.800000<=pL<=0.840000, 0.520000<=pK<=0.560000;
-0.800000<=pL<=0.840000, 0.560000<=pK<=0.600000;
-0.800000<=pL<=0.840000, 0.600000<=pK<=0.640000;
-0.800000<=pL<=0.840000, 0.640000<=pK<=0.680000;
-0.800000<=pL<=0.840000, 0.680000<=pK<=0.720000;
-0.800000<=pL<=0.840000, 0.720000<=pK<=0.760000;
-0.800000<=pL<=0.840000, 0.760000<=pK<=0.800000;
-0.800000<=pL<=0.840000, 0.800000<=pK<=0.840000;
-0.800000<=pL<=0.840000, 0.840000<=pK<=0.880000;
-0.800000<=pL<=0.840000, 0.880000<=pK<=0.920000;
-0.800000<=pL<=0.840000, 0.920000<=pK<=0.960000;
-0.800000<=pL<=0.840000, 0.960000<=pK<=0.999990;
-0.840000<=pL<=0.880000, 0.000010<=pK<=0.040000;
-0.840000<=pL<=0.880000, 0.040000<=pK<=0.080000;
-0.840000<=pL<=0.880000, 0.080000<=pK<=0.120000;
-0.840000<=pL<=0.880000, 0.120000<=pK<=0.160000;
-0.840000<=pL<=0.880000, 0.160000<=pK<=0.200000;
-0.840000<=pL<=0.880000, 0.200000<=pK<=0.240000;
-0.840000<=pL<=0.880000, 0.240000<=pK<=0.280000;
-0.840000<=pL<=0.880000, 0.280000<=pK<=0.320000;
-0.840000<=pL<=0.880000, 0.320000<=pK<=0.360000;
-0.840000<=pL<=0.880000, 0.360000<=pK<=0.400000;
-0.840000<=pL<=0.880000, 0.400000<=pK<=0.440000;
-0.840000<=pL<=0.880000, 0.440000<=pK<=0.480000;
-0.840000<=pL<=0.880000, 0.480000<=pK<=0.520000;
-0.840000<=pL<=0.880000, 0.520000<=pK<=0.560000;
-0.840000<=pL<=0.880000, 0.560000<=pK<=0.600000;
-0.840000<=pL<=0.880000, 0.600000<=pK<=0.640000;
-0.840000<=pL<=0.880000, 0.640000<=pK<=0.680000;
-0.840000<=pL<=0.880000, 0.680000<=pK<=0.720000;
-0.840000<=pL<=0.880000, 0.720000<=pK<=0.760000;
-0.840000<=pL<=0.880000, 0.760000<=pK<=0.800000;
-0.840000<=pL<=0.880000, 0.800000<=pK<=0.840000;
-0.840000<=pL<=0.880000, 0.840000<=pK<=0.880000;
-0.840000<=pL<=0.880000, 0.880000<=pK<=0.920000;
-0.840000<=pL<=0.880000, 0.920000<=pK<=0.960000;
-0.840000<=pL<=0.880000, 0.960000<=pK<=0.999990;
-0.880000<=pL<=0.920000, 0.000010<=pK<=0.040000;
-0.880000<=pL<=0.920000, 0.040000<=pK<=0.080000;
-0.880000<=pL<=0.920000, 0.080000<=pK<=0.120000;
-0.880000<=pL<=0.920000, 0.120000<=pK<=0.160000;
-0.880000<=pL<=0.920000, 0.160000<=pK<=0.200000;
-0.880000<=pL<=0.920000, 0.200000<=pK<=0.240000;
-0.880000<=pL<=0.920000, 0.240000<=pK<=0.280000;
-0.880000<=pL<=0.920000, 0.280000<=pK<=0.320000;
-0.880000<=pL<=0.920000, 0.320000<=pK<=0.360000;
-0.880000<=pL<=0.920000, 0.360000<=pK<=0.400000;
-0.880000<=pL<=0.920000, 0.400000<=pK<=0.440000;
-0.880000<=pL<=0.920000, 0.440000<=pK<=0.480000;
-0.880000<=pL<=0.920000, 0.480000<=pK<=0.520000;
-0.880000<=pL<=0.920000, 0.520000<=pK<=0.560000;
-0.880000<=pL<=0.920000, 0.560000<=pK<=0.600000;
-0.880000<=pL<=0.920000, 0.600000<=pK<=0.640000;
-0.880000<=pL<=0.920000, 0.640000<=pK<=0.680000;
-0.880000<=pL<=0.920000, 0.680000<=pK<=0.720000;
-0.880000<=pL<=0.920000, 0.720000<=pK<=0.760000;
-0.880000<=pL<=0.920000, 0.760000<=pK<=0.800000;
-0.880000<=pL<=0.920000, 0.800000<=pK<=0.840000;
-0.880000<=pL<=0.920000, 0.840000<=pK<=0.880000;
-0.880000<=pL<=0.920000, 0.880000<=pK<=0.920000;
-0.880000<=pL<=0.920000, 0.920000<=pK<=0.960000;
-0.880000<=pL<=0.920000, 0.960000<=pK<=0.999990;
-0.920000<=pL<=0.960000, 0.000010<=pK<=0.040000;
-0.920000<=pL<=0.960000, 0.040000<=pK<=0.080000;
-0.920000<=pL<=0.960000, 0.080000<=pK<=0.120000;
-0.920000<=pL<=0.960000, 0.120000<=pK<=0.160000;
-0.920000<=pL<=0.960000, 0.160000<=pK<=0.200000;
-0.920000<=pL<=0.960000, 0.200000<=pK<=0.240000;
-0.920000<=pL<=0.960000, 0.240000<=pK<=0.280000;
-0.920000<=pL<=0.960000, 0.280000<=pK<=0.320000;
-0.920000<=pL<=0.960000, 0.320000<=pK<=0.360000;
-0.920000<=pL<=0.960000, 0.360000<=pK<=0.400000;
-0.920000<=pL<=0.960000, 0.400000<=pK<=0.440000;
-0.920000<=pL<=0.960000, 0.440000<=pK<=0.480000;
-0.920000<=pL<=0.960000, 0.480000<=pK<=0.520000;
-0.920000<=pL<=0.960000, 0.520000<=pK<=0.560000;
-0.920000<=pL<=0.960000, 0.560000<=pK<=0.600000;
-0.920000<=pL<=0.960000, 0.600000<=pK<=0.640000;
-0.920000<=pL<=0.960000, 0.640000<=pK<=0.680000;
-0.920000<=pL<=0.960000, 0.680000<=pK<=0.720000;
-0.920000<=pL<=0.960000, 0.720000<=pK<=0.760000;
-0.920000<=pL<=0.960000, 0.760000<=pK<=0.800000;
-0.920000<=pL<=0.960000, 0.800000<=pK<=0.840000;
-0.920000<=pL<=0.960000, 0.840000<=pK<=0.880000;
-0.920000<=pL<=0.960000, 0.880000<=pK<=0.920000;
-0.920000<=pL<=0.960000, 0.920000<=pK<=0.960000;
-0.920000<=pL<=0.960000, 0.960000<=pK<=0.999990;
-0.960000<=pL<=0.999990, 0.000010<=pK<=0.040000;
-0.960000<=pL<=0.999990, 0.040000<=pK<=0.080000;
-0.960000<=pL<=0.999990, 0.080000<=pK<=0.120000;
-0.960000<=pL<=0.999990, 0.120000<=pK<=0.160000;
-0.960000<=pL<=0.999990, 0.160000<=pK<=0.200000;
-0.960000<=pL<=0.999990, 0.200000<=pK<=0.240000;
-0.960000<=pL<=0.999990, 0.240000<=pK<=0.280000;
-0.960000<=pL<=0.999990, 0.280000<=pK<=0.320000;
-0.960000<=pL<=0.999990, 0.320000<=pK<=0.360000;
-0.960000<=pL<=0.999990, 0.360000<=pK<=0.400000;
-0.960000<=pL<=0.999990, 0.400000<=pK<=0.440000;
-0.960000<=pL<=0.999990, 0.440000<=pK<=0.480000;
-0.960000<=pL<=0.999990, 0.480000<=pK<=0.520000;
-0.960000<=pL<=0.999990, 0.520000<=pK<=0.560000;
-0.960000<=pL<=0.999990, 0.560000<=pK<=0.600000;
-0.960000<=pL<=0.999990, 0.600000<=pK<=0.640000;
-0.960000<=pL<=0.999990, 0.640000<=pK<=0.680000;
-0.960000<=pL<=0.999990, 0.680000<=pK<=0.720000;
-0.960000<=pL<=0.999990, 0.720000<=pK<=0.760000;
-0.960000<=pL<=0.999990, 0.760000<=pK<=0.800000;
-0.960000<=pL<=0.999990, 0.800000<=pK<=0.840000;
-0.960000<=pL<=0.999990, 0.840000<=pK<=0.880000;
-0.960000<=pL<=0.999990, 0.880000<=pK<=0.920000;
-0.960000<=pL<=0.999990, 0.920000<=pK<=0.960000;
-0.960000<=pL<=0.999990, 0.960000<=pK<=0.999990;
diff --git a/examples/pdtmc/brp_rewards2/brp_rewards2_space.txt b/examples/pdtmc/brp_rewards2/brp_rewards2_space.txt
new file mode 100644
index 000000000..444b98e90
--- /dev/null
+++ b/examples/pdtmc/brp_rewards2/brp_rewards2_space.txt
@@ -0,0 +1,2 @@
+0.000010<=pL<=0.999990, 0.000010<=pK<=0.999990;
+
diff --git a/examples/pdtmc/brp_rewards2/models b/examples/pdtmc/brp_rewards2/models
index 055586d1f..b12533a0b 100644
--- a/examples/pdtmc/brp_rewards2/models
+++ b/examples/pdtmc/brp_rewards2/models
@@ -1,4 +1,2 @@
-brp.pm -const N=512,MAX=5
-brp.pm -const N=1024,MAX=5
-
-
+brp_rewards2.pm -const N=512,MAX=5
+brp_rewards2.pm -const N=1024,MAX=5
diff --git a/examples/pdtmc/brp_rewards4/brp_rewards4_space.txt b/examples/pdtmc/brp_rewards4/brp_rewards4_space.txt
new file mode 100644
index 000000000..71a8cd59a
--- /dev/null
+++ b/examples/pdtmc/brp_rewards4/brp_rewards4_space.txt
@@ -0,0 +1,2 @@
+0.000010<=pL<=0.999990, 0.000010<=pK<=0.999990, 0.000010<=TOMsg<=0.999990, 0.000010<=TOAck<=0.999990;
+
diff --git a/examples/pdtmc/brp_rewards4/models b/examples/pdtmc/brp_rewards4/models
index 3fb543c9a..13a317bf0 100644
--- a/examples/pdtmc/brp_rewards4/models
+++ b/examples/pdtmc/brp_rewards4/models
@@ -1,2 +1,2 @@
-brp.pm -const N=512,MAX=5
-brp.pm -const N=1024,MAX=5
+brp_rewards4.pm -const N=512,MAX=5
+brp_rewards4.pm -const N=1024,MAX=5
diff --git a/examples/pdtmc/crowds/crowds_space.txt b/examples/pdtmc/crowds/crowds_space.txt
new file mode 100644
index 000000000..f36cebf3e
--- /dev/null
+++ b/examples/pdtmc/crowds/crowds_space.txt
@@ -0,0 +1,2 @@
+0.000010<=PF<=0.999990, 0.000010<=badC<=0.999990;
+
diff --git a/examples/pdtmc/nand/nand_space.txt b/examples/pdtmc/nand/nand_space.txt
new file mode 100644
index 000000000..fcd54b798
--- /dev/null
+++ b/examples/pdtmc/nand/nand_space.txt
@@ -0,0 +1,2 @@
+0.000010<=perr<=0.999990, 0.000010<=prob1<=0.999990;
+
diff --git a/examples/pmdp/brp/brp_space.txt b/examples/pmdp/brp/brp_space.txt
new file mode 100644
index 000000000..444b98e90
--- /dev/null
+++ b/examples/pmdp/brp/brp_space.txt
@@ -0,0 +1,2 @@
+0.000010<=pL<=0.999990, 0.000010<=pK<=0.999990;
+
diff --git a/examples/pmdp/brp/models b/examples/pmdp/brp/models
index 70d0bf3d4..afe9c2e13 100644
--- a/examples/pmdp/brp/models
+++ b/examples/pmdp/brp/models
@@ -1,4 +1,3 @@
brp.pm -const N=256,MAX=5
brp.pm -const N=512,MAX=5
brp.pm -const N=1024,MAX=5
-
diff --git a/examples/pmdp/coin2/coin2_space.txt b/examples/pmdp/coin2/coin2_space.txt
new file mode 100644
index 000000000..618c29eee
--- /dev/null
+++ b/examples/pmdp/coin2/coin2_space.txt
@@ -0,0 +1,2 @@
+0.000010<=p1<=0.999990, 0.000010<=p2<=0.999990;
+
diff --git a/examples/pmdp/coin4/coin2.prctl b/examples/pmdp/coin4/coin4.prctl
similarity index 100%
rename from examples/pmdp/coin4/coin2.prctl
rename to examples/pmdp/coin4/coin4.prctl
diff --git a/examples/pmdp/coin4/coin4_space.txt b/examples/pmdp/coin4/coin4_space.txt
new file mode 100644
index 000000000..4c0a341e1
--- /dev/null
+++ b/examples/pmdp/coin4/coin4_space.txt
@@ -0,0 +1,2 @@
+0.000010<=p1<=0.999990, 0.000010<=p2<=0.999990, 0.000010<=p3<=0.999990, 0.000010<=p4<=0.999990;
+
diff --git a/examples/pmdp/firewire/firewire_space.txt b/examples/pmdp/firewire/firewire_space.txt
new file mode 100644
index 000000000..189ca282f
--- /dev/null
+++ b/examples/pmdp/firewire/firewire_space.txt
@@ -0,0 +1,2 @@
+0.000010<=fast1<=0.999990, 0.000010<=fast2<=0.999990;
+
diff --git a/examples/pmdp/reporter2/reporter2_space.txt b/examples/pmdp/reporter2/reporter2_space.txt
new file mode 100644
index 000000000..ef1f8db6c
--- /dev/null
+++ b/examples/pmdp/reporter2/reporter2_space.txt
@@ -0,0 +1,2 @@
+0.000010<=pL<=0.999990, 0.000010<=pH<=0.999990;
+
diff --git a/examples/pmdp/reporter4/reporter4_space.txt b/examples/pmdp/reporter4/reporter4_space.txt
new file mode 100644
index 000000000..d0f12ccfc
--- /dev/null
+++ b/examples/pmdp/reporter4/reporter4_space.txt
@@ -0,0 +1,2 @@
+0.000010<=pL<=0.999990, 0.000010<=pH<=0.999990, 0.000010<=pLDiff<=0.999990, 0.000010<=pHDiff<=0.999990;
+
diff --git a/examples/pmdp/zeroconf/zeroconf_space.txt b/examples/pmdp/zeroconf/zeroconf_space.txt
new file mode 100644
index 000000000..54ffa3425
--- /dev/null
+++ b/examples/pmdp/zeroconf/zeroconf_space.txt
@@ -0,0 +1,2 @@
+0.000010<=loss<=0.999990, 0.000010<=old<=0.999990;
+
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index 0b1268913..75ac5421d 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -36,10 +36,14 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Currently parametric region verification is only available for DTMCs and Mdps.");
}
for (auto const& formula : formulas) {
- std::cout << std::endl << "Model checking property: " << *formula << " for all parameters in the given regions." << std::endl;
+ std::cout << std::endl << "Model checking property: " << *formula << " for all parameters in the given region(s)." << std::endl;
STORM_LOG_THROW(modelchecker->canHandle(*formula.get()), storm::exceptions::InvalidSettingsException, "The parametric region check engine does not support this property.");
modelchecker->specifyFormula(formula);
- modelchecker->checkRegions(regions);
+ if(storm::settings::regionSettings().doRefinement()){
+ modelchecker->refineAndCheckRegion(regions, storm::settings::regionSettings().getRefinementThreshold());
+ } else {
+ modelchecker->checkRegions(regions);
+ }
modelchecker->printStatisticsToStream(std::cout);
std::cout << std::endl;
}
diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp
index f41c143df..9311882d5 100644
--- a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp
+++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp
@@ -195,6 +195,42 @@ namespace storm {
std::cout << " done!" << std::endl;
}
+ 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.flush();
+ CoefficientType areaOfParameterSpace = regions.front().area();
+ uint_fast64_t indexOfCurrentRegion=0;
+ CoefficientType fractionOfUndiscoveredArea = storm::utility::one<CoefficientType>();
+ CoefficientType fractionOfAllSatArea = storm::utility::zero<CoefficientType>();
+ CoefficientType fractionOfAllViolatedArea = storm::utility::zero<CoefficientType>();
+ while(fractionOfUndiscoveredArea > storm::utility::region::convertNumber<CoefficientType>(refinementThreshold)){
+ STORM_LOG_THROW(indexOfCurrentRegion < regions.size(), storm::exceptions::InvalidStateException, "Threshold for undiscovered area not reached but no unprocessed regions left.");
+ ParameterRegion<ParametricType>& currentRegion = regions[indexOfCurrentRegion];
+ this->checkRegion(currentRegion);
+ switch(currentRegion.getCheckResult()){
+ case RegionCheckResult::ALLSAT:
+ fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
+ fractionOfAllSatArea += currentRegion.area() / areaOfParameterSpace;
+ break;
+ case RegionCheckResult::ALLVIOLATED:
+ fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
+ fractionOfAllViolatedArea += currentRegion.area() / areaOfParameterSpace;
+ break;
+ default:
+ std::vector<ParameterRegion<ParametricType>> newRegions;
+ currentRegion.split(currentRegion.getCenterPoint(), newRegions);
+ regions.insert(regions.end(), newRegions.begin(), newRegions.end());
+ break;
+ }
+ ++indexOfCurrentRegion;
+ }
+ std::cout << " done! " << std::endl << "Fraction of ALLSAT;ALLVIOLATED;UNDISCOVERED area:" << std::endl;
+ std::cout << "REFINEMENTRESULT;" <<storm::utility::region::convertNumber<double>(fractionOfAllSatArea) << ";" << storm::utility::region::convertNumber<double>(fractionOfAllViolatedArea) << ";" << storm::utility::region::convertNumber<double>(fractionOfUndiscoveredArea) << std::endl;
+
+ }
+
template<typename ParametricSparseModelType, typename ConstantType>
void AbstractSparseRegionModelChecker<ParametricSparseModelType, ConstantType>::checkRegion(ParameterRegion<ParametricType>& region) {
std::chrono::high_resolution_clock::time_point timeCheckRegionStart = std::chrono::high_resolution_clock::now();
diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.h b/src/modelchecker/region/AbstractSparseRegionModelChecker.h
index a4b3f6fb5..c11dee38b 100644
--- a/src/modelchecker/region/AbstractSparseRegionModelChecker.h
+++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.h
@@ -63,6 +63,19 @@ namespace storm {
*/
void checkRegions(std::vector<ParameterRegion<ParametricType>>& regions);
+ /*!
+ * Refines a given region and checks whether the specified formula holds for all parameters in the subregion.
+ * The procedure stops as soon as the fraction of the area of regions where the result is neither "ALLSAT" nor "ALLVIOLATED" is less then the given threshold.
+ *
+ * It is required that the given vector of regions contains exactly one region (the parameter space). All the analyzed regions are appended to that vector.
+ *
+ * @note A formula has to be specified first.
+ *
+ * @param regions The considered region
+ * @param refinementThreshold The considered threshold.
+ */
+ void refineAndCheckRegion(std::vector<ParameterRegion<ParametricType>>& regions, double const& refinementThreshold);
+
/*!
* Checks whether the given formula holds for all parameters that lie in the given region.
* Sets the region checkresult accordingly.
diff --git a/src/modelchecker/region/ParameterRegion.cpp b/src/modelchecker/region/ParameterRegion.cpp
index ff55102af..3860cab19 100644
--- a/src/modelchecker/region/ParameterRegion.cpp
+++ b/src/modelchecker/region/ParameterRegion.cpp
@@ -14,6 +14,7 @@
#include "src/settings/modules/RegionSettings.h"
#include "src/exceptions/InvalidSettingsException.h"
#include "src/exceptions/InvalidArgumentException.h"
+#include "utility/constants.h"
namespace storm {
namespace modelchecker {
@@ -56,14 +57,14 @@ namespace storm {
template<typename ParametricType>
typename ParameterRegion<ParametricType>::CoefficientType const& ParameterRegion<ParametricType>::getLowerBoundary(VariableType const& variable) const {
auto const& result = lowerBoundaries.find(variable);
- STORM_LOG_THROW(result != lowerBoundaries.end(), storm::exceptions::InvalidArgumentException, "tried to find a lower boundary of a variable that is not specified by this region");
+ STORM_LOG_THROW(result != lowerBoundaries.end(), storm::exceptions::InvalidArgumentException, "tried to find a lower boundary for variable " << variable << " which is not specified by this region");
return (*result).second;
}
template<typename ParametricType>
typename ParameterRegion<ParametricType>::CoefficientType const& ParameterRegion<ParametricType>::getUpperBoundary(VariableType const& variable) const {
auto const& result = upperBoundaries.find(variable);
- STORM_LOG_THROW(result != upperBoundaries.end(), storm::exceptions::InvalidArgumentException, "tried to find an upper boundary of a variable that is not specified by this region");
+ STORM_LOG_THROW(result != upperBoundaries.end(), storm::exceptions::InvalidArgumentException, "tried to find an upper boundary for variable " << variable << " which is not specified by this region");
return (*result).second;
}
@@ -108,7 +109,55 @@ namespace storm {
typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getSomePoint() const {
return this->getLowerBoundaries();
}
+
+ template<typename ParametricType>
+ typename ParameterRegion<ParametricType>::VariableSubstitutionType ParameterRegion<ParametricType>::getCenterPoint() const {
+ VariableSubstitutionType result;
+ for (auto const& variable : this->variables) {
+ result.insert(typename VariableSubstitutionType::value_type(variable, (this->getLowerBoundary(variable) + this->getUpperBoundary(variable))/2));
+ }
+ return result;
+ }
+
+ template<typename ParametricType>
+ typename ParameterRegion<ParametricType>::CoefficientType ParameterRegion<ParametricType>::area() const{
+ CoefficientType result = storm::utility::one<CoefficientType>();
+ for( auto const& variable : this->variables){
+ result *= (this->getUpperBoundary(variable) - this->getLowerBoundary(variable));
+ }
+ return result;
+ }
+ template<typename ParametricType>
+ void ParameterRegion<ParametricType>::split(VariableSubstitutionType const& splittingPoint, std::vector<ParameterRegion<ParametricType> >& regionVector) const{
+ //Check if splittingPoint is valid.
+ STORM_LOG_THROW(splittingPoint.size() == this->variables.size(), storm::exceptions::InvalidArgumentException, "Tried to split a region w.r.t. a point, but the point considers a different number of variables.");
+ for(auto const& variable : this->variables){
+ auto splittingPointEntry=splittingPoint.find(variable);
+ STORM_LOG_THROW(splittingPointEntry != splittingPoint.end(), storm::exceptions::InvalidArgumentException, "tried to split a region but a variable of this region is not defined by the splitting point.");
+ STORM_LOG_THROW(this->getLowerBoundary(variable) <=splittingPointEntry->second, storm::exceptions::InvalidArgumentException, "tried to split a region but the splitting point is not contained in the region.");
+ STORM_LOG_THROW(this->getUpperBoundary(variable) >=splittingPointEntry->second, storm::exceptions::InvalidArgumentException, "tried to split a region but the splitting point is not contained in the region.");
+ }
+
+ //Now compute the subregions.
+ std::vector<VariableSubstitutionType> vertices(this->getVerticesOfRegion(this->variables));
+ for(auto const& vertex : vertices){
+ //The resulting subregion is the smallest region containing vertex and splittingPoint.
+ VariableSubstitutionType subLower, subUpper;
+ for(auto variableBound : this->lowerBoundaries){
+ Variable variable = variableBound.first;
+ auto vertexEntry=vertex.find(variable);
+ auto splittingPointEntry=splittingPoint.find(variable);
+ subLower.insert(typename VariableSubstitutionType::value_type(variable, std::min(vertexEntry->second, splittingPointEntry->second)));
+ subUpper.insert(typename VariableSubstitutionType::value_type(variable, std::max(vertexEntry->second, splittingPointEntry->second)));
+ }
+ ParameterRegion<ParametricType> subRegion((subLower), (subUpper));
+ if(subRegion.area() != storm::utility::zero<CoefficientType>()){
+ regionVector.push_back((subRegion));
+ }
+ }
+ }
+
template<typename ParametricType>
RegionCheckResult ParameterRegion<ParametricType>::getCheckResult() const {
return checkResult;
diff --git a/src/modelchecker/region/ParameterRegion.h b/src/modelchecker/region/ParameterRegion.h
index e79e29001..e06f3ed2b 100644
--- a/src/modelchecker/region/ParameterRegion.h
+++ b/src/modelchecker/region/ParameterRegion.h
@@ -27,6 +27,8 @@ namespace storm {
ParameterRegion(VariableSubstitutionType const& lowerBounds, VariableSubstitutionType const& upperBounds);
ParameterRegion(VariableSubstitutionType&& lowerBounds, VariableSubstitutionType&& upperBounds);
+ ParameterRegion(ParameterRegion const& pr) = default;
+
virtual ~ParameterRegion();
std::set<VariableType> getVariables() const;
@@ -50,6 +52,23 @@ namespace storm {
* Returns some point that lies within this region
*/
VariableSubstitutionType getSomePoint() const;
+
+ /*!
+ * Returns the center point of this region
+ */
+ VariableSubstitutionType getCenterPoint() const;
+
+ /*!
+ * Returns the area of this region
+ */
+ CoefficientType area() const;
+
+ /*!
+ * Splits the region at the given point and inserts the resulting subregions at the end of the given vector.
+ * It is assumed that the point lies within this region.
+ * Subregions with area()==0 are not inserted in the vector.
+ */
+ void split(VariableSubstitutionType const& splittingPoint, std::vector<ParameterRegion<ParametricType>>& regionVector) const;
RegionCheckResult getCheckResult() const;
void setCheckResult(RegionCheckResult checkResult);
@@ -128,8 +147,8 @@ namespace storm {
void init();
- VariableSubstitutionType const lowerBoundaries;
- VariableSubstitutionType const upperBoundaries;
+ VariableSubstitutionType lowerBoundaries;
+ VariableSubstitutionType upperBoundaries;
std::set<VariableType> variables;
RegionCheckResult checkResult;
VariableSubstitutionType satPoint;
diff --git a/src/settings/modules/RegionSettings.cpp b/src/settings/modules/RegionSettings.cpp
index 2f15e15c1..0e36af58d 100644
--- a/src/settings/modules/RegionSettings.cpp
+++ b/src/settings/modules/RegionSettings.cpp
@@ -17,6 +17,7 @@ namespace storm {
const std::string RegionSettings::approxmodeOptionName = "approxmode";
const std::string RegionSettings::samplemodeOptionName = "samplemode";
const std::string RegionSettings::smtmodeOptionName = "smtmode";
+ const std::string RegionSettings::refinementOptionName = "refinement";
RegionSettings::RegionSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName), modesModified(false) {
this->addOption(storm::settings::OptionBuilder(moduleName, regionfileOptionName, true, "Specifies the regions via a file. Format: 0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9")
@@ -36,6 +37,8 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, smtmodeOptionName, true, "Sets whether SMT solving should be done and whether to encode it via a function or the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("mode", "The mode, (off, function (default), model)")
.addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(smtModes)).setDefaultValueString("off").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, refinementOptionName, true, "Sets whether refinement (iteratively split regions) should be done. Only works if exactly one region (the parameter spaces) is specified.")
+ .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("threshold", "Number between zero and one. Sets the fraction of undiscovered area at which refinement stops.").build()).build());
}
bool RegionSettings::isRegionFileSet() const{
@@ -136,12 +139,25 @@ namespace storm {
void RegionSettings::resetModes() {
this->modesModified=false;
}
+
+ bool RegionSettings::doRefinement() const{
+ return this->getOption(refinementOptionName).getHasOptionBeenSet();
+ }
+
+ double RegionSettings::getRefinementThreshold() const{
+ return this->getOption(refinementOptionName).getArgumentByName("threshold").getValueAsDouble();
+ }
+
bool RegionSettings::check() const{
if(isRegionsSet() && isRegionFileSet()){
STORM_LOG_ERROR("Regions specified twice: via command line AND via file.");
return false;
}
+ if(doRefinement() && (getRefinementThreshold()<0.0 || getRefinementThreshold()>1.0)){
+ STORM_LOG_ERROR("Refinement Threshold should be between zero and one.");
+ return false;
+ }
return true;
}
diff --git a/src/settings/modules/RegionSettings.h b/src/settings/modules/RegionSettings.h
index 98368585c..af8e607c9 100644
--- a/src/settings/modules/RegionSettings.h
+++ b/src/settings/modules/RegionSettings.h
@@ -88,6 +88,8 @@ namespace storm {
*/
void resetModes();
+ bool doRefinement() const;
+ double getRefinementThreshold() const;
bool check() const override;
@@ -99,6 +101,7 @@ namespace storm {
const static std::string approxmodeOptionName;
const static std::string samplemodeOptionName;
const static std::string smtmodeOptionName;
+ const static std::string refinementOptionName;
bool modesModified;
ApproxMode approxMode;
diff --git a/src/storm.cpp b/src/storm.cpp
index 3b060120b..d7864fb36 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -1,4 +1,5 @@
// Include other headers.
+#include <chrono>
#include "src/exceptions/BaseException.h"
#include "src/utility/macros.h"
#include "src/cli/cli.h"
@@ -8,6 +9,7 @@
*/
int main(const int argc, const char** argv) {
try {
+ auto starttime = std::chrono::high_resolution_clock::now();
storm::utility::setUp();
storm::cli::printHeader(argc, argv);
bool optionsCorrect = storm::cli::parseOptions(argc, argv);
@@ -20,6 +22,10 @@ int main(const int argc, const char** argv) {
// All operations have now been performed, so we clean up everything and terminate.
storm::utility::cleanUp();
+ auto endtime = std::chrono::high_resolution_clock::now();
+ auto duration = std::chrono::duration_cast<std::chrono::milliseconds>(endtime-starttime);
+ auto durationSec = std::chrono::duration_cast<std::chrono::seconds>(endtime-starttime);
+ std::cout << "OVERALL RUNTIME: " << duration.count() << " ms. ( approx " << durationSec.count() << " seconds)." << std::endl;
return 0;
} catch (storm::exceptions::BaseException const& exception) {
STORM_LOG_ERROR("An exception caused StoRM to terminate. The message of the exception is: " << exception.what());
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 0b58a3d02..fecd67bf8 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -21,7 +21,7 @@
#include "src/settings/modules/BisimulationSettings.h"
#include "src/settings/modules/ParametricSettings.h"
-
+#include "src/settings/modules/RegionSettings.h"
// Formula headers.
#include "src/logic/Formulas.h"