Merge branch 'master' into monitoring

.travis.yml

@@ -48,13 +48,13 @@ jobs:
     # Docker Storm stable
     - os: linux
       compiler: gcc
-      env: TASK=Test CONFIG=Release DOCKER=storm:1.6.0 PYTHON=python3
+      env: TASK=Test CONFIG=Release DOCKER=storm:1.6.2 PYTHON=python3
       script:
         travis/build.sh
     # Docker Storm stable in debug mode
     - os: linux
       compiler: gcc
-      env: TASK=Test CONFIG=Debug DOCKER=storm:1.6.0-debug PYTHON=python3
+      env: TASK=Test CONFIG=Debug DOCKER=storm:1.6.2-debug PYTHON=python3
       script:
         travis/build.sh
     # Documentation
@@ -76,6 +76,6 @@ jobs:
   # Allow failures of stable versions as new features might have been added
   allow_failures:
     - os: linux
-      env: TASK=Test CONFIG=Release DOCKER=storm:1.6.0 PYTHON=python3
+      env: TASK=Test CONFIG=Release DOCKER=storm:1.6.2 PYTHON=python3
     - os: linux
-      env: TASK=Test CONFIG=Debug DOCKER=storm:1.6.0-debug PYTHON=python3
+      env: TASK=Test CONFIG=Debug DOCKER=storm:1.6.2-debug PYTHON=python3

CHANGELOG.md

@@ -4,12 +4,20 @@ Changelog
 Version 1.6.x
 -------------
 
-### Version 1.6.1 (under development)
+### Version 1.6.2 (2020/09)
+Requires storm version >= 1.6.2 and pycarl version >= 2.0.4
 
+- Adaptions to changes in Storm
+- Create models (DTMC, MDP, CTMC, MA) directly from model components. Support creation of transition matrix, labeling, reward models, etc.
 - Explicit State Lookup: Finding a state based on the variable values
 - Support for pPOMDPs
 - (p)POMDPs: Support for unfolding memory, making POMDPs simple, and exporting POMDP to a pMC
 - Export to DRN options to support exporting without placeholders
+- Renamed `preprocess_prism_program` to `preprocess_symbolic_input`
+- Bindings for Storm-dft; most notably transformations, symmetries and relevant events
+
+### Version 1.6.1
+Skipped for compatibility with Storm.
 
 ### Version 1.6.0 (2020/06)
 Requires storm version >= 1.6.0 and pycarl version >= 2.0.4

lib/stormpy/_version.py

@@ -1 +1 @@
-__version__ = "1.6.0"
+__version__ = "1.6.2"

setup.py

@@ -14,7 +14,7 @@ if sys.version_info[0] == 2:
     sys.exit('Sorry, Python 2.x is not supported')
 
 # Minimal storm version required
-storm_min_version = "1.6.1"
+storm_min_version = "1.6.2"
 
 # Get the long description from the README file
 with open(os.path.join(os.path.abspath(os.path.dirname(__file__)), 'README.md'), encoding='utf-8') as f:

src/logic/formulae.cpp

@@ -21,22 +21,26 @@ void define_formulae(py::module& m) {
         .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")
-
+        .def_property_readonly("is_eventually_formula", &storm::logic::Formula::isEventuallyFormula)
+        .def_property_readonly("is_bounded_until_formula", &storm::logic::Formula::isBoundedUntilFormula)
+        .def_property_readonly("is_until_formula", &storm::logic::Formula::isUntilFormula)
             ;
 
     // 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);
     py::class_<storm::logic::UnaryPathFormula, std::shared_ptr<storm::logic::UnaryPathFormula>> unaryPathFormula(m, "UnaryPathFormula", "Path formula with one operand", pathFormula);
     unaryPathFormula.def_property_readonly("subformula", &storm::logic::UnaryPathFormula::getSubformula, "the subformula");
-    unaryPathFormula.def_property_readonly("is_eventually_formula", &storm::logic::UnaryPathFormula::isEventuallyFormula);
-    unaryPathFormula.def_property_readonly("is_bounded_until_formula", &storm::logic::UnaryPathFormula::isBoundedUntilFormula);
-    unaryPathFormula.def_property_readonly("is_until_formula", &storm::logic::UnaryPathFormula::isUntilFormula);
     py::class_<storm::logic::EventuallyFormula, std::shared_ptr<storm::logic::EventuallyFormula>>(m, "EventuallyFormula", "Formula for eventually", unaryPathFormula);
     py::class_<storm::logic::GloballyFormula, std::shared_ptr<storm::logic::GloballyFormula>>(m, "GloballyFormula", "Formula for globally", unaryPathFormula);
     py::class_<storm::logic::BinaryPathFormula, std::shared_ptr<storm::logic::BinaryPathFormula>> binaryPathFormula(m, "BinaryPathFormula", "Path formula with two operands", pathFormula);
     binaryPathFormula.def_property_readonly("left_subformula", &storm::logic::BinaryPathFormula::getLeftSubformula);
     binaryPathFormula.def_property_readonly("right_subformula", &storm::logic::BinaryPathFormula::getRightSubformula);
-    py::class_<storm::logic::BoundedUntilFormula, std::shared_ptr<storm::logic::BoundedUntilFormula>>(m, "BoundedUntilFormula", "Until Formula with either a step or a time bound.", binaryPathFormula);
+    py::class_<storm::logic::BoundedUntilFormula, std::shared_ptr<storm::logic::BoundedUntilFormula>>(m, "BoundedUntilFormula", "Until Formula with either a step or a time bound.", binaryPathFormula)
+    .def_property_readonly("is_multidimensional", &storm::logic::BoundedUntilFormula::isMultiDimensional, "Is the bound multi-dimensional")
+    .def_property_readonly("has_lower_bound", [](storm::logic::BoundedUntilFormula const& form) { return form.hasLowerBound(); })
+    .def_property_readonly("upper_bound_expression", [](storm::logic::BoundedUntilFormula const& form) { return form.getUpperBound(); } )
+    .def_property_readonly("left_subformula", [](storm::logic::BoundedUntilFormula const& form) -> storm::logic::Formula const& { return form.getLeftSubformula(); }, py::return_value_policy::reference_internal)
+    .def_property_readonly("right_subformula", [](storm::logic::BoundedUntilFormula const& form)-> storm::logic::Formula const& { return form.getRightSubformula(); }, py::return_value_policy::reference_internal);
     py::class_<storm::logic::ConditionalFormula, std::shared_ptr<storm::logic::ConditionalFormula>>(m, "ConditionalFormula", "Formula with the right hand side being a condition.", formula);
     py::class_<storm::logic::UntilFormula, std::shared_ptr<storm::logic::UntilFormula>>(m, "UntilFormula", "Path Formula for unbounded until", binaryPathFormula);
 

src/storage/prism.cpp

@@ -73,6 +73,8 @@ void define_prism(py::module& m) {
 
     py::class_<Command> command(m, "PrismCommand", "A command in a Prism program");
     command.def_property_readonly("global_index", &Command::getGlobalIndex, "Get global index")
+            .def_property_readonly("labeled", &Command::isLabeled, "Is the command labeled")
+            .def_property_readonly("action_index", &Command::getActionIndex, "What is the action index of the command")
             .def_property_readonly("guard_expression", &Command::getGuardExpression, "Get guard expression")
             .def_property_readonly("updates", [](Command const& command) {
                     return command.getUpdates();