Merge branch 'master' into reward-bounded-multi-objective

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})

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<typename SparseModelType::ValueType> oneStepProbs;
+                std::vector<ConstantType> oneStepProbs;
                 oneStepProbs.reserve(parameterLifter->getMatrix().getRowCount());
                 for (uint64_t row = 0; row < parameterLifter->getMatrix().getRowCount(); ++row) {
-                    oneStepProbs.push_back(storm::utility::one<typename SparseModelType::ValueType>() - parameterLifter->getMatrix().getRowSum(row));
+                    oneStepProbs.push_back(storm::utility::one<ConstantType>() - parameterLifter->getMatrix().getRowSum(row));
                 }
                 if (dirForParameters == storm::OptimizationDirection::Minimize) {
-                    storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<typename SparseModelType::ValueType> dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+                    storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<ConstantType> dsmpi(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
                     solver->setUpperBounds(dsmpi.computeUpperBounds());
                 } else {
-                    storm::modelchecker::helper::BaierUpperRewardBoundsComputer<typename SparseModelType::ValueType> baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
+                    storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ConstantType> baier(parameterLifter->getMatrix(), parameterLifter->getVector(), oneStepProbs);
                     solver->setUpperBound(baier.computeUpperBound());
                 }
             }

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<ValueType>::SolutionMethod::ValueIteration && isTrackSchedulerSet()) {
+            if (this->getSettings().getSolutionMethod() == IterativeMinMaxLinearEquationSolverSettings<ValueType>::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<uint_fast64_t>(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()) {

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();
             }