Python bindings for storm-pars

CMakeLists.txt

@@ -6,7 +6,7 @@ option(STORMPY_DISABLE_SIGNATURE_DOC "disables the signature in the documentatio
 find_package(storm REQUIRED)
 add_subdirectory(resources/pybind11)
 
-configure_file(${CMAKE_CURRENT_SOURCE_DIR}/src/config.h.in ${CMAKE_CURRENT_BINARY_DIR}/src/generated/config.h) 
+configure_file(${CMAKE_CURRENT_SOURCE_DIR}/src/config.h.in ${CMAKE_CURRENT_BINARY_DIR}/src/generated/config.h)
 
 message(STATUS "STORM-DIR: ${storm_DIR}")
 set(STORMPY_LIB_DIR "${CMAKE_SOURCE_DIR}/lib/stormpy" CACHE STRING "Sets the storm library dir")
@@ -49,8 +49,10 @@ stormpy_module(logic)
 stormpy_module(storage)
 stormpy_module(utility)
 
+if(HAVE_STORM_PARS)
+    stormpy_module(pars "${STORMPY_LIB_DIR}/pars" storm-pars "${storm-pars_INCLUDE_DIR}")
+endif()
+
 if(HAVE_STORM_DFT)
     stormpy_module(dft "${STORMPY_LIB_DIR}/dft" storm-dft "${storm-dft_INCLUDE_DIR}")
 endif()
-
-

cmake/CMakeLists.txt

@@ -2,6 +2,15 @@ cmake_minimum_required(VERSION 3.0.0)
 project(storm-version)
 find_package(storm REQUIRED)
 
+# Check for storm-pars
+if(EXISTS "${storm_DIR}/lib/libstorm-pars.dylib")
+    set(HAVE_STORM_PARS TRUE)
+elseif(EXISTS "${storm_DIR}/lib/libstorm-pars.so")
+    set(HAVE_STORM_PARS TRUE)
+else()
+    set(HAVE_STORM_PARS FALSE)
+endif()
+
 # Check for storm-dft
 if(EXISTS "${storm_DIR}/lib/libstorm-dft.dylib")
     set(HAVE_STORM_DFT TRUE)
@@ -15,6 +24,12 @@ endif()
 set(STORM_DIR ${storm_DIR})
 set(STORM_VERSION ${storm_VERSION})
 
+if(HAVE_STORM_PARS)
+    set(HAVE_STORM_PARS_BOOL "True")
+else()
+    set(HAVE_STORM_PARS_BOOL "False")
+endif()
+
 if(HAVE_STORM_DFT)
     set(HAVE_STORM_DFT_BOOL "True")
 else()

cmake/config.py.in

@@ -1,7 +1,8 @@
-# Auto-generated by Cmake.
+# Auto-generated by CMake.
 
 STORM_DIR = "@STORM_DIR@"
 STORM_VERSION = "@STORM_VERSION@"
 STORM_CLN_EA = @STORM_CLN_EA_BOOL@
 STORM_CLN_RF = @STORM_CLN_RF_BOOL@
+HAVE_STORM_PARS = @HAVE_STORM_PARS_BOOL@
 HAVE_STORM_DFT = @HAVE_STORM_DFT_BOOL@

lib/.gitignore

@@ -1,4 +1,6 @@
 *.so
 __pycache__/
 stormpy.egg-info/
+stormpy/_config.py
 stormpy/dft/_config.py
+stormpy/pars/_config.py

lib/stormpy/pars/__init__.py

@@ -0,0 +1,9 @@
+from . import _config
+
+if not _config.has_storm_pars:
+    raise ImportError("No support for parametric analysis was built in Storm.")
+
+from . import pars
+from .pars import *
+
+pars._set_up()

setup.py

@@ -106,6 +106,13 @@ class CMakeBuild(build_ext):
                     f.write("storm_version = {}\n".format(self.conf.STORM_VERSION))
                     f.write("storm_cln_ea = {}\n".format(self.conf.STORM_CLN_EA))
                     f.write("storm_cln_rf = {}".format(self.conf.STORM_CLN_RF))
+            elif ext.name == "pars":
+                with open(os.path.join(self.extdir(ext.name),  ext.subdir, "_config.py"), "w") as f:
+                    f.write("# Generated from setup.py at {}\n".format(datetime.datetime.now()))
+                    f.write("has_storm_pars = {}".format(self.conf.HAVE_STORM_PARS))
+                if not self.conf.HAVE_STORM_PARS:
+                    print("WARNING: storm-pars not found. No support for parametric analysis will be built.")
+                    continue
             elif ext.name == "dft":
                 with open(os.path.join(self.extdir(ext.name),  ext.subdir, "_config.py"), "w") as f:
                     f.write("# Generated from setup.py at {}\n".format(datetime.datetime.now()))
@@ -141,6 +148,8 @@ class CMakeBuild(build_ext):
         cmake_args += ['-DCMAKE_BUILD_TYPE=' + build_type]
         if self.conf.STORM_DIR is not None:
             cmake_args += ['-Dstorm_DIR=' + self.conf.STORM_DIR]
+        if self.conf.HAVE_STORM_PARS:
+            cmake_args += ['-DHAVE_STORM_PARS=ON']
         if self.conf.HAVE_STORM_DFT:
             cmake_args += ['-DHAVE_STORM_DFT=ON']
 
@@ -172,7 +181,8 @@ setup(
     maintainer_email="sebastian.junges@cs.rwth-aachen.de",
     url="http://moves.rwth-aachen.de",
     description="stormpy - Python Bindings for Storm",
-    packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility', 'stormpy.dft'],
+    packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic', 'stormpy.storage', 'stormpy.utility',
+              'stormpy.pars', 'stormpy.dft'],
     package_dir={'': 'lib'},
     ext_package='stormpy',
     ext_modules=[CMakeExtension('core', subdir=''),
@@ -181,7 +191,8 @@ setup(
                  CMakeExtension('logic', subdir='logic'),
                  CMakeExtension('storage', subdir='storage'),
                  CMakeExtension('utility', subdir='utility'),
-                 CMakeExtension('dft', subdir='dft')
+                 CMakeExtension('pars', subdir='pars'),
+                 CMakeExtension('dft', subdir='dft'),
                  ],
     cmdclass={'build_ext': CMakeBuild, 'test': PyTest},
     zip_safe=False,

src/core/pla.cpp

@@ -1,61 +0,0 @@
-#include "pla.h"
-#include "src/helpers.h"
-#include "storm/modelchecker/parametric/SparseDtmcRegionChecker.h"
-
-typedef storm::modelchecker::parametric::SparseDtmcRegionChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double, storm::RationalNumber> SparseDtmcRegionChecker;
-typedef storm::storage::ParameterRegion<storm::RationalFunction> Region;
-
-// Thin wrappers
-void specifyFormula(std::shared_ptr<SparseDtmcRegionChecker>& checker, std::shared_ptr<const storm::logic::Formula> const& formula) {
-    checker->specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction>(*formula, true));
-}
-storm::modelchecker::parametric::RegionCheckResult checkRegion(std::shared_ptr<SparseDtmcRegionChecker>& checker, Region& region, storm::modelchecker::parametric::RegionCheckResult initialResult, bool sampleVertices) {
-    return checker->analyzeRegion(region, initialResult, sampleVertices);
-}
-
-std::set<storm::Polynomial> gatherDerivatives(storm::models::sparse::Dtmc<storm::RationalFunction> const& model, carl::Variable const& var) {
-    std::set<storm::Polynomial> derivatives;
-    for (auto it : model.getTransitionMatrix()) {
-        storm::Polynomial pol = it.getValue().derivative(var, 1).nominator();
-        if (!pol.isConstant()) {
-            derivatives.insert(pol);
-        }
-    }
-    return derivatives;
-}
-
-// Define python bindings
-void define_pla(py::module& m) {
-
-    // RegionCheckResult
-    py::enum_<storm::modelchecker::parametric::RegionCheckResult>(m, "RegionCheckResult", "Types of region check results")
-        .value("EXISTSSAT", storm::modelchecker::parametric::RegionCheckResult::ExistsSat)
-        .value("EXISTSVIOLATED", storm::modelchecker::parametric::RegionCheckResult::ExistsViolated)
-        .value("EXISTSBOTH", storm::modelchecker::parametric::RegionCheckResult::ExistsBoth)
-        .value("CENTERSAT", storm::modelchecker::parametric::RegionCheckResult::CenterSat)
-        .value("CENTERVIOLATED", storm::modelchecker::parametric::RegionCheckResult::CenterViolated)
-        .value("ALLSAT", storm::modelchecker::parametric::RegionCheckResult::AllSat)
-        .value("ALLVIOLATED", storm::modelchecker::parametric::RegionCheckResult::AllViolated)
-        .value("UNKNOWN", storm::modelchecker::parametric::RegionCheckResult::Unknown)
-        .def("__str__", &streamToString<storm::modelchecker::parametric::RegionCheckResult>)
-    ;
-
-    // Region
-    py::class_<Region, std::shared_ptr<Region>>(m, "ParameterRegion", "Parameter region")
-       .def("__init__", [](Region &instance, std::string const& regionString, std::set<Region::VariableType> const& variables) -> void {
-                new (&instance) Region(Region::parseRegion(regionString, variables));
-            })
-        //.def(py::init<Region::VariableSubstitutionType &, Region::VariableSubstitutionType &>(), py::arg("lowerBounds"), py::arg("upperBounds"))
-    ;
-
-    // RegionChecker
-    py::class_<SparseDtmcRegionChecker, std::shared_ptr<SparseDtmcRegionChecker>>(m, "SparseDtmcRegionChecker", "Region model checker for sparse DTMCs")
-        .def("__init__", [](SparseDtmcRegionChecker& instance, std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model) -> void {
-                new (&instance) SparseDtmcRegionChecker(*model);
-            })
-        .def("specify_formula", &specifyFormula, "Specify formula", py::arg("formula"))
-        .def("check_region", &checkRegion, "Check region", py::arg("region"), py::arg("initialResult") = storm::modelchecker::parametric::RegionCheckResult::Unknown, py::arg("sampleVertices") = false)
-    ;
-
-    m.def("gather_derivatives", &gatherDerivatives, "Gather all derivatives of transition probabilities", py::arg("model"), py::arg("var"));
-}

src/core/pla.h

@@ -1,8 +0,0 @@
-#ifndef PYTHON_CORE_PLA_H_
-#define PYTHON_CORE_PLA_H_
-
-#include "common.h"
-
-void define_pla(py::module& m);
-
-#endif /* PYTHON_CORE_PLA_H_ */

src/mod_core.cpp

@@ -5,16 +5,15 @@
 #include "core/modelchecking.h"
 #include "core/bisimulation.h"
 #include "core/input.h"
-#include "core/pla.h"
 
 PYBIND11_PLUGIN(core) {
     py::module m("core");
-    
+
 #ifdef STORMPY_DISABLE_SIGNATURE_DOC
     py::options options;
 //    options.disable_function_signatures();
 #endif
-    
+
     define_core(m);
     define_property(m);
     define_parse(m);
@@ -25,6 +24,5 @@ PYBIND11_PLUGIN(core) {
     define_modelchecking(m);
     define_bisimulation(m);
     define_input(m);
-    define_pla(m);
     return m.ptr();
 }

src/mod_pars.cpp

@@ -0,0 +1,19 @@
+#include "common.h"
+
+#include "pars/pars.h"
+#include "pars/pla.h"
+#include "pars/model_instantiator.h"
+
+PYBIND11_PLUGIN(pars) {
+    py::module m("pars", "Functionality for parametric analysis");
+
+#ifdef STORMPY_DISABLE_SIGNATURE_DOC
+    py::options options;
+    options.disable_function_signatures();
+#endif
+
+    define_pars(m);
+    define_pla(m);
+    define_model_instantiator(m);
+    return m.ptr();
+}

src/mod_storage.cpp

@@ -18,7 +18,6 @@ PYBIND11_PLUGIN(storage) {
     define_model(m);
     define_sparse_matrix(m);
     define_state(m);
-    define_model_instantiator(m);
     define_labeling(m);
     return m.ptr();
 }

src/pars/common.h

@@ -0,0 +1,3 @@
+#include "src/common.h"
+
+#include "storm-pars/api/storm-pars.h"

src/pars/model_instantiator.cpp

@@ -0,0 +1,29 @@
+#include "model_instantiator.h"
+#include "storm/models/sparse/Model.h"
+
+template<typename ValueType> using Model = storm::models::sparse::Model<ValueType>;
+template<typename ValueType> using Dtmc = storm::models::sparse::Dtmc<ValueType>;
+template<typename ValueType> using Mdp = storm::models::sparse::Mdp<ValueType>;
+template<typename ValueType> using Ctmc = storm::models::sparse::Ctmc<ValueType>;
+template<typename ValueType> using MarkovAutomaton = storm::models::sparse::MarkovAutomaton<ValueType>;
+
+// Model instantiator
+void define_model_instantiator(py::module& m) {
+    py::class_<storm::utility::ModelInstantiator<Dtmc<storm::RationalFunction>, Dtmc<double>>>(m, "PDtmcInstantiator", "Instantiate PDTMCs to DTMCs")
+        .def(py::init<Dtmc<storm::RationalFunction>>(), "parametric model"_a)
+        .def("instantiate", &storm::utility::ModelInstantiator<Dtmc<storm::RationalFunction>, Dtmc<double>>::instantiate, "Instantiate model with given parameter values")
+    ;
+
+    py::class_<storm::utility::ModelInstantiator<Mdp<storm::RationalFunction>,Mdp<double>>>(m, "PMdpInstantiator", "Instantiate PMDPs to MDPs")
+        .def(py::init<Mdp<storm::RationalFunction>>(), "parametric model"_a)
+        .def("instantiate", &storm::utility::ModelInstantiator<Mdp<storm::RationalFunction>, Mdp<double>>::instantiate, "Instantiate model with given parameter values")
+    ;
+
+    py::class_<storm::utility::ModelInstantiator<Ctmc<storm::RationalFunction>,Ctmc<double>>>(m, "PCtmcInstantiator", "Instantiate PCTMCs to CTMCs")
+        .def(py::init<Ctmc<storm::RationalFunction>>(), "parametric model"_a)
+        .def("instantiate", &storm::utility::ModelInstantiator<Ctmc<storm::RationalFunction>, Ctmc<double>>::instantiate, "Instantiate model with given parameter values");
+
+    py::class_<storm::utility::ModelInstantiator<MarkovAutomaton<storm::RationalFunction>,MarkovAutomaton<double>>>(m, "PMaInstantiator", "Instantiate PMAs to MAs")
+        .def(py::init<MarkovAutomaton<storm::RationalFunction>>(), "parametric model"_a)
+        .def("instantiate", &storm::utility::ModelInstantiator<MarkovAutomaton<storm::RationalFunction>, MarkovAutomaton<double>>::instantiate, "Instantiate model with given parameter values");
+}

src/pars/model_instantiator.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_PARS_MODEL_INSTANTIATOR_H_
+#define PYTHON_PARS_MODEL_INSTANTIATOR_H_
+
+#include "common.h"
+
+void define_model_instantiator(py::module& m);
+
+#endif /* PYTHON_PARS_MODEL_INSTANTIATOR_H_ */

src/pars/pars.cpp

@@ -0,0 +1,11 @@
+#include "pars.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm-pars/settings/modules/ParametricSettings.h"
+#include "storm-pars/settings/modules/RegionSettings.h"
+
+void define_pars(py::module& m) {
+    m.def("_set_up", []() {
+            storm::settings::addModule<storm::settings::modules::ParametricSettings>();
+            storm::settings::addModule<storm::settings::modules::RegionSettings>();
+        }, "Initialize Storm-pars");
+}

src/pars/pars.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_PARS_PARS_H_
+#define PYTHON_PARS_PARS_H_
+
+#include "common.h"
+
+void define_pars(py::module& m);
+
+#endif /* PYTHON_PARS_PARS_H_ */

src/pars/pla.cpp

@@ -0,0 +1,70 @@
+#include "pla.h"
+#include "src/helpers.h"
+#include "storm/api/storm.h"
+
+typedef storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double> SparseDtmcRegionChecker;
+typedef storm::modelchecker::RegionModelChecker<storm::RationalFunction> RegionModelChecker;
+typedef storm::storage::ParameterRegion<storm::RationalFunction> Region;
+
+// Thin wrappers
+std::shared_ptr<RegionModelChecker> createRegionChecker(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> const& model, std::shared_ptr<storm::logic::Formula> const& formula) {
+    return storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, storm::api::createTask<storm::RationalFunction>(formula, true));
+}
+
+storm::modelchecker::RegionResult checkRegion(std::shared_ptr<RegionModelChecker>& checker, Region& region, storm::modelchecker::RegionResult initialResult, bool sampleVertices) {
+    return checker->analyzeRegion(region, initialResult, sampleVertices);
+}
+
+std::set<storm::Polynomial> gatherDerivatives(storm::models::sparse::Dtmc<storm::RationalFunction> const& model, carl::Variable const& var) {
+    std::set<storm::Polynomial> derivatives;
+    for (auto it : model.getTransitionMatrix()) {
+        storm::Polynomial pol = it.getValue().derivative(var, 1).nominator();
+        if (!pol.isConstant()) {
+            derivatives.insert(pol);
+        }
+    }
+    return derivatives;
+}
+
+
+
+// Define python bindings
+void define_pla(py::module& m) {
+
+    // RegionResult
+    py::enum_<storm::modelchecker::RegionResult>(m, "RegionResult", "Types of region check results")
+        .value("EXISTSSAT", storm::modelchecker::RegionResult::ExistsSat)
+        .value("EXISTSVIOLATED", storm::modelchecker::RegionResult::ExistsViolated)
+        .value("EXISTSBOTH", storm::modelchecker::RegionResult::ExistsBoth)
+        .value("CENTERSAT", storm::modelchecker::RegionResult::CenterSat)
+        .value("CENTERVIOLATED", storm::modelchecker::RegionResult::CenterViolated)
+        .value("ALLSAT", storm::modelchecker::RegionResult::AllSat)
+        .value("ALLVIOLATED", storm::modelchecker::RegionResult::AllViolated)
+        .value("UNKNOWN", storm::modelchecker::RegionResult::Unknown)
+        .def("__str__", &streamToString<storm::modelchecker::RegionResult>)
+    ;
+
+    // Region
+    py::class_<Region, std::shared_ptr<Region>>(m, "ParameterRegion", "Parameter region")
+       .def("__init__", [](Region &instance, std::string const& regionString, std::set<Region::VariableType> const& variables) -> void {
+                new (&instance) Region(storm::api::parseRegion<storm::RationalFunction>(regionString, variables));
+            })
+    ;
+
+    // RegionModelChecker
+    //py::class_<SparseDtmcRegionChecker, std::shared_ptr<SparseDtmcRegionChecker>>(m, "SparseDtmcRegionChecker", "Region model checker for sparse DTMCs")
+    py::class_<RegionModelChecker, std::shared_ptr<RegionModelChecker>>(m, "RegionModelChecker", "Region model checker via paramater lifting")
+/*        .def("__init__", [](std::unique_ptr<SparseDtmcRegionChecker>& instance, std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> model, storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> const& task) -> void {
+                // Better use storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, task);
+                //SparseDtmcRegionChecker tmp;
+                //tmp.specify(model, task);
+                auto tmp = storm::api::initializeParameterLiftingRegionModelChecker<storm::RationalFunction, double>(model, task);
+                new (&instance) std::unique_ptr<SparseDtmcRegionChecker>(tmp);
+            }, py::arg("model"), py::arg("task")*/
+        .def("check_region", &checkRegion, "Check region", py::arg("region"), py::arg("initialResult") = storm::modelchecker::RegionResult::Unknown, py::arg("sampleVertices") = false)
+    ;
+
+    m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("model"), py::arg("formula"));
+    //m.def("is_parameter_lifting_sound", &storm::utility::parameterlifting::validateParameterLiftingSound, "Check if parameter lifting is sound", py::arg("model"), py::arg("formula"));
+    m.def("gather_derivatives", &gatherDerivatives, "Gather all derivatives of transition probabilities", py::arg("model"), py::arg("var"));
+}

