diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp index 0f1b88684..8e4dd4f08 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp @@ -25,20 +25,14 @@ namespace storm { template void SparseMultiObjectiveWeightVectorChecker::check(std::vector const& weightVector) { - //STORM_LOG_DEBUG("Checking weighted objectives with weight vector " << std::endl << "\t" << weightVector); + checkHasBeenCalled=true; + STORM_LOG_DEBUG("Invoked WeightVectorChecker with weights " << std::endl << "\t" << weightVector); unboundedWeightedPhase(weightVector); - //STORM_LOG_DEBUG("Unbounded weighted phase resulted in " << std::endl << "\t Result: " << weightedResult << std::endl << "\t Scheduler: " << scheduler); + STORM_LOG_DEBUG("Unbounded weighted phase result: " << weightedResult[data.preprocessedModel.getInitialStates().getNextSetIndex(0)] << " (value in initial state)."); unboundedIndividualPhase(weightVector); - //STORM_LOG_DEBUG("Unbounded individual phase resulted in..."); - for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { - // STORM_LOG_DEBUG("\t objective " << objIndex << ":" << objectiveResults[objIndex]); - } + STORM_LOG_DEBUG("Unbounded individual phase results in initial state: " << getInitialStateResultOfObjectives()); boundedPhase(weightVector); - // STORM_LOG_DEBUG("Bounded phase resulted in..."); - for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) { - // STORM_LOG_DEBUG("\t objective " << objIndex << ":" << objectiveResults[objIndex]); - } - checkHasBeenCalled=true; + STORM_LOG_DEBUG("Bounded individual phase results in initial state: " << getInitialStateResultOfObjectives() << " ...WeightVectorChecker done."); } template @@ -146,19 +140,15 @@ namespace storm { //Also only compute values for objectives with weightVector != zero, //one check can be omitted as the result can be computed back from the weighed result and the results from the remaining objectives for(uint_fast64_t objIndex = 0; objIndex < weightVector.size(); ++objIndex) { - if(!data.objectives[objIndex].stepBound){ - + if(data.objectives[objIndex].stepBound){ + objectiveResults[objIndex] = std::vector(data.preprocessedModel.getNumberOfStates(), storm::utility::zero()); + } else { storm::utility::vector::selectVectorValues(deterministicStateRewards, this->scheduler.getChoices(), data.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector()); - - //std::cout << "stateActionRewardVector for objective " << objIndex << " is " << storm::utility::vector::toString(data.preprocessedModel.getRewardModel(data.objectives[objIndex].rewardModelName).getStateActionRewardVector()) << std::endl; - //std::cout << "deterministic state rewards for objective " << objIndex << " are " << storm::utility::vector::toString(deterministicStateRewards) << std::endl; - storm::storage::BitVector statesWithRewards = ~storm::utility::vector::filterZero(deterministicStateRewards); - // As target states, we take the states from which no reward is reachable. - STORM_LOG_WARN("TODO: target state selection is currently only valid for reachability properties..."); - //TODO: we should be able to give some hint to the solver.. - storm::storage::BitVector targetStates = storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); - targetStates.complement(); + // As target states, we pick the states from which no reward is reachable. + storm::storage::BitVector targetStates = ~storm::utility::graph::performProbGreater0(deterministicBackwardTransitions, storm::storage::BitVector(deterministicMatrix.getRowCount(), true), statesWithRewards); + + //TODO: we could give the solver some hint for the result (e.g., weightVector[ObjIndex] * weightedResult or (weightedResult - sum_i=0^objIndex-1 objectiveResult) * weightVector[objIndex]/ sum_i=objIndex^n weightVector[i] ) objectiveResults[objIndex] = storm::modelchecker::helper::SparseDtmcPrctlHelper::computeReachabilityRewards(deterministicMatrix, deterministicBackwardTransitions, deterministicStateRewards, diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index aa3a469a0..0179b4213 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -42,14 +42,6 @@ namespace storm { newX = new std::vector(x.size()); xMemoryProvided = false; } - - std::vector currentScheduler; - std::vector newScheduler; - if(this->trackScheduler){ - //Allocate memory for the schedulers and initialize them with valid choices - currentScheduler = std::vector(this->A.getRowGroupCount()); - newScheduler = std::vector(this->A.getRowGroupCount()); - } uint_fast64_t iterations = 0; bool converged = false; @@ -63,24 +55,8 @@ namespace storm { gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult); gmm::add(b, *multiplyResult); - if(this->trackScheduler){ - // Reduce the vector x by applying min/max over all nondeterministic choices. Also keep track of the choices made - storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices, &newScheduler); - // We update the currentScheduler conservatively - // This is to prevent that e.g. a choice for a selfloop with probability 1 is taken - auto currentChoice = currentScheduler.begin(); - auto newChoice = newScheduler.begin(); - for(storm::storage::sparse::state_type state = 0; stateprecision, this->relative)){ - *currentChoice = *newChoice; - } - ++currentChoice; - ++newChoice; - } - } else { - // Reduce the vector x by applying min/max over all nondeterministic choices. - storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices); - } + // Reduce the vector x by applying min/max over all nondeterministic choices. + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, *newX, rowGroupIndices); // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->precision, this->relative); @@ -96,17 +72,24 @@ namespace storm { } else { STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations."); } - - // If requested, we store the scheduler for retrieval. - if (this->isTrackSchedulerSet()) { - this->scheduler = std::make_unique(std::move(currentScheduler)); - } // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result // is currently stored in currentX, but x is the output vector. if (currentX == copyX) { std::swap(x, *currentX); } + + // If requested, we store the scheduler for retrieval. + if (this->isTrackSchedulerSet()) { + if(iterations==0){ //may happen due to custom termination condition. Then we need to compute x'= A*x+b + gmm::mult(*gmmxxMatrix, x, *multiplyResult); + gmm::add(b, *multiplyResult); + } + std::vector choices(this->A.getRowGroupCount()); + // Reduce the multiplyResult again and keep track of the choices made + storm::utility::vector::reduceVectorMinOrMax(dir, *multiplyResult, x, rowGroupIndices, &choices); + this->scheduler = std::make_unique(std::move(choices)); + } if (!xMemoryProvided) { delete copyX;