Add bindings for quantitative POMDP analysis (#125)

* Add bindings for quantitative POMDP analysis

* Add check if Storm was built with POMDP support

* Increase required Storm version

lib/stormpy/examples/files/pomdp/maze-concise.prism

@@ -0,0 +1,85 @@
+pomdp
+
+// 3 | x x x x x
+// 2 | x   x   x
+// 1 | x   x   x
+// 0 | x   x   x
+// y ____________
+//   x 0 1 2 3 4
+
+// can go in this direction
+formula u = y<3;
+formula r = y=3 & x<4;
+formula d = y>0 & (x=0 | x=2 | x=4);
+formula l = y=3 & x>0;
+
+// target cell
+formula goal = x=2 & y=0;
+formula bad = (x=0 | x=4) & y=0;
+
+// updates of coordinates (if possible)
+formula yu = u ? (y+1) : y;
+formula xr = r ? (x+1) : x;
+formula yd = d ? (y-1) : y;
+formula xl = l ? (x-1) : x;
+
+// corresponding observables
+observable "u" = clk=1 & u;
+observable "r" = clk=1 & r;
+observable "d" = clk=1 & d;
+observable "l" = clk=1 & l;
+observable "goal" = goal;
+observable "bad" = bad;
+
+
+// modules
+
+module clock
+    // 0 - init, 1 - drive
+    clk : [0..1] init 0;
+
+    // random placement
+    [place] clk=0 -> (clk'=1);
+
+    // drive
+    [up] 	clk=1 -> true;
+    [right] clk=1 -> true;
+    [down] 	clk=1 -> true;
+    [left]  clk=1 -> true;
+endmodule
+
+module maze
+
+	x : [0..4] init 0;
+    y : [0..3] init 0;
+
+	// initialisation
+	[place] true ->
+          1/13 :    (x'=0)&(y'=0)
+        + 1/13 :    (x'=0)&(y'=1)
+		+ 1/13 :    (x'=0)&(y'=2)
+		+ 1/13 :    (x'=0)&(y'=3)
+		+ 1/13 :    (x'=1)&(y'=3)
+		+ 1/13 :    (x'=2)&(y'=0)
+		+ 1/13 :    (x'=2)&(y'=1)
+		+ 1/13 :    (x'=2)&(y'=2)
+		+ 1/13 :    (x'=2)&(y'=3)
+		+ 1/13 :    (x'=3)&(y'=3)
+		+ 1/13 :    (x'=4)&(y'=1)
+		+ 1/13 :    (x'=4)&(y'=2)
+		+ 1/13 :    (x'=4)&(y'=3);
+
+	// moving around the maze (all combinations)
+
+    [up]        true -> 0.8: (y'=yu) + 0.08: (x'=xr) + 0.08: (x'=xl) + 0.04: (y'=yd);
+    [right]     true -> 0.8: (x'=xr) + 0.08: (y'=yu) + 0.08: (y'=yd) + 0.04: (x'=xl);
+    [down]      true -> 0.8: (y'=yd) + 0.08: (x'=xr) + 0.08: (x'=xl) + 0.04: (y'=yu);
+    [left]      true -> 0.8: (x'=xl) + 0.08: (y'=yu) + 0.08: (y'=yd) + 0.04: (x'=xr);
+
+endmodule
+
+// rewards
+
+rewards "steps"
+	clk=1: 1;
+endrewards

setup.py

@@ -13,7 +13,7 @@
     sys.exit('Sorry, Python 2.x is not supported')
 
 # Minimal storm version required
-storm_min_version = "1.8.0"
+storm_min_version = "1.8.2"
 
 # Get the long description from the README file
 with open(os.path.join(os.path.abspath(os.path.dirname(__file__)), 'README.md'), encoding='utf-8') as f:

src/mod_pomdp.cpp

@@ -5,6 +5,7 @@
 #include "pomdp/qualitative_analysis.h"
 #include "pomdp/transformations.h"
 #include "pomdp/memory.h"
+#include "pomdp/quantitative_analysis.h"
 #include <storm/adapters/RationalFunctionAdapter.h>
 
 PYBIND11_MODULE(pomdp, m) {
@@ -22,6 +23,7 @@ PYBIND11_MODULE(pomdp, m) {
     define_transformations_nt(m);
     define_transformations<double>(m, "Double");
     define_transformations<storm::RationalNumber>(m, "Exact");
+    define_belief_exploration<double>(m, "Double");
 
     define_transformations<storm::RationalFunction>(m, "Rf");
 }

src/pomdp/quantitative_analysis.cpp

@@ -0,0 +1,61 @@
+#include "quantitative_analysis.h"
+#include <storm/models/sparse/Pomdp.h>
+#include <storm-pomdp/api/verification.h>
+
+template<typename ValueType> using Pomdp = storm::models::sparse::Pomdp<ValueType, typename storm::models::sparse::StandardRewardModel<ValueType>>;
+template<typename ValueType> using BeliefExplorationPomdpModelChecker = typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<Pomdp<ValueType>, ValueType, ValueType>;
+template<typename ValueType> using BeliefExplorationPomdpModelCheckerResult = typename storm::pomdp::modelchecker::BeliefExplorationPomdpModelChecker<ValueType>::Result;
+template<typename ValueType> using Options = storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions<ValueType>;
+template<typename ValueType> using additionalCutoffValueType = std::vector<std::vector<std::unordered_map<uint64_t, ValueType>>>;
+
+
+template<typename ValueType>
+void define_belief_exploration(py::module& m, std::string const& vtSuffix) {
+    py::class_<BeliefExplorationPomdpModelChecker<ValueType>> belmc(m, ("BeliefExplorationModelChecker" + vtSuffix).c_str());
+    belmc.def(py::init<std::shared_ptr<Pomdp<ValueType>>, Options<ValueType>>(), py::arg("model"), py::arg("options"));
+
+    belmc.def("check", py::overload_cast<storm::logic::Formula const&,additionalCutoffValueType<ValueType> const&>(&BeliefExplorationPomdpModelChecker<ValueType>::check), py::arg("formula"), py::arg("cutoff_values"));
+    belmc.def("check_with_preprocessing_environment", py::overload_cast<storm::logic::Formula const&, storm::Environment const&, additionalCutoffValueType<ValueType> const&>(&BeliefExplorationPomdpModelChecker<ValueType>::check), py::arg("formula"), py::arg("pre_processing_environment"), py::arg("cutoff_values"));
+    belmc.def("check_with_environment", py::overload_cast<storm::Environment const&, storm::logic::Formula const&, additionalCutoffValueType<ValueType> const&>(&BeliefExplorationPomdpModelChecker<ValueType>::check), py::arg("environment"), py::arg("formula"), py::arg("cutoff_values"));
+    belmc.def("check_with_environment_and_pre_processing_environment", py::overload_cast<storm::Environment const&, storm::logic::Formula const&, storm::Environment const&, additionalCutoffValueType<ValueType> const&>(&BeliefExplorationPomdpModelChecker<ValueType>::check), py::arg("environment"), py::arg("formula"), py::arg("pre_processing_environment"), py::arg("cutoff_values"));
+
+    belmc.def("pause_unfolding", &BeliefExplorationPomdpModelChecker<ValueType>::pauseUnfolding);
+    belmc.def("continue_unfolding", &BeliefExplorationPomdpModelChecker<ValueType>::continueUnfolding);
+    belmc.def("terminate_unfolding", &BeliefExplorationPomdpModelChecker<ValueType>::terminateUnfolding);
+    belmc.def("is_result_ready", &BeliefExplorationPomdpModelChecker<ValueType>::isResultReady);
+    belmc.def("is_exploring", &BeliefExplorationPomdpModelChecker<ValueType>::isExploring);
+    belmc.def("get_interactive_result", &BeliefExplorationPomdpModelChecker<ValueType>::getInteractiveResult);
+    belmc.def("get_status", &BeliefExplorationPomdpModelChecker<ValueType>::getStatus);
+    belmc.def("get_interactive_belief_explorer", &BeliefExplorationPomdpModelChecker<ValueType>::getInteractiveBeliefExplorer);
+    belmc.def("has_converged", &BeliefExplorationPomdpModelChecker<ValueType>::hasConverged);
+
+    py::class_<typename storm::builder::BeliefMdpExplorer<Pomdp<ValueType>, ValueType>> belmdpexpl(m, ("BeliefMdpExplorer" + vtSuffix).c_str());
+    belmdpexpl.def("set_fsc_values", &storm::builder::BeliefMdpExplorer<Pomdp<ValueType>, ValueType>::setFMSchedValueList, py::arg("value_list"));
+
+    py::class_<Options<ValueType>> belexploptions(m, ("BeliefExplorationModelCheckerOptions" + vtSuffix).c_str());
+    belexploptions.def(py::init<bool, bool>(), py::arg("discretize"), py::arg("unfold"));
+    belexploptions.def_readwrite("use_state_elimination_cutoff", &Options<ValueType>::useStateEliminationCutoff);
+    belexploptions.def_readwrite("size_threshold_init", &Options<ValueType>::sizeThresholdInit);
+    belexploptions.def_readwrite("use_clipping", &Options<ValueType>::useClipping);
+    belexploptions.def_readwrite("exploration_time_limit", &Options<ValueType>::explorationTimeLimit);
+    belexploptions.def_readwrite("clipping_grid_res", &Options<ValueType>::clippingGridRes);
+    belexploptions.def_readwrite("gap_threshold_init", &Options<ValueType>::gapThresholdInit);
+    belexploptions.def_readwrite("size_threshold_factor", &Options<ValueType>::sizeThresholdFactor);
+    belexploptions.def_readwrite("refine_precision", &Options<ValueType>::refinePrecision);
+    belexploptions.def_readwrite("refine_step_limit", &Options<ValueType>::refineStepLimit);
+    belexploptions.def_readwrite("refine", &Options<ValueType>::refine);
+    belexploptions.def_readwrite("exploration_heuristic", &Options<ValueType>::explorationHeuristic);
+    belexploptions.def_readwrite("skip_heuristic_schedulers", &Options<ValueType>::skipHeuristicSchedulers);
+    belexploptions.def_readwrite("interactive_unfolding", &Options<ValueType>::interactiveUnfolding);
+    belexploptions.def_readwrite("cut_zero_gap", &Options<ValueType>::cutZeroGap);
+
+    py::class_<typename BeliefExplorationPomdpModelChecker<ValueType>::Result> belexplres(m, ("BeliefExplorationPomdpModelCheckerResult" + vtSuffix).c_str());
+    belexplres.def_readonly("induced_mc_from_scheduler", &BeliefExplorationPomdpModelChecker<ValueType>::Result::schedulerAsMarkovChain);
+    belexplres.def_readonly("cutoff_schedulers", &BeliefExplorationPomdpModelChecker<ValueType>::Result::cutoffSchedulers);
+    belexplres.def_readonly("lower_bound", &BeliefExplorationPomdpModelChecker<ValueType>::Result::lowerBound);
+    belexplres.def_readonly("upper_bound", &BeliefExplorationPomdpModelChecker<ValueType>::Result::upperBound);
+
+    m.def("create_interactive_mc", &storm::pomdp::api::createInteractiveUnfoldingModelChecker<ValueType>, py::arg("env"), py::arg("pomdp"), py::arg("use_clipping"));
+}
+
+template void define_belief_exploration<double>(py::module& m, std::string const& vtSuffix);

src/pomdp/quantitative_analysis.h

@@ -0,0 +1,5 @@
+#pragma once
+#include "common.h"
+
+template<typename VT>
+void define_belief_exploration(py::module& m, std::string const& vtSuffix);

tests/configurations.py

@@ -8,6 +8,7 @@
 has_gspn = config.storm_with_gspn
 has_pars = config.storm_with_pars
 has_spot = config.storm_with_spot
+has_pomdp = config.storm_with_pomdp
 
 try:
     import numpy
@@ -31,6 +32,7 @@
 dft = pytest.mark.skipif(not has_dft, reason="No support for DFTs")
 gspn = pytest.mark.skipif(not has_gspn, reason="No support for GSPNs")
 pars = pytest.mark.skipif(not has_pars, reason="No support for parametric model checking")
+pomdp = pytest.mark.skipif(not has_pomdp, reason="No support for POMDPs")
 spot = pytest.mark.skipif(not has_spot, reason="No support for LTL via spot")
 numpy_avail = pytest.mark.skipif(not has_numpy, reason="Numpy not available")
 plotting = pytest.mark.skipif(not has_matplotlib or not has_scipy, reason="Libraries for plotting not available")

tests/pomdp/conftest.py

@@ -0,0 +1,4 @@
+from configurations import has_pomdp
+
+if has_pomdp:
+    import stormpy.pomdp

tests/pomdp/test_pomdp_quantitative_analysis.py

@@ -0,0 +1,60 @@
+import stormpy
+
+from configurations import pomdp
+
+from helpers.helper import get_example_path
+
+import math
+
+@pomdp
+class TestPomdpQuantitative:
+    def test_underapprox_mc_maze_pmax(self):
+        program = stormpy.parse_prism_program(get_example_path("pomdp", "maze_2.prism"))
+        formulas = stormpy.parse_properties_for_prism_program("Pmax=? [ !\"bad\" U \"goal\" ]", program)
+        model = stormpy.build_model(program, formulas)
+        model = stormpy.pomdp.make_canonic(model)
+        options = stormpy.pomdp.BeliefExplorationModelCheckerOptionsDouble(False, True)
+        options.use_state_elimination_cutoff = False
+        options.size_threshold_init = 10
+        options.use_clipping = False
+        belmc = stormpy.pomdp.BeliefExplorationModelCheckerDouble(model, options)
+        result = belmc.check(formulas[0].raw_formula, [])
+        assert math.isclose(result.lower_bound, 0.351985, abs_tol=10**-6)
+        assert math.isinf(result.upper_bound)
+        assert result.induced_mc_from_scheduler.nr_states == 10
+        assert result.induced_mc_from_scheduler.nr_transitions == 23
+        assert len(result.cutoff_schedulers) == 4
+
+    def test_underapprox_mc_maze_rmin(self):
+        program = stormpy.parse_prism_program(get_example_path("pomdp", "maze_2.prism"))
+        formulas = stormpy.parse_properties_for_prism_program("Rmin=? [ F \"goal\" ]", program)
+        model = stormpy.build_model(program, formulas)
+        model = stormpy.pomdp.make_canonic(model)
+        options = stormpy.pomdp.BeliefExplorationModelCheckerOptionsDouble(False, True)
+        options.use_state_elimination_cutoff = False
+        options.size_threshold_init = 10
+        options.use_clipping = False
+        belmc = stormpy.pomdp.BeliefExplorationModelCheckerDouble(model, options)
+        result = belmc.check(formulas[0].raw_formula, [])
+        assert math.isinf(result.lower_bound)
+        assert math.isclose(result.upper_bound, 12.270484, abs_tol=10**-6)
+        assert result.induced_mc_from_scheduler.nr_states == 9
+        assert result.induced_mc_from_scheduler.nr_transitions == 17
+        assert len(result.cutoff_schedulers) == 3
+
+    def test_underapprox_mc_cmaze_rmin(self):
+        program = stormpy.parse_prism_program(get_example_path("pomdp", "maze-concise.prism"))
+        formulas = stormpy.parse_properties_for_prism_program("R{\"steps\"}min=? [F ((x = 2) & (y = 0))]", program)
+        model = stormpy.build_model(program, formulas)
+        model = stormpy.pomdp.make_canonic(model)
+        options = stormpy.pomdp.BeliefExplorationModelCheckerOptionsDouble(False, True)
+        options.use_state_elimination_cutoff = False
+        options.size_threshold_init = 10
+        options.use_clipping = False
+        belmc = stormpy.pomdp.BeliefExplorationModelCheckerDouble(model, options)
+        result = belmc.check(formulas[0].raw_formula, [])
+        assert math.isinf(result.lower_bound)
+        assert math.isclose(result.upper_bound, 19.781437, abs_tol=10**-6)
+        assert result.induced_mc_from_scheduler.nr_states == 9
+        assert result.induced_mc_from_scheduler.nr_transitions == 15
+        assert len(result.cutoff_schedulers) == 3