Merge branch 'multi-objective'

src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp

@@ -74,12 +74,12 @@ namespace storm {
                     updateDataToCurrentEpoch(MS, PS, *minMax, consideredObjectives, currentEpoch, weightVector, lowerTimeBoundIt, lowerTimeBounds, upperTimeBoundIt, upperTimeBounds);
                     
                     // Compute the values that can be obtained at probabilistic states in the current time epoch
-                    performPSStep(PS, MS, *minMax, *linEq, optimalChoicesAtCurrentEpoch,  consideredObjectives);
+                    performPSStep(PS, MS, *minMax, *linEq, optimalChoicesAtCurrentEpoch,  consideredObjectives, weightVector);
                     
                     // Compute values that can be obtained at Markovian states after letting one (digitized) time unit pass.
                     // Only perform such a step if there is time left.
                     if(currentEpoch>0) {
-                        performMSStep(MS, PS, consideredObjectives);
+                        performMSStep(MS, PS, consideredObjectives, weightVector);
                         --currentEpoch;
                     } else {
                         break;
@@ -354,10 +354,19 @@ namespace storm {
             }
             
             template <class SparseMaModelType>
-            void SparseMaPcaaWeightVectorChecker<SparseMaModelType>::performPSStep(SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector<uint_fast64_t>& optimalChoicesAtCurrentEpoch,  storm::storage::BitVector const& consideredObjectives) const {
+            void SparseMaPcaaWeightVectorChecker<SparseMaModelType>::performPSStep(SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector<uint_fast64_t>& optimalChoicesAtCurrentEpoch,  storm::storage::BitVector const& consideredObjectives, std::vector<ValueType> const& weightVector) const {
                 // compute a choice vector for the probabilistic states that is optimal w.r.t. the weighted reward vector
                 minMax.solver->solveEquations(PS.weightedSolutionVector, minMax.b);
                 auto newScheduler = minMax.solver->getScheduler();
+                if(consideredObjectives.getNumberOfSetBits() == 1 && !storm::utility::isZero(weightVector[*consideredObjectives.begin()])) {
+                    // In this case there is no need to perform the computation on the individual objectives
+                    optimalChoicesAtCurrentEpoch = newScheduler->getChoices();
+                    auto objIndex = *consideredObjectives.begin();
+                    PS.objectiveSolutionVectors[objIndex] = PS.weightedSolutionVector;
+                    if(!storm::utility::isOne(weightVector[objIndex])) {
+                        storm::utility::vector::scaleVectorInPlace(PS.objectiveSolutionVectors[objIndex], storm::utility::one<ValueType>()/weightVector[objIndex]);
+                    }
+                } else {
                     // check whether the linEqSolver needs to be updated, i.e., whether the scheduler has changed
                     if(linEq.solver == nullptr || newScheduler->getChoices() != optimalChoicesAtCurrentEpoch) {
                         optimalChoicesAtCurrentEpoch = newScheduler->getChoices();
@@ -389,15 +398,23 @@ namespace storm {
                         linEq.solver->solveEquations(PS.objectiveSolutionVectors[objIndex], linEq.b);
                     }
                 }
+            }
 
             template <class SparseMaModelType>
-            void SparseMaPcaaWeightVectorChecker<SparseMaModelType>::performMSStep(SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives) const {
+            void SparseMaPcaaWeightVectorChecker<SparseMaModelType>::performMSStep(SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives, std::vector<ValueType> const& weightVector) const {
                 
                 MS.toMS.multiplyWithVector(MS.weightedSolutionVector, MS.auxChoiceValues);
                 storm::utility::vector::addVectors(MS.weightedRewardVector, MS.auxChoiceValues, MS.weightedSolutionVector);
                 MS.toPS.multiplyWithVector(PS.weightedSolutionVector, MS.auxChoiceValues);
                 storm::utility::vector::addVectors(MS.weightedSolutionVector, MS.auxChoiceValues, MS.weightedSolutionVector);
-                
+                if(consideredObjectives.getNumberOfSetBits() == 1 && !storm::utility::isZero(weightVector[*consideredObjectives.begin()])) {
+                    // In this case there is no need to perform the computation on the individual objectives
+                    auto objIndex = *consideredObjectives.begin();
+                    MS.objectiveSolutionVectors[objIndex] = MS.weightedSolutionVector;
+                    if(!storm::utility::isOne(weightVector[objIndex])) {
+                        storm::utility::vector::scaleVectorInPlace(MS.objectiveSolutionVectors[objIndex], storm::utility::one<ValueType>()/weightVector[objIndex]);
+                    }
+                } else {
                     for(auto objIndex : consideredObjectives) {
                         MS.toMS.multiplyWithVector(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues);
                         storm::utility::vector::addVectors(MS.objectiveRewardVectors[objIndex], MS.auxChoiceValues, MS.objectiveSolutionVectors[objIndex]);
@@ -405,6 +422,7 @@ namespace storm {
                         storm::utility::vector::addVectors(MS.objectiveSolutionVectors[objIndex], MS.auxChoiceValues, MS.objectiveSolutionVectors[objIndex]);
                     }
                 }
+            }
             
             
             template class SparseMaPcaaWeightVectorChecker<storm::models::sparse::MarkovAutomaton<double>>;

src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h

@@ -138,7 +138,7 @@ namespace storm {
                  * 
                  * The resulting values represent the rewards at probabilistic states that are obtained at the current time epoch.
                  */
-                void performPSStep(SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector<uint_fast64_t>& optimalChoicesAtCurrentEpoch,  storm::storage::BitVector const& consideredObjectives) const;
+                void performPSStep(SubModel& PS, SubModel const& MS, MinMaxSolverData& minMax, LinEqSolverData& linEq, std::vector<uint_fast64_t>& optimalChoicesAtCurrentEpoch,  storm::storage::BitVector const& consideredObjectives, std::vector<ValueType> const& weightVector) const;
                 
                 /*
                  * Performs a step for the Markovian states, that is
@@ -146,7 +146,7 @@ namespace storm {
                  *
                  * The resulting values represent the rewards at Markovian states that are obtained after one (digitized) time unit has passed.
                  */
-                void performMSStep(SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives) const;
+                void performMSStep(SubModel& MS, SubModel const& PS, storm::storage::BitVector const& consideredObjectives, std::vector<ValueType> const& weightVector) const;
                 
             };
             

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp

@@ -51,8 +51,6 @@ namespace storm {
             
             template <class SparseModelType, typename GeometryValueType>
             std::unique_ptr<CheckResult> SparsePcaaQuantitativeQuery<SparseModelType, GeometryValueType>::check() {
-               
-                
                 // First find one solution that achieves the given thresholds ...
                 if(this->checkAchievability()) {
                     // ... then improve it
@@ -73,6 +71,7 @@ namespace storm {
             
             template <class SparseModelType, typename GeometryValueType>
             bool SparsePcaaQuantitativeQuery<SparseModelType, GeometryValueType>::checkAchievability() {
+                 if(this->objectives.size()>1) {
                     // We don't care for the optimizing objective at this point
                     this->diracWeightVectorsToBeChecked.set(indexOfOptimizingObjective, false);
                 
@@ -89,6 +88,10 @@ namespace storm {
                             return true;
                         }
                     }
+                } else {
+                    // If there is only one objective than its the optimizing one. Thus the query has to be achievable.
+                    return true;
+                }
                 STORM_LOG_ERROR("Could not check whether thresholds are achievable: Exceeded maximum number of refinement steps");
                 return false;
             }
@@ -124,6 +127,12 @@ namespace storm {
                 // thresholds) and (with very low probability) a scheduler that satisfies all (possibly strict) thresholds.
                 GeometryValueType result = storm::utility::zero<GeometryValueType>();
                 while(!this->maxStepsPerformed()) {
+                    if(this->refinementSteps.empty()) {
+                        // We did not make any refinement steps during the checkAchievability phase (e.g., because there is only one objective).
+                        this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber<typename SparseModelType::ValueType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision()));
+                        WeightVector separatingVector = directionOfOptimizingObjective;
+                        this->performRefinementStep(std::move(separatingVector));
+                    }
                     std::pair<Point, bool> optimizationRes = this->underApproximation->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective);
                     STORM_LOG_THROW(optimizationRes.second, storm::exceptions::UnexpectedException, "The underapproximation is either unbounded or empty.");
                     result = optimizationRes.first[indexOfOptimizingObjective];
@@ -155,11 +164,12 @@ namespace storm {
             void SparsePcaaQuantitativeQuery<SparseModelType, GeometryValueType>::updateWeightedPrecisionInImprovingPhase(WeightVector const& weights) {
                 STORM_LOG_THROW(!storm::utility::isZero(weights[this->indexOfOptimizingObjective]), exceptions::UnexpectedException, "The chosen weight-vector gives zero weight for the objective that is to be optimized.");
                 // If weighs[indexOfOptimizingObjective] is low, the computation of the weightVectorChecker needs to be more precise.
-                // Our heuristic ensures that if p is the new vertex of the under-approximation, then max{ eps | p' = p + (0..0 eps 0..0) is in the over-approximation } <= multiobjective_precision/2
+                // Our heuristic ensures that if p is the new vertex of the under-approximation, then max{ eps | p' = p + (0..0 eps 0..0) is in the over-approximation } <= multiobjective_precision/0.9
                     GeometryValueType weightedPrecision = weights[this->indexOfOptimizingObjective] * storm::utility::convertNumber<GeometryValueType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision());
                     // Normalize by division with the Euclidean Norm of the weight-vector
                     weightedPrecision /= storm::utility::sqrt(storm::utility::vector::dotProduct(weights, weights));
-                    weightedPrecision /= GeometryValueType(2);
+                    weightedPrecision *= storm::utility::convertNumber<GeometryValueType>(0.9);
+
                     this->weightVectorChecker->setWeightedPrecision(storm::utility::convertNumber<typename SparseModelType::ValueType>(weightedPrecision));
             }
             

src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp

@@ -159,6 +159,18 @@ namespace storm {
             template <class SparseModelType>
             void SparsePcaaWeightVectorChecker<SparseModelType>::unboundedIndividualPhase(std::vector<ValueType> const& weightVector) {
                 
+                if(objectivesWithNoUpperTimeBound.getNumberOfSetBits()==1) {
+                    auto objIndex = *objectivesWithNoUpperTimeBound.begin();
+                    objectiveResults[objIndex] = weightedResult;
+                    if(!storm::utility::isZero(weightVector[objIndex])) {
+                        storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], storm::utility::one<ValueType>()/weightVector[objIndex]);
+                    }
+                    for (uint_fast64_t objIndex2 = 0; objIndex2 < objectives.size(); ++objIndex2) {
+			if(objIndex != objIndex2) {
+                            objectiveResults[objIndex2] = std::vector<ValueType>(model.getNumberOfStates(), storm::utility::zero<ValueType>());
+                        }
+                    }
+                } else {
                     storm::storage::SparseMatrix<ValueType> deterministicMatrix = model.getTransitionMatrix().selectRowsFromRowGroups(this->scheduler.getChoices(), true);
                     storm::storage::SparseMatrix<ValueType> deterministicBackwardTransitions = deterministicMatrix.transpose();
                     std::vector<ValueType> deterministicStateRewards(deterministicMatrix.getRowCount());
@@ -205,6 +217,7 @@ namespace storm {
                         }
                     }
                 }
+            }
             
             template <class SparseModelType>
             void SparsePcaaWeightVectorChecker<SparseModelType>::transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix<ValueType> const& reducedMatrix,