From c401de1fb9ce2f1142c4201e20341ba37983b2a6 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 11 Jun 2016 00:43:03 +0200 Subject: [PATCH] handling of end components in which no reward is earned Former-commit-id: 84f61490110c3f1c1ff02e83d62ef45e245db95b --- ...SparseMultiObjectiveModelCheckerHelper.cpp | 4 +- ...seWeightedObjectivesModelCheckerHelper.cpp | 91 ++++---- src/transformer/EffectlessMECRemover.h | 211 ++++++++++++++++++ 3 files changed, 261 insertions(+), 45 deletions(-) create mode 100644 src/transformer/EffectlessMECRemover.h diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp index c29e112c0..07c0a2012 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveModelCheckerHelper.cpp @@ -327,8 +327,8 @@ namespace storm { } STORM_LOG_WARN("REMOVE ADDING ADDITIONAL VERTICES AS SOON AS HYPRO WORKS FOR DEGENERATED POLYTOPES"); - Point p1 = {-1000, 0}; - Point p2 = {0, -1000}; + Point p1 = {-1000, -999}; + Point p2 = {-999, -1000}; paretoPointsVec.push_back(p1); paretoPointsVec.push_back(p2); diff --git a/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp b/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp index 55d5262ca..9d0b969ce 100644 --- a/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp @@ -5,6 +5,7 @@ #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "src/solver/LinearEquationSolver.h" #include "src/solver/MinMaxLinearEquationSolver.h" +#include "src/transformer/EffectlessMECRemover.h" #include "src/utility/graph.h" #include "src/utility/macros.h" #include "src/utility/solver.h" @@ -70,55 +71,59 @@ namespace storm { //std::cout << "weighted reward vector is " << storm::utility::vector::toString(weightedRewardVector) << std::endl; - storm::storage::BitVector actionsWithRewards = storm::utility::vector::filter(weightedRewardVector, [&] (ValueType const& value) -> bool {return !storm::utility::isZero(value);}); - storm::storage::BitVector statesWithRewards(info.preprocessedModel.getNumberOfStates(), false); - uint_fast64_t currActionIndex = actionsWithRewards.getNextSetIndex(0); - auto endOfRowGroup = info.preprocessedModel.getTransitionMatrix().getRowGroupIndices().begin() + 1; - for(uint_fast64_t state = 0; stateweightedResult = std::vector(info.preprocessedModel.getNumberOfStates()); - this->scheduler = storm::storage::TotalScheduler(info.preprocessedModel.getNumberOfStates()); + // Remove end components in which no reward is earned + auto removerResult = storm::transformer::EffectlessMECRemover::transform(info.preprocessedModel.getTransitionMatrix(), weightedRewardVector, storm::storage::BitVector(info.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true)); - storm::storage::SparseMatrix submatrix = info.preprocessedModel.getTransitionMatrix().getSubmatrix(true, maybeStates, maybeStates, false); - std::vector b(submatrix.getRowCount()); - storm::utility::vector::selectVectorValues(b, maybeStates, info.preprocessedModel.getTransitionMatrix().getRowGroupIndices(), weightedRewardVector); - std::vector x(submatrix.getRowGroupCount(), storm::utility::zero()); + std::vector subResult(removerResult.matrix.getRowGroupCount()); storm::utility::solver::MinMaxLinearEquationSolverFactory solverFactory; - std::unique_ptr> solver = solverFactory.create(submatrix, true); + std::unique_ptr> solver = solverFactory.create(removerResult.matrix, true); solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); - solver->solveEquationSystem(x, b); - - storm::utility::vector::setVectorValues(this->weightedResult, maybeStates, x); - storm::utility::vector::setVectorValues(this->weightedResult, ~maybeStates, storm::utility::zero()); + solver->solveEquationSystem(subResult, removerResult.vector); - uint_fast64_t currentSubState = 0; - for (auto maybeState : maybeStates) { - this->scheduler.setChoice(maybeState, solver->getScheduler().getChoice(currentSubState)); - ++currentSubState; + this->weightedResult = std::vector(info.preprocessedModel.getNumberOfStates()); + this->scheduler = storm::storage::TotalScheduler(info.preprocessedModel.getNumberOfStates()); + storm::storage::BitVector statesWithUndefinedScheduler(info.preprocessedModel.getNumberOfStates(), false); + for(uint_fast64_t state = 0; state < info.preprocessedModel.getNumberOfStates(); ++state) { + uint_fast64_t stateInReducedModel = removerResult.oldToNewStateMapping[state]; + // Check if the state exists in the reduced model + if(stateInReducedModel < removerResult.matrix.getRowGroupCount()) { + this->weightedResult[state] = subResult[stateInReducedModel]; + // Check if the chosen row originaly belonged to the current state + uint_fast64_t chosenRowInReducedModel = removerResult.matrix.getRowGroupIndices()[stateInReducedModel] + solver->getScheduler().getChoice(stateInReducedModel); + uint_fast64_t chosenRowInOriginalModel = removerResult.newToOldRowMapping[chosenRowInReducedModel]; + if(chosenRowInOriginalModel >= info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state] && + chosenRowInOriginalModel < info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]) { + this->scheduler.setChoice(state, chosenRowInOriginalModel - info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]); + } else { + statesWithUndefinedScheduler.set(state); + } + } else { + // if the state does not exist in the reduced model, it means that the result is always zero, independent of the scheduler. + // Hence, we don't have to set the scheduler explicitly + this->weightedResult[state] = storm::utility::zero(); + } + } + while(!statesWithUndefinedScheduler.empty()) { + for(auto state : statesWithUndefinedScheduler) { + // Try to find a choice that stays inside the EC (i.e., for which all successors are represented by the same state in the reduced model) + // And at least one successor has a defined scheduler. + // This way, a scheduler is chosen that leads (with probability one) to the state from which the EC can be left + uint_fast64_t stateInReducedModel = removerResult.oldToNewStateMapping[state]; + for(uint_fast64_t row = info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row < info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { + bool rowStaysInEC = true; + bool rowLeadsToDefinedScheduler = false; + for(auto const& entry : info.preprocessedModel.getTransitionMatrix().getRow(row)) { + rowStaysInEC &= ( stateInReducedModel == removerResult.oldToNewStateMapping[entry.getColumn()]); + rowLeadsToDefinedScheduler |= !statesWithUndefinedScheduler.get(entry.getColumn()); + } + if(rowStaysInEC && rowLeadsToDefinedScheduler) { + this->scheduler.setChoice(state, row - info.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]); + statesWithUndefinedScheduler.set(state, false); + } + } + } } - // Note that the choices for the ~maybeStates are arbitrary as no states with rewards are reachable any way. } template diff --git a/src/transformer/EffectlessMECRemover.h b/src/transformer/EffectlessMECRemover.h new file mode 100644 index 000000000..60c79cb4e --- /dev/null +++ b/src/transformer/EffectlessMECRemover.h @@ -0,0 +1,211 @@ +#ifndef STORM_TRANSFORMER_EFFECTLESSMECREMOVER_H +#define STORM_TRANSFORMER_EFFECTLESSMECREMOVER_H + + +#include "src/utility/constants.h" +#include "src/utility/macros.h" +#include "src/utility/graph.h" +#include "src/utility/vector.h" +#include "src/storage/MaximalEndComponentDecomposition.h" + +namespace storm { + namespace transformer { + + template + class EffectlessMECRemover { + public: + + struct EffectlessMECRemoverReturnType { + // The resulting matrix + storm::storage::SparseMatrix matrix; + // The resulting vector + std::vector vector; + // Index mapping that gives for each row of the resulting matrix and vector the corresponding row in the original matrix and vector. + // For the rows that lead to the newly introduced sink state, some row of the original matrix that stays inside the EC is given. + // The selfloop of the newly introduced sink state has no entry, i.e., matrix.rowCount() == newToOldRowMapping.size() + 1. + std::vector newToOldRowMapping; + // Gives for each state (=rowGroup) of the original matrix and vector the corresponding state in the resulting matrix and vector. + // if the given state does not exist in the result, the returned value will be numeric_limits::max() + std::vector oldToNewStateMapping; + }; + + /* + * Identifies maximal effectless end components and replaces them by a single state. + * + * A choice is effectless, iff the given vector is zero at the corresponding row. + * An EC is effectless iff it only consideres effectless choices. + * For each such EC that is not contained by another effectles EC, we add a new state and redirect all incoming and outgoing + * transitions of the EC to (and from) this state. + * If allowChoiceToSink is true for at least one state in an effectless EC, a choice that leads to a sink state is added to the new state. + * States from which all reachable choices are effectless will be removed. + * + */ + static EffectlessMECRemoverReturnType transform(storm::storage::SparseMatrix const& originalMatrix, std::vector const& originalVector, storm::storage::BitVector const& allowChoiceToSink) { + STORM_LOG_DEBUG("Invoked EffectlessMECRemover on matrix with " << originalMatrix.getRowGroupCount() << " row groups."); + + storm::storage::BitVector keptStates = computeStatesFromWhichNonEffectlessChoiceIsReachable(originalMatrix, originalVector); + storm::storage::MaximalEndComponentDecomposition effectlessECs = computeEffectlessECs(originalMatrix, originalVector, keptStates); + + //further shrink the set of kept states by removing all states that are part of an effectless EC + for (auto const& ec : effectlessECs) { + for (auto const& stateActionsPair : ec) { + keptStates.set(stateActionsPair.first, false); + } + } + STORM_LOG_DEBUG("Found " << effectlessECs.size() << " effectless End Components. Keeping " << keptStates.getNumberOfSetBits() << " of " << keptStates.size() << " original states."); + + EffectlessMECRemoverReturnType result; + std::vector newRowGroupIndices; + result.oldToNewStateMapping = std::vector(originalMatrix.getRowGroupCount(), std::numeric_limits::max()); + storm::storage::BitVector rowsToSinkState(originalMatrix.getRowCount(), false); // will be resized as soon as rowCount of resulting matrix is known + + for(auto keptState : keptStates) { + result.oldToNewStateMapping[keptState] = newRowGroupIndices.size(); // i.e., the current number of processed states + newRowGroupIndices.push_back(result.newToOldRowMapping.size()); // i.e., the current number of processed rows + for(uint_fast64_t oldRow = originalMatrix.getRowGroupIndices()[keptState]; oldRow < originalMatrix.getRowGroupIndices()[keptState + 1]; ++oldRow) { + result.newToOldRowMapping.push_back(oldRow); + } + } + for (auto const& ec : effectlessECs) { + newRowGroupIndices.push_back(result.newToOldRowMapping.size()); + bool ecHasChoiceToSink = false; + for (auto const& stateActionsPair : ec) { + result.oldToNewStateMapping[stateActionsPair.first] = newRowGroupIndices.size()-1; + for(uint_fast64_t choice = 0; choice < originalMatrix.getRowGroupSize(stateActionsPair.first); ++choice) { + if(stateActionsPair.second.find(choice) == stateActionsPair.second.end()) { + result.newToOldRowMapping.push_back(originalMatrix.getRowGroupIndices()[stateActionsPair.first] + choice); + } + } + ecHasChoiceToSink |= allowChoiceToSink.get(stateActionsPair.first); + } + if(ecHasChoiceToSink) { + STORM_LOG_ASSERT(result.newToOldRowMapping.size() < originalMatrix.getRowCount(), "Didn't expect to see more rows in the reduced matrix than in the original one."); + rowsToSinkState.set(result.newToOldRowMapping.size(), true); + result.newToOldRowMapping.push_back(originalMatrix.getRowGroupIndices()[ec.begin()->first] + (*ec.begin()->second.begin())); + } + } + + newRowGroupIndices.push_back(result.newToOldRowMapping.size()); + newRowGroupIndices.push_back(result.newToOldRowMapping.size()+1); + rowsToSinkState.resize(result.newToOldRowMapping.size()); + + result.matrix = buildTransformedMatrix(originalMatrix, newRowGroupIndices, result.newToOldRowMapping, result.oldToNewStateMapping, rowsToSinkState); + result.vector = buildTransformedVector(originalVector, result.newToOldRowMapping); + + STORM_LOG_DEBUG("EffectlessMECRemover is done. Resulting matrix has " << result.matrix.getRowGroupCount() << " row groups."); + return result; + } + + private: + + static storm::storage::BitVector computeStatesFromWhichNonEffectlessChoiceIsReachable(storm::storage::SparseMatrix const& originalMatrix, std::vector const& originalVector) { + storm::storage::BitVector statesWithNonEffectlessChoice(originalMatrix.getRowGroupCount(), false); + for(uint_fast64_t rowGroup = 0; rowGroup < originalMatrix.getRowGroupCount(); ++rowGroup){ + for(uint_fast64_t row = originalMatrix.getRowGroupIndices()[rowGroup]; row < originalMatrix.getRowGroupIndices()[rowGroup+1]; ++row) { + if(!storm::utility::isZero(originalVector[row])) { + statesWithNonEffectlessChoice.set(rowGroup); + break; + } + } + } + storm::storage::BitVector trueVector(originalMatrix.getRowGroupCount(), true); + return storm::utility::graph::performProbGreater0E(originalMatrix, originalMatrix.getRowGroupIndices(), originalMatrix.transpose(true), trueVector, statesWithNonEffectlessChoice); + } + + static storm::storage::MaximalEndComponentDecomposition computeEffectlessECs(storm::storage::SparseMatrix const& originalMatrix, std::vector const& originalVector, storm::storage::BitVector const& keptStates) { + // Get an auxiliary matrix to identify the effectless end components. + // This is done by redirecting choices that can never be part of an effectless EC to a sink state. + // Such choices are either non-effectless choices or choices that lead to a state that is not in keptStates. + storm::storage::BitVector effectlessChoices = storm::utility::vector::filter(originalVector, [&] (ValueType const& value) -> bool {return storm::utility::isZero(value); } ); + uint_fast64_t sinkState = originalMatrix.getRowGroupCount(); + storm::storage::SparseMatrixBuilder builder(originalMatrix.getRowCount() + 1, originalMatrix.getColumnCount() + 1, originalMatrix.getEntryCount() + 1, false, true, originalMatrix.getRowGroupCount()+1); + uint_fast64_t row = 0; + for(uint_fast64_t rowGroup = 0; rowGroup < originalMatrix.getRowGroupCount(); ++rowGroup) { + builder.newRowGroup(row); + for (; row < originalMatrix.getRowGroupIndices()[rowGroup+1]; ++row ){ + bool keepRow = effectlessChoices.get(row); + if(keepRow) { //Also check whether all successors are kept + for(auto const& entry : originalMatrix.getRow(row)){ + keepRow &= keptStates.get(entry.getColumn()); + } + } + if(keepRow) { + for(auto const& entry : originalMatrix.getRow(row)){ + builder.addNextValue(row, entry.getColumn(), entry.getValue()); + } + } else { + builder.addNextValue(row, sinkState, storm::utility::one()); + } + } + } + builder.newRowGroup(row); + builder.addNextValue(row, sinkState, storm::utility::one()); + storm::storage::SparseMatrix auxiliaryMatrix = builder.build(); + storm::storage::SparseMatrix backwardsTransitions = auxiliaryMatrix.transpose(true); + storm::storage::BitVector sinkStateAsBitVector(auxiliaryMatrix.getRowGroupCount(), false); + sinkStateAsBitVector.set(sinkState); + storm::storage::BitVector subsystem = keptStates; + subsystem.resize(keptStates.size() + 1, true); + // The states for which sinkState is reachable under any scheduler can not be part of an EC + subsystem &= ~(storm::utility::graph::performProbGreater0A(auxiliaryMatrix, auxiliaryMatrix.getRowGroupIndices(), backwardsTransitions, subsystem, sinkStateAsBitVector)); + return storm::storage::MaximalEndComponentDecomposition(auxiliaryMatrix, backwardsTransitions, subsystem); + } + + static storm::storage::SparseMatrix buildTransformedMatrix(storm::storage::SparseMatrix const& originalMatrix, + std::vector const& newRowGroupIndices, + std::vector const& newToOldRowMapping, + std::vector const& oldToNewStateMapping, + storm::storage::BitVector const& rowsToSinkState) { + + uint_fast64_t numRowGroups = newRowGroupIndices.size()-1; + uint_fast64_t sinkState = numRowGroups-1; + storm::storage::SparseMatrixBuilder builder(newToOldRowMapping.size()+1, numRowGroups, 0, false, true, numRowGroups); + // Insert all matrix entries except the selfloop of the sink state + for(uint_fast64_t newRowGroup = 0; newRowGroup < numRowGroups-1; ++newRowGroup) { + uint_fast64_t newRow = newRowGroupIndices[newRowGroup]; + builder.newRowGroup(newRow); + for(; newRow < newRowGroupIndices[newRowGroup+1]; ++newRow) { + if(rowsToSinkState.get(newRow)) { + builder.addNextValue(newRow, sinkState, storm::utility::one()); + } else { + // Make sure that the entries for this row are inserted in the right order. + // Also, transitions to the same EC need to be merged. and transitions to states that are erased need to be ignored + std::map sortedEntries; + for(auto const& entry : originalMatrix.getRow(newToOldRowMapping[newRow])){ + uint_fast64_t newColumn = oldToNewStateMapping[entry.getColumn()]; + if(newColumn < numRowGroups) { + auto insertRes = sortedEntries.insert(std::make_pair(newColumn, entry.getValue())); + if(!insertRes.second) { + // We have already seen an entry with this column. ==> merge transitions + insertRes.first->second += entry.getValue(); + } + } + } + for(auto const& sortedEntry : sortedEntries) { + builder.addNextValue(newRow, sortedEntry.first, sortedEntry.second); + } + } + } + } + //Now add the selfloop at the sink state + builder.newRowGroup(newRowGroupIndices[sinkState]); + builder.addNextValue(newRowGroupIndices[sinkState], sinkState, storm::utility::one()); + + return builder.build(); + } + + static std::vector buildTransformedVector(std::vector const& originalVector, std::vector const& newToOldRowMapping) { + std::vector v; + v.reserve(newToOldRowMapping.size()+1); + for(auto const& oldRow : newToOldRowMapping) { + v.push_back(originalVector[oldRow]); + } + // add entry for the sink state + v.push_back(storm::utility::zero()); + return v; + } + + }; + } +} +#endif // STORM_TRANSFORMER_EFFECTLESSMECREMOVER_H