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 modelCheckingSparseEngine(std: return storm::api::verifyWithSparseEngine(model, task); } +std::vector computeAllUntilProbabilities(storm::Environment const& env, CheckTask const& task, std::shared_ptr> ctmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + storm::solver::SolveGoal 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 computeTransientProbabilities(storm::Environment const& env, std::shared_ptr> 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, "Perform model checking", py::arg("model"), py::arg("task")); m.def("_parametric_model_checking_sparse_engine", &modelCheckingSparseEngine, "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, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states")); m.def("_compute_prob01states_rationalfunc", &computeProb01, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states"));