From 2cd54a1e0d3d943a49ed8cf814197e4fef2a3d3a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 21 Jun 2018 10:38:25 +0200 Subject: [PATCH 1/6] Updated CHANGELOG --- CHANGELOG.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 41f4233..d5e60a5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,6 +7,14 @@ Version 1.2.x ### Version 1.2.x Requires storm version >= 1.2.2 and pycarl version >= 2.0.2 +- Adaptions to changes in Storm +- Bindings for symbolic models: + * building symbolic models + * bisimulation + * transforming symbolic to sparse models +- Extraction of schedulers and queries on schedulers +- Extended PLA bindings +- Extended documentation ### Version 1.2.0 Requires storm version >= 1.2.0 and pycarl version >= 2.0.2 From c0ac30fcd2d3eed5c59f3e954d567dbbbcf2f783 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 18 Jul 2018 15:41:17 +0200 Subject: [PATCH 2/6] access to: preserved label names during building --- src/core/core.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/core/core.cpp b/src/core/core.cpp index bbb8790..b592420 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -106,6 +106,7 @@ void define_build(py::module& m) { py::class_(m, "BuilderOptions", "Options for building process") .def(py::init> const&>(), "Initialise with formulae to preserve", py::arg("formulae")) .def(py::init(), "Initialise without formulae", py::arg("build_all_reward_models"), py::arg("build_all_labels")) + .def_property_readonly("preserved_label_names", &storm::builder::BuilderOptions::getLabelNames, "Labels preserved") .def("set_build_with_choice_origins", &storm::builder::BuilderOptions::setBuildChoiceOrigins, "Build choice origins", py::arg("new_value")=true) .def("set_add_out_of_bounds_state", &storm::builder::BuilderOptions::setAddOutOfBoundsState, "Build with out of bounds state", py::arg("new_value")=true) .def("set_add_overlapping_guards_label", &storm::builder::BuilderOptions::setAddOverlappingGuardsLabel, "Build with overlapping guards state labeled", py::arg("new_value")=true); From db71b7e5fd6e6d0b3768255b2486128bcf41dde7 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 18 Jul 2018 15:41:43 +0200 Subject: [PATCH 3/6] fixed transformation after changes in storm --- src/core/transformation.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/transformation.cpp b/src/core/transformation.cpp index 6db4330..12507d8 100644 --- a/src/core/transformation.cpp +++ b/src/core/transformation.cpp @@ -3,6 +3,6 @@ void define_transformation(py::module& m) { // Transform model - m.def("_transform_to_sparse_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic model into sparse model", py::arg("model")); - m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic parametric model into sparse parametric model", py::arg("model")); + m.def("_transform_to_sparse_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic model into sparse model", py::arg("model"), py::arg("formulae")); + m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic parametric model into sparse parametric model", py::arg("model"), py::arg("formulae")); } \ No newline at end of file From f08df44acf542ad71fa1c294e6cd700ab417dbc4 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 18 Jul 2018 15:42:31 +0200 Subject: [PATCH 4/6] access to is prop operator, is reward operator in formulae --- src/logic/formulae.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index 9294c00..8b80dea 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -18,7 +18,10 @@ void define_formulae(py::module& m) { formula.def("__str__", &storm::logic::Formula::toString) .def("clone", [](storm::logic::Formula const& f) { storm::logic::CloneVisitor cv; return cv.clone(f);}) .def("substitute_labels_by_labels", [](storm::logic::Formula const& f, std::map const& labelSubs) {storm::logic::LabelSubstitutionVisitor lsv(labelSubs); return lsv.substitute(f);}, "substitute label occurences", py::arg("replacements")) - ; + .def_property_readonly("is_probability_operator", &storm::logic::Formula::isProbabilityOperatorFormula, "is it a probability operator") + .def_property_readonly("is_reward_operator", &storm::logic::Formula::isRewardOperatorFormula, "is it a reward operator") + + ; // Path Formulae py::class_> pathFormula(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", formula); From 4ef4844c304dcf0dff71e247494c97b645b82889 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 18 Jul 2018 15:43:06 +0200 Subject: [PATCH 5/6] std::chrono support in stormpy --- src/mod_utility.cpp | 2 ++ src/utility/chrono.cpp | 8 ++++++++ src/utility/chrono.h | 5 +++++ 3 files changed, 15 insertions(+) create mode 100644 src/utility/chrono.cpp create mode 100644 src/utility/chrono.h diff --git a/src/mod_utility.cpp b/src/mod_utility.cpp index 8d1a504..777e80a 100644 --- a/src/mod_utility.cpp +++ b/src/mod_utility.cpp @@ -2,6 +2,7 @@ #include "utility/shortestPaths.h" #include "utility/smtsolver.h" +#include "utility/chrono.h" PYBIND11_MODULE(utility, m) { @@ -9,4 +10,5 @@ PYBIND11_MODULE(utility, m) { define_ksp(m); define_smt(m); + define_chrono(m); } diff --git a/src/utility/chrono.cpp b/src/utility/chrono.cpp new file mode 100644 index 0000000..def183e --- /dev/null +++ b/src/utility/chrono.cpp @@ -0,0 +1,8 @@ +#include "chrono.h" +#include "src/helpers.h" + +void define_chrono(py::module& m) { + py::class_(m, "milliseconds") + .def("count", &std::chrono::milliseconds::count) + .def("__str__", [](std::chrono::milliseconds const& t) { std::stringstream strstr; strstr << t.count(); return strstr.str(); }); +} \ No newline at end of file diff --git a/src/utility/chrono.h b/src/utility/chrono.h new file mode 100644 index 0000000..42762f5 --- /dev/null +++ b/src/utility/chrono.h @@ -0,0 +1,5 @@ +#pragma once + +#include "src/common.h" + +void define_chrono(py::module& m); \ No newline at end of file From 7bb7023e018ff57de9626852ead00d3ddf2cb109 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 18 Jul 2018 15:58:09 +0200 Subject: [PATCH 6/6] transformation: default no formulae given --- src/core/transformation.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/transformation.cpp b/src/core/transformation.cpp index 12507d8..bdf939c 100644 --- a/src/core/transformation.cpp +++ b/src/core/transformation.cpp @@ -3,6 +3,6 @@ void define_transformation(py::module& m) { // Transform model - m.def("_transform_to_sparse_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic model into sparse model", py::arg("model"), py::arg("formulae")); - m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic parametric model into sparse parametric model", py::arg("model"), py::arg("formulae")); + m.def("_transform_to_sparse_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic model into sparse model", py::arg("model"), py::arg("formulae") = std::vector>()); + m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel, "Transform symbolic parametric model into sparse parametric model", py::arg("model"), py::arg("formulae") = std::vector>()); } \ No newline at end of file