Matthias Volk
8 years ago
23 changed files with 218 additions and 113 deletions
-
8CMakeLists.txt
-
15cmake/CMakeLists.txt
-
3cmake/config.py.in
-
2lib/.gitignore
-
9lib/stormpy/pars/__init__.py
-
15setup.py
-
61src/core/pla.cpp
-
8src/core/pla.h
-
6src/mod_core.cpp
-
19src/mod_pars.cpp
-
1src/mod_storage.cpp
-
3src/pars/common.h
-
29src/pars/model_instantiator.cpp
-
8src/pars/model_instantiator.h
-
11src/pars/pars.cpp
-
8src/pars/pars.h
-
70src/pars/pla.cpp
-
8src/pars/pla.h
-
23src/storage/model.cpp
-
1src/storage/model.h
-
3tests/pars/test_model_instantiator.py
-
0tests/pars/test_parametric.py
-
20tests/pars/test_pla.py
@ -1,7 +1,8 @@ |
|||||
# Auto-generated by Cmake. |
|
||||
|
# Auto-generated by CMake. |
||||
|
|
||||
STORM_DIR = "@STORM_DIR@" |
STORM_DIR = "@STORM_DIR@" |
||||
STORM_VERSION = "@STORM_VERSION@" |
STORM_VERSION = "@STORM_VERSION@" |
||||
STORM_CLN_EA = @STORM_CLN_EA_BOOL@ |
STORM_CLN_EA = @STORM_CLN_EA_BOOL@ |
||||
STORM_CLN_RF = @STORM_CLN_RF_BOOL@ |
STORM_CLN_RF = @STORM_CLN_RF_BOOL@ |
||||
|
HAVE_STORM_PARS = @HAVE_STORM_PARS_BOOL@ |
||||
HAVE_STORM_DFT = @HAVE_STORM_DFT_BOOL@ |
HAVE_STORM_DFT = @HAVE_STORM_DFT_BOOL@ |
@ -1,4 +1,6 @@ |
|||||
*.so |
*.so |
||||
__pycache__/ |
__pycache__/ |
||||
stormpy.egg-info/ |
stormpy.egg-info/ |
||||
|
stormpy/_config.py |
||||
stormpy/dft/_config.py |
stormpy/dft/_config.py |
||||
|
stormpy/pars/_config.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() |
@ -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")); |
|
||||
} |
|
@ -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_ */ |
|
@ -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(); |
||||
|
} |
@ -0,0 +1,3 @@ |
|||||
|
#include "src/common.h" |
||||
|
|
||||
|
#include "storm-pars/api/storm-pars.h" |
@ -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"); |
||||
|
} |
@ -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_ */ |
@ -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"); |
||||
|
} |
@ -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_ */ |
@ -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")); |
||||
|
} |
@ -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_ */ |
Write
Preview
Loading…
Cancel
Save
Reference in new issue