diff --git a/examples/pmdp/brp/brp.prctl b/examples/pmdp/brp/brp.prctl new file mode 100644 index 000000000..7278b1e7f --- /dev/null +++ b/examples/pmdp/brp/brp.prctl @@ -0,0 +1,2 @@ +P<0.5 [ F (s=5 & T) ] + diff --git a/examples/pmdp/brp/brpRegions.txt b/examples/pmdp/brp/brpRegions.txt new file mode 100644 index 000000000..fe67834cc --- /dev/null +++ b/examples/pmdp/brp/brpRegions.txt @@ -0,0 +1,400 @@ +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/brp/brp_16_2.nm b/examples/pmdp/brp/brp_16_2.nm new file mode 100644 index 000000000..2141803ae --- /dev/null +++ b/examples/pmdp/brp/brp_16_2.nm @@ -0,0 +1,139 @@ +// bounded retransmission protocol [D'AJJL01] +// gxn/dxp 23/05/2001 +// Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de) + +mdp +//dtmc + +// number of chunks +const int N = 16; +// maximum number of retransmissions +const int MAX = 2; + +// reliability of channels +const double pL; +const double pK; + +global T : bool; + +module sender + + s : [0..6]; + // 0 idle + // 1 next_frame + // 2 wait_ack + // 3 retransmit + // 4 success + // 5 error + // 6 wait sync + srep : [0..3]; + // 0 bottom + // 1 not ok (nok) + // 2 do not know (dk) + // 3 ok (ok) + nrtr : [0..MAX]; + i : [0..N]; + bs : bool; + s_ab : bool; + fs : bool; + ls : bool; + + // idle + [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); + // next_frame + [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); + // wait_ack + [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); + [TO_Msg] (s=2) -> (s'=3); + [TO_Ack] (s=2) -> (s'=3); + // retransmit + [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); + [] (s=4) & (i=N) -> (s'=0) & (srep'=3); + // error + [SyncWait] (s=5) -> (s'=6); + // wait sync + [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); + +endmodule + +module receiver + + r : [0..5]; + // 0 new_file + // 1 fst_safe + // 2 frame_received + // 3 frame_reported + // 4 idle + // 5 resync + rrep : [0..4]; + // 0 bottom + // 1 fst + // 2 inc + // 3 ok + // 4 nok + fr : bool; + lr : bool; + br : bool; + r_ab : bool; + recv : bool; + + + // new_file + [SyncWait] (r=0) -> (r'=0); + [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + // fst_safe_frame + [] (r=1) -> (r'=2) & (r_ab'=br); + // frame_received + [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); + [aA] (r=2) & !(r_ab=br) -> (r'=4); + // frame_reported + [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); + // idle + [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + [SyncWait] (r=4) & (ls=true) -> (r'=5); + [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); + // resync + [SyncWait] (r=5) -> (r'=0) & (rrep'=0); + +endmodule + +module checker + + [NewFile] (T=false) -> (T'=false); + [NewFile] (T=false) -> (T'=true); + +endmodule + +module channelK + + k : [0..2]; + + // idle + [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); + // sending + [aG] (k=1) -> (k'=0); + // lost + [TO_Msg] (k=2) -> (k'=0); + +endmodule + +module channelL + + l : [0..2]; + + // idle + [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); + // sending + [aB] (l=1) -> (l'=0); + // lost + [TO_Ack] (l=2) -> (l'=0); + +endmodule + + diff --git a/examples/pmdp/brp/brp_256_5.nm b/examples/pmdp/brp/brp_256_5.nm new file mode 100644 index 000000000..dd98aee83 --- /dev/null +++ b/examples/pmdp/brp/brp_256_5.nm @@ -0,0 +1,139 @@ +// bounded retransmission protocol [D'AJJL01] +// gxn/dxp 23/05/2001 +// Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de) + +mdp +//dtmc + +// number of chunks +const int N = 256; +// maximum number of retransmissions +const int MAX = 5; + +// reliability of channels +const double pL; +const double pK; + +global T : bool; + +module sender + + s : [0..6]; + // 0 idle + // 1 next_frame + // 2 wait_ack + // 3 retransmit + // 4 success + // 5 error + // 6 wait sync + srep : [0..3]; + // 0 bottom + // 1 not ok (nok) + // 2 do not know (dk) + // 3 ok (ok) + nrtr : [0..MAX]; + i : [0..N]; + bs : bool; + s_ab : bool; + fs : bool; + ls : bool; + + // idle + [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); + // next_frame + [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); + // wait_ack + [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); + [TO_Msg] (s=2) -> (s'=3); + [TO_Ack] (s=2) -> (s'=3); + // retransmit + [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); + [] (s=4) & (i=N) -> (s'=0) & (srep'=3); + // error + [SyncWait] (s=5) -> (s'=6); + // wait sync + [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); + +endmodule + +module receiver + + r : [0..5]; + // 0 new_file + // 1 fst_safe + // 2 frame_received + // 3 frame_reported + // 4 idle + // 5 resync + rrep : [0..4]; + // 0 bottom + // 1 fst + // 2 inc + // 3 ok + // 4 nok + fr : bool; + lr : bool; + br : bool; + r_ab : bool; + recv : bool; + + + // new_file + [SyncWait] (r=0) -> (r'=0); + [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + // fst_safe_frame + [] (r=1) -> (r'=2) & (r_ab'=br); + // frame_received + [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); + [aA] (r=2) & !(r_ab=br) -> (r'=4); + // frame_reported + [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); + // idle + [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + [SyncWait] (r=4) & (ls=true) -> (r'=5); + [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); + // resync + [SyncWait] (r=5) -> (r'=0) & (rrep'=0); + +endmodule + +module checker + + [NewFile] (T=false) -> (T'=false); + [NewFile] (T=false) -> (T'=true); + +endmodule + +module channelK + + k : [0..2]; + + // idle + [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); + // sending + [aG] (k=1) -> (k'=0); + // lost + [TO_Msg] (k=2) -> (k'=0); + +endmodule + +module channelL + + l : [0..2]; + + // idle + [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); + // sending + [aB] (l=1) -> (l'=0); + // lost + [TO_Ack] (l=2) -> (l'=0); + +endmodule + + diff --git a/examples/pmdp/brp/brp_512_5.nm b/examples/pmdp/brp/brp_512_5.nm new file mode 100644 index 000000000..63beec6d5 --- /dev/null +++ b/examples/pmdp/brp/brp_512_5.nm @@ -0,0 +1,139 @@ +// bounded retransmission protocol [D'AJJL01] +// gxn/dxp 23/05/2001 +// Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de) + +mdp +//dtmc + +// number of chunks +const int N = 512; +// maximum number of retransmissions +const int MAX = 5; + +// reliability of channels +const double pL; +const double pK; + +global T : bool; + +module sender + + s : [0..6]; + // 0 idle + // 1 next_frame + // 2 wait_ack + // 3 retransmit + // 4 success + // 5 error + // 6 wait sync + srep : [0..3]; + // 0 bottom + // 1 not ok (nok) + // 2 do not know (dk) + // 3 ok (ok) + nrtr : [0..MAX]; + i : [0..N]; + bs : bool; + s_ab : bool; + fs : bool; + ls : bool; + + // idle + [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); + // next_frame + [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); + // wait_ack + [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); + [TO_Msg] (s=2) -> (s'=3); + [TO_Ack] (s=2) -> (s'=3); + // retransmit + [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); + [] (s=4) & (i=N) -> (s'=0) & (srep'=3); + // error + [SyncWait] (s=5) -> (s'=6); + // wait sync + [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); + +endmodule + +module receiver + + r : [0..5]; + // 0 new_file + // 1 fst_safe + // 2 frame_received + // 3 frame_reported + // 4 idle + // 5 resync + rrep : [0..4]; + // 0 bottom + // 1 fst + // 2 inc + // 3 ok + // 4 nok + fr : bool; + lr : bool; + br : bool; + r_ab : bool; + recv : bool; + + + // new_file + [SyncWait] (r=0) -> (r'=0); + [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + // fst_safe_frame + [] (r=1) -> (r'=2) & (r_ab'=br); + // frame_received + [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); + [aA] (r=2) & !(r_ab=br) -> (r'=4); + // frame_reported + [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); + // idle + [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + [SyncWait] (r=4) & (ls=true) -> (r'=5); + [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); + // resync + [SyncWait] (r=5) -> (r'=0) & (rrep'=0); + +endmodule + +module checker + + [NewFile] (T=false) -> (T'=false); + [NewFile] (T=false) -> (T'=true); + +endmodule + +module channelK + + k : [0..2]; + + // idle + [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); + // sending + [aG] (k=1) -> (k'=0); + // lost + [TO_Msg] (k=2) -> (k'=0); + +endmodule + +module channelL + + l : [0..2]; + + // idle + [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); + // sending + [aB] (l=1) -> (l'=0); + // lost + [TO_Ack] (l=2) -> (l'=0); + +endmodule + + diff --git a/examples/pmdp/brp/brp_64_4.nm b/examples/pmdp/brp/brp_64_4.nm new file mode 100644 index 000000000..e75829359 --- /dev/null +++ b/examples/pmdp/brp/brp_64_4.nm @@ -0,0 +1,139 @@ +// bounded retransmission protocol [D'AJJL01] +// gxn/dxp 23/05/2001 +// Modified by Ernst Moritz Hahn (emh@cs.uni-sb.de) + +mdp +//dtmc + +// number of chunks +const int N = 64; +// maximum number of retransmissions +const int MAX = 4; + +// reliability of channels +const double pL; +const double pK; + +global T : bool; + +module sender + + s : [0..6]; + // 0 idle + // 1 next_frame + // 2 wait_ack + // 3 retransmit + // 4 success + // 5 error + // 6 wait sync + srep : [0..3]; + // 0 bottom + // 1 not ok (nok) + // 2 do not know (dk) + // 3 ok (ok) + nrtr : [0..MAX]; + i : [0..N]; + bs : bool; + s_ab : bool; + fs : bool; + ls : bool; + + // idle + [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); + // next_frame + [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); + // wait_ack + [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); + [TO_Msg] (s=2) -> (s'=3); + [TO_Ack] (s=2) -> (s'=3); + // retransmit + [aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i<N) -> (s'=1) & (i'=i+1); + [] (s=4) & (i=N) -> (s'=0) & (srep'=3); + // error + [SyncWait] (s=5) -> (s'=6); + // wait sync + [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); + +endmodule + +module receiver + + r : [0..5]; + // 0 new_file + // 1 fst_safe + // 2 frame_received + // 3 frame_reported + // 4 idle + // 5 resync + rrep : [0..4]; + // 0 bottom + // 1 fst + // 2 inc + // 3 ok + // 4 nok + fr : bool; + lr : bool; + br : bool; + r_ab : bool; + recv : bool; + + + // new_file + [SyncWait] (r=0) -> (r'=0); + [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + // fst_safe_frame + [] (r=1) -> (r'=2) & (r_ab'=br); + // frame_received + [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); + [aA] (r=2) & !(r_ab=br) -> (r'=4); + // frame_reported + [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); + // idle + [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + [SyncWait] (r=4) & (ls=true) -> (r'=5); + [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); + // resync + [SyncWait] (r=5) -> (r'=0) & (rrep'=0); + +endmodule + +module checker + + [NewFile] (T=false) -> (T'=false); + [NewFile] (T=false) -> (T'=true); + +endmodule + +module channelK + + k : [0..2]; + + // idle + [aF] (k=0) -> pK : (k'=1) + 1-pK : (k'=2); + // sending + [aG] (k=1) -> (k'=0); + // lost + [TO_Msg] (k=2) -> (k'=0); + +endmodule + +module channelL + + l : [0..2]; + + // idle + [aA] (l=0) -> pL : (l'=1) + 1-pL : (l'=2); + // sending + [aB] (l=1) -> (l'=0); + // lost + [TO_Ack] (l=2) -> (l'=0); + +endmodule + + diff --git a/examples/pmdp/consensus/4pars/coin4_2.nm b/examples/pmdp/consensus/4pars/coin4_2.nm deleted file mode 100644 index 60a4359f1..000000000 --- a/examples/pmdp/consensus/4pars/coin4_2.nm +++ /dev/null @@ -1,69 +0,0 @@ -// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] -// gxn/dxp 20/11/00 - -mdp - -// constants -const int N=4; -const int K=2; -const int range = 2*(K+1)*N; -const int counter_init = (K+1)*N; -const int left = N; -const int right = 2*(K+1)*N - N; - -//Coin Probabilities -const double p1; -const double p2; -const double p3; -const double p4; - -// shared coin -global counter : [0..range] init counter_init; - -module process1 - - // program counter - pc1 : [0..3]; - // 0 - flip - // 1 - write - // 2 - check - // 3 - finished - - // local coin - coin1 : [0..1]; - - // flip coin - [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1-p1 : (coin1'=1) & (pc1'=1); - // write tails -1 (reset coin to add regularity) - [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); - // write heads +1 (reset coin to add regularity) - [] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); - // check - // decide tails - [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); - // decide heads - [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); - // flip again - [] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); - // loop (all loop together when done) - [done] (pc1=3) -> 1 : (pc1'=3); - -endmodule - -// construct remaining processes through renaming -module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule -module process3 = process1[pc1=pc3,coin1=coin3,p1=p3] endmodule -module process4 = process1[pc1=pc4,coin1=coin4,p1=p4] endmodule - -// labels -label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 ; -label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 ; -label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 ; -label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 ; -label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 ; - -// rewards -rewards "steps" - true : 1; -endrewards - diff --git a/examples/pmdp/consensus/4pars/coin4_8.nm b/examples/pmdp/consensus/4pars/coin4_8.nm deleted file mode 100644 index c0d28c969..000000000 --- a/examples/pmdp/consensus/4pars/coin4_8.nm +++ /dev/null @@ -1,69 +0,0 @@ -// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] -// gxn/dxp 20/11/00 - -mdp - -// constants -const int N=4; -const int K=8; -const int range = 2*(K+1)*N; -const int counter_init = (K+1)*N; -const int left = N; -const int right = 2*(K+1)*N - N; - -//Coin Probabilities -const double p1; -const double p2; -const double p3; -const double p4; - -// shared coin -global counter : [0..range] init counter_init; - -module process1 - - // program counter - pc1 : [0..3]; - // 0 - flip - // 1 - write - // 2 - check - // 3 - finished - - // local coin - coin1 : [0..1]; - - // flip coin - [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1-p1 : (coin1'=1) & (pc1'=1); - // write tails -1 (reset coin to add regularity) - [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); - // write heads +1 (reset coin to add regularity) - [] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); - // check - // decide tails - [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); - // decide heads - [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); - // flip again - [] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); - // loop (all loop together when done) - [done] (pc1=3) -> 1 : (pc1'=3); - -endmodule - -// construct remaining processes through renaming -module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule -module process3 = process1[pc1=pc3,coin1=coin3,p1=p3] endmodule -module process4 = process1[pc1=pc4,coin1=coin4,p1=p4] endmodule - -// labels -label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 ; -label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 ; -label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 ; -label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 ; -label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 ; - -// rewards -rewards "steps" - true : 1; -endrewards - diff --git a/examples/pmdp/consensus/coin.prctl b/examples/pmdp/consensus/coin.prctl new file mode 100644 index 000000000..2fe017f65 --- /dev/null +++ b/examples/pmdp/consensus/coin.prctl @@ -0,0 +1,4 @@ +P>=0.25 [ F "finished"&"all_coins_equal_1" ] + + + diff --git a/examples/pmdp/consensus/coin2ParRegions.txt b/examples/pmdp/consensus/coin2ParRegions.txt new file mode 100644 index 000000000..80387f197 --- /dev/null +++ b/examples/pmdp/consensus/coin2ParRegions.txt @@ -0,0 +1,400 @@ +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/consensus/coin2_1024.nm b/examples/pmdp/consensus/coin2_1024.nm deleted file mode 100644 index c45370e98..000000000 --- a/examples/pmdp/consensus/coin2_1024.nm +++ /dev/null @@ -1,65 +0,0 @@ -// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] -// gxn/dxp 20/11/00 - -mdp - -// constants -const int N=2; -const int K=1024; -const int range = 2*(K+1)*N; -const int counter_init = (K+1)*N; -const int left = N; -const int right = 2*(K+1)*N - N; - -//Coin Probabilities -const double p; -const double q; - -// shared coin -global counter : [0..range] init counter_init; - -module process1 - - // program counter - pc1 : [0..3]; - // 0 - flip - // 1 - write - // 2 - check - // 3 - finished - - // local coin - coin1 : [0..1]; - - // flip coin - [] (pc1=0) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); - // write tails -1 (reset coin to add regularity) - [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); - // write heads +1 (reset coin to add regularity) - [] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); - // check - // decide tails - [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); - // decide heads - [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); - // flip again - [] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); - // loop (all loop together when done) - [done] (pc1=3) -> 1 : (pc1'=3); - -endmodule - -// construct remaining processes through renaming -module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule - -// labels -label "finished" = pc1=3 & pc2=3 ; -label "all_coins_equal_0" = coin1=0 & coin2=0 ; -label "all_coins_equal_1" = coin1=1 & coin2=1 ; -label "agree" = coin1=coin2 ; -label "finish_with_1" = pc1=3 & pc2=3 & coin1=1 & coin2=1 ; - -// rewards -rewards "steps" - true : 1; -endrewards - diff --git a/examples/pmdp/consensus/coin2_128.nm b/examples/pmdp/consensus/coin2_128.nm new file mode 100644 index 000000000..73944141b --- /dev/null +++ b/examples/pmdp/consensus/coin2_128.nm @@ -0,0 +1,56 @@ +//Randomised Consensus Protocol + +mdp +const double p1; // in [0.2 , 0.8] +const double p2; // in [0.2 , 0.8] + + +const int N=2; +const int K=128; +const int range = 2*(K+1)*N; +const int counter_init = (K+1)*N; +const int left = N; +const int right = 2*(K+1)*N - N; + +// shared coin +global counter : [0..range] init counter_init; + +module process1 + + // program counter + pc1 : [0..3]; + // 0 - flip + // 1 - write + // 2 - check + // 3 - finished + + // local coin + coin1 : [0..1]; + + // flip coin + [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> (pc1'=3); + +endmodule + +module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule +label "finished" = pc1=3 &pc2=3 ; +label "all_coins_equal_1" = coin1=1 &coin2=1 ; +rewards "steps" + true : 1; +endrewards + + + diff --git a/examples/pmdp/consensus/coin2_2.nm b/examples/pmdp/consensus/coin2_2.nm index b9d095acc..3f5358cdd 100644 --- a/examples/pmdp/consensus/coin2_2.nm +++ b/examples/pmdp/consensus/coin2_2.nm @@ -1,9 +1,10 @@ -// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] -// gxn/dxp 20/11/00 +//Randomised Consensus Protocol mdp +const double p1; // in [0.2 , 0.8] +const double p2; // in [0.2 , 0.8] + -// constants const int N=2; const int K=2; const int range = 2*(K+1)*N; @@ -11,10 +12,6 @@ const int counter_init = (K+1)*N; const int left = N; const int right = 2*(K+1)*N - N; -//Coin Probabilities -const double p; -const double q; - // shared coin global counter : [0..range] init counter_init; @@ -31,35 +28,29 @@ module process1 coin1 : [0..1]; // flip coin - [] (pc1=0) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); + [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1); // write tails -1 (reset coin to add regularity) - [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); // write heads +1 (reset coin to add regularity) - [] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + [] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0); // check // decide tails - [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); // decide heads - [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); // flip again - [] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); + [] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0); // loop (all loop together when done) - [done] (pc1=3) -> 1 : (pc1'=3); + [done] (pc1=3) -> (pc1'=3); endmodule -// construct remaining processes through renaming -module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule - -// labels -label "finished" = pc1=3 & pc2=3 ; -label "all_coins_equal_0" = coin1=0 & coin2=0 ; -label "all_coins_equal_1" = coin1=1 & coin2=1 ; -label "agree" = coin1=coin2 ; -label "finish_with_1" = pc1=3 & pc2=3 & coin1=1 & coin2=1 ; - -// rewards +module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule +label "finished" = pc1=3 &pc2=3 ; +label "all_coins_equal_1" = coin1=1 &coin2=1 ; rewards "steps" true : 1; endrewards + + diff --git a/examples/pmdp/consensus/coin2_4.nm b/examples/pmdp/consensus/coin2_4.nm new file mode 100644 index 000000000..ce7bd1e80 --- /dev/null +++ b/examples/pmdp/consensus/coin2_4.nm @@ -0,0 +1,56 @@ +//Randomised Consensus Protocol + +mdp +const double p1; // in [0.2 , 0.8] +const double p2; // in [0.2 , 0.8] + + +const int N=2; +const int K=4; +const int range = 2*(K+1)*N; +const int counter_init = (K+1)*N; +const int left = N; +const int right = 2*(K+1)*N - N; + +// shared coin +global counter : [0..range] init counter_init; + +module process1 + + // program counter + pc1 : [0..3]; + // 0 - flip + // 1 - write + // 2 - check + // 3 - finished + + // local coin + coin1 : [0..1]; + + // flip coin + [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> (pc1'=3); + +endmodule + +module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule +label "finished" = pc1=3 &pc2=3 ; +label "all_coins_equal_1" = coin1=1 &coin2=1 ; +rewards "steps" + true : 1; +endrewards + + + diff --git a/examples/pmdp/consensus/coin2_64.nm b/examples/pmdp/consensus/coin2_64.nm index c2fe236c1..7f516964c 100644 --- a/examples/pmdp/consensus/coin2_64.nm +++ b/examples/pmdp/consensus/coin2_64.nm @@ -1,9 +1,10 @@ -// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] -// gxn/dxp 20/11/00 +//Randomised Consensus Protocol mdp +const double p1; // in [0.2 , 0.8] +const double p2; // in [0.2 , 0.8] + -// constants const int N=2; const int K=64; const int range = 2*(K+1)*N; @@ -11,10 +12,6 @@ const int counter_init = (K+1)*N; const int left = N; const int right = 2*(K+1)*N - N; -//Coin Probabilities -const double p; -const double q; - // shared coin global counter : [0..range] init counter_init; @@ -31,35 +28,29 @@ module process1 coin1 : [0..1]; // flip coin - [] (pc1=0) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); + [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1); // write tails -1 (reset coin to add regularity) - [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); // write heads +1 (reset coin to add regularity) - [] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + [] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0); // check // decide tails - [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); // decide heads - [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); // flip again - [] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); + [] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0); // loop (all loop together when done) - [done] (pc1=3) -> 1 : (pc1'=3); + [done] (pc1=3) -> (pc1'=3); endmodule -// construct remaining processes through renaming -module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule - -// labels -label "finished" = pc1=3 & pc2=3 ; -label "all_coins_equal_0" = coin1=0 & coin2=0 ; -label "all_coins_equal_1" = coin1=1 & coin2=1 ; -label "agree" = coin1=coin2 ; -label "finish_with_1" = pc1=3 & pc2=3 & coin1=1 & coin2=1 ; - -// rewards +module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule +label "finished" = pc1=3 &pc2=3 ; +label "all_coins_equal_1" = coin1=1 &coin2=1 ; rewards "steps" true : 1; endrewards + + diff --git a/examples/pmdp/consensus/coin2_7.nm b/examples/pmdp/consensus/coin2_7.nm new file mode 100644 index 000000000..8b86e2c6a --- /dev/null +++ b/examples/pmdp/consensus/coin2_7.nm @@ -0,0 +1,56 @@ +//Randomised Consensus Protocol + +mdp +const double p1; // in [0.2 , 0.8] +const double p2; // in [0.2 , 0.8] + + +const int N=2; +const int K=7; +const int range = 2*(K+1)*N; +const int counter_init = (K+1)*N; +const int left = N; +const int right = 2*(K+1)*N - N; + +// shared coin +global counter : [0..range] init counter_init; + +module process1 + + // program counter + pc1 : [0..3]; + // 0 - flip + // 1 - write + // 2 - check + // 3 - finished + + // local coin + coin1 : [0..1]; + + // flip coin + [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1); + // write tails -1 (reset coin to add regularity) + [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); + // write heads +1 (reset coin to add regularity) + [] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0); + // check + // decide tails + [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); + // decide heads + [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); + // flip again + [] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0); + // loop (all loop together when done) + [done] (pc1=3) -> (pc1'=3); + +endmodule + +module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule +label "finished" = pc1=3 &pc2=3 ; +label "all_coins_equal_1" = coin1=1 &coin2=1 ; +rewards "steps" + true : 1; +endrewards + + + diff --git a/examples/pmdp/consensus/coin2_8.nm b/examples/pmdp/consensus/coin2_8.nm index 9bc7e590c..81d9bf13c 100644 --- a/examples/pmdp/consensus/coin2_8.nm +++ b/examples/pmdp/consensus/coin2_8.nm @@ -1,9 +1,10 @@ -// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] -// gxn/dxp 20/11/00 +//Randomised Consensus Protocol mdp +const double p1; // in [0.2 , 0.8] +const double p2; // in [0.2 , 0.8] + -// constants const int N=2; const int K=8; const int range = 2*(K+1)*N; @@ -11,10 +12,6 @@ const int counter_init = (K+1)*N; const int left = N; const int right = 2*(K+1)*N - N; -//Coin Probabilities -const double p; -const double q; - // shared coin global counter : [0..range] init counter_init; @@ -31,35 +28,29 @@ module process1 coin1 : [0..1]; // flip coin - [] (pc1=0) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); + [] (pc1=0) -> p1 : (coin1'=0) & (pc1'=1) + 1 - p1 : (coin1'=1) & (pc1'=1); // write tails -1 (reset coin to add regularity) - [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); + [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); // write heads +1 (reset coin to add regularity) - [] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); + [] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0); // check // decide tails - [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); + [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); // decide heads - [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); + [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); // flip again - [] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); + [] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0); // loop (all loop together when done) - [done] (pc1=3) -> 1 : (pc1'=3); + [done] (pc1=3) -> (pc1'=3); endmodule -// construct remaining processes through renaming -module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule - -// labels -label "finished" = pc1=3 & pc2=3 ; -label "all_coins_equal_0" = coin1=0 & coin2=0 ; -label "all_coins_equal_1" = coin1=1 & coin2=1 ; -label "agree" = coin1=coin2 ; -label "finish_with_1" = pc1=3 & pc2=3 & coin1=1 & coin2=1 ; - -// rewards +module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule +label "finished" = pc1=3 &pc2=3 ; +label "all_coins_equal_1" = coin1=1 &coin2=1 ; rewards "steps" true : 1; endrewards + + diff --git a/examples/pmdp/consensus/coin4_2.nm b/examples/pmdp/consensus/coin4_2.nm deleted file mode 100644 index f0e534ee4..000000000 --- a/examples/pmdp/consensus/coin4_2.nm +++ /dev/null @@ -1,67 +0,0 @@ -// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] -// gxn/dxp 20/11/00 - -mdp - -// constants -const int N=4; -const int K=2; -const int range = 2*(K+1)*N; -const int counter_init = (K+1)*N; -const int left = N; -const int right = 2*(K+1)*N - N; - -//Coin Probabilities -const double p; -const double q; - -// shared coin -global counter : [0..range] init counter_init; - -module process1 - - // program counter - pc1 : [0..3]; - // 0 - flip - // 1 - write - // 2 - check - // 3 - finished - - // local coin - coin1 : [0..1]; - - // flip coin - [] (pc1=0) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); - // write tails -1 (reset coin to add regularity) - [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); - // write heads +1 (reset coin to add regularity) - [] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); - // check - // decide tails - [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); - // decide heads - [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); - // flip again - [] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); - // loop (all loop together when done) - [done] (pc1=3) -> 1 : (pc1'=3); - -endmodule - -// construct remaining processes through renaming -module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule -module process3 = process1[pc1=pc3,coin1=coin3] endmodule -module process4 = process1[pc1=pc4,coin1=coin4,p=q] endmodule - -// labels -label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 ; -label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 ; -label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 ; -label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 ; -label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 ; - -// rewards -rewards "steps" - true : 1; -endrewards - diff --git a/examples/pmdp/consensus/coin4_8.nm b/examples/pmdp/consensus/coin4_8.nm deleted file mode 100644 index 5acd2c6fa..000000000 --- a/examples/pmdp/consensus/coin4_8.nm +++ /dev/null @@ -1,67 +0,0 @@ -// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] -// gxn/dxp 20/11/00 - -mdp - -// constants -const int N=4; -const int K=8; -const int range = 2*(K+1)*N; -const int counter_init = (K+1)*N; -const int left = N; -const int right = 2*(K+1)*N - N; - -//Coin Probabilities -const double p; -const double q; - -// shared coin -global counter : [0..range] init counter_init; - -module process1 - - // program counter - pc1 : [0..3]; - // 0 - flip - // 1 - write - // 2 - check - // 3 - finished - - // local coin - coin1 : [0..1]; - - // flip coin - [] (pc1=0) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); - // write tails -1 (reset coin to add regularity) - [] (pc1=1) & (coin1=0) & (counter>0) -> 1 : (counter'=counter-1) & (pc1'=2) & (coin1'=0); - // write heads +1 (reset coin to add regularity) - [] (pc1=1) & (coin1=1) & (counter<range) -> 1 : (counter'=counter+1) & (pc1'=2) & (coin1'=0); - // check - // decide tails - [] (pc1=2) & (counter<=left) -> 1 : (pc1'=3) & (coin1'=0); - // decide heads - [] (pc1=2) & (counter>=right) -> 1 : (pc1'=3) & (coin1'=1); - // flip again - [] (pc1=2) & (counter>left) & (counter<right) -> 1 : (pc1'=0); - // loop (all loop together when done) - [done] (pc1=3) -> 1 : (pc1'=3); - -endmodule - -// construct remaining processes through renaming -module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule -module process3 = process1[pc1=pc3,coin1=coin3] endmodule -module process4 = process1[pc1=pc4,coin1=coin4,p=q] endmodule - -// labels -label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 ; -label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 ; -label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 ; -label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 ; -label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 ; - -// rewards -rewards "steps" - true : 1; -endrewards - diff --git a/examples/pmdp/consensus/coin6_2.nm b/examples/pmdp/consensus/coin6_2.nm deleted file mode 100644 index 471e4216e..000000000 --- a/examples/pmdp/consensus/coin6_2.nm +++ /dev/null @@ -1,69 +0,0 @@ -// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] -// gxn/dxp 20/11/00 - -mdp - -// constants -const int N=6; -const int K=2; -const int range = 2*(K+1)*N; -const int counter_init = (K+1)*N; -const int left = N; -const int right = 2*(K+1)*N - N; - -//Coin Probabilities -const double p; -const double q; - -// shared coin -global counter : [0..range] init counter_init; - -module process1 - - // program counter - pc1 : [0..3]; - // 0 - flip - // 1 - write - // 2 - check - // 3 - finished - - // local coin - coin1 : [0..1]; - - // flip coin - [] (pc1=0) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); - // write tails -1 (reset coin to add regularity) - [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); - // write heads +1 (reset coin to add regularity) - [] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0); - // check - // decide tails - [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); - // decide heads - [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); - // flip again - [] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0); - // loop (all loop together when done) - [done] (pc1=3) -> (pc1'=3); - -endmodule - -// construct remaining processes through renaming -module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule -module process3 = process1[pc1=pc3,coin1=coin3] endmodule -module process4 = process1[pc1=pc4,coin1=coin4,p=q] endmodule -module process5 = process1[pc1=pc5,coin1=coin5] endmodule -module process6 = process1[pc1=pc6,coin1=coin6,p=q] endmodule - -// labels -label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 ; -label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 & coin5=0 & coin6=0 ; -label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1 ; -label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 & coin4=coin5 & coin5=coin6 ; -label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1; - -// rewards -rewards "steps" - true : 1; -endrewards - diff --git a/examples/pmdp/consensus/coin6_8.nm b/examples/pmdp/consensus/coin6_8.nm deleted file mode 100644 index 7b322627d..000000000 --- a/examples/pmdp/consensus/coin6_8.nm +++ /dev/null @@ -1,70 +0,0 @@ -// COIN FLIPPING PROTOCOL FOR POLYNOMIAL RANDOMIZED CONSENSUS [AH90] -// gxn/dxp 20/11/00 - -mdp - -// constants -const int N=6; -const int K=8; -const int range = 2*(K+1)*N; -const int counter_init = (K+1)*N; -const int left = N; -const int right = 2*(K+1)*N - N; - -//Coin Probabilities -const double p; -const double q; - -// shared coin -global counter : [0..range] init counter_init; - -module process1 - - // program counter - pc1 : [0..3]; - // 0 - flip - // 1 - write - // 2 - check - // 3 - finished - - // local coin - coin1 : [0..1]; - - // flip coin - [] (pc1=0) -> p : (coin1'=0) & (pc1'=1) + 1-p : (coin1'=1) & (pc1'=1); - // write tails -1 (reset coin to add regularity) - [] (pc1=1) & (coin1=0) & (counter>0) -> (counter'=counter-1) & (pc1'=2) & (coin1'=0); - // write heads +1 (reset coin to add regularity) - [] (pc1=1) & (coin1=1) & (counter<range) -> (counter'=counter+1) & (pc1'=2) & (coin1'=0); - // check - // decide tails - [] (pc1=2) & (counter<=left) -> (pc1'=3) & (coin1'=0); - // decide heads - [] (pc1=2) & (counter>=right) -> (pc1'=3) & (coin1'=1); - // flip again - [] (pc1=2) & (counter>left) & (counter<right) -> (pc1'=0); - // loop (all loop together when done) - [done] (pc1=3) -> (pc1'=3); - -endmodule - -// construct remaining processes through renaming -module process2 = process1[pc1=pc2,coin1=coin2,p=q] endmodule -module process3 = process1[pc1=pc3,coin1=coin3] endmodule -module process4 = process1[pc1=pc4,coin1=coin4,p=q] endmodule -module process5 = process1[pc1=pc5,coin1=coin5] endmodule -module process6 = process1[pc1=pc6,coin1=coin6,p=q] endmodule - -// labels -label "finished" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 ; -label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3=0 & coin4=0 & coin5=0 & coin6=0 ; -label "all_coins_equal_1" = coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1 ; -label "agree" = coin1=coin2 & coin2=coin3 & coin3=coin4 & coin4=coin5 & coin5=coin6 ; -label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 ; -label "finish_with_1" = pc1=3 & pc2=3 & pc3=3 & pc4=3 & pc5=3 & pc6=3 & coin1=1 & coin2=1 & coin3=1 & coin4=1 & coin5=1 & coin6=1; - -// rewards -rewards "steps" - true : 1; -endrewards - diff --git a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp index 9b02c0c1d..4fa049b91 100644 --- a/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp +++ b/src/modelchecker/region/AbstractSparseRegionModelChecker.cpp @@ -194,7 +194,6 @@ namespace storm { STORM_LOG_THROW(this->getSpecifiedFormula()!=nullptr, storm::exceptions::InvalidStateException, "Tried to analyze a region although no property has been specified" ); STORM_LOG_DEBUG("Analyzing the region " << region.toString()); - //std::cout << "Analyzing the region " << region.toString() << std::endl; //switches for the different steps. bool done=false; @@ -203,7 +202,7 @@ namespace storm { bool doSampling=storm::settings::regionSettings().doSample(); bool doSmt=storm::settings::regionSettings().doSmt(); - if(!done && this->isResultConstant()){ + if(this->isResultConstant()){ STORM_LOG_DEBUG("Checking a region although the result is constant, i.e., independent of the region. This makes sense none."); if(this->valueIsInBoundOfFormula(this->getReachabilityValue(region.getSomePoint()))){ region.setCheckResult(RegionCheckResult::ALLSAT); @@ -435,6 +434,7 @@ namespace storm { } else{ outstream << "Simple model: " << this->getSimpleModel()->getNumberOfStates() << " states, " << this->getSimpleModel()->getNumberOfTransitions() << " transitions" << std::endl; + outstream << "Simple formula: " << *this->getSimpleFormula() << std::endl; } outstream << "Approximation is " << (this->isApproximationApplicable ? "" : "not ") << "applicable" << std::endl; outstream << "Number of checked regions: " << this->numOfCheckedRegions << std::endl; diff --git a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp index f89d4aec4..d74a1dbf8 100644 --- a/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseDtmcRegionModelChecker.cpp @@ -90,6 +90,10 @@ namespace storm { } else { preprocessForProbabilities(maybeStates, targetStates, isApproximationApplicable, constantResult); } + if(constantResult && constantResult.get()>=storm::utility::zero<ConstantType>()){ + //The result is already known. Nothing else to do here + return; + } 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); @@ -245,9 +249,10 @@ namespace storm { boost::optional<ConstantType>& constantResult) { STORM_LOG_DEBUG("Preprocessing for Dtmcs and reachability probabilities invoked."); //Get Target States - storm::logic::AtomicLabelFormula const& labelFormula = this->getSpecifiedFormula()->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().asAtomicLabelFormula(); storm::modelchecker::SparsePropositionalModelChecker<ParametricSparseModelType> modelChecker(this->getModel()); - std::unique_ptr<CheckResult> targetStatesResultPtr = modelChecker.checkAtomicLabelFormula(labelFormula); + std::unique_ptr<CheckResult> 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<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->getModel(), storm::storage::BitVector(this->getModel().getNumberOfStates(),true), targetStates); @@ -258,6 +263,7 @@ namespace storm { STORM_LOG_WARN("The probability of the initial state is constant (zero or one)"); this->reachabilityFunction = std::make_shared<ParametricType>(statesWithProbability01.first.get(initialState) ? storm::utility::zero<ParametricType>() : storm::utility::one<ParametricType>()); constantResult = statesWithProbability01.first.get(initialState) ? storm::utility::zero<ConstantType>() : storm::utility::one<ConstantType>(); + isApproximationApplicable = true; return; //nothing else to do... } //extend target states @@ -302,9 +308,10 @@ namespace storm { rewardModel=&(this->getModel().getUniqueRewardModel()->second); } //Get target states - storm::logic::AtomicLabelFormula const& labelFormula = this->getSpecifiedFormula()->asRewardOperatorFormula().getSubformula().asReachabilityRewardFormula().getSubformula().asAtomicLabelFormula(); - storm::modelchecker::SparsePropositionalModelChecker<ParametricSparseModelType> modelChecker(this->getModel()); - std::unique_ptr<CheckResult> targetStatesResultPtr= modelChecker.checkAtomicLabelFormula(labelFormula); + storm::modelchecker::SparsePropositionalModelChecker<ParametricSparseModelType> modelChecker(this->getModel()); + std::unique_ptr<CheckResult> 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); @@ -319,6 +326,7 @@ namespace storm { // In that case, we are going to throw in exception if the function is accessed (i.e. in getReachabilityFunction); this->reachabilityFunction = statesWithProbability1.get(initialState) ? std::make_shared<ParametricType>(storm::utility::zero<ParametricType>()) : nullptr; constantResult = statesWithProbability1.get(initialState) ? storm::utility::zero<ConstantType>() : storm::utility::infinity<ConstantType>(); + isApproximationApplicable = true; return; //nothing else to do... } //check if approximation is applicable and whether the result is constant diff --git a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp index a22615f16..2219abee2 100644 --- a/src/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -58,13 +58,13 @@ namespace storm { if (eventuallyFormula.getSubformula().isPropositionalFormula()) { return true; } - } else if (formula.isReachabilityRewardFormula()) { - storm::logic::ReachabilityRewardFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula(); - if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) { - return true; - } + // } else if (formula.isReachabilityRewardFormula()) { + // storm::logic::ReachabilityRewardFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula(); + // if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) { + // return true; + // } } - STORM_LOG_DEBUG("Region Model Checker could not handle (sub)formula " << formula); + STORM_LOG_DEBUG("Region Model Checker could not handle (sub)formula " << formula); return false; } @@ -77,7 +77,10 @@ namespace storm { 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<ConstantType>()){ + //The result is already known. Nothing else to do here + return; + } 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); @@ -198,9 +201,10 @@ namespace storm { boost::optional<ConstantType>& constantResult) { STORM_LOG_DEBUG("Preprocessing for Mdps and reachability probabilities invoked."); //Get Target States - storm::logic::AtomicLabelFormula const& labelFormula = this->getSpecifiedFormula()->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().asAtomicLabelFormula(); storm::modelchecker::SparsePropositionalModelChecker<ParametricSparseModelType> modelChecker(this->getModel()); - std::unique_ptr<CheckResult> targetStatesResultPtr = modelChecker.checkAtomicLabelFormula(labelFormula); + std::unique_ptr<CheckResult> 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. @@ -216,6 +220,7 @@ namespace storm { 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<ConstantType>() : storm::utility::one<ConstantType>(); + isApproximationApplicable = true; return; //nothing else to do... } //extend target states diff --git a/src/solver/GameSolver.cpp b/src/solver/GameSolver.cpp index 29201ad99..1e12f1dd5 100644 --- a/src/solver/GameSolver.cpp +++ b/src/solver/GameSolver.cpp @@ -4,6 +4,7 @@ #include "src/utility/solver.h" #include "src/storage/SparseMatrix.h" #include "src/utility/vector.h" +#include "src/utility/graph.h" namespace storm { namespace solver { @@ -34,10 +35,24 @@ namespace storm { selectedRows[pl1State] = player2Matrix.getRowGroupIndices()[pl2State] + (*initialPlayer2Policy)[pl2State]; } storm::storage::SparseMatrix<ValueType> eqSysMatrix = player2Matrix.selectRowsFromRowIndexSequence(selectedRows, true); - eqSysMatrix.convertToEquationSystem(); - std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = storm::utility::solver::LinearEquationSolverFactory<ValueType>().create(eqSysMatrix); std::vector<ValueType> subB(numberOfPlayer1States); storm::utility::vector::selectVectorValues<ValueType>(subB, selectedRows, b); + //depending on the choices, qualitative properties might have changed. + storm::storage::BitVector targetStates(subB.size(), false); + for(std::size_t index = 0; index < targetStates.size(); ++index){ + if(!storm::utility::isZero(subB[index])){ + targetStates.set(index); + } + } + auto prob01States = storm::utility::graph::performProb01(eqSysMatrix.transpose(), storm::storage::BitVector(targetStates.size(), true), targetStates); + for(auto const& probZeroState : prob01States.first){ + x[probZeroState] = storm::utility::zero<ValueType>(); + } + for(auto const& probZeroState : prob01States.second){ + x[probZeroState] = storm::utility::one<ValueType>(); + } + eqSysMatrix.convertToEquationSystem(); + std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = storm::utility::solver::LinearEquationSolverFactory<ValueType>().create(eqSysMatrix); solver->solveEquationSystem(x, subB); } diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index 793c1c3e3..a572f3e16 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -9,6 +9,7 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "utility/graph.h" namespace storm { namespace solver { @@ -49,13 +50,27 @@ namespace storm { if(initialPolicy != nullptr){ //Get initial values for x like it is done for policy iteration. storm::storage::SparseMatrix<ValueType> submatrix = this->A.selectRowsFromRowGroups(*initialPolicy, true); - submatrix.convertToEquationSystem(); - GmmxxLinearEquationSolver<ValueType> gmmLinearEquationSolver(submatrix); std::vector<ValueType> subB(rowGroupIndices.size() - 1); storm::utility::vector::selectVectorValues<ValueType>(subB, *initialPolicy, rowGroupIndices, b); + //depending on the choice, qualitative properties might have changed. + storm::storage::BitVector targetStates(subB.size(), false); + for(std::size_t index = 0; index < targetStates.size(); ++index){ + if(!storm::utility::isZero(subB[index])){ + targetStates.set(index); + } + } + auto prob01States = storm::utility::graph::performProb01(submatrix.transpose(), storm::storage::BitVector(targetStates.size(), true), targetStates); + for(auto const& probZeroState : prob01States.first){ + (*currentX)[probZeroState] = storm::utility::zero<ValueType>(); + } + for(auto const& probZeroState : prob01States.second){ + (*currentX)[probZeroState] = storm::utility::one<ValueType>(); + } + + submatrix.convertToEquationSystem(); + GmmxxLinearEquationSolver<ValueType> gmmLinearEquationSolver(submatrix); // Solve the resulting linear equation system - std::vector<ValueType> deterministicMultiplyResult(rowGroupIndices.size() - 1); - gmmLinearEquationSolver.solveEquationSystem(*currentX, subB, &deterministicMultiplyResult); + gmmLinearEquationSolver.solveEquationSystem(*currentX, subB); } uint_fast64_t iterations = 0; diff --git a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp index d4314d4de..a04414602 100644 --- a/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseMdpRegionModelCheckerTest.cpp @@ -72,7 +72,7 @@ TEST(SparseMdpRegionModelCheckerTest, two_dice_Prob) { TEST(SparseMdpRegionModelCheckerTest, coin_Prob) { std::string const& programFile = STORM_CPP_BASE_PATH "/examples/pmdp/consensus/coin2_2.nm"; - std::string const& formulaAsString = "P>0.25 [F \"finish_with_1\" ]"; + 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 @@ -91,9 +91,9 @@ TEST(SparseMdpRegionModelCheckerTest, coin_Prob) { modelchecker.specifyFormula(formulas[0]); //start testing - auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=p<=0.45,0.2<=q<=0.54"); - auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p<=0.65,0.5<=q<=0.7"); - auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p<=0.7,0.55<=q<=0.6"); + auto allSatRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.3<=p1<=0.45,0.2<=p2<=0.54"); + auto exBothRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::parseRegion("0.4<=p1<=0.65,0.5<=p2<=0.7"); + auto allVioRegion=storm::modelchecker::region::ParameterRegion<storm::RationalFunction>::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());