Add bindings for computing steady-state distributions

lib/stormpy/__init__.py

@@ -532,6 +532,21 @@ def compute_expected_number_of_visits(environment, model):
     return core._compute_expected_number_of_visits_double(environment, model)
 
 
+def compute_steady_state_distribution(environment, model):
+    """
+    Compute the steady-state (aka stationary) distribution. Model must be deterministic.
+
+    :param environment: A model checking environment
+    :param model: A DTMC or CTMC
+    :return: A vector with the steady-state distribution
+    """
+    if model.supports_parameters:
+        raise NotImplementedError("Steady-state distribution is not implemented for parametric models")
+    if model.is_exact:
+        return core._compute_steady_state_distribution_exact(environment, model)
+    return core._compute_steady_state_distribution_double(environment, model)
+
+
 def construct_submodel(model, states, actions, keep_unreachable_states=True, options=SubsystemBuilderOptions()):
     """
 

src/core/modelchecking.cpp

@@ -75,6 +75,10 @@ template<typename ValueType>
 std::shared_ptr<storm::modelchecker::CheckResult> getExpectedNumberOfVisits(storm::Environment const& env, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
     return storm::api::computeExpectedVisitingTimesWithSparseEngine(env, model);
 }
+template<typename ValueType>
+std::shared_ptr<storm::modelchecker::CheckResult> getSteadyStateDistribution(storm::Environment const& env, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) {
+    return storm::api::computeSteadyStateDistributionWithSparseEngine(env, model);
+}
 
 template<typename ValueType>
 storm::storage::BitVector getReachableStates(storm::models::sparse::Model<ValueType> const& model, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, boost::optional<uint64_t> maximalStep, boost::optional<storm::storage::BitVector> const& choiceFilter) {
@@ -123,6 +127,9 @@ void define_modelchecking(py::module& m) {
     m.def("_compute_expected_number_of_visits_double", &getExpectedNumberOfVisits<double>, py::arg("env"), py::arg("model"));
     m.def("_compute_expected_number_of_visits_exact", &getExpectedNumberOfVisits<storm::RationalNumber>,  py::arg("env"), py::arg("model"));
 
+    m.def("_compute_steady_state_distribution_double", &getSteadyStateDistribution<double>, py::arg("env"), py::arg("model"));
+    m.def("_compute_steady_state_distribution_exact", &getSteadyStateDistribution<storm::RationalNumber>,  py::arg("env"), py::arg("model"));
+
     // Model checking
     m.def("_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine<double>, py::arg("model"), py::arg("task"), py::arg("environment")  = storm::Environment());
     m.def("_exact_model_checking_fully_observable", &modelCheckingFullyObservableSparseEngine<storm::RationalNumber>, py::arg("model"), py::arg("task"), py::arg("environment")  = storm::Environment());

tests/core/test_modelchecking.py

@@ -179,3 +179,16 @@ def test_compute_expected_number_of_visits(self):
         result = stormpy.compute_expected_number_of_visits(environment, model)
         assert result.at(0) == 1
         assert math.isclose(result.at(1),2.0/3)
+
+    def test_compute_steady_state_distribution(self):
+        program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm"))
+        model = stormpy.build_model(program)
+        environment = stormpy.Environment()
+        result = stormpy.compute_steady_state_distribution(environment, model)
+        values = result.get_values()
+        assert len(values) == 13
+        sorted(values)
+        for i in range(7): 
+            assert values[i] == 0
+        for i in range(7,13):
+            assert math.isclose(values[i], 1.0/6)