From 9a8f40bb333f7d671d8b38ff4e88ea1bbde67296 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 14 Oct 2020 14:45:27 +0200
Subject: [PATCH] Multi-obj preprocessor: Fixed an issue when preprocessing LRA
 operator formulas

---
 .../preprocessing/SparseMultiObjectivePreprocessor.cpp          | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
index c0185e658..1fd427456 100644
--- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
+++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
@@ -189,7 +189,7 @@ namespace storm {
                             auto lraStates = mc.check(pathFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
                             // Compute Sat(Forall F (Forall G not "lraStates"))
                             auto forallGloballyNotLraStates = storm::utility::graph::performProb0A(backwardTransitions, ~lraStates, lraStates);
-                            absorbingStatesForSubformula = storm::utility::graph::performProb1A(model->getTransitionMatrix(), model->getNondeterministicChoiceIndices(), backwardTransitions, storm::storage::BitVector(model->getNumberOfStates(), true), forallGloballyNotLraStates);
+                            absorbingStatesForSubformula = storm::utility::graph::performProb1A(model->getTransitionMatrix(), model->getNondeterministicChoiceIndices(), backwardTransitions, ~lraStates, forallGloballyNotLraStates);
                         } else {
                             STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *opFormula << " of " << originalFormula << " because it is not supported");
                         }