src/pars/pla.h

@@ -0,0 +1,8 @@
+#ifndef PYTHON_PARS_PLA_H_
+#define PYTHON_PARS_PLA_H_
+
+#include "common.h"
+
+void define_pla(py::module& m);
+
+#endif /* PYTHON_PARS_PLA_H_ */

src/storage/model.cpp

@@ -5,8 +5,9 @@
 #include "storm/models/sparse/Model.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
+#include "storm/models/sparse/Ctmc.h"
+#include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/utility/ModelInstantiator.h"
 
 #include <functional>
 #include <string>
@@ -159,23 +160,3 @@ void define_model(py::module& m) {
 
 }
 
-// Model instantiator
-void define_model_instantiator(py::module& m) {
-    py::class_<storm::utility::ModelInstantiator<Dtmc<RationalFunction>, Dtmc<double>>>(m, "PdtmcInstantiator", "Instantiate PDTMCs to DTMCs")
-        .def(py::init<Dtmc<RationalFunction>>(), "parametric model"_a)
-        .def("instantiate", &storm::utility::ModelInstantiator<Dtmc<RationalFunction>, Dtmc<double>>::instantiate, "Instantiate model with given parameter values")
-    ;
-
-    py::class_<storm::utility::ModelInstantiator<Mdp<RationalFunction>,Mdp<double>>>(m, "PmdpInstantiator", "Instantiate PMDPs to MDPs")
-        .def(py::init<Mdp<RationalFunction>>(), "parametric model"_a)
-        .def("instantiate", &storm::utility::ModelInstantiator<Mdp<RationalFunction>, Mdp<double>>::instantiate, "Instantiate model with given parameter values")
-    ;
-
-    py::class_<storm::utility::ModelInstantiator<Ctmc<storm::RationalFunction>,Ctmc<double>>>(m, "PctmcInstantiator", "Instantiate PCTMCs to CTMCs")
-        .def(py::init<Ctmc<storm::RationalFunction>>(), "parametric model"_a)
-        .def("instantiate", &storm::utility::ModelInstantiator<Ctmc<storm::RationalFunction>, Ctmc<double>>::instantiate, "Instantiate model with given parameter values");
-
-    py::class_<storm::utility::ModelInstantiator<MarkovAutomaton<storm::RationalFunction>,MarkovAutomaton<double>>>(m, "PmaInstantiator", "Instantiate PMAs to MAs")
-        .def(py::init<MarkovAutomaton<storm::RationalFunction>>(), "parametric model"_a)
-        .def("instantiate", &storm::utility::ModelInstantiator<MarkovAutomaton<storm::RationalFunction>, MarkovAutomaton<double>>::instantiate, "Instantiate model with given parameter values");
-}

