From 84dca993d264078696a37097c2f787253472f08a Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 26 Sep 2020 11:57:10 -0700 Subject: [PATCH] updates in the monitoring API --- CHANGELOG.md | 1 + lib/stormpy/__init__.py | 14 ++++++++++++++ lib/stormpy/pomdp/__init__.py | 13 ++++++++++--- src/core/core.cpp | 6 +++--- src/pomdp/tracker.cpp | 9 ++++++++- 5 files changed, 36 insertions(+), 7 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index c602295..8cedadf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,7 @@ Version 1.6.x ### Version 1.6.3 (to be released) - Support for exact arithmetic in models +- `export_parametric_to_drn` no longer exists, use `export_to_drn` instead ### Version 1.6.2 (2020/09) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 90a5f3c..c47377c 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -515,3 +515,17 @@ def parse_properties(properties, context=None, filters=None): core.parse_properties_for_jani_model(properties, context, filters) else: raise StormError("Unclear context. Please pass a symbolic model description") + +def export_to_drn(model, file, options=DirectEncodingOptions()): + """ + Export a model to DRN format + :param model: The model + :param file: A path + :param options: DirectEncodingOptions + :return: + """ + if model.supports_parameters: + return core._export_parametric_to_drn(model, file, options) + if model.is_exact: + return core._export_exact_to_drn(model, file, options) + return core._export_to_drn(model, file, options) \ No newline at end of file diff --git a/lib/stormpy/pomdp/__init__.py b/lib/stormpy/pomdp/__init__.py index a258c1c..d490e77 100644 --- a/lib/stormpy/pomdp/__init__.py +++ b/lib/stormpy/pomdp/__init__.py @@ -45,16 +45,23 @@ def apply_unknown_fsc(model, mode): return pomdp._apply_unknown_fsc_Double(model, mode) -def create_nondeterminstic_belief_tracker(model): +def create_nondeterminstic_belief_tracker(model, reduction_timeout, track_timeout): """ :param model: A POMDP + :param reduction_timeout: timeout in milliseconds for the reduction algorithm, 0 for no timeout. :return: """ if model.is_exact: - return pomdp.NondeterministicBeliefTrackerExactSparse(model) + opts = NondeterministicBeliefTrackerExactSparseOptions() + opts.reduction_timeout = reduction_timeout + opts.track_timeout = track_timeout + return pomdp.NondeterministicBeliefTrackerExactSparse(model, opts) else: - return pomdp.NondeterministicBeliefTrackerDoubleSparse(model) + opts = NondeterministicBeliefTrackerDoubleSparseOptions() + opts.reduction_timeout = reduction_timeout + opts.track_timeout = track_timeout + return pomdp.NondeterministicBeliefTrackerDoubleSparse(model, opts) def create_observation_trace_unfolder(model, risk_assessment, expr_manager): diff --git a/src/core/core.cpp b/src/core/core.cpp index dc01e13..ebf10f8 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -169,7 +169,7 @@ void define_export(py::module& m) { opts.def_readwrite("allow_placeholders", &storm::exporter::DirectEncodingOptions::allowPlaceholders); // Export // TODO make one export_to_drn that infers which of the folliwng to use. - m.def("export_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions()); - m.def("export_exact_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions()); - m.def("export_parametric_to_drn", &exportDRN, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions()); + m.def("_export_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions()); + m.def("_export_exact_to_drn", &exportDRN, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions()); + m.def("_export_parametric_to_drn", &exportDRN, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions()); } diff --git a/src/pomdp/tracker.cpp b/src/pomdp/tracker.cpp index 468d9aa..3e072db 100644 --- a/src/pomdp/tracker.cpp +++ b/src/pomdp/tracker.cpp @@ -29,8 +29,14 @@ void define_tracker(py::module& m, std::string const& vtSuffix) { // dbel.def_property_readonly("risk", &storm::generator::ObservationDenseBeliefState::getRisk); // dbel.def("__str__", &storm::generator::ObservationDenseBeliefState::toString); + py::class_::Options> opts(m, ("NondeterministicBeliefTracker" + vtSuffix + "SparseOptions").c_str(), "Options for the corresponding tracker"); + opts.def(py::init<>()); + opts.def_readwrite("track_timeout", &NDPomdpTrackerSparse::Options::trackTimeOut); + opts.def_readwrite("reduction_timeout", &NDPomdpTrackerSparse::Options::timeOut); + opts.def_readwrite("reduction_wiggle", &NDPomdpTrackerSparse::Options::wiggle); + py::class_> ndetbelieftracker(m, ("NondeterministicBeliefTracker" + vtSuffix + "Sparse").c_str(), "Tracker for belief states and uncontrollable actions"); - ndetbelieftracker.def(py::init const&>(), py::arg("pomdp")); + ndetbelieftracker.def(py::init const&, typename NDPomdpTrackerSparse::Options>(), py::arg("pomdp"), py::arg("options")); ndetbelieftracker.def("reset", &NDPomdpTrackerSparse::reset); ndetbelieftracker.def("set_risk", &NDPomdpTrackerSparse::setRisk, py::arg("risk")); ndetbelieftracker.def("obtain_current_risk",&NDPomdpTrackerSparse::getCurrentRisk, py::arg("max")=true); @@ -40,6 +46,7 @@ void define_tracker(py::module& m, std::string const& vtSuffix) { ndetbelieftracker.def("dimension", &NDPomdpTrackerSparse::getCurrentDimension); ndetbelieftracker.def("obtain_last_observation", &NDPomdpTrackerSparse::getCurrentObservation); ndetbelieftracker.def("reduce",&NDPomdpTrackerSparse::reduce); + ndetbelieftracker.def("reduction_timed_out", &NDPomdpTrackerSparse::hasTimedOut); // py::class_> ndetbelieftrackerd(m, "NondeterministicBeliefTrackerDoubleDense", "Tracker for belief states and uncontrollable actions"); // ndetbelieftrackerd.def(py::init const&>(), py::arg("pomdp"));