Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm

resources/3rdparty/cudd-3.0.0/cudd/cuddSat.c

@@ -843,11 +843,12 @@ Cudd_EqualSupNormRel(
     /* Check terminal cases. */
     if (f == g) return(1);
     if (Cudd_IsConstant(f) && Cudd_IsConstant(g)) {
-        if (ddAbs((cuddV(f) - cuddV(g))/cuddV(f)) < tolerance) {
+        CUDD_VALUE_TYPE absDiff = ddAbs((cuddV(f) - cuddV(g)));
+        if (absDiff/cuddV(f) < tolerance || absDiff < Cudd_ReadEpsilon(dd)) {
             return(1);
         } else {
             if (pr>0) {
-                (void) fprintf(dd->out,"Offending nodes:\n");
+                (void) fprintf(dd->out,"Offending nodes (wrt. precision %0.30f) with diff %0.30f:\n", Cudd_ReadEpsilon(dd), absDiff);
                 (void) fprintf(dd->out,
                                "f: address = %p\t value = %40.30f\n",
                                (void *) f, cuddV(f));

src/storm-gspn-cli/storm-gspn.cpp

@@ -96,21 +96,16 @@ int main(const int argc, const char **argv) {
             auto capacities = parseCapacitiesList(storm::settings::getModule<storm::settings::modules::GSPNSettings>().getCapacitiesFilename());
             gspn->setCapacities(capacities);
         }
-      
-        
-        if(storm::settings::getModule<storm::settings::modules::GSPNExportSettings>().isWriteToDotSet()) {
-            std::ofstream file;
-            file.open(storm::settings::getModule<storm::settings::modules::GSPNExportSettings>().getWriteToDotFilename());
-            gspn->writeDotToStream(file);
-        }
+
+        storm::handleGSPNExportSettings(*gspn);
         
         if(storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
             storm::jani::Model* model = storm::buildJani(*gspn);
             storm::exportJaniModel(*model, {}, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
             delete model;
         }
-        
-        
+
+        delete gspn;
         return 0;
         
 //

src/storm-gspn/builder/JaniGSPNBuilder.cpp

@@ -1 +1,150 @@
 #include "JaniGSPNBuilder.h"
+
+namespace storm {
+    namespace builder {
+
+        storm::jani::Model* JaniGSPNBuilder::build(std::string const& automatonName) {
+            storm::jani::Model* model = new storm::jani::Model(gspn.getName(), storm::jani::ModelType::MA, janiVersion, expressionManager);
+            storm::jani::Automaton mainAutomaton(automatonName, expressionManager->declareIntegerVariable("loc"));
+            addVariables(model);
+            uint64_t locId = addLocation(mainAutomaton);
+            addEdges(mainAutomaton, locId);
+            model->addAutomaton(mainAutomaton);
+            model->setStandardSystemComposition();
+            return model;
+        }
+
+        void JaniGSPNBuilder::addVariables(storm::jani::Model* model) {
+            for (auto const& place : gspn.getPlaces()) {
+                storm::jani::Variable* janiVar = nullptr;
+                if (!place.hasRestrictedCapacity()) {
+                    // Effectively no capacity limit known
+                    janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()));
+                } else {
+                    assert(place.hasRestrictedCapacity());
+                    janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity()));
+                }
+                assert(janiVar != nullptr);
+                assert(vars.count(place.getID()) == 0);
+                vars[place.getID()] = &model->addVariable(*janiVar);
+                delete janiVar;
+            }
+        }
+
+        uint64_t JaniGSPNBuilder::addLocation(storm::jani::Automaton& automaton) {
+            uint64_t janiLoc = automaton.addLocation(storm::jani::Location("loc"));
+            automaton.addInitialLocation("loc");
+            return janiLoc;
+        }
+
+        void JaniGSPNBuilder::addEdges(storm::jani::Automaton& automaton, uint64_t locId) {
+
+            uint64_t lastPriority = -1;
+            storm::expressions::Expression lastPriorityGuard = expressionManager->boolean(false);
+            storm::expressions::Expression priorityGuard = expressionManager->boolean(true);
+
+            for (auto const& partition : gspn.getPartitions()) {
+                storm::expressions::Expression guard = expressionManager->boolean(false);
+
+                assert(lastPriority >= partition.priority);
+                if (lastPriority > partition.priority) {
+                    priorityGuard = priorityGuard && !lastPriorityGuard;
+                    lastPriority = partition.priority;
+                } else {
+                    assert(lastPriority == partition.priority);
+                }
+
+                // Compute enabled weight expression.
+                storm::expressions::Expression totalWeight = expressionManager->rational(0.0);
+                for (auto const& transId : partition.transitions) {
+                    auto const& trans = gspn.getImmediateTransitions()[transId];
+                    if (trans.noWeightAttached()) {
+                        continue;
+                    }
+                    storm::expressions::Expression destguard = expressionManager->boolean(true);
+                    for (auto const& inPlaceEntry : trans.getInputPlaces()) {
+                        destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
+                    }
+                    for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
+                        destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
+                    }
+                    totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0));
+
+                }
+                totalWeight = totalWeight.simplify();
+
+
+                std::vector<storm::jani::OrderedAssignments> oas;
+                std::vector<storm::expressions::Expression> probabilities;
+                std::vector<uint64_t> destinationLocations;
+                for (auto const& transId : partition.transitions) {
+                    auto const& trans = gspn.getImmediateTransitions()[transId];
+                    if (trans.noWeightAttached()) {
+                        std::cout << "ERROR -- no weights attached at transition" << std::endl;
+                        continue;
+                    }
+                    storm::expressions::Expression destguard = expressionManager->boolean(true);
+                    std::vector<storm::jani::Assignment> assignments;
+                    for (auto const& inPlaceEntry : trans.getInputPlaces()) {
+                        destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
+                        if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
+                            assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
+                        }
+                    }
+                    for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
+                        destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
+                    }
+                    for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
+                        if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
+                            assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
+                        } else {
+                            assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second -  trans.getInputPlaces().at(outputPlaceEntry.first));
+                        }
+                    }
+                    destguard = destguard.simplify();
+                    guard = guard || destguard;
+
+                    oas.emplace_back(assignments);
+                    destinationLocations.emplace_back(locId);
+                    probabilities.emplace_back(storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)));
+                }
+
+                std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge((priorityGuard && guard).simplify());
+                for (auto const& oa : oas) {
+                    templateEdge->addDestination(storm::jani::TemplateEdgeDestination(oa));
+                }
+                storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, templateEdge, destinationLocations, probabilities);
+                automaton.addEdge(e);
+                lastPriorityGuard = lastPriorityGuard || guard;
+
+            }
+            for (auto const& trans : gspn.getTimedTransitions()) {
+                storm::expressions::Expression guard = expressionManager->boolean(true);
+
+                std::vector<storm::jani::Assignment> assignments;
+                for (auto const& inPlaceEntry : trans.getInputPlaces()) {
+                    guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
+                    if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
+                        assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
+                    }
+                }
+                for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
+                    guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
+                }
+                for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
+                    if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
+                        assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
+                    } else {
+                        assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second -  trans.getInputPlaces().at(outputPlaceEntry.first));
+                    }
+                }
+
+                std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(guard);
+                templateEdge->addDestination(assignments);
+                storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans.getRate()), templateEdge, {locId}, {expressionManager->integer(1)});
+                automaton.addEdge(e);
+
+            }
+        }
+    }
+}

