Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/stormpy

doc/source/installation.rst

@@ -1,7 +1,18 @@
 Installation
 ***********************
 
-Before installing stormpy, make sure `storm <https://moves-rwth.github.io/storm/>`_ is installed.
+Requirements
+
+Before installing stormpy, make sure 
+
+`pycarl <https://moves-rwth.github.io/pycarl>`_ 
+`storm <https://moves-rwth.github.io/storm/>`_ 
+
+are both available on your system. To avoid issues, we suggest that both use the same version of `carl <https://smtrat.github.io/carl>`_. 
+The simplest way of ensuring this is to first install carl as explained in the `storm installation guide <https://moves-rwth.github.io/storm/documentation/installation.md#carl>_'.
+You can then install storm and pycarl independently.
+
+
 
 Clone stormpy into any suitable location::
 

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<T>)
 PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr<T const>)
-
-namespace pybind11 {
-namespace detail {
-/**
- * Dummy type caster for handle, so functions can return pybind11 handles directly
- */
-/*template <> class type_caster<handle> {
-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 <typename TupleType, typename ... Keys> struct tuple_caster {
-    typedef TupleType type;
-    template<typename Type>
-    using type_conv = type_caster<typename intrinsic_type<Type>::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<int N, typename Type, typename ... Types>
-    bool loadItem(pybind11::tuple& tup, bool convert) {
-        type_conv<Type> conv;
-        if (!conv.load(tup[N], convert))
-                return false;
-        std::get<N>(value) = static_cast<Type>(conv);
-        return loadItem<N+1, Types...>(tup, convert);
-    }
-
-    template<int N, typename Type>
-    bool loadItem(pybind11::tuple& tup, bool convert) {
-        type_conv<Type> conv;
-        if (!conv.load(tup[N], convert))
-                return false;
-        std::get<N>(value) = static_cast<Type>(conv);
-        return true;
-    }
-
-    template<int N, typename Type, typename ... Types>
-    static bool castItem(pybind11::tuple& tup, const type &src, return_value_policy policy, handle parent) {
-        auto obj = type_conv<Type>::cast(std::get<N>(src), policy, parent);
-        object value_ = object(obj, false);
-        if (!obj) {
-            return false;
-        }
-        return castItem<N+1, Types...>(tup, src, policy, parent);
-    }
-
-    template<int N, typename Type>
-    static bool castItem(pybind11::tuple& tu, const type &src, return_value_policy policy, handle parent) {
-        auto obj = type_conv<Type>::cast(std::get<N>(src), policy, parent);
-        object value_ = object(obj, false);
-        if (!obj) {
-            return false;
-        }
-        return true;
-    }
-};
-
-template <typename ... Types> struct type_caster<std::tuple<Types...>>
- : tuple_caster<std::tuple<Types...>, Types...> { };
-
-template <typename Type1, typename Type2> struct type_caster<std::pair<Type1, Type2>>
- : tuple_caster<std::pair<Type1, Type2>, Type1, Type2> { };
-*/
-
-}
-}

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();
 }

src/storage/model.cpp

@@ -22,6 +22,14 @@ storm::storage::SparseMatrix<ValueType>& getTransitionMatrix(storm::models::spar
     return model.getTransitionMatrix();
 }
 
+std::set<storm::RationalFunctionVariable> probabilityVariables(storm::models::sparse::Model<storm::RationalFunction> const& model) {
+    return storm::models::sparse::getProbabilityParameters(model);
+}
+
+std::set<storm::RationalFunctionVariable> rewardVariables(storm::models::sparse::Model<storm::RationalFunction> 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_<storm::models::sparse::Model<storm::RationalFunction>, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>>> 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<storm::RationalFunction>& model) {
                 return model.getStateLabeling().getLabels();
             }, "Labels")

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)