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

implemented refinement of regions plus benchmarks 

Former-commit-id: 09faedc1be
main
TimQu 9 years ago
parent
3ce8643d96
commit
56be3c183b
29 changed files with 236 additions and 645 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. 13
      examples/benchmarkRegions.sh
  2. 46
      examples/benchmarkRegionsRefinement.sh
  3. 2
      examples/pdtmc/brp/brp_space.txt
  4. 2
      examples/pdtmc/brp/models
  5. 625
      examples/pdtmc/brp_rewards2/brp_rewards2_regions.txt
  6. 2
      examples/pdtmc/brp_rewards2/brp_rewards2_space.txt
  7. 6
      examples/pdtmc/brp_rewards2/models
  8. 2
      examples/pdtmc/brp_rewards4/brp_rewards4_space.txt
  9. 4
      examples/pdtmc/brp_rewards4/models
  10. 2
      examples/pdtmc/crowds/crowds_space.txt
  11. 2
      examples/pdtmc/nand/nand_space.txt
  12. 2
      examples/pmdp/brp/brp_space.txt
  13. 1
      examples/pmdp/brp/models
  14. 2
      examples/pmdp/coin2/coin2_space.txt
  15. 0
      examples/pmdp/coin4/coin4.prctl
  16. 2
      examples/pmdp/coin4/coin4_space.txt
  17. 2
      examples/pmdp/firewire/firewire_space.txt
  18. 2
      examples/pmdp/reporter2/reporter2_space.txt
  19. 2
      examples/pmdp/reporter4/reporter4_space.txt
  20. 2
      examples/pmdp/zeroconf/zeroconf_space.txt
  21. 8
      src/cli/entrypoints.h
  22. 36
      src/modelchecker/region/AbstractSparseRegionModelChecker.cpp
  23. 13
      src/modelchecker/region/AbstractSparseRegionModelChecker.h
  24. 53
      src/modelchecker/region/ParameterRegion.cpp
  25. 23
      src/modelchecker/region/ParameterRegion.h
  26. 16
      src/settings/modules/RegionSettings.cpp
  27. 3
      src/settings/modules/RegionSettings.h
  28. 6
      src/storm.cpp
  29. 2
      src/utility/storm.h

13
examples/benchmarkRegions.sh
View File

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

46
examples/benchmarkRegionsRefinement.sh
View File

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

2
examples/pdtmc/brp/brp_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=pL<=0.999990, 0.000010<=pK<=0.999990;

2
examples/pdtmc/brp/models
View File

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

625
examples/pdtmc/brp_rewards2/brp_rewards2_regions.txt
View File

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

2
examples/pdtmc/brp_rewards2/brp_rewards2_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=pL<=0.999990, 0.000010<=pK<=0.999990;

6
examples/pdtmc/brp_rewards2/models
View File

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

2
examples/pdtmc/brp_rewards4/brp_rewards4_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=pL<=0.999990, 0.000010<=pK<=0.999990, 0.000010<=TOMsg<=0.999990, 0.000010<=TOAck<=0.999990;

4
examples/pdtmc/brp_rewards4/models
View File

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

2
examples/pdtmc/crowds/crowds_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=PF<=0.999990, 0.000010<=badC<=0.999990;

2
examples/pdtmc/nand/nand_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=perr<=0.999990, 0.000010<=prob1<=0.999990;

2
examples/pmdp/brp/brp_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=pL<=0.999990, 0.000010<=pK<=0.999990;

1
examples/pmdp/brp/models
View File

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

2
examples/pmdp/coin2/coin2_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=p1<=0.999990, 0.000010<=p2<=0.999990;

0
examples/pmdp/coin4/coin2.prctl → examples/pmdp/coin4/coin4.prctl
View File

2
examples/pmdp/coin4/coin4_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=p1<=0.999990, 0.000010<=p2<=0.999990, 0.000010<=p3<=0.999990, 0.000010<=p4<=0.999990;

2
examples/pmdp/firewire/firewire_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=fast1<=0.999990, 0.000010<=fast2<=0.999990;

2
examples/pmdp/reporter2/reporter2_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=pL<=0.999990, 0.000010<=pH<=0.999990;

2
examples/pmdp/reporter4/reporter4_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=pL<=0.999990, 0.000010<=pH<=0.999990, 0.000010<=pLDiff<=0.999990, 0.000010<=pHDiff<=0.999990;

2
examples/pmdp/zeroconf/zeroconf_space.txt
View File

@ -0,0 +1,2 @@
0.000010<=loss<=0.999990, 0.000010<=old<=0.999990;

8
src/cli/entrypoints.h
View File

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

36
src/modelchecker/region/AbstractSparseRegionModelChecker.cpp
View File

@ -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();

13
src/modelchecker/region/AbstractSparseRegionModelChecker.h
View File

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

53
src/modelchecker/region/ParameterRegion.cpp
View File

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

23
src/modelchecker/region/ParameterRegion.h
View File

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

16
src/settings/modules/RegionSettings.cpp
View File

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

3
src/settings/modules/RegionSettings.h
View File

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

6
src/storm.cpp
View File

@ -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());

2
src/utility/storm.h
View File

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

Write Preview
Loading…
Cancel
Save