updates in the monitoring API

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)

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)

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):

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<double>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions());
-    m.def("export_exact_to_drn", &exportDRN<double>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions());
-    m.def("export_parametric_to_drn", &exportDRN<storm::RationalFunction>, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions());
+    m.def("_export_to_drn", &exportDRN<double>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions());
+    m.def("_export_exact_to_drn", &exportDRN<storm::RationalNumber>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions());
+    m.def("_export_parametric_to_drn", &exportDRN<storm::RationalFunction>, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions());
 }

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<double>::getRisk);
 //    dbel.def("__str__", &storm::generator::ObservationDenseBeliefState<double>::toString);
 
+    py::class_<typename NDPomdpTrackerSparse<ValueType>::Options> opts(m, ("NondeterministicBeliefTracker" + vtSuffix + "SparseOptions").c_str(), "Options for the corresponding tracker");
+    opts.def(py::init<>());
+    opts.def_readwrite("track_timeout", &NDPomdpTrackerSparse<ValueType>::Options::trackTimeOut);
+    opts.def_readwrite("reduction_timeout", &NDPomdpTrackerSparse<ValueType>::Options::timeOut);
+    opts.def_readwrite("reduction_wiggle", &NDPomdpTrackerSparse<ValueType>::Options::wiggle);
+
     py::class_<NDPomdpTrackerSparse<ValueType>> ndetbelieftracker(m, ("NondeterministicBeliefTracker" + vtSuffix + "Sparse").c_str(), "Tracker for belief states and uncontrollable actions");
-    ndetbelieftracker.def(py::init<SparsePomdp<ValueType> const&>(), py::arg("pomdp"));
+    ndetbelieftracker.def(py::init<SparsePomdp<ValueType> const&, typename NDPomdpTrackerSparse<ValueType>::Options>(), py::arg("pomdp"), py::arg("options"));
     ndetbelieftracker.def("reset", &NDPomdpTrackerSparse<ValueType>::reset);
     ndetbelieftracker.def("set_risk", &NDPomdpTrackerSparse<ValueType>::setRisk, py::arg("risk"));
     ndetbelieftracker.def("obtain_current_risk",&NDPomdpTrackerSparse<ValueType>::getCurrentRisk, py::arg("max")=true);
@@ -40,6 +46,7 @@ void define_tracker(py::module& m, std::string const& vtSuffix) {
     ndetbelieftracker.def("dimension", &NDPomdpTrackerSparse<ValueType>::getCurrentDimension);
     ndetbelieftracker.def("obtain_last_observation", &NDPomdpTrackerSparse<ValueType>::getCurrentObservation);
     ndetbelieftracker.def("reduce",&NDPomdpTrackerSparse<ValueType>::reduce);
+    ndetbelieftracker.def("reduction_timed_out", &NDPomdpTrackerSparse<ValueType>::hasTimedOut);
 
 //    py::class_<NDPomdpTrackerDense<double>> ndetbelieftrackerd(m, "NondeterministicBeliefTrackerDoubleDense", "Tracker for belief states and uncontrollable actions");
 //    ndetbelieftrackerd.def(py::init<SparsePomdp<double> const&>(), py::arg("pomdp"));