src/storm-gspn/builder/JaniGSPNBuilder.h

@@ -8,165 +8,32 @@ namespace storm {
     namespace builder {
         class JaniGSPNBuilder {
         public:
-            JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr<storm::expressions::ExpressionManager> const& expManager) : gspn(gspn), expressionManager(expManager) {
+            JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr<storm::expressions::ExpressionManager> const& expManager)
+                    : gspn(gspn), expressionManager(expManager) {
                 
             }
             
             virtual ~JaniGSPNBuilder() {
-                
+                // Intentionally left empty.
             }
             
             
-            storm::jani::Model* build() {
-                storm::jani::Model* model = new storm::jani::Model(gspn.getName(), storm::jani::ModelType::MA, janiVersion, expressionManager);
-                storm::jani::Automaton mainAutomaton("immediate", expressionManager->declareIntegerVariable("loc"));
-                addVariables(model);
-                uint64_t locId = addLocation(mainAutomaton);
-                addEdges(mainAutomaton, locId);
-                model->addAutomaton(mainAutomaton);
-                model->setStandardSystemComposition();
-                return model;
-            }
+            storm::jani::Model* build(std::string const& automatonName = "gspn_automaton");
             
             storm::jani::Variable const& getPlaceVariable(uint64_t placeId) {
                 return *vars.at(placeId);
             }
-            
-            void addVariables(storm::jani::Model* model) {
-                for (auto const& place : gspn.getPlaces()) {
-                    storm::jani::Variable* janiVar = nullptr;
-                    if (!place.hasRestrictedCapacity()) {
-                        // Effectively no capacity limit known
-                        janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()));
-                    } else {
-                        assert(place.hasRestrictedCapacity());
-                        janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity()));
-                    }
-                    assert(janiVar != nullptr);
-                    assert(vars.count(place.getID()) == 0);
-                    vars[place.getID()] = &model->addVariable(*janiVar);
-                    delete janiVar;
-                }
-            }
-            
-            uint64_t addLocation(storm::jani::Automaton& automaton) {
-                uint64_t janiLoc = automaton.addLocation(storm::jani::Location("loc"));
-                automaton.addInitialLocation("loc");
-                return janiLoc;
-            }
-            
-            void addEdges(storm::jani::Automaton& automaton, uint64_t locId) {
-                
-                uint64_t lastPriority = -1;
-                storm::expressions::Expression lastPriorityGuard = expressionManager->boolean(false);
-                storm::expressions::Expression priorityGuard = expressionManager->boolean(true);
-                // TODO here there is something to fix if we add transition partitions.
-                
-                for (auto const& partition : gspn.getPartitions()) {
-                    storm::expressions::Expression guard = expressionManager->boolean(false);
-                    
-                    assert(lastPriority >= partition.priority);
-                    if (lastPriority > partition.priority) {
-                        priorityGuard = priorityGuard && !lastPriorityGuard;
-                        lastPriority = partition.priority;
-                    } else {
-                        assert(lastPriority == partition.priority);
-                    }
-                    
-                    // Compute enabled weight expression.
-                    storm::expressions::Expression totalWeight = expressionManager->rational(0.0);
-                    for (auto const& transId : partition.transitions) {
-                        auto const& trans = gspn.getImmediateTransitions()[transId];
-                        if (trans.noWeightAttached()) {
-                            continue;
-                        }
-                        storm::expressions::Expression destguard = expressionManager->boolean(true);
-                        for (auto const& inPlaceEntry : trans.getInputPlaces()) {
-                            destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
-                        }
-                        for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
-                            destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
-                        }
-                        totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0));
-                        
-                    }
-                    totalWeight = totalWeight.simplify();
-                    
-                    
-                    std::vector<storm::jani::OrderedAssignments> oas;
-                    std::vector<storm::expressions::Expression> probabilities;
-                    std::vector<uint64_t> destinationLocations;
-                    for (auto const& transId : partition.transitions) {
-                        auto const& trans = gspn.getImmediateTransitions()[transId];
-                        if (trans.noWeightAttached()) {
-                            std::cout << "ERROR -- no weights attached at transition" << std::endl;
-                            continue;
-                        }
-                        storm::expressions::Expression destguard = expressionManager->boolean(true);
-                        std::vector<storm::jani::Assignment> assignments;
-                        for (auto const& inPlaceEntry : trans.getInputPlaces()) {
-                            destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
-                            if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
-                                assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
-                            }
-                        }
-                        for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
-                            destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
-                        }
-                        for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
-                            if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
-                                assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
-                            } else {
-                                assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second -  trans.getInputPlaces().at(outputPlaceEntry.first));
-                            }
-                        }
-                        destguard = destguard.simplify();
-                        guard = guard || destguard;
-                        
-                        oas.emplace_back(assignments);
-                        destinationLocations.emplace_back(locId);
-                        probabilities.emplace_back(storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)));
-                    }
-                    
-                    std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge((priorityGuard && guard).simplify());
-                    for (auto const& oa : oas) {
-                        templateEdge->addDestination(storm::jani::TemplateEdgeDestination(oa));
-                    }
-                    storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, templateEdge, destinationLocations, probabilities);
-                    automaton.addEdge(e);
-                    lastPriorityGuard = lastPriorityGuard || guard;
-                    
-                }
-                for (auto const& trans : gspn.getTimedTransitions()) {
-                    storm::expressions::Expression guard = expressionManager->boolean(true);
-                    
-                    std::vector<storm::jani::Assignment> assignments;
-                    for (auto const& inPlaceEntry : trans.getInputPlaces()) {
-                        guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
-                        if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
-                            assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
-                        }
-                    }
-                    for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
-                        guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
-                    }
-                    for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
-                        if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
-                            assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
-                        } else {
-                            assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second -  trans.getInputPlaces().at(outputPlaceEntry.first));
-                        }
-                    }
-                    
-                    std::shared_ptr<storm::jani::TemplateEdge> templateEdge = automaton.createTemplateEdge(guard);
-                    templateEdge->addDestination(assignments);
-                    storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans.getRate()), templateEdge, {locId}, {expressionManager->integer(1)});
-                    automaton.addEdge(e);
-                    
-                }
-            }
+
             
         private:
