diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp index 32578be5c..024b71730 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpRewardBoundedPcaaWeightVectorChecker.cpp @@ -56,8 +56,8 @@ namespace storm { ++numCheckedEpochs; swEqBuilding.start(); - auto& result = cachedData.solutions; - result.resize(epochModel.epochInStates.getNumberOfSetBits(), typename MultiDimensionalRewardUnfolding::SolutionType()); + std::vector::SolutionType> result; + result.reserve(epochModel.epochInStates.getNumberOfSetBits()); uint64_t solutionSize = this->objectives.size() + 1; // Formulate a min-max equation system max(A*x+b)=x for the weighted sum of the objectives @@ -87,12 +87,10 @@ namespace storm { cachedData.minMaxSolver->solveEquations(cachedData.xMinMax, cachedData.bMinMax); swMinMaxSolving.stop(); swEqBuilding.start(); - auto resultIt = result.begin(); for (auto const& state : epochModel.epochInStates) { - resultIt->clear(); - resultIt->reserve(solutionSize); - resultIt->push_back(cachedData.xMinMax[state]); - ++resultIt; + result.emplace_back(); + result.back().reserve(solutionSize); + result.back().push_back(cachedData.xMinMax[state]); } // Check whether the linear equation solver needs to be updated @@ -144,7 +142,7 @@ namespace storm { cachedData.linEqSolver->solveEquations(x, cachedData.bLinEq); swLinEqSolving.stop(); swEqBuilding.start(); - resultIt = result.begin(); + auto resultIt = result.begin(); for (auto const& state : epochModel.epochInStates) { resultIt->push_back(x[state]); ++resultIt; @@ -152,7 +150,7 @@ namespace storm { } swEqBuilding.stop(); swAux3.stop(); - rewardUnfolding.setSolutionForCurrentEpoch(result); + rewardUnfolding.setSolutionForCurrentEpoch(std::move(result)); } template diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.cpp index e5a4affbd..4431e00e4 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/EpochManager.cpp @@ -29,12 +29,12 @@ namespace storm { } uint64_t const& EpochManager::getDimensionCount() const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); return dimensionCount; } bool EpochManager::compareEpochClass(Epoch const& epoch1, Epoch const& epoch2) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); uint64_t mask = dimensionBitMask; for (uint64_t d = 0; d < dimensionCount; ++d) { if (((epoch1 & mask) == mask) != ((epoch2 & mask) == mask)) { @@ -48,7 +48,7 @@ namespace storm { } typename EpochManager::EpochClass EpochManager::getEpochClass(Epoch const& epoch) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); EpochClass result = 0; uint64_t mask = dimensionBitMask; for (uint64_t d = 0; d < dimensionCount; ++d) { @@ -62,13 +62,13 @@ namespace storm { } typename EpochManager::Epoch EpochManager::getSuccessorEpoch(Epoch const& epoch, Epoch const& step) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); - + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(!hasBottomDimension(step), "The given step has at least one bottom dimension."); + // Start with dimension zero uint64_t mask = dimensionBitMask; uint64_t e_d = epoch & mask; uint64_t s_d = step & mask; - assert(s_d != mask); uint64_t result = (e_d < s_d || e_d == mask) ? mask : e_d - s_d; // Consider the remaining dimensions @@ -76,39 +76,72 @@ namespace storm { mask = mask << bitsPerDimension; e_d = epoch & mask; s_d = step & mask; - assert(s_d != mask); result |= ((e_d < s_d || e_d == mask) ? mask : e_d - s_d); } return result; } std::vector EpochManager::getPredecessorEpochs(Epoch const& epoch, Epoch const& step) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); - + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(!hasBottomDimension(step), "The given step has at least one bottom dimension."); + std::set resultAsSet; + gatherPredecessorEpochs(resultAsSet, epoch, step); + return std::vector(resultAsSet.begin(), resultAsSet.end()); } void EpochManager::gatherPredecessorEpochs(std::set& gatheredPredecessorEpochs, Epoch const& epoch, Epoch const& step) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); - + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(!hasBottomDimension(step), "The given step has at least one bottom dimension."); + Epoch currStep = step; + uint64_t d = 0; + while (d < dimensionCount) { + Epoch predecessor = epoch; + for (uint64_t dPrime = 0; dPrime < dimensionCount; ++dPrime) { + uint64_t step_dPrime = getDimensionOfEpoch(currStep, dPrime); + if (isBottomDimension(predecessor, dPrime)) { + if (step_dPrime != 0) { + setDimensionOfEpoch(predecessor, dPrime, step_dPrime - 1); + } + } else { + setDimensionOfEpoch(predecessor, dPrime, getDimensionOfEpoch(predecessor, dPrime) + step_dPrime); + } + } + assert(epoch == getSuccessorEpoch(predecessor, step)); + gatheredPredecessorEpochs.insert(predecessor); + + do { + if (isBottomDimension(epoch, d)) { + uint64_t step_d = getDimensionOfEpoch(currStep, d); + if (step_d == 0) { + setDimensionOfEpoch(currStep, d, getDimensionOfEpoch(step, d)); + } else { + setDimensionOfEpoch(currStep, d, step_d - 1); + d = 0; + break; + } + } + ++d; + } while(d < dimensionCount); + } } bool EpochManager::isValidDimensionValue(uint64_t const& value) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); return ((value & dimensionBitMask) == value) && value != dimensionBitMask; } bool EpochManager::isZeroEpoch(Epoch const& epoch) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); return (epoch & relevantBitsMask) == 0; } bool EpochManager::isBottomEpoch(Epoch const& epoch) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); return (epoch & relevantBitsMask) == relevantBitsMask; } bool EpochManager::hasBottomDimension(Epoch const& epoch) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); uint64_t mask = dimensionBitMask; for (uint64_t d = 0; d < dimensionCount; ++d) { if ((epoch | mask) == epoch) { @@ -120,29 +153,29 @@ namespace storm { } void EpochManager::setBottomDimension(Epoch& epoch, uint64_t const& dimension) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); epoch |= (dimensionBitMask << (dimension * bitsPerDimension)); } void EpochManager::setDimensionOfEpoch(Epoch& epoch, uint64_t const& dimension, uint64_t const& value) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); STORM_LOG_ASSERT(isValidDimensionValue(value), "The dimension value " << value << " is too high."); epoch &= ~(dimensionBitMask << (dimension * bitsPerDimension)); epoch |= (value << (dimension * bitsPerDimension)); } bool EpochManager::isBottomDimension(Epoch const& epoch, uint64_t const& dimension) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); return (epoch | (dimensionBitMask << (dimension * bitsPerDimension))) == epoch; } uint64_t EpochManager::getDimensionOfEpoch(Epoch const& epoch, uint64_t const& dimension) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); return (epoch >> (dimension * bitsPerDimension)) & dimensionBitMask; } std::string EpochManager::toString(Epoch const& epoch) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); std::string res = "<" + (isBottomDimension(epoch, 0) ? "_" : std::to_string(getDimensionOfEpoch(epoch, 0))); for (uint64_t d = 1; d < dimensionCount; ++d) { res += ", "; @@ -153,7 +186,7 @@ namespace storm { } bool EpochManager::epochClassZigZagOrder(Epoch const& epoch1, Epoch const& epoch2) const { - STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked EpochManager with zero dimension count."); + STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count."); // Return true iff epoch 1 has to be computed before epoch 2 diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp index 413444142..a4e84ec6f 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.cpp @@ -389,7 +389,6 @@ namespace storm { swAux4.start(); epochModel.epochMatrix = std::move(ecElimResult.matrix); epochModelToProductChoiceMap = std::move(ecElimResult.newToOldRowMapping); - productToEpochModelStateMap = std::move(ecElimResult.oldToNewStateMapping); epochModel.stepChoices = storm::storage::BitVector(epochModel.epochMatrix.getRowCount(), false); for (uint64_t choice = 0; choice < epochModel.epochMatrix.getRowCount(); ++choice) { @@ -410,14 +409,17 @@ namespace storm { epochModel.epochInStates = storm::storage::BitVector(epochModel.epochMatrix.getRowGroupCount(), false); for (auto const& productState : productInStates) { - STORM_LOG_ASSERT(productToEpochModelStateMap[productState] < epochModel.epochMatrix.getRowGroupCount(), "Selected product state does not exist in the epoch model."); - epochModel.epochInStates.set(productToEpochModelStateMap[productState], true); + STORM_LOG_ASSERT(ecElimResult.oldToNewStateMapping[productState] < epochModel.epochMatrix.getRowGroupCount(), "Selected product state does not exist in the epoch model."); + epochModel.epochInStates.set(ecElimResult.oldToNewStateMapping[productState], true); } epochModelInStateToProductStatesMap.assign(epochModel.epochInStates.getNumberOfSetBits(), std::vector()); + std::vector toEpochModelInStatesMap(productModel->getProduct().getNumberOfStates(), std::numeric_limits::max()); for (auto const& productState : productInStates) { - epochModelInStateToProductStatesMap[epochModel.epochInStates.getNumberOfSetBitsBeforeIndex(productToEpochModelStateMap[productState])].push_back(productState); + toEpochModelInStatesMap[productState] = epochModel.epochInStates.getNumberOfSetBitsBeforeIndex(ecElimResult.oldToNewStateMapping[productState]); + epochModelInStateToProductStatesMap[epochModel.epochInStates.getNumberOfSetBitsBeforeIndex(ecElimResult.oldToNewStateMapping[productState])].push_back(productState); } + productStateToEpochModelInStateMap = std::make_shared const>(std::move(toEpochModelInStatesMap)); swAux4.stop(); swSetEpochClass.stop(); @@ -478,49 +480,47 @@ namespace storm { } template - void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector& inStateSolutions) { + void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(std::vector&& inStateSolutions) { swInsertSol.start(); + STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before."); STORM_LOG_ASSERT(inStateSolutions.size() == epochModelInStateToProductStatesMap.size(), "Invalid number of solutions."); - auto solIt = inStateSolutions.begin(); - for (auto const& productStates : epochModelInStateToProductStatesMap) { - assert(!productStates.empty()); - auto productStateIt = productStates.begin(); - // Skip the first product state for now. It's result will be std::move'd afterwards. - for (++productStateIt; productStateIt != productStates.end(); ++productStateIt) { - setSolutionForCurrentEpoch(*productStateIt, *solIt); + + std::set predecessorEpochs, successorEpochs; + for (auto const& step : possibleEpochSteps) { + epochManager.gatherPredecessorEpochs(predecessorEpochs, currentEpoch.get(), step); + successorEpochs.insert(epochManager.getSuccessorEpoch(currentEpoch.get(), step)); + } + predecessorEpochs.erase(currentEpoch.get()); + successorEpochs.erase(currentEpoch.get()); + STORM_LOG_ASSERT(!predecessorEpochs.empty(), "There are no predecessors for the epoch " << epochManager.toString(currentEpoch.get())); + + // clean up solutions that are not needed anymore + for (auto const& successorEpoch : successorEpochs) { + auto successorEpochSolutionIt = epochSolutions.find(successorEpoch); + STORM_LOG_ASSERT(successorEpochSolutionIt != epochSolutions.end(), "Solution for successor epoch does not exist (anymore)."); + --successorEpochSolutionIt->second.count; + if (successorEpochSolutionIt->second.count == 0) { + epochSolutions.erase(successorEpochSolutionIt); } - setSolutionForCurrentEpoch(productStates.front(), std::move(*solIt)); - - ++solIt; } - maxSolutionsStored = std::max((uint64_t) solutions.size(), maxSolutionsStored); + // add the new solution + EpochSolution solution; + solution.count = predecessorEpochs.size(); + solution.productStateToSolutionVectorMap = productStateToEpochModelInStateMap; + solution.solutions = std::move(inStateSolutions); + epochSolutions[currentEpoch.get()] = std::move(solution); + + maxSolutionsStored = std::max((uint64_t) epochSolutions.size(), maxSolutionsStored); swInsertSol.stop(); - } - - template - void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution) { - STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before."); - // std::cout << "Setting solution for state " << productState << " in epoch " << epochManager.toString(currentEpoch.get()) << std::endl; - solutions[std::make_pair(currentEpoch.get(), productState)] = solution; - } - - template - void MultiDimensionalRewardUnfolding::setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType&& solution) { - STORM_LOG_ASSERT(currentEpoch, "Tried to set a solution for the current epoch, but no epoch was specified before."); - // std::cout << "Setting solution for state " << productState << " in epoch " << epochManager.toString(currentEpoch.get()) << std::endl; - solutions[std::make_pair(currentEpoch.get(), productState)] = std::move(solution); + } template typename MultiDimensionalRewardUnfolding::SolutionType const& MultiDimensionalRewardUnfolding::getStateSolution(Epoch const& epoch, uint64_t const& productState) { - swFindSol.start(); - //std::cout << "Getting solution for epoch " << epochManager.toString(epoch) << " and state " << productState << std::endl; - auto solutionIt = solutions.find(std::make_pair(epoch, productState)); - STORM_LOG_ASSERT(solutionIt != solutions.end(), "Requested unexisting solution for epoch " << epochManager.toString(epoch) << "."); - //std::cout << "Retrieved solution for state " << productState << " in epoch " << epochManager.toString(epoch) << std::endl; - swFindSol.stop(); - return solutionIt->second; + STORM_LOG_ASSERT(epochSolutions.find(epoch) != epochSolutions.end(), "Requested unexisting solution for epoch " << epochManager.toString(epoch) << "."); + EpochSolution const& epochSolution = epochSolutions[epoch]; + return epochSolution.solutions[(*epochSolution.productStateToSolutionVectorMap)[productState]]; } template diff --git a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h index a749f5300..521e3fb2d 100644 --- a/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h +++ b/src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h @@ -73,7 +73,7 @@ namespace storm { EpochModel& setCurrentEpoch(Epoch const& epoch); - void setSolutionForCurrentEpoch(std::vector& inStateSolutions); + void setSolutionForCurrentEpoch(std::vector&& inStateSolutions); SolutionType const& getInitialStateResult(Epoch const& epoch); // Assumes that the initial state is unique SolutionType const& getInitialStateResult(Epoch const& epoch, uint64_t initialStateIndex); @@ -104,8 +104,6 @@ namespace storm { template::type = 0> std::string solutionToString(SolutionType const& solution) const; - void setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType const& solution); - void setSolutionForCurrentEpoch(uint64_t const& productState, SolutionType&& solution); SolutionType const& getStateSolution(Epoch const& epoch, uint64_t const& productState); storm::models::sparse::Mdp const& model; @@ -114,7 +112,7 @@ namespace storm { std::unique_ptr> productModel; std::vector epochModelToProductChoiceMap; - std::vector productToEpochModelStateMap; + std::shared_ptr const> productStateToEpochModelInStateMap; std::vector> epochModelInStateToProductStatesMap; std::set possibleEpochSteps; @@ -129,7 +127,12 @@ namespace storm { std::vector scalingFactors; - std::map, SolutionType> solutions; + struct EpochSolution { + uint64_t count; + std::shared_ptr const> productStateToSolutionVectorMap; + std::vector solutions; + }; + std::map epochSolutions; storm::utility::Stopwatch swInit, swFindSol, swInsertSol, swSetEpoch, swSetEpochClass, swAux1, swAux2, swAux3, swAux4; diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index ca5ff1cae..6dba4aeab 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -77,7 +77,7 @@ namespace storm { auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch); // initialize data that will be needed for each epoch - std::vector x, b, epochResult; + std::vector x, b; std::unique_ptr> minMaxSolver; for (auto const& epoch : epochOrder) { // Update some data for the case that the Matrix has changed @@ -108,9 +108,7 @@ namespace storm { minMaxSolver->solveEquations(x, b); // Plug in the result into the reward unfolding - epochResult.resize(epochModel.epochInStates.getNumberOfSetBits()); - storm::utility::vector::selectVectorValues(epochResult, epochModel.epochInStates, x); - rewardUnfolding.setSolutionForCurrentEpoch(epochResult); + rewardUnfolding.setSolutionForCurrentEpoch(storm::utility::vector::filterVector(x, epochModel.epochInStates)); } std::map result;