sp
/
tempestpy
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

support for exact arithmetic

refactoring
Sebastian Junges 5 years ago
parent
1e6fb8740a
commit
58da4df1c3
24 changed files with 297 additions and 326 deletions
Unified View
  1. 4
      CHANGELOG.md
  2. 12
      lib/stormpy/__init__.py
  3. 5
      lib/stormpy/simulator.py
  4. 10
      src/core/core.cpp
  5. 10
      src/core/modelchecking.cpp
  6. 23
      src/core/simulator.cpp
  7. 3
      src/core/simulator.h
  8. 4
      src/mod_core.cpp
  9. 5
      src/mod_pomdp.cpp
  10. 18
      src/mod_storage.cpp
  11. 59
      src/pomdp/tracker.cpp
  12. 3
      src/pomdp/tracker.h
  13. 14
      src/pomdp/transformations.cpp
  14. 4
      src/storage/distribution.cpp
  15. 1
      src/storage/jani.cpp
  16. 187
      src/storage/matrix.cpp
  17. 5
      src/storage/matrix.h
  18. 140
      src/storage/model.cpp
  19. 4
      src/storage/model.h
  20. 39
      src/storage/model_components.cpp
  21. 3
      src/storage/model_components.h
  22. 3
      src/storage/scheduler.cpp
  23. 64
      src/storage/state.cpp
  24. 3
      src/storage/state.h

4
CHANGELOG.md
View File

@ -4,6 +4,10 @@ Changelog
Version 1.6.x Version 1.6.x
------------- -------------
### Version 1.6.3 (to be released)
- Support for exact arithmetic in models
### Version 1.6.2 (2020/09) ### Version 1.6.2 (2020/09)
Requires storm version >= 1.6.2 and pycarl version >= 2.0.4 Requires storm version >= 1.6.2 and pycarl version >= 2.0.4

12
lib/stormpy/__init__.py
View File

@ -297,9 +297,15 @@ def check_model_sparse(model, property, only_initial_states=False, extract_sched
task.set_produce_schedulers(extract_scheduler) task.set_produce_schedulers(extract_scheduler)
return core._parametric_model_checking_sparse_engine(model, task, environment=environment) return core._parametric_model_checking_sparse_engine(model, task, environment=environment)
else: else:
task = core.CheckTask(formula, only_initial_states) if model.is_exact:
task.set_produce_schedulers(extract_scheduler) task = core.ExactCheckTask(formula, only_initial_states)
return core._model_checking_sparse_engine(model, task, environment=environment) 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()): def check_model_dd(model, property, only_initial_states=False, environment=Environment()):

5
lib/stormpy/simulator.py
View File

@ -93,7 +93,10 @@ class SparseSimulator(Simulator):
def __init__(self, model, seed=None): def __init__(self, model, seed=None):
super().__init__(seed) super().__init__(seed)
self._model = model 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: if seed is not None:
self._engine.set_seed(seed) self._engine.set_seed(seed)
self._state_valuations = None self._state_valuations = None

10
src/core/core.cpp
View File

@ -101,24 +101,28 @@ void define_build(py::module& m) {
// Build model // Build model
m.def("_build_sparse_model_from_symbolic_description", &buildSparseModel<double>, "Build the model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("_build_sparse_model_from_symbolic_description", &buildSparseModel<double>, "Build the model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false);
m.def("_build_sparse_exact_model_from_symbolic_description", &buildSparseModel<storm::RationalNumber>, "Build the model in sparse representation with exact number representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false);
m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel<storm::RationalFunction>, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false); m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel<storm::RationalFunction>, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>(), py::arg("use_jit") = false, py::arg("doctor") = false);
m.def("build_sparse_model_with_options", &buildSparseModelWithOptions<double>, "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_model_with_options", &buildSparseModelWithOptions<double>, "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<storm::RationalNumber>, "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<storm::RationalFunction>, "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_parametric_model_with_options", &buildSparseModelWithOptions<storm::RationalFunction>, "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<storm::dd::DdType::Sylvan, double>, "Build the model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>()); m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, double>, "Build the model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Build the parametric model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>()); m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Build the parametric model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions()); m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
m.def("_build_sparse_exact_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalNumber>, "Build the model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions()); m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel<double>, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = ""); m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel<double>, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = "");
m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options")); m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"));
m.def("make_sparse_model_builder_exact", &storm::api::makeExplicitModelBuilder<storm::RationalNumber>, "Construct a builder instance", py::arg("model_description"), py::arg("options"));
m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options")); m.def("make_sparse_model_builder_parametric", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"));
py::class_<storm::builder::ExplicitModelBuilder<double>>(m, "ExplicitModelBuilder_Double", "Model builder for sparse models") py::class_<storm::builder::ExplicitModelBuilder<double>>(m, "ExplicitModelBuilder", "Model builder for sparse models")
.def("build", &storm::builder::ExplicitModelBuilder<double>::build, "Build the model") .def("build", &storm::builder::ExplicitModelBuilder<double>::build, "Build the model")
.def("export_lookup", &storm::builder::ExplicitModelBuilder<double>::exportExplicitStateLookup, "Export a lookup model") .def("export_lookup", &storm::builder::ExplicitModelBuilder<double>::exportExplicitStateLookup, "Export a lookup model")
; ;
py::class_<storm::builder::ExplicitModelBuilder<storm::RationalFunction>>(m, "ExplicitModelBuilder_RF", "Model builder for sparse models") py::class_<storm::builder::ExplicitModelBuilder<storm::RationalFunction>>(m, "ExplicitParametricModelBuilder", "Model builder for sparse models")
.def("build", &storm::builder::ExplicitModelBuilder<storm::RationalFunction>::build, "Build the model") .def("build", &storm::builder::ExplicitModelBuilder<storm::RationalFunction>::build, "Build the model")
.def("export_lookup", &storm::builder::ExplicitModelBuilder<storm::RationalFunction>::exportExplicitStateLookup, "Export a lookup model") .def("export_lookup", &storm::builder::ExplicitModelBuilder<storm::RationalFunction>::exportExplicitStateLookup, "Export a lookup model")
; ;
@ -164,6 +168,8 @@ void define_export(py::module& m) {
opts.def(py::init<>()); opts.def(py::init<>());
opts.def_readwrite("allow_placeholders", &storm::exporter::DirectEncodingOptions::allowPlaceholders); opts.def_readwrite("allow_placeholders", &storm::exporter::DirectEncodingOptions::allowPlaceholders);
// Export // Export
// TODO make one export_to_drn that infers which of the folliwng to use.
m.def("export_to_drn", &exportDRN<double>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions()); m.def("export_to_drn", &exportDRN<double>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions());
m.def("export_exact_to_drn", &exportDRN<double>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions());
m.def("export_parametric_to_drn", &exportDRN<storm::RationalFunction>, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions()); m.def("export_parametric_to_drn", &exportDRN<storm::RationalFunction>, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::exporter::DirectEncodingOptions());
} }

10
src/core/modelchecking.cpp
View File

