From 7a2082eb54fe25a631931328c10677aeee40ebf8 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 7 Sep 2020 14:04:25 +0200 Subject: [PATCH 1/6] Updated CHANGELOG --- CHANGELOG.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index ad7d56f..17cfbbf 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,10 +6,13 @@ Version 1.6.x ### Version 1.6.1 (under development) +- Adaptions to changes in Storm - 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.0 (2020/06) Requires storm version >= 1.6.0 and pycarl version >= 2.0.4 From 760c6e9f567a3dc694bee576ebe32b7dca9a39d8 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 7 Sep 2020 14:08:17 +0200 Subject: [PATCH 2/6] Require Storm version 1.6.2 --- .travis.yml | 8 ++++---- CHANGELOG.md | 6 +++++- setup.py | 2 +- 3 files changed, 10 insertions(+), 6 deletions(-) diff --git a/.travis.yml b/.travis.yml index 810b2d4..a59a4c3 100644 --- a/.travis.yml +++ b/.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 diff --git a/CHANGELOG.md b/CHANGELOG.md index 17cfbbf..eaa9077 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,7 +4,8 @@ Changelog Version 1.6.x ------------- -### Version 1.6.1 (under development) +### Version 1.6.2 (under development) +Requires storm version >= 1.6.2 and pycarl version >= 2.0.4 - Adaptions to changes in Storm - Explicit State Lookup: Finding a state based on the variable values @@ -14,6 +15,9 @@ Version 1.6.x - 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 diff --git a/setup.py b/setup.py index e91e74d..977d354 100755 --- a/setup.py +++ b/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: From 618b0b5b5e0b8d20f97ac1c773ac45c30f259c5e Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 7 Sep 2020 14:23:40 +0200 Subject: [PATCH 3/6] Updated CHANGELOG --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index eaa9077..e4d09c0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,7 @@ Version 1.6.x 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 From 53e7e102c8cb69685d927269e754b2dee9ef2e9d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 11 Sep 2020 10:55:49 +0200 Subject: [PATCH 4/6] Stormpy version 1.6.2 --- CHANGELOG.md | 2 +- lib/stormpy/_version.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index e4d09c0..427bae8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,7 +4,7 @@ Changelog Version 1.6.x ------------- -### Version 1.6.2 (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 diff --git a/lib/stormpy/_version.py b/lib/stormpy/_version.py index e4adfb8..51bbb3f 100644 --- a/lib/stormpy/_version.py +++ b/lib/stormpy/_version.py @@ -1 +1 @@ -__version__ = "1.6.0" +__version__ = "1.6.2" From 18dd4f1c4b22d6c7ea91f2c90a2de505ef0aef4e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 21 Sep 2020 15:23:05 -0700 Subject: [PATCH 5/6] more operators on (bounded) until formulae --- src/logic/formulae.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index ebb7873..3e4d773 100644 --- a/src/logic/formulae.cpp +++ b/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 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_> pathFormula(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", formula); py::class_> 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_>(m, "EventuallyFormula", "Formula for eventually", unaryPathFormula); py::class_>(m, "GloballyFormula", "Formula for globally", unaryPathFormula); py::class_> 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_>(m, "BoundedUntilFormula", "Until Formula with either a step or a time bound.", binaryPathFormula); + py::class_>(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_>(m, "ConditionalFormula", "Formula with the right hand side being a condition.", formula); py::class_>(m, "UntilFormula", "Path Formula for unbounded until", binaryPathFormula); From e1daceccd0fa974df055fe4ac3db8ed634b6d3ea Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 21 Sep 2020 15:23:31 -0700 Subject: [PATCH 6/6] extend prism command interface --- src/storage/prism.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp index 0e96e6c..f2f510a 100644 --- a/src/storage/prism.cpp +++ b/src/storage/prism.cpp @@ -73,6 +73,8 @@ void define_prism(py::module& m) { py::class_ 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();