Bindings for intervals

lib/stormpy/__init__.py

@@ -216,6 +216,22 @@ def build_parametric_model_from_drn(file, options = DirectEncodingParserOptions(
     return _convert_sparse_model(intermediate, parametric=True)
 
 
+def build_interval_model_from_drn(file, options = DirectEncodingParserOptions()):
+    """
+    Build an interval model in sparse representation from the explicit DRN representation.
+
+    :param String file: DRN file containing the model.
+    :param DirectEncodingParserOptions: Options for the parser.
+    :return: Interval model in sparse representation.
+    """
+    intermediate = core._build_sparse_interval_model_from_drn(file, options)
+    assert intermediate.supports_uncertainty
+    if intermediate.model_type == ModelType.MDP:
+        return intermediate._as_sparse_imdp()
+    else:
+        raise StormError("Not supported interval model constructed")
+
+
 def perform_bisimulation(model, properties, bisimulation_type):
     """
     Perform bisimulation on model.
@@ -300,7 +316,9 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched
         if force_fully_observable:
             # Note that casting a model to a fully observable model wont work with python/pybind, so we actually have other access points
             if model.supports_parameters:
-                raise NotImplementedError("")
+                raise NotImplementedError("Model checking of partially observable models is not supported for parametric models.")
+            elif model.supports_uncertainty:
+                raise NotImplementedError("Model checking of partially observable models is not supported for interval models.")
             elif model.is_exact:
                 task = core.ExactCheckTask(formula, only_initial_states)
                 task.set_produce_schedulers(extract_scheduler)
@@ -600,11 +618,11 @@ def parse_properties(properties, context=None, filters=None):
         if context.is_prism_program():
             return core.parse_properties_for_prism_program(properties, context.as_prism_program(), filters)
         else:
-            core.parse_properties_for_jani_program(properties, context.as_jani_model(), filters)
+            return core.parse_properties_for_jani_program(properties, context.as_jani_model(), filters)
     elif type(context) == storage.PrismProgram:
         return core.parse_properties_for_prism_program(properties, context, filters)
     elif type(context) == storage.JaniModel:
-        core.parse_properties_for_jani_model(properties, context, filters)
+        return core.parse_properties_for_jani_model(properties, context, filters)
     else:
         raise StormError("Unclear context. Please pass a symbolic model description")
 
@@ -619,6 +637,8 @@ def export_to_drn(model, file, options=DirectEncodingOptions()):
     """
     if model.supports_parameters:
         return core._export_parametric_to_drn(model, file, options)
+    if model.supports_uncertainty:
+        return core._export_to_drn_interval(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/examples/files/imdp/tiny-01.drn

@@ -0,0 +1,20 @@
+@type: MDP
+@parameters
+
+@reward_models
+
+@nr_states
+3
+@nr_choices
+3
+@model
+state 0 init
+	action 0
+		1 : [0.4, 0.9]
+		2 : [0.5, 0.8]
+state 1 target
+	action 0
+		1 : [1, 1]
+state 2
+	action 0
+		2 : [1, 1]

lib/stormpy/storage/__init__.py

@@ -77,5 +77,7 @@ def get_maximal_end_components(model):
         return stormpy.jMaximalEndComponentDecomposition_ratfunc(model)
     elif model.is_exact:
         return stormpy.MaximalEndComponentDecomposition_exact(model)
+    elif model.supports_uncertainty:
+        return stormpy.MaximalEndComponentDecomposition_interval(model)
     else:
         return stormpy.MaximalEndComponentDecomposition_double(model)

src/core/core.cpp

@@ -128,6 +128,7 @@ void define_build(py::module& m) {
     m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
     m.def("_build_sparse_exact_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalNumber>, "Build the model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
     m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
+    m.def("_build_sparse_interval_model_from_drn", &storm::api::buildExplicitDRNModel<storm::Interval>, "Build the interval model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
     m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel<double>, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = "");
 
     m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr);
@@ -191,8 +192,8 @@ void define_export(py::module& m) {
     opts.def(py::init<>());
     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_to_drn_interval", &exportDRN<storm::Interval>, "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/core/modelchecking.cpp

@@ -1,5 +1,8 @@
 #include "modelchecking.h"
 #include "result.h"
+#include "storm/api/verification.h"
+#include "storm/environment/Environment.h"
+#include "storm/environment/solver/MinMaxSolverEnvironment.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
 #include "storm/modelchecker/results/CheckResult.h"
 #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
@@ -46,6 +49,11 @@ std::shared_ptr<storm::modelchecker::CheckResult> modelCheckingHybridEngine(std:
     return storm::api::verifyWithHybridEngine<DdType, ValueType>(env, model, task);
 }
 
+std::shared_ptr<storm::modelchecker::CheckResult> checkIntervalMdp(std::shared_ptr<storm::models::sparse::Mdp<storm::Interval>> mdp, CheckTask<double> const& task, storm::Environment& env) {
+    auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::Interval>>(*mdp);
+    return checker.check(env, task);
+}
+
 std::vector<double> computeAllUntilProbabilities(storm::Environment const& env, CheckTask<double> const& task, std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
     storm::solver::SolveGoal<double> goal(*ctmc, task);
     return storm::modelchecker::helper::SparseCtmcCslHelper::computeAllUntilProbabilities(env, std::move(goal), ctmc->getTransitionMatrix(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates);
@@ -55,7 +63,6 @@ std::vector<double> computeTransientProbabilities(storm::Environment const& env,
     return storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities(env, ctmc->getTransitionMatrix(), ctmc->getInitialStates(), phiStates, psiStates, ctmc->getExitRateVector(), timeBound);
 }
 
-
 // Thin wrapper for computing prob01 states
 template<typename ValueType>
 std::pair<storm::storage::BitVector, storm::storage::BitVector> computeProb01(storm::models::sparse::Dtmc<ValueType> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
@@ -100,6 +107,7 @@ void define_modelchecking(py::module& m) {
         .def(py::init<storm::logic::Formula const&, bool>(), py::arg("formula"), py::arg("only_initial_states") = false)
         .def("set_produce_schedulers", &CheckTask<double>::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true)
         .def("set_hint", &CheckTask<double>::setHint, "Sets a hint that may speed up the solver")
+        .def("set_robust_uncertainty", &CheckTask<double>::setRobustUncertainty, "Sets whether robust uncertainty should be considered")
     ;
     // CheckTask
     py::class_<CheckTask<storm::RationalNumber>, std::shared_ptr<CheckTask<storm::RationalNumber>>>(m, "ExactCheckTask", "Task for model checking with exact numbers")
@@ -141,6 +149,7 @@ void define_modelchecking(py::module& m) {
     m.def("_parametric_model_checking_dd_engine", &modelCheckingDdEngine<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Perform parametric model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment());
     m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine<storm::dd::DdType::Sylvan, double>, "Perform model checking using the hybrid engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment());
     m.def("_parametric_model_checking_hybrid_engine", &modelCheckingHybridEngine<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Perform parametric model checking using the hybrid engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment());
+    m.def("check_interval_mdp", &checkIntervalMdp, "Check interval MDP");
     m.def("compute_all_until_probabilities", &computeAllUntilProbabilities, "Compute forward until probabilities");
     m.def("compute_transient_probabilities", &computeTransientProbabilities, "Compute transient probabilities");
     m.def("_compute_prob01states_double", &computeProb01<double>, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states"));

src/mod_storage.cpp

@@ -34,36 +34,44 @@ PYBIND11_MODULE(storage, m) {
     define_model(m);
     define_sparse_model<double>(m, "");
     define_sparse_model<storm::RationalNumber>(m, "Exact");
+    define_sparse_model<storm::Interval>(m, "Interval");
     define_sparse_parametric_model(m);
     define_statevaluation(m);
     define_simplevaluation(m);
     define_sparse_matrix<double>(m, "");
     define_sparse_matrix<storm::RationalNumber>(m, "Exact");
+    define_sparse_matrix<storm::Interval>(m, "Interval");
     define_sparse_matrix<storm::RationalFunction>(m, "Parametric");
     define_sparse_matrix_nt(m);
     define_symbolic_model<storm::dd::DdType::Sylvan>(m, "Sylvan");
     define_state<double>(m, "");
     define_state<storm::RationalNumber>(m, "Exact");
+    define_state<storm::Interval>(m, "Interval");
     define_state<storm::RationalFunction>(m, "Parametric");
     define_prism(m);
     define_jani(m);
     define_jani_transformers(m);
     define_labeling(m);
     define_origins(m);
     define_expressions(m);
-    define_scheduler<double>(m, "Double");
+    define_scheduler<double>(m, "");
     define_scheduler<storm::RationalNumber>(m, "Exact");
+    define_scheduler<storm::Interval>(m, "Interval");
     define_scheduler<storm::RationalFunction>(m, "Parametric");
-    define_distribution<double>(m, "Double");
+    define_distribution<double>(m, "");
+    define_distribution<storm::RationalNumber>(m, "Exact");
+    define_distribution<storm::Interval>(m, "Interval");
     define_sparse_model_components<double>(m, "");
     define_sparse_model_components<storm::RationalNumber>(m, "Exact");
+    define_sparse_model_components<storm::Interval>(m, "Interval");
     define_sparse_model_components<storm::RationalFunction>(m, "Parametric");
     define_geometry<double>(m, "Double");
     define_geometry<storm::RationalNumber>(m, "Exact");
 
     define_maximal_end_components(m);
     define_maximal_end_component_decomposition<double>(m, "_double");
     define_maximal_end_component_decomposition<storm::RationalNumber>(m, "_exact");
+    define_maximal_end_component_decomposition<storm::Interval>(m, "_interval");
     define_maximal_end_component_decomposition<storm::RationalFunction>(m, "_ratfunc");
 
 }

src/storage/bitvector.cpp

@@ -21,6 +21,7 @@ void define_bitvector(py::module& m) {
         .def("set", [](BitVector& b, uint_fast64_t i, bool v) {
                 b.set(i, v);
             }, py::arg("index"), py::arg("value") = true, "Set")
+        .def("as_int", &BitVector::getAsInt, py::arg("index"), py::arg("no_bits"), "Get as unsigned int")
 
         .def("__len__", [](BitVector const& b) { return b.size(); })
         .def("__getitem__", [](BitVector const& b, uint_fast64_t i) {
@@ -49,7 +50,9 @@ void define_bitvector(py::module& m) {
         .def(py::self |= py::self)
 
         .def("__str__", &streamToString<BitVector>)
-
+        .def("__hash__", [](const BitVector &b) {
+                return storm::storage::Murmur3BitVectorHash<uint64_t>()(b);
+            })
     ;
 
 }

src/storage/decomposition.cpp

@@ -36,4 +36,5 @@ void define_maximal_end_component_decomposition(py::module& m, std::string const
 
 template void define_maximal_end_component_decomposition<double>(py::module& m, std::string const& vt_suffix);
 template void define_maximal_end_component_decomposition<storm::RationalNumber>(py::module& m, std::string const& vt_suffix);
+template void define_maximal_end_component_decomposition<storm::Interval>(py::module& m, std::string const& vt_suffix);
 template void define_maximal_end_component_decomposition<storm::RationalFunction>(py::module& m, std::string const& vt_suffix);

src/storage/distribution.cpp

@@ -17,3 +17,4 @@ void define_distribution(py::module& m, std::string vt_suffix) {
 
 template void define_distribution<double>(py::module&, std::string vt_suffix);
 template void define_distribution<storm::RationalNumber>(py::module&, std::string vt_suffix);
+template void define_distribution<storm::Interval>(py::module&, std::string vt_suffix);

src/storage/matrix.cpp

@@ -131,5 +131,6 @@ void define_sparse_matrix(py::module& m, std::string const& vtSuffix) {
 
 template void define_sparse_matrix<double>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_matrix<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
+template void define_sparse_matrix<storm::Interval>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_matrix<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
 

src/storage/model.cpp

@@ -147,6 +147,9 @@ void define_model(py::module& m) {
         .def("_as_sparse_pmdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparseMdp<RationalFunction>>();
             }, "Get model as sparse pMDP")
+        .def("_as_sparse_imdp", [](ModelBase &modelbase) {
+                return modelbase.as<SparseMdp<storm::Interval>>();
+            }, "Get model as sparse interval MDP")
         .def("_as_sparse_pomdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparsePomdp<double>>();
             }, "Get model as sparse POMDP")
@@ -200,14 +203,16 @@ void define_sparse_model(py::module& m, std::string const& vtSuffix) {
     // Models with double numbers
     py::class_<SparseModel<ValueType>, std::shared_ptr<SparseModel<ValueType>>, ModelBase> model(m, ("_Sparse" + vtSuffix + "Model").c_str(),
                                                                                            "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix");
-    model.def_property_readonly("labeling", &getLabeling<ValueType>, "Labels")
+    model.def_property_readonly("supports_uncertainty", &SparseModel<ValueType>::supportsUncertainty, "Flag whether model supports uncertainty via intervals")
+        .def_property_readonly("labeling", &getLabeling<ValueType>, "Labels")
         .def("has_choice_labeling", [](SparseModel<ValueType> const& model) {return model.hasChoiceLabeling();}, "Does the model have an associated choice labelling?")
         .def_property_readonly("choice_labeling", [](SparseModel<ValueType> const& model) {return model.getChoiceLabeling();}, "get choice labelling")
         .def("has_choice_origins", [](SparseModel<ValueType> const& model) {return model.hasChoiceOrigins();}, "has choice origins?")
         .def_property_readonly("choice_origins", [](SparseModel<ValueType> const& model) {return model.getChoiceOrigins();})
         .def("labels_state", &SparseModel<ValueType>::getLabelsOfState, py::arg("state"), "Get labels of state")
         .def_property_readonly("initial_states", &getSparseInitialStates<ValueType>, "Initial states")
         .def_property_readonly("initial_states_as_bitvector", [](SparseModel<ValueType> const& model) {return model.getInitialStates();})
+        .def("set_initial_states", &SparseModel<ValueType>::setInitialStates, py::arg("states"), "Set initial states")
         .def_property_readonly("states", [](SparseModel<ValueType>& model) {
                 return SparseModelStates<ValueType>(model);
             }, "Get states")
@@ -453,3 +458,4 @@ void define_symbolic_model(py::module& m, std::string vt_suffix) {
 template void define_symbolic_model<storm::dd::DdType::Sylvan>(py::module& m, std::string vt_suffix);
 template void define_sparse_model<double>(py::module& m, std::string const& vt_suffix);
 template void define_sparse_model<storm::RationalNumber>(py::module& m, std::string const& vt_suffix);
+template void define_sparse_model<storm::Interval>(py::module& m, std::string const& vt_suffix);

src/storage/model.h

@@ -7,6 +7,7 @@ void define_model(py::module& m);
 template<typename ValueType>
 void define_sparse_model(py::module& m, std::string const& vtSuffix);
 void define_sparse_parametric_model(py::module& m);
+void define_sparse_interval_model(py::module& m);
 
 template<storm::dd::DdType DdType>
 void define_symbolic_model(py::module& m, std::string vt_suffix);

src/storage/model_components.cpp

@@ -54,4 +54,5 @@ void define_sparse_model_components(py::module& m, std::string const& vtSuffix)
 
 template void define_sparse_model_components<double>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_model_components<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
-template void define_sparse_model_components<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
+template void define_sparse_model_components<storm::Interval>(py::module& m, std::string const& vtSuffix);
+template void define_sparse_model_components<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);