diff --git a/examples/pdtmc/brp_rewards/brp_rewards.prctl b/examples/pdtmc/brp_rewards/brp_rewards.prctl index 438f1c4b0..3a194c0be 100644 --- a/examples/pdtmc/brp_rewards/brp_rewards.prctl +++ b/examples/pdtmc/brp_rewards/brp_rewards.prctl @@ -1,2 +1,2 @@ -R<2 [ F ((s=5) | (s=0&srep=3)) ] +R<3 [ F ((s=5) | (s=0&srep=3)) ] diff --git a/examples/pmdp/brp/brpRegions.txt b/examples/pmdp/brp/brpRegions.txt deleted file mode 100644 index fe67834cc..000000000 --- a/examples/pmdp/brp/brpRegions.txt +++ /dev/null @@ -1,400 +0,0 @@ -0.000010<=pL<=0.050000, 0.000010<=pK<=0.050000; -0.000010<=pL<=0.050000, 0.050000<=pK<=0.100000; -0.000010<=pL<=0.050000, 0.100000<=pK<=0.150000; -0.000010<=pL<=0.050000, 0.150000<=pK<=0.200000; -0.000010<=pL<=0.050000, 0.200000<=pK<=0.250000; -0.000010<=pL<=0.050000, 0.250000<=pK<=0.300000; -0.000010<=pL<=0.050000, 0.300000<=pK<=0.350000; -0.000010<=pL<=0.050000, 0.350000<=pK<=0.400000; -0.000010<=pL<=0.050000, 0.400000<=pK<=0.450000; -0.000010<=pL<=0.050000, 0.450000<=pK<=0.500000; -0.000010<=pL<=0.050000, 0.500000<=pK<=0.550000; -0.000010<=pL<=0.050000, 0.550000<=pK<=0.600000; -0.000010<=pL<=0.050000, 0.600000<=pK<=0.650000; -0.000010<=pL<=0.050000, 0.650000<=pK<=0.700000; -0.000010<=pL<=0.050000, 0.700000<=pK<=0.750000; -0.000010<=pL<=0.050000, 0.750000<=pK<=0.800000; -0.000010<=pL<=0.050000, 0.800000<=pK<=0.850000; -0.000010<=pL<=0.050000, 0.850000<=pK<=0.900000; -0.000010<=pL<=0.050000, 0.900000<=pK<=0.950000; -0.000010<=pL<=0.050000, 0.950000<=pK<=0.999990; -0.050000<=pL<=0.100000, 0.000010<=pK<=0.050000; -0.050000<=pL<=0.100000, 0.050000<=pK<=0.100000; -0.050000<=pL<=0.100000, 0.100000<=pK<=0.150000; -0.050000<=pL<=0.100000, 0.150000<=pK<=0.200000; -0.050000<=pL<=0.100000, 0.200000<=pK<=0.250000; -0.050000<=pL<=0.100000, 0.250000<=pK<=0.300000; -0.050000<=pL<=0.100000, 0.300000<=pK<=0.350000; -0.050000<=pL<=0.100000, 0.350000<=pK<=0.400000; -0.050000<=pL<=0.100000, 0.400000<=pK<=0.450000; -0.050000<=pL<=0.100000, 0.450000<=pK<=0.500000; -0.050000<=pL<=0.100000, 0.500000<=pK<=0.550000; -0.050000<=pL<=0.100000, 0.550000<=pK<=0.600000; -0.050000<=pL<=0.100000, 0.600000<=pK<=0.650000; -0.050000<=pL<=0.100000, 0.650000<=pK<=0.700000; -0.050000<=pL<=0.100000, 0.700000<=pK<=0.750000; -0.050000<=pL<=0.100000, 0.750000<=pK<=0.800000; -0.050000<=pL<=0.100000, 0.800000<=pK<=0.850000; -0.050000<=pL<=0.100000, 0.850000<=pK<=0.900000; -0.050000<=pL<=0.100000, 0.900000<=pK<=0.950000; -0.050000<=pL<=0.100000, 0.950000<=pK<=0.999990; -0.100000<=pL<=0.150000, 0.000010<=pK<=0.050000; -0.100000<=pL<=0.150000, 0.050000<=pK<=0.100000; -0.100000<=pL<=0.150000, 0.100000<=pK<=0.150000; -0.100000<=pL<=0.150000, 0.150000<=pK<=0.200000; -0.100000<=pL<=0.150000, 0.200000<=pK<=0.250000; -0.100000<=pL<=0.150000, 0.250000<=pK<=0.300000; -0.100000<=pL<=0.150000, 0.300000<=pK<=0.350000; -0.100000<=pL<=0.150000, 0.350000<=pK<=0.400000; -0.100000<=pL<=0.150000, 0.400000<=pK<=0.450000; -0.100000<=pL<=0.150000, 0.450000<=pK<=0.500000; -0.100000<=pL<=0.150000, 0.500000<=pK<=0.550000; -0.100000<=pL<=0.150000, 0.550000<=pK<=0.600000; -0.100000<=pL<=0.150000, 0.600000<=pK<=0.650000; -0.100000<=pL<=0.150000, 0.650000<=pK<=0.700000; -0.100000<=pL<=0.150000, 0.700000<=pK<=0.750000; -0.100000<=pL<=0.150000, 0.750000<=pK<=0.800000; -0.100000<=pL<=0.150000, 0.800000<=pK<=0.850000; -0.100000<=pL<=0.150000, 0.850000<=pK<=0.900000; -0.100000<=pL<=0.150000, 0.900000<=pK<=0.950000; -0.100000<=pL<=0.150000, 0.950000<=pK<=0.999990; -0.150000<=pL<=0.200000, 0.000010<=pK<=0.050000; -0.150000<=pL<=0.200000, 0.050000<=pK<=0.100000; -0.150000<=pL<=0.200000, 0.100000<=pK<=0.150000; -0.150000<=pL<=0.200000, 0.150000<=pK<=0.200000; -0.150000<=pL<=0.200000, 0.200000<=pK<=0.250000; -0.150000<=pL<=0.200000, 0.250000<=pK<=0.300000; -0.150000<=pL<=0.200000, 0.300000<=pK<=0.350000; -0.150000<=pL<=0.200000, 0.350000<=pK<=0.400000; -0.150000<=pL<=0.200000, 0.400000<=pK<=0.450000; -0.150000<=pL<=0.200000, 0.450000<=pK<=0.500000; -0.150000<=pL<=0.200000, 0.500000<=pK<=0.550000; -0.150000<=pL<=0.200000, 0.550000<=pK<=0.600000; -0.150000<=pL<=0.200000, 0.600000<=pK<=0.650000; -0.150000<=pL<=0.200000, 0.650000<=pK<=0.700000; -0.150000<=pL<=0.200000, 0.700000<=pK<=0.750000; -0.150000<=pL<=0.200000, 0.750000<=pK<=0.800000; -0.150000<=pL<=0.200000, 0.800000<=pK<=0.850000; -0.150000<=pL<=0.200000, 0.850000<=pK<=0.900000; -0.150000<=pL<=0.200000, 0.900000<=pK<=0.950000; -0.150000<=pL<=0.200000, 0.950000<=pK<=0.999990; -0.200000<=pL<=0.250000, 0.000010<=pK<=0.050000; -0.200000<=pL<=0.250000, 0.050000<=pK<=0.100000; -0.200000<=pL<=0.250000, 0.100000<=pK<=0.150000; -0.200000<=pL<=0.250000, 0.150000<=pK<=0.200000; -0.200000<=pL<=0.250000, 0.200000<=pK<=0.250000; -0.200000<=pL<=0.250000, 0.250000<=pK<=0.300000; -0.200000<=pL<=0.250000, 0.300000<=pK<=0.350000; -0.200000<=pL<=0.250000, 0.350000<=pK<=0.400000; -0.200000<=pL<=0.250000, 0.400000<=pK<=0.450000; -0.200000<=pL<=0.250000, 0.450000<=pK<=0.500000; -0.200000<=pL<=0.250000, 0.500000<=pK<=0.550000; -0.200000<=pL<=0.250000, 0.550000<=pK<=0.600000; -0.200000<=pL<=0.250000, 0.600000<=pK<=0.650000; -0.200000<=pL<=0.250000, 0.650000<=pK<=0.700000; -0.200000<=pL<=0.250000, 0.700000<=pK<=0.750000; -0.200000<=pL<=0.250000, 0.750000<=pK<=0.800000; -0.200000<=pL<=0.250000, 0.800000<=pK<=0.850000; -0.200000<=pL<=0.250000, 0.850000<=pK<=0.900000; -0.200000<=pL<=0.250000, 0.900000<=pK<=0.950000; -0.200000<=pL<=0.250000, 0.950000<=pK<=0.999990; -0.250000<=pL<=0.300000, 0.000010<=pK<=0.050000; -0.250000<=pL<=0.300000, 0.050000<=pK<=0.100000; -0.250000<=pL<=0.300000, 0.100000<=pK<=0.150000; -0.250000<=pL<=0.300000, 0.150000<=pK<=0.200000; -0.250000<=pL<=0.300000, 0.200000<=pK<=0.250000; -0.250000<=pL<=0.300000, 0.250000<=pK<=0.300000; -0.250000<=pL<=0.300000, 0.300000<=pK<=0.350000; -0.250000<=pL<=0.300000, 0.350000<=pK<=0.400000; -0.250000<=pL<=0.300000, 0.400000<=pK<=0.450000; -0.250000<=pL<=0.300000, 0.450000<=pK<=0.500000; -0.250000<=pL<=0.300000, 0.500000<=pK<=0.550000; -0.250000<=pL<=0.300000, 0.550000<=pK<=0.600000; -0.250000<=pL<=0.300000, 0.600000<=pK<=0.650000; -0.250000<=pL<=0.300000, 0.650000<=pK<=0.700000; -0.250000<=pL<=0.300000, 0.700000<=pK<=0.750000; -0.250000<=pL<=0.300000, 0.750000<=pK<=0.800000; -0.250000<=pL<=0.300000, 0.800000<=pK<=0.850000; -0.250000<=pL<=0.300000, 0.850000<=pK<=0.900000; -0.250000<=pL<=0.300000, 0.900000<=pK<=0.950000; -0.250000<=pL<=0.300000, 0.950000<=pK<=0.999990; -0.300000<=pL<=0.350000, 0.000010<=pK<=0.050000; -0.300000<=pL<=0.350000, 0.050000<=pK<=0.100000; -0.300000<=pL<=0.350000, 0.100000<=pK<=0.150000; -0.300000<=pL<=0.350000, 0.150000<=pK<=0.200000; -0.300000<=pL<=0.350000, 0.200000<=pK<=0.250000; -0.300000<=pL<=0.350000, 0.250000<=pK<=0.300000; -0.300000<=pL<=0.350000, 0.300000<=pK<=0.350000; -0.300000<=pL<=0.350000, 0.350000<=pK<=0.400000; -0.300000<=pL<=0.350000, 0.400000<=pK<=0.450000; -0.300000<=pL<=0.350000, 0.450000<=pK<=0.500000; -0.300000<=pL<=0.350000, 0.500000<=pK<=0.550000; -0.300000<=pL<=0.350000, 0.550000<=pK<=0.600000; -0.300000<=pL<=0.350000, 0.600000<=pK<=0.650000; -0.300000<=pL<=0.350000, 0.650000<=pK<=0.700000; -0.300000<=pL<=0.350000, 0.700000<=pK<=0.750000; -0.300000<=pL<=0.350000, 0.750000<=pK<=0.800000; -0.300000<=pL<=0.350000, 0.800000<=pK<=0.850000; -0.300000<=pL<=0.350000, 0.850000<=pK<=0.900000; -0.300000<=pL<=0.350000, 0.900000<=pK<=0.950000; -0.300000<=pL<=0.350000, 0.950000<=pK<=0.999990; -0.350000<=pL<=0.400000, 0.000010<=pK<=0.050000; -0.350000<=pL<=0.400000, 0.050000<=pK<=0.100000; -0.350000<=pL<=0.400000, 0.100000<=pK<=0.150000; -0.350000<=pL<=0.400000, 0.150000<=pK<=0.200000; -0.350000<=pL<=0.400000, 0.200000<=pK<=0.250000; -0.350000<=pL<=0.400000, 0.250000<=pK<=0.300000; -0.350000<=pL<=0.400000, 0.300000<=pK<=0.350000; -0.350000<=pL<=0.400000, 0.350000<=pK<=0.400000; -0.350000<=pL<=0.400000, 0.400000<=pK<=0.450000; -0.350000<=pL<=0.400000, 0.450000<=pK<=0.500000; -0.350000<=pL<=0.400000, 0.500000<=pK<=0.550000; -0.350000<=pL<=0.400000, 0.550000<=pK<=0.600000; -0.350000<=pL<=0.400000, 0.600000<=pK<=0.650000; -0.350000<=pL<=0.400000, 0.650000<=pK<=0.700000; -0.350000<=pL<=0.400000, 0.700000<=pK<=0.750000; -0.350000<=pL<=0.400000, 0.750000<=pK<=0.800000; -0.350000<=pL<=0.400000, 0.800000<=pK<=0.850000; -0.350000<=pL<=0.400000, 0.850000<=pK<=0.900000; -0.350000<=pL<=0.400000, 0.900000<=pK<=0.950000; -0.350000<=pL<=0.400000, 0.950000<=pK<=0.999990; -0.400000<=pL<=0.450000, 0.000010<=pK<=0.050000; -0.400000<=pL<=0.450000, 0.050000<=pK<=0.100000; -0.400000<=pL<=0.450000, 0.100000<=pK<=0.150000; -0.400000<=pL<=0.450000, 0.150000<=pK<=0.200000; -0.400000<=pL<=0.450000, 0.200000<=pK<=0.250000; -0.400000<=pL<=0.450000, 0.250000<=pK<=0.300000; -0.400000<=pL<=0.450000, 0.300000<=pK<=0.350000; -0.400000<=pL<=0.450000, 0.350000<=pK<=0.400000; -0.400000<=pL<=0.450000, 0.400000<=pK<=0.450000; -0.400000<=pL<=0.450000, 0.450000<=pK<=0.500000; -0.400000<=pL<=0.450000, 0.500000<=pK<=0.550000; -0.400000<=pL<=0.450000, 0.550000<=pK<=0.600000; -0.400000<=pL<=0.450000, 0.600000<=pK<=0.650000; -0.400000<=pL<=0.450000, 0.650000<=pK<=0.700000; -0.400000<=pL<=0.450000, 0.700000<=pK<=0.750000; -0.400000<=pL<=0.450000, 0.750000<=pK<=0.800000; -0.400000<=pL<=0.450000, 0.800000<=pK<=0.850000; -0.400000<=pL<=0.450000, 0.850000<=pK<=0.900000; -0.400000<=pL<=0.450000, 0.900000<=pK<=0.950000; -0.400000<=pL<=0.450000, 0.950000<=pK<=0.999990; -0.450000<=pL<=0.500000, 0.000010<=pK<=0.050000; -0.450000<=pL<=0.500000, 0.050000<=pK<=0.100000; -0.450000<=pL<=0.500000, 0.100000<=pK<=0.150000; -0.450000<=pL<=0.500000, 0.150000<=pK<=0.200000; -0.450000<=pL<=0.500000, 0.200000<=pK<=0.250000; -0.450000<=pL<=0.500000, 0.250000<=pK<=0.300000; -0.450000<=pL<=0.500000, 0.300000<=pK<=0.350000; -0.450000<=pL<=0.500000, 0.350000<=pK<=0.400000; -0.450000<=pL<=0.500000, 0.400000<=pK<=0.450000; -0.450000<=pL<=0.500000, 0.450000<=pK<=0.500000; -0.450000<=pL<=0.500000, 0.500000<=pK<=0.550000; -0.450000<=pL<=0.500000, 0.550000<=pK<=0.600000; -0.450000<=pL<=0.500000, 0.600000<=pK<=0.650000; -0.450000<=pL<=0.500000, 0.650000<=pK<=0.700000; -0.450000<=pL<=0.500000, 0.700000<=pK<=0.750000; -0.450000<=pL<=0.500000, 0.750000<=pK<=0.800000; -0.450000<=pL<=0.500000, 0.800000<=pK<=0.850000; -0.450000<=pL<=0.500000, 0.850000<=pK<=0.900000; -0.450000<=pL<=0.500000, 0.900000<=pK<=0.950000; -0.450000<=pL<=0.500000, 0.950000<=pK<=0.999990; -0.500000<=pL<=0.550000, 0.000010<=pK<=0.050000; -0.500000<=pL<=0.550000, 0.050000<=pK<=0.100000; -0.500000<=pL<=0.550000, 0.100000<=pK<=0.150000; -0.500000<=pL<=0.550000, 0.150000<=pK<=0.200000; -0.500000<=pL<=0.550000, 0.200000<=pK<=0.250000; -0.500000<=pL<=0.550000, 0.250000<=pK<=0.300000; -0.500000<=pL<=0.550000, 0.300000<=pK<=0.350000; -0.500000<=pL<=0.550000, 0.350000<=pK<=0.400000; -0.500000<=pL<=0.550000, 0.400000<=pK<=0.450000; -0.500000<=pL<=0.550000, 0.450000<=pK<=0.500000; -0.500000<=pL<=0.550000, 0.500000<=pK<=0.550000; -0.500000<=pL<=0.550000, 0.550000<=pK<=0.600000; -0.500000<=pL<=0.550000, 0.600000<=pK<=0.650000; -0.500000<=pL<=0.550000, 0.650000<=pK<=0.700000; -0.500000<=pL<=0.550000, 0.700000<=pK<=0.750000; -0.500000<=pL<=0.550000, 0.750000<=pK<=0.800000; -0.500000<=pL<=0.550000, 0.800000<=pK<=0.850000; -0.500000<=pL<=0.550000, 0.850000<=pK<=0.900000; -0.500000<=pL<=0.550000, 0.900000<=pK<=0.950000; -0.500000<=pL<=0.550000, 0.950000<=pK<=0.999990; -0.550000<=pL<=0.600000, 0.000010<=pK<=0.050000; -0.550000<=pL<=0.600000, 0.050000<=pK<=0.100000; -0.550000<=pL<=0.600000, 0.100000<=pK<=0.150000; -0.550000<=pL<=0.600000, 0.150000<=pK<=0.200000; -0.550000<=pL<=0.600000, 0.200000<=pK<=0.250000; -0.550000<=pL<=0.600000, 0.250000<=pK<=0.300000; -0.550000<=pL<=0.600000, 0.300000<=pK<=0.350000; -0.550000<=pL<=0.600000, 0.350000<=pK<=0.400000; -0.550000<=pL<=0.600000, 0.400000<=pK<=0.450000; -0.550000<=pL<=0.600000, 0.450000<=pK<=0.500000; -0.550000<=pL<=0.600000, 0.500000<=pK<=0.550000; -0.550000<=pL<=0.600000, 0.550000<=pK<=0.600000; -0.550000<=pL<=0.600000, 0.600000<=pK<=0.650000; -0.550000<=pL<=0.600000, 0.650000<=pK<=0.700000; -0.550000<=pL<=0.600000, 0.700000<=pK<=0.750000; -0.550000<=pL<=0.600000, 0.750000<=pK<=0.800000; -0.550000<=pL<=0.600000, 0.800000<=pK<=0.850000; -0.550000<=pL<=0.600000, 0.850000<=pK<=0.900000; -0.550000<=pL<=0.600000, 0.900000<=pK<=0.950000; -0.550000<=pL<=0.600000, 0.950000<=pK<=0.999990; -0.600000<=pL<=0.650000, 0.000010<=pK<=0.050000; -0.600000<=pL<=0.650000, 0.050000<=pK<=0.100000; -0.600000<=pL<=0.650000, 0.100000<=pK<=0.150000; -0.600000<=pL<=0.650000, 0.150000<=pK<=0.200000; -0.600000<=pL<=0.650000, 0.200000<=pK<=0.250000; -0.600000<=pL<=0.650000, 0.250000<=pK<=0.300000; -0.600000<=pL<=0.650000, 0.300000<=pK<=0.350000; -0.600000<=pL<=0.650000, 0.350000<=pK<=0.400000; -0.600000<=pL<=0.650000, 0.400000<=pK<=0.450000; -0.600000<=pL<=0.650000, 0.450000<=pK<=0.500000; -0.600000<=pL<=0.650000, 0.500000<=pK<=0.550000; -0.600000<=pL<=0.650000, 0.550000<=pK<=0.600000; -0.600000<=pL<=0.650000, 0.600000<=pK<=0.650000; -0.600000<=pL<=0.650000, 0.650000<=pK<=0.700000; -0.600000<=pL<=0.650000, 0.700000<=pK<=0.750000; -0.600000<=pL<=0.650000, 0.750000<=pK<=0.800000; -0.600000<=pL<=0.650000, 0.800000<=pK<=0.850000; -0.600000<=pL<=0.650000, 0.850000<=pK<=0.900000; -0.600000<=pL<=0.650000, 0.900000<=pK<=0.950000; -0.600000<=pL<=0.650000, 0.950000<=pK<=0.999990; -0.650000<=pL<=0.700000, 0.000010<=pK<=0.050000; -0.650000<=pL<=0.700000, 0.050000<=pK<=0.100000; -0.650000<=pL<=0.700000, 0.100000<=pK<=0.150000; -0.650000<=pL<=0.700000, 0.150000<=pK<=0.200000; -0.650000<=pL<=0.700000, 0.200000<=pK<=0.250000; -0.650000<=pL<=0.700000, 0.250000<=pK<=0.300000; -0.650000<=pL<=0.700000, 0.300000<=pK<=0.350000; -0.650000<=pL<=0.700000, 0.350000<=pK<=0.400000; -0.650000<=pL<=0.700000, 0.400000<=pK<=0.450000; -0.650000<=pL<=0.700000, 0.450000<=pK<=0.500000; -0.650000<=pL<=0.700000, 0.500000<=pK<=0.550000; -0.650000<=pL<=0.700000, 0.550000<=pK<=0.600000; -0.650000<=pL<=0.700000, 0.600000<=pK<=0.650000; -0.650000<=pL<=0.700000, 0.650000<=pK<=0.700000; -0.650000<=pL<=0.700000, 0.700000<=pK<=0.750000; -0.650000<=pL<=0.700000, 0.750000<=pK<=0.800000; -0.650000<=pL<=0.700000, 0.800000<=pK<=0.850000; -0.650000<=pL<=0.700000, 0.850000<=pK<=0.900000; -0.650000<=pL<=0.700000, 0.900000<=pK<=0.950000; -0.650000<=pL<=0.700000, 0.950000<=pK<=0.999990; -0.700000<=pL<=0.750000, 0.000010<=pK<=0.050000; -0.700000<=pL<=0.750000, 0.050000<=pK<=0.100000; -0.700000<=pL<=0.750000, 0.100000<=pK<=0.150000; -0.700000<=pL<=0.750000, 0.150000<=pK<=0.200000; -0.700000<=pL<=0.750000, 0.200000<=pK<=0.250000; -0.700000<=pL<=0.750000, 0.250000<=pK<=0.300000; -0.700000<=pL<=0.750000, 0.300000<=pK<=0.350000; -0.700000<=pL<=0.750000, 0.350000<=pK<=0.400000; -0.700000<=pL<=0.750000, 0.400000<=pK<=0.450000; -0.700000<=pL<=0.750000, 0.450000<=pK<=0.500000; -0.700000<=pL<=0.750000, 0.500000<=pK<=0.550000; -0.700000<=pL<=0.750000, 0.550000<=pK<=0.600000; -0.700000<=pL<=0.750000, 0.600000<=pK<=0.650000; -0.700000<=pL<=0.750000, 0.650000<=pK<=0.700000; -0.700000<=pL<=0.750000, 0.700000<=pK<=0.750000; -0.700000<=pL<=0.750000, 0.750000<=pK<=0.800000; -0.700000<=pL<=0.750000, 0.800000<=pK<=0.850000; -0.700000<=pL<=0.750000, 0.850000<=pK<=0.900000; -0.700000<=pL<=0.750000, 0.900000<=pK<=0.950000; -0.700000<=pL<=0.750000, 0.950000<=pK<=0.999990; -0.750000<=pL<=0.800000, 0.000010<=pK<=0.050000; -0.750000<=pL<=0.800000, 0.050000<=pK<=0.100000; -0.750000<=pL<=0.800000, 0.100000<=pK<=0.150000; -0.750000<=pL<=0.800000, 0.150000<=pK<=0.200000; -0.750000<=pL<=0.800000, 0.200000<=pK<=0.250000; -0.750000<=pL<=0.800000, 0.250000<=pK<=0.300000; -0.750000<=pL<=0.800000, 0.300000<=pK<=0.350000; -0.750000<=pL<=0.800000, 0.350000<=pK<=0.400000; -0.750000<=pL<=0.800000, 0.400000<=pK<=0.450000; -0.750000<=pL<=0.800000, 0.450000<=pK<=0.500000; -0.750000<=pL<=0.800000, 0.500000<=pK<=0.550000; -0.750000<=pL<=0.800000, 0.550000<=pK<=0.600000; -0.750000<=pL<=0.800000, 0.600000<=pK<=0.650000; -0.750000<=pL<=0.800000, 0.650000<=pK<=0.700000; -0.750000<=pL<=0.800000, 0.700000<=pK<=0.750000; -0.750000<=pL<=0.800000, 0.750000<=pK<=0.800000; -0.750000<=pL<=0.800000, 0.800000<=pK<=0.850000; -0.750000<=pL<=0.800000, 0.850000<=pK<=0.900000; -0.750000<=pL<=0.800000, 0.900000<=pK<=0.950000; -0.750000<=pL<=0.800000, 0.950000<=pK<=0.999990; -0.800000<=pL<=0.850000, 0.000010<=pK<=0.050000; -0.800000<=pL<=0.850000, 0.050000<=pK<=0.100000; -0.800000<=pL<=0.850000, 0.100000<=pK<=0.150000; -0.800000<=pL<=0.850000, 0.150000<=pK<=0.200000; -0.800000<=pL<=0.850000, 0.200000<=pK<=0.250000; -0.800000<=pL<=0.850000, 0.250000<=pK<=0.300000; -0.800000<=pL<=0.850000, 0.300000<=pK<=0.350000; -0.800000<=pL<=0.850000, 0.350000<=pK<=0.400000; -0.800000<=pL<=0.850000, 0.400000<=pK<=0.450000; -0.800000<=pL<=0.850000, 0.450000<=pK<=0.500000; -0.800000<=pL<=0.850000, 0.500000<=pK<=0.550000; -0.800000<=pL<=0.850000, 0.550000<=pK<=0.600000; -0.800000<=pL<=0.850000, 0.600000<=pK<=0.650000; -0.800000<=pL<=0.850000, 0.650000<=pK<=0.700000; -0.800000<=pL<=0.850000, 0.700000<=pK<=0.750000; -0.800000<=pL<=0.850000, 0.750000<=pK<=0.800000; -0.800000<=pL<=0.850000, 0.800000<=pK<=0.850000; -0.800000<=pL<=0.850000, 0.850000<=pK<=0.900000; -0.800000<=pL<=0.850000, 0.900000<=pK<=0.950000; -0.800000<=pL<=0.850000, 0.950000<=pK<=0.999990; -0.850000<=pL<=0.900000, 0.000010<=pK<=0.050000; -0.850000<=pL<=0.900000, 0.050000<=pK<=0.100000; -0.850000<=pL<=0.900000, 0.100000<=pK<=0.150000; -0.850000<=pL<=0.900000, 0.150000<=pK<=0.200000; -0.850000<=pL<=0.900000, 0.200000<=pK<=0.250000; -0.850000<=pL<=0.900000, 0.250000<=pK<=0.300000; -0.850000<=pL<=0.900000, 0.300000<=pK<=0.350000; -0.850000<=pL<=0.900000, 0.350000<=pK<=0.400000; -0.850000<=pL<=0.900000, 0.400000<=pK<=0.450000; -0.850000<=pL<=0.900000, 0.450000<=pK<=0.500000; -0.850000<=pL<=0.900000, 0.500000<=pK<=0.550000; -0.850000<=pL<=0.900000, 0.550000<=pK<=0.600000; -0.850000<=pL<=0.900000, 0.600000<=pK<=0.650000; -0.850000<=pL<=0.900000, 0.650000<=pK<=0.700000; -0.850000<=pL<=0.900000, 0.700000<=pK<=0.750000; -0.850000<=pL<=0.900000, 0.750000<=pK<=0.800000; -0.850000<=pL<=0.900000, 0.800000<=pK<=0.850000; -0.850000<=pL<=0.900000, 0.850000<=pK<=0.900000; -0.850000<=pL<=0.900000, 0.900000<=pK<=0.950000; -0.850000<=pL<=0.900000, 0.950000<=pK<=0.999990; -0.900000<=pL<=0.950000, 0.000010<=pK<=0.050000; -0.900000<=pL<=0.950000, 0.050000<=pK<=0.100000; -0.900000<=pL<=0.950000, 0.100000<=pK<=0.150000; -0.900000<=pL<=0.950000, 0.150000<=pK<=0.200000; -0.900000<=pL<=0.950000, 0.200000<=pK<=0.250000; -0.900000<=pL<=0.950000, 0.250000<=pK<=0.300000; -0.900000<=pL<=0.950000, 0.300000<=pK<=0.350000; -0.900000<=pL<=0.950000, 0.350000<=pK<=0.400000; -0.900000<=pL<=0.950000, 0.400000<=pK<=0.450000; -0.900000<=pL<=0.950000, 0.450000<=pK<=0.500000; -0.900000<=pL<=0.950000, 0.500000<=pK<=0.550000; -0.900000<=pL<=0.950000, 0.550000<=pK<=0.600000; -0.900000<=pL<=0.950000, 0.600000<=pK<=0.650000; -0.900000<=pL<=0.950000, 0.650000<=pK<=0.700000; -0.900000<=pL<=0.950000, 0.700000<=pK<=0.750000; -0.900000<=pL<=0.950000, 0.750000<=pK<=0.800000; -0.900000<=pL<=0.950000, 0.800000<=pK<=0.850000; -0.900000<=pL<=0.950000, 0.850000<=pK<=0.900000; -0.900000<=pL<=0.950000, 0.900000<=pK<=0.950000; -0.900000<=pL<=0.950000, 0.950000<=pK<=0.999990; -0.950000<=pL<=0.999990, 0.000010<=pK<=0.050000; -0.950000<=pL<=0.999990, 0.050000<=pK<=0.100000; -0.950000<=pL<=0.999990, 0.100000<=pK<=0.150000; -0.950000<=pL<=0.999990, 0.150000<=pK<=0.200000; -0.950000<=pL<=0.999990, 0.200000<=pK<=0.250000; -0.950000<=pL<=0.999990, 0.250000<=pK<=0.300000; -0.950000<=pL<=0.999990, 0.300000<=pK<=0.350000; -0.950000<=pL<=0.999990, 0.350000<=pK<=0.400000; -0.950000<=pL<=0.999990, 0.400000<=pK<=0.450000; -0.950000<=pL<=0.999990, 0.450000<=pK<=0.500000; -0.950000<=pL<=0.999990, 0.500000<=pK<=0.550000; -0.950000<=pL<=0.999990, 0.550000<=pK<=0.600000; -0.950000<=pL<=0.999990, 0.600000<=pK<=0.650000; -0.950000<=pL<=0.999990, 0.650000<=pK<=0.700000; -0.950000<=pL<=0.999990, 0.700000<=pK<=0.750000; -0.950000<=pL<=0.999990, 0.750000<=pK<=0.800000; -0.950000<=pL<=0.999990, 0.800000<=pK<=0.850000; -0.950000<=pL<=0.999990, 0.850000<=pK<=0.900000; -0.950000<=pL<=0.999990, 0.900000<=pK<=0.950000; -0.950000<=pL<=0.999990, 0.950000<=pK<=0.999990; diff --git a/examples/pmdp/coin/coin2ParRegions.txt b/examples/pmdp/coin/coin2ParRegions.txt deleted file mode 100644 index 80387f197..000000000 --- a/examples/pmdp/coin/coin2ParRegions.txt +++ /dev/null @@ -1,400 +0,0 @@ -0.000010<=p1<=0.050000, 0.000010<=p2<=0.050000; -0.000010<=p1<=0.050000, 0.050000<=p2<=0.100000; -0.000010<=p1<=0.050000, 0.100000<=p2<=0.150000; -0.000010<=p1<=0.050000, 0.150000<=p2<=0.200000; -0.000010<=p1<=0.050000, 0.200000<=p2<=0.250000; -0.000010<=p1<=0.050000, 0.250000<=p2<=0.300000; -0.000010<=p1<=0.050000, 0.300000<=p2<=0.350000; -0.000010<=p1<=0.050000, 0.350000<=p2<=0.400000; -0.000010<=p1<=0.050000, 0.400000<=p2<=0.450000; -0.000010<=p1<=0.050000, 0.450000<=p2<=0.500000; -0.000010<=p1<=0.050000, 0.500000<=p2<=0.550000; -0.000010<=p1<=0.050000, 0.550000<=p2<=0.600000; -0.000010<=p1<=0.050000, 0.600000<=p2<=0.650000; -0.000010<=p1<=0.050000, 0.650000<=p2<=0.700000; -0.000010<=p1<=0.050000, 0.700000<=p2<=0.750000; -0.000010<=p1<=0.050000, 0.750000<=p2<=0.800000; -0.000010<=p1<=0.050000, 0.800000<=p2<=0.850000; -0.000010<=p1<=0.050000, 0.850000<=p2<=0.900000; -0.000010<=p1<=0.050000, 0.900000<=p2<=0.950000; -0.000010<=p1<=0.050000, 0.950000<=p2<=0.999990; -0.050000<=p1<=0.100000, 0.000010<=p2<=0.050000; -0.050000<=p1<=0.100000, 0.050000<=p2<=0.100000; -0.050000<=p1<=0.100000, 0.100000<=p2<=0.150000; -0.050000<=p1<=0.100000, 0.150000<=p2<=0.200000; -0.050000<=p1<=0.100000, 0.200000<=p2<=0.250000; -0.050000<=p1<=0.100000, 0.250000<=p2<=0.300000; -0.050000<=p1<=0.100000, 0.300000<=p2<=0.350000; -0.050000<=p1<=0.100000, 0.350000<=p2<=0.400000; -0.050000<=p1<=0.100000, 0.400000<=p2<=0.450000; -0.050000<=p1<=0.100000, 0.450000<=p2<=0.500000; -0.050000<=p1<=0.100000, 0.500000<=p2<=0.550000; -0.050000<=p1<=0.100000, 0.550000<=p2<=0.600000; -0.050000<=p1<=0.100000, 0.600000<=p2<=0.650000; -0.050000<=p1<=0.100000, 0.650000<=p2<=0.700000; -0.050000<=p1<=0.100000, 0.700000<=p2<=0.750000; -0.050000<=p1<=0.100000, 0.750000<=p2<=0.800000; -0.050000<=p1<=0.100000, 0.800000<=p2<=0.850000; -0.050000<=p1<=0.100000, 0.850000<=p2<=0.900000; -0.050000<=p1<=0.100000, 0.900000<=p2<=0.950000; -0.050000<=p1<=0.100000, 0.950000<=p2<=0.999990; -0.100000<=p1<=0.150000, 0.000010<=p2<=0.050000; -0.100000<=p1<=0.150000, 0.050000<=p2<=0.100000; -0.100000<=p1<=0.150000, 0.100000<=p2<=0.150000; -0.100000<=p1<=0.150000, 0.150000<=p2<=0.200000; -0.100000<=p1<=0.150000, 0.200000<=p2<=0.250000; -0.100000<=p1<=0.150000, 0.250000<=p2<=0.300000; -0.100000<=p1<=0.150000, 0.300000<=p2<=0.350000; -0.100000<=p1<=0.150000, 0.350000<=p2<=0.400000; -0.100000<=p1<=0.150000, 0.400000<=p2<=0.450000; -0.100000<=p1<=0.150000, 0.450000<=p2<=0.500000; -0.100000<=p1<=0.150000, 0.500000<=p2<=0.550000; -0.100000<=p1<=0.150000, 0.550000<=p2<=0.600000; -0.100000<=p1<=0.150000, 0.600000<=p2<=0.650000; -0.100000<=p1<=0.150000, 0.650000<=p2<=0.700000; -0.100000<=p1<=0.150000, 0.700000<=p2<=0.750000; -0.100000<=p1<=0.150000, 0.750000<=p2<=0.800000; -0.100000<=p1<=0.150000, 0.800000<=p2<=0.850000; -0.100000<=p1<=0.150000, 0.850000<=p2<=0.900000; -0.100000<=p1<=0.150000, 0.900000<=p2<=0.950000; -0.100000<=p1<=0.150000, 0.950000<=p2<=0.999990; -0.150000<=p1<=0.200000, 0.000010<=p2<=0.050000; -0.150000<=p1<=0.200000, 0.050000<=p2<=0.100000; -0.150000<=p1<=0.200000, 0.100000<=p2<=0.150000; -0.150000<=p1<=0.200000, 0.150000<=p2<=0.200000; -0.150000<=p1<=0.200000, 0.200000<=p2<=0.250000; -0.150000<=p1<=0.200000, 0.250000<=p2<=0.300000; -0.150000<=p1<=0.200000, 0.300000<=p2<=0.350000; -0.150000<=p1<=0.200000, 0.350000<=p2<=0.400000; -0.150000<=p1<=0.200000, 0.400000<=p2<=0.450000; -0.150000<=p1<=0.200000, 0.450000<=p2<=0.500000; -0.150000<=p1<=0.200000, 0.500000<=p2<=0.550000; -0.150000<=p1<=0.200000, 0.550000<=p2<=0.600000; -0.150000<=p1<=0.200000, 0.600000<=p2<=0.650000; -0.150000<=p1<=0.200000, 0.650000<=p2<=0.700000; -0.150000<=p1<=0.200000, 0.700000<=p2<=0.750000; -0.150000<=p1<=0.200000, 0.750000<=p2<=0.800000; -0.150000<=p1<=0.200000, 0.800000<=p2<=0.850000; -0.150000<=p1<=0.200000, 0.850000<=p2<=0.900000; -0.150000<=p1<=0.200000, 0.900000<=p2<=0.950000; -0.150000<=p1<=0.200000, 0.950000<=p2<=0.999990; -0.200000<=p1<=0.250000, 0.000010<=p2<=0.050000; -0.200000<=p1<=0.250000, 0.050000<=p2<=0.100000; -0.200000<=p1<=0.250000, 0.100000<=p2<=0.150000; -0.200000<=p1<=0.250000, 0.150000<=p2<=0.200000; -0.200000<=p1<=0.250000, 0.200000<=p2<=0.250000; -0.200000<=p1<=0.250000, 0.250000<=p2<=0.300000; -0.200000<=p1<=0.250000, 0.300000<=p2<=0.350000; -0.200000<=p1<=0.250000, 0.350000<=p2<=0.400000; -0.200000<=p1<=0.250000, 0.400000<=p2<=0.450000; -0.200000<=p1<=0.250000, 0.450000<=p2<=0.500000; -0.200000<=p1<=0.250000, 0.500000<=p2<=0.550000; -0.200000<=p1<=0.250000, 0.550000<=p2<=0.600000; -0.200000<=p1<=0.250000, 0.600000<=p2<=0.650000; -0.200000<=p1<=0.250000, 0.650000<=p2<=0.700000; -0.200000<=p1<=0.250000, 0.700000<=p2<=0.750000; -0.200000<=p1<=0.250000, 0.750000<=p2<=0.800000; -0.200000<=p1<=0.250000, 0.800000<=p2<=0.850000; -0.200000<=p1<=0.250000, 0.850000<=p2<=0.900000; -0.200000<=p1<=0.250000, 0.900000<=p2<=0.950000; -0.200000<=p1<=0.250000, 0.950000<=p2<=0.999990; -0.250000<=p1<=0.300000, 0.000010<=p2<=0.050000; -0.250000<=p1<=0.300000, 0.050000<=p2<=0.100000; -0.250000<=p1<=0.300000, 0.100000<=p2<=0.150000; -0.250000<=p1<=0.300000, 0.150000<=p2<=0.200000; -0.250000<=p1<=0.300000, 0.200000<=p2<=0.250000; -0.250000<=p1<=0.300000, 0.250000<=p2<=0.300000; -0.250000<=p1<=0.300000, 0.300000<=p2<=0.350000; -0.250000<=p1<=0.300000, 0.350000<=p2<=0.400000; -0.250000<=p1<=0.300000, 0.400000<=p2<=0.450000; -0.250000<=p1<=0.300000, 0.450000<=p2<=0.500000; -0.250000<=p1<=0.300000, 0.500000<=p2<=0.550000; -0.250000<=p1<=0.300000, 0.550000<=p2<=0.600000; -0.250000<=p1<=0.300000, 0.600000<=p2<=0.650000; -0.250000<=p1<=0.300000, 0.650000<=p2<=0.700000; -0.250000<=p1<=0.300000, 0.700000<=p2<=0.750000; -0.250000<=p1<=0.300000, 0.750000<=p2<=0.800000; -0.250000<=p1<=0.300000, 0.800000<=p2<=0.850000; -0.250000<=p1<=0.300000, 0.850000<=p2<=0.900000; -0.250000<=p1<=0.300000, 0.900000<=p2<=0.950000; -0.250000<=p1<=0.300000, 0.950000<=p2<=0.999990; -0.300000<=p1<=0.350000, 0.000010<=p2<=0.050000; -0.300000<=p1<=0.350000, 0.050000<=p2<=0.100000; -0.300000<=p1<=0.350000, 0.100000<=p2<=0.150000; -0.300000<=p1<=0.350000, 0.150000<=p2<=0.200000; -0.300000<=p1<=0.350000, 0.200000<=p2<=0.250000; -0.300000<=p1<=0.350000, 0.250000<=p2<=0.300000; -0.300000<=p1<=0.350000, 0.300000<=p2<=0.350000; -0.300000<=p1<=0.350000, 0.350000<=p2<=0.400000; -0.300000<=p1<=0.350000, 0.400000<=p2<=0.450000; -0.300000<=p1<=0.350000, 0.450000<=p2<=0.500000; -0.300000<=p1<=0.350000, 0.500000<=p2<=0.550000; -0.300000<=p1<=0.350000, 0.550000<=p2<=0.600000; -0.300000<=p1<=0.350000, 0.600000<=p2<=0.650000; -0.300000<=p1<=0.350000, 0.650000<=p2<=0.700000; -0.300000<=p1<=0.350000, 0.700000<=p2<=0.750000; -0.300000<=p1<=0.350000, 0.750000<=p2<=0.800000; -0.300000<=p1<=0.350000, 0.800000<=p2<=0.850000; -0.300000<=p1<=0.350000, 0.850000<=p2<=0.900000; -0.300000<=p1<=0.350000, 0.900000<=p2<=0.950000; -0.300000<=p1<=0.350000, 0.950000<=p2<=0.999990; -0.350000<=p1<=0.400000, 0.000010<=p2<=0.050000; -0.350000<=p1<=0.400000, 0.050000<=p2<=0.100000; -0.350000<=p1<=0.400000, 0.100000<=p2<=0.150000; -0.350000<=p1<=0.400000, 0.150000<=p2<=0.200000; -0.350000<=p1<=0.400000, 0.200000<=p2<=0.250000; -0.350000<=p1<=0.400000, 0.250000<=p2<=0.300000; -0.350000<=p1<=0.400000, 0.300000<=p2<=0.350000; -0.350000<=p1<=0.400000, 0.350000<=p2<=0.400000; -0.350000<=p1<=0.400000, 0.400000<=p2<=0.450000; -0.350000<=p1<=0.400000, 0.450000<=p2<=0.500000; -0.350000<=p1<=0.400000, 0.500000<=p2<=0.550000; -0.350000<=p1<=0.400000, 0.550000<=p2<=0.600000; -0.350000<=p1<=0.400000, 0.600000<=p2<=0.650000; -0.350000<=p1<=0.400000, 0.650000<=p2<=0.700000; -0.350000<=p1<=0.400000, 0.700000<=p2<=0.750000; -0.350000<=p1<=0.400000, 0.750000<=p2<=0.800000; -0.350000<=p1<=0.400000, 0.800000<=p2<=0.850000; -0.350000<=p1<=0.400000, 0.850000<=p2<=0.900000; -0.350000<=p1<=0.400000, 0.900000<=p2<=0.950000; -0.350000<=p1<=0.400000, 0.950000<=p2<=0.999990; -0.400000<=p1<=0.450000, 0.000010<=p2<=0.050000; -0.400000<=p1<=0.450000, 0.050000<=p2<=0.100000; -0.400000<=p1<=0.450000, 0.100000<=p2<=0.150000; -0.400000<=p1<=0.450000, 0.150000<=p2<=0.200000; -0.400000<=p1<=0.450000, 0.200000<=p2<=0.250000; -0.400000<=p1<=0.450000, 0.250000<=p2<=0.300000; -0.400000<=p1<=0.450000, 0.300000<=p2<=0.350000; -0.400000<=p1<=0.450000, 0.350000<=p2<=0.400000; -0.400000<=p1<=0.450000, 0.400000<=p2<=0.450000; -0.400000<=p1<=0.450000, 0.450000<=p2<=0.500000; -0.400000<=p1<=0.450000, 0.500000<=p2<=0.550000; -0.400000<=p1<=0.450000, 0.550000<=p2<=0.600000; -0.400000<=p1<=0.450000, 0.600000<=p2<=0.650000; -0.400000<=p1<=0.450000, 0.650000<=p2<=0.700000; -0.400000<=p1<=0.450000, 0.700000<=p2<=0.750000; -0.400000<=p1<=0.450000, 0.750000<=p2<=0.800000; -0.400000<=p1<=0.450000, 0.800000<=p2<=0.850000; -0.400000<=p1<=0.450000, 0.850000<=p2<=0.900000; -0.400000<=p1<=0.450000, 0.900000<=p2<=0.950000; -0.400000<=p1<=0.450000, 0.950000<=p2<=0.999990; -0.450000<=p1<=0.500000, 0.000010<=p2<=0.050000; -0.450000<=p1<=0.500000, 0.050000<=p2<=0.100000; -0.450000<=p1<=0.500000, 0.100000<=p2<=0.150000; -0.450000<=p1<=0.500000, 0.150000<=p2<=0.200000; -0.450000<=p1<=0.500000, 0.200000<=p2<=0.250000; -0.450000<=p1<=0.500000, 0.250000<=p2<=0.300000; -0.450000<=p1<=0.500000, 0.300000<=p2<=0.350000; -0.450000<=p1<=0.500000, 0.350000<=p2<=0.400000; -0.450000<=p1<=0.500000, 0.400000<=p2<=0.450000; -0.450000<=p1<=0.500000, 0.450000<=p2<=0.500000; -0.450000<=p1<=0.500000, 0.500000<=p2<=0.550000; -0.450000<=p1<=0.500000, 0.550000<=p2<=0.600000; -0.450000<=p1<=0.500000, 0.600000<=p2<=0.650000; -0.450000<=p1<=0.500000, 0.650000<=p2<=0.700000; -0.450000<=p1<=0.500000, 0.700000<=p2<=0.750000; -0.450000<=p1<=0.500000, 0.750000<=p2<=0.800000; -0.450000<=p1<=0.500000, 0.800000<=p2<=0.850000; -0.450000<=p1<=0.500000, 0.850000<=p2<=0.900000; -0.450000<=p1<=0.500000, 0.900000<=p2<=0.950000; -0.450000<=p1<=0.500000, 0.950000<=p2<=0.999990; -0.500000<=p1<=0.550000, 0.000010<=p2<=0.050000; -0.500000<=p1<=0.550000, 0.050000<=p2<=0.100000; -0.500000<=p1<=0.550000, 0.100000<=p2<=0.150000; -0.500000<=p1<=0.550000, 0.150000<=p2<=0.200000; -0.500000<=p1<=0.550000, 0.200000<=p2<=0.250000; -0.500000<=p1<=0.550000, 0.250000<=p2<=0.300000; -0.500000<=p1<=0.550000, 0.300000<=p2<=0.350000; -0.500000<=p1<=0.550000, 0.350000<=p2<=0.400000; -0.500000<=p1<=0.550000, 0.400000<=p2<=0.450000; -0.500000<=p1<=0.550000, 0.450000<=p2<=0.500000; -0.500000<=p1<=0.550000, 0.500000<=p2<=0.550000; -0.500000<=p1<=0.550000, 0.550000<=p2<=0.600000; -0.500000<=p1<=0.550000, 0.600000<=p2<=0.650000; -0.500000<=p1<=0.550000, 0.650000<=p2<=0.700000; -0.500000<=p1<=0.550000, 0.700000<=p2<=0.750000; -0.500000<=p1<=0.550000, 0.750000<=p2<=0.800000; -0.500000<=p1<=0.550000, 0.800000<=p2<=0.850000; -0.500000<=p1<=0.550000, 0.850000<=p2<=0.900000; -0.500000<=p1<=0.550000, 0.900000<=p2<=0.950000; -0.500000<=p1<=0.550000, 0.950000<=p2<=0.999990; -0.550000<=p1<=0.600000, 0.000010<=p2<=0.050000; -0.550000<=p1<=0.600000, 0.050000<=p2<=0.100000; -0.550000<=p1<=0.600000, 0.100000<=p2<=0.150000; -0.550000<=p1<=0.600000, 0.150000<=p2<=0.200000; -0.550000<=p1<=0.600000, 0.200000<=p2<=0.250000; -0.550000<=p1<=0.600000, 0.250000<=p2<=0.300000; -0.550000<=p1<=0.600000, 0.300000<=p2<=0.350000; -0.550000<=p1<=0.600000, 0.350000<=p2<=0.400000; -0.550000<=p1<=0.600000, 0.400000<=p2<=0.450000; -0.550000<=p1<=0.600000, 0.450000<=p2<=0.500000; -0.550000<=p1<=0.600000, 0.500000<=p2<=0.550000; -0.550000<=p1<=0.600000, 0.550000<=p2<=0.600000; -0.550000<=p1<=0.600000, 0.600000<=p2<=0.650000; -0.550000<=p1<=0.600000, 0.650000<=p2<=0.700000; -0.550000<=p1<=0.600000, 0.700000<=p2<=0.750000; -0.550000<=p1<=0.600000, 0.750000<=p2<=0.800000; -0.550000<=p1<=0.600000, 0.800000<=p2<=0.850000; -0.550000<=p1<=0.600000, 0.850000<=p2<=0.900000; -0.550000<=p1<=0.600000, 0.900000<=p2<=0.950000; -0.550000<=p1<=0.600000, 0.950000<=p2<=0.999990; -0.600000<=p1<=0.650000, 0.000010<=p2<=0.050000; -0.600000<=p1<=0.650000, 0.050000<=p2<=0.100000; -0.600000<=p1<=0.650000, 0.100000<=p2<=0.150000; -0.600000<=p1<=0.650000, 0.150000<=p2<=0.200000; -0.600000<=p1<=0.650000, 0.200000<=p2<=0.250000; -0.600000<=p1<=0.650000, 0.250000<=p2<=0.300000; -0.600000<=p1<=0.650000, 0.300000<=p2<=0.350000; -0.600000<=p1<=0.650000, 0.350000<=p2<=0.400000; -0.600000<=p1<=0.650000, 0.400000<=p2<=0.450000; -0.600000<=p1<=0.650000, 0.450000<=p2<=0.500000; -0.600000<=p1<=0.650000, 0.500000<=p2<=0.550000; -0.600000<=p1<=0.650000, 0.550000<=p2<=0.600000; -0.600000<=p1<=0.650000, 0.600000<=p2<=0.650000; -0.600000<=p1<=0.650000, 0.650000<=p2<=0.700000; -0.600000<=p1<=0.650000, 0.700000<=p2<=0.750000; -0.600000<=p1<=0.650000, 0.750000<=p2<=0.800000; -0.600000<=p1<=0.650000, 0.800000<=p2<=0.850000; -0.600000<=p1<=0.650000, 0.850000<=p2<=0.900000; -0.600000<=p1<=0.650000, 0.900000<=p2<=0.950000; -0.600000<=p1<=0.650000, 0.950000<=p2<=0.999990; -0.650000<=p1<=0.700000, 0.000010<=p2<=0.050000; -0.650000<=p1<=0.700000, 0.050000<=p2<=0.100000; -0.650000<=p1<=0.700000, 0.100000<=p2<=0.150000; -0.650000<=p1<=0.700000, 0.150000<=p2<=0.200000; -0.650000<=p1<=0.700000, 0.200000<=p2<=0.250000; -0.650000<=p1<=0.700000, 0.250000<=p2<=0.300000; -0.650000<=p1<=0.700000, 0.300000<=p2<=0.350000; -0.650000<=p1<=0.700000, 0.350000<=p2<=0.400000; -0.650000<=p1<=0.700000, 0.400000<=p2<=0.450000; -0.650000<=p1<=0.700000, 0.450000<=p2<=0.500000; -0.650000<=p1<=0.700000, 0.500000<=p2<=0.550000; -0.650000<=p1<=0.700000, 0.550000<=p2<=0.600000; -0.650000<=p1<=0.700000, 0.600000<=p2<=0.650000; -0.650000<=p1<=0.700000, 0.650000<=p2<=0.700000; -0.650000<=p1<=0.700000, 0.700000<=p2<=0.750000; -0.650000<=p1<=0.700000, 0.750000<=p2<=0.800000; -0.650000<=p1<=0.700000, 0.800000<=p2<=0.850000; -0.650000<=p1<=0.700000, 0.850000<=p2<=0.900000; -0.650000<=p1<=0.700000, 0.900000<=p2<=0.950000; -0.650000<=p1<=0.700000, 0.950000<=p2<=0.999990; -0.700000<=p1<=0.750000, 0.000010<=p2<=0.050000; -0.700000<=p1<=0.750000, 0.050000<=p2<=0.100000; -0.700000<=p1<=0.750000, 0.100000<=p2<=0.150000; -0.700000<=p1<=0.750000, 0.150000<=p2<=0.200000; -0.700000<=p1<=0.750000, 0.200000<=p2<=0.250000; -0.700000<=p1<=0.750000, 0.250000<=p2<=0.300000; -0.700000<=p1<=0.750000, 0.300000<=p2<=0.350000; -0.700000<=p1<=0.750000, 0.350000<=p2<=0.400000; -0.700000<=p1<=0.750000, 0.400000<=p2<=0.450000; -0.700000<=p1<=0.750000, 0.450000<=p2<=0.500000; -0.700000<=p1<=0.750000, 0.500000<=p2<=0.550000; -0.700000<=p1<=0.750000, 0.550000<=p2<=0.600000; -0.700000<=p1<=0.750000, 0.600000<=p2<=0.650000; -0.700000<=p1<=0.750000, 0.650000<=p2<=0.700000; -0.700000<=p1<=0.750000, 0.700000<=p2<=0.750000; -0.700000<=p1<=0.750000, 0.750000<=p2<=0.800000; -0.700000<=p1<=0.750000, 0.800000<=p2<=0.850000; -0.700000<=p1<=0.750000, 0.850000<=p2<=0.900000; -0.700000<=p1<=0.750000, 0.900000<=p2<=0.950000; -0.700000<=p1<=0.750000, 0.950000<=p2<=0.999990; -0.750000<=p1<=0.800000, 0.000010<=p2<=0.050000; -0.750000<=p1<=0.800000, 0.050000<=p2<=0.100000; -0.750000<=p1<=0.800000, 0.100000<=p2<=0.150000; -0.750000<=p1<=0.800000, 0.150000<=p2<=0.200000; -0.750000<=p1<=0.800000, 0.200000<=p2<=0.250000; -0.750000<=p1<=0.800000, 0.250000<=p2<=0.300000; -0.750000<=p1<=0.800000, 0.300000<=p2<=0.350000; -0.750000<=p1<=0.800000, 0.350000<=p2<=0.400000; -0.750000<=p1<=0.800000, 0.400000<=p2<=0.450000; -0.750000<=p1<=0.800000, 0.450000<=p2<=0.500000; -0.750000<=p1<=0.800000, 0.500000<=p2<=0.550000; -0.750000<=p1<=0.800000, 0.550000<=p2<=0.600000; -0.750000<=p1<=0.800000, 0.600000<=p2<=0.650000; -0.750000<=p1<=0.800000, 0.650000<=p2<=0.700000; -0.750000<=p1<=0.800000, 0.700000<=p2<=0.750000; -0.750000<=p1<=0.800000, 0.750000<=p2<=0.800000; -0.750000<=p1<=0.800000, 0.800000<=p2<=0.850000; -0.750000<=p1<=0.800000, 0.850000<=p2<=0.900000; -0.750000<=p1<=0.800000, 0.900000<=p2<=0.950000; -0.750000<=p1<=0.800000, 0.950000<=p2<=0.999990; -0.800000<=p1<=0.850000, 0.000010<=p2<=0.050000; -0.800000<=p1<=0.850000, 0.050000<=p2<=0.100000; -0.800000<=p1<=0.850000, 0.100000<=p2<=0.150000; -0.800000<=p1<=0.850000, 0.150000<=p2<=0.200000; -0.800000<=p1<=0.850000, 0.200000<=p2<=0.250000; -0.800000<=p1<=0.850000, 0.250000<=p2<=0.300000; -0.800000<=p1<=0.850000, 0.300000<=p2<=0.350000; -0.800000<=p1<=0.850000, 0.350000<=p2<=0.400000; -0.800000<=p1<=0.850000, 0.400000<=p2<=0.450000; -0.800000<=p1<=0.850000, 0.450000<=p2<=0.500000; -0.800000<=p1<=0.850000, 0.500000<=p2<=0.550000; -0.800000<=p1<=0.850000, 0.550000<=p2<=0.600000; -0.800000<=p1<=0.850000, 0.600000<=p2<=0.650000; -0.800000<=p1<=0.850000, 0.650000<=p2<=0.700000; -0.800000<=p1<=0.850000, 0.700000<=p2<=0.750000; -0.800000<=p1<=0.850000, 0.750000<=p2<=0.800000; -0.800000<=p1<=0.850000, 0.800000<=p2<=0.850000; -0.800000<=p1<=0.850000, 0.850000<=p2<=0.900000; -0.800000<=p1<=0.850000, 0.900000<=p2<=0.950000; -0.800000<=p1<=0.850000, 0.950000<=p2<=0.999990; -0.850000<=p1<=0.900000, 0.000010<=p2<=0.050000; -0.850000<=p1<=0.900000, 0.050000<=p2<=0.100000; -0.850000<=p1<=0.900000, 0.100000<=p2<=0.150000; -0.850000<=p1<=0.900000, 0.150000<=p2<=0.200000; -0.850000<=p1<=0.900000, 0.200000<=p2<=0.250000; -0.850000<=p1<=0.900000, 0.250000<=p2<=0.300000; -0.850000<=p1<=0.900000, 0.300000<=p2<=0.350000; -0.850000<=p1<=0.900000, 0.350000<=p2<=0.400000; -0.850000<=p1<=0.900000, 0.400000<=p2<=0.450000; -0.850000<=p1<=0.900000, 0.450000<=p2<=0.500000; -0.850000<=p1<=0.900000, 0.500000<=p2<=0.550000; -0.850000<=p1<=0.900000, 0.550000<=p2<=0.600000; -0.850000<=p1<=0.900000, 0.600000<=p2<=0.650000; -0.850000<=p1<=0.900000, 0.650000<=p2<=0.700000; -0.850000<=p1<=0.900000, 0.700000<=p2<=0.750000; -0.850000<=p1<=0.900000, 0.750000<=p2<=0.800000; -0.850000<=p1<=0.900000, 0.800000<=p2<=0.850000; -0.850000<=p1<=0.900000, 0.850000<=p2<=0.900000; -0.850000<=p1<=0.900000, 0.900000<=p2<=0.950000; -0.850000<=p1<=0.900000, 0.950000<=p2<=0.999990; -0.900000<=p1<=0.950000, 0.000010<=p2<=0.050000; -0.900000<=p1<=0.950000, 0.050000<=p2<=0.100000; -0.900000<=p1<=0.950000, 0.100000<=p2<=0.150000; -0.900000<=p1<=0.950000, 0.150000<=p2<=0.200000; -0.900000<=p1<=0.950000, 0.200000<=p2<=0.250000; -0.900000<=p1<=0.950000, 0.250000<=p2<=0.300000; -0.900000<=p1<=0.950000, 0.300000<=p2<=0.350000; -0.900000<=p1<=0.950000, 0.350000<=p2<=0.400000; -0.900000<=p1<=0.950000, 0.400000<=p2<=0.450000; -0.900000<=p1<=0.950000, 0.450000<=p2<=0.500000; -0.900000<=p1<=0.950000, 0.500000<=p2<=0.550000; -0.900000<=p1<=0.950000, 0.550000<=p2<=0.600000; -0.900000<=p1<=0.950000, 0.600000<=p2<=0.650000; -0.900000<=p1<=0.950000, 0.650000<=p2<=0.700000; -0.900000<=p1<=0.950000, 0.700000<=p2<=0.750000; -0.900000<=p1<=0.950000, 0.750000<=p2<=0.800000; -0.900000<=p1<=0.950000, 0.800000<=p2<=0.850000; -0.900000<=p1<=0.950000, 0.850000<=p2<=0.900000; -0.900000<=p1<=0.950000, 0.900000<=p2<=0.950000; -0.900000<=p1<=0.950000, 0.950000<=p2<=0.999990; -0.950000<=p1<=0.999990, 0.000010<=p2<=0.050000; -0.950000<=p1<=0.999990, 0.050000<=p2<=0.100000; -0.950000<=p1<=0.999990, 0.100000<=p2<=0.150000; -0.950000<=p1<=0.999990, 0.150000<=p2<=0.200000; -0.950000<=p1<=0.999990, 0.200000<=p2<=0.250000; -0.950000<=p1<=0.999990, 0.250000<=p2<=0.300000; -0.950000<=p1<=0.999990, 0.300000<=p2<=0.350000; -0.950000<=p1<=0.999990, 0.350000<=p2<=0.400000; -0.950000<=p1<=0.999990, 0.400000<=p2<=0.450000; -0.950000<=p1<=0.999990, 0.450000<=p2<=0.500000; -0.950000<=p1<=0.999990, 0.500000<=p2<=0.550000; -0.950000<=p1<=0.999990, 0.550000<=p2<=0.600000; -0.950000<=p1<=0.999990, 0.600000<=p2<=0.650000; -0.950000<=p1<=0.999990, 0.650000<=p2<=0.700000; -0.950000<=p1<=0.999990, 0.700000<=p2<=0.750000; -0.950000<=p1<=0.999990, 0.750000<=p2<=0.800000; -0.950000<=p1<=0.999990, 0.800000<=p2<=0.850000; -0.950000<=p1<=0.999990, 0.850000<=p2<=0.900000; -0.950000<=p1<=0.999990, 0.900000<=p2<=0.950000; -0.950000<=p1<=0.999990, 0.950000<=p2<=0.999990; diff --git a/examples/pmdp/two_dice/two_dice.prctl b/examples/pmdp/two_dice/two_dice.prctl index cde083400..3368d9651 100644 --- a/examples/pmdp/two_dice/two_dice.prctl +++ b/examples/pmdp/two_dice/two_dice.prctl @@ -1,4 +1,4 @@ -P<0.15 [ F "doubles" ] +P<=0.17 [ F "doubles" ] diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index c42743f8d..1d5356e67 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -27,32 +27,22 @@ namespace storm { inline void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas) { if (storm::settings::generalSettings().isParametricRegionSet()){ auto regions=storm::modelchecker::region::ParameterRegion::getRegionsFromSettings(); - if(model->getType() == storm::models::ModelType::Dtmc){ - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " for all parameters in the given regions." << 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); - modelchecker.printStatisticsToStream(std::cout); - } - } else if (model->getType() == storm::models::ModelType::Mdp){ - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::region::SparseMdpRegionModelChecker, double> modelchecker(*mdp); - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " for all parameters in the given regions." << 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); - modelchecker.printStatisticsToStream(std::cout); - } + std::shared_ptr, double>> modelchecker; + if(model->isOfType(storm::models::ModelType::Dtmc)){ + modelchecker = std::make_shared, double>>(model); + } else if (model->isOfType(storm::models::ModelType::Mdp)){ + modelchecker = std::make_shared, double>>(model); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Currently parametric region verification is only available for DTMCs and Mdps."); } - // for(auto const& reg : regions){ - // std::cout << reg.toString() << " Result: " << reg.getCheckResult() << std::endl; - // } + for (auto const& formula : formulas) { + std::cout << std::endl << "Model checking property: " << *formula << " for all parameters in the given regions." << 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); + modelchecker->printStatisticsToStream(std::cout); + std::cout << std::endl; + } } else { for (auto const& formula : formulas) { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs."); diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp index 4fa049b91..66ecc60f8 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp @@ -33,10 +33,10 @@ namespace storm { namespace region { template - AbstractSparseRegionModelChecker::AbstractSparseRegionModelChecker(ParametricSparseModelType const& model) : + AbstractSparseRegionModelChecker::AbstractSparseRegionModelChecker(std::shared_ptr model) : model(model), specifiedFormula(nullptr){ - STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Model is required to have exactly one initial state."); + STORM_LOG_THROW(model->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Model is required to have exactly one initial state."); } template @@ -45,13 +45,13 @@ namespace storm { } template - ParametricSparseModelType const& AbstractSparseRegionModelChecker::getModel() const { + std::shared_ptr const& AbstractSparseRegionModelChecker::getModel() const { return this->model; } template std::shared_ptr const& AbstractSparseRegionModelChecker::getSpecifiedFormula() const { - return specifiedFormula; + return this->specifiedFormula; } template @@ -60,8 +60,8 @@ namespace storm { } template - bool AbstractSparseRegionModelChecker::specifiedFormulaHasUpperBound() const { - return !storm::logic::isLowerBound(this->getSpecifiedFormula()->getComparisonType()); + bool AbstractSparseRegionModelChecker::specifiedFormulaHasLowerBound() const { + return storm::logic::isLowerBound(this->getSpecifiedFormula()->getComparisonType()); } template @@ -308,9 +308,7 @@ namespace storm { proveAllSat=true; } - bool computeLowerBounds = (!this->specifiedFormulaHasUpperBound() && proveAllSat) || (this->specifiedFormulaHasUpperBound() && !proveAllSat); - STORM_LOG_DEBUG("Approximation for " << (computeLowerBounds ? "lower" : "upper") << "bounds"); - bool formulaSatisfied = this->valueIsInBoundOfFormula(this->getApproximationModel()->computeInitialStateValue(region, computeLowerBounds)); + bool formulaSatisfied = this->valueIsInBoundOfFormula(this->getApproximativeReachabilityValue(region, proveAllSat)); //check if approximation was conclusive if(proveAllSat && formulaSatisfied){ @@ -325,8 +323,7 @@ namespace storm { if(region.getCheckResult()==RegionCheckResult::UNKNOWN){ //In this case, it makes sense to try to prove the contrary statement proveAllSat=!proveAllSat; - computeLowerBounds=!computeLowerBounds; - formulaSatisfied = this->valueIsInBoundOfFormula(this->getApproximationModel()->computeInitialStateValue(region, computeLowerBounds)); + formulaSatisfied = this->valueIsInBoundOfFormula(this->getApproximativeReachabilityValue(region, proveAllSat)); //check if approximation was conclusive if(proveAllSat && formulaSatisfied){ @@ -342,6 +339,12 @@ namespace storm { return false; } + template + ConstantType AbstractSparseRegionModelChecker::getApproximativeReachabilityValue(ParameterRegion const& region, bool proveAllSat){ + bool computeLowerBounds = (this->specifiedFormulaHasLowerBound() && proveAllSat) || (!this->specifiedFormulaHasLowerBound() && !proveAllSat); + return this->getApproximationModel()->computeInitialStateValue(region, computeLowerBounds); + } + template std::shared_ptr> const& AbstractSparseRegionModelChecker::getApproximationModel() { if(this->approximationModel==nullptr){ @@ -427,7 +430,7 @@ namespace storm { outstream << std::endl << "Region Model Checker Statistics:" << std::endl; outstream << "-----------------------------------------------" << std::endl; - outstream << "Model: " << this->model.getNumberOfStates() << " states, " << this->model.getNumberOfTransitions() << " transitions." << std::endl; + outstream << "Model: " << this->model->getNumberOfStates() << " states, " << this->model->getNumberOfTransitions() << " transitions." << std::endl; outstream << "Formula: " << *this->getSpecifiedFormula() << std::endl; if(this->isResultConstant()){ outstream << "The requested value is constant (i.e. independent of any parameters)" << std::endl; @@ -468,8 +471,7 @@ namespace storm { //note: for other template instantiations, add rules for the typedefs of VariableType and CoefficientType in utility/regions.h #ifdef STORM_HAVE_CARL - template class AbstractSparseRegionModelChecker>, double>; - template class AbstractSparseRegionModelChecker>, double>; + template class AbstractSparseRegionModelChecker>, double>; #endif } // namespace region } //namespace modelchecker diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.h b/src/modelchecker/region/AbstractSparseRegionModelChecker.h index 4f8ff8864..d4cfedc78 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.h +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.h @@ -33,7 +33,7 @@ namespace storm { typedef typename storm::utility::region::VariableType VariableType; typedef typename storm::utility::region::CoefficientType CoefficientType; - explicit AbstractSparseRegionModelChecker(ParametricSparseModelType const& model); + explicit AbstractSparseRegionModelChecker(std::shared_ptr model); virtual ~AbstractSparseRegionModelChecker(); @@ -66,7 +66,6 @@ namespace storm { /*! * Checks whether the given formula holds for all parameters that lie in the given region. * Sets the region checkresult accordingly. - * TODO: set region.satpoint and violated point correctly. * * @note A formula has to be specified first. * @@ -76,12 +75,21 @@ namespace storm { void checkRegion(ParameterRegion& region); /*! - * Returns the reachability Value at the specified point by instantiating the sampling model. + * Returns the reachability Value at the specified point by instantiating and checking the sampling model. * * @param point The point (i.e. parameter evaluation) at which to compute the reachability value. */ ConstantType getReachabilityValue(std::mapconst& point); + /*! + * Returns the approximative Value for the given region by instantiating and checking the approximation model. + * + * @param region The region for which to compute the approximative value + * @param proveAllSat if set to true, the returned value can be used to prove that the property is SATISFIED for all parameters in the given region. (false for VIOLATED) + * @return a lower or upper bound of the actual reachability value (depending on the given flag 'proveAllSat' and whether the specified formula has a lower or an upper bound) + */ + ConstantType getApproximativeReachabilityValue(ParameterRegion const& region, bool proveAllSat); + /*! * Returns true iff the given value satisfies the bound given by the specified property */ @@ -97,16 +105,23 @@ namespace storm { */ void printStatisticsToStream(std::ostream& outstream); + /*! + * Returns the model that has been specified upon initialization of this + */ + std::shared_ptr const& getModel() const; + + /*! + * Returns the formula that has been specified upon initialization of this + */ + std::shared_ptr const& getSpecifiedFormula() const; protected: /*! * some trivial getters */ - ParametricSparseModelType const& getModel() const; - std::shared_ptr const& getSpecifiedFormula() const; ConstantType getSpecifiedFormulaBound() const; - bool specifiedFormulaHasUpperBound() const; + bool specifiedFormulaHasLowerBound() const; bool const& isComputeRewards() const; bool const isResultConstant() const; std::shared_ptr const& getSimpleModel() const; @@ -189,7 +204,7 @@ namespace storm { void initializeSamplingModel(ParametricSparseModelType const& model, std::shared_ptr formula); // The model this model checker is supposed to analyze. - ParametricSparseModelType const& model; + std::shared_ptr model; //The currently specified formula std::shared_ptr specifiedFormula; //A flag that is true iff we are interested in rewards @@ -227,6 +242,7 @@ namespace storm { protected: std::chrono::high_resolution_clock::duration timeComputeReachabilityFunction; }; + } //namespace region } //namespace modelchecker } //namespace storm diff --git a/src/modelchecker/region/ApproximationModel.cpp b/src/modelchecker/region/ApproximationModel.cpp index db500cec6..5bf1ff8a2 100644 --- a/src/modelchecker/region/ApproximationModel.cpp +++ b/src/modelchecker/region/ApproximationModel.cpp @@ -30,11 +30,13 @@ namespace storm { template ApproximationModel::ApproximationModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula) { //First some simple checks and initializations + this->typeOfParametricModel = parametricModel.getType(); if(formula->isProbabilityOperatorFormula()){ this->computeRewards=false; + STORM_LOG_THROW(this->typeOfParametricModel==storm::models::ModelType::Dtmc || this->typeOfParametricModel==storm::models::ModelType::Mdp, storm::exceptions::InvalidArgumentException, "Approximation with probabilities is only implemented for Dtmcs and Mdps"); } else if(formula->isRewardOperatorFormula()){ this->computeRewards=true; - STORM_LOG_THROW(parametricModel.getType()==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Approximation with rewards is only implemented for Dtmcs"); + STORM_LOG_THROW(this->typeOfParametricModel==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Approximation with rewards is only implemented for Dtmcs"); STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should be unique"); STORM_LOG_THROW(parametricModel.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the approximation model should have state rewards only"); } else { @@ -65,7 +67,7 @@ namespace storm { } this->matrixData.assignment.shrink_to_fit(); this->vectorData.assignment.shrink_to_fit(); - if(parametricModel.getType()==storm::models::ModelType::Mdp){ + if(this->typeOfParametricModel==storm::models::ModelType::Mdp){ initializePlayer1Matrix(parametricModel); this->solverData.lastPlayer1Policy = Policy(this->solverData.player1Matrix.getRowGroupCount(), 0); } @@ -108,7 +110,7 @@ namespace storm { for(uint_fast64_t substitutionId=0ull; substitutionId currSubstitution; std::size_t parameterIndex=0ull; for(auto const& parameter : occurringVariables){ @@ -196,7 +198,6 @@ namespace storm { template void ApproximationModel::initializeRewards(ParametricSparseModelType const& parametricModel, std::vector const& newIndices){ STORM_LOG_DEBUG("Approximation model initialization for Rewards"); - STORM_LOG_THROW(parametricModel.getType()==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Rewards are only supported for DTMCs (yet)"); //Note: Since the original model is assumed to be a DTMC, there is no outgoing transition of a maybeState that leads to an infinity state. //Hence, we do not have to set entries of the eqSys vector to infinity (as it would be required for mdp model checking...) STORM_LOG_THROW(this->vectorData.vector.size()==this->matrixData.matrix.getRowCount(), storm::exceptions::UnexpectedException, "The size of the eq-sys vector does not match to the number of rows in the eq-sys matrix"); @@ -347,10 +348,10 @@ namespace storm { for(std::pair const& sub : this->funcSubData.substitutions[substitutionIndex]){ switch(sub.second){ case RegionBoundary::LOWER: - instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getLowerBound(sub.first))); + instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getLowerBoundary(sub.first))); break; case RegionBoundary::UPPER: - instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getUpperBound(sub.first))); + instantiatedSubs[substitutionIndex].insert(std::make_pair(sub.first, region.getUpperBoundary(sub.first))); break; case RegionBoundary::UNSPECIFIED: //Insert some dummy value @@ -396,37 +397,38 @@ namespace storm { } - template<> - void ApproximationModel, double>::invokeSolver(bool computeLowerBounds, Policy& policy){ - storm::solver::SolveGoal goal(computeLowerBounds); - std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(goal, storm::utility::solver::MinMaxLinearEquationSolverFactory(), this->matrixData.matrix); - storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver, - this->solverData.result, this->vectorData.vector, - goal.direction(), - policy, - this->matrixData.targetChoices, (this->computeRewards ? storm::utility::infinity() : storm::utility::zero())); - } - - template<> - void ApproximationModel, double>::invokeSolver(bool computeLowerBounds, Policy& policy){ + template + void ApproximationModel::invokeSolver(bool computeLowerBounds, Policy& policy){ storm::solver::SolveGoal player2Goal(computeLowerBounds); - std::unique_ptr> solver = storm::utility::solver::GameSolverFactory().create(this->solverData.player1Matrix, this->matrixData.matrix); - storm::utility::policyguessing::solveGame(*solver, - this->solverData.result, this->vectorData.vector, - this->solverData.player1Goal.direction(), player2Goal.direction(), - this->solverData.lastPlayer1Policy, policy, - this->matrixData.targetChoices, (this->computeRewards ? storm::utility::infinity() : storm::utility::zero())); - - // this->solverData.result = std::vector(this->solverData.result.size(), 0.0); - // solver->solveGame(this->solverData.player1Goal.direction(), player2Goal.direction(), this->solverData.result, this->vectorData.vector); + if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){ + //Invoke mdp model checking + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(player2Goal, storm::utility::solver::MinMaxLinearEquationSolverFactory(), this->matrixData.matrix); + storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver, + this->solverData.result, this->vectorData.vector, + player2Goal.direction(), + policy, + this->matrixData.targetChoices, (this->computeRewards ? storm::utility::infinity() : storm::utility::zero()) + ); + } else if(this->typeOfParametricModel == storm::models::ModelType::Mdp){ + //Invoke stochastic two player game model checking + std::unique_ptr> solver = storm::utility::solver::GameSolverFactory().create(this->solverData.player1Matrix, this->matrixData.matrix); + storm::utility::policyguessing::solveGame(*solver, + this->solverData.result, this->vectorData.vector, + this->solverData.player1Goal.direction(), player2Goal.direction(), + this->solverData.lastPlayer1Policy, policy, + this->matrixData.targetChoices, (this->computeRewards ? storm::utility::infinity() : storm::utility::zero()) + ); + // Alternatively(without policy guessing) + // this->solverData.result = std::vector(this->solverData.result.size(), 0.0); + // solver->solveGame(this->solverData.player1Goal.direction(), player2Goal.direction(), this->solverData.result, this->vectorData.vector); + } else { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of model"); + } } - - #ifdef STORM_HAVE_CARL - template class ApproximationModel>, double>; - template class ApproximationModel>, double>; + template class ApproximationModel>, double>; #endif } //namespace region } diff --git a/src/modelchecker/region/ApproximationModel.h b/src/modelchecker/region/ApproximationModel.h index b7af5aed6..492a84fc0 100644 --- a/src/modelchecker/region/ApproximationModel.h +++ b/src/modelchecker/region/ApproximationModel.h @@ -80,6 +80,8 @@ namespace storm { //A flag that denotes whether we compute probabilities or rewards bool computeRewards; + //The model type of the original (parametric) model + storm::models::ModelType typeOfParametricModel; //Some designated states in the original model storm::storage::BitVector targetStates, maybeStates; diff --git a/src/modelchecker/region/ParameterRegion.cpp b/src/modelchecker/region/ParameterRegion.cpp index 0b7a75893..ff55102af 100644 --- a/src/modelchecker/region/ParameterRegion.cpp +++ b/src/modelchecker/region/ParameterRegion.cpp @@ -20,26 +20,26 @@ namespace storm { namespace region { template - ParameterRegion::ParameterRegion(VariableSubstitutionType const& lowerBounds, VariableSubstitutionType const& upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) { + ParameterRegion::ParameterRegion(VariableSubstitutionType const& lowerBoundaries, VariableSubstitutionType const& upperBoundaries) : lowerBoundaries(lowerBoundaries), upperBoundaries(upperBoundaries), checkResult(RegionCheckResult::UNKNOWN) { init(); } template - ParameterRegion::ParameterRegion(VariableSubstitutionType&& lowerBounds, VariableSubstitutionType&& upperBounds) : lowerBounds(std::move(lowerBounds)), upperBounds(std::move(upperBounds)), checkResult(RegionCheckResult::UNKNOWN) { + ParameterRegion::ParameterRegion(VariableSubstitutionType&& lowerBoundaries, VariableSubstitutionType&& upperBoundaries) : lowerBoundaries(std::move(lowerBoundaries)), upperBoundaries(std::move(upperBoundaries)), checkResult(RegionCheckResult::UNKNOWN) { init(); } template void ParameterRegion::init() { - //check whether both mappings map the same variables, check that lowerbound <= upper bound, and pre-compute the set of variables - for (auto const& variableWithLowerBound : this->lowerBounds) { - auto variableWithUpperBound = this->upperBounds.find(variableWithLowerBound.first); - STORM_LOG_THROW((variableWithUpperBound != upperBounds.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No upper bound specified for Variable " << variableWithLowerBound.first); - STORM_LOG_THROW((variableWithLowerBound.second<=variableWithUpperBound->second), storm::exceptions::InvalidArgumentException, "Couldn't create region. The lower bound for " << variableWithLowerBound.first << " is larger then the upper bound"); - this->variables.insert(variableWithLowerBound.first); + //check whether both mappings map the same variables, check that lowerboundary <= upper boundary, and pre-compute the set of variables + for (auto const& variableWithLowerBoundary : this->lowerBoundaries) { + auto variableWithUpperBoundary = this->upperBoundaries.find(variableWithLowerBoundary.first); + STORM_LOG_THROW((variableWithUpperBoundary != upperBoundaries.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No upper boundary specified for Variable " << variableWithLowerBoundary.first); + STORM_LOG_THROW((variableWithLowerBoundary.second<=variableWithUpperBoundary->second), storm::exceptions::InvalidArgumentException, "Couldn't create region. The lower boundary for " << variableWithLowerBoundary.first << " is larger then the upper boundary"); + this->variables.insert(variableWithLowerBoundary.first); } - for (auto const& variableWithBound : this->upperBounds) { - STORM_LOG_THROW((this->variables.find(variableWithBound.first) != this->variables.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No lower bound specified for Variable " << variableWithBound.first); + for (auto const& variableWithBoundary : this->upperBoundaries) { + STORM_LOG_THROW((this->variables.find(variableWithBoundary.first) != this->variables.end()), storm::exceptions::InvalidArgumentException, "Couldn't create region. No lower boundary specified for Variable " << variableWithBoundary.first); } } @@ -54,27 +54,27 @@ namespace storm { } template - typename ParameterRegion::CoefficientType const& ParameterRegion::getLowerBound(VariableType const& variable) const { - auto const& result = lowerBounds.find(variable); - STORM_LOG_THROW(result != lowerBounds.end(), storm::exceptions::InvalidArgumentException, "tried to find a lower bound of a variable that is not specified by this region"); + typename ParameterRegion::CoefficientType const& ParameterRegion::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"); return (*result).second; } template - typename ParameterRegion::CoefficientType const& ParameterRegion::getUpperBound(VariableType const& variable) const { - auto const& result = upperBounds.find(variable); - STORM_LOG_THROW(result != upperBounds.end(), storm::exceptions::InvalidArgumentException, "tried to find an upper bound of a variable that is not specified by this region"); + typename ParameterRegion::CoefficientType const& ParameterRegion::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"); return (*result).second; } template - const typename ParameterRegion::VariableSubstitutionType ParameterRegion::getUpperBounds() const { - return upperBounds; + const typename ParameterRegion::VariableSubstitutionType ParameterRegion::getUpperBoundaries() const { + return upperBoundaries; } template - const typename ParameterRegion::VariableSubstitutionType ParameterRegion::getLowerBounds() const { - return lowerBounds; + const typename ParameterRegion::VariableSubstitutionType ParameterRegion::getLowerBoundaries() const { + return lowerBoundaries; } template @@ -90,13 +90,13 @@ namespace storm { for (uint_fast64_t vertexId = 0; vertexId < numOfVertices; ++vertexId) { //interprete vertexId as a bit sequence //the consideredVariables.size() least significant bits of vertex will always represent the next vertex - //(00...0 = lower bounds for all variables, 11...1 = upper bounds for all variables) + //(00...0 = lower boundaries for all variables, 11...1 = upper boundaries for all variables) std::size_t variableIndex = 0; for (auto const& variable : consideredVariables) { if ((vertexId >> variableIndex) % 2 == 0) { - resultingVector[vertexId].insert(std::pair(variable, getLowerBound(variable))); + resultingVector[vertexId].insert(std::pair(variable, getLowerBoundary(variable))); } else { - resultingVector[vertexId].insert(std::pair(variable, getUpperBound(variable))); + resultingVector[vertexId].insert(std::pair(variable, getUpperBoundary(variable))); } ++variableIndex; } @@ -106,7 +106,7 @@ namespace storm { template typename ParameterRegion::VariableSubstitutionType ParameterRegion::getSomePoint() const { - return this->getLowerBounds(); + return this->getLowerBoundaries(); } template @@ -163,11 +163,11 @@ namespace storm { std::string ParameterRegion::toString() const { std::stringstream regionstringstream; for (auto var : this->getVariables()) { - regionstringstream << storm::utility::region::convertNumber(this->getLowerBound(var)); + regionstringstream << storm::utility::region::convertNumber(this->getLowerBoundary(var)); regionstringstream << "<="; regionstringstream << storm::utility::region::getVariableName(var); regionstringstream << "<="; - regionstringstream << storm::utility::region::convertNumber(this->getUpperBound(var)); + regionstringstream << storm::utility::region::convertNumber(this->getUpperBoundary(var)); regionstringstream << ","; } std::string regionstring = regionstringstream.str(); @@ -179,41 +179,41 @@ namespace storm { template - void ParameterRegion::parseParameterBounds( - VariableSubstitutionType& lowerBounds, - VariableSubstitutionType& upperBounds, - std::string const& parameterBoundsString){ + void ParameterRegion::parseParameterBoundaries( + VariableSubstitutionType& lowerBoundaries, + VariableSubstitutionType& upperBoundaries, + std::string const& parameterBoundariesString){ - std::string::size_type positionOfFirstRelation = parameterBoundsString.find("<="); - STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a '<=' after the first number"); - std::string::size_type positionOfSecondRelation = parameterBoundsString.find("<=", positionOfFirstRelation+2); - STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a '<=' after the parameter"); + std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<="); + STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the first number"); + std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2); + STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the parameter"); - std::string parameter=parameterBoundsString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2)); + std::string parameter=parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2)); //removes all whitespaces from the parameter string: parameter.erase(std::remove_if(parameter.begin(), parameter.end(), ::isspace), parameter.end()); - STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundsString << " I could not find a parameter"); + STORM_LOG_THROW(parameter.length()>0, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a parameter"); VariableType var = storm::utility::region::getVariableFromString(parameter); - CoefficientType lb = storm::utility::region::convertNumber(parameterBoundsString.substr(0,positionOfFirstRelation)); - CoefficientType ub = storm::utility::region::convertNumber(parameterBoundsString.substr(positionOfSecondRelation+2)); - lowerBounds.emplace(std::make_pair(var, lb)); - upperBounds.emplace(std::make_pair(var, ub)); + CoefficientType lb = storm::utility::region::convertNumber(parameterBoundariesString.substr(0,positionOfFirstRelation)); + CoefficientType ub = storm::utility::region::convertNumber(parameterBoundariesString.substr(positionOfSecondRelation+2)); + lowerBoundaries.emplace(std::make_pair(var, lb)); + upperBoundaries.emplace(std::make_pair(var, ub)); } template ParameterRegion ParameterRegion::parseRegion( std::string const& regionString){ - VariableSubstitutionType lowerBounds; - VariableSubstitutionType upperBounds; - std::vector parameterBounds; - boost::split(parameterBounds, regionString, boost::is_any_of(",")); - for(auto const& parameterBound : parameterBounds){ - if(!std::all_of(parameterBound.begin(),parameterBound.end(), ::isspace)){ //skip this string if it only consists of space - parseParameterBounds(lowerBounds, upperBounds, parameterBound); + VariableSubstitutionType lowerBoundaries; + VariableSubstitutionType upperBoundaries; + std::vector parameterBoundaries; + boost::split(parameterBoundaries, regionString, boost::is_any_of(",")); + for(auto const& parameterBoundary : parameterBoundaries){ + if(!std::all_of(parameterBoundary.begin(),parameterBoundary.end(), ::isspace)){ //skip this string if it only consists of space + parseParameterBoundaries(lowerBoundaries, upperBoundaries, parameterBoundary); } } - return ParameterRegion(std::move(lowerBounds), std::move(upperBounds)); + return ParameterRegion(std::move(lowerBoundaries), std::move(upperBoundaries)); } template diff --git a/src/modelchecker/region/ParameterRegion.h b/src/modelchecker/region/ParameterRegion.h index 4b1e3fe4e..e79e29001 100644 --- a/src/modelchecker/region/ParameterRegion.h +++ b/src/modelchecker/region/ParameterRegion.h @@ -30,10 +30,10 @@ namespace storm { virtual ~ParameterRegion(); std::set getVariables() const; - CoefficientType const& getLowerBound(VariableType const& variable) const; - CoefficientType const& getUpperBound(VariableType const& variable) const; - const VariableSubstitutionType getUpperBounds() const; - const VariableSubstitutionType getLowerBounds() const; + CoefficientType const& getLowerBoundary(VariableType const& variable) const; + CoefficientType const& getUpperBoundary(VariableType const& variable) const; + const VariableSubstitutionType getUpperBoundaries() const; + const VariableSubstitutionType getLowerBoundaries() const; /*! * Returns a vector of all possible combinations of lower and upper bounds of the given variables. @@ -89,15 +89,15 @@ namespace storm { std::string toString() const; /* - * Can be used to parse a single parameter with its bounds from a string of the form "0.3<=p<=0.5". + * Can be used to parse a single parameter with its boundaries from a string of the form "0.3<=p<=0.5". * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::CoefficientType. * The results will be inserted in the given maps * */ - static void parseParameterBounds( - VariableSubstitutionType& lowerBounds, - VariableSubstitutionType& upperBounds, - std::string const& parameterBoundsString + static void parseParameterBoundaries( + VariableSubstitutionType& lowerBoundaries, + VariableSubstitutionType& upperBoundaries, + std::string const& parameterBoundariesString ); /* @@ -128,8 +128,8 @@ namespace storm { void init(); - VariableSubstitutionType const lowerBounds; - VariableSubstitutionType const upperBounds; + VariableSubstitutionType const lowerBoundaries; + VariableSubstitutionType const upperBoundaries; std::set variables; RegionCheckResult checkResult; VariableSubstitutionType satPoint; diff --git a/src/modelchecker/region/SamplingModel.cpp b/src/modelchecker/region/SamplingModel.cpp index 5ecc26b91..2c6716609 100644 --- a/src/modelchecker/region/SamplingModel.cpp +++ b/src/modelchecker/region/SamplingModel.cpp @@ -29,11 +29,13 @@ namespace storm { template SamplingModel::SamplingModel(ParametricSparseModelType const& parametricModel, std::shared_ptr formula){ //First some simple checks and initializations.. + this->typeOfParametricModel = parametricModel.getType(); if(formula->isProbabilityOperatorFormula()){ this->computeRewards=false; + STORM_LOG_THROW(this->typeOfParametricModel==storm::models::ModelType::Dtmc || this->typeOfParametricModel==storm::models::ModelType::Mdp, storm::exceptions::InvalidArgumentException, "Sampling with probabilities is only implemented for Dtmcs and Mdps"); } else if(formula->isRewardOperatorFormula()){ this->computeRewards=true; - STORM_LOG_THROW(parametricModel.getType()==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Sampling with rewards is only implemented for Dtmcs"); + STORM_LOG_THROW(this->typeOfParametricModel==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Sampling with rewards is only implemented for Dtmcs"); STORM_LOG_THROW(parametricModel.hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should be unique"); STORM_LOG_THROW(parametricModel.getUniqueRewardModel()->second.hasOnlyStateRewards(), storm::exceptions::InvalidArgumentException, "The rewardmodel of the sampling model should have state rewards only"); } else { @@ -75,7 +77,7 @@ namespace storm { //First run: get a matrix with dummy entries at the new positions ConstantType dummyValue = storm::utility::one(); bool addRowGroups = parametricModel.getTransitionMatrix().hasNontrivialRowGrouping(); - bool isDtmc = (parametricModel.getType()==storm::models::ModelType::Dtmc); //The equation system for DTMCs need the (I-P)-matrix (i.e., we need diagonal entries) + bool isDtmc = (this->typeOfParametricModel==storm::models::ModelType::Dtmc); //The equation system for DTMCs need the (I-P)-matrix (i.e., we need diagonal entries) auto numOfMaybeStates = this->maybeStates.getNumberOfSetBits(); storm::storage::SparseMatrixBuilder matrixBuilder(addRowGroups ? parametricModel.getTransitionMatrix().getRowCount() : numOfMaybeStates, numOfMaybeStates, @@ -188,7 +190,6 @@ namespace storm { template void SamplingModel::initializeRewards(ParametricSparseModelType const& parametricModel, std::vector const& newIndices){ //Run through the state reward vector... Note that this only works for dtmcs - STORM_LOG_THROW(parametricModel.getType()==storm::models::ModelType::Dtmc, storm::exceptions::InvalidArgumentException, "Rewards are only supported for DTMCs (yet)"); STORM_LOG_THROW(this->vectorData.vector.size()==this->matrixData.matrix.getRowCount(), storm::exceptions::UnexpectedException, "The size of the eq-sys vector does not match to the number of rows in the eq-sys matrix"); this->vectorData.assignment.reserve(vectorData.vector.size()); ConstantType dummyValue = storm::utility::one(); @@ -251,26 +252,26 @@ namespace storm { } } - template<> - void SamplingModel, double>::invokeSolver(){ - std::unique_ptr> solver = storm::utility::solver::LinearEquationSolverFactory().create(this->matrixData.matrix); - solver->solveEquationSystem(this->solverData.result, this->vectorData.vector); - } - template<> - void SamplingModel, double>::invokeSolver(){ - std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(this->solverData.solveGoal, storm::utility::solver::MinMaxLinearEquationSolverFactory(), this->matrixData.matrix); - storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver, - this->solverData.result, this->vectorData.vector, - this->solverData.solveGoal.direction(), - this->solverData.lastPolicy, - this->matrixData.targetChoices, (this->computeRewards ? storm::utility::infinity() : storm::utility::zero())); + template + void SamplingModel::invokeSolver(){ + if(this->typeOfParametricModel == storm::models::ModelType::Dtmc){ + std::unique_ptr> solver = storm::utility::solver::LinearEquationSolverFactory().create(this->matrixData.matrix); + solver->solveEquationSystem(this->solverData.result, this->vectorData.vector); + } else if(this->typeOfParametricModel == storm::models::ModelType::Mdp){ + std::unique_ptr> solver = storm::solver::configureMinMaxLinearEquationSolver(this->solverData.solveGoal, storm::utility::solver::MinMaxLinearEquationSolverFactory(), this->matrixData.matrix); + storm::utility::policyguessing::solveMinMaxLinearEquationSystem(*solver, + this->solverData.result, this->vectorData.vector, + this->solverData.solveGoal.direction(), + this->solverData.lastPolicy, + this->matrixData.targetChoices, (this->computeRewards ? storm::utility::infinity() : storm::utility::zero())); + } else { + STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected Type of model"); + } } - #ifdef STORM_HAVE_CARL - template class SamplingModel>, double>; - template class SamplingModel>, double>; + template class SamplingModel>, double>; #endif } //namespace region } diff --git a/src/modelchecker/region/SamplingModel.h b/src/modelchecker/region/SamplingModel.h index 9d0ddb2f3..cb2b15e8c 100644 --- a/src/modelchecker/region/SamplingModel.h +++ b/src/modelchecker/region/SamplingModel.h @@ -61,6 +61,8 @@ namespace storm { //A flag that denotes whether we compute probabilities or rewards bool computeRewards; + //The model type of the original (parametric) model + storm::models::ModelType typeOfParametricModel; //Some designated states in the original model storm::storage::BitVector targetStates, maybeStates; diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index d74a1dbf8..fee98db91 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -35,7 +35,7 @@ namespace storm { namespace region { template - SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(ParametricSparseModelType const& model) : + SparseDtmcRegionModelChecker::SparseDtmcRegionModelChecker(std::shared_ptr model) : AbstractSparseRegionModelChecker(model){ //intentionally left empty } @@ -75,7 +75,7 @@ namespace storm { bool& isApproximationApplicable, boost::optional& constantResult){ STORM_LOG_DEBUG("Preprocessing for DTMC started."); - STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Input model is required to have exactly one initial state."); + STORM_LOG_THROW(this->getModel()->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Input model is required to have exactly one initial state."); //Reset some data this->smtSolver=nullptr; this->reachabilityFunction=nullptr; @@ -96,15 +96,15 @@ namespace storm { } STORM_LOG_DEBUG("Elimination of states with constant outgoing transitions is happening now."); // Determine the set of states that is reachable from the initial state without jumping over a target state. - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, targetStates); + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel()->getTransitionMatrix(), this->getModel()->getInitialStates(), maybeStates, targetStates); // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). maybeStates &= reachableStates; // Create a vector for the probabilities to go to a target state in one step. - std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowSumVector(maybeStates, targetStates); + std::vector oneStepProbabilities = this->getModel()->getTransitionMatrix().getConstrainedRowSumVector(maybeStates, targetStates); // Determine the initial state of the sub-model. - storm::storage::sparse::state_type initialState = *(this->getModel().getInitialStates() % maybeStates).begin(); + storm::storage::sparse::state_type initialState = *(this->getModel()->getInitialStates() % maybeStates).begin(); // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrix = this->getModel()->getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates); // Eliminate all states with only constant outgoing transitions // Convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. storm::storage::FlexibleSparseMatrix flexibleTransitions(submatrix); @@ -224,7 +224,7 @@ namespace storm { } boost::optional>> noChoiceLabeling; // the final model - simpleModel = std::make_shared(matrixBuilder.build(), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling)); + simpleModel = std::make_shared>(matrixBuilder.build(), std::move(labeling), std::move(rewardModels), std::move(noChoiceLabeling)); // the corresponding formula STORM_LOG_DEBUG("Building the resulting simplified formula."); std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); @@ -238,7 +238,7 @@ namespace storm { //Check if the reachability function needs to be computed if((storm::settings::regionSettings().getSmtMode()==storm::settings::modules::RegionSettings::SmtMode::FUNCTION) || (storm::settings::regionSettings().getSampleMode()==storm::settings::modules::RegionSettings::SampleMode::EVALUATE)){ - this->computeReachabilityFunction(*simpleModel); + this->computeReachabilityFunction(*(this->getSimpleModel())->template as>()); } } @@ -249,16 +249,16 @@ namespace storm { boost::optional& constantResult) { STORM_LOG_DEBUG("Preprocessing for Dtmcs and reachability probabilities invoked."); //Get Target States - storm::modelchecker::SparsePropositionalModelChecker modelChecker(this->getModel()); + storm::modelchecker::SparsePropositionalModelChecker modelChecker(*(this->getModel())); std::unique_ptr targetStatesResultPtr = modelChecker.check( this->getSpecifiedFormula()->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula() ); targetStates = std::move(targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector()); //maybeStates: Compute the subset of states that have a probability of 0 or 1, respectively and reduce the considered states accordingly. - std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), storm::storage::BitVector(this->getModel().getNumberOfStates(),true), targetStates); + std::pair statesWithProbability01 = storm::utility::graph::performProb01(this->getModel()->getBackwardTransitions(), storm::storage::BitVector(this->getModel()->getNumberOfStates(),true), targetStates); maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second); // If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction. - storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); + storm::storage::sparse::state_type initialState = *(this->getModel()->getInitialStates().begin()); if (!maybeStates.get(initialState)) { STORM_LOG_WARN("The probability of the initial state is constant (zero or one)"); this->reachabilityFunction = std::make_shared(statesWithProbability01.first.get(initialState) ? storm::utility::zero() : storm::utility::one()); @@ -272,7 +272,7 @@ namespace storm { isApproximationApplicable=true; bool isResultConstant=true; for (auto state=maybeStates.begin(); (state!=maybeStates.end()) && isApproximationApplicable; ++state) { - for(auto const& entry : this->getModel().getTransitionMatrix().getRow(*state)){ + for(auto const& entry : this->getModel()->getTransitionMatrix().getRow(*state)){ if(!storm::utility::isConstant(entry.getValue())){ isResultConstant=false; if(!storm::utility::region::functionIsLinear(entry.getValue())){ @@ -300,26 +300,26 @@ namespace storm { ParametricRewardModelType const* rewardModel; if(this->getSpecifiedFormula()->asRewardOperatorFormula().hasRewardModelName()){ std::string const& rewardModelName = this->getSpecifiedFormula()->asRewardOperatorFormula().getRewardModelName(); - STORM_LOG_THROW(this->getModel().hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException, "The Property specifies refers to the reward model '" << rewardModelName << "which is not defined by the given model"); - rewardModel=&(this->getModel().getRewardModel(rewardModelName)); + STORM_LOG_THROW(this->getModel()->hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException, "The Property specifies refers to the reward model '" << rewardModelName << "which is not defined by the given model"); + rewardModel=&(this->getModel()->getRewardModel(rewardModelName)); } else { - STORM_LOG_THROW(this->getModel().hasRewardModel(), storm::exceptions::InvalidArgumentException, "No reward model specified"); - STORM_LOG_THROW(this->getModel().hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "Ambiguous reward model. Specify it in the formula!"); - rewardModel=&(this->getModel().getUniqueRewardModel()->second); + STORM_LOG_THROW(this->getModel()->hasRewardModel(), storm::exceptions::InvalidArgumentException, "No reward model specified"); + STORM_LOG_THROW(this->getModel()->hasUniqueRewardModel(), storm::exceptions::InvalidArgumentException, "Ambiguous reward model. Specify it in the formula!"); + rewardModel=&(this->getModel()->getUniqueRewardModel()->second); } //Get target states - storm::modelchecker::SparsePropositionalModelChecker modelChecker(this->getModel()); + storm::modelchecker::SparsePropositionalModelChecker modelChecker(*(this->getModel())); std::unique_ptr targetStatesResultPtr = modelChecker.check( this->getSpecifiedFormula()->asRewardOperatorFormula().getSubformula().asReachabilityRewardFormula().getSubformula() ); targetStates = std::move(targetStatesResultPtr->asExplicitQualitativeCheckResult().getTruthValuesVector()); //maybeStates: Compute the subset of states that has a reachability reward less than infinity. - storm::storage::BitVector statesWithProbability1 = storm::utility::graph::performProb1(this->getModel().getBackwardTransitions(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), targetStates); + storm::storage::BitVector statesWithProbability1 = storm::utility::graph::performProb1(this->getModel()->getBackwardTransitions(), storm::storage::BitVector(this->getModel()->getNumberOfStates(), true), targetStates); maybeStates = ~targetStates & statesWithProbability1; //Compute the new state reward vector - stateRewards=rewardModel->getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel().getTransitionMatrix(), maybeStates); + stateRewards=rewardModel->getTotalRewardVector(maybeStates.getNumberOfSetBits(), this->getModel()->getTransitionMatrix(), maybeStates); // If the initial state is known to have 0 reward or an infinite reachability reward value, we can directly set the reachRewardFunction. - storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); + storm::storage::sparse::state_type initialState = *this->getModel()->getInitialStates().begin(); if (!maybeStates.get(initialState)) { STORM_LOG_WARN("The expected reward of the initial state is constant (infinity or zero)"); // Note: storm::utility::infinity does not work at this moment. @@ -336,7 +336,7 @@ namespace storm { std::set probPars; //the set of parameters that occur on a probability function for (auto state=maybeStates.begin(); state!=maybeStates.end() && isApproximationApplicable; ++state) { //Constant/Linear probability functions - for(auto const& entry : this->getModel().getTransitionMatrix().getRow(*state)){ + for(auto const& entry : this->getModel()->getTransitionMatrix().getRow(*state)){ if(!storm::utility::isConstant(entry.getValue())){ isResultConstant=false; if(!storm::utility::region::functionIsLinear(entry.getValue())){ @@ -385,7 +385,7 @@ namespace storm { } template - void SparseDtmcRegionModelChecker::computeReachabilityFunction(ParametricSparseModelType const& simpleModel){ + void SparseDtmcRegionModelChecker::computeReachabilityFunction(storm::models::sparse::Dtmc const& simpleModel){ std::chrono::high_resolution_clock::time_point timeComputeReachabilityFunctionStart = std::chrono::high_resolution_clock::now(); STORM_LOG_DEBUG("Computing the Reachability function..."); //get the one step probabilities and the transition matrix of the simple model without target/sink state @@ -406,7 +406,7 @@ namespace storm { if(this->isComputeRewards()){ stateRewards = simpleModel.getUniqueRewardModel()->second.getTotalRewardVector(maybeStates.getNumberOfSetBits(), simpleModel.getTransitionMatrix(), maybeStates); } - storm::modelchecker::SparseDtmcEliminationModelChecker eliminationModelChecker(simpleModel); + storm::modelchecker::SparseDtmcEliminationModelChecker> eliminationModelChecker(simpleModel); std::vector statePriorities = eliminationModelChecker.getStatePriorities(forwardTransitions,backwardTransitions,newInitialStates,oneStepProbabilities); this->reachabilityFunction=std::make_shared(eliminationModelChecker.computeReachabilityValue(forwardTransitions, oneStepProbabilities, backwardTransitions, newInitialStates , phiStates, simpleModel.getStates("target"), stateRewards, statePriorities)); /* std::string funcStr = " (/ " + @@ -465,7 +465,7 @@ namespace storm { return this->reachabilityFunction; } STORM_LOG_WARN("Reachability Function requested but it has not been computed when specifying the formula. Will compute it now."); - computeReachabilityFunction(*this->getSimpleModel()); + computeReachabilityFunction(*(this->getSimpleModel())->template as>()); } STORM_LOG_THROW((!this->isResultConstant() || storm::utility::isConstant(*this->reachabilityFunction)), storm::exceptions::UnexpectedException, "The result was assumed to be constant but it isn't."); return this->reachabilityFunction; @@ -493,8 +493,8 @@ namespace storm { //add constraints for the region for(auto const& variable : region.getVariables()) { - storm::utility::region::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::GreaterEqual, region.getLowerBound(variable)); - storm::utility::region::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::LessEqual, region.getUpperBound(variable)); + storm::utility::region::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::GreaterEqual, region.getLowerBoundary(variable)); + storm::utility::region::addParameterBoundsToSmtSolver(this->smtSolver, variable, storm::logic::ComparisonType::LessEqual, region.getUpperBoundary(variable)); } //add constraint that states what we want to prove @@ -627,7 +627,7 @@ namespace storm { #ifdef STORM_HAVE_CARL - template class SparseDtmcRegionModelChecker>, double>; + template class SparseDtmcRegionModelChecker>, double>; #endif } // namespace region } // namespace modelchecker diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.h b/src/modelchecker/region/SparseDtmcRegionModelChecker.h index d82df9897..169dd3d41 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.h +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.h @@ -20,7 +20,7 @@ namespace storm { typedef typename storm::utility::region::VariableType VariableType; typedef typename storm::utility::region::CoefficientType CoefficientType; - explicit SparseDtmcRegionModelChecker(ParametricSparseModelType const& model); + explicit SparseDtmcRegionModelChecker(std::shared_ptr model); virtual ~SparseDtmcRegionModelChecker(); @@ -86,7 +86,7 @@ namespace storm { * Computes the reachability function via state elimination * @note computeFlagsAndSimplifiedModel should be called before calling this */ - void computeReachabilityFunction(ParametricSparseModelType const& simpleModel); + void computeReachabilityFunction(storm::models::sparse::Dtmc const& simpleModel); /*! * Checks the value of the function at the given sampling point. diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp index 2219abee2..542c85e4c 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -34,9 +34,9 @@ namespace storm { namespace region { template - SparseMdpRegionModelChecker::SparseMdpRegionModelChecker(ParametricSparseModelType const& model) : + SparseMdpRegionModelChecker::SparseMdpRegionModelChecker(std::shared_ptr model) : AbstractSparseRegionModelChecker(model){ - //intentionally left empty + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidArgumentException, "Tried to create an mdp region model checker for a model that is not an mdp"); } template @@ -74,7 +74,7 @@ namespace storm { bool& isApproximationApplicable, boost::optional& constantResult){ STORM_LOG_DEBUG("Preprocessing for MDPs started."); - STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Input model is required to have exactly one initial state."); + STORM_LOG_THROW(this->getModel()->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::InvalidArgumentException, "Input model is required to have exactly one initial state."); storm::storage::BitVector maybeStates, targetStates; preprocessForProbabilities(maybeStates, targetStates, isApproximationApplicable, constantResult); if(constantResult && constantResult.get()>=storm::utility::zero()){ @@ -83,15 +83,15 @@ namespace storm { } STORM_LOG_DEBUG("Elimination of deterministic states with constant outgoing transitions is happening now."); // Determine the set of states that is reachable from the initial state without jumping over a target state. - storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel().getTransitionMatrix(), this->getModel().getInitialStates(), maybeStates, targetStates); + storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(this->getModel()->getTransitionMatrix(), this->getModel()->getInitialStates(), maybeStates, targetStates); // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state). maybeStates &= reachableStates; // Create a vector for the probabilities to go to a target state in one step. - std::vector oneStepProbabilities = this->getModel().getTransitionMatrix().getConstrainedRowGroupSumVector(maybeStates, targetStates); + std::vector oneStepProbabilities = this->getModel()->getTransitionMatrix().getConstrainedRowGroupSumVector(maybeStates, targetStates); // Determine the initial state of the sub-model. - storm::storage::sparse::state_type initialState = *(this->getModel().getInitialStates() % maybeStates).begin(); + storm::storage::sparse::state_type initialState = *(this->getModel()->getInitialStates() % maybeStates).begin(); // We then build the submatrix that only has the transitions of the maybe states. - storm::storage::SparseMatrix submatrix = this->getModel().getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates); + storm::storage::SparseMatrix submatrix = this->getModel()->getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates); boost::optional> noStateRewards; // Eliminate all deterministic states with only constant outgoing transitions // Convert the reduced matrix to a more flexible format to be able to perform state elimination more easily. @@ -186,7 +186,7 @@ namespace storm { //Other ingredients std::unordered_map noRewardModels; boost::optional>> noChoiceLabeling; - simpleModel = std::make_shared(matrixBuilder.build(), std::move(labeling), std::move(noRewardModels), std::move(noChoiceLabeling)); + simpleModel = std::make_shared>(matrixBuilder.build(), std::move(labeling), std::move(noRewardModels), std::move(noChoiceLabeling)); //Get the simplified formula std::shared_ptr targetFormulaPtr(new storm::logic::AtomicLabelFormula("target")); @@ -201,7 +201,7 @@ namespace storm { boost::optional& constantResult) { STORM_LOG_DEBUG("Preprocessing for Mdps and reachability probabilities invoked."); //Get Target States - storm::modelchecker::SparsePropositionalModelChecker modelChecker(this->getModel()); + storm::modelchecker::SparsePropositionalModelChecker modelChecker(*(this->getModel())); std::unique_ptr targetStatesResultPtr = modelChecker.check( this->getSpecifiedFormula()->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula() ); @@ -209,14 +209,14 @@ namespace storm { //maybeStates: Compute the subset of states that have a probability of 0 or 1, respectively and reduce the considered states accordingly. std::pair statesWithProbability01; - if (this->specifiedFormulaHasUpperBound()){ - statesWithProbability01 = storm::utility::graph::performProb01Max(this->getModel(), storm::storage::BitVector(this->getModel().getNumberOfStates(),true), targetStates); + if (this->specifiedFormulaHasLowerBound()){ + statesWithProbability01 = storm::utility::graph::performProb01Min(this->getModel()->getTransitionMatrix(), this->getModel()->getTransitionMatrix().getRowGroupIndices(), this->getModel()->getBackwardTransitions(), storm::storage::BitVector(this->getModel()->getNumberOfStates(),true), targetStates); } else { - statesWithProbability01 = storm::utility::graph::performProb01Min(this->getModel(), storm::storage::BitVector(this->getModel().getNumberOfStates(),true), targetStates); + statesWithProbability01 = storm::utility::graph::performProb01Max(this->getModel()->getTransitionMatrix(), this->getModel()->getTransitionMatrix().getRowGroupIndices(), this->getModel()->getBackwardTransitions(), storm::storage::BitVector(this->getModel()->getNumberOfStates(),true), targetStates); } maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second); // If the initial state is known to have either probability 0 or 1, we can directly set the reachProbFunction. - storm::storage::sparse::state_type initialState = *this->getModel().getInitialStates().begin(); + storm::storage::sparse::state_type initialState = *(this->getModel()->getInitialStates().begin()); if (!maybeStates.get(initialState)) { STORM_LOG_WARN("The probability of the initial state is constant (zero or one)"); constantResult = statesWithProbability01.first.get(initialState) ? storm::utility::zero() : storm::utility::one(); @@ -229,7 +229,7 @@ namespace storm { isApproximationApplicable=true; bool isResultConstant=true; for (auto state=maybeStates.begin(); (state!=maybeStates.end()) && isApproximationApplicable; ++state) { - for(auto const& entry : this->getModel().getTransitionMatrix().getRowGroup(*state)){ + for(auto const& entry : this->getModel()->getTransitionMatrix().getRowGroup(*state)){ if(!storm::utility::isConstant(entry.getValue())){ isResultConstant=false; if(!storm::utility::region::functionIsLinear(entry.getValue())){ @@ -276,7 +276,7 @@ namespace storm { } #ifdef STORM_HAVE_CARL - template class SparseMdpRegionModelChecker>, double>; + template class SparseMdpRegionModelChecker>, double>; #endif } // namespace region } // namespace modelchecker diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.h b/src/modelchecker/region/SparseMdpRegionModelChecker.h index da5503b49..fca926fa5 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.h +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.h @@ -19,7 +19,7 @@ namespace storm { typedef typename storm::utility::region::VariableType VariableType; typedef typename storm::utility::region::CoefficientType CoefficientType; - explicit SparseMdpRegionModelChecker(ParametricSparseModelType const& model); + explicit SparseMdpRegionModelChecker(std::shared_ptr model); virtual ~SparseMdpRegionModelChecker(); diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 1c3495335..eba059635 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -323,7 +323,7 @@ namespace storm { std::vector Z3SmtSolver::getUnsatAssumptions() { #ifdef STORM_HAVE_Z3 - STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.") + STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable."); STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not involve assumptions."); z3::expr_vector z3UnsatAssumptions = this->solver->unsat_core(); diff --git a/src/utility/region.h b/src/utility/region.h index 6becfb3a4..fa740a9d8 100644 --- a/src/utility/region.h +++ b/src/utility/region.h @@ -24,6 +24,7 @@ namespace storm { namespace utility{ namespace region { + //Obtain the correct type for Variables and Coefficients out of a given Function type #ifdef STORM_HAVE_CARL template using VariableType = typename std::conditional<(std::is_same::value), storm::Variable, std::nullptr_t>::type; @@ -35,10 +36,6 @@ namespace storm { template using CoefficientType = std::nullptr_t; #endif - // template - // using PointType = std::map, CoefficientType>; - - enum class VariableSort {VS_BOOL, VS_REAL, VS_INT}; /* * Converts a number from one type to a number from the other. @@ -61,6 +58,7 @@ namespace storm { template VarType getVariableFromString(std::string variableString); + enum class VariableSort {VS_BOOL, VS_REAL, VS_INT}; /* * Creates a new variable with the given name and the given sort * If there is already a variable with that name, that variable is returned. diff --git a/src/utility/storm.h b/src/utility/storm.h index 4eefc31c1..643c826a0 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -302,6 +302,95 @@ namespace storm { } return result; } + + /*! + * Initializes a region model checker. + * + * @param regionModelChecker the resulting model checker object + * @param programFilePath a path to the prism program file + * @param formulaString The considered formula (as path to the file or directly as string.) Should be exactly one formula. + * @param constantsString can be used to specify constants for certain parameters, e.g., "p=0.9,R=42" + * @return true when initialization was successful + */ + inline bool initializeRegionModelChecker(std::shared_ptr, double>>& regionModelChecker, + std::string const& programFilePath, + std::string const& formulaString, + std::string const& constantsString=""){ + regionModelChecker.reset(); + // Program and formula + storm::prism::Program program = parseProgram(programFilePath); + program.checkValidity(); + std::vector> formulas = parseFormulasForProgram(formulaString, program); + if(formulas.size()!=1){ + STORM_LOG_ERROR("The given formulaString does not specify exactly one formula"); + return false; + } + // Parametric model + typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + options.addConstantDefinitionsFromString(program, constantsString); + options.preserveFormula(*formulas[0]); + std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program, options)->as>(); + preprocessModel(model,formulas); + // ModelChecker + if(model->isOfType(storm::models::ModelType::Dtmc)){ + regionModelChecker = std::make_shared, double>>(model); + } else if (model->isOfType(storm::models::ModelType::Mdp)){ + regionModelChecker = std::make_shared, double>>(model); + } else { + STORM_LOG_ERROR("The type of the given model is not supported (only Dtmcs or Mdps are supported"); + return false; + } + // Specify the formula + if(!regionModelChecker->canHandle(*formulas[0])){ + STORM_LOG_ERROR("The given formula is not supported."); + return false; + } + regionModelChecker->specifyFormula(formulas[0]); + return true; + } + + /*! + * Computes the reachability value at the given point by instantiating the model. + * + * @param regionModelChecker the model checker object that is to be used + * @param point the valuation of the different variables + * @return true iff the specified formula is satisfied (i.e., iff the reachability value is within the bound of the formula) + */ + inline bool checkSamplingPoint(std::shared_ptr, double>> regionModelChecker, + std::map const& point){ + return regionModelChecker->valueIsInBoundOfFormula(regionModelChecker->getReachabilityValue(point)); + } + + /*! + * Does an approximation of the reachability value for all parameters in the given region. + * @param regionModelChecker the model checker object that is to be used + * @param lowerBoundaries maps every variable to its lowest possible value within the region. (corresponds to the bottom left corner point in the 2D case) + * @param upperBoundaries maps every variable to its highest possible value within the region. (corresponds to the top right corner point in the 2D case) + * @param proveAllSat if set to true, it is checked whether the property is satisfied for all parameters in the given region. Otherwise, it is checked + * whether the property is violated for all parameters. + * @return true iff the objective was accomplished. + * + * So there are the following cases: + * proveAllSat=true, return=true ==> the property is SATISFIED for all parameters in the given region + * proveAllSat=true, return=false ==> the approximative value is NOT within the bound of the formula (either the approximation is too bad or there are points in the region that violate the property) + * proveAllSat=false, return=true ==> the property is VIOLATED for all parameters in teh given region + * proveAllSat=false, return=false ==> the approximative value IS within the bound of the formula (either the approximation is too bad or there are points in the region that satisfy the property) + */ + inline bool checkRegionApproximation(std::shared_ptr, double>> regionModelChecker, + std::map const& lowerBoundaries, + std::map const& upperBoundaries, + bool proveAllSat){ + storm::modelchecker::region::ParameterRegion region(lowerBoundaries, upperBoundaries); + double result=regionModelChecker->getApproximativeReachabilityValue(region, proveAllSat); + if(proveAllSat && regionModelChecker->valueIsInBoundOfFormula(result)){ + return true; + } else if (!proveAllSat && !regionModelChecker->valueIsInBoundOfFormula(result)){ + return true; + } else { + return false; + } + } + #endif diff --git a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp index 3752731f2..9f0b774ca 100644 --- a/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcRegionModelCheckerTest.cpp @@ -9,14 +9,9 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/RegionSettings.h" -#include "src/models/sparse/Dtmc.h" -#include "src/parser/PrismParser.h" -#include "src/parser/FormulaParser.h" -#include "src/logic/Formulas.h" -#include "src/models/ModelBase.h" +#include "utility/storm.h" #include "src/models/sparse/Model.h" -#include "src/models/sparse/Dtmc.h" -#include "builder/ExplicitPrismModelBuilder.h" +#include "modelchecker/region/AbstractSparseRegionModelChecker.h" #include "modelchecker/region/SparseDtmcRegionModelChecker.h" #include "modelchecker/region/ParameterRegion.h" @@ -26,49 +21,38 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { std::string const& formulaAsString = "P<=0.84 [F s=5 ]"; std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - //Build model, formula, region model checker - boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); - program->checkValidity(); - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - std::vector> formulas = formulaParser.parseFromString(formulaAsString); - typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); - options.addConstantDefinitionsFromString(program.get(), constantsAsString); - options.preserveFormula(*formulas[0]); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program.get(), options)->as>(); - ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); - ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); - modelchecker.specifyFormula(formulas[0]); + std::shared_ptr, double>> modelchecker; + ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); + auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pL<=0.9,0.75<=pK<=0.95"); auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=pL<=0.65,0.75<=pK<=0.95"); auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pL<=0.73,0.2<=pK<=0.715"); - EXPECT_NEAR(0.8369631407, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.8369631407, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allSatRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.0476784174, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.0476784174, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allSatRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.9987948367, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.9987948367, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(exBothRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6020480995, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6020480995, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(exBothRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.0000000000, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.0000000000, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.8429289733, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.8429289733, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.8369631407, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.8369631407, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.0476784174, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.0476784174, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.9987948367, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.9987948367, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.6020480995, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.6020480995, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(1.0000000000, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(1.0000000000, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.8429289733, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.8429289733, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_FALSE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegion); + dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); - modelchecker.checkRegion(exBothRegion); + dtmcModelchecker->checkRegion(exBothRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); - modelchecker.checkRegion(allVioRegion); + dtmcModelchecker->checkRegion(allVioRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) @@ -79,11 +63,11 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Prob) { ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegionSmt); + dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); - modelchecker.checkRegion(exBothRegionSmt); + dtmcModelchecker->checkRegion(exBothRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); - modelchecker.checkRegion(allVioRegionSmt); + dtmcModelchecker->checkRegion(allVioRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); @@ -95,20 +79,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { std::string const& formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; std::string const& constantsAsString = "pL=0.9,TOAck=0.5"; - //Build model, formula, region model checker - boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); - program->checkValidity(); - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - std::vector> formulas = formulaParser.parseFromString(formulaAsString); - typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); - options.addConstantDefinitionsFromString(program.get(), constantsAsString); - options.preserveFormula(*formulas[0]); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program.get(), options)->as>(); - ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); - ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); - modelchecker.specifyFormula(formulas[0]); + std::shared_ptr, double>> modelchecker; + ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); + auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pK<=0.875,0.75<=TOMsg<=0.95"); @@ -116,39 +89,39 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { auto exBothHardRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.5<=pK<=0.75,0.3<=TOMsg<=0.4"); //this region has a local maximum! auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pK<=0.3,0.2<=TOMsg<=0.3"); - EXPECT_NEAR(4.367791292, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(4.367791292, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allSatRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(3.044795147, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(3.044795147, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allSatRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(3.182535759, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(3.182535759, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(exBothRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(2.609602197, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(2.609602197, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(exBothRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.842551039, modelchecker.getReachabilityValue(exBothHardRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.842551039, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(exBothHardRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(2.453500364, modelchecker.getReachabilityValue(exBothHardRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(2.453500364, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(exBothHardRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6721974438, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6721974438, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.308324558, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(1.308324558, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(4.367791292, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(4.367791292, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(3.044795147, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(3.044795147, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(3.182535759, dtmcModelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(3.182535759, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(2.609602197, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(2.609602197, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(1.842551039, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(1.842551039, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(2.453500364, dtmcModelchecker->getReachabilityValue(exBothHardRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(2.453500364, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothHardRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.6721974438, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.6721974438, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(1.308324558, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(1.308324558, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_FALSE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegion); + dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); - modelchecker.checkRegion(exBothRegion); + dtmcModelchecker->checkRegion(exBothRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); - modelchecker.checkRegion(exBothHardRegion); + dtmcModelchecker->checkRegion(exBothHardRegion); //At this moment, Approximation should not be able to get a result for this region. (However, it is not wrong if it can) EXPECT_TRUE( (exBothHardRegion.getCheckResult()==(storm::modelchecker::region::RegionCheckResult::EXISTSBOTH)) || (exBothHardRegion.getCheckResult()==(storm::modelchecker::region::RegionCheckResult::EXISTSVIOLATED)) ); - modelchecker.checkRegion(allVioRegion); + dtmcModelchecker->checkRegion(allVioRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) @@ -160,13 +133,13 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegionSmt); + dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); - modelchecker.checkRegion(exBothRegionSmt); + dtmcModelchecker->checkRegion(exBothRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); - modelchecker.checkRegion(exBothHardRegionSmt); + dtmcModelchecker->checkRegion(exBothHardRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmt.getCheckResult()); - modelchecker.checkRegion(allVioRegionSmt); + dtmcModelchecker->checkRegion(allVioRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); //test smt + approx @@ -175,7 +148,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew) { ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(exBothHardRegionSmt); + dtmcModelchecker->checkRegion(exBothHardRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothHardRegionSmtApp.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); @@ -188,32 +161,21 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) { std::string const& formulaAsString = "R>2.5 [F (s=0&srep=3) ]"; std::string const& constantsAsString = ""; - //Build model, formula, region model checker - boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); - program->checkValidity(); - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - std::vector> formulas = formulaParser.parseFromString(formulaAsString); - typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); - options.addConstantDefinitionsFromString(program.get(), constantsAsString); - options.preserveFormula(*formulas[0]); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program.get(), options)->as>(); - ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); - ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); - modelchecker.specifyFormula(formulas[0]); + std::shared_ptr, double>> modelchecker; + ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); + auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion(""); - EXPECT_EQ(storm::utility::infinity(), modelchecker.getReachabilityValue(allSatRegion.getLowerBounds())); + EXPECT_EQ(storm::utility::infinity(), dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries())); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_FALSE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegion); + dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) @@ -222,7 +184,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_Infty) { ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegionSmt); + dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); @@ -235,43 +197,32 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) { std::string const& formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; std::string const& constantsAsString = ""; //!! this model will have 4 parameters - //Build model, formula, region model checker - boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); - program->checkValidity(); - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - std::vector> formulas = formulaParser.parseFromString(formulaAsString); - typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); - options.addConstantDefinitionsFromString(program.get(), constantsAsString); - options.preserveFormula(*formulas[0]); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program.get(), options)->as>(); - ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); - ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); - modelchecker.specifyFormula(formulas[0]); + std::shared_ptr, double>> modelchecker; + ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); + auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.7<=pK<=0.9,0.6<=pL<=0.85,0.9<=TOMsg<=0.95,0.85<=TOAck<=0.9"); auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pK<=0.7,0.2<=pL<=0.8,0.15<=TOMsg<=0.65,0.3<=TOAck<=0.9"); auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=pK<=0.4,0.2<=pL<=0.3,0.15<=TOMsg<=0.3,0.1<=TOAck<=0.2"); - EXPECT_NEAR(4.834779705, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(4.834779705, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allSatRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(4.674651623, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(4.674651623, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(exBothRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.4467496536, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.4467496536, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(4.834779705, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(4.834779705, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(4.674651623, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(4.674651623, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.4467496536, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.4467496536, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_FALSE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegion); + dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); - modelchecker.checkRegion(exBothRegion); + dtmcModelchecker->checkRegion(exBothRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); - modelchecker.checkRegion(allVioRegion); + dtmcModelchecker->checkRegion(allVioRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) @@ -282,11 +233,11 @@ TEST(SparseDtmcRegionModelCheckerTest, Brp_Rew_4Par) { ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegionSmt); + dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); - modelchecker.checkRegion(exBothRegionSmt); + dtmcModelchecker->checkRegion(exBothRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); - modelchecker.checkRegion(allVioRegionSmt); + dtmcModelchecker->checkRegion(allVioRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); @@ -299,20 +250,9 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) { std::string const& formulaAsString = "P<0.5 [F \"observe0Greater1\" ]"; std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - //Build model, formula, region model checker - boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); - program->checkValidity(); - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - std::vector> formulas = formulaParser.parseFromString(formulaAsString); - typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); - options.addConstantDefinitionsFromString(program.get(), constantsAsString); - options.preserveFormula(*formulas[0]); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program.get(), options)->as>(); - ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); - ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); - modelchecker.specifyFormula(formulas[0]); + std::shared_ptr, double>> modelchecker; + ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); + auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.1<=PF<=0.75,0.15<=badC<=0.2"); @@ -320,31 +260,31 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) { auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.2"); auto allVioHardRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.95,0.2<=badC<=0.9"); - EXPECT_NEAR(0.1734086422, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1734086422, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allSatRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.47178, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.47178, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allSatRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(exBothRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.5095205203, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.5095205203, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6819701472, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6819701472, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.999895897, modelchecker.getReachabilityValue(allVioHardRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.999895897, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioHardRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1734086422, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1734086422, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.47178, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.47178, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.5095205203, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.5095205203, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.6819701472, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.6819701472, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.999895897, dtmcModelchecker->getReachabilityValue(allVioHardRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.999895897, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioHardRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_FALSE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegion); + dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); - modelchecker.checkRegion(exBothRegion); + dtmcModelchecker->checkRegion(exBothRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); - modelchecker.checkRegion(allVioRegion); + dtmcModelchecker->checkRegion(allVioRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); - modelchecker.checkRegion(allVioHardRegion); + dtmcModelchecker->checkRegion(allVioHardRegion); //At this moment, Approximation should not be able to get a result for this region. (However, it is not wrong if it can) EXPECT_TRUE( (allVioHardRegion.getCheckResult()==(storm::modelchecker::region::RegionCheckResult::ALLVIOLATED)) || @@ -360,13 +300,13 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) { ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegionSmt); + dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); - modelchecker.checkRegion(exBothRegionSmt); + dtmcModelchecker->checkRegion(exBothRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); - modelchecker.checkRegion(allVioRegionSmt); + dtmcModelchecker->checkRegion(allVioRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); - modelchecker.checkRegion(allVioHardRegionSmt); + dtmcModelchecker->checkRegion(allVioHardRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmt.getCheckResult()); //test smt + approx @@ -375,7 +315,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob) { ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allVioHardRegionSmt); + dtmcModelchecker->checkRegion(allVioHardRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioHardRegionSmtApp.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); @@ -388,45 +328,34 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) { std::string const& formulaAsString = "P>0.75 [F \"observe0Greater1\" ]"; std::string const& constantsAsString = "badC=0.3"; //e.g. pL=0.9,TOACK=0.5 - //Build model, formula, region model checker - boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); - program->checkValidity(); - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - std::vector> formulas = formulaParser.parseFromString(formulaAsString); - typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); - options.addConstantDefinitionsFromString(program.get(), constantsAsString); - options.preserveFormula(*formulas[0]); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program.get(), options)->as>(); - ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); - ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); - modelchecker.specifyFormula(formulas[0]); + std::shared_ptr, double>> modelchecker; + ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); + auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.9<=PF<=0.99"); auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.8<=PF<=0.9"); auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.01<=PF<=0.8"); - EXPECT_NEAR(0.8430128158, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.8430128158, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allSatRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7731321947, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7731321947, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(exBothRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.4732302663, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.4732302663, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7085157883, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allVioRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.8430128158, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.8430128158, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.7731321947, dtmcModelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.7731321947, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(exBothRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.4732302663, dtmcModelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.4732302663, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.7085157883, dtmcModelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.7085157883, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allVioRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_FALSE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegion); + dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); - modelchecker.checkRegion(exBothRegion); + dtmcModelchecker->checkRegion(exBothRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); - modelchecker.checkRegion(allVioRegion); + dtmcModelchecker->checkRegion(allVioRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) @@ -437,11 +366,11 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_1Par) { ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegionSmt); + dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); - modelchecker.checkRegion(exBothRegionSmt); + dtmcModelchecker->checkRegion(exBothRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegionSmt.getCheckResult()); - modelchecker.checkRegion(allVioRegionSmt); + dtmcModelchecker->checkRegion(allVioRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegionSmt.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); @@ -454,34 +383,24 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) { std::string const& formulaAsString = "P>0.6 [F \"observe0Greater1\" ]"; std::string const& constantsAsString = "PF=0.9,badC=0.2"; - //Build model, formula, region model checker - boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); - program->checkValidity(); - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - std::vector> formulas = formulaParser.parseFromString(formulaAsString); - typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); - options.addConstantDefinitionsFromString(program.get(), constantsAsString); - options.preserveFormula(*formulas[0]); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program.get(), options)->as>(); - ASSERT_EQ(storm::models::ModelType::Dtmc, model->getType()); - std::shared_ptr> dtmc = model->template as>(); - storm::modelchecker::region::SparseDtmcRegionModelChecker, double> modelchecker(*dtmc); - ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); - modelchecker.specifyFormula(formulas[0]); + std::shared_ptr, double>> modelchecker; + ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); + auto dtmcModelchecker = std::static_pointer_cast, double>>(modelchecker); + //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion(""); - EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allSatRegion.getUpperBounds())), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6119660237, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(modelchecker.evaluateReachabilityFunction(allSatRegion.getLowerBounds())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getUpperBoundaries())), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.6119660237, dtmcModelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.6119660237, storm::utility::region::convertNumber(dtmcModelchecker->evaluateReachabilityFunction(allSatRegion.getLowerBoundaries())), storm::settings::generalSettings().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_FALSE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegion); + dtmcModelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); //test smt method (the regions need to be created again, because the old ones have some information stored in their internal state) @@ -490,7 +409,7 @@ TEST(SparseDtmcRegionModelCheckerTest, Crowds_Prob_Const) { ASSERT_FALSE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_TRUE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegionSmt); + dtmcModelchecker->checkRegion(allSatRegionSmt); //smt EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegionSmt.getCheckResult()); storm::settings::mutableRegionSettings().resetModes(); diff --git a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp index a321ff837..6a6db1078 100644 --- a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp @@ -9,62 +9,62 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/RegionSettings.h" -#include "src/models/sparse/Dtmc.h" -#include "src/parser/PrismParser.h" -#include "src/parser/FormulaParser.h" -#include "src/logic/Formulas.h" -#include "src/models/ModelBase.h" +#include "utility/storm.h" #include "src/models/sparse/Model.h" -#include "src/models/sparse/Dtmc.h" -#include "builder/ExplicitPrismModelBuilder.h" -#include "modelchecker/region/SparseMdpRegionModelChecker.h" +#include "modelchecker/region/AbstractSparseRegionModelChecker.h" #include "modelchecker/region/ParameterRegion.h" TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) { std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pmdp/two_dice/two_dice.nm"; - std::string const& formulaAsString = "P<=0.17 [F \"doubles\" ]"; + std::string const& formulaFile = STORM_CPP_BASE_PATH "/examples/pmdp/two_dice/two_dice.prctl"; //P<=0.17 [F \"doubles\" ]"; std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - //Build model, formula, region model checker - boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); - program->checkValidity(); - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - std::vector> formulas = formulaParser.parseFromString(formulaAsString); - typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); - options.addConstantDefinitionsFromString(program.get(), constantsAsString); - options.preserveFormula(*formulas[0]); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program.get(), options)->as>(); - ASSERT_EQ(storm::models::ModelType::Mdp, model->getType()); - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::region::SparseMdpRegionModelChecker, double> modelchecker(*mdp); - ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); - modelchecker.specifyFormula(formulas[0]); + std::shared_ptr, double>> modelchecker; + ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaFile, constantsAsString)); - //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.495<=p1<=0.5,0.5<=p2<=0.505"); auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.45<=p1<=0.55,0.45<=p2<=0.55"); auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.6<=p1<=0.7,0.6<=p2<=0.6"); - EXPECT_NEAR(0.1666665285, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1666665529, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1716553235, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1709666953, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1826972576, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.1964429282, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - + //Test the methods provided in storm.h + EXPECT_TRUE(storm::checkSamplingPoint(modelchecker,allSatRegion.getLowerBoundaries())); + EXPECT_TRUE(storm::checkSamplingPoint(modelchecker,allSatRegion.getUpperBoundaries())); + EXPECT_FALSE(storm::checkSamplingPoint(modelchecker,exBothRegion.getLowerBoundaries())); + EXPECT_FALSE(storm::checkSamplingPoint(modelchecker,exBothRegion.getUpperBoundaries())); + EXPECT_TRUE(storm::checkSamplingPoint(modelchecker,exBothRegion.getVerticesOfRegion(exBothRegion.getVariables())[1])); + EXPECT_TRUE(storm::checkSamplingPoint(modelchecker,exBothRegion.getVerticesOfRegion(exBothRegion.getVariables())[2])); + EXPECT_FALSE(storm::checkSamplingPoint(modelchecker,exBothRegion.getUpperBoundaries())); + EXPECT_FALSE(storm::checkSamplingPoint(modelchecker,allVioRegion.getLowerBoundaries())); + EXPECT_FALSE(storm::checkSamplingPoint(modelchecker,allVioRegion.getUpperBoundaries())); + + EXPECT_TRUE(storm::checkRegionApproximation(modelchecker, allSatRegion.getLowerBoundaries(), allSatRegion.getUpperBoundaries(), true)); + EXPECT_FALSE(storm::checkRegionApproximation(modelchecker, allSatRegion.getLowerBoundaries(), allSatRegion.getUpperBoundaries(), false)); + EXPECT_FALSE(storm::checkRegionApproximation(modelchecker, exBothRegion.getLowerBoundaries(), exBothRegion.getUpperBoundaries(), true)); + EXPECT_FALSE(storm::checkRegionApproximation(modelchecker, exBothRegion.getLowerBoundaries(), exBothRegion.getUpperBoundaries(), false)); + EXPECT_FALSE(storm::checkRegionApproximation(modelchecker, allVioRegion.getLowerBoundaries(), allVioRegion.getUpperBoundaries(), true)); + EXPECT_TRUE(storm::checkRegionApproximation(modelchecker, allVioRegion.getLowerBoundaries(), allVioRegion.getUpperBoundaries(), false)); + + //Remaining tests.. + EXPECT_NEAR(0.1666665285, modelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1666665529, modelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1716553235, modelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1709666953, modelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1826972576, modelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.1964429282, modelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_FALSE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegion); + + modelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); - modelchecker.checkRegion(exBothRegion); + modelchecker->checkRegion(exBothRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); - modelchecker.checkRegion(allVioRegion); + modelchecker->checkRegion(allVioRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); - + storm::settings::mutableRegionSettings().resetModes(); carl::VariablePool::getInstance().clear(); } @@ -75,43 +75,31 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) { std::string const& formulaAsString = "P>0.25 [F \"finished\"&\"all_coins_equal_1\" ]"; std::string const& constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 - //Build model, formula, region model checker - boost::optional program=storm::parser::PrismParser::parse(programFile).simplify().simplify(); - program->checkValidity(); - storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer()); - std::vector> formulas = formulaParser.parseFromString(formulaAsString); - typename storm::builder::ExplicitPrismModelBuilder::Options options=storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); - options.addConstantDefinitionsFromString(program.get(), constantsAsString); - options.preserveFormula(*formulas[0]); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder().translateProgram(program.get(), options)->as>(); - ASSERT_EQ(storm::models::ModelType::Mdp, model->getType()); - std::shared_ptr> mdp = model->template as>(); - storm::modelchecker::region::SparseMdpRegionModelChecker, double> modelchecker(*mdp); - ASSERT_TRUE(modelchecker.canHandle(*formulas[0])); - modelchecker.specifyFormula(formulas[0]); + std::shared_ptr, double>> modelchecker; + ASSERT_TRUE(storm::initializeRegionModelChecker(modelchecker, programFile, formulaAsString, constantsAsString)); //start testing auto allSatRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54"); auto exBothRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7"); auto allVioRegion=storm::modelchecker::region::ParameterRegion::parseRegion("0.4<=p1<=0.7,0.55<=p2<=0.6"); - EXPECT_NEAR(0.95127874851, modelchecker.getReachabilityValue(allSatRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.26787251126, modelchecker.getReachabilityValue(allSatRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.41880006098, modelchecker.getReachabilityValue(exBothRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.01535089684, modelchecker.getReachabilityValue(exBothRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.24952791523, modelchecker.getReachabilityValue(allVioRegion.getLowerBounds()), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.01711494956, modelchecker.getReachabilityValue(allVioRegion.getUpperBounds()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.95127874851, modelchecker->getReachabilityValue(allSatRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.26787251126, modelchecker->getReachabilityValue(allSatRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.41880006098, modelchecker->getReachabilityValue(exBothRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.01535089684, modelchecker->getReachabilityValue(exBothRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.24952791523, modelchecker->getReachabilityValue(allVioRegion.getLowerBoundaries()), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.01711494956, modelchecker->getReachabilityValue(allVioRegion.getUpperBoundaries()), storm::settings::generalSettings().getPrecision()); //test approximative method storm::settings::mutableRegionSettings().modifyModes(storm::settings::modules::RegionSettings::ApproxMode::TESTFIRST, storm::settings::modules::RegionSettings::SampleMode::INSTANTIATE, storm::settings::modules::RegionSettings::SmtMode::OFF); ASSERT_TRUE(storm::settings::regionSettings().doApprox()); ASSERT_TRUE(storm::settings::regionSettings().doSample()); ASSERT_FALSE(storm::settings::regionSettings().doSmt()); - modelchecker.checkRegion(allSatRegion); + modelchecker->checkRegion(allSatRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLSAT), allSatRegion.getCheckResult()); - modelchecker.checkRegion(exBothRegion); + modelchecker->checkRegion(exBothRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::EXISTSBOTH), exBothRegion.getCheckResult()); - modelchecker.checkRegion(allVioRegion); + modelchecker->checkRegion(allVioRegion); EXPECT_EQ((storm::modelchecker::region::RegionCheckResult::ALLVIOLATED), allVioRegion.getCheckResult()); storm::settings::mutableRegionSettings().resetModes();