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 ad7d56f..427bae8 100644 --- a/CHANGELOG.md +++ b/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 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" 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: 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); 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();