From be6638a5a49ae4e212d18bcea90bd066b5b9c49f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 21 Sep 2023 14:07:35 +0200 Subject: [PATCH 1/5] Bindings for interval models --- lib/stormpy/__init__.py | 6 +++++- lib/stormpy/storage/__init__.py | 2 ++ src/core/core.cpp | 2 +- src/core/modelchecking.cpp | 12 +++++++++++- src/mod_storage.cpp | 8 ++++++++ src/storage/decomposition.cpp | 1 + src/storage/distribution.cpp | 1 + src/storage/matrix.cpp | 1 + src/storage/model.cpp | 4 +++- src/storage/model.h | 1 + src/storage/model_components.cpp | 3 ++- src/storage/scheduler.cpp | 4 +++- src/storage/state.cpp | 1 + 13 files changed, 40 insertions(+), 6 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 7bfebb041..d3c7e881b 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -300,7 +300,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) @@ -619,6 +621,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) diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 383501d20..5a79b4b23 100644 --- a/lib/stormpy/storage/__init__.py +++ b/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) diff --git a/src/core/core.cpp b/src/core/core.cpp index ceeb5cdc9..fa4481201 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -191,8 +191,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, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions()); + m.def("_export_to_drn_interval", &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/core/modelchecking.cpp b/src/core/modelchecking.cpp index 6b31567f6..c85ee58c3 100644 --- a/src/core/modelchecking.cpp +++ b/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,12 @@ std::shared_ptr modelCheckingHybridEngine(std: return storm::api::verifyWithHybridEngine(env, model, task); } +std::shared_ptr checkIntervalMdp(std::shared_ptr> mdp, CheckTask const& task, storm::Environment& env) { + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(*mdp); + return checker.check(env, task); +} + std::vector computeAllUntilProbabilities(storm::Environment const& env, CheckTask const& task, std::shared_ptr> ctmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { storm::solver::SolveGoal goal(*ctmc, task); return storm::modelchecker::helper::SparseCtmcCslHelper::computeAllUntilProbabilities(env, std::move(goal), ctmc->getTransitionMatrix(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates); @@ -55,7 +64,6 @@ std::vector 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 std::pair computeProb01(storm::models::sparse::Dtmc const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { @@ -100,6 +108,7 @@ void define_modelchecking(py::module& m) { .def(py::init(), py::arg("formula"), py::arg("only_initial_states") = false) .def("set_produce_schedulers", &CheckTask::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true) .def("set_hint", &CheckTask::setHint, "Sets a hint that may speed up the solver") + .def("set_robust_uncertainty", &CheckTask::setRobustUncertainty, "Sets whether robust uncertainty should be considered") ; // CheckTask py::class_, std::shared_ptr>>(m, "ExactCheckTask", "Task for model checking with exact numbers") @@ -141,6 +150,7 @@ void define_modelchecking(py::module& m) { m.def("_parametric_model_checking_dd_engine", &modelCheckingDdEngine, "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, "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, "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, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index 97e7a9287..e8b97eb50 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -34,16 +34,19 @@ PYBIND11_MODULE(storage, m) { define_model(m); define_sparse_model(m, ""); define_sparse_model(m, "Exact"); + define_sparse_model(m, "Interval"); define_sparse_parametric_model(m); define_statevaluation(m); define_simplevaluation(m); define_sparse_matrix(m, ""); define_sparse_matrix(m, "Exact"); + define_sparse_matrix(m, "Interval"); define_sparse_matrix(m, "Parametric"); define_sparse_matrix_nt(m); define_symbolic_model(m, "Sylvan"); define_state(m, ""); define_state(m, "Exact"); + define_state(m, "Interval"); define_state(m, "Parametric"); define_prism(m); define_jani(m); @@ -53,10 +56,14 @@ PYBIND11_MODULE(storage, m) { define_expressions(m); define_scheduler(m, "Double"); define_scheduler(m, "Exact"); +// define_scheduler(m, "Interval"); define_scheduler(m, "Parametric"); define_distribution(m, "Double"); + define_distribution(m, "Exact"); + define_distribution(m, "Interval"); define_sparse_model_components(m, ""); define_sparse_model_components(m, "Exact"); + define_sparse_model_components(m, "Interval"); define_sparse_model_components(m, "Parametric"); define_geometry(m, "Double"); define_geometry(m, "Exact"); @@ -64,6 +71,7 @@ PYBIND11_MODULE(storage, m) { define_maximal_end_components(m); define_maximal_end_component_decomposition(m, "_double"); define_maximal_end_component_decomposition(m, "_exact"); + define_maximal_end_component_decomposition(m, "_interval"); define_maximal_end_component_decomposition(m, "_ratfunc"); } diff --git a/src/storage/decomposition.cpp b/src/storage/decomposition.cpp index 0e900cc6c..7c4e2a4f1 100644 --- a/src/storage/decomposition.cpp +++ 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(py::module& m, std::string const& vt_suffix); template void define_maximal_end_component_decomposition(py::module& m, std::string const& vt_suffix); +template void define_maximal_end_component_decomposition(py::module& m, std::string const& vt_suffix); template void define_maximal_end_component_decomposition(py::module& m, std::string const& vt_suffix); diff --git a/src/storage/distribution.cpp b/src/storage/distribution.cpp index 07b692f45..590322a79 100644 --- a/src/storage/distribution.cpp +++ b/src/storage/distribution.cpp @@ -17,3 +17,4 @@ void define_distribution(py::module& m, std::string vt_suffix) { template void define_distribution(py::module&, std::string vt_suffix); template void define_distribution(py::module&, std::string vt_suffix); +template void define_distribution(py::module&, std::string vt_suffix); diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index aec56d54f..7f4651c45 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -131,5 +131,6 @@ void define_sparse_matrix(py::module& m, std::string const& vtSuffix) { template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); +template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); template void define_sparse_matrix(py::module& m, std::string const& vtSuffix); diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 2e5c99533..d498ec430 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -200,7 +200,8 @@ void define_sparse_model(py::module& m, std::string const& vtSuffix) { // Models with double numbers py::class_, std::shared_ptr>, 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, "Labels") + model.def_property_readonly("supports_uncertainty", &SparseModel::supportsUncertainty, "Flag whether model supports uncertainty via intervals") + .def_property_readonly("labeling", &getLabeling, "Labels") .def("has_choice_labeling", [](SparseModel const& model) {return model.hasChoiceLabeling();}, "Does the model have an associated choice labelling?") .def_property_readonly("choice_labeling", [](SparseModel const& model) {return model.getChoiceLabeling();}, "get choice labelling") .def("has_choice_origins", [](SparseModel const& model) {return model.hasChoiceOrigins();}, "has choice origins?") @@ -453,3 +454,4 @@ void define_symbolic_model(py::module& m, std::string vt_suffix) { template void define_symbolic_model(py::module& m, std::string vt_suffix); template void define_sparse_model(py::module& m, std::string const& vt_suffix); template void define_sparse_model(py::module& m, std::string const& vt_suffix); +template void define_sparse_model(py::module& m, std::string const& vt_suffix); diff --git a/src/storage/model.h b/src/storage/model.h index ead0d7f82..98f38aa24 100644 --- a/src/storage/model.h +++ b/src/storage/model.h @@ -7,6 +7,7 @@ void define_model(py::module& m); template 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 void define_symbolic_model(py::module& m, std::string vt_suffix); diff --git a/src/storage/model_components.cpp b/src/storage/model_components.cpp index d130be5f4..5cc55fddf 100644 --- a/src/storage/model_components.cpp +++ b/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(py::module& m, std::string const& vtSuffix); template void define_sparse_model_components(py::module& m, std::string const& vtSuffix); -template void define_sparse_model_components(py::module& m, std::string const& vtSuffix); \ No newline at end of file +template void define_sparse_model_components(py::module& m, std::string const& vtSuffix); +template void define_sparse_model_components(py::module& m, std::string const& vtSuffix); diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp index 434e370ce..d1e8db790 100644 --- a/src/storage/scheduler.cpp +++ b/src/storage/scheduler.cpp @@ -23,6 +23,7 @@ void define_scheduler(py::module& m, std::string vt_suffix) { .def_property_readonly("partial", &Scheduler::isPartialScheduler, "Is the scheduler partial?") .def("cast_to_double_datatype", &Scheduler::template toValueType, "Construct the scheduler with `double` value type") .def("cast_to_exact_datatype", &Scheduler::template toValueType, "Construct the scheduler with `exact` value type") + // TODO does not work for Interval .def("cast_to_parametric_datatype", &Scheduler::template toValueType, "Construct the scheduler with `parametric` value type") .def("get_choice", &Scheduler::getChoice, py::arg("state_index"), py::arg("memory_index") = 0) .def("compute_action_support", &Scheduler::computeActionSupport, "nondeterministic_choice_indices"_a) @@ -49,4 +50,5 @@ void define_scheduler(py::module& m, std::string vt_suffix) { template void define_scheduler(py::module& m, std::string vt_suffix); template void define_scheduler(py::module& m, std::string vt_suffix); -template void define_scheduler(py::module& m, std::string vt_suffix); \ No newline at end of file +//template void define_scheduler(py::module& m, std::string vt_suffix); +template void define_scheduler(py::module& m, std::string vt_suffix); diff --git a/src/storage/state.cpp b/src/storage/state.cpp index f5ca6cdbf..b21cae9c8 100644 --- a/src/storage/state.cpp +++ b/src/storage/state.cpp @@ -35,5 +35,6 @@ void define_state(py::module& m, std::string const& vtSuffix) { template void define_state(py::module& m, std::string const& vtSuffix); template void define_state(py::module& m, std::string const& vtSuffix); +template void define_state(py::module& m, std::string const& vtSuffix); template void define_state(py::module& m, std::string const& vtSuffix); From d146a9a078a85240fd1c6e21ee30b1d3126e9bbd Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 19 Dec 2023 21:32:57 +0100 Subject: [PATCH 2/5] Scheduler with interval datatype --- src/mod_storage.cpp | 6 +++--- src/storage/scheduler.cpp | 26 ++++++++++++++++++-------- 2 files changed, 21 insertions(+), 11 deletions(-) diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index e8b97eb50..380167ffc 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -54,11 +54,11 @@ PYBIND11_MODULE(storage, m) { define_labeling(m); define_origins(m); define_expressions(m); - define_scheduler(m, "Double"); + define_scheduler(m, ""); define_scheduler(m, "Exact"); -// define_scheduler(m, "Interval"); + define_scheduler(m, "Interval"); define_scheduler(m, "Parametric"); - define_distribution(m, "Double"); + define_distribution(m, ""); define_distribution(m, "Exact"); define_distribution(m, "Interval"); define_sparse_model_components(m, ""); diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp index d1e8db790..a777650ed 100644 --- a/src/storage/scheduler.cpp +++ b/src/storage/scheduler.cpp @@ -21,34 +21,44 @@ void define_scheduler(py::module& m, std::string vt_suffix) { .def_property_readonly("memory_size", &Scheduler::getNumberOfMemoryStates, "How much memory does the scheduler take?") .def_property_readonly("deterministic", &Scheduler::isDeterministicScheduler, "Is the scheduler deterministic?") .def_property_readonly("partial", &Scheduler::isPartialScheduler, "Is the scheduler partial?") - .def("cast_to_double_datatype", &Scheduler::template toValueType, "Construct the scheduler with `double` value type") - .def("cast_to_exact_datatype", &Scheduler::template toValueType, "Construct the scheduler with `exact` value type") - // TODO does not work for Interval - .def("cast_to_parametric_datatype", &Scheduler::template toValueType, "Construct the scheduler with `parametric` value type") .def("get_choice", &Scheduler::getChoice, py::arg("state_index"), py::arg("memory_index") = 0) + .def("set_choice", &Scheduler::setChoice, py::arg("choice"), py::arg("state"), py::arg("memory_index") = 0) .def("compute_action_support", &Scheduler::computeActionSupport, "nondeterministic_choice_indices"_a) .def("to_json_str", [](Scheduler const& s, std::shared_ptr> model, bool skipUniqueChoices, bool skipDontCareStates) { std::stringstream str; s.printJsonToStream(str, model, skipUniqueChoices, skipDontCareStates); return str.str(); - }, py::arg("model"), py::arg("skip_unique_choices") = false, py::arg("skip_dont_care_states") = false); - + }, py::arg("model"), py::arg("skip_unique_choices") = false, py::arg("skip_dont_care_states") = false) ; + if constexpr (!std::is_same_v) { + // Conversion from Interval not implemented + scheduler + .def("cast_to_double_datatype", &Scheduler::template toValueType, "Construct the scheduler with `double` value type") + .def("cast_to_exact_datatype", &Scheduler::template toValueType, "Construct the scheduler with `exact` value type") + .def("cast_to_parametric_datatype", &Scheduler::template toValueType, "Construct the scheduler with `parametric` value type") + ; + if constexpr (!std::is_same_v) { + // Conversion from RationalFunction to Interval not implemented + scheduler.def("cast_to_interval_datatype", &Scheduler::template toValueType, "Construct the scheduler with `interval` value type"); + } + } + + std::string schedulerChoiceClassName = std::string("SchedulerChoice") + vt_suffix; py::class_ schedulerChoice(m, schedulerChoiceClassName.c_str(), "A choice of a finite memory scheduler"); schedulerChoice + .def(py::init(), "choice"_a) .def_property_readonly("defined", &SchedulerChoice::isDefined, "Is the choice defined by the scheduler?") .def_property_readonly("deterministic", &SchedulerChoice::isDeterministic, "Is the choice deterministic (given by a Dirac distribution)?") .def("get_deterministic_choice", &SchedulerChoice::getDeterministicChoice, "Get the deterministic choice") .def("get_choice", &SchedulerChoice::getChoiceAsDistribution, "Get the distribution over the actions") .def("__str__", &streamToString); - } template void define_scheduler(py::module& m, std::string vt_suffix); template void define_scheduler(py::module& m, std::string vt_suffix); -//template void define_scheduler(py::module& m, std::string vt_suffix); +template void define_scheduler(py::module& m, std::string vt_suffix); template void define_scheduler(py::module& m, std::string vt_suffix); From e30bfc51cd96692aa03e6a75f2f753407711409f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 19 Dec 2023 21:33:50 +0100 Subject: [PATCH 3/5] Additional bindings --- lib/stormpy/__init__.py | 4 ++-- src/storage/bitvector.cpp | 5 ++++- src/storage/model.cpp | 1 + 3 files changed, 7 insertions(+), 3 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index d3c7e881b..901ad52b5 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -602,11 +602,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") diff --git a/src/storage/bitvector.cpp b/src/storage/bitvector.cpp index 9718695e5..fa53f88c7 100644 --- a/src/storage/bitvector.cpp +++ b/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) - + .def("__hash__", [](const BitVector &b) { + return storm::storage::Murmur3BitVectorHash()(b); + }) ; } diff --git a/src/storage/model.cpp b/src/storage/model.cpp index d498ec430..60602acd9 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -209,6 +209,7 @@ void define_sparse_model(py::module& m, std::string const& vtSuffix) { .def("labels_state", &SparseModel::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("initial_states", &getSparseInitialStates, "Initial states") .def_property_readonly("initial_states_as_bitvector", [](SparseModel const& model) {return model.getInitialStates();}) + .def("set_initial_states", &SparseModel::setInitialStates, py::arg("states"), "Set initial states") .def_property_readonly("states", [](SparseModel& model) { return SparseModelStates(model); }, "Get states") From 97b1685ba11d06ad883333ed8f53e19e7e68f4f0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 21 Dec 2023 09:38:06 +0100 Subject: [PATCH 4/5] Suggested improvement by SJ --- src/storage/scheduler.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp index a777650ed..b5cb1ad98 100644 --- a/src/storage/scheduler.cpp +++ b/src/storage/scheduler.cpp @@ -49,7 +49,7 @@ void define_scheduler(py::module& m, std::string vt_suffix) { std::string schedulerChoiceClassName = std::string("SchedulerChoice") + vt_suffix; py::class_ schedulerChoice(m, schedulerChoiceClassName.c_str(), "A choice of a finite memory scheduler"); schedulerChoice - .def(py::init(), "choice"_a) + .def(py::init(), "choice"_a) .def_property_readonly("defined", &SchedulerChoice::isDefined, "Is the choice defined by the scheduler?") .def_property_readonly("deterministic", &SchedulerChoice::isDeterministic, "Is the choice deterministic (given by a Dirac distribution)?") .def("get_deterministic_choice", &SchedulerChoice::getDeterministicChoice, "Get the deterministic choice") From 119e739c3523e46f2bcefe755a3f01f3ca4136f9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 21 Dec 2023 10:55:22 +0100 Subject: [PATCH 5/5] Added test case for iMDP modelchecking and bindings for parsing iMDP from DRN --- lib/stormpy/__init__.py | 16 +++++++++++ lib/stormpy/examples/files/imdp/tiny-01.drn | 20 +++++++++++++ src/core/core.cpp | 1 + src/core/modelchecking.cpp | 1 - src/storage/model.cpp | 3 ++ tests/core/test_modelchecking.py | 32 +++++++++++++++++++++ 6 files changed, 72 insertions(+), 1 deletion(-) create mode 100644 lib/stormpy/examples/files/imdp/tiny-01.drn diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 901ad52b5..6df1255e1 100644 --- a/lib/stormpy/__init__.py +++ b/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. diff --git a/lib/stormpy/examples/files/imdp/tiny-01.drn b/lib/stormpy/examples/files/imdp/tiny-01.drn new file mode 100644 index 000000000..6bf3ab10c --- /dev/null +++ b/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] \ No newline at end of file diff --git a/src/core/core.cpp b/src/core/core.cpp index fa4481201..cf48357b5 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -128,6 +128,7 @@ void define_build(py::module& m) { m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel, "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, "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, "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, "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, "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, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr); diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp index c85ee58c3..4505f2203 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -50,7 +50,6 @@ std::shared_ptr modelCheckingHybridEngine(std: } std::shared_ptr checkIntervalMdp(std::shared_ptr> mdp, CheckTask const& task, storm::Environment& env) { - env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); auto checker = storm::modelchecker::SparseMdpPrctlModelChecker>(*mdp); return checker.check(env, task); } diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 60602acd9..5f0f4777e 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -147,6 +147,9 @@ void define_model(py::module& m) { .def("_as_sparse_pmdp", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse pMDP") + .def("_as_sparse_imdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse interval MDP") .def("_as_sparse_pomdp", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse POMDP") diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index eb0848dad..020161fcb 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -44,6 +44,38 @@ def test_model_checking_prism_mdp(self): result = stormpy.model_checking(model, formulas[0]) assert math.isclose(result.at(initial_state), 49 / 128, rel_tol=1e-5) + def test_model_checking_interval_mdp(self): + model = stormpy.build_interval_model_from_drn(get_example_path("imdp", "tiny-01.drn")) + formulas = stormpy.parse_properties("Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]") + initial_state = model.initial_states[0] + assert initial_state == 0 + + env = stormpy.Environment() + env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.value_iteration + + task = stormpy.CheckTask(formulas[0].raw_formula, only_initial_states=True) + task.set_produce_schedulers() + # Compute maximal robust + task.set_robust_uncertainty(True) + result = stormpy.check_interval_mdp(model, task, env) + assert math.isclose(result.at(initial_state), 0.4, rel_tol=1e-4) + # Compute maximal non-robust + task.set_robust_uncertainty(False) + result = stormpy.check_interval_mdp(model, task, env) + assert math.isclose(result.at(initial_state), 0.5, rel_tol=1e-4) + + task = stormpy.CheckTask(formulas[1].raw_formula, only_initial_states=True) + task.set_produce_schedulers() + # Compute minimal robust + task.set_robust_uncertainty(True) + result = stormpy.check_interval_mdp(model, task, env) + assert math.isclose(result.at(initial_state), 0.5, rel_tol=1e-4) + # Compute minimal non-robust + task.set_robust_uncertainty(False) + result = stormpy.check_interval_mdp(model, task, env) + assert math.isclose(result.at(initial_state), 0.4, rel_tol=1e-4) + + def test_model_checking_jani_dtmc(self): jani_model, formulas = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) formulas = stormpy.eliminate_reward_accumulations(jani_model, formulas)