src/storage/model.h

@@ -4,6 +4,5 @@
 #include "common.h"
 
 void define_model(py::module& m);
-void define_model_instantiator(py::module& m);
 
 #endif /* PYTHON_STORAGE_MODEL_H_ */

tests/storage/test_model_instantiator.py → tests/pars/test_model_instantiator.py

@@ -1,6 +1,7 @@
 import pycarl
 import stormpy
 import stormpy.logic
+import stormpy.pars
 from helpers.helper import get_example_path
 
 
@@ -10,7 +11,7 @@ class TestModel:
         formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program)
         model = stormpy.build_parametric_model(program, formulas)
         parameters = model.collect_probability_parameters()
-        instantiator = stormpy.ModelInstantiator(model)
+        instantiator = stormpy.pars.PDtmcInstantiator(model)
 
         point = {p: stormpy.RationalRF("0.4") for p in parameters}
         instantiated_model = instantiator.instantiate(point)

tests/core/test_pla.py → tests/pars/test_pla.py

@@ -1,5 +1,6 @@
 import stormpy
 import stormpy.logic
+import stormpy.pars
 from helpers.helper import get_example_path
 
 class TestModelChecking:
@@ -13,19 +14,18 @@ class TestModelChecking:
         assert model.nr_transitions == 803
         assert model.model_type == stormpy.ModelType.DTMC
         assert model.has_parameters
