diff --git a/examples/analysis/05-analysis.py b/examples/analysis/05-analysis.py new file mode 100644 index 0000000000..4a33811934 --- /dev/null +++ b/examples/analysis/05-analysis.py @@ -0,0 +1,31 @@ +import stormpy + +import stormpy.examples +import stormpy.examples.files + + +def example_analysis_05(): + exact = True + path = stormpy.examples.files.prism_mdp_maze_multigoal + prism_program = stormpy.parse_prism_program(path) + + formula_str = "multi(Pmax=? [F \"goalalt1\"], Pmax=? [F \"goalalt2\"])" + properties = stormpy.parse_properties(formula_str, prism_program) + + options = stormpy.BuilderOptions([p.raw_formula for p in properties]) + options.set_build_state_valuations() + env = stormpy.Environment() + + if exact: + env.solver_environment.set_linear_equation_solver_type(stormpy.EquationSolverType.eigen) + env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.policy_iteration + model = stormpy.build_sparse_exact_model_with_options(prism_program, options) + lower_bound, upper_bound = stormpy.compute_rel_reach_helper_exact(env, model, properties[0].raw_formula) + else: + model = stormpy.build_sparse_model_with_options(prism_program, options) + lower_bound, upper_bound = stormpy.compute_rel_reach_helper(env, model, properties[0].raw_formula) + print(lower_bound) + print(upper_bound) + +if __name__ == '__main__': + example_analysis_05() diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index 3044c45b07..3a4e2115eb 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -34,7 +34,9 @@ def _path(folder, file): prism_mdp_firewire = _path("mdp", "firewire.nm") """Prism version for Firewire protocol""" prism_mdp_maze = _path("mdp", "maze_2.nm") -"""Prism version of maze MDP""" +"""Prism example for the maze MDPs""" +prism_mdp_maze_multigoal = _path("mdp", "maze_2_multigoal.nm") +"""Prism example for the maze MDP with multiple goal""" prism_mdp_slipgrid = _path("mdp", "slipgrid.nm") """Prism version of maze MDP towards sketching""" prism_mdp_slipgrid_sketch = _path("mdp", "slipgrid_sketch.nm") diff --git a/lib/stormpy/examples/files/mdp/maze_2_multigoal.nm b/lib/stormpy/examples/files/mdp/maze_2_multigoal.nm new file mode 100644 index 0000000000..7230b2d4bc --- /dev/null +++ b/lib/stormpy/examples/files/mdp/maze_2_multigoal.nm @@ -0,0 +1,122 @@ + + +// maze example (POMDP) as an MDP +// slightly extends that presented in +// Littman, Cassandra and Kaelbling +// Learning policies for partially observable environments: Scaling up +// Technical Report CS, Brown University +// gxn 29/01/16 +// Made into a MDP for documentation of stormpy. + +// state space (value of variable "s") + +// 0 1 2 3 4 +// 5 6 7 +// 8 9 10 +// 11 13 12 + +// 13 is the target + +mdp + + +module maze + + s : [-1..13]; + + // initialisation + [] s=-1 -> 1/5 : (s'=0) + + 1/5 : (s'=1) + + 1/5 : (s'=2) + + 1/5 : (s'=3) + + 1/5 : (s'=4); + + // moving around the maze + + [east] s=0 -> (s'=1); + [west] s=0 -> (s'=0); + [north] s=0 -> (s'=0); + [south] s=0 -> (s'=5); + + [east] s=1 -> (s'=2); + [west] s=1 -> (s'=0); + [north] s=1 -> (s'=1); + [south] s=1 -> (s'=1); + + [east] s=2 -> (s'=3); + [west] s=2 -> (s'=1); + [north] s=2 -> (s'=2); + [south] s=2 -> (s'=6); + + [east] s=3 -> (s'=4); + [west] s=3 -> (s'=2); + [north] s=3 -> (s'=3); + [south] s=3 -> (s'=3); + + [east] s=4 -> (s'=4); + [west] s=4 -> (s'=3); + [north] s=4 -> (s'=4); + [south] s=4 -> (s'=7); + + [east] s=5 -> (s'=5); + [west] s=5 -> (s'=5); + [north] s=5 -> (s'=0); + [south] s=5 -> (s'=8); + + [east] s=6 -> (s'=6); + [west] s=6 -> (s'=6); + [north] s=6 -> (s'=2); + [south] s=6 -> (s'=9); + + [east] s=7 -> (s'=7); + [west] s=7 -> (s'=7); + [north] s=7 -> (s'=4); + [south] s=7 -> (s'=10); + + [east] s=8 -> (s'=8); + [west] s=8 -> (s'=8); + [north] s=8 -> (s'=5); + [south] s=8 -> (s'=11); + + [east] s=9 -> (s'=9); + [west] s=9 -> (s'=9); + [north] s=9 -> (s'=6); + [south] s=9 -> (s'=13); + + [east] s=10 -> (s'=10); + [west] s=10 -> (s'=10); + [north] s=10 -> (s'=7); + [south] s=10 -> (s'=12); + + [east] s=11 -> (s'=11); + [west] s=11 -> (s'=11); + [north] s=11 -> (s'=8); + [south] s=11 -> (s'=11); + + [east] s=12 -> (s'=12); + [west] s=12 -> (s'=12); + [north] s=12 -> (s'=10); + [south] s=12 -> (s'=12); + + // loop when we reach the target + [done] s=13 -> true; + +endmodule + +// reward structure (number of steps to reach the target) +rewards + + [east] true : 1; + [west] true : 1; + [north] true : 1; + [south] true : 1; + +endrewards + +// target observation +label "goal" = s=13; +label "goalalt1" = s=11; +label "goalalt2" = s=12; + + + diff --git a/src/core/multiobjective.cpp b/src/core/multiobjective.cpp new file mode 100644 index 0000000000..cf37cba3be --- /dev/null +++ b/src/core/multiobjective.cpp @@ -0,0 +1,33 @@ +#include "multiobjective.h" + +#include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h" +#include "storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h" +#include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h" +#include "storm/adapters/RationalNumberAdapter.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/utility/macros.h" +#include "storm/environment/Environment.h" +// +//// Helper class to avoid that we also need to bind the preprocessing. +template +std::pair>>, std::optional> makeWeightedObjectiveMDPModelChecker(storm::Environment const& env, storm::models::sparse::Mdp const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, bool produceScheduler) { + auto const preprocessresult = storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessor>::preprocess(env, originalModel, originalFormula, produceScheduler); + return std::make_pair(storm::modelchecker::multiobjective::createWeightVectorChecker(preprocessresult), preprocessresult.memoryIncorporationReverseData); +} +// +template +void define_multiobjective(py::module& m, std::string const& vtSuffix) { + m.def(("_make_weighted_objective_mdp_model_checker_" + vtSuffix).c_str(), &makeWeightedObjectiveMDPModelChecker, py::arg("env"), py::arg("model"), py::arg("formula"), py::arg("compute_scheduler")=false); + + using PcaaWeightVectorChecker = storm::modelchecker::multiobjective::PcaaWeightVectorChecker>; + py::class_> weightedObjectiveMdpModelChecker(m, ("WeightedObjectiveMdpModelChecker" + vtSuffix).c_str()); + weightedObjectiveMdpModelChecker.def("check", &PcaaWeightVectorChecker::check, py::arg("env"), py::arg("weight_vector")) + .def("get_achievable_point", &PcaaWeightVectorChecker::getAchievablePoint) + .def("get_optimal_weighted_sum", &PcaaWeightVectorChecker::getOptimalWeightedSum, "Note that this sum can be hard to interpret whenever one includes also minimization objectives.") + .def("compute_scheduler", &PcaaWeightVectorChecker::computeScheduler, "Note that this is a scheduler on the preprocessed MDP.") + .def("set_weighted_precision", &PcaaWeightVectorChecker::setWeightedPrecision, py::arg("value"), "A smaller value means a higher precision."); +} +// +template void define_multiobjective(py::module&, std::string const&); +template void define_multiobjective(py::module&, std::string const&); \ No newline at end of file diff --git a/src/core/multiobjective.h b/src/core/multiobjective.h new file mode 100644 index 0000000000..db4229da2d --- /dev/null +++ b/src/core/multiobjective.h @@ -0,0 +1,6 @@ +#pragma once + +#include "common.h" + +template +void define_multiobjective(py::module& m, std::string const& vtSuffix); diff --git a/src/mod_core.cpp b/src/mod_core.cpp index 4363adb935..5fc021d6e3 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -3,6 +3,7 @@ #include "core/core.h" #include "core/result.h" #include "core/modelchecking.h" +#include "core/multiobjective.h" #include "core/bisimulation.h" #include "core/input.h" #include "core/analysis.h" @@ -32,6 +33,8 @@ PYBIND11_MODULE(_core, m) { define_check_task(m, "ExactCheckTask"); define_check_task(m, "ParametricCheckTask"); define_modelchecking(m); + define_multiobjective(m, "Double"); + define_multiobjective(m, "Exact"); define_counterexamples(m); define_bisimulation(m); define_input(m); diff --git a/src/storage/memorystructure.cpp b/src/storage/memorystructure.cpp index d6b1f814d8..a52c866ef5 100644 --- a/src/storage/memorystructure.cpp +++ b/src/storage/memorystructure.cpp @@ -4,6 +4,7 @@ #include #include #include +#include void define_memorystructure_untyped(py::module& m) { @@ -15,6 +16,11 @@ void define_memorystructure_untyped(py::module& m) { memoryStructure.def("_product_model_parametric", [](MemoryStructure& ms, storm::models::sparse::Model const& sparseModel) {return ms.product(sparseModel);}); memoryStructure.def_property_readonly("nr_states", &MemoryStructure::getNumberOfStates); memoryStructure.def_property_readonly("state_labeling", &MemoryStructure::getStateLabeling); + + py::class_ memoryProductReverseData(m, "SparseModelMemoryProductReverseData"); + memoryProductReverseData.def("_reverse_scheduler_double", &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler, py::arg("product_scheduler")); + memoryProductReverseData.def("_reverse_scheduler_exact", &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler, py::arg("product_scheduler")); + memoryProductReverseData.def("_reverse_scheduler_parametric", &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler, py::arg("product_scheduler")); } template diff --git a/tests/core/test_multiobjective.py b/tests/core/test_multiobjective.py index 84bc2742c4..b10c98563c 100644 --- a/tests/core/test_multiobjective.py +++ b/tests/core/test_multiobjective.py @@ -1,10 +1,12 @@ +import math + import stormpy from helpers.helper import get_example_path from configurations import plotting, numpy_avail -class TestModelChecking: +class TestMultiObjectiveModelChecking: def naive_api_double_no_plotting_test(self): program = stormpy.parse_prism_program(get_example_path("mdp", "multiobjective1.nm")) properties = stormpy.parse_properties_for_prism_program('multi(Pmax=? [ F<=3 s=2 ],R{"rew"}max=? [ F s=2 ])', program) @@ -38,3 +40,29 @@ def naive_api_double_with_plotting_test(self): ax.set_xlabel(formula.subformulas[0]) ax.set_ylabel(formula.subformulas[1]) # plt.show() + +class TestWeightedObjectiveModelChecking: + def test_maze_double(self): + path = stormpy.examples.files.prism_mdp_maze_multigoal + prism_program = stormpy.parse_prism_program(path) + + formula_str = "multi(Rmin=? [F \"goalalt1\"], Pmax=? [F \"goalalt2\"])" + properties = stormpy.parse_properties(formula_str, prism_program) + + options = stormpy.BuilderOptions([p.raw_formula for p in properties]) + options.set_build_state_valuations() + env = stormpy.Environment() + model = stormpy.build_sparse_model_with_options(prism_program, options) + weighted_model_checker, inverter = stormpy._core._make_weighted_objective_mdp_model_checker_Double(env, model, properties[0].raw_formula, compute_scheduler=True) + weighted_model_checker.set_weighted_precision(0.0001) + weighted_model_checker.check(env, [0.5, 0.5]) + point = weighted_model_checker.get_achievable_point() + assert len(point) == 2 + assert math.isclose(point[0], 3.8) + assert math.isclose(point[1], 0.4) + value = weighted_model_checker.get_optimal_weighted_sum() + assert math.isclose(value, -1.7) + scheduler = inverter._reverse_scheduler_double(weighted_model_checker.compute_scheduler()) + assert scheduler.memory_size == 4 + +