+
+
+            void addVariables(storm::jani::Model* model);
+
+            uint64_t addLocation(storm::jani::Automaton& automaton);
+
+            void addEdges(storm::jani::Automaton& automaton, uint64_t locId);
+
             const uint64_t janiVersion = 1;
             storm::gspn::GSPN const& gspn;
             std::map<uint64_t, storm::jani::Variable const*> vars;

src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp

@@ -175,7 +175,7 @@ namespace storm {
 
                         // Solve the equation system.
                         std::unique_ptr<storm::solver::SymbolicLinearEquationSolver<DdType, ValueType>> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs());
-                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector);
+                        storm::dd::Add<DdType, ValueType> result = solver->solveEquations(model.getManager().getConstant(0.0) * maybeStatesAdd, subvector);
                         
                         return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity<ValueType>()), result);
                     } else {

src/storm/settings/modules/CuddSettings.cpp

@@ -20,7 +20,7 @@ namespace storm {
             const std::string CuddSettings::reorderOptionName = "reorder";
             
             CuddSettings::CuddSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-15).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "Sets the precision used by Cudd.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision up to which to constants are considered to be different.").setDefaultValueDouble(1e-16).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, maximalMemoryOptionName, true, "Sets the upper bound of memory available to Cudd in MB.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "The memory available to Cudd (0 means unlimited).").setDefaultValueUnsignedInteger(4096).build()).build());
                 

