From da65ef3aa93fb3ff60e15c841e795397303ad76b Mon Sep 17 00:00:00 2001 From: TimQu Date: Sat, 11 Jun 2016 11:47:47 +0200 Subject: [PATCH] Renamed Effectless -> Neutral. Also removed additional (useless) sink state Former-commit-id: 64bb2ec9310742a9d5d11d07aa633e1f656ecf90 --- ...seWeightedObjectivesModelCheckerHelper.cpp | 4 +- ...ectlessMECRemover.h => NeutralECRemover.h} | 119 ++++++++---------- 2 files changed, 55 insertions(+), 68 deletions(-) rename src/transformer/{EffectlessMECRemover.h => NeutralECRemover.h} (64%) diff --git a/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp b/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp index 9d0b969ce..5f97dbdba 100644 --- a/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp @@ -5,7 +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/transformer/NeutralECRemover.h" #include "src/utility/graph.h" #include "src/utility/macros.h" #include "src/utility/solver.h" @@ -72,7 +72,7 @@ namespace storm { //std::cout << "weighted reward vector is " << storm::utility::vector::toString(weightedRewardVector) << std::endl; // 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)); + auto removerResult = storm::transformer::NeutralECRemover::transform(info.preprocessedModel.getTransitionMatrix(), weightedRewardVector, storm::storage::BitVector(info.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true)); std::vector subResult(removerResult.matrix.getRowGroupCount()); diff --git a/src/transformer/EffectlessMECRemover.h b/src/transformer/NeutralECRemover.h similarity index 64% rename from src/transformer/EffectlessMECRemover.h rename to src/transformer/NeutralECRemover.h index 60c79cb4e..a79eca0d6 100644 --- a/src/transformer/EffectlessMECRemover.h +++ b/src/transformer/NeutralECRemover.h @@ -1,5 +1,5 @@ -#ifndef STORM_TRANSFORMER_EFFECTLESSMECREMOVER_H -#define STORM_TRANSFORMER_EFFECTLESSMECREMOVER_H +#ifndef STORM_TRANSFORMER_NEUTRALECREMOVER_H +#define STORM_TRANSFORMER_NEUTRALECREMOVER_H #include "src/utility/constants.h" @@ -12,52 +12,51 @@ namespace storm { namespace transformer { template - class EffectlessMECRemover { + class NeutralECRemover { public: - struct EffectlessMECRemoverReturnType { + struct NeutralECRemoverReturnType { // 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. + // 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 numeric_limits::max() + // if the given state does not exist in the result, the returned value will be std::numeric_limits::max(), i.e., an invalid index. std::vector oldToNewStateMapping; }; /* - * Identifies maximal effectless end components and replaces them by a single state. + * Identifies neutral 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 + * 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 * 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. + * 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. * */ - 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."); + 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."); - storm::storage::BitVector keptStates = computeStatesFromWhichNonEffectlessChoiceIsReachable(originalMatrix, originalVector); - storm::storage::MaximalEndComponentDecomposition effectlessECs = computeEffectlessECs(originalMatrix, originalVector, keptStates); + storm::storage::BitVector keptStates = computeStatesFromWhichNonNeutralChoiceIsReachable(originalMatrix, originalVector); + storm::storage::MaximalEndComponentDecomposition neutralECs = computeNeutralECs(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) { + //further shrink the set of kept states by removing all states that are part of a neutral EC + for (auto const& ec : neutralECs) { 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."); + STORM_LOG_DEBUG("Found " << neutralECs.size() << " neutral End Components. Keeping " << keptStates.getNumberOfSetBits() << " of " << keptStates.size() << " original states."); - EffectlessMECRemoverReturnType result; + NeutralECRemoverReturnType 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 + storm::storage::BitVector emptyRows(originalMatrix.getRowCount(), false); // will be resized as soon as the rowCount of the resulting matrix is known for(auto keptState : keptStates) { result.oldToNewStateMapping[keptState] = newRowGroupIndices.size(); // i.e., the current number of processed states @@ -66,9 +65,9 @@ namespace storm { result.newToOldRowMapping.push_back(oldRow); } } - for (auto const& ec : effectlessECs) { + for (auto const& ec : neutralECs) { newRowGroupIndices.push_back(result.newToOldRowMapping.size()); - bool ecHasChoiceToSink = false; + bool ecGetsEmptyRow = 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) { @@ -76,54 +75,52 @@ namespace storm { result.newToOldRowMapping.push_back(originalMatrix.getRowGroupIndices()[stateActionsPair.first] + choice); } } - ecHasChoiceToSink |= allowChoiceToSink.get(stateActionsPair.first); + ecGetsEmptyRow |= allowEmptyRow.get(stateActionsPair.first); } - if(ecHasChoiceToSink) { + if(ecGetsEmptyRow) { 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); + emptyRows.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()); + emptyRows.resize(result.newToOldRowMapping.size()); - result.matrix = buildTransformedMatrix(originalMatrix, newRowGroupIndices, result.newToOldRowMapping, result.oldToNewStateMapping, rowsToSinkState); + result.matrix = buildTransformedMatrix(originalMatrix, newRowGroupIndices, result.newToOldRowMapping, result.oldToNewStateMapping, emptyRows); result.vector = buildTransformedVector(originalVector, result.newToOldRowMapping); - - STORM_LOG_DEBUG("EffectlessMECRemover is done. Resulting matrix has " << result.matrix.getRowGroupCount() << " row groups."); + + STORM_LOG_DEBUG("NeutralECRemover is done. Resulting matrix has " << result.matrix.getRowGroupCount() << " row groups. Resulting Matrix: " << std::endl << result.matrix << std::endl << " resulting vector: " << result.vector ); return result; } private: - static storm::storage::BitVector computeStatesFromWhichNonEffectlessChoiceIsReachable(storm::storage::SparseMatrix const& originalMatrix, std::vector const& originalVector) { - storm::storage::BitVector statesWithNonEffectlessChoice(originalMatrix.getRowGroupCount(), false); + static storm::storage::BitVector computeStatesFromWhichNonNeutralChoiceIsReachable(storm::storage::SparseMatrix const& originalMatrix, std::vector const& originalVector) { + storm::storage::BitVector statesWithNonNeutralChoice(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); + statesWithNonNeutralChoice.set(rowGroup); break; } } } storm::storage::BitVector trueVector(originalMatrix.getRowGroupCount(), true); - return storm::utility::graph::performProbGreater0E(originalMatrix, originalMatrix.getRowGroupIndices(), originalMatrix.transpose(true), trueVector, statesWithNonEffectlessChoice); + return storm::utility::graph::performProbGreater0E(originalMatrix, originalMatrix.getRowGroupIndices(), originalMatrix.transpose(true), trueVector, statesWithNonNeutralChoice); } - 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); } ); + 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); } ); 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); + bool keepRow = neutralChoices.get(row); if(keepRow) { //Also check whether all successors are kept for(auto const& entry : originalMatrix.getRow(row)){ keepRow &= keptStates.get(entry.getColumn()); @@ -140,7 +137,7 @@ namespace storm { } builder.newRowGroup(row); builder.addNextValue(row, sinkState, storm::utility::one()); - storm::storage::SparseMatrix auxiliaryMatrix = builder.build(); + storm::storage::SparseMatrix auxiliaryMatrix = builder.build(originalMatrix.getRowCount() + 1, originalMatrix.getColumnCount()+1, originalMatrix.getRowGroupCount() +1); storm::storage::SparseMatrix backwardsTransitions = auxiliaryMatrix.transpose(true); storm::storage::BitVector sinkStateAsBitVector(auxiliaryMatrix.getRowGroupCount(), false); sinkStateAsBitVector.set(sinkState); @@ -155,29 +152,25 @@ namespace storm { std::vector const& newRowGroupIndices, std::vector const& newToOldRowMapping, std::vector const& oldToNewStateMapping, - storm::storage::BitVector const& rowsToSinkState) { + storm::storage::BitVector const& emptyRows) { 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]; + uint_fast64_t newRow = 0; + storm::storage::SparseMatrixBuilder builder(newToOldRowMapping.size(), numRowGroups, originalMatrix.getEntryCount(), false, true, numRowGroups); + for(uint_fast64_t newRowGroup = 0; newRowGroup < numRowGroups; ++newRowGroup) { builder.newRowGroup(newRow); for(; newRow < newRowGroupIndices[newRowGroup+1]; ++newRow) { - if(rowsToSinkState.get(newRow)) { - builder.addNextValue(newRow, sinkState, storm::utility::one()); - } else { + if(!emptyRows.get(newRow)) { // 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 + // 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) { + auto insertResult = sortedEntries.insert(std::make_pair(newColumn, entry.getValue())); + if(!insertResult.second) { // We have already seen an entry with this column. ==> merge transitions - insertRes.first->second += entry.getValue(); + insertResult.first->second += entry.getValue(); } } } @@ -187,25 +180,19 @@ namespace storm { } } } - //Now add the selfloop at the sink state - builder.newRowGroup(newRowGroupIndices[sinkState]); - builder.addNextValue(newRowGroupIndices[sinkState], sinkState, storm::utility::one()); - - return builder.build(); + 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()+1); + v.reserve(newToOldRowMapping.size()); 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 +#endif // STORM_TRANSFORMER_NEUTRALECREMOVER_H