Support for weighted objective model checking,

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()

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")

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;
+
+
+

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<typename ValueType>
+std::pair<std::unique_ptr<storm::modelchecker::multiobjective::PcaaWeightVectorChecker<storm::models::sparse::Mdp<ValueType>>>, std::optional<storm::storage::SparseModelMemoryProductReverseData>> makeWeightedObjectiveMDPModelChecker(storm::Environment const& env, storm::models::sparse::Mdp<ValueType> const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, bool produceScheduler) {
+    auto const preprocessresult = storm::modelchecker::multiobjective::preprocessing::SparseMultiObjectivePreprocessor<storm::models::sparse::Mdp<ValueType>>::preprocess(env, originalModel, originalFormula, produceScheduler);
+    return std::make_pair(storm::modelchecker::multiobjective::createWeightVectorChecker(preprocessresult), preprocessresult.memoryIncorporationReverseData);
+}
+//
+template<typename ValueType>
+void define_multiobjective(py::module& m, std::string const& vtSuffix) {
+    m.def(("_make_weighted_objective_mdp_model_checker_" + vtSuffix).c_str(), &makeWeightedObjectiveMDPModelChecker<ValueType>, py::arg("env"), py::arg("model"), py::arg("formula"), py::arg("compute_scheduler")=false);
+
+    using PcaaWeightVectorChecker = storm::modelchecker::multiobjective::PcaaWeightVectorChecker<storm::models::sparse::Mdp<ValueType>>;
+    py::class_<PcaaWeightVectorChecker, std::unique_ptr<PcaaWeightVectorChecker>> 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<double>(py::module&, std::string const&);
+template void define_multiobjective<storm::RationalNumber>(py::module&, std::string const&);

src/core/multiobjective.h

@@ -0,0 +1,6 @@
+#pragma once
+
+#include "common.h"
+
+template<typename ValueType>
+void define_multiobjective(py::module& m, std::string const& vtSuffix);

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<storm::RationalNumber>(m, "ExactCheckTask");
     define_check_task<storm::RationalFunction>(m, "ParametricCheckTask");
     define_modelchecking(m);
+    define_multiobjective<double>(m, "Double");
+    define_multiobjective<storm::RationalNumber>(m, "Exact");
     define_counterexamples(m);
     define_bisimulation(m);
     define_input(m);

src/storage/memorystructure.cpp

@@ -4,6 +4,7 @@
 #include <storm/storage/memorystructure/MemoryStructure.h>
 #include <storm/storage/memorystructure/MemoryStructureBuilder.h>
 #include <storm/storage/memorystructure/SparseModelMemoryProduct.h>
+#include <storm/storage/memorystructure/SparseModelMemoryProductReverseData.h>
 
 
 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<storm::RationalFunction> const& sparseModel) {return ms.product(sparseModel);});
     memoryStructure.def_property_readonly("nr_states", &MemoryStructure::getNumberOfStates);
     memoryStructure.def_property_readonly("state_labeling", &MemoryStructure::getStateLabeling);
+
+    py::class_<storm::storage::SparseModelMemoryProductReverseData> memoryProductReverseData(m, "SparseModelMemoryProductReverseData");
+    memoryProductReverseData.def("_reverse_scheduler_double", &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler<double>, py::arg("product_scheduler"));
+    memoryProductReverseData.def("_reverse_scheduler_exact", &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler<storm::RationalNumber>, py::arg("product_scheduler"));
+    memoryProductReverseData.def("_reverse_scheduler_parametric", &storm::storage::SparseModelMemoryProductReverseData::createMemorySchedulerFromProductScheduler<storm::RationalFunction>, py::arg("product_scheduler"));
 }
 
 template<typename VT>

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
+
+