@ -66,6 +66,12 @@ void define_modelchecking(py::module& m) {
.def(py::init<storm::logic::Formula const&, bool>(), py::arg("formula"), py::arg("only_initial_states") = false) .def(py::init<storm::logic::Formula const&, bool>(), py::arg("formula"), py::arg("only_initial_states") = false)
.def("set_produce_schedulers", &CheckTask<double>::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true) .def("set_produce_schedulers", &CheckTask<double>::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true)
; ;
// CheckTask
py::class_<CheckTask<storm::RationalNumber>, std::shared_ptr<CheckTask<storm::RationalNumber>>>(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<storm::logic::Formula const&, bool>(), py::arg("formula"), py::arg("only_initial_states") = false)
.def("set_produce_schedulers", &CheckTask<storm::RationalNumber>::setProduceSchedulers, "Set whether schedulers should be produced (if possible)", py::arg("produce_schedulers") = true)
;
py::class_<CheckTask<storm::RationalFunction>, std::shared_ptr<CheckTask<storm::RationalFunction>>>(m, "ParametricCheckTask", "Task for parametric model checking") py::class_<CheckTask<storm::RationalFunction>, std::shared_ptr<CheckTask<storm::RationalFunction>>>(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); //m.def("create_check_task", &storm::api::createTask, "Create task for verification", py::arg("formula"), py::arg("only_initial_states") = false);
.def(py::init<storm::logic::Formula const&, bool>(), py::arg("formula"), py::arg("only_initial_states") = false) .def(py::init<storm::logic::Formula const&, bool>(), py::arg("formula"), py::arg("only_initial_states") = false)
@ -73,8 +79,10 @@ void define_modelchecking(py::module& m) {
; ;
// Model checking // Model checking
m.def("model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine<double>, py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); m.def("_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine<double>, py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment());
m.def("_exact_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine<storm::RationalNumber>, py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment());
m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine<double>, "Perform model checking using the sparse engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine<double>, "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<storm::RationalNumber>, "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<storm::RationalFunction>, "Perform parametric 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<storm::RationalFunction>, "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<storm::dd::DdType::Sylvan, double>, "Perform model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); m.def("_model_checking_dd_engine", &modelCheckingDdEngine<storm::dd::DdType::Sylvan, double>, "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<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Perform parametric model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment()); m.def("_parametric_model_checking_dd_engine", &modelCheckingDdEngine<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Perform parametric model checking using the dd engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment());

23
src/core/simulator.cpp
View File

@ -1,14 +1,17 @@
#include "simulator.h" #include "simulator.h"
#include <storm/simulator/DiscreteTimeSparseModelSimulator.h> #include <storm/simulator/DiscreteTimeSparseModelSimulator.h>
void define_sparse_model_simulator(py::module& m) { template<typename ValueType>
py::class_<storm::simulator::DiscreteTimeSparseModelSimulator<double>> dtsmsd(m, "_DiscreteTimeSparseModelSimulatorDouble", "Simulator for sparse discrete-time models in memory (ValueType = double)"); void define_sparse_model_simulator(py::module& m, std::string const& vtSuffix) {
dtsmsd.def(py::init<storm::models::sparse::Model<double> const&>()); py::class_<storm::simulator::DiscreteTimeSparseModelSimulator<ValueType>> dtsmsd(m, ("_DiscreteTimeSparseModelSimulator" + vtSuffix).c_str(), "Simulator for sparse discrete-time models in memory (ValueType = double)");
dtsmsd.def("set_seed", &storm::simulator::DiscreteTimeSparseModelSimulator<double>::setSeed, py::arg("seed")); dtsmsd.def(py::init<storm::models::sparse::Model<ValueType> const&>());
dtsmsd.def("step", &storm::simulator::DiscreteTimeSparseModelSimulator<double>::step, py::arg("action")); dtsmsd.def("set_seed", &storm::simulator::DiscreteTimeSparseModelSimulator<ValueType>::setSeed, py::arg("seed"));
dtsmsd.def("random_step", &storm::simulator::DiscreteTimeSparseModelSimulator<double>::randomStep); dtsmsd.def("step", &storm::simulator::DiscreteTimeSparseModelSimulator<ValueType>::step, py::arg("action"));
dtsmsd.def("get_last_reward", &storm::simulator::DiscreteTimeSparseModelSimulator<double>::getLastRewards); dtsmsd.def("random_step", &storm::simulator::DiscreteTimeSparseModelSimulator<ValueType>::randomStep);
dtsmsd.def("get_current_state", &storm::simulator::DiscreteTimeSparseModelSimulator<double>::getCurrentState); dtsmsd.def("get_last_reward", &storm::simulator::DiscreteTimeSparseModelSimulator<ValueType>::getLastRewards);
dtsmsd.def("reset_to_initial_state", &storm::simulator::DiscreteTimeSparseModelSimulator<double>::resetToInitial); dtsmsd.def("get_current_state", &storm::simulator::DiscreteTimeSparseModelSimulator<ValueType>::getCurrentState);
dtsmsd.def("reset_to_initial_state", &storm::simulator::DiscreteTimeSparseModelSimulator<ValueType>::resetToInitial);
}
} template void define_sparse_model_simulator<double>(py::module& m, std::string const& vtSuffix);
template void define_sparse_model_simulator<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);

3
src/core/simulator.h
View File

@ -2,4 +2,5 @@
#include "common.h" #include "common.h"
void define_sparse_model_simulator(py::module& m); template<typename ValueType>
void define_sparse_model_simulator(py::module& m, std::string const& vtSuffix);

4
src/mod_core.cpp
View File

@ -34,5 +34,7 @@ PYBIND11_MODULE(core, m) {
define_input(m); define_input(m);
define_graph_constraints(m); define_graph_constraints(m);
define_transformation(m); define_transformation(m);
define_sparse_model_simulator(m); define_sparse_model_simulator<double>(m, "Double");
define_sparse_model_simulator<storm::RationalNumber>(m, "Exact");
} }

5
src/mod_pomdp.cpp
View File

@ -14,11 +14,14 @@ PYBIND11_MODULE(pomdp, m) {
py::options options; py::options options;
options.disable_function_signatures(); options.disable_function_signatures();
#endif #endif
define_tracker(m); define_tracker<double>(m, "Double");
define_tracker<storm::RationalNumber>(m, "Exact");
define_qualitative_policy_search<double>(m, "Double"); define_qualitative_policy_search<double>(m, "Double");
define_qualitative_policy_search_nt(m); define_qualitative_policy_search_nt(m);
define_memory(m); define_memory(m);
define_transformations_nt(m); define_transformations_nt(m);
define_transformations<double>(m, "Double"); define_transformations<double>(m, "Double");
define_transformations<storm::RationalNumber>(m, "Exact");
define_transformations<storm::RationalFunction>(m, "Rf"); define_transformations<storm::RationalFunction>(m, "Rf");
} }

18
src/mod_storage.cpp
View File

@ -28,12 +28,19 @@ PYBIND11_MODULE(storage, m) {
define_bitvector(m); define_bitvector(m);
define_dd<storm::dd::DdType::Sylvan>(m, "Sylvan"); define_dd<storm::dd::DdType::Sylvan>(m, "Sylvan");
define_dd_nt(m); define_dd_nt(m);
define_model(m); define_model(m);
define_sparse_model<double>(m, "");
define_sparse_model<storm::RationalNumber>(m, "Exact");
define_sparse_parametric_model(m);
define_statevaluation(m); define_statevaluation(m);
define_sparse_model(m); define_sparse_matrix<double>(m, "");
define_sparse_matrix(m); define_sparse_matrix<storm::RationalNumber>(m, "Exact");
define_sparse_matrix<storm::RationalFunction>(m, "Parametric");
define_sparse_matrix_nt(m);
define_symbolic_model<storm::dd::DdType::Sylvan>(m, "Sylvan"); define_symbolic_model<storm::dd::DdType::Sylvan>(m, "Sylvan");
define_state(m); define_state<double>(m, "");
define_state<storm::RationalNumber>(m, "Exact");
define_prism(m); define_prism(m);
define_jani(m); define_jani(m);
define_jani_transformers(m); define_jani_transformers(m);
@ -41,6 +48,9 @@ PYBIND11_MODULE(storage, m) {
define_origins(m); define_origins(m);
define_expressions(m); define_expressions(m);
define_scheduler<double>(m, "Double"); define_scheduler<double>(m, "Double");
define_scheduler<storm::RationalNumber>(m, "Exact");
define_distribution<double>(m, "Double"); define_distribution<double>(m, "Double");
define_sparse_model_components(m); define_sparse_model_components<double>(m, "");
define_sparse_model_components<storm::RationalNumber>(m, "Exact");
} }

59
src/pomdp/tracker.cpp
View File

