From b78772e56066f6e09f3f9ab99ea5ce2ffc4c77da Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Sun, 8 Apr 2018 22:11:18 +0200
Subject: [PATCH] Binding for computing all forward probabilities

---
 src/core/modelchecking.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp
index d2325a5..555a0fd 100644
--- a/src/core/modelchecking.cpp
+++ b/src/core/modelchecking.cpp
@@ -12,6 +12,10 @@ std::shared_ptr<storm::modelchecker::CheckResult> modelCheckingSparseEngine(std:
     return storm::api::verifyWithSparseEngine<ValueType>(model, task);
 }
 
+std::vector<double> computeAllUntilProbabilities(storm::Environment const& env, CheckTask<double> const& task, std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
+    storm::solver::SolveGoal<double> goal(*ctmc, task);
+    return storm::modelchecker::helper::SparseCtmcCslHelper::computeAllUntilProbabilities(env, std::move(goal), ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates);
+}
 
 std::vector<double> computeTransientProbabilities(storm::Environment const& env, std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double timeBound) {
     return storm::modelchecker::helper::SparseCtmcCslHelper::computeAllTransientProbabilities(env, ctmc->getTransitionMatrix(), ctmc->getBackwardTransitions(), ctmc->getInitialStates(), phiStates, psiStates, ctmc->getExitRateVector(), timeBound);
@@ -52,6 +56,7 @@ void define_modelchecking(py::module& m) {
     // Model checking
     m.def("_model_checking_sparse_engine", &modelCheckingSparseEngine<double>, "Perform model checking", py::arg("model"), py::arg("task"));
     m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine<storm::RationalFunction>, "Perform parametric model checking", py::arg("model"), py::arg("task"));
+    m.def("compute_all_until_probabilities", &computeAllUntilProbabilities, "Compute forward until probabilities");
     m.def("compute_transient_probabilities", &computeTransientProbabilities, "Compute transient probabilities");
     m.def("_compute_prob01states_double", &computeProb01<double>, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states"));
     m.def("_compute_prob01states_rationalfunc", &computeProb01<storm::RationalFunction>, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states"));