diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 039b11b..e9fac64 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -36,6 +36,8 @@ def _convert_sparse_model(model, parametric=False): return model._as_sparse_pdtmc() elif model.model_type == ModelType.MDP: return model._as_sparse_pmdp() + elif model.model_type == ModelType.POMDP: + return model._as_sparse_ppomdp() elif model.model_type == ModelType.CTMC: return model._as_sparse_pctmc() elif model.model_type == ModelType.MA: diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index 59e1f00..177bf2f 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -37,6 +37,8 @@ prism_mdp_maze = _path("mdp", "maze_2.nm") """Prism example for the maze MDP""" prism_pomdp_maze = _path("pomdp", "maze_2.prism") """Prism example for the maze POMDP""" +prism_par_pomdp_maze = _path("pomdp", "maze_2_par.prism") +"""Prism example for the parametric POMDP""" dft_galileo_hecs = _path("dft", "hecs.dft") """DFT example for HECS (Galileo format)""" dft_json_and = _path("dft", "and.json") diff --git a/lib/stormpy/examples/files/pomdp/maze_2_par.prism b/lib/stormpy/examples/files/pomdp/maze_2_par.prism new file mode 100644 index 0000000..12408fb --- /dev/null +++ b/lib/stormpy/examples/files/pomdp/maze_2_par.prism @@ -0,0 +1,142 @@ + + +// maze example (POMDP) +// slightly extends that presented in +// Littman, Cassandra and Kaelbling +// Learning policies for partially observable environments: Scaling up +// Technical Report CS, Brown University +// gxn 29/01/16 + +// state space (value of variable "s") + +// 0 1 2 3 4 +// 5 6 7 +// 8 9 10 +// 11 13 12 + +// 13 is the target + +pomdp + +// can observe the walls and target +observables + o +endobservables +// o=0 - observation in initial state +// o=1 - west and north walls (s0) +// o=2 - north and south walls (s1 and s3) +// o=3 - north wall (s2) +// o=4 - east and north way (s4) +// o=5 - east and west walls (s5, s6, s7, s8, s9 and s10) +// o=6 - east, west and south walls (s11 and s12) +// o=7 - the target (s13) + +const double p; + +module maze + + s : [-1..13]; + o : [0..7]; + + // initialisation + [] s=-1 -> 1/13 : (s'=0) & (o'=1) + + 1/13 : (s'=1) & (o'=2) + + 1/13 : (s'=2) & (o'=3) + + 1/13 : (s'=3) & (o'=2) + + 1/13 : (s'=4) & (o'=4) + + 1/13 : (s'=5) & (o'=5) + + 1/13 : (s'=6) & (o'=5) + + 1/13 : (s'=7) & (o'=5) + + 1/13 : (s'=8) & (o'=5) + + 1/13 : (s'=9) & (o'=5) + + 1/13 : (s'=10) & (o'=5) + + 1/13 : (s'=11) & (o'=6) + + 1/13 : (s'=12) & (o'=6); + + // moving around the maze + + [east] s=0 -> (s'=1) & (o'=2); + [west] s=0 -> (s'=0); + [north] s=0 -> (s'=0); + [south] s=0 -> (s'=5) & (o'=5); + + [east] s=1 -> (s'=2) & (o'=3); + [west] s=1 -> (s'=0) & (o'=1); + [north] s=1 -> (s'=1); + [south] s=1 -> (s'=1); + + [east] s=2 -> (s'=3) & (o'=2); + [west] s=2 -> (s'=1) & (o'=2); + [north] s=2 -> (s'=2); + [south] s=2 -> (s'=6) & (o'=5); + + [east] s=3 -> (s'=4) & (o'=4); + [west] s=3 -> (s'=2) & (o'=3); + [north] s=3 -> (s'=3); + [south] s=3 -> (s'=3); + + [east] s=4 -> (s'=4); + [west] s=4 -> (s'=3) & (o'=2); + [north] s=4 -> (s'=4); + [south] s=4 -> (s'=7) & (o'=5); + + [east] s=5 -> (s'=5); + [west] s=5 -> (s'=5); + [north] s=5 -> (s'=0) & (o'=1); + [south] s=5 -> (s'=8); + + [east] s=6 -> (s'=6); + [west] s=6 -> (s'=6); + [north] s=6 -> (s'=2) & (o'=3); + [south] s=6 -> (s'=9); + + [east] s=7 -> (s'=7); + [west] s=7 -> (s'=7); + [north] s=7 -> (s'=4) & (o'=4); + [south] s=7 -> (s'=10); + + [east] s=8 -> (s'=8); + [west] s=8 -> (s'=8); + [north] s=8 -> (s'=5); + [south] s=8 -> (s'=11) & (o'=6); + + [east] s=9 -> (s'=9); + [west] s=9 -> (s'=9); + [north] s=9 -> (s'=6); + [south] s=9 -> p: (s'=13) & (o'=7) + (1-p):(s'=9); + + [east] s=10 -> (s'=10); + [west] s=10 -> (s'=10); + [north] s=10 -> (s'=7); + [south] s=10 -> (s'=12) & (o'=6); + + [east] s=11 -> (s'=11); + [west] s=11 -> (s'=11); + [north] s=11 -> (s'=8) & (o'=5); + [south] s=11 -> (s'=11); + + [east] s=12 -> (s'=12); + [west] s=12 -> (s'=12); + [north] s=12 -> (s'=10) & (o'=5); + [south] s=12 -> (s'=12); + + // loop when we reach the target + [done] s=13 -> true; + +endmodule + +// reward structure (number of steps to reach the target) +rewards + + [east] true : 1; + [west] true : 1; + [north] true : 1; + [south] true : 1; + +endrewards + +// target observation +label "goal" = o=7; +label "bad" = o=6; + + diff --git a/lib/stormpy/pomdp/__init__.py b/lib/stormpy/pomdp/__init__.py index c27a6d0..e1e1c97 100644 --- a/lib/stormpy/pomdp/__init__.py +++ b/lib/stormpy/pomdp/__init__.py @@ -2,4 +2,7 @@ from . import pomdp from .pomdp import * def make_canonic(model): - return pomdp._make_canonic_Double(model) \ No newline at end of file + if model.supports_parameters: + return pomdp._make_canonic_Rf(model) + else: + return pomdp._make_canonic_Double(model) \ No newline at end of file diff --git a/src/mod_pomdp.cpp b/src/mod_pomdp.cpp index d507824..e318fda 100644 --- a/src/mod_pomdp.cpp +++ b/src/mod_pomdp.cpp @@ -4,6 +4,7 @@ #include "pomdp/tracker.h" #include "pomdp/qualitative_analysis.h" #include "pomdp/transformations.h" +#include PYBIND11_MODULE(pomdp, m) { m.doc() = "Functionality for POMDP analysis"; @@ -16,4 +17,5 @@ PYBIND11_MODULE(pomdp, m) { define_qualitative_policy_search(m, "Double"); define_qualitative_policy_search_nt(m); define_transformations(m, "Double"); + define_transformations(m, "Rf"); } diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp index db0e77a..d3834c0 100644 --- a/src/pomdp/transformations.cpp +++ b/src/pomdp/transformations.cpp @@ -13,3 +13,4 @@ void define_transformations(py::module& m, std::string const& vtSuffix) { } template void define_transformations(py::module& m, std::string const& vtSuffix); +template void define_transformations(py::module& m, std::string const& vtSuffix); \ No newline at end of file diff --git a/src/storage/model.cpp b/src/storage/model.cpp index b978c51..4fd4d0d 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -124,6 +124,9 @@ void define_model(py::module& m) { .def("_as_sparse_pomdp", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse POMDP") + .def("_as_sparse_ppomdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse pPOMDP") .def("_as_sparse_ctmc", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse CTMC") @@ -261,11 +264,20 @@ void define_sparse_model(py::module& m) { py::class_, std::shared_ptr>>(m, "SparseParametricDtmc", "pDTMC in sparse representation", modelRatFunc) .def("__str__", &getModelInfoPrinter) ; - py::class_, std::shared_ptr>>(m, "SparseParametricMdp", "pMDP in sparse representation", modelRatFunc) - .def_property_readonly("nondeterministic_choice_indices", [](SparseMdp const& mdp) { return mdp.getNondeterministicChoiceIndices(); }) + py::class_, std::shared_ptr>> pmdp(m, "SparseParametricMdp", "pMDP in sparse representation", modelRatFunc); + pmdp.def_property_readonly("nondeterministic_choice_indices", [](SparseMdp const& mdp) { return mdp.getNondeterministicChoiceIndices(); }) .def("apply_scheduler", [](SparseMdp const& mdp, storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { return mdp.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true) .def("__str__", &getModelInfoPrinter) ; + + py::class_, std::shared_ptr>>(m, "SparseParametricPomdp", "POMDP in sparse representation", pmdp) + .def(py::init>(), py::arg("other_model")) + .def("__str__", &getModelInfoPrinter) + .def("get_observation", &SparsePomdp::getObservation, py::arg("state")) + .def_property_readonly("observations", &SparsePomdp::getObservations) + .def_property_readonly("nr_observations", &SparsePomdp::getNrObservations) + ; + py::class_, std::shared_ptr>>(m, "SparseParametricCtmc", "pCTMC in sparse representation", modelRatFunc) .def("__str__", &getModelInfoPrinter) ;