Hack SparseParametricModelSimplifier.cpp

moves-rwth · Jan 10, 2025 · af98210 · af98210
1 parent 2419cd6
commit af98210
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 4 deletions.
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -95,9 +95,9 @@ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType, Robus
 
     if (allowModelSimplifications && graphPreserving) {
         auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<SparseModelType>(*dtmc);
-        if (!graphPreserving || !transformer::TimeTravelling::lastSavedAnnotations.empty()) {
-            simplifier.setSkipConstantDeterministicStateElimination(true);
-        }
+        // if (Robust) {
+        //     simplifier.setSkipConstantDeterministicStateElimination(true);
+        // }
         if (!simplifier.simplify(checkTask.getFormula())) {
             STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
         }

diff --git a/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp b/src/storm-pars/transformer/SparseParametricModelSimplifier.cpp
@@ -110,6 +110,7 @@ std::shared_ptr<SparseModelType> SparseParametricModelSimplifier<SparseModelType
     }
 
     storm::storage::SparseMatrix<typename SparseModelType::ValueType> const& sparseMatrix = model.getTransitionMatrix();
+    auto backwardsSparseMatrix = sparseMatrix.transpose();
 
     // get the action-based reward values
     std::vector<typename SparseModelType::ValueType> actionRewards;
@@ -131,14 +132,21 @@ std::shared_ptr<SparseModelType> SparseParametricModelSimplifier<SparseModelType
                     break;
                 }
             }
+            // TODO: HACK to make matrix stochastic
+            for (auto const& entry : backwardsSparseMatrix.getRowGroup(state)) {
+                if (!storm::utility::isConstant(entry.getValue())) {
+                    selectedStates.set(state, false);
+                    break;
+                }
+            }
         } else {
             selectedStates.set(state, false);
         }
     }
 
     // invoke elimination and obtain resulting transition matrix
     storm::storage::FlexibleSparseMatrix<typename SparseModelType::ValueType> flexibleMatrix(sparseMatrix);
-    storm::storage::FlexibleSparseMatrix<typename SparseModelType::ValueType> flexibleBackwardTransitions(sparseMatrix.transpose(), true);
+    storm::storage::FlexibleSparseMatrix<typename SparseModelType::ValueType> flexibleBackwardTransitions(backwardsSparseMatrix, true);
     storm::solver::stateelimination::NondeterministicModelStateEliminator<typename SparseModelType::ValueType> stateEliminator(
         flexibleMatrix, flexibleBackwardTransitions, actionRewards);
     for (auto state : selectedStates) {