diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 34e38bbf7..3a8a99435 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -227,6 +227,10 @@ if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL) else() message(SEND_ERROR "File ${carlLOCATION} does not exist, did you build carl?") endif() + if("${carl_MINORYEARVERSION}" STREQUAL "" OR "${carl_MINORMONTHVERSION}" STREQUAL "" OR "${carl_MAINTENANCEVERSION}" STREQUAL "") + # don't have detailed version information, probably an old version of carl + message(FATAL_ERROR "Carl at ${carlLOCATION} outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") + endif() if(${carl_MINORYEARVERSION} LESS ${CARL_MINYEAR}) message(SEND_ERROR "Carl outdated, require ${CARL_MINYEAR}.${CARL_MINMONTH}.${CARL_MINPATCH}, have ${carl_VERSION}") elseif(${carl_MINORYEARVERSION} EQUAL ${CARL_MINYEAR}) diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 150a9d86c..8ac2bdea8 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -258,16 +258,16 @@ namespace storm { solver->setUpperBound(upperResultBound.get()); } else if (solvingRequiresUpperRewardBounds) { // For the min-case, we use DS-MPI, for the max-case variant 2 of the Baier et al. paper (CAV'17). - std::vector oneStepProbs; + std::vector oneStepProbs; oneStepProbs.reserve(parameterLifter->getMatrix().getRowCount()); for (uint64_t row = 0; row < parameterLifter->getMatrix().getRowCount(); ++row) { - oneStepProbs.push_back(storm::utility::one() - parameterLifter->getMatrix().getRowSum(row)); + oneStepProbs.push_back(storm::utility::one() - parameterLifter->getMatrix().getRowSum(row)); } if (dirForParameters == storm::OptimizationDirection::Minimize) { - storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs); + storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs); solver->setUpperBounds(dsmpi.computeUpperBounds()); } else { - storm::modelchecker::helper::BaierUpperRewardBoundsComputer baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs); + storm::modelchecker::helper::BaierUpperRewardBoundsComputer baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs); solver->setUpperBound(baier.computeUpperBound()); } } diff --git a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp index 70d2de0c1..a44024125 100644 --- a/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/IterativeMinMaxLinearEquationSolver.cpp @@ -256,7 +256,7 @@ namespace storm { MinMaxLinearEquationSolverRequirements requirements(this->linearEquationSolverFactory->getRequirements()); // In case we perform value iteration and need to retrieve a scheduler, end components are forbidden - if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration && isTrackSchedulerSet()) { + if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings::SolutionMethod::ValueIteration && this->isTrackSchedulerSet()) { requirements.requireNoEndComponents(); } @@ -380,7 +380,7 @@ namespace storm { // If requested, we store the scheduler for retrieval. if (this->isTrackSchedulerSet()) { this->schedulerChoices = std::vector(this->A->getRowGroupCount()); - this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *currentX, &this->schedulerChoices.get()); + this->linEqSolverA->multiplyAndReduce(dir, this->A->getRowGroupIndices(), x, &b, *auxiliaryRowGroupVector.get(), &this->schedulerChoices.get()); } if (!this->isCachingEnabled()) { diff --git a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp index 0369d301d..024bcf260 100644 --- a/src/storm/solver/LpMinMaxLinearEquationSolver.cpp +++ b/src/storm/solver/LpMinMaxLinearEquationSolver.cpp @@ -115,7 +115,7 @@ namespace storm { MinMaxLinearEquationSolverRequirements requirements; // In case we need to retrieve a scheduler, end components are forbidden - if (isTrackSchedulerSet()) { + if (this->isTrackSchedulerSet()) { requirements.requireNoEndComponents(); }