diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddSat.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddSat.c index 91daa142b..c07b948c3 100644 --- a/resources/3rdparty/cudd-3.0.0/cudd/cuddSat.c +++ b/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)); diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 7cf58f2f1..fdf2594fc 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/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().getCapacitiesFilename()); gspn->setCapacities(capacities); } - - - if(storm::settings::getModule().isWriteToDotSet()) { - std::ofstream file; - file.open(storm::settings::getModule().getWriteToDotFilename()); - gspn->writeDotToStream(file); - } + + storm::handleGSPNExportSettings(*gspn); if(storm::settings::getModule().isJaniFileSet()) { storm::jani::Model* model = storm::buildJani(*gspn); storm::exportJaniModel(*model, {}, storm::settings::getModule().getJaniFilename()); delete model; } - - + + delete gspn; return 0; // diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index 061e9bd67..386d2b0a2 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/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 oas; + std::vector probabilities; + std::vector 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 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 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 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 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); + + } + } + } +} \ No newline at end of file diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h index 92a7062b6..791989009 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.h +++ b/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 const& expManager) : gspn(gspn), expressionManager(expManager) { + JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr 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 oas; - std::vector probabilities; - std::vector 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 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 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 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 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 vars; diff --git a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp index eff8fdf1b..0b912c623 100644 --- a/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SymbolicDtmcPrctlHelper.cpp @@ -175,7 +175,7 @@ namespace storm { // Solve the equation system. std::unique_ptr> solver = linearEquationSolverFactory.create(submatrix, maybeStates, model.getRowVariables(), model.getColumnVariables(), model.getRowColumnMetaVariablePairs()); - storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.5) * maybeStatesAdd, subvector); + storm::dd::Add result = solver->solveEquations(model.getManager().getConstant(0.0) * maybeStatesAdd, subvector); return infinityStates.ite(model.getManager().getConstant(storm::utility::infinity()), result); } else { diff --git a/src/storm/settings/modules/CuddSettings.cpp b/src/storm/settings/modules/CuddSettings.cpp index e680276bf..0a2313757 100644 --- a/src/storm/settings/modules/CuddSettings.cpp +++ b/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()); diff --git a/src/storm/solver/NativeLinearEquationSolver.cpp b/src/storm/solver/NativeLinearEquationSolver.cpp index fcd3ed83c..f9763434a 100644 --- a/src/storm/solver/NativeLinearEquationSolver.cpp +++ b/src/storm/solver/NativeLinearEquationSolver.cpp @@ -110,7 +110,7 @@ namespace storm { template bool NativeLinearEquationSolver::solveEquations(std::vector& x, std::vector const& b) const { - if(!this->cachedRowVector) { + if (!this->cachedRowVector) { this->cachedRowVector = std::make_unique>(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(); } } diff --git a/src/storm/solver/SymbolicLinearEquationSolver.cpp b/src/storm/solver/SymbolicLinearEquationSolver.cpp index 5bcaea1bc..4e018586d 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicLinearEquationSolver.cpp @@ -37,7 +37,10 @@ namespace storm { storm::dd::Add lu = diagonal.ite(this->A.getDdManager().template getAddZero(), this->A); storm::dd::Add diagonalAdd = diagonal.template toAdd(); - storm::dd::Add dinv = diagonalAdd / (diagonalAdd * this->A); + storm::dd::Add diag = diagonalAdd.multiplyMatrix(this->A, this->columnMetaVariables); + + storm::dd::Add scaledLu = lu / diag; + storm::dd::Add scaledB = b / diag; // Set up additional environment variables. storm::dd::Add xCopy = x; @@ -46,21 +49,23 @@ namespace storm { while (!converged && iterationCount < maximalNumberOfIterations) { storm::dd::Add xCopyAsColumn = xCopy.swapVariables(this->rowColumnMetaVariablePairs); - - storm::dd::Add tmp = lu.multiplyMatrix(xCopyAsColumn, this->columnMetaVariables); - tmp = b - tmp; - tmp = tmp.swapVariables(this->rowColumnMetaVariablePairs); - tmp = dinv.multiplyMatrix(tmp, this->columnMetaVariables); + storm::dd::Add 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; } diff --git a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp b/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp index eced26e13..7189b1544 100644 --- a/src/storm/solver/SymbolicMinMaxLinearEquationSolver.cpp +++ b/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; }