diff --git a/doc/source/installation.rst b/doc/source/installation.rst
index bbdb0e1..74a69ac 100644
--- a/doc/source/installation.rst
+++ b/doc/source/installation.rst
@@ -1,7 +1,18 @@
Installation
***********************
-Before installing stormpy, make sure `storm `_ is installed.
+Requirements
+
+Before installing stormpy, make sure
+
+`pycarl `_
+`storm `_
+
+are both available on your system. To avoid issues, we suggest that both use the same version of `carl `_.
+The simplest way of ensuring this is to first install carl as explained in the `storm installation guide _'.
+You can then install storm and pycarl independently.
+
+
Clone stormpy into any suitable location::
diff --git a/src/common.h b/src/common.h
index b7da720..7fbfb27 100644
--- a/src/common.h
+++ b/src/common.h
@@ -1,10 +1,3 @@
-/*
- * common.h
- *
- * Created on: 15 Apr 2016
- * Author: hbruintjes
- */
-
#pragma once
#include "config.h"
@@ -27,104 +20,3 @@ using namespace pybind11::literals;
PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr)
PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr)
-
-namespace pybind11 {
-namespace detail {
-/**
- * Dummy type caster for handle, so functions can return pybind11 handles directly
- */
-/*template <> class type_caster {
-public:
- bool load(handle src, bool) {
- value = handle(src).inc_ref();
- return true;
- }
-
- static handle cast(handle src, return_value_policy policy, handle parent) {
- switch(policy) {
- case return_value_policy::automatic:
- case return_value_policy::copy:
- case return_value_policy::take_ownership:
- return handle(src);
- case return_value_policy::reference:
- return handle(src).inc_ref();
- case return_value_policy::reference_internal:
- parent.inc_ref();
- return handle(src);
- }
- return handle(src);
- }
- PYBIND11_TYPE_CASTER(handle, _("handle"));
-};*/
-/*
-template struct tuple_caster {
- typedef TupleType type;
- template
- using type_conv = type_caster::type>;
-
- bool load(handle src, bool convert) {
- pybind11::tuple tup(src, true);
- if (!tup.check())
- return false;
-
- return loadItem<0, Keys...>(tup, convert);
- }
-
- static handle cast(const type &src, return_value_policy policy, handle parent) {
- pybind11::tuple tup(sizeof...(Keys));
- if (!castItem<0, Keys...>(tup, src, policy, parent)) {
- return handle();
- }
-
- return tup.release();
- }
-
-private:
- template
- bool loadItem(pybind11::tuple& tup, bool convert) {
- type_conv conv;
- if (!conv.load(tup[N], convert))
- return false;
- std::get(value) = static_cast(conv);
- return loadItem(tup, convert);
- }
-
- template
- bool loadItem(pybind11::tuple& tup, bool convert) {
- type_conv conv;
- if (!conv.load(tup[N], convert))
- return false;
- std::get(value) = static_cast(conv);
- return true;
- }
-
- template
- static bool castItem(pybind11::tuple& tup, const type &src, return_value_policy policy, handle parent) {
- auto obj = type_conv::cast(std::get(src), policy, parent);
- object value_ = object(obj, false);
- if (!obj) {
- return false;
- }
- return castItem(tup, src, policy, parent);
- }
-
- template
- static bool castItem(pybind11::tuple& tu, const type &src, return_value_policy policy, handle parent) {
- auto obj = type_conv::cast(std::get(src), policy, parent);
- object value_ = object(obj, false);
- if (!obj) {
- return false;
- }
- return true;
- }
-};
-
-template struct type_caster>
- : tuple_caster, Types...> { };
-
-template struct type_caster>
- : tuple_caster, Type1, Type2> { };
-*/
-
-}
-}
diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp
index e91907c..003646b 100644
--- a/src/mod_storage.cpp
+++ b/src/mod_storage.cpp
@@ -15,5 +15,6 @@ PYBIND11_PLUGIN(storage) {
define_bitvector(m);
define_model(m);
define_sparse_matrix(m);
+ define_model_instantiator(m);
return m.ptr();
}
diff --git a/src/storage/model.cpp b/src/storage/model.cpp
index c8a8945..f411bd2 100644
--- a/src/storage/model.cpp
+++ b/src/storage/model.cpp
@@ -22,6 +22,14 @@ storm::storage::SparseMatrix& getTransitionMatrix(storm::models::spar
return model.getTransitionMatrix();
}
+std::set probabilityVariables(storm::models::sparse::Model const& model) {
+ return storm::models::sparse::getProbabilityParameters(model);
+}
+
+std::set rewardVariables(storm::models::sparse::Model const& model) {
+ return storm::models::sparse::getRewardParameters(model);
+}
+
// Define python bindings
void define_model(py::module& m) {
@@ -64,7 +72,8 @@ void define_model(py::module& m) {
;
py::class_, std::shared_ptr>> modelRatFunc(m, "SparseParametricModel", "A probabilistic model where transitions are represented by rational functions and saved in a sparse matrix", modelBase);
- modelRatFunc.def("collect_probability_parameters", &storm::models::sparse::getProbabilityParameters, "Collect parameters")
+ modelRatFunc.def("collect_probability_parameters", &probabilityVariables, "Collect parameters")
+ .def("collect_reward_parameters", &rewardVariables, "Collect reward parameters")
.def_property_readonly("labels", [](storm::models::sparse::Model& model) {
return model.getStateLabeling().getLabels();
}, "Labels")
diff --git a/tests/storage/test_model_instantiator.py b/tests/storage/test_model_instantiator.py
new file mode 100644
index 0000000..867b3c8
--- /dev/null
+++ b/tests/storage/test_model_instantiator.py
@@ -0,0 +1,21 @@
+import pycarl
+import stormpy
+import stormpy.logic
+from helpers.helper import get_example_path
+
+class TestModel:
+ def test_instantiate_dtmc(self):
+ program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm"))
+ formulas = stormpy.parse_formulas_for_prism_program("P=? [ F s=5 ]", program)
+ model = stormpy.build_parametric_model(program, formulas[0])
+ parameters = model.collect_probability_parameters()
+ instantiator = stormpy.storage.PdtmcInstantiator(model)
+ point = dict()
+ for p in parameters:
+ point[p] = 0.4
+ instantiated_model = instantiator.instantiate(point)
+ assert instantiated_model.nr_states == model.nr_states
+ assert not instantiated_model.has_parameters
+ for p in parameters:
+ point[p] = 0.5
+ instatiated_model2 = instantiator.instantiate(point)
\ No newline at end of file