diff --git a/examples/pomdp/01-pomdps.py b/examples/pomdp/01-pomdps.py new file mode 100644 index 0000000..e05d4d8 --- /dev/null +++ b/examples/pomdp/01-pomdps.py @@ -0,0 +1,45 @@ +import stormpy +import stormpy.core +import stormpy.info + +import pycarl +import pycarl.core + +import stormpy.examples +import stormpy.examples.files + +import stormpy.pomdp + +import stormpy._config as config + + +def example_parametric_models_02(): + # Check support for parameters + if not config.storm_with_pars: + print("Support parameters is missing. Try building storm-pars.") + return + + import stormpy.pars + from pycarl.formula import FormulaType, Relation + if stormpy.info.storm_ratfunc_use_cln(): + import pycarl.cln.formula + else: + import pycarl.gmp.formula + + path = stormpy.examples.files.prism_pomdp_maze + prism_program = stormpy.parse_prism_program(path) + + formula_str = "P=? [\"goal\"]" + properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program) + pomdp = stormpy.build_model(prism_program, properties) + pomdp = stormpy.pomdp.make_canonic(pomdp) + pomdp = stormpy.pomdp.make_simple(pomdp) + memory_builder = stormpy.pomdp.PomdpMemoryBuilder() + memory = memory_builder.build(stormpy.pomdp.PomdpMemoryPattern.selective_counter, 2) + pomdp = stormpy.pomdp.unfold_memory(pomdp, memory) + pmc = stormpy.pomdp.apply_unknown_fsc(pomdp, stormpy.pomdp.PomdpFscApplicationMode.simple_linear) + + stormpy.export_parametric_to_drn(pmc, "test.out") + +if __name__ == '__main__': + example_parametric_models_02() diff --git a/lib/stormpy/pomdp/__init__.py b/lib/stormpy/pomdp/__init__.py index e1e1c97..00c7b95 100644 --- a/lib/stormpy/pomdp/__init__.py +++ b/lib/stormpy/pomdp/__init__.py @@ -2,7 +2,44 @@ from . import pomdp from .pomdp import * def make_canonic(model): + """ + Make the POMDP canonic + :param model: + :return: + """ + if model.supports_parameters: return pomdp._make_canonic_Rf(model) else: - return pomdp._make_canonic_Double(model) \ No newline at end of file + return pomdp._make_canonic_Double(model) + +def make_simple(model): + """ + 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, + + :param model: + :return: + """ + if model.supports_parameters: + return pomdp._make_simple_Rf(model) + else: + return pomdp._make_simple_Double(model) + +def unfold_memory(model, memory): + """ + Unfold the memory for an FSC into the POMDP + + :param model: A pomdp + :param memory: A memory structure + :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) + else: + return pomdp._unfold_memory_Double(model, memory) + +def apply_unknown_fsc(model, mode): + if model.supports_parameters: + return pomdp._apply_unknown_fsc_Rf(model, mode) + else: + return pomdp._apply_unknown_fsc_Double(model, mode) \ No newline at end of file diff --git a/src/mod_pomdp.cpp b/src/mod_pomdp.cpp index e318fda..4e86642 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 "pomdp/memory.h" #include PYBIND11_MODULE(pomdp, m) { @@ -16,6 +17,8 @@ PYBIND11_MODULE(pomdp, m) { define_tracker(m); define_qualitative_policy_search(m, "Double"); define_qualitative_policy_search_nt(m); + define_memory(m); + define_transformations_nt(m); define_transformations(m, "Double"); define_transformations(m, "Rf"); } diff --git a/src/pomdp/memory.cpp b/src/pomdp/memory.cpp new file mode 100644 index 0000000..3941f43 --- /dev/null +++ b/src/pomdp/memory.cpp @@ -0,0 +1,27 @@ +#include "memory.h" +#include "src/helpers.h" +#include + + +void define_memory(py::module& m) { + py::class_ memory(m, "PomdpMemory", "Memory for POMDP policies"); + memory.def_property_readonly("nr_states",&storm::storage::PomdpMemory::getNumberOfStates, "How many states does the memory structure have"); + + // Trivial, FixedCounter, SelectiveCounter, FixedRing, SelectiveRing, SettableBits, Full + py::enum_(m, "PomdpMemoryPattern", "Memory pattern for POMDP memory") + .value("trivial", storm::storage::PomdpMemoryPattern::Trivial) + .value("fixed_counter", storm::storage::PomdpMemoryPattern::FixedCounter) + .value("selective_counter", storm::storage::PomdpMemoryPattern::SelectiveCounter) + .value("fixed_ring", storm::storage::PomdpMemoryPattern::FixedRing) + .value("selective_ring", storm::storage::PomdpMemoryPattern::SelectiveRing) + .value("settable_bits", storm::storage::PomdpMemoryPattern::SettableBits) + .value("full", storm::storage::PomdpMemoryPattern::Full) + ; + + + py::class_ memorybuilder(m, "PomdpMemoryBuilder", "MemoryBuilder for POMDP policies"); + memorybuilder.def(py::init<>()); + memorybuilder.def("build", &storm::storage::PomdpMemoryBuilder::build, py::arg("pattern"), py::arg("nr_states")); + + +} \ No newline at end of file diff --git a/src/pomdp/memory.h b/src/pomdp/memory.h new file mode 100644 index 0000000..c47eb0d --- /dev/null +++ b/src/pomdp/memory.h @@ -0,0 +1,4 @@ +#pragma once +#include "common.h" + +void define_memory(py::module& m); diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp index d3834c0..9bbafd1 100644 --- a/src/pomdp/transformations.cpp +++ b/src/pomdp/transformations.cpp @@ -1,5 +1,8 @@ #include "transformations.h" #include +#include +#include +#include template std::shared_ptr> make_canonic(storm::models::sparse::Pomdp const& pomdp) { @@ -7,9 +10,41 @@ std::shared_ptr> make_canonic(storm::mod return makeCanonic.transform(); } +template +std::shared_ptr> unfold_memory(storm::models::sparse::Pomdp const& pomdp, storm::storage::PomdpMemory const& memory) { + storm::transformer::PomdpMemoryUnfolder unfolder(pomdp, memory); + return unfolder.transform(); +} + +template +std::shared_ptr> make_simple(storm::models::sparse::Pomdp const& pomdp) { + storm::transformer::BinaryPomdpTransformer transformer; + return transformer.transform(pomdp,true); +} + +template +std::shared_ptr> apply_unknown_fsc(storm::models::sparse::Pomdp const& pomdp, storm::transformer::PomdpFscApplicationMode const& applicationMode) { + storm::transformer::ApplyFiniteSchedulerToPomdp transformer(pomdp); + return transformer.transform(applicationMode); +} +// STANDARD, SIMPLE_LINEAR, SIMPLE_LINEAR_INVERSE, SIMPLE_LOG, FULL +void define_transformations_nt(py::module &m) { + py::enum_(m, "PomdpFscApplicationMode") + .value("standard", storm::transformer::PomdpFscApplicationMode::STANDARD) + .value("simple_linear", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR) + .value("simple_linear_inverse", storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR_INVERSE) + .value("simple_log", storm::transformer::PomdpFscApplicationMode::SIMPLE_LOG) + .value("full", storm::transformer::PomdpFscApplicationMode::FULL) + ; + +} + 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(("_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); } template void define_transformations(py::module& m, std::string const& vtSuffix); diff --git a/src/pomdp/transformations.h b/src/pomdp/transformations.h index b261e6d..4410946 100644 --- a/src/pomdp/transformations.h +++ b/src/pomdp/transformations.h @@ -2,5 +2,6 @@ #include "common.h" +void define_transformations_nt(py::module& m); template void define_transformations(py::module& m, std::string const& vtSuffix); diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp index 85d6074..a42aa2b 100644 --- a/src/storage/expressions.cpp +++ b/src/storage/expressions.cpp @@ -14,8 +14,6 @@ void define_expressions(py::module& m) { using Variable = storm::expressions::Variable; using Valuation = storm::expressions::Valuation; - - // ExpressionManager py::class_>(m, "ExpressionManager", "Manages variables for expressions") .def(py::init(), "Constructor")