From 3396141e13d61ecbee7e200f2a8360cf65ab71fd Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 3 Jan 2017 11:06:02 +0100 Subject: [PATCH 1/4] updated installation docu --- doc/source/installation.rst | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) 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:: From 7133a4e79ebf93cecf7721729402717016e1de7f Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 3 Jan 2017 11:39:36 +0100 Subject: [PATCH 2/4] some support for getting parameters --- src/mod_storage.cpp | 1 + src/storage/model.cpp | 11 ++++++++++- 2 files changed, 11 insertions(+), 1 deletion(-) 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") From 32eae51b16f03a98751d2b06bdb979033ba29b77 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 3 Jan 2017 11:40:13 +0100 Subject: [PATCH 3/4] first working test for model instantiator --- tests/storage/test_model_instantiator.py | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 tests/storage/test_model_instantiator.py 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 From 01a529b46fd4af3fd19488f93e5e569e6ee9fc7e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 3 Jan 2017 11:40:38 +0100 Subject: [PATCH 4/4] cleaned the common.h --- src/common.h | 108 --------------------------------------------------- 1 file changed, 108 deletions(-) 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> { }; -*/ - -} -}