no maximal end component decomposition for multi-obj model checking when it is not necessary.

src/storm/modelchecker/multiobjective/pcaa.cpp

@@ -31,7 +31,7 @@ namespace storm {
                 }
                 
                 auto preprocessorResult = SparsePcaaPreprocessor<SparseModelType>::preprocess(model, formula);
-                STORM_LOG_DEBUG("Preprocessing done. Result: " << preprocessorResult);
+                STORM_LOG_INFO("Preprocessing done. Result: " << preprocessorResult);
                 
                 std::unique_ptr<SparsePcaaQuery<SparseModelType, storm::RationalNumber>> query;
                 switch (preprocessorResult.queryType) {

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

@@ -81,6 +81,7 @@ namespace storm {
                         return;
                     }
                     STORM_LOG_DEBUG("Current precision of the approximation of the pareto curve is ~" << storm::utility::convertNumber<double>(farestDistance));
+                    std::cout << "Current precision of the approximation of the pareto curve is ~" << storm::utility::convertNumber<double>(farestDistance) << std::endl;
                     WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector();
                     this->performRefinementStep(std::move(direction));
                 }

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

@@ -27,7 +27,7 @@ namespace storm {
                 
                 //Invoke preprocessing on the individual objectives
                 for(auto const& subFormula : originalFormula.getSubformulas()){
-                    STORM_LOG_DEBUG("Preprocessing objective " << *subFormula<< ".");
+                    STORM_LOG_INFO("Preprocessing objective " << *subFormula<< ".");
                     result.objectives.emplace_back();
                     PcaaObjective<ValueType>& currentObjective = result.objectives.back();
                     currentObjective.originalFormula = subFormula;
@@ -37,7 +37,6 @@ namespace storm {
                         STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported");
                     }
                 }
-                
                 // Set the query type. In case of a quantitative query, also set the index of the objective to be optimized.
                 // Note: If there are only zero (or one) objectives left, we should not consider a pareto query!
                 storm::storage::BitVector objectivesWithoutThreshold(result.objectives.size());
@@ -55,13 +54,13 @@ namespace storm {
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The number of objectives without threshold is not valid. It should be either 0 (achievability query), 1 (quantitative query), or " << result.objectives.size() << " (Pareto Query). Got " << numOfObjectivesWithoutThreshold << " instead.");
                 }
-                
+
                 //We can remove the original reward models to save some memory
                 std::set<std::string> origRewardModels = originalFormula.getReferencedRewardModels();
                 for (auto const& rewModel : origRewardModels){
                     result.preprocessedModel.removeRewardModel(rewModel);
                 }
-                
+
                 //Get actions to which a positive or negative reward is assigned for at least one objective
                 result.actionsWithPositiveReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false);
                 result.actionsWithNegativeReward = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false);
@@ -74,11 +73,16 @@ namespace storm {
                         }
                     }
                 }
-                
-                auto backwardTransitions = result.preprocessedModel.getBackwardTransitions();
-                analyzeEndComponents(result, backwardTransitions);
-                ensureRewardFiniteness(result, backwardTransitions);
-                
+
+                // Analyze End components and ensure reward finiteness.
+                // Note that this is only necessary if there is at least one objective with no upper time bound
+                for (auto const& obj : result.objectives) {
+                    if(!obj.upperTimeBound) {
+                        auto backwardTransitions = result.preprocessedModel.getBackwardTransitions();
+                        analyzeEndComponents(result, backwardTransitions);
+                        ensureRewardFiniteness(result, backwardTransitions);
+                    }
+                }
                 return result;
             }
             

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

@@ -121,6 +121,7 @@ namespace storm {
                 }
                 overApproximation = overApproximation->intersection(h);
                 STORM_LOG_DEBUG("Updated OverApproximation to " << overApproximation->toString(true));
+                std::cout << "Updated OverApproximation to " << overApproximation->toString(true) << std::endl;
             }
             
             template <class SparseModelType, typename GeometryValueType>
@@ -132,6 +133,7 @@ namespace storm {
                 }
                 underApproximation = storm::storage::geometry::Polytope<GeometryValueType>::createDownwardClosure(paretoPoints);
                 STORM_LOG_DEBUG("Updated UnderApproximation to " << underApproximation->toString(true));
+                std::cout << "Updated UnderApproximation to " << underApproximation->toString(true) << std::endl;
             }
             
             template <class SparseModelType, typename GeometryValueType>

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

@@ -50,7 +50,7 @@ namespace storm {
             template <class SparseModelType>
             void SparsePcaaWeightVectorChecker<SparseModelType>::check(std::vector<ValueType> const& weightVector) {
                 checkHasBeenCalled=true;
-                STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(weightVector)));
+                STORM_LOG_INFO("Invoked WeightVectorChecker with weights " << std::endl << "\t" << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(weightVector)));
                 std::vector<ValueType> weightedRewardVector(model.getTransitionMatrix().getRowCount(), storm::utility::zero<ValueType>());
                 for(auto objIndex : objectivesWithNoUpperTimeBound) {
                     storm::utility::vector::addScaledVector(weightedRewardVector, discreteActionRewards[objIndex], weightVector[objIndex]);
@@ -64,7 +64,7 @@ namespace storm {
                         break;
                     }
                 }
-                STORM_LOG_DEBUG("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(getLowerBoundsOfInitialStateResults())));
+                STORM_LOG_INFO("Weight vector check done. Lower bounds for results in initial state: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(getLowerBoundsOfInitialStateResults())));
                 // Validate that the results are sufficiently precise
                 ValueType resultingWeightedPrecision = storm::utility::vector::dotProduct(getUpperBoundsOfInitialStateResults(), weightVector) - storm::utility::vector::dotProduct(getLowerBoundsOfInitialStateResults(), weightVector);
                 STORM_LOG_THROW(resultingWeightedPrecision >= storm::utility::zero<ValueType>(), storm::exceptions::UnexpectedException, "The distance between the lower and the upper result is negative.");
@@ -146,8 +146,10 @@ namespace storm {
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.create(ecEliminatorResult.matrix);
                 solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
                 solver->setTrackScheduler(true);
+                std::cout << "invoked minmaxsolver" << std::endl;
                 solver->solveEquations(subResult, subRewardVector);
-                
+                std::cout << "minmaxsolver done" << std::endl;
+
                 this->weightedResult = std::vector<ValueType>(model.getNumberOfStates());
                 std::vector<uint_fast64_t> optimalChoices(model.getNumberOfStates());