From e002b5938b73d7f02ff3b69e17d6dbd6ac82b9cc Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 3 Jan 2018 15:21:47 +0100 Subject: [PATCH 01/17] Model Building: First example for substitution of existing parametric models --- .../building_models/01-building-models.py | 5 +- .../building_models/02-building-models.py | 60 +++++++++++++++++++ 2 files changed, 62 insertions(+), 3 deletions(-) create mode 100644 examples/building_models/02-building-models.py diff --git a/examples/building_models/01-building-models.py b/examples/building_models/01-building-models.py index 68ee92d..2ecccbf 100644 --- a/examples/building_models/01-building-models.py +++ b/examples/building_models/01-building-models.py @@ -5,7 +5,7 @@ import stormpy.examples import stormpy.examples.files -def example_building_models(): +def example_building_models_01(): path = stormpy.examples.files.drn_ctmc_dft model = stormpy.build_model_from_drn(path) print(model.model_type) @@ -24,6 +24,5 @@ def example_building_models(): print("Number of states: {}".format(model.nr_states)) - if __name__ == '__main__': - example_building_models() \ No newline at end of file + example_building_models_01() \ No newline at end of file diff --git a/examples/building_models/02-building-models.py b/examples/building_models/02-building-models.py new file mode 100644 index 0000000..12f76ac --- /dev/null +++ b/examples/building_models/02-building-models.py @@ -0,0 +1,60 @@ +import stormpy +import stormpy.core + +import stormpy.examples +import stormpy.examples.files + +import stormpy.info +import pycarl + +def example_building_models_02(): + + + import stormpy.pars + if stormpy.info.storm_ratfunc_use_cln(): + import pycarl.cln as pc + else: + import pycarl.gmp as pc + + def make_factorized_rf(var, cache): + num = pc.FactorizedPolynomial(pc.Polynomial(var), cache) + denom = pc.FactorizedPolynomial(pc.Rational(1)) + return pc.FactorizedRationalFunction(num, denom) + + # And the parametric + path = stormpy.examples.files.drn_pdtmc_die + model = stormpy.build_parametric_model_from_drn(path) + print(model.model_type) + print("Number of states: {}".format(model.nr_states)) + + + + parameters = model.collect_probability_parameters() + bar_parameters = dict() + + for p in parameters: + # Ensure that variables with that name are not recognized by pycarl. + assert pycarl.variable_with_name(p.name + "_bar").is_no_variable + bar_parameters[p] = pycarl.Variable(p.name + "_bar") + print(pc.Polynomial(1) - p) + substitutions = dict([[pc.Polynomial(1) - p, bar_parameters[p]] for p in parameters]) + print(substitutions) + + matrix = model.transition_matrix + for e in matrix: + val = e.value() + if val.is_constant(): + continue + val_pol = val.numerator.polynomial() + cache = val.numerator.cache() + for sub, repl in substitutions.items(): + print(sub) + print(val_pol - sub) + if val_pol - sub == 0: + print("Found substitution") + e.set_value(make_factorized_rf(repl, cache)) + break # Assume only one substitution per entry + print(matrix) + +if __name__ == '__main__': + example_building_models_02() \ No newline at end of file From 80b4be446797280778d11eba46374436c7b41fdb Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 3 Jan 2018 15:34:01 +0100 Subject: [PATCH 02/17] cleaned the example a bit --- examples/building_models/02-building-models.py | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/examples/building_models/02-building-models.py b/examples/building_models/02-building-models.py index 12f76ac..67cedec 100644 --- a/examples/building_models/02-building-models.py +++ b/examples/building_models/02-building-models.py @@ -24,19 +24,17 @@ def example_building_models_02(): # And the parametric path = stormpy.examples.files.drn_pdtmc_die model = stormpy.build_parametric_model_from_drn(path) - print(model.model_type) - print("Number of states: {}".format(model.nr_states)) + parameters = model.collect_probability_parameters() bar_parameters = dict() - for p in parameters: # Ensure that variables with that name are not recognized by pycarl. assert pycarl.variable_with_name(p.name + "_bar").is_no_variable bar_parameters[p] = pycarl.Variable(p.name + "_bar") - print(pc.Polynomial(1) - p) + substitutions = dict([[pc.Polynomial(1) - p, bar_parameters[p]] for p in parameters]) print(substitutions) @@ -48,8 +46,6 @@ def example_building_models_02(): val_pol = val.numerator.polynomial() cache = val.numerator.cache() for sub, repl in substitutions.items(): - print(sub) - print(val_pol - sub) if val_pol - sub == 0: print("Found substitution") e.set_value(make_factorized_rf(repl, cache)) From 58dd78c7910a5757dd12fe898d1576c67a8de855 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 8 Jan 2018 14:11:29 +0100 Subject: [PATCH 03/17] Left and right subformulae of binary path formula --- src/logic/formulae.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index 072136f..e36a28a 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -22,6 +22,8 @@ void define_formulae(py::module& m) { 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, "ConditionalFormula", "Formula with the right hand side being a condition.", formula); py::class_>(m, "UntilFormula", "Path Formula for unbounded until", binaryPathFormula); From 326c64a9532a4aa8eb7e96320edf8b4e77326967 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 8 Jan 2018 14:21:01 +0100 Subject: [PATCH 04/17] reward models from drn files --- doc/source/reward_models.rst | 2 +- examples/reward_models/01-reward-models.py | 4 +++- lib/stormpy/examples/files/pdtmc/die.drn | 16 ++++++++-------- 3 files changed, 12 insertions(+), 10 deletions(-) diff --git a/doc/source/reward_models.rst b/doc/source/reward_models.rst index 11956d1..8f12b20 100644 --- a/doc/source/reward_models.rst +++ b/doc/source/reward_models.rst @@ -22,6 +22,7 @@ We consider the die again, but with another property which talks about the expec >>> assert len(model.reward_models) == 1 The model now has a reward model, as the property talks about rewards. +When :doc:`building_models` from explicit sources, the reward model is always included if it is defined in the source. We can do model checking analogous to probabilities:: @@ -61,4 +62,3 @@ In this example, we only have state-action rewards. These rewards are a vector, 0.0 - diff --git a/examples/reward_models/01-reward-models.py b/examples/reward_models/01-reward-models.py index 47c586c..1ce13dc 100644 --- a/examples/reward_models/01-reward-models.py +++ b/examples/reward_models/01-reward-models.py @@ -24,7 +24,9 @@ def example_reward_models_01(): print(reward) assert not model.reward_models[reward_model_name].has_transition_rewards - + model = stormpy.build_parametric_model_from_drn(stormpy.examples.files.drn_pdtmc_die) + assert len(model.reward_models) == 1 + assert reward_model_name == "coin_flips" if __name__ == '__main__': example_reward_models_01() \ No newline at end of file diff --git a/lib/stormpy/examples/files/pdtmc/die.drn b/lib/stormpy/examples/files/pdtmc/die.drn index f1d0e3e..2f035a8 100644 --- a/lib/stormpy/examples/files/pdtmc/die.drn +++ b/lib/stormpy/examples/files/pdtmc/die.drn @@ -4,35 +4,35 @@ @parameters p q @reward_models - +coin_flips @nr_states 13 @model -state 0 init +state 0 init [1] action 0 1 : p 2 : (-1)*p+1 -state 1 +state 1 [1] action 0 3 : q 4 : (-1)*q+1 -state 2 +state 2 [1] action 0 5 : q 6 : (-1)*q+1 -state 3 +state 3 [1] action 0 1 : p 7 : (-1)*p+1 -state 4 +state 4 [1] action 0 8 : p 9 : (-1)*p+1 -state 5 +state 5 [1] action 0 2 : p 10 : (-1)*p+1 -state 6 +state 6 [1] action 0 11 : p 12 : (-1)*p+1 From 10eea677e978ea8ad7d6c08aa0d43c84ba0c913a Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 8 Jan 2018 15:54:57 +0100 Subject: [PATCH 05/17] Add support for integer cast from state objects --- src/storage/state.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storage/state.cpp b/src/storage/state.cpp index fadd676..b13c887 100644 --- a/src/storage/state.cpp +++ b/src/storage/state.cpp @@ -17,12 +17,14 @@ void define_state(py::module& m) { .def_property_readonly("id", &SparseModelState::getIndex, "Id") .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") + .def("__int__",&SparseModelState::getIndex) ; py::class_>(m, "SparseParametricModelState", "State in sparse parametric model") .def("__str__", &SparseModelState::toString) .def_property_readonly("id", &SparseModelState::getIndex, "Id") .def_property_readonly("labels", &SparseModelState::getLabels, "Labels") .def_property_readonly("actions", &SparseModelState::getActions, "Get actions") + .def("__int__",&SparseModelState::getIndex) ; // SparseModelActions From b27b26f2b74ba9ce4acbf1f72bd7cd9fed6dfd9f Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 8 Jan 2018 15:55:27 +0100 Subject: [PATCH 06/17] row group start and row group end for iteration over matrices --- src/storage/matrix.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp index 0e09ffc..19b74d2 100644 --- a/src/storage/matrix.cpp +++ b/src/storage/matrix.cpp @@ -38,6 +38,9 @@ void define_sparse_matrix(py::module& m) { .def_property_readonly("nr_columns", &SparseMatrix::getColumnCount, "Number of columns") .def_property_readonly("nr_entries", &SparseMatrix::getEntryCount, "Number of non-zero entries") .def_property_readonly("_row_group_indices", &SparseMatrix::getRowGroupIndices, "Starting rows of row groups") + + .def("get_row_group_start", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row];}) + .def("get_row_group_end", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row+1];}) .def_property_readonly("has_trivial_row_grouping", &SparseMatrix::hasTrivialRowGrouping, "Trivial row grouping") .def("get_row", [](SparseMatrix& matrix, entry_index row) { return matrix.getRows(row, row+1); @@ -87,6 +90,8 @@ void define_sparse_matrix(py::module& m) { .def_property_readonly("nr_columns", &SparseMatrix::getColumnCount, "Number of columns") .def_property_readonly("nr_entries", &SparseMatrix::getEntryCount, "Number of non-zero entries") .def_property_readonly("_row_group_indices", &SparseMatrix::getRowGroupIndices, "Starting rows of row groups") + .def("get_row_group_start", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row];}) + .def("get_row_group_end", [](SparseMatrix& matrix, entry_index row) {return matrix.getRowGroupIndices()[row+1];}) .def_property_readonly("has_trivial_row_grouping", &SparseMatrix::hasTrivialRowGrouping, "Trivial row grouping") .def("get_row", [](SparseMatrix& matrix, entry_index row) { return matrix.getRows(row, row+1); From 0a8482d0680ee1986bfb7e2e12001eea16b0071c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 12 Jan 2018 18:10:43 +0100 Subject: [PATCH 07/17] Computing model checking result only for inital states --- lib/stormpy/__init__.py | 8 +++++--- tests/core/test_modelchecking.py | 11 +++++++++++ 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 93a83ad..8ffd318 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -137,11 +137,13 @@ def perform_bisimulation(model, properties, bisimulation_type): return core._perform_bisimulation(model, formulae, bisimulation_type) -def model_checking(model, property): +def model_checking(model, property, only_initial_states=False): """ Perform model checking on model for property. :param model: Model. :param property: Property to check for. + :param only_initial_states: If True, only results for initial states are computed. + If False, results for all states are computed. :return: Model checking result. :rtype: CheckResult """ @@ -151,10 +153,10 @@ def model_checking(model, property): formula = property if model.supports_parameters: - task = core.ParametricCheckTask(formula, False) + task = core.ParametricCheckTask(formula, only_initial_states) return core._parametric_model_checking_sparse_engine(model, task) else: - task = core.CheckTask(formula, False) + task = core.CheckTask(formula, only_initial_states) return core._model_checking_sparse_engine(model, task) diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index b0c1c1b..70b6ae5 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -69,6 +69,17 @@ class TestModelChecking: reference = [0.16666666666666663, 0.3333333333333333, 0, 0.6666666666666666, 0, 0, 0, 1, 0, 0, 0, 0, 0] assert all(map(math.isclose, result.get_values(), reference)) + def test_model_checking_only_initial(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) + formulas = stormpy.parse_properties_for_prism_program("Pmax=? [F{\"coin_flips\"}<=3 \"one\"]", program) + model = stormpy.build_model(program, formulas) + assert len(model.initial_states) == 1 + initial_state = model.initial_states[0] + assert initial_state == 0 + result = stormpy.model_checking(model, formulas[0], only_initial_states=True) + assert not result.result_for_all_states + assert math.isclose(result.at(initial_state), 0.125) + def test_model_checking_prob01(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulaPhi = stormpy.parse_properties("true")[0] From d9ff33a9e06a4df0db0ac9ce85847ca98b3f8ba3 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 12 Jan 2018 23:38:58 +0100 Subject: [PATCH 08/17] extended pla bindings for latest additions in PLA and to build PLA checker directly --- src/pars/pla.cpp | 47 +++++++++++++++++++++++++++++++---------------- 1 file changed, 31 insertions(+), 16 deletions(-) diff --git a/src/pars/pla.cpp b/src/pars/pla.cpp index 92ab461..54c1d0a 100644 --- a/src/pars/pla.cpp +++ b/src/pars/pla.cpp @@ -3,23 +3,36 @@ #include "storm/api/storm.h" -typedef storm::modelchecker::SparseDtmcParameterLiftingModelChecker, double> SparseDtmcRegionChecker; +typedef storm::modelchecker::SparseDtmcParameterLiftingModelChecker, double> DtmcParameterLiftingModelChecker; +typedef storm::modelchecker::SparseMdpParameterLiftingModelChecker, double> MdpParameterLiftingModelChecker; + typedef storm::modelchecker::RegionModelChecker RegionModelChecker; typedef storm::storage::ParameterRegion Region; // Thin wrappers -std::shared_ptr createRegionChecker(storm::Environment const& env, std::shared_ptr> const& model, std::shared_ptr const& formula) { - return storm::api::initializeParameterLiftingRegionModelChecker(env, model, storm::api::createTask(formula, true)); +std::shared_ptr createRegionChecker(storm::Environment const& env, std::shared_ptr> const& model, std::shared_ptr const& formula, bool generateSplittingEstimate, bool allowModelSimplifications) { + return storm::api::initializeParameterLiftingRegionModelChecker(env, model, storm::api::createTask(formula, true), generateSplittingEstimate, allowModelSimplifications); +} + +void specify(std::shared_ptr& checker, storm::Environment const& env, std::shared_ptr> const& model, std::shared_ptr const& formula, bool generateSplittingEstimate, bool allowModelSimplifications) { + return checker->specify(env, model, storm::api::createTask(formula, true), generateSplittingEstimate, allowModelSimplifications); } storm::modelchecker::RegionResult checkRegion(std::shared_ptr& checker, storm::Environment const& env, Region const& region, storm::modelchecker::RegionResultHypothesis const& hypothesis, storm::modelchecker::RegionResult const& initialResult, bool sampleVertices) { return checker->analyzeRegion(env, region, hypothesis, initialResult, sampleVertices); } -storm::RationalFunction getBound(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { +storm::RationalFunction getBoundAtInit(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { return checker->getBoundAtInitState(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize); } +storm::modelchecker::ExplicitQuantitativeCheckResult getBound_dtmc(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { + return res = checker->getBound(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)->asExplicitQuantitativeCheckResult(); +} + +std::unique_ptr> getBound_mdp(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { + return checker->getBound(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)->asExplicitQuantitativeCheckResult(); +} std::set gatherDerivatives(storm::models::sparse::Model const& model, carl::Variable const& var) { std::set derivatives; @@ -66,20 +79,22 @@ void define_pla(py::module& m) { ; // RegionModelChecker - //py::class_>(m, "SparseDtmcRegionChecker", "Region model checker for sparse DTMCs") - py::class_>(m, "RegionModelChecker", "Region model checker via paramater lifting") -/* .def("__init__", [](std::unique_ptr& instance, std::shared_ptr> model, storm::modelchecker::CheckTask const& task) -> void { - // Better use storm::api::initializeParameterLiftingRegionModelChecker(model, task); - //SparseDtmcRegionChecker tmp; - //tmp.specify(model, task); - auto tmp = storm::api::initializeParameterLiftingRegionModelChecker(model, task); - new (&instance) std::unique_ptr(tmp); - }, py::arg("model"), py::arg("task")*/ - .def("check_region", &checkRegion, "Check region", py::arg("environment"), py::arg("region"), py::arg("hypothesis") = storm::modelchecker::RegionResultHypothesis::Unknown, py::arg("initialResult") = storm::modelchecker::RegionResult::Unknown, py::arg("sampleVertices") = false) - .def("get_bound", &getBound, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true); + + py::class_> regionModelChecker(m, "RegionModelChecker", "Region model checker via paramater lifting"); + regionModelChecker.def("check_region", &checkRegion, "Check region", py::arg("environment"), py::arg("region"), py::arg("hypothesis") = storm::modelchecker::RegionResultHypothesis::Unknown, py::arg("initialResult") = storm::modelchecker::RegionResult::Unknown, py::arg("sampleVertices") = false) + .def("get_bound", &getBoundAtInit, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true) + .def("specify", &specify, "specify arguments",py::arg("environment"), py::arg("model"), py::arg("formula"), py::arg("generate_splitting_estimate") = false, py::arg("allow_model_simplification") = true); ; - m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("environment"), py::arg("model"), py::arg("formula")); + + py::class_>(m, "DtmcParameterLiftingModelChecker", "Region model checker for DTMCs", regionModelChecker) + .def(py::init<>()) + .def("get_bound_all_states", &getBound_dtmc, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true); + py::class_>(m, "MdpParameterLiftingModelChecker", "Region model checker for MPDs", regionModelChecker) + .def(py::init<>()) + .def("get_bound_all_states", &getBound_mdp, "Get bound", py::arg("environment"), py::arg("region"), py::arg("maximise")= true); + + m.def("create_region_checker", &createRegionChecker, "Create region checker", py::arg("environment"), py::arg("model"), py::arg("formula"), py::arg("generate_splitting_estimate") = false, py::arg("allow_model_simplification") = true); //m.def("is_parameter_lifting_sound", &storm::utility::parameterlifting::validateParameterLiftingSound, "Check if parameter lifting is sound", py::arg("model"), py::arg("formula")); m.def("gather_derivatives", &gatherDerivatives, "Gather all derivatives of transition probabilities", py::arg("model"), py::arg("var")); } From 75ac1a3e258e6501d12c1f1c31d740a631cfe6f6 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 19 Jan 2018 14:23:38 +0100 Subject: [PATCH 09/17] get state reward directly --- src/storage/model.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 167e003..e2c82fd 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -156,6 +156,7 @@ void define_model(py::module& m) { .def_property_readonly("has_transition_rewards", &RewardModel::hasTransitionRewards) .def_property_readonly("transition_rewards", [](RewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) .def_property_readonly("state_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) + .def("get_state_reward", [](RewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) .def("reduce_to_state_based_rewards", [](RewardModel& rewardModel, SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") ; @@ -201,6 +202,7 @@ void define_model(py::module& m) { .def_property_readonly("has_transition_rewards", &RewardModel::hasTransitionRewards) .def_property_readonly("transition_rewards", [](RewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) .def_property_readonly("state_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) + .def("get_state_reward", [](RewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) .def("reduce_to_state_based_rewards", [](RewardModel& rewardModel, SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") ; From 474b5a8cbc8009230797133990980610ae362787 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 19 Jan 2018 14:23:52 +0100 Subject: [PATCH 10/17] fix for pla --- src/pars/pla.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/pars/pla.cpp b/src/pars/pla.cpp index 54c1d0a..2afb288 100644 --- a/src/pars/pla.cpp +++ b/src/pars/pla.cpp @@ -27,10 +27,10 @@ storm::RationalFunction getBoundAtInit(std::shared_ptr& chec } storm::modelchecker::ExplicitQuantitativeCheckResult getBound_dtmc(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { - return res = checker->getBound(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)->asExplicitQuantitativeCheckResult(); + return checker->getBound(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)->asExplicitQuantitativeCheckResult(); } -std::unique_ptr> getBound_mdp(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { +storm::modelchecker::ExplicitQuantitativeCheckResult getBound_mdp(std::shared_ptr& checker, storm::Environment const& env, Region const& region, bool maximise) { return checker->getBound(env, region, maximise ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize)->asExplicitQuantitativeCheckResult(); } From 04f70bd7068c70c7d07b49f13f668fddc84fdda1 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 19 Jan 2018 14:24:07 +0100 Subject: [PATCH 11/17] Additional tests for PLA bindings --- tests/pars/test_pla.py | 67 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 67 insertions(+) diff --git a/tests/pars/test_pla.py b/tests/pars/test_pla.py index 6336527..87a55d8 100644 --- a/tests/pars/test_pla.py +++ b/tests/pars/test_pla.py @@ -1,5 +1,6 @@ import stormpy import stormpy.logic +import math from helpers.helper import get_example_path from configurations import pars @@ -30,3 +31,69 @@ class TestPLA: region = stormpy.pars.ParameterRegion("0.1<=pL<=0.73,0.2<=pK<=0.715", parameters) result = checker.check_region(env, region) assert result == stormpy.pars.RegionResult.ALLVIOLATED + + def test_pla_bounds(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + prop = "P=? [F s=5 ]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_parametric_model(program, formulas) + assert model.has_parameters + env = stormpy.Environment() + checker = stormpy.pars.create_region_checker(env, model, formulas[0].raw_formula) + parameters = model.collect_probability_parameters() + assert len(parameters) == 2 + region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) + result = checker.get_bound(env, region, True) + assert math.isclose(float(result.constant_part()), 0.8369631383670559) + #result_vec = checker.get_bound_all_states(env, region, True) + #result = result_vec.at(model.initial_states[0]) + #assert math.isclose(float(result.constant_part()), 0.8369631383670559) + + def test_pla_manual(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + prop = "P=? [F s=5 ]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_parametric_model(program, formulas) + assert model.has_parameters + env = stormpy.Environment() + checker = stormpy.pars.DtmcParameterLiftingModelChecker() + checker.specify(env, model, formulas[0].raw_formula) + parameters = model.collect_probability_parameters() + assert len(parameters) == 2 + region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) + result = checker.get_bound(env, region, True) + assert math.isclose(float(result.constant_part()), 0.8369631383670559) + + def test_pla_manual_no_simplification(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + prop = "P=? [F s=5 ]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_parametric_model(program, formulas) + assert model.has_parameters + env = stormpy.Environment() + checker = stormpy.pars.DtmcParameterLiftingModelChecker() + checker.specify(env, model, formulas[0].raw_formula, allow_model_simplification=False) + parameters = model.collect_probability_parameters() + assert len(parameters) == 2 + region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) + result = checker.get_bound(env, region, True) + assert math.isclose(float(result.constant_part()), 0.836963056082918) + + def test_pla_state_bounds(self): + program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) + prop = "P=? [F s=5 ]" + formulas = stormpy.parse_properties_for_prism_program(prop, program) + model = stormpy.build_parametric_model(program, formulas) + assert model.has_parameters + env = stormpy.Environment() + checker = stormpy.pars.DtmcParameterLiftingModelChecker() + checker.specify(env, model, formulas[0].raw_formula, allow_model_simplification=False) + parameters = model.collect_probability_parameters() + assert len(parameters) == 2 + region = stormpy.pars.ParameterRegion("0.7<=pL<=0.9,0.75<=pK<=0.95", parameters) + result_vec = checker.get_bound_all_states(env, region, True) + assert len(result_vec.get_values()) == model.nr_states + assert math.isclose(result_vec.at(model.initial_states[0]), 0.836963056082918) + + + From 8db0759f58e13d470a2397a7e14bf8f1e0ddec23 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 27 Jan 2018 19:15:24 +0100 Subject: [PATCH 12/17] optimality type for formulae --- src/core/core.cpp | 8 ++++++++ src/core/core.h | 1 + src/logic/formulae.cpp | 6 ++---- src/mod_core.cpp | 1 + 4 files changed, 12 insertions(+), 4 deletions(-) diff --git a/src/core/core.cpp b/src/core/core.cpp index d5f03be..b4b5de6 100644 --- a/src/core/core.cpp +++ b/src/core/core.cpp @@ -2,6 +2,7 @@ #include "storm/utility/initialize.h" #include "storm/utility/DirectEncodingExporter.h" #include "storm/storage/ModelFormulasPair.h" +#include "storm/solver/OptimizationDirection.h" void define_core(py::module& m) { // Init @@ -68,6 +69,13 @@ void define_build(py::module& m) { } +void define_optimality_type(py::module& m) { + py::enum_(m, "OptimizationDirection") + .value("Minimize", storm::solver::OptimizationDirection::Minimize) + .value("Maximize", storm::solver::OptimizationDirection::Maximize) + ; +} + // Thin wrapper for exporting model template void exportDRN(std::shared_ptr> model, std::string const& file) { diff --git a/src/core/core.h b/src/core/core.h index b56aa28..51bc696 100644 --- a/src/core/core.h +++ b/src/core/core.h @@ -7,5 +7,6 @@ void define_core(py::module& m); void define_parse(py::module& m); void define_build(py::module& m); void define_export(py::module& m); +void define_optimality_type(py::module& m); #endif /* PYTHON_CORE_CORE_H_ */ diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index e36a28a..d6d2dd8 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -58,10 +58,8 @@ void define_formulae(py::module& m) { .def("set_bound", [](storm::logic::OperatorFormula& f, storm::logic::ComparisonType comparisonType, storm::expressions::Expression const& bound) { f.setBound(storm::logic::Bound(comparisonType, bound)); }, "Set bound", py::arg("comparison_type"), py::arg("bound")) - // the above method should be sufficient for now; reinstate the following if needed - //.def_property("_threshold_expression", &storm::logic::OperatorFormula::getThreshold, &storm::logic::OperatorFormula::setThreshold, "Threshold expression") - //.def_property_readonly("_threshold_as_rational", &storm::logic::OperatorFormula::getThresholdAs, "Rational threshold of bound, if applicable") - //.def_property_readonly("_threshold_expression_has_rational_type", [](storm::logic::OperatorFormula const& f) { return f.getThreshold().hasRationalType(); } , "Check expression type [without needing a Python expression object]") + .def_property_readonly("has_optimality_type", &storm::logic::OperatorFormula::hasOptimalityType, "Flag if an optimality type is present") + .def_property_readonly("optimality_type", &storm::logic::OperatorFormula::getOptimalityType, "Flag for the optimality type") ; py::class_>(m, "TimeOperator", "The time operator", operatorFormula); py::class_>(m, "LongRunAvarageOperator", "Long run average operator", operatorFormula); diff --git a/src/mod_core.cpp b/src/mod_core.cpp index 583eff6..615a7ef 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -20,6 +20,7 @@ PYBIND11_MODULE(core, m) { define_property(m); define_parse(m); define_build(m); + define_optimality_type(m); define_export(m); define_result(m); define_modelchecking(m); From 777a24f29ea84c6ce3b25ab76e1a0c10b771db9c Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 18 Dec 2017 22:23:08 +0100 Subject: [PATCH 13/17] bindings for expression type --- src/storage/expressions.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp index a12cdc9..f65d16f 100644 --- a/src/storage/expressions.cpp +++ b/src/storage/expressions.cpp @@ -38,4 +38,10 @@ void define_expressions(py::module& m) { .def("__str__", &streamToString) ; + py::class_(m, "ExpressionType", "The type of an expression") + .def_property_readonly("is_boolean", &storm::expressions::Type::isBooleanType) + .def_property_readonly("is_integer", &storm::expressions::Type::isIntegerType) + .def_property_readonly("is_rational", &storm::expressions::Type::isRationalType) + .def("__str__", &storm::expressions::Type::getStringRepresentation); + } \ No newline at end of file From 3b2036465ebb19c5f870cd184ce67ade2db68497 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 18 Dec 2017 22:23:45 +0100 Subject: [PATCH 14/17] towards support for more info from prism programs --- src/core/input.cpp | 19 ------------------- src/mod_storage.cpp | 2 ++ src/storage/prism.cpp | 33 +++++++++++++++++++++++++++++++++ src/storage/prism.h | 5 +++++ 4 files changed, 40 insertions(+), 19 deletions(-) create mode 100644 src/storage/prism.cpp create mode 100644 src/storage/prism.h diff --git a/src/core/input.cpp b/src/core/input.cpp index a87c18a..1ce6a5a 100644 --- a/src/core/input.cpp +++ b/src/core/input.cpp @@ -19,25 +19,6 @@ void define_input(py::module& m) { // Parse Jani model m.def("parse_jani_model", &storm::api::parseJaniModel, "Parse Jani model", py::arg("path")); - // PrismType - py::enum_(m, "PrismModelType", "Type of the prism model") - .value("DTMC", storm::prism::Program::ModelType::DTMC) - .value("CTMC", storm::prism::Program::ModelType::CTMC) - .value("MDP", storm::prism::Program::ModelType::MDP) - .value("CTMDP", storm::prism::Program::ModelType::CTMDP) - .value("MA", storm::prism::Program::ModelType::MA) - .value("UNDEFINED", storm::prism::Program::ModelType::UNDEFINED) - ; - - // PrismProgram - py::class_(m, "PrismProgram", "Prism program") - .def_property_readonly("nr_modules", &storm::prism::Program::getNumberOfModules, "Number of modules") - .def_property_readonly("model_type", &storm::prism::Program::getModelType, "Model type") - .def_property_readonly("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Flag if program has undefined constants") - .def_property_readonly("undefined_constants_are_graph_preserving", &storm::prism::Program::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure") - .def("__str__", &streamToString) - ; - // JaniType py::enum_(m, "JaniModelType", "Type of the Jani model") .value("DTMC", storm::jani::ModelType::DTMC) diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp index b507db6..62ced7d 100644 --- a/src/mod_storage.cpp +++ b/src/mod_storage.cpp @@ -3,6 +3,7 @@ #include "storage/bitvector.h" #include "storage/model.h" #include "storage/matrix.h" +#include "storage/prism.h" #include "storage/state.h" #include "storage/labeling.h" #include "storage/expressions.h" @@ -19,6 +20,7 @@ PYBIND11_MODULE(storage, m) { define_model(m); define_sparse_matrix(m); define_state(m); + define_prism(m); define_labeling(m); define_expressions(m); } diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp new file mode 100644 index 0000000..4c97de3 --- /dev/null +++ b/src/storage/prism.cpp @@ -0,0 +1,33 @@ +#include "prism.h" +#include +#include "src/helpers.h" + +using namespace storm::prism; + +void define_prism(py::module& m) { + py::class_> program(m, "PrismProgram", "A Prism Program"); + program.def_property_readonly("constants", &Program::getConstants, "Get Program Constants") + .def_property_readonly("nr_modules", &storm::prism::Program::getNumberOfModules, "Number of modules") + .def_property_readonly("model_type", &storm::prism::Program::getModelType, "Model type") + .def_property_readonly("has_undefined_constants", &storm::prism::Program::hasUndefinedConstants, "Flag if program has undefined constants") + .def_property_readonly("undefined_constants_are_graph_preserving", &storm::prism::Program::undefinedConstantsAreGraphPreserving, "Flag if the undefined constants do not change the graph structure") + .def("__str__", &streamToString); + + + // PrismType + py::enum_(m, "PrismModelType", "Type of the prism model") + .value("DTMC", storm::prism::Program::ModelType::DTMC) + .value("CTMC", storm::prism::Program::ModelType::CTMC) + .value("MDP", storm::prism::Program::ModelType::MDP) + .value("CTMDP", storm::prism::Program::ModelType::CTMDP) + .value("MA", storm::prism::Program::ModelType::MA) + .value("UNDEFINED", storm::prism::Program::ModelType::UNDEFINED) + ; + + + py::class_> constant(m, "Constant", "A constant in a Prism program"); + constant.def_property_readonly("name", &Constant::getName, "Constant name") + .def_property_readonly("defined", &Constant::isDefined, "Is the constant defined?") + .def_property_readonly("type", &Constant::getType, "The type of the constant"); + +} \ No newline at end of file diff --git a/src/storage/prism.h b/src/storage/prism.h new file mode 100644 index 0000000..17f3a63 --- /dev/null +++ b/src/storage/prism.h @@ -0,0 +1,5 @@ +#pragma once + +#include "common.h" + +void define_prism(py::module& m); From 8b81d0d1a0a3c19f38000f998bdd4120d2ff9cdb Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sun, 28 Jan 2018 20:02:37 +0100 Subject: [PATCH 15/17] state action rewards convenience function added --- src/storage/model.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/storage/model.cpp b/src/storage/model.cpp index e2c82fd..ec3d43f 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -157,7 +157,8 @@ void define_model(py::module& m) { .def_property_readonly("transition_rewards", [](RewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) .def_property_readonly("state_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) .def("get_state_reward", [](RewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) - .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) + .def("get_state_action_reward", [](RewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) + .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) .def("reduce_to_state_based_rewards", [](RewardModel& rewardModel, SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") ; @@ -203,6 +204,8 @@ void define_model(py::module& m) { .def_property_readonly("transition_rewards", [](RewardModel& rewardModel) {return rewardModel.getTransitionRewardMatrix();}) .def_property_readonly("state_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateRewardVector();}) .def("get_state_reward", [](RewardModel& rewardModel, uint64_t state) {return rewardModel.getStateReward(state);}) + .def("get_state_action_reward", [](RewardModel& rewardModel, uint64_t action_index) {return rewardModel.getStateActionReward(action_index);}) + .def_property_readonly("state_action_rewards", [](RewardModel& rewardModel) {return rewardModel.getStateActionRewardVector();}) .def("reduce_to_state_based_rewards", [](RewardModel& rewardModel, SparseMatrix const& transitions, bool onlyStateRewards){return rewardModel.reduceToStateBasedRewards(transitions, onlyStateRewards);}, py::arg("transition_matrix"), py::arg("only_state_rewards"), "Reduce to state-based rewards") ; From 010e95e925f4222500f9b837ad58c3996123053f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 29 Jan 2018 13:07:31 +0100 Subject: [PATCH 16/17] apt-get update in travis --- travis/build.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/travis/build.sh b/travis/build.sh index 9ac4fba..745305b 100755 --- a/travis/build.sh +++ b/travis/build.sh @@ -16,6 +16,7 @@ linux) docker exec stormpy mkdir opt/stormpy docker cp . stormpy:/opt/stormpy # Install virtualenv + docker exec stormpy apt-get update docker exec stormpy apt-get install -qq -y python python3 virtualenv set +e From b98ac4efa1cdcc2883f3edd1f40fc82716689ff7 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 30 Jan 2018 21:23:05 +0100 Subject: [PATCH 17/17] at for qualitative check results --- src/core/result.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/core/result.cpp b/src/core/result.cpp index 6d7d9ab..33f6bce 100644 --- a/src/core/result.cpp +++ b/src/core/result.cpp @@ -43,6 +43,9 @@ void define_result(py::module& m) { // QualitativeCheckResult py::class_> qualitativeCheckResult(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results", checkResult); py::class_>(m, "ExplicitQualitativeCheckResult", "Explicit qualitative model checking result", qualitativeCheckResult) + .def("at", [](storm::modelchecker::ExplicitQualitativeCheckResult const& result, storm::storage::sparse::state_type state) { + return result[state]; + }, py::arg("state"), "Get result for given state") .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult::getTruthValuesVector, "Get BitVector representing the truth values") ;