From 75ad72a5747de2ca2567285d2dbd6006235198a2 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 24 Aug 2020 22:26:00 -0700 Subject: [PATCH 1/5] add_memory_labels for memory unfolding added --- lib/stormpy/pomdp/__init__.py | 6 +++--- src/pomdp/transformations.cpp | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/lib/stormpy/pomdp/__init__.py b/lib/stormpy/pomdp/__init__.py index 00c7b95..88bc23c 100644 --- a/lib/stormpy/pomdp/__init__.py +++ b/lib/stormpy/pomdp/__init__.py @@ -25,7 +25,7 @@ def make_simple(model): else: return pomdp._make_simple_Double(model) -def unfold_memory(model, memory): +def unfold_memory(model, memory, add_memory_labels=False): """ Unfold the memory for an FSC into the POMDP @@ -34,9 +34,9 @@ def unfold_memory(model, memory): :return: A pomdp that contains states from the product of the original POMDP and the FSC Memory """ if model.supports_parameters: - return pomdp._unfold_memory_Rf(model, memory) + return pomdp._unfold_memory_Rf(model, memory, add_memory_labels) else: - return pomdp._unfold_memory_Double(model, memory) + return pomdp._unfold_memory_Double(model, memory, add_memory_labels) def apply_unknown_fsc(model, mode): if model.supports_parameters: diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp index 9bbafd1..da18cbc 100644 --- a/src/pomdp/transformations.cpp +++ b/src/pomdp/transformations.cpp @@ -11,8 +11,8 @@ std::shared_ptr> make_canonic(storm::mod } template -std::shared_ptr> unfold_memory(storm::models::sparse::Pomdp const& pomdp, storm::storage::PomdpMemory const& memory) { - storm::transformer::PomdpMemoryUnfolder unfolder(pomdp, memory); +std::shared_ptr> unfold_memory(storm::models::sparse::Pomdp const& pomdp, storm::storage::PomdpMemory const& memory, bool addMemoryLabels) { + storm::transformer::PomdpMemoryUnfolder unfolder(pomdp, memory, addMemoryLabels); return unfolder.transform(); } @@ -42,7 +42,7 @@ void define_transformations_nt(py::module &m) { template void define_transformations(py::module& m, std::string const& vtSuffix) { m.def(("_make_canonic_" + vtSuffix).c_str(), &make_canonic, "Return a canonicly-ordered POMDP", py::arg("pomdp")); - m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure")); + m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"), py::arg("memorylabels") = false); m.def(("_make_simple_"+ vtSuffix).c_str(), &make_simple, "Make POMDP simple", py::arg("pomdp")); m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR); } From 7cee208518e777d2daa74b21a1cdb8b5587fb667 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 24 Aug 2020 23:41:57 -0700 Subject: [PATCH 2/5] keep state valuations --- lib/stormpy/pomdp/__init__.py | 12 ++++++------ src/pomdp/transformations.cpp | 12 ++++++------ 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/lib/stormpy/pomdp/__init__.py b/lib/stormpy/pomdp/__init__.py index 88bc23c..8f93f3e 100644 --- a/lib/stormpy/pomdp/__init__.py +++ b/lib/stormpy/pomdp/__init__.py @@ -13,7 +13,7 @@ def make_canonic(model): else: return pomdp._make_canonic_Double(model) -def make_simple(model): +def make_simple(model, keep_state_valuations=False): """ Make the POMDP simple (aka alternating), i.e., each state has at most two actions, and if there is nondeterminism, then there is no probabilistic branching, @@ -21,11 +21,11 @@ def make_simple(model): :return: """ if model.supports_parameters: - return pomdp._make_simple_Rf(model) + return pomdp._make_simple_Rf(model, keep_state_valuations) else: - return pomdp._make_simple_Double(model) + return pomdp._make_simple_Double(model, keep_state_valuations) -def unfold_memory(model, memory, add_memory_labels=False): +def unfold_memory(model, memory, add_memory_labels=False, keep_state_valuations=False): """ Unfold the memory for an FSC into the POMDP @@ -34,9 +34,9 @@ def unfold_memory(model, memory, add_memory_labels=False): :return: A pomdp that contains states from the product of the original POMDP and the FSC Memory """ if model.supports_parameters: - return pomdp._unfold_memory_Rf(model, memory, add_memory_labels) + return pomdp._unfold_memory_Rf(model, memory, add_memory_labels, keep_state_valuations) else: - return pomdp._unfold_memory_Double(model, memory, add_memory_labels) + return pomdp._unfold_memory_Double(model, memory, add_memory_labels, keep_state_valuations) def apply_unknown_fsc(model, mode): if model.supports_parameters: diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp index da18cbc..7fd2287 100644 --- a/src/pomdp/transformations.cpp +++ b/src/pomdp/transformations.cpp @@ -11,15 +11,15 @@ std::shared_ptr> make_canonic(storm::mod } template -std::shared_ptr> unfold_memory(storm::models::sparse::Pomdp const& pomdp, storm::storage::PomdpMemory const& memory, bool addMemoryLabels) { - storm::transformer::PomdpMemoryUnfolder unfolder(pomdp, memory, addMemoryLabels); +std::shared_ptr> unfold_memory(storm::models::sparse::Pomdp const& pomdp, storm::storage::PomdpMemory const& memory, bool addMemoryLabels, bool keepStateValuations) { + storm::transformer::PomdpMemoryUnfolder unfolder(pomdp, memory, addMemoryLabels, keepStateValuations); return unfolder.transform(); } template -std::shared_ptr> make_simple(storm::models::sparse::Pomdp const& pomdp) { +std::shared_ptr> make_simple(storm::models::sparse::Pomdp const& pomdp, bool keepStateValuations) { storm::transformer::BinaryPomdpTransformer transformer; - return transformer.transform(pomdp,true); + return transformer.transform(pomdp,true, keepStateValuations); } template @@ -42,8 +42,8 @@ void define_transformations_nt(py::module &m) { template void define_transformations(py::module& m, std::string const& vtSuffix) { m.def(("_make_canonic_" + vtSuffix).c_str(), &make_canonic, "Return a canonicly-ordered POMDP", py::arg("pomdp")); - m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"), py::arg("memorylabels") = false); - m.def(("_make_simple_"+ vtSuffix).c_str(), &make_simple, "Make POMDP simple", py::arg("pomdp")); + m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"), py::arg("memorylabels") = false, py::arg("keep_state_valuations")=false); + m.def(("_make_simple_"+ vtSuffix).c_str(), &make_simple, "Make POMDP simple", py::arg("pomdp"), py::arg("keep_state_valuations")=false); m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR); } From 694904b4c2f19dabbf87bded95cf11851f023b04 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 26 Aug 2020 21:50:42 -0700 Subject: [PATCH 3/5] convenience functions on prism programs --- src/storage/prism.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp index 7f057a0..0e96e6c 100644 --- a/src/storage/prism.cpp +++ b/src/storage/prism.cpp @@ -44,6 +44,10 @@ void define_prism(py::module& m) { .def_property_readonly("hasUndefinedConstants", &Program::hasUndefinedConstants, "Does the program have undefined constants?") .def_property_readonly("isDeterministicModel", &Program::isDeterministicModel, "Does the program describe a deterministic model?") .def_property_readonly("expression_manager", &Program::getManager, "Get the expression manager for expressions in this program") + .def("get_synchronizing_action_indices", &Program::getSynchronizingActionIndices, "Get the synchronizing action indices") + .def("get_action_name", &Program::getActionName, py::arg("action_index"), "Get the action name for a given action index") + .def("get_module_indices_by_action_index", &Program::getModuleIndicesByActionIndex, py::arg("action_index"), "get all modules that have a particular action index") + .def_property_readonly("number_of_unlabeled_commands", &Program::getNumberOfUnlabeledCommands, "Gets the number of commands that are not labelled") .def("flatten", &Program::flattenModules, "Put program into a single module", py::arg("smt_factory")=std::shared_ptr(new storm::utility::solver::SmtSolverFactory())) .def("to_jani", [](storm::prism::Program const& program, std::vector const& properties, bool allVariablesGlobal, std::string suffix) { return program.toJani(properties, allVariablesGlobal, suffix); @@ -63,6 +67,7 @@ void define_prism(py::module& m) { .def_property_readonly("boolean_variables", &Module::getBooleanVariables, "All boolean Variables of this module") .def("get_integer_variable", &Module::getIntegerVariable, py::arg("variable_name")) .def("get_boolean_variable", &Module::getBooleanVariable, py::arg("variable_name")) + .def("get_command_indices_by_action_index", &Module::getCommandIndicesByActionIndex, py::arg("action_index")) .def("__str__", &streamToString) ; From 92268776fdd6449294346c67f3454de4f5175331 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 2 Sep 2020 09:22:32 -0700 Subject: [PATCH 4/5] set seed for the simulator after initialization --- lib/stormpy/simulator.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/lib/stormpy/simulator.py b/lib/stormpy/simulator.py index 4ef7433..28e26e9 100644 --- a/lib/stormpy/simulator.py +++ b/lib/stormpy/simulator.py @@ -99,6 +99,9 @@ class SparseSimulator(Simulator): self._state_valuations = None self.set_full_observability(self._model.model_type != stormpy.storage.ModelType.POMDP) + def set_seed(self, value): + self._engine.set_seed(value) + def available_actions(self): if self._action_mode == SimulatorActionMode.INDEX_LEVEL: return range(self.nr_available_actions()) From 642779e56f48ab8354af86ae41d1b64d039d1e2e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 2 Sep 2020 20:11:38 -0700 Subject: [PATCH 5/5] precision for native solver --- src/core/environment.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/core/environment.cpp b/src/core/environment.cpp index c44c3ed..2e23f97 100644 --- a/src/core/environment.cpp +++ b/src/core/environment.cpp @@ -52,6 +52,7 @@ void define_environment(py::module& m) { py::class_(m, "NativeSolverEnvironment", "Environment for Native solvers") .def_property("method", &storm::NativeSolverEnvironment::getMethod, [](storm::NativeSolverEnvironment& nsenv, storm::solver::NativeLinearEquationSolverMethod const& m) {nsenv.setMethod(m);}) .def_property("maximum_iterations", &storm::NativeSolverEnvironment::getMaximalNumberOfIterations, [](storm::NativeSolverEnvironment& nsenv, uint64_t iters) {nsenv.setMaximalNumberOfIterations(iters);} ) + .def_property("precision", &storm::NativeSolverEnvironment::getPrecision, &storm::NativeSolverEnvironment::setPrecision) ; py::class_(m, "MinMaxSolverEnvironment", "Environment for Min-Max-Solvers")