src/storm/solver/NativeLinearEquationSolver.cpp

@@ -110,7 +110,7 @@ namespace storm {
         
         template<typename ValueType>
         bool NativeLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
-            if(!this->cachedRowVector) {
+            if (!this->cachedRowVector) {
                 this->cachedRowVector = std::make_unique<std::vector<ValueType>>(getMatrixRowCount());
             }
             
@@ -180,7 +180,7 @@ namespace storm {
                     std::swap(x, *currentX);
                 }
                 
-                if(!this->isCachingEnabled()) {
+                if (!this->isCachingEnabled()) {
                     clearCache();
                 }
                 
@@ -208,7 +208,7 @@ namespace storm {
                     result.swap(*this->cachedRowVector);
                 }
                 
-                if(!this->isCachingEnabled()) {
+                if (!this->isCachingEnabled()) {
                     clearCache();
                 }
             }

src/storm/solver/SymbolicLinearEquationSolver.cpp

@@ -37,7 +37,10 @@ namespace storm {
             
             storm::dd::Add<DdType, ValueType> lu = diagonal.ite(this->A.getDdManager().template getAddZero<ValueType>(), this->A);
             storm::dd::Add<DdType> diagonalAdd = diagonal.template toAdd<ValueType>();
-            storm::dd::Add<DdType, ValueType> dinv = diagonalAdd / (diagonalAdd * this->A);
+            storm::dd::Add<DdType, ValueType> diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables);
+            
+            storm::dd::Add<DdType, ValueType> scaledLu = lu / diag;
+            storm::dd::Add<DdType, ValueType> scaledB = b / diag;
             
             // Set up additional environment variables.
             storm::dd::Add<DdType, ValueType> xCopy = x;
@@ -46,21 +49,23 @@ namespace storm {
             
             while (!converged && iterationCount < maximalNumberOfIterations) {
                 storm::dd::Add<DdType, ValueType> xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs);
-
-                storm::dd::Add<DdType, ValueType> tmp = lu.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables);
-                tmp = b - tmp;
-                tmp = tmp.swapVariables(this->rowColumnMetaVariablePairs);
-                tmp = dinv.multiplyMatrix(tmp, this->columnMetaVariables);
+                storm::dd::Add<DdType, ValueType> tmp = scaledB - scaledLu.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables);
                 
                 // Now check if the process already converged within our precision.
-                converged = xCopy.equalModuloPrecision(tmp, precision, relative);
+                converged = tmp.equalModuloPrecision(xCopy, precision, relative);
 
                 xCopy = tmp;
                 
                 // Increase iteration count so we can abort if convergence is too slow.
                 ++iterationCount;
             }
-                        
+            
+            if (converged) {
+                STORM_LOG_TRACE("Iterative solver converged in " << iterationCount << " iterations.");
+            } else {
+                STORM_LOG_WARN("Iterative solver did not converge in " << iterationCount << " iterstions.");
+            }
+            
             return xCopy;
         }
         

src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp

@@ -43,8 +43,6 @@ namespace storm {
                 tmp += b;
                 
                 if (minimize) {
-                    // This is a hack and only here because of the lack of a suitable minAbstract/maxAbstract function
-                    // that can properly deal with a restriction of the choices.
                     tmp += illegalMaskAdd;
                     tmp = tmp.minAbstract(this->choiceVariables);
                 } else {
@@ -54,11 +52,14 @@ namespace storm {
                 // Now check if the process already converged within our precision.
                 converged = xCopy.equalModuloPrecision(tmp, precision, relative);
                 
-                // If the method did not converge yet, we prepare the x vector for the next iteration.
-                if (!converged) {
-                    xCopy = tmp;
-                }
+                xCopy = tmp;
                 
+                if (converged) {
+                    STORM_LOG_TRACE("Iterative solver converged in " << iterations << " iterations.");
+                } else {
+                    STORM_LOG_WARN("Iterative solver did not converge in " << iterations << " iterstions.");
+                }
+
                 ++iterations;
             }