@ -7,39 +7,39 @@
template<typename ValueType> using SparsePomdp = storm::models::sparse::Pomdp<ValueType>; template<typename ValueType> using SparsePomdp = storm::models::sparse::Pomdp<ValueType>;
template<typename ValueType> using SparsePomdpTracker = storm::generator::BeliefSupportTracker<ValueType>; template<typename ValueType> using SparsePomdpTracker = storm::generator::BeliefSupportTracker<ValueType>;
template<typename ValueType> using NDPomdpTrackerSparse = storm::generator::NondeterministicBeliefTracker<double, storm::generator::SparseBeliefState<double>>; template<typename ValueType> using NDPomdpTrackerSparse = storm::generator::NondeterministicBeliefTracker<ValueType, storm::generator::SparseBeliefState<ValueType>>;
template<typename ValueType> using NDPomdpTrackerDense = storm::generator::NondeterministicBeliefTracker<double, storm::generator::ObservationDenseBeliefState<double>>; template<typename ValueType> using NDPomdpTrackerDense = storm::generator::NondeterministicBeliefTracker<ValueType, storm::generator::ObservationDenseBeliefState<ValueType>>;
template<typename ValueType>
void define_tracker(py::module& m, std::string const& vtSuffix) {
void define_tracker(py::module& m) { py::class_<storm::generator::BeliefSupportTracker<ValueType>> tracker(m, ("BeliefSupportTracker" + vtSuffix).c_str(), "Tracker for BeliefSupports");
py::class_<storm::generator::BeliefSupportTracker<double>> tracker(m, "BeliefSupportTrackerDouble", "Tracker for BeliefSupports"); tracker.def(py::init<SparsePomdp<ValueType> const&>(), py::arg("pomdp"));
tracker.def(py::init<SparsePomdp<double> const&>(), py::arg("pomdp")); tracker.def("get_current_belief_support", &SparsePomdpTracker<ValueType>::getCurrentBeliefSupport, "What is the support given the trace so far");
tracker.def("get_current_belief_support", &SparsePomdpTracker<double>::getCurrentBeliefSupport, "What is the support given the trace so far"); tracker.def("track", &SparsePomdpTracker<ValueType>::track, py::arg("action"), py::arg("observation"));
tracker.def("track", &SparsePomdpTracker<double>::track, py::arg("action"), py::arg("observation")); py::class_<storm::generator::SparseBeliefState<ValueType>> sbel(m, ("SparseBeliefState" + vtSuffix).c_str(), "Belief state in sparse format");
sbel.def("get", &storm::generator::SparseBeliefState<ValueType>::get, py::arg("state"));
py::class_<storm::generator::SparseBeliefState<double>> sbel(m, "SparseBeliefStateDouble", "Belief state in sparse format"); sbel.def_property_readonly("risk", &storm::generator::SparseBeliefState<ValueType>::getRisk);
sbel.def("get", &storm::generator::SparseBeliefState<double>::get, py::arg("state")); sbel.def("__str__", &storm::generator::SparseBeliefState<ValueType>::toString);
sbel.def_property_readonly("risk", &storm::generator::SparseBeliefState<double>::getRisk); sbel.def_property_readonly("is_valid", &storm::generator::SparseBeliefState<ValueType>::isValid);
sbel.def("__str__", &storm::generator::SparseBeliefState<double>::toString);
sbel.def_property_readonly("is_valid", &storm::generator::SparseBeliefState<double>::isValid);
// //
// py::class_<storm::generator::ObservationDenseBeliefState<double>> dbel(m, "DenseBeliefStateDouble", "Belief state in dense format"); // py::class_<storm::generator::ObservationDenseBeliefState<double>> dbel(m, "DenseBeliefStateDouble", "Belief state in dense format");
// dbel.def("get", &storm::generator::ObservationDenseBeliefState<double>::get, py::arg("state")); // dbel.def("get", &storm::generator::ObservationDenseBeliefState<double>::get, py::arg("state"));
// dbel.def_property_readonly("risk", &storm::generator::ObservationDenseBeliefState<double>::getRisk); // dbel.def_property_readonly("risk", &storm::generator::ObservationDenseBeliefState<double>::getRisk);
// dbel.def("__str__", &storm::generator::ObservationDenseBeliefState<double>::toString); // dbel.def("__str__", &storm::generator::ObservationDenseBeliefState<double>::toString);
py::class_<NDPomdpTrackerSparse<double>> ndetbelieftracker(m, "NondeterministicBeliefTrackerDoubleSparse", "Tracker for belief states and uncontrollable actions"); py::class_<NDPomdpTrackerSparse<ValueType>> ndetbelieftracker(m, ("NondeterministicBeliefTracker" + vtSuffix + "Sparse").c_str(), "Tracker for belief states and uncontrollable actions");
ndetbelieftracker.def(py::init<SparsePomdp<double> const&>(), py::arg("pomdp")); ndetbelieftracker.def(py::init<SparsePomdp<ValueType> const&>(), py::arg("pomdp"));
ndetbelieftracker.def("reset", &NDPomdpTrackerSparse<double>::reset); ndetbelieftracker.def("reset", &NDPomdpTrackerSparse<ValueType>::reset);
ndetbelieftracker.def("set_risk", &NDPomdpTrackerSparse<double>::setRisk, py::arg("risk")); ndetbelieftracker.def("set_risk", &NDPomdpTrackerSparse<ValueType>::setRisk, py::arg("risk"));
ndetbelieftracker.def("obtain_current_risk",&NDPomdpTrackerSparse<double>::getCurrentRisk, py::arg("max")=true); ndetbelieftracker.def("obtain_current_risk",&NDPomdpTrackerSparse<ValueType>::getCurrentRisk, py::arg("max")=true);
ndetbelieftracker.def("track", &NDPomdpTrackerSparse<double>::track, py::arg("observation")); ndetbelieftracker.def("track", &NDPomdpTrackerSparse<ValueType>::track, py::arg("observation"));
ndetbelieftracker.def("obtain_beliefs", &NDPomdpTrackerSparse<double>::getCurrentBeliefs); ndetbelieftracker.def("obtain_beliefs", &NDPomdpTrackerSparse<ValueType>::getCurrentBeliefs);
ndetbelieftracker.def("size", &NDPomdpTrackerSparse<double>::getNumberOfBeliefs); ndetbelieftracker.def("size", &NDPomdpTrackerSparse<ValueType>::getNumberOfBeliefs);
ndetbelieftracker.def("dimension", &NDPomdpTrackerSparse<double>::getCurrentDimension); ndetbelieftracker.def("dimension", &NDPomdpTrackerSparse<ValueType>::getCurrentDimension);
ndetbelieftracker.def("obtain_last_observation", &NDPomdpTrackerSparse<double>::getCurrentObservation); ndetbelieftracker.def("obtain_last_observation", &NDPomdpTrackerSparse<ValueType>::getCurrentObservation);
ndetbelieftracker.def("reduce",&NDPomdpTrackerSparse<double>::reduce); ndetbelieftracker.def("reduce",&NDPomdpTrackerSparse<ValueType>::reduce);
// py::class_<NDPomdpTrackerDense<double>> ndetbelieftrackerd(m, "NondeterministicBeliefTrackerDoubleDense", "Tracker for belief states and uncontrollable actions"); // py::class_<NDPomdpTrackerDense<double>> ndetbelieftrackerd(m, "NondeterministicBeliefTrackerDoubleDense", "Tracker for belief states and uncontrollable actions");
// ndetbelieftrackerd.def(py::init<SparsePomdp<double> const&>(), py::arg("pomdp")); // ndetbelieftrackerd.def(py::init<SparsePomdp<double> const&>(), py::arg("pomdp"));
@ -51,4 +51,7 @@ void define_tracker(py::module& m) {
// ndetbelieftrackerd.def("obtain_last_observation", &NDPomdpTrackerDense<double>::getCurrentObservation); // ndetbelieftrackerd.def("obtain_last_observation", &NDPomdpTrackerDense<double>::getCurrentObservation);
// ndetbelieftrackerd.def("reduce",&NDPomdpTrackerDense<double>::reduce); // ndetbelieftrackerd.def("reduce",&NDPomdpTrackerDense<double>::reduce);
} }
template void define_tracker<double>(py::module& m, std::string const& vtSuffix);
template void define_tracker<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);

3
src/pomdp/tracker.h
View File

@ -1,4 +1,5 @@
#pragma once #pragma once
#include "common.h" #include "common.h"
void define_tracker(py::module& m); template<typename ValueType>
void define_tracker(py::module& m, std::string const& vtSuffix);

14
src/pomdp/transformations.cpp
View File

@ -46,13 +46,6 @@ void define_transformations_nt(py::module &m) {
.value("full", storm::transformer::PomdpFscApplicationMode::FULL) .value("full", storm::transformer::PomdpFscApplicationMode::FULL)
; ;
py::class_<storm::pomdp::ObservationTraceUnfolder<double>> unfolder(m, "ObservationTraceUnfolderDouble", "Unfolds observation traces in models");
unfolder.def(py::init<storm::models::sparse::Pomdp<double> const&, std::vector<double> const&, std::shared_ptr<storm::expressions::ExpressionManager>&>(), py::arg("model"), py::arg("risk"), py::arg("expression_manager"));
unfolder.def("transform", &storm::pomdp::ObservationTraceUnfolder<double>::transform, py::arg("trace"));
unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder<double>::extend, py::arg("new_observation"));
unfolder.def("reset", &storm::pomdp::ObservationTraceUnfolder<double>::reset, py::arg("new_observation"));
} }
template<typename ValueType> template<typename ValueType>
@ -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<ValueType>, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR); m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc<ValueType>, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR);
//m.def(("_unfold_trace_" + vtSuffix).c_str(), &unfold_trace<ValueType>, "Unfold observed trace", py::arg("pomdp"), py::arg("expression_manager"),py::arg("observation_trace"), py::arg("risk_definition")); //m.def(("_unfold_trace_" + vtSuffix).c_str(), &unfold_trace<ValueType>, "Unfold observed trace", py::arg("pomdp"), py::arg("expression_manager"),py::arg("observation_trace"), py::arg("risk_definition"));
py::class_<storm::pomdp::ObservationTraceUnfolder<ValueType>> unfolder(m, ("ObservationTraceUnfolder" + vtSuffix).c_str(), "Unfolds observation traces in models");
unfolder.def(py::init<storm::models::sparse::Pomdp<ValueType> const&, std::vector<ValueType> const&, std::shared_ptr<storm::expressions::ExpressionManager>&>(), py::arg("model"), py::arg("risk"), py::arg("expression_manager"));
unfolder.def("transform", &storm::pomdp::ObservationTraceUnfolder<ValueType>::transform, py::arg("trace"));
unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder<ValueType>::extend, py::arg("new_observation"));
unfolder.def("reset", &storm::pomdp::ObservationTraceUnfolder<ValueType>::reset, py::arg("new_observation"));
} }
template void define_transformations<double>(py::module& m, std::string const& vtSuffix); template void define_transformations<double>(py::module& m, std::string const& vtSuffix);
template void define_transformations<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
template void define_transformations<storm::RationalFunction>(py::module& m, std::string const& vtSuffix); template void define_transformations<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);

4
src/storage/distribution.cpp
View File

@ -1,3 +1,4 @@
#include <storm/adapters/RationalNumberAdapter.h>
#include "distribution.h" #include "distribution.h"
#include "src/helpers.h" #include "src/helpers.h"
@ -14,4 +15,5 @@ void define_distribution(py::module& m, std::string vt_suffix) {
} }
template void define_distribution<double>(py::module&, std::string vt_suffix); template void define_distribution<double>(py::module&, std::string vt_suffix);
template void define_distribution<storm::RationalNumber>(py::module&, std::string vt_suffix);

1
src/storage/jani.cpp
View File

