Complain if bigstep gets a non-probabilistic matrix

moves-rwth · Jul 16, 2024 · 21acd0b · 21acd0b
1 parent 8f2281e
commit 21acd0b
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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();