From 21e9bbf34a9bdfa03e310b0e8b7d1ba0f1fcd814 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 30 Jun 2017 18:13:10 +0200
Subject: [PATCH] Python bindings for storm-pars
---
CMakeLists.txt | 8 ++-
cmake/CMakeLists.txt | 15 ++++
cmake/config.py.in | 3 +-
lib/.gitignore | 2 +
lib/stormpy/pars/__init__.py | 9 +++
setup.py | 15 +++-
src/core/pla.cpp | 61 ----------------
src/core/pla.h | 8 ---
src/mod_core.cpp | 6 +-
src/mod_pars.cpp | 19 +++++
src/mod_storage.cpp | 1 -
src/pars/common.h | 3 +
src/pars/model_instantiator.cpp | 29 ++++++++
src/pars/model_instantiator.h | 8 +++
src/pars/pars.cpp | 11 +++
src/pars/pars.h | 8 +++
src/pars/pla.cpp | 70 +++++++++++++++++++
src/pars/pla.h | 8 +++
src/storage/model.cpp | 23 +-----
src/storage/model.h | 1 -
.../test_model_instantiator.py | 3 +-
tests/{core => pars}/test_parametric.py | 0
tests/{core => pars}/test_pla.py | 20 +++---
23 files changed, 218 insertions(+), 113 deletions(-)
create mode 100644 lib/stormpy/pars/__init__.py
delete mode 100644 src/core/pla.cpp
delete mode 100644 src/core/pla.h
create mode 100644 src/mod_pars.cpp
create mode 100644 src/pars/common.h
create mode 100644 src/pars/model_instantiator.cpp
create mode 100644 src/pars/model_instantiator.h
create mode 100644 src/pars/pars.cpp
create mode 100644 src/pars/pars.h
create mode 100644 src/pars/pla.cpp
create mode 100644 src/pars/pla.h
rename tests/{storage => pars}/test_model_instantiator.py (92%)
rename tests/{core => pars}/test_parametric.py (100%)
rename tests/{core => pars}/test_pla.py (66%)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index a01dcea..1eab77a 100644
--- a/CMakeLists.txt
+++ b/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()
-
-
diff --git a/cmake/CMakeLists.txt b/cmake/CMakeLists.txt
index 309669e..ef03051 100644
--- a/cmake/CMakeLists.txt
+++ b/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()
diff --git a/cmake/config.py.in b/cmake/config.py.in
index 122d464..16e5ee7 100644
--- a/cmake/config.py.in
+++ b/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@
diff --git a/lib/.gitignore b/lib/.gitignore
index f40fdce..bc81f1a 100644
--- a/lib/.gitignore
+++ b/lib/.gitignore
@@ -1,4 +1,6 @@
*.so
__pycache__/
stormpy.egg-info/
+stormpy/_config.py
stormpy/dft/_config.py
+stormpy/pars/_config.py
diff --git a/lib/stormpy/pars/__init__.py b/lib/stormpy/pars/__init__.py
new file mode 100644
index 0000000..f178522
--- /dev/null
+++ b/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()
diff --git a/setup.py b/setup.py
index 229dc50..fe28eea 100755
--- a/setup.py
+++ b/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,
diff --git a/src/core/pla.cpp b/src/core/pla.cpp
deleted file mode 100644
index 1f34f12..0000000
--- a/src/core/pla.cpp
+++ /dev/null
@@ -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"));
-}
diff --git a/src/core/pla.h b/src/core/pla.h
deleted file mode 100644
index 7ca587a..0000000
--- a/src/core/pla.h
+++ /dev/null
@@ -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_ */
diff --git a/src/mod_core.cpp b/src/mod_core.cpp
index 10cbe19..1c2485a 100644
--- a/src/mod_core.cpp
+++ b/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();
}
diff --git a/src/mod_pars.cpp b/src/mod_pars.cpp
new file mode 100644
index 0000000..b65de7b
--- /dev/null
+++ b/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();
+}
diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp
index 2755911..ef8903f 100644
--- a/src/mod_storage.cpp
+++ b/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();
}
diff --git a/src/pars/common.h b/src/pars/common.h
new file mode 100644
index 0000000..79a9840
--- /dev/null
+++ b/src/pars/common.h
@@ -0,0 +1,3 @@
+#include "src/common.h"
+
+#include "storm-pars/api/storm-pars.h"
diff --git a/src/pars/model_instantiator.cpp b/src/pars/model_instantiator.cpp
new file mode 100644
index 0000000..78b0376
--- /dev/null
+++ b/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");
+}
diff --git a/src/pars/model_instantiator.h b/src/pars/model_instantiator.h
new file mode 100644
index 0000000..d841821
--- /dev/null
+++ b/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_ */
diff --git a/src/pars/pars.cpp b/src/pars/pars.cpp
new file mode 100644
index 0000000..662735c
--- /dev/null
+++ b/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");
+}
diff --git a/src/pars/pars.h b/src/pars/pars.h
new file mode 100644
index 0000000..2f1cf7d
--- /dev/null
+++ b/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_ */
diff --git a/src/pars/pla.cpp b/src/pars/pla.cpp
new file mode 100644
index 0000000..1e786db
--- /dev/null
+++ b/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"));
+}
diff --git a/src/pars/pla.h b/src/pars/pla.h
new file mode 100644
index 0000000..327e627
--- /dev/null
+++ b/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_ */
diff --git a/src/storage/model.cpp b/src/storage/model.cpp
index e37c38e..cb05b12 100644
--- a/src/storage/model.cpp
+++ b/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");
-}
diff --git a/src/storage/model.h b/src/storage/model.h
index 69e4359..c779f26 100644
--- a/src/storage/model.h
+++ b/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_ */
diff --git a/tests/storage/test_model_instantiator.py b/tests/pars/test_model_instantiator.py
similarity index 92%
rename from tests/storage/test_model_instantiator.py
rename to tests/pars/test_model_instantiator.py
index f34b5f9..046dbbb 100644
--- a/tests/storage/test_model_instantiator.py
+++ b/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)
diff --git a/tests/core/test_parametric.py b/tests/pars/test_parametric.py
similarity index 100%
rename from tests/core/test_parametric.py
rename to tests/pars/test_parametric.py
diff --git a/tests/core/test_pla.py b/tests/pars/test_pla.py
similarity index 66%
rename from tests/core/test_pla.py
rename to tests/pars/test_pla.py
index 0301692..62b8030 100644
--- a/tests/core/test_pla.py
+++ b/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