sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Renamed Effectless -> Neutral. Also removed additional (useless) sink state 

Former-commit-id: 64bb2ec931
main
TimQu 9 years ago
parent
c401de1fb9
commit
da65ef3aa9
2 changed files with 55 additions and 68 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp
  2. 119
      src/transformer/NeutralECRemover.h

4
src/modelchecker/multiobjective/helper/SparseWeightedObjectivesModelCheckerHelper.cpp
View File

@ -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<ValueType>::transform(info.preprocessedModel.getTransitionMatrix(), weightedRewardVector, storm::storage::BitVector(info.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true));
auto removerResult = storm::transformer::NeutralECRemover<ValueType>::transform(info.preprocessedModel.getTransitionMatrix(), weightedRewardVector, storm::storage::BitVector(info.preprocessedModel.getTransitionMatrix().getRowGroupCount(), true));
std::vector<ValueType> subResult(removerResult.matrix.getRowGroupCount());

119
src/transformer/EffectlessMECRemover.h → src/transformer/NeutralECRemover.h
View File

@ -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 <typename ValueType>
class EffectlessMECRemover {
class NeutralECRemover {
public:
struct EffectlessMECRemoverReturnType {
struct NeutralECRemoverReturnType {
// The resulting matrix
storm::storage::SparseMatrix<ValueType> matrix;
// The resulting vector
std::vector<ValueType> 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<uint_fast64_t> 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<uint_fast64_t>::max()
// if the given state does not exist in the result, the returned value will be std::numeric_limits<uint_fast64_t>::max(), i.e., an invalid index.
std::vector<uint_fast64_t> 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<ValueType> const& originalMatrix, std::vector<ValueType> 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<ValueType> const& originalMatrix, std::vector<ValueType> 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<ValueType> effectlessECs = computeEffectlessECs(originalMatrix, originalVector, keptStates);
storm::storage::BitVector keptStates = computeStatesFromWhichNonNeutralChoiceIsReachable(originalMatrix, originalVector);
storm::storage::MaximalEndComponentDecomposition<ValueType> 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<uint_fast64_t> newRowGroupIndices;
result.oldToNewStateMapping = std::vector<uint_fast64_t>(originalMatrix.getRowGroupCount(), std::numeric_limits<uint_fast64_t>::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<ValueType> const& originalMatrix, std::vector<ValueType> const& originalVector) {
storm::storage::BitVector statesWithNonEffectlessChoice(originalMatrix.getRowGroupCount(), false);
static storm::storage::BitVector computeStatesFromWhichNonNeutralChoiceIsReachable(storm::storage::SparseMatrix<ValueType> const& originalMatrix, std::vector<ValueType> 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<ValueType> computeEffectlessECs(storm::storage::SparseMatrix<ValueType> const& originalMatrix, std::vector<ValueType> 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<ValueType>(originalVector, [&] (ValueType const& value) -> bool {return storm::utility::isZero(value); } );
static storm::storage::MaximalEndComponentDecomposition<ValueType> computeNeutralECs(storm::storage::SparseMatrix<ValueType> const& originalMatrix, std::vector<ValueType> 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<ValueType>(originalVector, [&] (ValueType const& value) -> bool {return storm::utility::isZero(value); } );
uint_fast64_t sinkState = originalMatrix.getRowGroupCount();
storm::storage::SparseMatrixBuilder<ValueType> 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<ValueType>());
storm::storage::SparseMatrix<ValueType> auxiliaryMatrix = builder.build();
storm::storage::SparseMatrix<ValueType> auxiliaryMatrix = builder.build(originalMatrix.getRowCount() + 1, originalMatrix.getColumnCount()+1, originalMatrix.getRowGroupCount() +1);
storm::storage::SparseMatrix<ValueType> backwardsTransitions = auxiliaryMatrix.transpose(true);
storm::storage::BitVector sinkStateAsBitVector(auxiliaryMatrix.getRowGroupCount(), false);
sinkStateAsBitVector.set(sinkState);
@ -155,29 +152,25 @@ namespace storm {
std::vector<uint_fast64_t> const& newRowGroupIndices,
std::vector<uint_fast64_t> const& newToOldRowMapping,
std::vector<uint_fast64_t> 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<ValueType> 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<ValueType> 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<ValueType>());
} 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<uint_fast64_t, ValueType> 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<ValueType>());
return builder.build();
return builder.build(newToOldRowMapping.size(), numRowGroups, numRowGroups);
}
static std::vector<ValueType> buildTransformedVector(std::vector<ValueType> const& originalVector, std::vector<uint_fast64_t> const& newToOldRowMapping) {
std::vector<ValueType> 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<ValueType>());
return v;
}
};
}
}
#endif // STORM_TRANSFORMER_EFFECTLESSMECREMOVER_H
#endif // STORM_TRANSFORMER_NEUTRALECREMOVER_H
Write Preview
Loading…
Cancel
Save