Merge branch 'master' into wrap_highlevel

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

src/core/core.cpp

@@ -106,6 +106,7 @@ void define_build(py::module& m) {
     py::class_<storm::builder::BuilderOptions>(m, "BuilderOptions", "Options for building process")
             .def(py::init<std::vector<std::shared_ptr<storm::logic::Formula const>> const&>(), "Initialise with formulae to preserve", py::arg("formulae"))
             .def(py::init<bool, bool>(), "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);

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<storm::dd::DdType::Sylvan, double>, "Transform symbolic model into sparse model", py::arg("model"));
-    m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Transform symbolic parametric model into sparse parametric model", py::arg("model"));
+    m.def("_transform_to_sparse_model", &storm::api::transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, double>, "Transform symbolic model into sparse model", py::arg("model"), py::arg("formulae") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
+    m.def("_transform_to_sparse_parametric_model", &storm::api::transformSymbolicToSparseModel<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Transform symbolic parametric model into sparse parametric model", py::arg("model"), py::arg("formulae") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
 }

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<std::string, std::string> 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_<storm::logic::PathFormula, std::shared_ptr<storm::logic::PathFormula>> pathFormula(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", formula);

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

src/utility/chrono.cpp

@@ -0,0 +1,8 @@
+#include "chrono.h"
+#include "src/helpers.h"
+
+void define_chrono(py::module& m) {
+    py::class_<std::chrono::milliseconds>(m, "milliseconds")
+            .def("count", &std::chrono::milliseconds::count)
+            .def("__str__", [](std::chrono::milliseconds const& t) { std::stringstream strstr; strstr << t.count(); return strstr.str(); });
+}

src/utility/chrono.h

@@ -0,0 +1,5 @@
+#pragma once
+
+#include "src/common.h"
+
+void define_chrono(py::module& m);