-        checker = stormpy.SparseDtmcRegionChecker(model)
-        checker.specify_formula(formulas[0].raw_formula)
+        checker = stormpy.pars.create_region_checker(model, formulas[0].raw_formula)
         parameters = model.collect_probability_parameters()
         assert len(parameters) == 2
-        region = stormpy.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
+        region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters)
         result = checker.check_region(region)
-        assert result == stormpy.RegionCheckResult.ALLSAT
-        region = stormpy.ParameterRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", parameters)
-        result = checker.check_region(region, stormpy.RegionCheckResult.UNKNOWN, True)
-        assert result == stormpy.RegionCheckResult.EXISTSBOTH
-        region = stormpy.ParameterRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", parameters)
+        assert result == stormpy.pars.RegionResult.ALLSAT
+        region = stormpy.pars.ParameterRegion("0.4<=pL<=0.65,0.75<=pK<=0.95", parameters)
+        result = checker.check_region(region, stormpy.pars.RegionResult.UNKNOWN, True)
+        assert result == stormpy.pars.RegionResult.EXISTSBOTH
+        region = stormpy.pars.ParameterRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", parameters)
         result = checker.check_region(region)
-        assert result == stormpy.RegionCheckResult.ALLVIOLATED
+        assert result == stormpy.pars.RegionResult.ALLVIOLATED
     
     def test_derivatives(self):
         import pycarl
@@ -39,5 +39,5 @@ class TestModelChecking:
         assert model.has_parameters
         parameters = model.collect_probability_parameters()
         assert len(parameters) == 2
-        derivatives = stormpy.gather_derivatives(model, list(parameters)[0])
+        derivatives = stormpy.pars.gather_derivatives(model, list(parameters)[0])
         assert len(derivatives) == 0