From 21acd0bd2790a56193b18fc956b878891c374286 Mon Sep 17 00:00:00 2001
From: Linus Heck <linus.heck@ru.nl>
Date: Tue, 16 Jul 2024 09:47:51 +0200
Subject: [PATCH] Complain if bigstep gets a non-probabilistic matrix

---
 src/storm-pars/transformer/TimeTravelling.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/storm-pars/transformer/TimeTravelling.cpp b/src/storm-pars/transformer/TimeTravelling.cpp
index 4b24deb8a5..46d64e8e64 100644
--- a/src/storm-pars/transformer/TimeTravelling.cpp
+++ b/src/storm-pars/transformer/TimeTravelling.cpp
@@ -126,6 +126,9 @@ std::pair<models::sparse::Dtmc<RationalFunction>, std::map<UniPoly, Annotation>>
     models::sparse::Dtmc<RationalFunction> const& model, modelchecker::CheckTask<logic::Formula, RationalFunction> const& checkTask) {
     models::sparse::Dtmc<RationalFunction> dtmc(model);
     storage::SparseMatrix<RationalFunction> transitionMatrix = dtmc.getTransitionMatrix();
+
+    STORM_LOG_ASSERT(transitionMatrix.isProbabilistic(), "Gave big-step a nonprobabilistic transition matrix.");
+
     uint64_t initialState = dtmc.getInitialStates().getNextSetIndex(0);
 
     uint64_t originalNumStates = dtmc.getNumberOfStates();