diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp index 46be193ee..f60295ad4 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.cpp @@ -8,7 +8,7 @@ #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h" #include "src/solver/MinMaxLinearEquationSolver.h" -#include "src/transformer/NeutralECRemover.h" +#include "src/transformer/EndComponentEliminator.h" #include "src/utility/graph.h" #include "src/utility/macros.h" #include "src/utility/vector.h" @@ -99,28 +99,31 @@ namespace storm { return; } // Remove end components in which no reward is earned - auto removerResult = storm::transformer::NeutralECRemover::transform(data.preprocessedModel.getTransitionMatrix(), weightedRewardVector, storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true)); - std::vector subResult(removerResult.matrix.getRowGroupCount()); + auto ecEliminatorResult = storm::transformer::EndComponentEliminator::transform(data.preprocessedModel.getTransitionMatrix(), storm::utility::vector::filterZero(weightedRewardVector), storm::storage::BitVector(data.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true)); + + std::vector subRewardVector(ecEliminatorResult.newToOldRowMapping.size()); + storm::utility::vector::selectVectorValues(subRewardVector, ecEliminatorResult.newToOldRowMapping, weightedRewardVector); + std::vector subResult(ecEliminatorResult.matrix.getRowGroupCount()); storm::solver::GeneralMinMaxLinearEquationSolverFactory solverFactory; - std::unique_ptr> solver = solverFactory.create(removerResult.matrix); + std::unique_ptr> solver = solverFactory.create(ecEliminatorResult.matrix); solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize); solver->setTrackScheduler(true); - solver->solveEquations(subResult, removerResult.vector); + solver->solveEquations(subResult, subRewardVector); this->weightedResult = std::vector(data.preprocessedModel.getNumberOfStates()); this->scheduler = storm::storage::TotalScheduler(data.preprocessedModel.getNumberOfStates()); std::unique_ptr solverScheduler = solver->getScheduler(); storm::storage::BitVector statesWithUndefinedScheduler(data.preprocessedModel.getNumberOfStates(), false); for(uint_fast64_t state = 0; state < data.preprocessedModel.getNumberOfStates(); ++state) { - uint_fast64_t stateInReducedModel = removerResult.oldToNewStateMapping[state]; + uint_fast64_t stateInReducedModel = ecEliminatorResult.oldToNewStateMapping[state]; // Check if the state exists in the reduced model - if(stateInReducedModel < removerResult.matrix.getRowGroupCount()) { + if(stateInReducedModel < ecEliminatorResult.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] + solverScheduler->getChoice(stateInReducedModel); - uint_fast64_t chosenRowInOriginalModel = removerResult.newToOldRowMapping[chosenRowInReducedModel]; + uint_fast64_t chosenRowInReducedModel = ecEliminatorResult.matrix.getRowGroupIndices()[stateInReducedModel] + solverScheduler->getChoice(stateInReducedModel); + uint_fast64_t chosenRowInOriginalModel = ecEliminatorResult.newToOldRowMapping[chosenRowInReducedModel]; if(chosenRowInOriginalModel >= data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state] && chosenRowInOriginalModel < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]) { this->scheduler.setChoice(state, chosenRowInOriginalModel - data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]); @@ -138,12 +141,12 @@ namespace storm { // 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 of the EC for which the scheduler is defined - uint_fast64_t stateInReducedModel = removerResult.oldToNewStateMapping[state]; + uint_fast64_t stateInReducedModel = ecEliminatorResult.oldToNewStateMapping[state]; for(uint_fast64_t row = data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state]; row < data.preprocessedModel.getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { bool rowStaysInEC = true; bool rowLeadsToDefinedScheduler = false; for(auto const& entry : data.preprocessedModel.getTransitionMatrix().getRow(row)) { - rowStaysInEC &= ( stateInReducedModel == removerResult.oldToNewStateMapping[entry.getColumn()]); + rowStaysInEC &= ( stateInReducedModel == ecEliminatorResult.oldToNewStateMapping[entry.getColumn()]); rowLeadsToDefinedScheduler |= !statesWithUndefinedScheduler.get(entry.getColumn()); } if(rowStaysInEC && rowLeadsToDefinedScheduler) { diff --git a/src/transformer/NeutralECRemover.h b/src/transformer/EndComponentEliminator.h similarity index 68% rename from src/transformer/NeutralECRemover.h rename to src/transformer/EndComponentEliminator.h index 26edc028a..d60dd9c2c 100644 --- a/src/transformer/NeutralECRemover.h +++ b/src/transformer/EndComponentEliminator.h @@ -1,59 +1,55 @@ -#ifndef STORM_TRANSFORMER_NEUTRALECREMOVER_H -#define STORM_TRANSFORMER_NEUTRALECREMOVER_H +#ifndef STORM_TRANSFORMER_ENDCOMPONENTELIMINATOR_H +#define STORM_TRANSFORMER_ENDCOMPONENTELIMINATOR_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 NeutralECRemover { + class EndComponentEliminator { public: - struct NeutralECRemoverReturnType { + struct EndComponentEliminatorReturnType { // 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. + // Index mapping that gives for each row of the resulting matrix the corresponding row in the original matrix. // For the empty rows added to EC states, some row of the original matrix that stays inside the EC is given. 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 std::numeric_limits::max(), i.e., an invalid index. + // Gives for each state (=rowGroup) of the original matrix the corresponding state in the resulting matrix. + // States of a removed end component are mapped to the state that substitutes the EC. + // If the given state does not exist in the result (e.g. it belonged to a bottom EC), the returned value will be std::numeric_limits::max(), i.e., an invalid index. std::vector oldToNewStateMapping; }; /* - * Identifies neutral end components and replaces them by a single state. + * Identifies end components and substitutes them by a single state. * - * A choice is neutral, iff the given vector is zero at the corresponding row. - * An EC is neutral iff it only consideres neutral choices. - * For each such EC that is not contained by another neutral EC, we add a new state and redirect all incoming and outgoing + * Only ECs for which the given bit vector is true for all choices are considered. + * For each such EC (that is not contained by another EC), we add a new state and redirect all incoming and outgoing * transitions of the EC to (and from) this state. - * If allowEmptyRow is true for at least one state in a neutral EC, an empty row is added to the new state (representing the choice to stay at the neutral EC forever). - * States from which all reachable choices are neutral will be removed. - * + * If allowEmptyRow is true for at least one state of an EC, an empty row is added to the new state (representing the choice to stay at the EC forever). + * States for which all reachable choices are selected by the given bit vector will be removed! */ - static NeutralECRemoverReturnType transform(storm::storage::SparseMatrix const& originalMatrix, std::vector const& originalVector, storm::storage::BitVector const& allowEmptyRow) { - STORM_LOG_DEBUG("Invoked NeutralECRemover on matrix with " << originalMatrix.getRowGroupCount() << " row groups."); + static EndComponentEliminatorReturnType transform(storm::storage::SparseMatrix const& originalMatrix, storm::storage::BitVector const& consideredRows, storm::storage::BitVector const& allowEmptyRow) { + STORM_LOG_DEBUG("Invoked EndComponentEliminator on matrix with " << originalMatrix.getRowGroupCount() << " row groups."); - storm::storage::BitVector keptStates = computeStatesFromWhichNonNeutralChoiceIsReachable(originalMatrix, originalVector); - storm::storage::MaximalEndComponentDecomposition neutralECs = computeNeutralECs(originalMatrix, originalVector, keptStates); + storm::storage::BitVector keptStates = computeStatesFromWhichNonConsideredRowIsReachable(originalMatrix, consideredRows); + storm::storage::MaximalEndComponentDecomposition ecs = computeECs(originalMatrix, consideredRows, keptStates); - //further shrink the set of kept states by removing all states that are part of a neutral EC - for (auto const& ec : neutralECs) { + //further shrink the set of kept states by removing all states that are part of an EC + for (auto const& ec : ecs) { for (auto const& stateActionsPair : ec) { keptStates.set(stateActionsPair.first, false); } } - STORM_LOG_DEBUG("Found " << neutralECs.size() << " neutral End Components. Keeping " << keptStates.getNumberOfSetBits() << " of " << keptStates.size() << " original states."); + STORM_LOG_DEBUG("Found " << ecs.size() << " end components to eliminate. Keeping " << keptStates.getNumberOfSetBits() << " of " << keptStates.size() << " original states."); - NeutralECRemoverReturnType result; + EndComponentEliminatorReturnType result; std::vector newRowGroupIndices; result.oldToNewStateMapping = std::vector(originalMatrix.getRowGroupCount(), std::numeric_limits::max()); storm::storage::BitVector emptyRows(originalMatrix.getRowCount(), false); // will be resized as soon as the rowCount of the resulting matrix is known @@ -65,7 +61,7 @@ namespace storm { result.newToOldRowMapping.push_back(oldRow); } } - for (auto const& ec : neutralECs) { + for (auto const& ec : ecs) { newRowGroupIndices.push_back(result.newToOldRowMapping.size()); bool ecGetsEmptyRow = false; for (auto const& stateActionsPair : ec) { @@ -87,40 +83,34 @@ namespace storm { emptyRows.resize(result.newToOldRowMapping.size()); result.matrix = buildTransformedMatrix(originalMatrix, newRowGroupIndices, result.newToOldRowMapping, result.oldToNewStateMapping, emptyRows); - result.vector = buildTransformedVector(originalVector, result.newToOldRowMapping); - - STORM_LOG_DEBUG("NeutralECRemover is done. Resulting matrix has " << result.matrix.getRowGroupCount() << " row groups."); + STORM_LOG_DEBUG("EndComponentEliminator is done. Resulting matrix has " << result.matrix.getRowGroupCount() << " row groups."); return result; } private: - static storm::storage::BitVector computeStatesFromWhichNonNeutralChoiceIsReachable(storm::storage::SparseMatrix const& originalMatrix, std::vector const& originalVector) { - storm::storage::BitVector statesWithNonNeutralChoice(originalMatrix.getRowGroupCount(), false); + static storm::storage::BitVector computeStatesFromWhichNonConsideredRowIsReachable(storm::storage::SparseMatrix const& originalMatrix, storm::storage::BitVector const& consideredRows) { + storm::storage::BitVector nonConsideredRows = ~consideredRows; + storm::storage::BitVector groupsWithNonConsideredRow(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])) { - statesWithNonNeutralChoice.set(rowGroup); - break; - } + if(nonConsideredRows.getNextSetIndex(originalMatrix.getRowGroupIndices()[rowGroup]) < originalMatrix.getRowGroupIndices()[rowGroup+1]) { + groupsWithNonConsideredRow.set(rowGroup); } } - storm::storage::BitVector trueVector(originalMatrix.getRowGroupCount(), true); - return storm::utility::graph::performProbGreater0E(originalMatrix, originalMatrix.getRowGroupIndices(), originalMatrix.transpose(true), trueVector, statesWithNonNeutralChoice); + return storm::utility::graph::performProbGreater0E(originalMatrix, originalMatrix.getRowGroupIndices(), originalMatrix.transpose(true), storm::storage::BitVector(originalMatrix.getRowGroupCount(), true), groupsWithNonConsideredRow); } - static storm::storage::MaximalEndComponentDecomposition computeNeutralECs(storm::storage::SparseMatrix const& originalMatrix, std::vector const& originalVector, storm::storage::BitVector const& keptStates) { - // Get an auxiliary matrix to identify the neutral end components. - // This is done by redirecting choices that can never be part of a neutral EC to a sink state. - // Such choices are either non-neutral choices or choices that lead to a state that is not in keptStates. - storm::storage::BitVector neutralChoices = storm::utility::vector::filter(originalVector, [&] (ValueType const& value) -> bool {return storm::utility::isZero(value); } ); + static storm::storage::MaximalEndComponentDecomposition computeECs(storm::storage::SparseMatrix const& originalMatrix, storm::storage::BitVector const& consideredRows, storm::storage::BitVector const& keptStates) { + // Get an auxiliary matrix to identify the correct end components w.r.t. the considered choices and the kept states. + // This is done by redirecting choices that can never be part of an EC to a sink state. + // Such choices are either non-considered choices or choices that lead to a state that is not in keptStates. 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 = neutralChoices.get(row); + bool keepRow = consideredRows.get(row); if(keepRow) { //Also check whether all successors are kept for(auto const& entry : originalMatrix.getRow(row)){ keepRow &= keptStates.get(entry.getColumn()); @@ -182,17 +172,7 @@ namespace storm { } return builder.build(newToOldRowMapping.size(), numRowGroups, numRowGroups); } - - static std::vector buildTransformedVector(std::vector const& originalVector, std::vector const& newToOldRowMapping) { - std::vector v; - v.reserve(newToOldRowMapping.size()); - for(auto const& oldRow : newToOldRowMapping) { - v.push_back(originalVector[oldRow]); - } - return v; - } - }; } } -#endif // STORM_TRANSFORMER_NEUTRALECREMOVER_H +#endif // STORM_TRANSFORMER_ENDCOMPONENTREMOVER_H diff --git a/src/utility/vector.h b/src/utility/vector.h index d5c796e84..cb6187579 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -94,7 +94,21 @@ namespace storm { vector[oldPosition++] = values[position]; } } - + + /*! + * Selects the elements from a vector at the specified positions and writes them consecutively into another vector. + * @param vector The vector into which the selected elements are to be written. + * @param positions The positions at which to select the elements from the values vector. + * @param values The vector from which to select the elements. + */ + template + void selectVectorValues(std::vector& vector, std::vector const& positions, std::vector const& values) { + uint_fast64_t oldPosition = 0; + for (auto position : positions) { + vector[oldPosition++] = values[position]; + } + } + /*! * Selects groups of elements from a vector at the specified positions and writes them consecutively into another vector. * @@ -413,8 +427,7 @@ namespace storm { */ template storm::storage::BitVector filterZero(std::vector const& values) { - std::function fnc = [] (T const& value) -> bool { return storm::utility::isZero(value); }; - return filter(values, fnc); + return filter(values, storm::utility::isZero); } /** diff --git a/test/functional/transformer/NeutralECRemoverTest.cpp b/test/functional/transformer/EndComponentEliminatorTest.cpp similarity index 89% rename from test/functional/transformer/NeutralECRemoverTest.cpp rename to test/functional/transformer/EndComponentEliminatorTest.cpp index 0557419c8..a4ce99a39 100644 --- a/test/functional/transformer/NeutralECRemoverTest.cpp +++ b/test/functional/transformer/EndComponentEliminatorTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" -#include "src/transformer/NeutralECRemover.h" +#include "src/transformer/EndComponentEliminator.h" TEST(NeutralECRemover, SimpleModelTest) { @@ -34,13 +34,18 @@ TEST(NeutralECRemover, SimpleModelTest) { storm::storage::SparseMatrix matrix; ASSERT_NO_THROW(matrix = builder.build()); - std::vector vector = {0.0, 0.0, 0.0, -12.0, 0.0, 0.0, 42.0, 1.0, 2.7, 0.0, 0.0, -1.0}; + storm::storage::BitVector consideredRows(12, true); + consideredRows.set(3, false); + consideredRows.set(6, false); + consideredRows.set(7, false); + consideredRows.set(8, false); + consideredRows.set(11, false); storm::storage::BitVector allowEmptyRows(5, true); allowEmptyRows.set(1, false); allowEmptyRows.set(4, false); - auto res = storm::transformer::NeutralECRemover::transform(matrix, vector, allowEmptyRows); + auto res = storm::transformer::EndComponentEliminator::transform(matrix, consideredRows, allowEmptyRows); // Expected data storm::storage::SparseMatrixBuilder expectedBuilder(8, 3, 8, true, true, 3); @@ -58,8 +63,6 @@ TEST(NeutralECRemover, SimpleModelTest) { storm::storage::SparseMatrix expectedMatrix; ASSERT_NO_THROW(expectedMatrix = expectedBuilder.build()); - std::vector expectedVector = {42.0, 1.0, 2.7, 0.0, 0.0, -1.0, 0.0, -12.0}; - std::vector expectedNewToOldRowMapping = {6,7,8,1,0,11,2,3}; std::vector expectedOldToNewStateMapping = {1,2,std::numeric_limits::max(), 0, 2}; @@ -68,7 +71,6 @@ TEST(NeutralECRemover, SimpleModelTest) { // In particular, the ordering within the row groups depends on the MEC decomposition implementation. // However, this is not checked here... EXPECT_EQ(expectedMatrix, res.matrix); - EXPECT_EQ(expectedVector, res.vector); EXPECT_EQ(expectedNewToOldRowMapping, res.newToOldRowMapping); EXPECT_EQ(expectedOldToNewStateMapping, res.oldToNewStateMapping); //std::cout << "Original matrix:" << std::endl << matrix << std::endl << std::endl << "Computation Result: " << std::endl << res.matrix << std::endl<< std::endl << "expected Matrix" << std::endl<< expectedMatrix << std::endl;