From 58da4df1c3611e3e83c0fc5c9c74047a3d4d253c Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 25 Sep 2020 15:19:34 -0700 Subject: [PATCH] support for exact arithmetic --- CHANGELOG.md | 4 + lib/stormpy/__init__.py | 12 +- lib/stormpy/simulator.py | 5 +- src/core/core.cpp | 10 +- src/core/modelchecking.cpp | 10 +- src/core/simulator.cpp | 23 ++-- src/core/simulator.h | 3 +- src/mod_core.cpp | 4 +- src/mod_pomdp.cpp | 5 +- src/mod_storage.cpp | 18 ++- src/pomdp/tracker.cpp | 59 +++++----- src/pomdp/tracker.h | 3 +- src/pomdp/transformations.cpp | 14 +-- src/storage/distribution.cpp | 4 +- src/storage/jani.cpp | 1 + src/storage/matrix.cpp | 187 ++++++++----------------------- src/storage/matrix.h | 5 +- src/storage/model.cpp | 140 ++++++++++++----------- src/storage/model.h | 4 +- src/storage/model_components.cpp | 39 ++++--- src/storage/model_components.h | 3 +- src/storage/scheduler.cpp | 3 +- src/storage/state.cpp | 64 +++++------ src/storage/state.h | 3 +- 24 files changed, 297 insertions(+), 326 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 427bae8..c602295 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,10 @@ Changelog Version 1.6.x ------------- +### Version 1.6.3 (to be released) +- Support for exact arithmetic in models + + ### Version 1.6.2 (2020/09) Requires storm version >= 1.6.2 and pycarl version >= 2.0.4 diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index d01e014..9aae889 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -297,9 +297,15 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched task.set_produce_schedulers(extract_scheduler) return core._parametric_model_checking_sparse_engine(model, task, environment=environment) else: - task = core.CheckTask(formula, only_initial_states) - task.set_produce_schedulers(extract_scheduler) - return core._model_checking_sparse_engine(model, task, environment=environment) + + if model.is_exact: + task = core.ExactCheckTask(formula, only_initial_states) + task.set_produce_schedulers(extract_scheduler) + return core._exact_model_checking_sparse_engine(model, task, environment=environment) + else: + task = core.CheckTask(formula, only_initial_states) + task.set_produce_schedulers(extract_scheduler) + return core._model_checking_sparse_engine(model, task, environment=environment) def check_model_dd(model, property, only_initial_states=False, environment=Environment()): diff --git a/lib/stormpy/simulator.py b/lib/stormpy/simulator.py index 28e26e9..8c8c6ef 100644 --- a/lib/stormpy/simulator.py +++ b/lib/stormpy/simulator.py @@ -93,7 +93,10 @@ class SparseSimulator(Simulator): def __init__(self, model, seed=None): super().__init__(seed) self._model = model - self._engine = stormpy.core._DiscreteTimeSparseModelSimulatorDouble(model) + if self._model.is_exact: + self._engine = stormpy.core._DiscreteTimeSparseModelSimulatorExact(model) + else: + self._engine = stormpy.core._DiscreteTimeSparseModelSimulatorDouble(model) if seed is not None: self._engine.set_seed(seed) self._state_valuations = None diff --git a/src/core/core.cpp b/src/core/core.cpp index e966019..dc01e13 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -101,24 +101,28 @@ void define_build(py::module& m) { // Build model m.def("_build_sparse_model_from_symbolic_description", &buildSparseModel, "Build the model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); + m.def("_build_sparse_exact_model_from_symbolic_description", &buildSparseModel, "Build the model in sparse representation with exact number representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector>(), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("build_sparse_model_with_options", &buildSparseModelWithOptions, "Build the model in sparse representation", py::arg("model_description"), py::arg("options"), py::arg("use_jit") = false, py::arg("doctor") = false); + m.def("build_sparse_exact_model_with_options", &buildSparseModelWithOptions, "Build the model in sparse representation with exact number representation", py::arg("model_description"), py::arg("options"), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("build_sparse_parametric_model_with_options", &buildSparseModelWithOptions, "Build the model in sparse representation", py::arg("model_description"), py::arg("options"), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel, "Build the model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel, "Build the parametric model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector>()); 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_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")); + m.def("make_sparse_model_builder_exact", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options")); m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder, "Construct a builder instance", py::arg("model_description"), py::arg("options")); - py::class_>(m, "ExplicitModelBuilder_Double", "Model builder for sparse models") + py::class_>(m, "ExplicitModelBuilder", "Model builder for sparse models") .def("build", &storm::builder::ExplicitModelBuilder::build, "Build the model") .def("export_lookup", &storm::builder::ExplicitModelBuilder::exportExplicitStateLookup, "Export a lookup model") ; - py::class_>(m, "ExplicitModelBuilder_RF", "Model builder for sparse models") + py::class_>(m, "ExplicitParametricModelBuilder", "Model builder for sparse models") .def("build", &storm::builder::ExplicitModelBuilder::build, "Build the model") .def("export_lookup", &storm::builder::ExplicitModelBuilder::exportExplicitStateLookup, "Export a lookup model") ; @@ -164,6 +168,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_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 f0c24d1..7175568 100644 --- a/src/core/modelchecking.cpp +++ b/src/core/modelchecking.cpp @@ -66,6 +66,12 @@ 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) ; + // CheckTask + py::class_, std::shared_ptr>>(m, "ExactCheckTask", "Task for model checking with exact numbers") + //m.def("create_check_task", &storm::api::createTask, "Create task for verification", py::arg("formula"), py::arg("only_initial_states") = false); + .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) + ; py::class_, std::shared_ptr>>(m, "ParametricCheckTask", "Task for parametric model checking") //m.def("create_check_task", &storm::api::createTask, "Create task for verification", py::arg("formula"), py::arg("only_initial_states") = false); .def(py::init(), py::arg("formula"), py::arg("only_initial_states") = false) @@ -73,8 +79,10 @@ void define_modelchecking(py::module& m) { ; // Model checking - m.def("model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + m.def("_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + m.def("_exact_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine, py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); + m.def("_exact_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform model checking using the sparse engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine, "Perform parametric model checking using the sparse engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); m.def("_model_checking_dd_engine", &modelCheckingDdEngine, "Perform model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); 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()); diff --git a/src/core/simulator.cpp b/src/core/simulator.cpp index 098dd1e..42a0731 100644 --- a/src/core/simulator.cpp +++ b/src/core/simulator.cpp @@ -1,14 +1,17 @@ #include "simulator.h" #include -void define_sparse_model_simulator(py::module& m) { - py::class_> dtsmsd(m, "_DiscreteTimeSparseModelSimulatorDouble", "Simulator for sparse discrete-time models in memory (ValueType = double)"); - dtsmsd.def(py::init const&>()); - dtsmsd.def("set_seed", &storm::simulator::DiscreteTimeSparseModelSimulator::setSeed, py::arg("seed")); - dtsmsd.def("step", &storm::simulator::DiscreteTimeSparseModelSimulator::step, py::arg("action")); - dtsmsd.def("random_step", &storm::simulator::DiscreteTimeSparseModelSimulator::randomStep); - dtsmsd.def("get_last_reward", &storm::simulator::DiscreteTimeSparseModelSimulator::getLastRewards); - dtsmsd.def("get_current_state", &storm::simulator::DiscreteTimeSparseModelSimulator::getCurrentState); - dtsmsd.def("reset_to_initial_state", &storm::simulator::DiscreteTimeSparseModelSimulator::resetToInitial); +template +void define_sparse_model_simulator(py::module& m, std::string const& vtSuffix) { + py::class_> dtsmsd(m, ("_DiscreteTimeSparseModelSimulator" + vtSuffix).c_str(), "Simulator for sparse discrete-time models in memory (ValueType = double)"); + dtsmsd.def(py::init const&>()); + dtsmsd.def("set_seed", &storm::simulator::DiscreteTimeSparseModelSimulator::setSeed, py::arg("seed")); + dtsmsd.def("step", &storm::simulator::DiscreteTimeSparseModelSimulator::step, py::arg("action")); + dtsmsd.def("random_step", &storm::simulator::DiscreteTimeSparseModelSimulator::randomStep); + dtsmsd.def("get_last_reward", &storm::simulator::DiscreteTimeSparseModelSimulator::getLastRewards); + dtsmsd.def("get_current_state", &storm::simulator::DiscreteTimeSparseModelSimulator::getCurrentState); + dtsmsd.def("reset_to_initial_state", &storm::simulator::DiscreteTimeSparseModelSimulator::resetToInitial); +} -} \ No newline at end of file +template void define_sparse_model_simulator(py::module& m, std::string const& vtSuffix); +template void define_sparse_model_simulator(py::module& m, std::string const& vtSuffix); diff --git a/src/core/simulator.h b/src/core/simulator.h index 4edb35b..bcb22e6 100644 --- a/src/core/simulator.h +++ b/src/core/simulator.h @@ -2,4 +2,5 @@ #include "common.h" -void define_sparse_model_simulator(py::module& m); \ No newline at end of file +template +void define_sparse_model_simulator(py::module& m, std::string const& vtSuffix); \ No newline at end of file diff --git a/src/mod_core.cpp b/src/mod_core.cpp index f16db4d..18c8680 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -34,5 +34,7 @@ PYBIND11_MODULE(core, m) { define_input(m); define_graph_constraints(m); define_transformation(m); - define_sparse_model_simulator(m); + define_sparse_model_simulator(m, "Double"); + define_sparse_model_simulator(m, "Exact"); + } diff --git a/src/mod_pomdp.cpp b/src/mod_pomdp.cpp index 4e86642..9cb8766 100644 --- a/src/mod_pomdp.cpp +++ b/src/mod_pomdp.cpp @@ -14,11 +14,14 @@ PYBIND11_MODULE(pomdp, m) { py::options options; options.disable_function_signatures(); #endif - define_tracker(m); + define_tracker(m, "Double"); + define_tracker(m, "Exact"); 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, "Exact"); + define_transformations(m, "Rf"); } diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index ba53955..09e5b6f 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -28,12 +28,19 @@ PYBIND11_MODULE(storage, m) { define_bitvector(m); define_dd(m, "Sylvan"); define_dd_nt(m); + define_model(m); + define_sparse_model(m, ""); + define_sparse_model(m, "Exact"); + define_sparse_parametric_model(m); define_statevaluation(m); - define_sparse_model(m); - define_sparse_matrix(m); + define_sparse_matrix(m, ""); + define_sparse_matrix(m, "Exact"); + define_sparse_matrix(m, "Parametric"); + define_sparse_matrix_nt(m); define_symbolic_model(m, "Sylvan"); - define_state(m); + define_state(m, ""); + define_state(m, "Exact"); define_prism(m); define_jani(m); define_jani_transformers(m); @@ -41,6 +48,9 @@ PYBIND11_MODULE(storage, m) { define_origins(m); define_expressions(m); define_scheduler(m, "Double"); + define_scheduler(m, "Exact"); define_distribution(m, "Double"); - define_sparse_model_components(m); + define_sparse_model_components(m, ""); + define_sparse_model_components(m, "Exact"); + } diff --git a/src/pomdp/tracker.cpp b/src/pomdp/tracker.cpp index 6798be4..468d9aa 100644 --- a/src/pomdp/tracker.cpp +++ b/src/pomdp/tracker.cpp @@ -7,39 +7,39 @@ template using SparsePomdp = storm::models::sparse::Pomdp; template using SparsePomdpTracker = storm::generator::BeliefSupportTracker; -template using NDPomdpTrackerSparse = storm::generator::NondeterministicBeliefTracker>; -template using NDPomdpTrackerDense = storm::generator::NondeterministicBeliefTracker>; - - -void define_tracker(py::module& m) { - py::class_> tracker(m, "BeliefSupportTrackerDouble", "Tracker for BeliefSupports"); - tracker.def(py::init const&>(), py::arg("pomdp")); - tracker.def("get_current_belief_support", &SparsePomdpTracker::getCurrentBeliefSupport, "What is the support given the trace so far"); - tracker.def("track", &SparsePomdpTracker::track, py::arg("action"), py::arg("observation")); - - py::class_> sbel(m, "SparseBeliefStateDouble", "Belief state in sparse format"); - sbel.def("get", &storm::generator::SparseBeliefState::get, py::arg("state")); - sbel.def_property_readonly("risk", &storm::generator::SparseBeliefState::getRisk); - sbel.def("__str__", &storm::generator::SparseBeliefState::toString); - sbel.def_property_readonly("is_valid", &storm::generator::SparseBeliefState::isValid); +template using NDPomdpTrackerSparse = storm::generator::NondeterministicBeliefTracker>; +template using NDPomdpTrackerDense = storm::generator::NondeterministicBeliefTracker>; + + +template +void define_tracker(py::module& m, std::string const& vtSuffix) { + py::class_> tracker(m, ("BeliefSupportTracker" + vtSuffix).c_str(), "Tracker for BeliefSupports"); + tracker.def(py::init const&>(), py::arg("pomdp")); + tracker.def("get_current_belief_support", &SparsePomdpTracker::getCurrentBeliefSupport, "What is the support given the trace so far"); + tracker.def("track", &SparsePomdpTracker::track, py::arg("action"), py::arg("observation")); + + py::class_> sbel(m, ("SparseBeliefState" + vtSuffix).c_str(), "Belief state in sparse format"); + sbel.def("get", &storm::generator::SparseBeliefState::get, py::arg("state")); + sbel.def_property_readonly("risk", &storm::generator::SparseBeliefState::getRisk); + sbel.def("__str__", &storm::generator::SparseBeliefState::toString); + sbel.def_property_readonly("is_valid", &storm::generator::SparseBeliefState::isValid); // // py::class_> dbel(m, "DenseBeliefStateDouble", "Belief state in dense format"); // dbel.def("get", &storm::generator::ObservationDenseBeliefState::get, py::arg("state")); // dbel.def_property_readonly("risk", &storm::generator::ObservationDenseBeliefState::getRisk); // dbel.def("__str__", &storm::generator::ObservationDenseBeliefState::toString); - py::class_> ndetbelieftracker(m, "NondeterministicBeliefTrackerDoubleSparse", "Tracker for belief states and uncontrollable actions"); - ndetbelieftracker.def(py::init const&>(), py::arg("pomdp")); - 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); - ndetbelieftracker.def("track", &NDPomdpTrackerSparse::track, py::arg("observation")); - ndetbelieftracker.def("obtain_beliefs", &NDPomdpTrackerSparse::getCurrentBeliefs); - ndetbelieftracker.def("size", &NDPomdpTrackerSparse::getNumberOfBeliefs); - ndetbelieftracker.def("dimension", &NDPomdpTrackerSparse::getCurrentDimension); - ndetbelieftracker.def("obtain_last_observation", &NDPomdpTrackerSparse::getCurrentObservation); - ndetbelieftracker.def("reduce",&NDPomdpTrackerSparse::reduce); - + 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("reset", &NDPomdpTrackerSparse::reset); + ndetbelieftracker.def("set_risk", &NDPomdpTrackerSparse::setRisk, py::arg("risk")); + ndetbelieftracker.def("obtain_current_risk",&NDPomdpTrackerSparse::getCurrentRisk, py::arg("max")=true); + ndetbelieftracker.def("track", &NDPomdpTrackerSparse::track, py::arg("observation")); + ndetbelieftracker.def("obtain_beliefs", &NDPomdpTrackerSparse::getCurrentBeliefs); + ndetbelieftracker.def("size", &NDPomdpTrackerSparse::getNumberOfBeliefs); + ndetbelieftracker.def("dimension", &NDPomdpTrackerSparse::getCurrentDimension); + ndetbelieftracker.def("obtain_last_observation", &NDPomdpTrackerSparse::getCurrentObservation); + ndetbelieftracker.def("reduce",&NDPomdpTrackerSparse::reduce); // py::class_> ndetbelieftrackerd(m, "NondeterministicBeliefTrackerDoubleDense", "Tracker for belief states and uncontrollable actions"); // ndetbelieftrackerd.def(py::init const&>(), py::arg("pomdp")); @@ -51,4 +51,7 @@ void define_tracker(py::module& m) { // ndetbelieftrackerd.def("obtain_last_observation", &NDPomdpTrackerDense::getCurrentObservation); // ndetbelieftrackerd.def("reduce",&NDPomdpTrackerDense::reduce); -} \ No newline at end of file +} + +template void define_tracker(py::module& m, std::string const& vtSuffix); +template void define_tracker(py::module& m, std::string const& vtSuffix); diff --git a/src/pomdp/tracker.h b/src/pomdp/tracker.h index 9370d29..b4b91ad 100644 --- a/src/pomdp/tracker.h +++ b/src/pomdp/tracker.h @@ -1,4 +1,5 @@ #pragma once #include "common.h" -void define_tracker(py::module& m); +template +void define_tracker(py::module& m, std::string const& vtSuffix); diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp index 91131a5..45c1e7d 100644 --- a/src/pomdp/transformations.cpp +++ b/src/pomdp/transformations.cpp @@ -46,13 +46,6 @@ void define_transformations_nt(py::module &m) { .value("full", storm::transformer::PomdpFscApplicationMode::FULL) ; - - py::class_> unfolder(m, "ObservationTraceUnfolderDouble", "Unfolds observation traces in models"); - unfolder.def(py::init const&, std::vector const&, std::shared_ptr&>(), py::arg("model"), py::arg("risk"), py::arg("expression_manager")); - unfolder.def("transform", &storm::pomdp::ObservationTraceUnfolder::transform, py::arg("trace")); - unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder::extend, py::arg("new_observation")); - unfolder.def("reset", &storm::pomdp::ObservationTraceUnfolder::reset, py::arg("new_observation")); - } template @@ -63,8 +56,13 @@ void define_transformations(py::module& m, std::string const& vtSuffix) { 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); //m.def(("_unfold_trace_" + vtSuffix).c_str(), &unfold_trace, "Unfold observed trace", py::arg("pomdp"), py::arg("expression_manager"),py::arg("observation_trace"), py::arg("risk_definition")); - + py::class_> unfolder(m, ("ObservationTraceUnfolder" + vtSuffix).c_str(), "Unfolds observation traces in models"); + unfolder.def(py::init const&, std::vector const&, std::shared_ptr&>(), py::arg("model"), py::arg("risk"), py::arg("expression_manager")); + unfolder.def("transform", &storm::pomdp::ObservationTraceUnfolder::transform, py::arg("trace")); + unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder::extend, py::arg("new_observation")); + unfolder.def("reset", &storm::pomdp::ObservationTraceUnfolder::reset, py::arg("new_observation")); } template void define_transformations(py::module& m, std::string const& vtSuffix); +template void define_transformations(py::module& m, std::string const& vtSuffix); template void define_transformations(py::module& m, std::string const& vtSuffix); \ No newline at end of file diff --git a/src/storage/distribution.cpp b/src/storage/distribution.cpp index 79a03a2..d2ab67b 100644 --- a/src/storage/distribution.cpp +++ b/src/storage/distribution.cpp @@ -1,3 +1,4 @@ +#include #include "distribution.h" #include "src/helpers.h" @@ -14,4 +15,5 @@ void define_distribution(py::module& m, std::string vt_suffix) { } -template void define_distribution(py::module&, std::string vt_suffix); \ No newline at end of file +template void define_distribution(py::module&, std::string vt_suffix); +template void define_distribution(py::module&, std::string vt_suffix); \ No newline at end of file diff --git a/src/storage/jani.cpp b/src/storage/jani.cpp index 3dd5831..2f8a88f 100644 --- a/src/storage/jani.cpp +++ b/src/storage/jani.cpp @@ -140,6 +140,7 @@ void define_jani(py::module& m) { py::class_> variable(m, "JaniVariable", "A Variable in JANI"); variable.def_property_readonly("name", &Variable::getName, "name of constant") .def_property_readonly("expression_variable", &Variable::getExpressionVariable, "expression variable for this variable") + //.def_property_readonly("initial_value_expression", &Variable::getInitialValue) ; py::class_> bivariable(m, "JaniBoundedIntegerVariable", "A Bounded Integer", variable); diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index bbbc859..c44bec0 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -12,30 +12,29 @@ template using MatrixEntry = storm::storage::MatrixEntry& matrix, std::vector initial) { return storm::utility::graph::getTopologicalSort(matrix, initial); }, "matrix"_a, "initial"_a, "get topological sort w.r.t. a transition matrix"); + m.def("_topological_sort_rf", [](SparseMatrix& matrix, std::vector initial) { return storm::utility::graph::getTopologicalSort(matrix, initial); }, "matrix"_a, "initial"_a, "get topological sort w.r.t. a transition matrix"); +} + +template +void define_sparse_matrix(py::module& m, std::string const& vtSuffix) { // MatrixEntry - py::class_>(m, "SparseMatrixEntry", "Entry of sparse matrix") - .def("__str__", &streamToString>) + py::class_>(m, (vtSuffix + "SparseMatrixEntry").c_str(), "Entry of sparse matrix") + .def("__str__", &streamToString>) //def_property threw "pointer being freed not allocated" after exiting - .def("value", &MatrixEntry::getValue, "Value") - .def("set_value", &MatrixEntry::setValue, py::arg("value"), "Set value") - .def_property_readonly("column", &MatrixEntry::getColumn, "Column") + .def("value", &MatrixEntry::getValue, "Value") + .def("set_value", &MatrixEntry::setValue, py::arg("value"), "Set value") + .def_property_readonly("column", &MatrixEntry::getColumn, "Column") ; - py::class_>(m, "ParametricSparseMatrixEntry", "Entry of parametric sparse matrix") - .def("__str__", &streamToString>) - //def_property threw "pointer being freed not allocated" after exiting - .def("value", &MatrixEntry::getValue, "Value") - .def("set_value", &MatrixEntry::setValue, py::arg("value"), "Set value") - .def_property_readonly("column", &MatrixEntry::getColumn, "Column") - ; // SparseMatrixBuilder - py::class_>(m, "SparseMatrixBuilder", "Builder of sparse matrix") + py::class_>(m, ( vtSuffix + "SparseMatrixBuilder").c_str(), "Builder of sparse matrix") .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "force_dimensions"_a = true, "has_custom_row_grouping"_a = false, "row_groups"_a = 0) - .def("add_next_value", &SparseMatrixBuilder::addNextValue, R"dox( + .def("add_next_value", &SparseMatrixBuilder::addNextValue, R"dox( Sets the matrix entry at the given row and column to the given value. After all entries have been added, calling function build() is mandatory. @@ -50,45 +49,12 @@ void define_sparse_matrix(py::module& m) { :param double value: The value that is to be set at the specified row and column )dox", py::arg("row"), py::arg("column"), py::arg("value")) - .def("new_row_group", &SparseMatrixBuilder::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix") - .def("build", &SparseMatrixBuilder::build, py::arg("overridden_row_count") = 0, py::arg("overridden_column_count") = 0, py::arg("overridden-row_group_count") = 0, "Finalize the sparse matrix") - .def("get_last_row", &SparseMatrixBuilder::getLastRow, "Get the most recently used row") - .def("get_current_row_group_count", &SparseMatrixBuilder::getCurrentRowGroupCount, "Get the current row group count") - .def("get_last_column", &SparseMatrixBuilder::getLastColumn, "the most recently used column") - .def("replace_columns", &SparseMatrixBuilder::replaceColumns, R"dox( - - Replaces all columns with id >= offset according to replacements. - Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted. - - :param std::vector const& replacements: replacements Mapping indicating the replacements from offset+i -> value of i - :param int offset: Offset to add to each id in vector index. - )dox", py::arg("replacements"), py::arg("offset")) - ; - - py::class_>(m, "ParametricSparseMatrixBuilder", "Builder of parametric sparse matrix") - .def(py::init(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "force_dimensions"_a = true, "has_custom_row_grouping"_a = false, "row_groups"_a = 0) - - .def("add_next_value", &SparseMatrixBuilder::addNextValue, R"dox( - - Sets the matrix entry at the given row and column to the given value. After all entries have been added, - calling function build() is mandatory. - - Note: this is a linear setter. That is, it must be called consecutively for each entry, row by row and - column by column. As multiple entries per column are admitted, consecutive calls to this method are - admitted to mention the same row-column-pair. If rows are skipped entirely, the corresponding rows are - treated as empty. If these constraints are not met, an exception is thrown. - - :param double row: The row in which the matrix entry is to be set - :param double column: The column in which the matrix entry is to be set - :param RationalFunction value: The value that is to be set at the specified row and column - )dox", py::arg("row"), py::arg("column"), py::arg("value")) - - .def("new_row_group", &SparseMatrixBuilder::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix") - .def("build", &SparseMatrixBuilder::build, py::arg("overridden_row_count") = 0, py::arg("overridden_column_count") = 0, py::arg("overridden-row_group_count") = 0, "Finalize the sparse matrix") - .def("get_last_row", &SparseMatrixBuilder::getLastRow, "Get the most recently used row") - .def("get_current_row_group_count", &SparseMatrixBuilder::getCurrentRowGroupCount, "Get the current row group count") - .def("get_last_column", &SparseMatrixBuilder::getLastColumn, "the most recently used column") - .def("replace_columns", &SparseMatrixBuilder::replaceColumns, R"dox( + .def("new_row_group", &SparseMatrixBuilder::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix") + .def("build", &SparseMatrixBuilder::build, py::arg("overridden_row_count") = 0, py::arg("overridden_column_count") = 0, py::arg("overridden-row_group_count") = 0, "Finalize the sparse matrix") + .def("get_last_row", &SparseMatrixBuilder::getLastRow, "Get the most recently used row") + .def("get_current_row_group_count", &SparseMatrixBuilder::getCurrentRowGroupCount, "Get the current row group count") + .def("get_last_column", &SparseMatrixBuilder::getLastColumn, "the most recently used column") + .def("replace_columns", &SparseMatrixBuilder::replaceColumns, R"dox( Replaces all columns with id >= offset according to replacements. Every state with id offset+i is replaced by the id in replacements[i]. Afterwards the columns are sorted. @@ -99,26 +65,26 @@ void define_sparse_matrix(py::module& m) { ; // SparseMatrix - py::class_>(m, "SparseMatrix", "Sparse matrix") - .def("__iter__", [](SparseMatrix& matrix) { + py::class_>(m, (vtSuffix + "SparseMatrix").c_str(), "Sparse matrix") + .def("__iter__", [](SparseMatrix& matrix) { return py::make_iterator(matrix.begin(), matrix.end()); }, py::keep_alive<0, 1>() /* Essential: keep object alive while iterator exists */) - .def("__str__", &streamToString>) - .def_property_readonly("nr_rows", &SparseMatrix::getRowCount, "Number of rows") - .def_property_readonly("nr_columns", &SparseMatrix::getColumnCount, "Number of columns") - .def_property_readonly("nr_entries", &SparseMatrix::getEntryCount, "Number of non-zero entries") - .def_property_readonly("_row_group_indices", &SparseMatrix::getRowGroupIndices, "Starting rows of row groups") - - .def("get_row_group_start", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row];}) - .def("get_row_group_end", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row+1];}) - .def_property_readonly("has_trivial_row_grouping", &SparseMatrix::hasTrivialRowGrouping, "Trivial row grouping") - .def("get_row", [](SparseMatrix& matrix, entry_index row) { + .def("__str__", &streamToString>) + .def_property_readonly("nr_rows", &SparseMatrix::getRowCount, "Number of rows") + .def_property_readonly("nr_columns", &SparseMatrix::getColumnCount, "Number of columns") + .def_property_readonly("nr_entries", &SparseMatrix::getEntryCount, "Number of non-zero entries") + .def_property_readonly("_row_group_indices", &SparseMatrix::getRowGroupIndices, "Starting rows of row groups") + + .def("get_row_group_start", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row];}) + .def("get_row_group_end", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row+1];}) + .def_property_readonly("has_trivial_row_grouping", &SparseMatrix::hasTrivialRowGrouping, "Trivial row grouping") + .def("get_row", [](SparseMatrix& matrix, entry_index row) { return matrix.getRows(row, row+1); }, py::return_value_policy::reference, py::keep_alive<1, 0>(), py::arg("row"), "Get row") - .def("get_rows", [](SparseMatrix& matrix, entry_index start, entry_index end) { + .def("get_rows", [](SparseMatrix& matrix, entry_index start, entry_index end) { return matrix.getRows(start, end); }, py::return_value_policy::reference, py::keep_alive<1, 0>(), py::arg("row_start"), py::arg("row_end"), "Get rows from start to end") - .def("print_row", [](SparseMatrix const& matrix, entry_index row) { + .def("print_row", [](SparseMatrix const& matrix, entry_index row) { std::stringstream stream; auto rows = matrix.getRows(row, row+1); for (auto transition : rows) { @@ -126,22 +92,22 @@ void define_sparse_matrix(py::module& m) { } return stream.str(); }, py::arg("row"), "Print rows from start to end") - .def("submatrix", [](SparseMatrix const& matrix, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalEntries = false) { + .def("submatrix", [](SparseMatrix const& matrix, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalEntries = false) { return matrix.getSubmatrix(true, rowConstraint, columnConstraint, insertDiagonalEntries); }, py::arg("row_constraint"), py::arg("column_constraint"), py::arg("insert_diagonal_entries") = false, "Get submatrix") // Entry_index lead to problems - .def("row_iter", [](SparseMatrix& matrix, row_index start, row_index end) { + .def("row_iter", [](SparseMatrix& matrix, row_index start, row_index end) { return py::make_iterator(matrix.begin(start), matrix.end(end)); }, py::keep_alive<0, 1>() /* keep object alive while iterator exists */, py::arg("row_start"), py::arg("row_end"), "Get iterator from start to end") // (partial) container interface to allow e.g. matrix[7:9] - .def("__len__", &SparseMatrix::getRowCount) - .def("__getitem__", [](SparseMatrix& matrix, entry_index i) { + .def("__len__", &SparseMatrix::getRowCount) + .def("__getitem__", [](SparseMatrix& matrix, entry_index i) { if (i >= matrix.getRowCount()) throw py::index_error(); return matrix.getRows(i, i+1); }, py::return_value_policy::reference, py::keep_alive<1, 0>()) - .def("__getitem__", [](SparseMatrix& matrix, py::slice slice) { + .def("__getitem__", [](SparseMatrix& matrix, py::slice slice) { size_t start, stop, step, slice_length; if (!slice.compute(matrix.getRowCount(), &start, &stop, &step, &slice_length)) throw py::error_already_set(); @@ -151,75 +117,18 @@ void define_sparse_matrix(py::module& m) { }, py::return_value_policy::reference, py::keep_alive<1, 0>()) ; - m.def("_topological_sort_double", [](SparseMatrix& matrix, std::vector initial) { return storm::utility::graph::getTopologicalSort(matrix, initial); }, "matrix"_a, "initial"_a, "get topological sort w.r.t. a transition matrix"); - m.def("_topological_sort_rf", [](SparseMatrix& matrix, std::vector initial) { return storm::utility::graph::getTopologicalSort(matrix, initial); }, "matrix"_a, "initial"_a, "get topological sort w.r.t. a transition matrix"); - - - py::class_>(m, "ParametricSparseMatrix", "Parametric sparse matrix") - .def("__iter__", [](SparseMatrix& matrix) { - return py::make_iterator(matrix.begin(), matrix.end()); - }, py::keep_alive<0, 1>() /* Essential: keep object alive while iterator exists */) - .def("__str__", &streamToString>) - .def_property_readonly("nr_rows", &SparseMatrix::getRowCount, "Number of rows") - .def_property_readonly("nr_columns", &SparseMatrix::getColumnCount, "Number of columns") - .def_property_readonly("nr_entries", &SparseMatrix::getEntryCount, "Number of non-zero entries") - .def_property_readonly("_row_group_indices", &SparseMatrix::getRowGroupIndices, "Starting rows of row groups") - .def("get_row_group_start", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row];}) - .def("get_row_group_end", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row+1];}) - .def_property_readonly("has_trivial_row_grouping", &SparseMatrix::hasTrivialRowGrouping, "Trivial row grouping") - .def("get_row", [](SparseMatrix& matrix, entry_index row) { - return matrix.getRows(row, row+1); - }, py::return_value_policy::reference, py::keep_alive<1, 0>(), py::arg("row"), "Get row") - .def("get_rows", [](SparseMatrix& matrix, entry_index start, entry_index end) { - return matrix.getRows(start, end); - }, py::return_value_policy::reference, py::keep_alive<1, 0>(), py::arg("row_start"), py::arg("row_end"), "Get rows from start to end") - .def("print_row", [](SparseMatrix const& matrix, entry_index row) { - std::stringstream stream; - auto rows = matrix.getRows(row, row+1); - for (auto transition : rows) { - stream << transition << ", "; - } - return stream.str(); - }, py::arg("row"), "Print row") - .def("submatrix", [](SparseMatrix const& matrix, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalEntries = false) { - return matrix.getSubmatrix(true, rowConstraint, columnConstraint, insertDiagonalEntries); - }, py::arg("row_constraint"), py::arg("column_constraint"), py::arg("insert_diagonal_entries") = false, "Get submatrix") - // Entry_index lead to problems - .def("row_iter", [](SparseMatrix& matrix, row_index start, row_index end) { - return py::make_iterator(matrix.begin(start), matrix.end(end)); - }, py::keep_alive<0, 1>() /* keep object alive while iterator exists */, py::arg("row_start"), py::arg("row_end"), "Get iterator from start to end") - - // (partial) container interface to allow e.g. matrix[7:9] - .def("__len__", &SparseMatrix::getRowCount) - .def("__getitem__", [](SparseMatrix& matrix, entry_index i) { - if (i >= matrix.getRowCount()) - throw py::index_error(); - return matrix.getRows(i, i+1); - }, py::return_value_policy::reference, py::keep_alive<1, 0>()) - .def("__getitem__", [](SparseMatrix& matrix, py::slice slice) { - size_t start, stop, step, slice_length; - if (!slice.compute(matrix.getRowCount(), &start, &stop, &step, &slice_length)) - throw py::error_already_set(); - if (step != 1) - throw py::value_error(); // not supported - return matrix.getRows(start, stop); - }, py::return_value_policy::reference, py::keep_alive<1, 0>()) - ; // Rows - py::class_::rows>(m, "SparseMatrixRows", "Set of rows in a sparse matrix") - .def("__iter__", [](SparseMatrix::rows& rows) { - return py::make_iterator(rows.begin(), rows.end()); - }, py::keep_alive<0, 1>()) - .def("__str__", &containerToString::rows>) - .def("__len__", &storm::storage::SparseMatrix::rows::getNumberOfEntries) - ; - - py::class_::rows>(m, "ParametricSparseMatrixRows", "Set of rows in a parametric sparse matrix") - .def("__iter__", [](SparseMatrix::rows& rows) { + py::class_::rows>(m, (vtSuffix + "SparseMatrixRows").c_str(), "Set of rows in a sparse matrix") + .def("__iter__", [](typename SparseMatrix::rows& rows) { return py::make_iterator(rows.begin(), rows.end()); }, py::keep_alive<0, 1>()) - .def("__str__", &containerToString::rows>) - .def("__len__", &storm::storage::SparseMatrix::rows::getNumberOfEntries) + .def("__str__", &containerToString::rows>) + .def("__len__", &storm::storage::SparseMatrix::rows::getNumberOfEntries) ; } + +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/matrix.h b/src/storage/matrix.h index 96e3df6..d6f3776 100644 --- a/src/storage/matrix.h +++ b/src/storage/matrix.h @@ -3,6 +3,9 @@ #include "common.h" -void define_sparse_matrix(py::module& m); +template +void define_sparse_matrix(py::module& m, std::string const& vtSuffix); + +void define_sparse_matrix_nt(py::module& m); #endif /* PYTHON_STORAGE_MATRIX_H_ */ diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 152c140..dee8661 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -115,12 +115,18 @@ void define_model(py::module& m) { .def("_as_sparse_dtmc", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse DTMC") + .def("_as_sparse_exact_dtmc", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse DTMC") .def("_as_sparse_pdtmc", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse pDTMC") .def("_as_sparse_mdp", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse MDP") + .def("_as_sparse_exact_mdp", [](ModelBase &modelbase) { + return modelbase.as>(); + }, "Get model as sparse exact MDP") .def("_as_sparse_pmdp", [](ModelBase &modelbase) { return modelbase.as>(); }, "Get model as sparse pMDP") @@ -171,90 +177,94 @@ void define_model(py::module& m) { // Bindings for sparse models -void define_sparse_model(py::module& m) { +template +void define_sparse_model(py::module& m, std::string const& vtSuffix) { // Models with double numbers - py::class_, std::shared_ptr>, ModelBase> model(m, "_SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix"); - model.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?") - .def_property_readonly("choice_origins", [](SparseModel const& model) {return model.getChoiceOrigins();}) - .def("labels_state", &SparseModel::getLabelsOfState, py::arg("state"), "Get labels of state") - .def_property_readonly("initial_states", &getSparseInitialStates, "Initial states") - .def_property_readonly("states", [](SparseModel& model) { - return SparseModelStates(model); + 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") + .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?") + .def_property_readonly("choice_origins", [](SparseModel const& model) {return model.getChoiceOrigins();}) + .def("labels_state", &SparseModel::getLabelsOfState, py::arg("state"), "Get labels of state") + .def_property_readonly("initial_states", &getSparseInitialStates, "Initial states") + .def_property_readonly("states", [](SparseModel& model) { + return SparseModelStates(model); }, "Get states") - .def_property_readonly("reward_models", [](SparseModel& model) {return model.getRewardModels(); }, "Reward models") - .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") - .def_property_readonly("backward_transition_matrix", &SparseModel::getBackwardTransitions, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") - .def("get_reward_model", [](SparseModel& model, std::string const& name) {return model.getRewardModel(name);}, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Reward model") - .def("has_state_valuations", [](SparseModel const& model) {return model.hasStateValuations();}, "has state valuation?") - .def_property_readonly("state_valuations", [](SparseModel const& model) {return model.getStateValuations();}, "state valuations") - .def("reduce_to_state_based_rewards", &SparseModel::reduceToStateBasedRewards) - .def("is_sink_state", &SparseModel::isSinkState, py::arg("state")) + .def_property_readonly("reward_models", [](SparseModel& model) {return model.getRewardModels(); }, "Reward models") + .def_property_readonly("transition_matrix", &getTransitionMatrix, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") + .def_property_readonly("backward_transition_matrix", &SparseModel::getBackwardTransitions, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") + .def("get_reward_model", [](SparseModel& model, std::string const& name) {return model.getRewardModel(name);}, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Reward model") + .def("has_state_valuations", [](SparseModel const& model) {return model.hasStateValuations();}, "has state valuation?") + .def_property_readonly("state_valuations", [](SparseModel const& model) {return model.getStateValuations();}, "state valuations") + .def("reduce_to_state_based_rewards", &SparseModel::reduceToStateBasedRewards) + .def("is_sink_state", &SparseModel::isSinkState, py::arg("state")) .def("__str__", &getModelInfoPrinter) - .def("to_dot", [](SparseModel& model) { std::stringstream ss; model.writeDotToStream(ss); return ss.str(); }, "Write dot to a string") + .def("to_dot", [](SparseModel& model) { std::stringstream ss; model.writeDotToStream(ss); return ss.str(); }, "Write dot to a string") ; - py::class_, std::shared_ptr>>(m, "SparseDtmc", "DTMC in sparse representation", model) - .def(py::init>(), py::arg("other_model")) - .def(py::init const&>(), py::arg("components")) + py::class_, std::shared_ptr>>(m, ("Sparse" + vtSuffix + "Dtmc").c_str(), "DTMC in sparse representation", model) + .def(py::init>(), py::arg("other_model")) + .def(py::init const&>(), py::arg("components")) .def("__str__", &getModelInfoPrinter) ; - py::class_, std::shared_ptr>> mdp(m, "SparseMdp", "MDP in sparse representation", model); - mdp.def(py::init>(), py::arg("other_model")) - .def(py::init const&, storm::models::ModelType>(), py::arg("components"), py::arg("type")=storm::models::ModelType::Mdp) - .def_property_readonly("nondeterministic_choice_indices", [](SparseMdp const& mdp) { return mdp.getNondeterministicChoiceIndices(); }) - .def("get_nr_available_actions", [](SparseMdp const& mdp, uint64_t stateIndex) { return mdp.getNondeterministicChoiceIndices()[stateIndex+1] - mdp.getNondeterministicChoiceIndices()[stateIndex] ; }, py::arg("state")) - .def("get_choice_index", [](SparseMdp const& mdp, uint64_t state, uint64_t actOff) { return mdp.getNondeterministicChoiceIndices()[state]+actOff; }, py::arg("state"), py::arg("action_offset"), "gets the choice index for the offset action from the given state.") - .def("apply_scheduler", [](SparseMdp const& mdp, storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { return mdp.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true) + py::class_, std::shared_ptr>> mdp(m, ("Sparse" + vtSuffix + "Mdp").c_str(), "MDP in sparse representation", model); + mdp.def(py::init>(), py::arg("other_model")) + .def(py::init const&, storm::models::ModelType>(), py::arg("components"), py::arg("type")=storm::models::ModelType::Mdp) + .def_property_readonly("nondeterministic_choice_indices", [](SparseMdp const& mdp) { return mdp.getNondeterministicChoiceIndices(); }) + .def("get_nr_available_actions", [](SparseMdp const& mdp, uint64_t stateIndex) { return mdp.getNondeterministicChoiceIndices()[stateIndex+1] - mdp.getNondeterministicChoiceIndices()[stateIndex] ; }, py::arg("state")) + .def("get_choice_index", [](SparseMdp const& mdp, uint64_t state, uint64_t actOff) { return mdp.getNondeterministicChoiceIndices()[state]+actOff; }, py::arg("state"), py::arg("action_offset"), "gets the choice index for the offset action from the given state.") + .def("apply_scheduler", [](SparseMdp const& mdp, storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { return mdp.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true) .def("__str__", &getModelInfoPrinter) ; - py::class_, std::shared_ptr>>(m, "SparsePomdp", "POMDP in sparse representation", mdp) - .def(py::init>(), py::arg("other_model")) - .def(py::init const&, bool>(), py::arg("components"), py::arg("canonic_flag")=false) + py::class_, std::shared_ptr>>(m, ("Sparse" + vtSuffix + "Pomdp").c_str(), "POMDP in sparse representation", mdp) + .def(py::init>(), py::arg("other_model")) + .def(py::init const&, bool>(), py::arg("components"), py::arg("canonic_flag")=false) .def("__str__", &getModelInfoPrinter) - .def("get_observation", &SparsePomdp::getObservation, py::arg("state")) - .def_property_readonly("observations", &SparsePomdp::getObservations) - .def_property_readonly("nr_observations", &SparsePomdp::getNrObservations) - .def("has_observation_valuations", &SparsePomdp::hasObservationValuations) - .def_property_readonly("observation_valuations", &SparsePomdp::getObservationValuations) + .def("get_observation", &SparsePomdp::getObservation, py::arg("state")) + .def_property_readonly("observations", &SparsePomdp::getObservations) + .def_property_readonly("nr_observations", &SparsePomdp::getNrObservations) + .def("has_observation_valuations", &SparsePomdp::hasObservationValuations) + .def_property_readonly("observation_valuations", &SparsePomdp::getObservationValuations) ; - py::class_, std::shared_ptr>>(m, "SparseCtmc", "CTMC in sparse representation", model) - .def(py::init>(), py::arg("other_model")) - .def(py::init const&>(), py::arg("components")) - .def_property_readonly("exit_rates", [](SparseCtmc const& ctmc) { return ctmc.getExitRateVector(); }) + py::class_, std::shared_ptr>>(m, ("Sparse" + vtSuffix + "Ctmc").c_str(), "CTMC in sparse representation", model) + .def(py::init>(), py::arg("other_model")) + .def(py::init const&>(), py::arg("components")) + .def_property_readonly("exit_rates", [](SparseCtmc const& ctmc) { return ctmc.getExitRateVector(); }) .def("__str__", &getModelInfoPrinter) ; - py::class_, std::shared_ptr>>(m, "SparseMA", "MA in sparse representation", model) - .def(py::init>(), py::arg("other_model")) - .def(py::init const&>(), py::arg("components")) - .def_property_readonly("exit_rates", [](SparseMarkovAutomaton const& ma) { return ma.getExitRates(); }) - .def_property_readonly("markovian_states", [](SparseMarkovAutomaton const& ma) { return ma.getMarkovianStates(); }) - .def_property_readonly("nondeterministic_choice_indices", [](SparseMarkovAutomaton const& ma) { return ma.getNondeterministicChoiceIndices(); }) - .def("apply_scheduler", [](SparseMarkovAutomaton const& ma, storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { return ma.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true) + py::class_, std::shared_ptr>>(m, ("Sparse" + vtSuffix + "MA").c_str(), "MA in sparse representation", model) + .def(py::init>(), py::arg("other_model")) + .def(py::init const&>(), py::arg("components")) + .def_property_readonly("exit_rates", [](SparseMarkovAutomaton const& ma) { return ma.getExitRates(); }) + .def_property_readonly("markovian_states", [](SparseMarkovAutomaton const& ma) { return ma.getMarkovianStates(); }) + .def_property_readonly("nondeterministic_choice_indices", [](SparseMarkovAutomaton const& ma) { return ma.getNondeterministicChoiceIndices(); }) + .def("apply_scheduler", [](SparseMarkovAutomaton const& ma, storm::storage::Scheduler const& scheduler, bool dropUnreachableStates) { return ma.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true) .def("__str__", &getModelInfoPrinter) - .def_property_readonly("convertible_to_ctmc", &SparseMarkovAutomaton::isConvertibleToCtmc, "Check whether the MA can be converted into a CTMC.") - .def("convert_to_ctmc", &SparseMarkovAutomaton::convertToCtmc, "Convert the MA into a CTMC.") + .def_property_readonly("convertible_to_ctmc", &SparseMarkovAutomaton::isConvertibleToCtmc, "Check whether the MA can be converted into a CTMC.") + .def("convert_to_ctmc", &SparseMarkovAutomaton::convertToCtmc, "Convert the MA into a CTMC.") ; - py::class_>(m, "SparseRewardModel", "Reward structure for sparse models") - .def(py::init> const&, boost::optional> const&, - boost::optional> const&>(), py::arg("optional_state_reward_vector") = boost::none, + py::class_>(m, ("Sparse" + vtSuffix + "RewardModel").c_str(), "Reward structure for sparse models") + .def(py::init> const&, boost::optional> const&, + boost::optional> const&>(), py::arg("optional_state_reward_vector") = boost::none, py::arg("optional_state_action_reward_vector") = boost::none, py::arg("optional_transition_reward_matrix") = boost::none) - .def_property_readonly("has_state_rewards", &SparseRewardModel::hasStateRewards) - .def_property_readonly("has_state_action_rewards", &SparseRewardModel::hasStateActionRewards) - .def_property_readonly("has_transition_rewards", &SparseRewardModel::hasTransitionRewards) - .def_property_readonly("transition_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) - .def_property_readonly("state_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) - .def("get_state_reward", [](SparseRewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) - .def("get_zero_reward_states", &SparseRewardModel::getStatesWithZeroReward, "get states where all rewards are zero", py::arg("transition_matrix")) - .def("get_state_action_reward", [](SparseRewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) - .def_property_readonly("state_action_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) - .def("reduce_to_state_based_rewards", [](SparseRewardModel& rewardModel, storm::storage::SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") + .def_property_readonly("has_state_rewards", &SparseRewardModel::hasStateRewards) + .def_property_readonly("has_state_action_rewards", &SparseRewardModel::hasStateActionRewards) + .def_property_readonly("has_transition_rewards", &SparseRewardModel::hasTransitionRewards) + .def_property_readonly("transition_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) + .def_property_readonly("state_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) + .def("get_state_reward", [](SparseRewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) + .def("get_zero_reward_states", &SparseRewardModel::template getStatesWithZeroReward, "get states where all rewards are zero", py::arg("transition_matrix")) + .def("get_state_action_reward", [](SparseRewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) + .def_property_readonly("state_action_rewards", [](SparseRewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) + .def("reduce_to_state_based_rewards", [](SparseRewardModel& rewardModel, storm::storage::SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") ; +} +void define_sparse_parametric_model(py::module& m) { // Parametric models py::class_, std::shared_ptr>, ModelBase> modelRatFunc(m, "_SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix"); modelRatFunc.def("collect_probability_parameters", &probabilityVariables, "Collect parameters") @@ -393,3 +403,5 @@ 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); diff --git a/src/storage/model.h b/src/storage/model.h index 7643d39..ead0d7f 100644 --- a/src/storage/model.h +++ b/src/storage/model.h @@ -4,7 +4,9 @@ #include "storm/storage/dd/DdType.h" void define_model(py::module& m); -void define_sparse_model(py::module& m); +template +void define_sparse_model(py::module& m, std::string const& vtSuffix); +void define_sparse_parametric_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 228bb60..837615c 100644 --- a/src/storage/model_components.cpp +++ b/src/storage/model_components.cpp @@ -16,36 +16,39 @@ template using SparseRewardModel = storm::models::sparse::St template using SparseModelComponents = storm::storage::sparse::ModelComponents; -// Parametric models, Valuetype: todo +template +void define_sparse_model_components(py::module& m, std::string const& vtSuffix) { -void define_sparse_model_components(py::module& m) { + py::class_, std::shared_ptr>>(m, ("Sparse" + vtSuffix + "ModelComponents").c_str(), "Components required for building a sparse model") - py::class_, std::shared_ptr>>(m, "SparseModelComponents", "Components required for building a sparse model") - - .def(py::init const&, StateLabeling const&, std::unordered_map> const&, + .def(py::init const&, StateLabeling const&, std::unordered_map> const&, bool, boost::optional const&, boost::optional> const&>(), - py::arg("transition_matrix") = SparseMatrix(), py::arg("state_labeling") = storm::models::sparse::StateLabeling(), - py::arg("reward_models") = std::unordered_map>(), py::arg("rate_transitions") = false, + py::arg("transition_matrix") = SparseMatrix(), py::arg("state_labeling") = storm::models::sparse::StateLabeling(), + py::arg("reward_models") = std::unordered_map>(), py::arg("rate_transitions") = false, py::arg("markovian_states") = boost::none, py::arg("player1_matrix") = boost::none) // General components (for all model types) - .def_readwrite("transition_matrix", &SparseModelComponents::transitionMatrix, "The transition matrix") - .def_readwrite("state_labeling", &SparseModelComponents::stateLabeling, "The state labeling") - .def_readwrite("reward_models", &SparseModelComponents::rewardModels, "Reward models associated with the model") - .def_readwrite("choice_labeling", &SparseModelComponents::choiceLabeling, "A list that stores a labeling for each choice") - .def_readwrite("state_valuations", &SparseModelComponents::stateValuations, "A list that stores for each state to which variable valuation it belongs") - .def_readwrite("choice_origins", &SparseModelComponents::choiceOrigins, "Stores for each choice from which parts of the input model description it originates") + .def_readwrite("transition_matrix", &SparseModelComponents::transitionMatrix, "The transition matrix") + .def_readwrite("state_labeling", &SparseModelComponents::stateLabeling, "The state labeling") + .def_readwrite("reward_models", &SparseModelComponents::rewardModels, "Reward models associated with the model") + .def_readwrite("choice_labeling", &SparseModelComponents::choiceLabeling, "A list that stores a labeling for each choice") + .def_readwrite("state_valuations", &SparseModelComponents::stateValuations, "A list that stores for each state to which variable valuation it belongs") + .def_readwrite("choice_origins", &SparseModelComponents::choiceOrigins, "Stores for each choice from which parts of the input model description it originates") // POMDP specific components - .def_readwrite("observability_classes", &SparseModelComponents::observabilityClasses, "The POMDP observations") + .def_readwrite("observability_classes", &SparseModelComponents::observabilityClasses, "The POMDP observations") // Continuous time specific components (CTMCs, Markov Automata): - .def_readwrite("rate_transitions", &SparseModelComponents::rateTransitions, "True iff the transition values (for Markovian choices) are interpreted as rates") - .def_readwrite("exit_rates", &SparseModelComponents::exitRates, "The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.") - .def_readwrite("markovian_states", &SparseModelComponents::markovianStates, "A list that stores which states are Markovian (only for Markov Automata)") + .def_readwrite("rate_transitions", &SparseModelComponents::rateTransitions, "True iff the transition values (for Markovian choices) are interpreted as rates") + .def_readwrite("exit_rates", &SparseModelComponents::exitRates, "The exit rate for each state. Must be given for CTMCs and MAs, if rate_transitions is false. Otherwise, it is optional.") + .def_readwrite("markovian_states", &SparseModelComponents::markovianStates, "A list that stores which states are Markovian (only for Markov Automata)") // Stochastic two player game specific components: - .def_readwrite("player1_matrix", &SparseModelComponents::observabilityClasses, "Matrix of player 1 choices (needed for stochastic two player games") + .def_readwrite("player1_matrix", &SparseModelComponents::observabilityClasses, "Matrix of player 1 choices (needed for stochastic two player games") ; } + + +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/model_components.h b/src/storage/model_components.h index 14117a7..badc0c7 100644 --- a/src/storage/model_components.h +++ b/src/storage/model_components.h @@ -3,6 +3,7 @@ #include "common.h" -void define_sparse_model_components(py::module& m); +template +void define_sparse_model_components(py::module& m, std::string const& vtSuffix); #endif /* PYTHON_STORAGE_SPARSEMODELCOMPONENTS_H */ \ No newline at end of file diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp index 97151c3..7480351 100644 --- a/src/storage/scheduler.cpp +++ b/src/storage/scheduler.cpp @@ -36,4 +36,5 @@ 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); \ No newline at end of file diff --git a/src/storage/state.cpp b/src/storage/state.cpp index b13c887..f5ca6cd 100644 --- a/src/storage/state.cpp +++ b/src/storage/state.cpp @@ -1,51 +1,39 @@ #include "state.h" -void define_state(py::module& m) { +template +void define_state(py::module& m, std::string const& vtSuffix) { // SparseModelStates - py::class_>(m, "SparseModelStates", "States in sparse model") - .def("__getitem__", &SparseModelStates::getState) - .def("__len__", &SparseModelStates::getSize) - ; - py::class_>(m, "SparseParametricModelStates", "States in sparse parametric model") - .def("__getitem__", &SparseModelStates::getState) - .def("__len__", &SparseModelStates::getSize) + py::class_>(m, ("Sparse" + vtSuffix + "ModelStates").c_str(), "States in sparse model") + .def("__getitem__", &SparseModelStates::getState) + .def("__len__", &SparseModelStates::getSize) ; + // SparseModelState - py::class_>(m, "SparseModelState", "State in sparse model") - .def("__str__", &SparseModelState::toString) - .def_property_readonly("id", &SparseModelState::getIndex, "Id") - .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") - .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") - .def("__int__",&SparseModelState::getIndex) - ; - py::class_>(m, "SparseParametricModelState", "State in sparse parametric model") - .def("__str__", &SparseModelState::toString) - .def_property_readonly("id", &SparseModelState::getIndex, "Id") - .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") - .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") - .def("__int__",&SparseModelState::getIndex) + py::class_>(m, ("Sparse" + vtSuffix + "ModelState").c_str(), "State in sparse model") + .def("__str__", &SparseModelState::toString) + .def_property_readonly("id", &SparseModelState::getIndex, "Id") + .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") + .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") + .def("__int__",&SparseModelState::getIndex) ; - + // SparseModelActions - py::class_>(m, "SparseModelActions", "Actions for state in sparse model") - .def("__getitem__", &SparseModelActions::getAction) - .def("__len__", &SparseModelActions::getSize) - ; - py::class_>(m, "SparseParametricModelActions", "Actions for state in sparse parametric model") - .def("__getitem__", &SparseModelActions::getAction) - .def("__len__", &SparseModelActions::getSize) + py::class_>(m, ("Sparse" + vtSuffix + "ModelActions").c_str(), "Actions for state in sparse model") + .def("__getitem__", &SparseModelActions::getAction) + .def("__len__", &SparseModelActions::getSize) ; + // SparseModelAction - py::class_>(m, "SparseModelAction", "Action for state in sparse model") - .def("__str__", &SparseModelAction::toString) - .def_property_readonly("id", &SparseModelAction::getIndex, "Id") - .def_property_readonly("transitions", &SparseModelAction::getTransitions, "Get transitions") - ; - py::class_>(m, "SparseParametricModelAction", "Action for state in sparse parametric model") - .def("__str__", &SparseModelAction::toString) - .def_property_readonly("id", &SparseModelAction::getIndex, "Id") - .def_property_readonly("transitions", &SparseModelAction::getTransitions, "Get transitions") + py::class_>(m, ("Sparse" + vtSuffix + "ModelAction").c_str(), "Action for state in sparse model") + .def("__str__", &SparseModelAction::toString) + .def_property_readonly("id", &SparseModelAction::getIndex, "Id") + .def_property_readonly("transitions", &SparseModelAction::getTransitions, "Get transitions") ; } + +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); + diff --git a/src/storage/state.h b/src/storage/state.h index 0e91a11..bbe84eb 100644 --- a/src/storage/state.h +++ b/src/storage/state.h @@ -125,6 +125,7 @@ class SparseModelActions { storm::models::sparse::Model& model; }; -void define_state(py::module& m); +template +void define_state(py::module& m, std::string const& vtSuffix); #endif /* PYTHON_STORAGE_STATE_H_ */