@ -140,6 +140,7 @@ void define_jani(py::module& m) {
py::class_<Variable, std::shared_ptr<Variable>> variable(m, "JaniVariable", "A Variable in JANI"); py::class_<Variable, std::shared_ptr<Variable>> variable(m, "JaniVariable", "A Variable in JANI");
variable.def_property_readonly("name", &Variable::getName, "name of constant") 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("expression_variable", &Variable::getExpressionVariable, "expression variable for this variable")
//.def_property_readonly("initial_value_expression", &Variable::getInitialValue)
; ;
py::class_<BoundedIntegerVariable, std::shared_ptr<BoundedIntegerVariable>> bivariable(m, "JaniBoundedIntegerVariable", "A Bounded Integer", variable); py::class_<BoundedIntegerVariable, std::shared_ptr<BoundedIntegerVariable>> bivariable(m, "JaniBoundedIntegerVariable", "A Bounded Integer", variable);

187
src/storage/matrix.cpp
View File

@ -12,30 +12,29 @@ template<typename ValueType> using MatrixEntry = storm::storage::MatrixEntry<ent
using RationalFunction = storm::RationalFunction; using RationalFunction = storm::RationalFunction;
using row_index = unsigned int; using row_index = unsigned int;
void define_sparse_matrix(py::module& m) { void define_sparse_matrix_nt(py::module& m) {
m.def("_topological_sort_double", [](SparseMatrix<double>& matrix, std::vector<uint64_t> 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<storm::RationalFunction>& matrix, std::vector<uint64_t> initial) { return storm::utility::graph::getTopologicalSort(matrix, initial); }, "matrix"_a, "initial"_a, "get topological sort w.r.t. a transition matrix");
}
template<typename ValueType>
void define_sparse_matrix(py::module& m, std::string const& vtSuffix) {
// MatrixEntry // MatrixEntry
py::class_<MatrixEntry<double>>(m, "SparseMatrixEntry", "Entry of sparse matrix") py::class_<MatrixEntry<ValueType>>(m, (vtSuffix + "SparseMatrixEntry").c_str(), "Entry of sparse matrix")
.def("__str__", &streamToString<MatrixEntry<double>>) .def("__str__", &streamToString<MatrixEntry<ValueType>>)
//def_property threw "pointer being freed not allocated" after exiting //def_property threw "pointer being freed not allocated" after exiting
.def("value", &MatrixEntry<double>::getValue, "Value") .def("value", &MatrixEntry<ValueType>::getValue, "Value")
.def("set_value", &MatrixEntry<double>::setValue, py::arg("value"), "Set value") .def("set_value", &MatrixEntry<ValueType>::setValue, py::arg("value"), "Set value")
.def_property_readonly("column", &MatrixEntry<double>::getColumn, "Column") .def_property_readonly("column", &MatrixEntry<ValueType>::getColumn, "Column")
; ;
py::class_<MatrixEntry<RationalFunction>>(m, "ParametricSparseMatrixEntry", "Entry of parametric sparse matrix")
.def("__str__", &streamToString<MatrixEntry<RationalFunction>>)
//def_property threw "pointer being freed not allocated" after exiting
.def("value", &MatrixEntry<RationalFunction>::getValue, "Value")
.def("set_value", &MatrixEntry<RationalFunction>::setValue, py::arg("value"), "Set value")
.def_property_readonly("column", &MatrixEntry<RationalFunction>::getColumn, "Column")
;
// SparseMatrixBuilder // SparseMatrixBuilder
py::class_<SparseMatrixBuilder<double>>(m, "SparseMatrixBuilder", "Builder of sparse matrix") py::class_<SparseMatrixBuilder<ValueType>>(m, ( vtSuffix + "SparseMatrixBuilder").c_str(), "Builder of sparse matrix")
.def(py::init<double, double, double, bool, bool, double>(), "rows"_a = 0, "columns"_a = 0, "entries"_a = 0, "force_dimensions"_a = true, "has_custom_row_grouping"_a = false, "row_groups"_a = 0) .def(py::init<double, double, double, bool, bool, double>(), "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<double>::addNextValue, R"dox( .def("add_next_value", &SparseMatrixBuilder<ValueType>::addNextValue, R"dox(
Sets the matrix entry at the given row and column to the given value. After all entries have been added, 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. 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 :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")) )dox", py::arg("row"), py::arg("column"), py::arg("value"))
.def("new_row_group", &SparseMatrixBuilder<double>::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix") .def("new_row_group", &SparseMatrixBuilder<ValueType>::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix")
.def("build", &SparseMatrixBuilder<double>::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("build", &SparseMatrixBuilder<ValueType>::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<double>::getLastRow, "Get the most recently used row") .def("get_last_row", &SparseMatrixBuilder<ValueType>::getLastRow, "Get the most recently used row")
.def("get_current_row_group_count", &SparseMatrixBuilder<double>::getCurrentRowGroupCount, "Get the current row group count") .def("get_current_row_group_count", &SparseMatrixBuilder<ValueType>::getCurrentRowGroupCount, "Get the current row group count")
.def("get_last_column", &SparseMatrixBuilder<double>::getLastColumn, "the most recently used column") .def("get_last_column", &SparseMatrixBuilder<ValueType>::getLastColumn, "the most recently used column")
.def("replace_columns", &SparseMatrixBuilder<double>::replaceColumns, R"dox( .def("replace_columns", &SparseMatrixBuilder<ValueType>::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<double> 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_<SparseMatrixBuilder<RationalFunction>>(m, "ParametricSparseMatrixBuilder", "Builder of parametric sparse matrix")
.def(py::init<double, double, double, bool, bool, double>(), "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<RationalFunction>::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<RationalFunction>::newRowGroup, py::arg("starting_row"), "Start a new row group in the matrix")
.def("build", &SparseMatrixBuilder<RationalFunction>::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<RationalFunction>::getLastRow, "Get the most recently used row")
.def("get_current_row_group_count", &SparseMatrixBuilder<RationalFunction>::getCurrentRowGroupCount, "Get the current row group count")
.def("get_last_column", &SparseMatrixBuilder<RationalFunction>::getLastColumn, "the most recently used column")
.def("replace_columns", &SparseMatrixBuilder<RationalFunction>::replaceColumns, R"dox(
Replaces all columns with id >= offset according to replacements. 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. 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 // SparseMatrix
py::class_<SparseMatrix<double>>(m, "SparseMatrix", "Sparse matrix") py::class_<SparseMatrix<ValueType>>(m, (vtSuffix + "SparseMatrix").c_str(), "Sparse matrix")
.def("__iter__", [](SparseMatrix<double>& matrix) { .def("__iter__", [](SparseMatrix<ValueType>& matrix) {
return py::make_iterator(matrix.begin(), matrix.end()); return py::make_iterator(matrix.begin(), matrix.end());
}, py::keep_alive<0, 1>() /* Essential: keep object alive while iterator exists */) }, py::keep_alive<0, 1>() /* Essential: keep object alive while iterator exists */)
.def("__str__", &streamToString<SparseMatrix<double>>) .def("__str__", &streamToString<SparseMatrix<ValueType>>)
.def_property_readonly("nr_rows", &SparseMatrix<double>::getRowCount, "Number of rows") .def_property_readonly("nr_rows", &SparseMatrix<ValueType>::getRowCount, "Number of rows")
.def_property_readonly("nr_columns", &SparseMatrix<double>::getColumnCount, "Number of columns") .def_property_readonly("nr_columns", &SparseMatrix<ValueType>::getColumnCount, "Number of columns")
.def_property_readonly("nr_entries", &SparseMatrix<double>::getEntryCount, "Number of non-zero entries") .def_property_readonly("nr_entries", &SparseMatrix<ValueType>::getEntryCount, "Number of non-zero entries")
.def_property_readonly("_row_group_indices", &SparseMatrix<double>::getRowGroupIndices, "Starting rows of row groups") .def_property_readonly("_row_group_indices", &SparseMatrix<ValueType>::getRowGroupIndices, "Starting rows of row groups")
.def("get_row_group_start", [](SparseMatrix<ValueType>& matrix, entry_index<ValueType> row) {return matrix.getRowGroupIndices()[row];})
.def("get_row_group_start", [](SparseMatrix<double>& matrix, entry_index<double> row) {return matrix.getRowGroupIndices()[row];}) .def("get_row_group_end", [](SparseMatrix<ValueType>& matrix, entry_index<ValueType> row) {return matrix.getRowGroupIndices()[row+1];})
.def("get_row_group_end", [](SparseMatrix<double>& matrix, entry_index<double> row) {return matrix.getRowGroupIndices()[row+1];}) .def_property_readonly("has_trivial_row_grouping", &SparseMatrix<ValueType>::hasTrivialRowGrouping, "Trivial row grouping")
.def_property_readonly("has_trivial_row_grouping", &SparseMatrix<double>::hasTrivialRowGrouping, "Trivial row grouping") .def("get_row", [](SparseMatrix<ValueType>& matrix, entry_index<ValueType> row) {
.def("get_row", [](SparseMatrix<double>& matrix, entry_index<double> row) {
return matrix.getRows(row, row+1); return matrix.getRows(row, row+1);
}, py::return_value_policy::reference, py::keep_alive<1, 0>(), py::arg("row"), "Get row") }, py::return_value_policy::reference, py::keep_alive<1, 0>(), py::arg("row"), "Get row")
.def("get_rows", [](SparseMatrix<double>& matrix, entry_index<double> start, entry_index<double> end) { .def("get_rows", [](SparseMatrix<ValueType>& matrix, entry_index<ValueType> start, entry_index<ValueType> end) {
return matrix.getRows(start, 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") }, 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<double> const& matrix, entry_index<double> row) { .def("print_row", [](SparseMatrix<ValueType> const& matrix, entry_index<ValueType> row) {
std::stringstream stream; std::stringstream stream;
auto rows = matrix.getRows(row, row+1); auto rows = matrix.getRows(row, row+1);
for (auto transition : rows) { for (auto transition : rows) {
@ -126,22 +92,22 @@ void define_sparse_matrix(py::module& m) {
} }
return stream.str(); return stream.str();
}, py::arg("row"), "Print rows from start to end") }, py::arg("row"), "Print rows from start to end")
.def("submatrix", [](SparseMatrix<double> const& matrix, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalEntries = false) { .def("submatrix", [](SparseMatrix<ValueType> const& matrix, storm::storage::BitVector const& rowConstraint, storm::storage::BitVector const& columnConstraint, bool insertDiagonalEntries = false) {
return matrix.getSubmatrix(true, rowConstraint, columnConstraint, insertDiagonalEntries); return matrix.getSubmatrix(true, rowConstraint, columnConstraint, insertDiagonalEntries);
}, py::arg("row_constraint"), py::arg("column_constraint"), py::arg("insert_diagonal_entries") = false, "Get submatrix") }, py::arg("row_constraint"), py::arg("column_constraint"), py::arg("insert_diagonal_entries") = false, "Get submatrix")
// Entry_index lead to problems // Entry_index lead to problems
.def("row_iter", [](SparseMatrix<double>& matrix, row_index start, row_index end) { .def("row_iter", [](SparseMatrix<ValueType>& matrix, row_index start, row_index end) {
return py::make_iterator(matrix.begin(start), matrix.end(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") }, 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] // (partial) container interface to allow e.g. matrix[7:9]
.def("__len__", &SparseMatrix<double>::getRowCount) .def("__len__", &SparseMatrix<ValueType>::getRowCount)
.def("__getitem__", [](SparseMatrix<double>& matrix, entry_index<double> i) { .def("__getitem__", [](SparseMatrix<ValueType>& matrix, entry_index<ValueType> i) {
if (i >= matrix.getRowCount()) if (i >= matrix.getRowCount())
throw py::index_error(); throw py::index_error();
return matrix.getRows(i, i+1); return matrix.getRows(i, i+1);
}, py::return_value_policy::reference, py::keep_alive<1, 0>()) }, py::return_value_policy::reference, py::keep_alive<1, 0>())
.def("__getitem__", [](SparseMatrix<double>& matrix, py::slice slice) { .def("__getitem__", [](SparseMatrix<ValueType>& matrix, py::slice slice) {
size_t start, stop, step, slice_length; size_t start, stop, step, slice_length;
if (!slice.compute(matrix.getRowCount(), &start, &stop, &step, &slice_length)) if (!slice.compute(matrix.getRowCount(), &start, &stop, &step, &slice_length))
throw py::error_already_set(); 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>()) }, py::return_value_policy::reference, py::keep_alive<1, 0>())
; ;
m.def("_topological_sort_double", [](SparseMatrix<double>& matrix, std::vector<uint64_t> 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<storm::RationalFunction>& matrix, std::vector<uint64_t> initial) { return storm::utility::graph::getTopologicalSort(matrix, initial); }, "matrix"_a, "initial"_a, "get topological sort w.r.t. a transition matrix");
py::class_<SparseMatrix<RationalFunction>>(m, "ParametricSparseMatrix", "Parametric sparse matrix")
.def("__iter__", [](SparseMatrix<RationalFunction>& matrix) {
return py::make_iterator(matrix.begin(), matrix.end());
}, py::keep_alive<0, 1>() /* Essential: keep object alive while iterator exists */)
.def("__str__", &streamToString<SparseMatrix<RationalFunction>>)
.def_property_readonly("nr_rows", &SparseMatrix<RationalFunction>::getRowCount, "Number of rows")
.def_property_readonly("nr_columns", &SparseMatrix<RationalFunction>::getColumnCount, "Number of columns")
.def_property_readonly("nr_entries", &SparseMatrix<RationalFunction>::getEntryCount, "Number of non-zero entries")
.def_property_readonly("_row_group_indices", &SparseMatrix<RationalFunction>::getRowGroupIndices, "Starting rows of row groups")
.def("get_row_group_start", [](SparseMatrix<RationalFunction>& matrix, entry_index<RationalFunction> row) {return matrix.getRowGroupIndices()[row];})
.def("get_row_group_end", [](SparseMatrix<RationalFunction>& matrix, entry_index<RationalFunction> row) {return matrix.getRowGroupIndices()[row+1];})
.def_property_readonly("has_trivial_row_grouping", &SparseMatrix<RationalFunction>::hasTrivialRowGrouping, "Trivial row grouping")
.def("get_row", [](SparseMatrix<RationalFunction>& matrix, entry_index<RationalFunction> 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<RationalFunction>& matrix, entry_index<storm::RationalFunction> start, entry_index<storm::RationalFunction> 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<RationalFunction> const& matrix, entry_index<storm::RationalFunction> 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<RationalFunction> 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<RationalFunction>& 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<RationalFunction>::getRowCount)
.def("__getitem__", [](SparseMatrix<RationalFunction>& matrix, entry_index<RationalFunction> 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<RationalFunction>& 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 // Rows
py::class_<SparseMatrix<double>::rows>(m, "SparseMatrixRows", "Set of rows in a sparse matrix") py::class_<typename SparseMatrix<ValueType>::rows>(m, (vtSuffix + "SparseMatrixRows").c_str(), "Set of rows in a sparse matrix")
.def("__iter__", [](SparseMatrix<double>::rows& rows) { .def("__iter__", [](typename SparseMatrix<ValueType>::rows& rows) {
return py::make_iterator(rows.begin(), rows.end());
}, py::keep_alive<0, 1>())
.def("__str__", &containerToString<SparseMatrix<double>::rows>)
.def("__len__", &storm::storage::SparseMatrix<double>::rows::getNumberOfEntries)
;
py::class_<SparseMatrix<RationalFunction>::rows>(m, "ParametricSparseMatrixRows", "Set of rows in a parametric sparse matrix")
.def("__iter__", [](SparseMatrix<RationalFunction>::rows& rows) {
return py::make_iterator(rows.begin(), rows.end()); return py::make_iterator(rows.begin(), rows.end());
}, py::keep_alive<0, 1>()) }, py::keep_alive<0, 1>())
.def("__str__", &containerToString<SparseMatrix<RationalFunction>::rows>) .def("__str__", &containerToString<typename SparseMatrix<ValueType>::rows>)
.def("__len__", &storm::storage::SparseMatrix<storm::RationalFunction>::rows::getNumberOfEntries) .def("__len__", &storm::storage::SparseMatrix<ValueType>::rows::getNumberOfEntries)
; ;
} }
template void define_sparse_matrix<double>(py::module& m, std::string const& vtSuffix);
template void define_sparse_matrix<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
template void define_sparse_matrix<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);

5
src/storage/matrix.h
View File

@ -3,6 +3,9 @@
#include "common.h" #include "common.h"
void define_sparse_matrix(py::module& m); template<typename ValueType>
void define_sparse_matrix(py::module& m, std::string const& vtSuffix);
void define_sparse_matrix_nt(py::module& m);
#endif /* PYTHON_STORAGE_MATRIX_H_ */ #endif /* PYTHON_STORAGE_MATRIX_H_ */

140
src/storage/model.cpp
View File

@ -115,12 +115,18 @@ void define_model(py::module& m) {
.def("_as_sparse_dtmc", [](ModelBase &modelbase) { .def("_as_sparse_dtmc", [](ModelBase &modelbase) {
return modelbase.as<SparseDtmc<double>>(); return modelbase.as<SparseDtmc<double>>();
}, "Get model as sparse DTMC") }, "Get model as sparse DTMC")
.def("_as_sparse_exact_dtmc", [](ModelBase &modelbase) {
return modelbase.as<SparseDtmc<storm::RationalNumber>>();
}, "Get model as sparse DTMC")
.def("_as_sparse_pdtmc", [](ModelBase &modelbase) { .def("_as_sparse_pdtmc", [](ModelBase &modelbase) {
return modelbase.as<SparseDtmc<RationalFunction>>(); return modelbase.as<SparseDtmc<RationalFunction>>();
}, "Get model as sparse pDTMC") }, "Get model as sparse pDTMC")
.def("_as_sparse_mdp", [](ModelBase &modelbase) { .def("_as_sparse_mdp", [](ModelBase &modelbase) {
return modelbase.as<SparseMdp<double>>(); return modelbase.as<SparseMdp<double>>();
}, "Get model as sparse MDP") }, "Get model as sparse MDP")
.def("_as_sparse_exact_mdp", [](ModelBase &modelbase) {
return modelbase.as<SparseMdp<storm::RationalNumber>>();
}, "Get model as sparse exact MDP")
.def("_as_sparse_pmdp", [](ModelBase &modelbase) { .def("_as_sparse_pmdp", [](ModelBase &modelbase) {
return modelbase.as<SparseMdp<RationalFunction>>(); return modelbase.as<SparseMdp<RationalFunction>>();
}, "Get model as sparse pMDP") }, "Get model as sparse pMDP")
@ -171,90 +177,94 @@ void define_model(py::module& m) {
// Bindings for sparse models // Bindings for sparse models
void define_sparse_model(py::module& m) { template<typename ValueType>
void define_sparse_model(py::module& m, std::string const& vtSuffix) {
// Models with double numbers // Models with double numbers
py::class_<SparseModel<double>, std::shared_ptr<SparseModel<double>>, ModelBase> model(m, "_SparseModel", "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix"); py::class_<SparseModel<ValueType>, std::shared_ptr<SparseModel<ValueType>>, ModelBase> model(m, ("_Sparse" + vtSuffix + "Model").c_str(),
model.def_property_readonly("labeling", &getLabeling<double>, "Labels") "A probabilistic model where transitions are represented by doubles and saved in a sparse matrix");
.def("has_choice_labeling", [](SparseModel<double> const& model) {return model.hasChoiceLabeling();}, "Does the model have an associated choice labelling?") model.def_property_readonly("labeling", &getLabeling<ValueType>, "Labels")
.def_property_readonly("choice_labeling", [](SparseModel<double> const& model) {return model.getChoiceLabeling();}, "get choice labelling") .def("has_choice_labeling", [](SparseModel<ValueType> const& model) {return model.hasChoiceLabeling();}, "Does the model have an associated choice labelling?")
.def("has_choice_origins", [](SparseModel<double> const& model) {return model.hasChoiceOrigins();}, "has choice origins?") .def_property_readonly("choice_labeling", [](SparseModel<ValueType> const& model) {return model.getChoiceLabeling();}, "get choice labelling")
.def_property_readonly("choice_origins", [](SparseModel<double> const& model) {return model.getChoiceOrigins();}) .def("has_choice_origins", [](SparseModel<ValueType> const& model) {return model.hasChoiceOrigins();}, "has choice origins?")
.def("labels_state", &SparseModel<double>::getLabelsOfState, py::arg("state"), "Get labels of state") .def_property_readonly("choice_origins", [](SparseModel<ValueType> const& model) {return model.getChoiceOrigins();})
.def_property_readonly("initial_states", &getSparseInitialStates<double>, "Initial states") .def("labels_state", &SparseModel<ValueType>::getLabelsOfState, py::arg("state"), "Get labels of state")
.def_property_readonly("states", [](SparseModel<double>& model) { .def_property_readonly("initial_states", &getSparseInitialStates<ValueType>, "Initial states")
return SparseModelStates<double>(model); .def_property_readonly("states", [](SparseModel<ValueType>& model) {
return SparseModelStates<ValueType>(model);
}, "Get states") }, "Get states")
.def_property_readonly("reward_models", [](SparseModel<double>& model) {return model.getRewardModels(); }, "Reward models") .def_property_readonly("reward_models", [](SparseModel<ValueType>& model) {return model.getRewardModels(); }, "Reward models")
.def_property_readonly("transition_matrix", &getTransitionMatrix<double>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix") .def_property_readonly("transition_matrix", &getTransitionMatrix<ValueType>, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Transition matrix")
.def_property_readonly("backward_transition_matrix", &SparseModel<double>::getBackwardTransitions, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix") .def_property_readonly("backward_transition_matrix", &SparseModel<ValueType>::getBackwardTransitions, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Backward transition matrix")
.def("get_reward_model", [](SparseModel<double>& model, std::string const& name) {return model.getRewardModel(name);}, py::return_value_policy::reference, py::keep_alive<1, 0>(), "Reward model") .def("get_reward_model", [](SparseModel<ValueType>& 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<double> const& model) {return model.hasStateValuations();}, "has state valuation?") .def("has_state_valuations", [](SparseModel<ValueType> const& model) {return model.hasStateValuations();}, "has state valuation?")
.def_property_readonly("state_valuations", [](SparseModel<double> const& model) {return model.getStateValuations();}, "state valuations") .def_property_readonly("state_valuations", [](SparseModel<ValueType> const& model) {return model.getStateValuations();}, "state valuations")
.def("reduce_to_state_based_rewards", &SparseModel<double>::reduceToStateBasedRewards) .def("reduce_to_state_based_rewards", &SparseModel<ValueType>::reduceToStateBasedRewards)
.def("is_sink_state", &SparseModel<double>::isSinkState, py::arg("state")) .def("is_sink_state", &SparseModel<ValueType>::isSinkState, py::arg("state"))
.def("__str__", &getModelInfoPrinter) .def("__str__", &getModelInfoPrinter)
.def("to_dot", [](SparseModel<double>& model) { std::stringstream ss; model.writeDotToStream(ss); return ss.str(); }, "Write dot to a string") .def("to_dot", [](SparseModel<ValueType>& model) { std::stringstream ss; model.writeDotToStream(ss); return ss.str(); }, "Write dot to a string")
; ;
py::class_<SparseDtmc<double>, std::shared_ptr<SparseDtmc<double>>>(m, "SparseDtmc", "DTMC in sparse representation", model) py::class_<SparseDtmc<ValueType>, std::shared_ptr<SparseDtmc<ValueType>>>(m, ("Sparse" + vtSuffix + "Dtmc").c_str(), "DTMC in sparse representation", model)
.def(py::init<SparseDtmc<double>>(), py::arg("other_model")) .def(py::init<SparseDtmc<ValueType>>(), py::arg("other_model"))
.def(py::init<ModelComponents<double> const&>(), py::arg("components")) .def(py::init<ModelComponents<ValueType> const&>(), py::arg("components"))
.def("__str__", &getModelInfoPrinter) .def("__str__", &getModelInfoPrinter)
; ;
py::class_<SparseMdp<double>, std::shared_ptr<SparseMdp<double>>> mdp(m, "SparseMdp", "MDP in sparse representation", model); py::class_<SparseMdp<ValueType>, std::shared_ptr<SparseMdp<ValueType>>> mdp(m, ("Sparse" + vtSuffix + "Mdp").c_str(), "MDP in sparse representation", model);
mdp.def(py::init<SparseMdp<double>>(), py::arg("other_model")) mdp.def(py::init<SparseMdp<ValueType>>(), py::arg("other_model"))
.def(py::init<ModelComponents<double> const&, storm::models::ModelType>(), py::arg("components"), py::arg("type")=storm::models::ModelType::Mdp) .def(py::init<ModelComponents<ValueType> const&, storm::models::ModelType>(), py::arg("components"), py::arg("type")=storm::models::ModelType::Mdp)
.def_property_readonly("nondeterministic_choice_indices", [](SparseMdp<double> const& mdp) { return mdp.getNondeterministicChoiceIndices(); }) .def_property_readonly("nondeterministic_choice_indices", [](SparseMdp<ValueType> const& mdp) { return mdp.getNondeterministicChoiceIndices(); })
.def("get_nr_available_actions", [](SparseMdp<double> const& mdp, uint64_t stateIndex) { return mdp.getNondeterministicChoiceIndices()[stateIndex+1] - mdp.getNondeterministicChoiceIndices()[stateIndex] ; }, py::arg("state")) .def("get_nr_available_actions", [](SparseMdp<ValueType> const& mdp, uint64_t stateIndex) { return mdp.getNondeterministicChoiceIndices()[stateIndex+1] - mdp.getNondeterministicChoiceIndices()[stateIndex] ; }, py::arg("state"))
.def("get_choice_index", [](SparseMdp<double> 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("get_choice_index", [](SparseMdp<ValueType> 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<double> const& mdp, storm::storage::Scheduler<double> const& scheduler, bool dropUnreachableStates) { return mdp.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true) .def("apply_scheduler", [](SparseMdp<ValueType> const& mdp, storm::storage::Scheduler<ValueType> const& scheduler, bool dropUnreachableStates) { return mdp.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true)
.def("__str__", &getModelInfoPrinter) .def("__str__", &getModelInfoPrinter)
; ;
py::class_<SparsePomdp<double>, std::shared_ptr<SparsePomdp<double>>>(m, "SparsePomdp", "POMDP in sparse representation", mdp) py::class_<SparsePomdp<ValueType>, std::shared_ptr<SparsePomdp<ValueType>>>(m, ("Sparse" + vtSuffix + "Pomdp").c_str(), "POMDP in sparse representation", mdp)
.def(py::init<SparsePomdp<double>>(), py::arg("other_model")) .def(py::init<SparsePomdp<ValueType>>(), py::arg("other_model"))
.def(py::init<ModelComponents<double> const&, bool>(), py::arg("components"), py::arg("canonic_flag")=false) .def(py::init<ModelComponents<ValueType> const&, bool>(), py::arg("components"), py::arg("canonic_flag")=false)
.def("__str__", &getModelInfoPrinter) .def("__str__", &getModelInfoPrinter)
.def("get_observation", &SparsePomdp<double>::getObservation, py::arg("state")) .def("get_observation", &SparsePomdp<ValueType>::getObservation, py::arg("state"))
.def_property_readonly("observations", &SparsePomdp<double>::getObservations) .def_property_readonly("observations", &SparsePomdp<ValueType>::getObservations)
.def_property_readonly("nr_observations", &SparsePomdp<double>::getNrObservations) .def_property_readonly("nr_observations", &SparsePomdp<ValueType>::getNrObservations)
.def("has_observation_valuations", &SparsePomdp<double>::hasObservationValuations) .def("has_observation_valuations", &SparsePomdp<ValueType>::hasObservationValuations)
.def_property_readonly("observation_valuations", &SparsePomdp<double>::getObservationValuations) .def_property_readonly("observation_valuations", &SparsePomdp<ValueType>::getObservationValuations)
; ;
py::class_<SparseCtmc<double>, std::shared_ptr<SparseCtmc<double>>>(m, "SparseCtmc", "CTMC in sparse representation", model) py::class_<SparseCtmc<ValueType>, std::shared_ptr<SparseCtmc<ValueType>>>(m, ("Sparse" + vtSuffix + "Ctmc").c_str(), "CTMC in sparse representation", model)
.def(py::init<SparseCtmc<double>>(), py::arg("other_model")) .def(py::init<SparseCtmc<ValueType>>(), py::arg("other_model"))
.def(py::init<ModelComponents<double> const&>(), py::arg("components")) .def(py::init<ModelComponents<ValueType> const&>(), py::arg("components"))
.def_property_readonly("exit_rates", [](SparseCtmc<double> const& ctmc) { return ctmc.getExitRateVector(); }) .def_property_readonly("exit_rates", [](SparseCtmc<ValueType> const& ctmc) { return ctmc.getExitRateVector(); })
.def("__str__", &getModelInfoPrinter) .def("__str__", &getModelInfoPrinter)
; ;
py::class_<SparseMarkovAutomaton<double>, std::shared_ptr<SparseMarkovAutomaton<double>>>(m, "SparseMA", "MA in sparse representation", model) py::class_<SparseMarkovAutomaton<ValueType>, std::shared_ptr<SparseMarkovAutomaton<ValueType>>>(m, ("Sparse" + vtSuffix + "MA").c_str(), "MA in sparse representation", model)
.def(py::init<SparseMarkovAutomaton<double>>(), py::arg("other_model")) .def(py::init<SparseMarkovAutomaton<ValueType>>(), py::arg("other_model"))
.def(py::init<ModelComponents<double> const&>(), py::arg("components")) .def(py::init<ModelComponents<ValueType> const&>(), py::arg("components"))
.def_property_readonly("exit_rates", [](SparseMarkovAutomaton<double> const& ma) { return ma.getExitRates(); }) .def_property_readonly("exit_rates", [](SparseMarkovAutomaton<ValueType> const& ma) { return ma.getExitRates(); })
.def_property_readonly("markovian_states", [](SparseMarkovAutomaton<double> const& ma) { return ma.getMarkovianStates(); }) .def_property_readonly("markovian_states", [](SparseMarkovAutomaton<ValueType> const& ma) { return ma.getMarkovianStates(); })
.def_property_readonly("nondeterministic_choice_indices", [](SparseMarkovAutomaton<double> const& ma) { return ma.getNondeterministicChoiceIndices(); }) .def_property_readonly("nondeterministic_choice_indices", [](SparseMarkovAutomaton<ValueType> const& ma) { return ma.getNondeterministicChoiceIndices(); })
.def("apply_scheduler", [](SparseMarkovAutomaton<double> const& ma, storm::storage::Scheduler<double> const& scheduler, bool dropUnreachableStates) { return ma.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true) .def("apply_scheduler", [](SparseMarkovAutomaton<ValueType> const& ma, storm::storage::Scheduler<ValueType> const& scheduler, bool dropUnreachableStates) { return ma.applyScheduler(scheduler, dropUnreachableStates); } , "apply scheduler", "scheduler"_a, "drop_unreachable_states"_a = true)
.def("__str__", &getModelInfoPrinter) .def("__str__", &getModelInfoPrinter)
.def_property_readonly("convertible_to_ctmc", &SparseMarkovAutomaton<double>::isConvertibleToCtmc, "Check whether the MA can be converted into a CTMC.") .def_property_readonly("convertible_to_ctmc", &SparseMarkovAutomaton<ValueType>::isConvertibleToCtmc, "Check whether the MA can be converted into a CTMC.")
.def("convert_to_ctmc", &SparseMarkovAutomaton<double>::convertToCtmc, "Convert the MA into a CTMC.") .def("convert_to_ctmc", &SparseMarkovAutomaton<ValueType>::convertToCtmc, "Convert the MA into a CTMC.")
; ;
py::class_<SparseRewardModel<double>>(m, "SparseRewardModel", "Reward structure for sparse models") py::class_<SparseRewardModel<ValueType>>(m, ("Sparse" + vtSuffix + "RewardModel").c_str(), "Reward structure for sparse models")
.def(py::init<boost::optional<std::vector<double>> const&, boost::optional<std::vector<double>> const&, .def(py::init<boost::optional<std::vector<ValueType>> const&, boost::optional<std::vector<ValueType>> const&,
boost::optional<storm::storage::SparseMatrix<double>> const&>(), py::arg("optional_state_reward_vector") = boost::none, boost::optional<storm::storage::SparseMatrix<ValueType>> 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) py::arg("optional_state_action_reward_vector") = boost::none, py::arg("optional_transition_reward_matrix") = boost::none)
.def_property_readonly("has_state_rewards", &SparseRewardModel<double>::hasStateRewards) .def_property_readonly("has_state_rewards", &SparseRewardModel<ValueType>::hasStateRewards)
.def_property_readonly("has_state_action_rewards", &SparseRewardModel<double>::hasStateActionRewards) .def_property_readonly("has_state_action_rewards", &SparseRewardModel<ValueType>::hasStateActionRewards)
.def_property_readonly("has_transition_rewards", &SparseRewardModel<double>::hasTransitionRewards) .def_property_readonly("has_transition_rewards", &SparseRewardModel<ValueType>::hasTransitionRewards)
.def_property_readonly("transition_rewards", [](SparseRewardModel<double>& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) .def_property_readonly("transition_rewards", [](SparseRewardModel<ValueType>& rewardModel) {return rewardModel.getTransitionRewardMatrix();})
.def_property_readonly("state_rewards", [](SparseRewardModel<double>& rewardModel) {return rewardModel.getStateRewardVector();}) .def_property_readonly("state_rewards", [](SparseRewardModel<ValueType>& rewardModel) {return rewardModel.getStateRewardVector();})
.def("get_state_reward", [](SparseRewardModel<double>& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) .def("get_state_reward", [](SparseRewardModel<ValueType>& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);})
.def("get_zero_reward_states", &SparseRewardModel<double>::getStatesWithZeroReward<double>, "get states where all rewards are zero", py::arg("transition_matrix")) .def("get_zero_reward_states", &SparseRewardModel<ValueType>::template getStatesWithZeroReward<ValueType>, "get states where all rewards are zero", py::arg("transition_matrix"))
.def("get_state_action_reward", [](SparseRewardModel<double>& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) .def("get_state_action_reward", [](SparseRewardModel<ValueType>& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);})
.def_property_readonly("state_action_rewards", [](SparseRewardModel<double>& rewardModel) {return rewardModel.getStateActionRewardVector();}) .def_property_readonly("state_action_rewards", [](SparseRewardModel<ValueType>& rewardModel) {return rewardModel.getStateActionRewardVector();})
.def("reduce_to_state_based_rewards", [](SparseRewardModel<double>& rewardModel, storm::storage::SparseMatrix<double> const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") .def("reduce_to_state_based_rewards", [](SparseRewardModel<ValueType>& rewardModel, storm::storage::SparseMatrix<ValueType> 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 // Parametric models
py::class_<SparseModel<RationalFunction>, std::shared_ptr<SparseModel<RationalFunction>>, ModelBase> modelRatFunc(m, "_SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix"); py::class_<SparseModel<RationalFunction>, std::shared_ptr<SparseModel<RationalFunction>>, 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") 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<storm::dd::DdType::Sylvan>(py::module& m, std::string vt_suffix); template void define_symbolic_model<storm::dd::DdType::Sylvan>(py::module& m, std::string vt_suffix);
template void define_sparse_model<double>(py::module& m, std::string const& vt_suffix);
template void define_sparse_model<storm::RationalNumber>(py::module& m, std::string const& vt_suffix);

4
src/storage/model.h
View File

@ -4,7 +4,9 @@
#include "storm/storage/dd/DdType.h" #include "storm/storage/dd/DdType.h"
void define_model(py::module& m); void define_model(py::module& m);
void define_sparse_model(py::module& m); template<typename ValueType>
void define_sparse_model(py::module& m, std::string const& vtSuffix);
void define_sparse_parametric_model(py::module& m);
template<storm::dd::DdType DdType> template<storm::dd::DdType DdType>
void define_symbolic_model(py::module& m, std::string vt_suffix); void define_symbolic_model(py::module& m, std::string vt_suffix);

39
src/storage/model_components.cpp
View File

@ -16,36 +16,39 @@ template<typename ValueType> using SparseRewardModel = storm::models::sparse::St
template<typename ValueType> using SparseModelComponents = storm::storage::sparse::ModelComponents<ValueType>; template<typename ValueType> using SparseModelComponents = storm::storage::sparse::ModelComponents<ValueType>;
// Parametric models, Valuetype: <storm::RationalFunction> todo template<typename ValueType>
void define_sparse_model_components(py::module& m, std::string const& vtSuffix) {
void define_sparse_model_components(py::module& m) { py::class_<SparseModelComponents<ValueType>, std::shared_ptr<SparseModelComponents<ValueType>>>(m, ("Sparse" + vtSuffix + "ModelComponents").c_str(), "Components required for building a sparse model")
py::class_<SparseModelComponents<double>, std::shared_ptr<SparseModelComponents<double>>>(m, "SparseModelComponents", "Components required for building a sparse model") .def(py::init<SparseMatrix<ValueType> const&, StateLabeling const&, std::unordered_map<std::string, SparseRewardModel<ValueType>> const&,
.def(py::init<SparseMatrix<double> const&, StateLabeling const&, std::unordered_map<std::string, SparseRewardModel<double>> const&,
bool, boost::optional<BitVector> const&, boost::optional<SparseMatrix<storm::storage::sparse::state_type>> const&>(), bool, boost::optional<BitVector> const&, boost::optional<SparseMatrix<storm::storage::sparse::state_type>> const&>(),
py::arg("transition_matrix") = SparseMatrix<double>(), py::arg("state_labeling") = storm::models::sparse::StateLabeling(), py::arg("transition_matrix") = SparseMatrix<ValueType>(), py::arg("state_labeling") = storm::models::sparse::StateLabeling(),
py::arg("reward_models") = std::unordered_map<std::string, SparseRewardModel<double>>(), py::arg("rate_transitions") = false, py::arg("reward_models") = std::unordered_map<std::string, SparseRewardModel<ValueType>>(), py::arg("rate_transitions") = false,
py::arg("markovian_states") = boost::none, py::arg("player1_matrix") = boost::none) py::arg("markovian_states") = boost::none, py::arg("player1_matrix") = boost::none)
// General components (for all model types) // General components (for all model types)
.def_readwrite("transition_matrix", &SparseModelComponents<double>::transitionMatrix, "The transition matrix") .def_readwrite("transition_matrix", &SparseModelComponents<ValueType>::transitionMatrix, "The transition matrix")
.def_readwrite("state_labeling", &SparseModelComponents<double>::stateLabeling, "The state labeling") .def_readwrite("state_labeling", &SparseModelComponents<ValueType>::stateLabeling, "The state labeling")
.def_readwrite("reward_models", &SparseModelComponents<double>::rewardModels, "Reward models associated with the model") .def_readwrite("reward_models", &SparseModelComponents<ValueType>::rewardModels, "Reward models associated with the model")
.def_readwrite("choice_labeling", &SparseModelComponents<double>::choiceLabeling, "A list that stores a labeling for each choice") .def_readwrite("choice_labeling", &SparseModelComponents<ValueType>::choiceLabeling, "A list that stores a labeling for each choice")
.def_readwrite("state_valuations", &SparseModelComponents<double>::stateValuations, "A list that stores for each state to which variable valuation it belongs") .def_readwrite("state_valuations", &SparseModelComponents<ValueType>::stateValuations, "A list that stores for each state to which variable valuation it belongs")
.def_readwrite("choice_origins", &SparseModelComponents<double>::choiceOrigins, "Stores for each choice from which parts of the input model description it originates") .def_readwrite("choice_origins", &SparseModelComponents<ValueType>::choiceOrigins, "Stores for each choice from which parts of the input model description it originates")
// POMDP specific components // POMDP specific components
.def_readwrite("observability_classes", &SparseModelComponents<double>::observabilityClasses, "The POMDP observations") .def_readwrite("observability_classes", &SparseModelComponents<ValueType>::observabilityClasses, "The POMDP observations")
// Continuous time specific components (CTMCs, Markov Automata): // Continuous time specific components (CTMCs, Markov Automata):
.def_readwrite("rate_transitions", &SparseModelComponents<double>::rateTransitions, "True iff the transition values (for Markovian choices) are interpreted as rates") .def_readwrite("rate_transitions", &SparseModelComponents<ValueType>::rateTransitions, "True iff the transition values (for Markovian choices) are interpreted as rates")
.def_readwrite("exit_rates", &SparseModelComponents<double>::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("exit_rates", &SparseModelComponents<ValueType>::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<double>::markovianStates, "A list that stores which states are Markovian (only for Markov Automata)") .def_readwrite("markovian_states", &SparseModelComponents<ValueType>::markovianStates, "A list that stores which states are Markovian (only for Markov Automata)")
// Stochastic two player game specific components: // Stochastic two player game specific components:
.def_readwrite("player1_matrix", &SparseModelComponents<double>::observabilityClasses, "Matrix of player 1 choices (needed for stochastic two player games") .def_readwrite("player1_matrix", &SparseModelComponents<ValueType>::observabilityClasses, "Matrix of player 1 choices (needed for stochastic two player games")
; ;
} }
template void define_sparse_model_components<double>(py::module& m, std::string const& vtSuffix);
template void define_sparse_model_components<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);

3
src/storage/model_components.h
View File

@ -3,6 +3,7 @@
#include "common.h" #include "common.h"
void define_sparse_model_components(py::module& m); template<typename ValueType>
void define_sparse_model_components(py::module& m, std::string const& vtSuffix);
#endif /* PYTHON_STORAGE_SPARSEMODELCOMPONENTS_H */ #endif /* PYTHON_STORAGE_SPARSEMODELCOMPONENTS_H */

3
src/storage/scheduler.cpp
View File

@ -36,4 +36,5 @@ void define_scheduler(py::module& m, std::string vt_suffix) {
} }
template void define_scheduler<double>(py::module& m, std::string vt_suffix); template void define_scheduler<double>(py::module& m, std::string vt_suffix);
template void define_scheduler<storm::RationalNumber>(py::module& m, std::string vt_suffix);

64
src/storage/state.cpp
View File

@ -1,51 +1,39 @@
#include "state.h" #include "state.h"
void define_state(py::module& m) { template<typename ValueType>
void define_state(py::module& m, std::string const& vtSuffix) {
// SparseModelStates // SparseModelStates
py::class_<SparseModelStates<double>>(m, "SparseModelStates", "States in sparse model") py::class_<SparseModelStates<ValueType>>(m, ("Sparse" + vtSuffix + "ModelStates").c_str(), "States in sparse model")
.def("__getitem__", &SparseModelStates<double>::getState) .def("__getitem__", &SparseModelStates<ValueType>::getState)
.def("__len__", &SparseModelStates<double>::getSize) .def("__len__", &SparseModelStates<ValueType>::getSize)
;
py::class_<SparseModelStates<storm::RationalFunction>>(m, "SparseParametricModelStates", "States in sparse parametric model")
.def("__getitem__", &SparseModelStates<storm::RationalFunction>::getState)
.def("__len__", &SparseModelStates<storm::RationalFunction>::getSize)
; ;
// SparseModelState // SparseModelState
py::class_<SparseModelState<double>>(m, "SparseModelState", "State in sparse model") py::class_<SparseModelState<ValueType>>(m, ("Sparse" + vtSuffix + "ModelState").c_str(), "State in sparse model")
.def("__str__", &SparseModelState<double>::toString) .def("__str__", &SparseModelState<ValueType>::toString)
.def_property_readonly("id", &SparseModelState<double>::getIndex, "Id") .def_property_readonly("id", &SparseModelState<ValueType>::getIndex, "Id")
.def_property_readonly("labels", &SparseModelState<double>::getLabels, "Labels") .def_property_readonly("labels", &SparseModelState<ValueType>::getLabels, "Labels")
.def_property_readonly("actions", &SparseModelState<double>::getActions, "Get actions") .def_property_readonly("actions", &SparseModelState<ValueType>::getActions, "Get actions")
.def("__int__",&SparseModelState<double>::getIndex) .def("__int__",&SparseModelState<ValueType>::getIndex)
;
py::class_<SparseModelState<storm::RationalFunction>>(m, "SparseParametricModelState", "State in sparse parametric model")
.def("__str__", &SparseModelState<storm::RationalFunction>::toString)
.def_property_readonly("id", &SparseModelState<storm::RationalFunction>::getIndex, "Id")
.def_property_readonly("labels", &SparseModelState<storm::RationalFunction>::getLabels, "Labels")
.def_property_readonly("actions", &SparseModelState<storm::RationalFunction>::getActions, "Get actions")
.def("__int__",&SparseModelState<storm::RationalFunction>::getIndex)
; ;
// SparseModelActions // SparseModelActions
py::class_<SparseModelActions<double>>(m, "SparseModelActions", "Actions for state in sparse model") py::class_<SparseModelActions<ValueType>>(m, ("Sparse" + vtSuffix + "ModelActions").c_str(), "Actions for state in sparse model")
.def("__getitem__", &SparseModelActions<double>::getAction) .def("__getitem__", &SparseModelActions<ValueType>::getAction)
.def("__len__", &SparseModelActions<double>::getSize) .def("__len__", &SparseModelActions<ValueType>::getSize)
;
py::class_<SparseModelActions<storm::RationalFunction>>(m, "SparseParametricModelActions", "Actions for state in sparse parametric model")
.def("__getitem__", &SparseModelActions<storm::RationalFunction>::getAction)
.def("__len__", &SparseModelActions<storm::RationalFunction>::getSize)
; ;
// SparseModelAction // SparseModelAction
py::class_<SparseModelAction<double>>(m, "SparseModelAction", "Action for state in sparse model") py::class_<SparseModelAction<ValueType>>(m, ("Sparse" + vtSuffix + "ModelAction").c_str(), "Action for state in sparse model")
.def("__str__", &SparseModelAction<double>::toString) .def("__str__", &SparseModelAction<ValueType>::toString)
.def_property_readonly("id", &SparseModelAction<double>::getIndex, "Id") .def_property_readonly("id", &SparseModelAction<ValueType>::getIndex, "Id")
.def_property_readonly("transitions", &SparseModelAction<double>::getTransitions, "Get transitions") .def_property_readonly("transitions", &SparseModelAction<ValueType>::getTransitions, "Get transitions")
;
py::class_<SparseModelAction<storm::RationalFunction>>(m, "SparseParametricModelAction", "Action for state in sparse parametric model")
.def("__str__", &SparseModelAction<storm::RationalFunction>::toString)
.def_property_readonly("id", &SparseModelAction<storm::RationalFunction>::getIndex, "Id")
.def_property_readonly("transitions", &SparseModelAction<storm::RationalFunction>::getTransitions, "Get transitions")
; ;
} }
template void define_state<double>(py::module& m, std::string const& vtSuffix);
template void define_state<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
template void define_state<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);

3
src/storage/state.h
View File

@ -125,6 +125,7 @@ class SparseModelActions {
storm::models::sparse::Model<ValueType>& model; storm::models::sparse::Model<ValueType>& model;
}; };
void define_state(py::module& m); template<typename ValueType>
void define_state(py::module& m, std::string const& vtSuffix);
#endif /* PYTHON_STORAGE_STATE_H_ */ #endif /* PYTHON_STORAGE_STATE_H_ */
Write Preview
|||||||
100:0
Loading…
Cancel
Save