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

Extended Functionality of goal state merger

main
TimQu 8 years ago
parent
dd647e93d2
commit
48957978eb
4 changed files with 283 additions and 139 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. 258
      src/storm/transformer/GoalStateMerger.cpp
  2. 40
      src/storm/transformer/GoalStateMerger.h
  3. 51
      src/storm/transformer/SparseParametricDtmcSimplifier.cpp
  4. 51
      src/storm/transformer/SparseParametricMdpSimplifier.cpp

258
src/storm/transformer/GoalStateMerger.cpp
View File

@ -2,15 +2,18 @@
#include <limits>
#include <memory>
#include <storm/exceptions/UnexpectedException.h>
#include "storm/utility/constants.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/MarkovAutomaton.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "storm/exceptions/UnexpectedException.h"
namespace storm {
@ -22,163 +25,246 @@ namespace storm {
}
template <typename SparseModelType>
std::shared_ptr<SparseModelType> GoalStateMerger<SparseModelType>::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector& targetStates, storm::storage::BitVector& sinkStates, std::vector<std::string> const& selectedRewardModels) {
typename GoalStateMerger<SparseModelType>::ReturnType GoalStateMerger<SparseModelType>::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels) const {
STORM_LOG_THROW(maybeStates.isDisjointFrom(targetStates) && targetStates.isDisjointFrom(sinkStates) && sinkStates.isDisjointFrom(maybeStates), storm::exceptions::InvalidArgumentException, "maybestates, targetstates, and sinkstates are assumed to be disjoint when creating the submodel. However, this is not the case.");
boost::optional<uint_fast64_t> targetState, sinkState;
auto builder = initializeTransitionMatrixBuilder(maybeStates, targetStates, sinkStates, targetState, sinkState);
auto transitionMatrix = buildTransitionMatrix(maybeStates, targetStates, sinkStates, targetState, sinkState, builder);
auto result = initialize(maybeStates, targetStates, sinkStates);
uint_fast64_t resNumStates = transitionMatrix.getRowGroupCount();
auto transitionMatrix = buildTransitionMatrix(maybeStates, targetStates, sinkStates, result.first, result.second);
auto labeling = buildStateLabeling(maybeStates, targetStates, sinkStates, result.first);
auto rewardModels = buildRewardModels(maybeStates, result.first, selectedRewardModels);
// Get the labeling for the initial states
storm::storage::BitVector initialStates = originalModel.getInitialStates() % maybeStates;
initialStates.resize(resNumStates, false);
if(!originalModel.getInitialStates().isDisjointFrom(targetStates)) {
initialStates.set(*targetState, true);
}
if(!originalModel.getInitialStates().isDisjointFrom(sinkStates)) {
initialStates.set(*sinkState, true);
}
storm::models::sparse::StateLabeling labeling(resNumStates);
labeling.addLabel("init", std::move(initialStates));
result.first.model = buildOutputModel(maybeStates, result.first, std::move(transitionMatrix), std::move(labeling), std::move(rewardModels));
// Get the reward models
std::unordered_map<std::string, typename SparseModelType::RewardModelType> rewardModels;
for (auto rewardModelName : selectedRewardModels) {
auto origTotalRewards = originalModel.getRewardModel(rewardModelName).getTotalRewardVector(originalModel.getTransitionMatrix());
auto transitionsOfMaybeStates = originalModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates);
auto resTotalRewards = storm::utility::vector::filterVector(origTotalRewards, transitionsOfMaybeStates);
resTotalRewards.resize(transitionMatrix.getRowCount(), storm::utility::zero<typename SparseModelType::RewardModelType::ValueType>());
rewardModels.insert(std::make_pair(rewardModelName, typename SparseModelType::RewardModelType(boost::none, resTotalRewards)));
}
// modify the given target and sink states
targetStates = storm::storage::BitVector(resNumStates, false);
if(targetState) {
targetStates.set(*targetState, true);
}
sinkStates = storm::storage::BitVector(resNumStates, false);
if(sinkState) {
sinkStates.set(*sinkState, true);
}
// Return the result
return std::make_shared<SparseModelType>(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels));
return result.first;
}
template <typename SparseModelType>
storm::storage::SparseMatrixBuilder<typename SparseModelType::ValueType> GoalStateMerger<SparseModelType>::initializeTransitionMatrixBuilder(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional<uint_fast64_t>& newTargetState, boost::optional<uint_fast64_t>& newSinkState) {
std::pair<typename GoalStateMerger<SparseModelType>::ReturnType, uint_fast64_t> GoalStateMerger<SparseModelType>::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const {
storm::storage::SparseMatrix<typename SparseModelType::ValueType> const& origMatrix = originalModel.getTransitionMatrix();
// Get the number of rows, cols and entries that the resulting transition matrix will have.
uint_fast64_t resNumStates(maybeStates.getNumberOfSetBits()), resNumActions(0), resNumTransitions(0);
ReturnType result;
result.keptChoices = storm::storage::BitVector(origMatrix.getRowCount(), false);
result.oldToNewStateIndexMapping = std::vector<uint_fast64_t>(maybeStates.size(), std::numeric_limits<uint_fast64_t>::max()); // init with some invalid state
uint_fast64_t transitionCount(0), stateCount(0);
bool targetStateRequired = !originalModel.getInitialStates().isDisjointFrom(targetStates);
bool sinkStateRequired = !originalModel.getInitialStates().isDisjointFrom(sinkStates);
for( auto state : maybeStates) {
resNumActions += origMatrix.getRowGroupSize(state);
result.oldToNewStateIndexMapping[state] = stateCount;
auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state+1];
bool stateIsDeadlock = true;
for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) {
bool hasTransitionToTarget(false), hasTransitionToSink(false);
uint_fast64_t transitionsToMaybeStates = 0;
bool keepThisRow(true), hasTransitionToTarget(false), hasTransitionToSink(false);
for (auto const& entry : origMatrix.getRow(row)) {
if (maybeStates.get(entry.getColumn())) {
++resNumTransitions;
++transitionsToMaybeStates;
} else if (targetStates.get(entry.getColumn())) {
hasTransitionToTarget = true;
} else if (sinkStates.get(entry.getColumn())) {
hasTransitionToSink = true;
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "There is a transition originating from a maybestate that does not lead to a maybe-, target-, or sinkstate.");
keepThisRow = false;
break;
}
}
if (keepThisRow) {
stateIsDeadlock = false;
result.keptChoices.set(row, true);
transitionCount += transitionsToMaybeStates;
if(hasTransitionToTarget) {
++resNumTransitions;
++transitionCount;
targetStateRequired = true;
}
if(hasTransitionToSink) {
++resNumTransitions;
++transitionCount;
sinkStateRequired = true;
}
}
STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!");
}
++stateCount;
}
// Get the index of the target/ sink state in the resulting model (if these states will exist)
// Treat the target and sink states (if these states will exist)
if(targetStateRequired) {
newTargetState = resNumStates;
++resNumStates;
++resNumActions;
++resNumTransitions;
result.targetState = stateCount;
++stateCount;
++transitionCount;
storm::utility::vector::setVectorValues(result.oldToNewStateIndexMapping, targetStates, *result.targetState);
}
if(sinkStateRequired) {
newSinkState = resNumStates;
++resNumStates;
++resNumActions;
++resNumTransitions;
result.sinkState = stateCount;
++stateCount;
++transitionCount;
storm::utility::vector::setVectorValues(result.oldToNewStateIndexMapping, sinkStates, *result.sinkState);
}
return storm::storage::SparseMatrixBuilder<typename SparseModelType::ValueType>(resNumActions, resNumStates, resNumTransitions, true, true, resNumStates);
return std::make_pair(std::move(result), std::move(transitionCount));
}
template <typename SparseModelType>
storm::storage::SparseMatrix<typename SparseModelType::ValueType> GoalStateMerger<SparseModelType>::buildTransitionMatrix(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional<uint_fast64_t> const& newTargetState, boost::optional<uint_fast64_t>const& newSinkState, storm::storage::SparseMatrixBuilder<typename SparseModelType::ValueType>& builder) {
// Get a Mapping that yields for each column in the old matrix the corresponding column in the new matrix
std::vector<uint_fast64_t> oldToNewIndexMap(maybeStates.size(), std::numeric_limits<uint_fast64_t>::max()); // init with some invalid state
uint_fast64_t newStateIndex = 0;
for (auto maybeState : maybeStates) {
oldToNewIndexMap[maybeState] = newStateIndex;
++newStateIndex;
}
storm::storage::SparseMatrix<typename SparseModelType::ValueType> GoalStateMerger<SparseModelType>::buildTransitionMatrix(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, uint_fast64_t transitionCount) const {
// Build the transition matrix
storm::storage::SparseMatrix<typename SparseModelType::ValueType> const& origMatrix = originalModel.getTransitionMatrix();
uint_fast64_t rowCount = resultData.keptChoices.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0);
uint_fast64_t maybeStateCount = maybeStates.getNumberOfSetBits();
uint_fast64_t stateCount = maybeStateCount + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0);
storm::storage::SparseMatrixBuilder<typename SparseModelType::ValueType> builder(rowCount, stateCount, transitionCount, true, origMatrix.hasTrivialRowGrouping(), origMatrix.hasTrivialRowGrouping() ? 0 : stateCount);
uint_fast64_t currRow = 0;
for (auto state : maybeStates) {
if (!origMatrix.hasTrivialRowGrouping()) {
builder.newRowGroup(currRow);
}
auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state + 1];
for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) {
boost::optional<typename SparseModelType::ValueType> targetProbability, sinkProbability;
for (uint_fast64_t row = resultData.keptChoices.getNextSetIndex(origMatrix.getRowGroupIndices()[state]); row < endOfRowGroup; row = resultData.keptChoices.getNextSetIndex(row + 1)) {
boost::optional<typename SparseModelType::ValueType> targetValue, sinkValue;
for (auto const& entry : origMatrix.getRow(row)) {
if(maybeStates.get(entry.getColumn())) {
builder.addNextValue(currRow, oldToNewIndexMap[entry.getColumn()], entry.getValue());
} else if (targetStates.get(entry.getColumn())) {
targetProbability = targetProbability.is_initialized() ? *targetProbability + entry.getValue() : entry.getValue();
} else if (sinkStates.get(entry.getColumn())) {
sinkProbability = sinkProbability.is_initialized() ? *sinkProbability + entry.getValue() : entry.getValue();
uint_fast64_t const& newColumn = resultData.oldToNewStateIndexMapping[entry.getColumn()];
if (newColumn < maybeStateCount) {
builder.addNextValue(currRow, newColumn, entry.getValue());
} else if (resultData.targetState && newColumn == resultData.targetState.get()) {
targetValue = targetValue.is_initialized() ? *targetValue + entry.getValue() : entry.getValue();
} else if (resultData.sinkState && newColumn == resultData.sinkState.get()) {
sinkValue = sinkValue.is_initialized() ? *sinkValue + entry.getValue() : entry.getValue();
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "There is a transition originating from a maybestate that does not lead to a maybe-, target-, or sinkstate.");
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "There is a transition originating from a maybestate that does not lead to a maybe-, target-, or sinkstate.");
}
}
if(targetProbability) {
assert(newTargetState);
builder.addNextValue(currRow, *newTargetState, storm::utility::simplify(*targetProbability));
if(targetValue) {
builder.addNextValue(currRow, *resultData.targetState, storm::utility::simplify(*targetValue));
}
if(sinkProbability) {
assert(newSinkState);
builder.addNextValue(currRow, *newSinkState, storm::utility::simplify(*sinkProbability));
if(sinkValue) {
builder.addNextValue(currRow, *resultData.sinkState, storm::utility::simplify(*sinkValue));
}
++currRow;
}
}
// Add the selfloops at target and sink
if(newTargetState) {
if(resultData.targetState) {
builder.newRowGroup(currRow);
builder.addNextValue(currRow, *newTargetState, storm::utility::one<typename SparseModelType::ValueType>());
builder.addNextValue(currRow, *resultData.targetState, storm::utility::one<typename SparseModelType::ValueType>());
++currRow;
}
if(newSinkState) {
if(resultData.sinkState) {
builder.newRowGroup(currRow);
builder.addNextValue(currRow, *newSinkState, storm::utility::one<typename SparseModelType::ValueType>());
builder.addNextValue(currRow, *resultData.sinkState, storm::utility::one<typename SparseModelType::ValueType>());
++currRow;
}
return builder.build();
}
template <typename SparseModelType>
storm::models::sparse::StateLabeling GoalStateMerger<SparseModelType>::buildStateLabeling(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, ReturnType const& resultData) const {
uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0);
storm::models::sparse::StateLabeling labeling(stateCount);
for (auto const& label : originalModel.getLabels()) {
storm::storage::BitVector const& oldStatesWithLabel = originalModel.getStates(label);
storm::storage::BitVector newStatesWithLabel = oldStatesWithLabel % maybeStates;
newStatesWithLabel.resize(stateCount, false);
if (!oldStatesWithLabel.isDisjointFrom(targetStates)) {
newStatesWithLabel.set(*resultData.targetState, true);
}
if (!oldStatesWithLabel.isDisjointFrom(sinkStates)) {
newStatesWithLabel.set(*resultData.sinkState, true);
}
labeling.addLabel(label, std::move(newStatesWithLabel));
}
return labeling;
}
template <typename SparseModelType>
std::unordered_map<std::string, typename SparseModelType::RewardModelType> GoalStateMerger<SparseModelType>::buildRewardModels(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, std::vector<std::string> const& selectedRewardModels) const {
typedef typename SparseModelType::RewardModelType::ValueType RewardValueType;
uint_fast64_t maybeStateCount = maybeStates.getNumberOfSetBits();
uint_fast64_t stateCount = maybeStateCount + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0);
uint_fast64_t choiceCount = resultData.keptChoices.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0);
std::unordered_map<std::string, typename SparseModelType::RewardModelType> rewardModels;
for (auto rewardModelName : selectedRewardModels) {
auto origRewardModel = originalModel.getRewardModel(rewardModelName);
boost::optional<std::vector<RewardValueType>> stateRewards;
if (origRewardModel.hasStateRewards) {
stateRewards = storm::utility::vector::filterVector(origRewardModel.getStateRewardVector(), maybeStates);
stateRewards->resize(stateCount, storm::utility::zero<RewardValueType>());
}
boost::optional<std::vector<RewardValueType>> stateActionRewards;
if (origRewardModel.hasStateActionRewards) {
stateActionRewards = storm::utility::vector::filterVector(origRewardModel.getStateActionRewardVector(), resultData.keptChoices);
stateActionRewards->resize(choiceCount, storm::utility::zero<RewardValueType>());
}
boost::optional<storm::storage::SparseMatrix<RewardValueType>> transitionRewards;
if (origRewardModel.hasTransitionRewards) {
storm::storage::SparseMatrixBuilder<RewardValueType> builder(choiceCount, stateCount, 0, true);
for (auto const& row : resultData.keptChoices) {
boost::optional<typename SparseModelType::ValueType> targetValue, sinkValue;
for (auto const& entry : origRewardModel.getTransitionRewardMatrix().getRow(row)) {
uint_fast64_t const& newColumn = resultData.oldToNewStateIndexMapping[entry.getColumn()];
if (newColumn < maybeStateCount) {
builder.addNextValue(row, newColumn, entry.getValue());
} else if (resultData.targetState && newColumn == resultData.targetState.get()) {
targetValue = targetValue.is_initialized() ? *targetValue + entry.getValue() : entry.getValue();
} else if (resultData.sinkState && newColumn == resultData.sinkState.get()) {
sinkValue = sinkValue.is_initialized() ? *sinkValue + entry.getValue() : entry.getValue();
} else {
STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "There is a transition reward originating from a maybestate that does not lead to a maybe-, target-, or sinkstate.");
}
}
if(targetValue) {
builder.addNextValue(row, *resultData.targetState, storm::utility::simplify(*targetValue));
}
if(sinkValue) {
builder.addNextValue(row, *resultData.sinkState, storm::utility::simplify(*sinkValue));
}
}
transitionRewards = builder.build();
}
rewardModels.insert(std::make_pair(rewardModelName, typename SparseModelType::RewardModelType(std::move(stateRewards), std::move(stateActionRewards), std::move(transitionRewards))));
}
return rewardModels;
}
template <>
std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> GoalStateMerger<storm::models::sparse::MarkovAutomaton<double>>::buildOutputModel(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix<double>&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, typename storm::models::sparse::MarkovAutomaton<double>::RewardModelType>&& rewardModels) const {
uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0);
storm::storage::BitVector markovianStates = originalModel.getMarkovianStates() % maybeStates;
markovianStates.resize(stateCount, true);
std::vector<double> exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), maybeStates);
exitRates.resize(stateCount, storm::utility::one<double>());
return std::make_shared<storm::models::sparse::MarkovAutomaton<double>> (std::move(transitionMatrix), std::move(labeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels));
}
template <typename SparseModelType>
std::shared_ptr<SparseModelType> GoalStateMerger<SparseModelType>::buildOutputModel(storm::storage::BitVector const& maybeStates, GoalStateMerger::ReturnType const& resultData, storm::storage::SparseMatrix<typename SparseModelType::ValueType>&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, typename SparseModelType::RewardModelType>&& rewardModels) const {
return std::make_shared<SparseModelType>(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels));
}
template class GoalStateMerger<storm::models::sparse::Dtmc<double>>;
template class GoalStateMerger<storm::models::sparse::Mdp<double>>;
template class GoalStateMerger<storm::models::sparse::MarkovAutomaton<double>>;
template class GoalStateMerger<storm::models::sparse::Dtmc<storm::RationalNumber>>;
template class GoalStateMerger<storm::models::sparse::Mdp<storm::RationalNumber>>;
template class GoalStateMerger<storm::models::sparse::Dtmc<storm::RationalFunction>>;

40
src/storm/transformer/GoalStateMerger.h
View File

@ -3,56 +3,64 @@
#include <memory>
#include <string>
#include <vector>
#include <unordered_map>
#include <boost/optional.hpp>
#include "storm/storage/BitVector.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/models/sparse/StateLabeling.h"
namespace storm {
namespace transformer {
/*
* Merges the given target and sink states into a single state with a selfloop
* Merges the given target and sink states into single states with a selfloop
*/
template <typename SparseModelType>
class GoalStateMerger {
public:
struct ReturnType {
std::shared_ptr<SparseModelType> model; // The output model
boost::optional<uint_fast64_t> targetState; // The target state of the output model (if reachable)
boost::optional<uint_fast64_t> sinkState; // The sink state of the output model (if reachable)
std::vector<uint_fast64_t> oldToNewStateIndexMapping; // maps a state from the input model to the corresponding state of the output model. Invalid index if the state does not exist
storm::storage::BitVector keptChoices; // The choices of the input model that are still present in the output model
};
GoalStateMerger(SparseModelType const& model);
/* Computes a submodel of the specified model that only considers the states given by maybeStates as well as
* * one target state to which all transitions to a state selected by targetStates are redirected and
* * one sink state to which all transitions to a state selected by sinkStates are redirected.
* If there is no transition to either target or sink, the corresponding state will not be created.
*
* The two given bitvectors targetStates and sinkStates are modified such that they represent the corresponding state in the obtained submodel.
*
* Notes:
* * The resulting model will not have any labels (other then "init") and only the selected reward models.
* * Rewards are reduced to stateActionRewards.
* * The target and sink states will not get any reward
* * It is assumed that the given set of maybeStates can only be left via either a target or a sink state. Otherwise an exception is thrown.
* * It is assumed that maybeStates, targetStates, and sinkStates are all disjoint. Otherwise an exception is thrown.
* * the target (or sink) state is not created, if it is not reachable
* * the target (or sink) state will get a label iff at least one of the given targetStates (sinkStates) have that label.
* * Only the selected reward models will be kept. The target and sink states will not get any reward.
* * Choices that lead from a maybeState to a ~(target | sink) state will be removed. An exception is thrown if this leads to deadlocks.
* * It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise an exception is thrown.
*/
std::shared_ptr<SparseModelType> mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector& targetStates, storm::storage::BitVector& sinkStates, std::vector<std::string> const& selectedRewardModels = std::vector<std::string>());
ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels = std::vector<std::string>()) const;
private:
SparseModelType const& originalModel;
/*!
* Initializes the matrix builder for the transition matrix of the resulting model
* Initializes the data required to build the result model
*
* @param newTargetState Will be set to the index of the target state of the resulting model (Only if it has a target state)
* @param newSinkState Will be set to the index of the sink state of the resulting model (Only if it has a sink state)
* @return The initialized result and the number of transitions of the result model
*/
storm::storage::SparseMatrixBuilder<typename SparseModelType::ValueType> initializeTransitionMatrixBuilder(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional<uint_fast64_t>& newTargetState, boost::optional<uint_fast64_t>& newSinkState);
std::pair<ReturnType, uint_fast64_t> initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const;
/*!
* Builds the transition matrix of the resulting model
*/
storm::storage::SparseMatrix<typename SparseModelType::ValueType> buildTransitionMatrix(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional<uint_fast64_t> const& newTargetState, boost::optional<uint_fast64_t> const& newSinkState, storm::storage::SparseMatrixBuilder<typename SparseModelType::ValueType>& builder);
storm::storage::SparseMatrix<typename SparseModelType::ValueType> buildTransitionMatrix(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, uint_fast64_t transitionCount) const;
storm::models::sparse::StateLabeling buildStateLabeling(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, ReturnType const& resultData) const;
std::unordered_map<std::string, typename SparseModelType::RewardModelType> buildRewardModels(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, std::vector<std::string> const& selectedRewardModels) const;
std::shared_ptr<SparseModelType> buildOutputModel(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix<typename SparseModelType::ValueType>&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map<std::string, typename SparseModelType::RewardModelType>&& rewardModels) const;
};
}

51
src/storm/transformer/SparseParametricDtmcSimplifier.cpp
View File

@ -38,12 +38,20 @@ namespace storm {
// obtain the resulting subsystem
storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first);
this->simplifiedModel->getStateLabeling().addLabel("target", statesWithProbability01.second);
this->simplifiedModel->getStateLabeling().addLabel("sink", statesWithProbability01.first);
storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first);
this->simplifiedModel = mergerResult.model;
statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
if (mergerResult.targetState) {
statesWithProbability01.first.set(mergerResult.targetState.get(), true);
}
std::string targetLabel = "target";
while (this->simplifiedModel->hasLabel(targetLabel)) {
targetLabel = "_" + targetLabel;
}
this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(statesWithProbability01.second));
// obtain the simplified formula for the simplified model
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> ("target");
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> (targetLabel);
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula const>(labelFormula, storm::logic::FormulaContext::Probability);
this->simplifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(eventuallyFormula, formula.getOperatorInformation());
@ -82,12 +90,20 @@ namespace storm {
// obtain the resulting subsystem
storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates);
this->simplifiedModel->getStateLabeling().addLabel("target", psiStates);
this->simplifiedModel->getStateLabeling().addLabel("sink", prob0States);
storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates);
this->simplifiedModel = mergerResult.model;
psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
if (mergerResult.targetState) {
psiStates.set(mergerResult.targetState.get(), true);
}
std::string targetLabel = "target";
while (this->simplifiedModel->hasLabel(targetLabel)) {
targetLabel = "_" + targetLabel;
}
this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates));
// obtain the simplified formula for the simplified model
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> ("target");
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> (targetLabel);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula const>(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps);
this->simplifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(boundedUntilFormula, formula.getOperatorInformation());
@ -116,12 +132,20 @@ namespace storm {
// obtain the resulting subsystem
std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector);
this->simplifiedModel->getStateLabeling().addLabel("target", targetStates);
this->simplifiedModel->getStateLabeling().addLabel("sink", infinityStates);
storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector);
this->simplifiedModel = mergerResult.model;
targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
if (mergerResult.targetState) {
targetStates.set(mergerResult.targetState.get(), true);
}
std::string targetLabel = "target";
while (this->simplifiedModel->hasLabel(targetLabel)) {
targetLabel = "_" + targetLabel;
}
this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates));
// obtain the simplified formula for the simplified model
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> ("target");
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> (targetLabel);
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula const>(labelFormula, storm::logic::FormulaContext::Reward);
this->simplifiedFormula = std::make_shared<storm::logic::RewardOperatorFormula const>(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation);
@ -151,7 +175,8 @@ namespace storm {
// obtain the resulting subsystem
std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector);
storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector);
this->simplifiedModel = mergerResult.model;
// obtain the simplified formula for the simplified model
this->simplifiedFormula = storm::logic::CloneVisitor().clone(formula);

51
src/storm/transformer/SparseParametricMdpSimplifier.cpp
View File

@ -45,12 +45,20 @@ namespace storm {
// obtain the resulting subsystem
storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first);
this->simplifiedModel->getStateLabeling().addLabel("target", statesWithProbability01.second);
this->simplifiedModel->getStateLabeling().addLabel("sink", statesWithProbability01.first);
storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first);
this->simplifiedModel = mergerResult.model;
statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
if (mergerResult.targetState) {
statesWithProbability01.first.set(mergerResult.targetState.get(), true);
}
std::string targetLabel = "target";
while (this->simplifiedModel->hasLabel(targetLabel)) {
targetLabel = "_" + targetLabel;
}
this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(statesWithProbability01.second));
// obtain the simplified formula for the simplified model
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> ("target");
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> (targetLabel);
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula const>(labelFormula, storm::logic::FormulaContext::Probability);
this->simplifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(eventuallyFormula, formula.getOperatorInformation());
@ -97,12 +105,20 @@ namespace storm {
// obtain the resulting subsystem
storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates);
this->simplifiedModel->getStateLabeling().addLabel("target", psiStates);
this->simplifiedModel->getStateLabeling().addLabel("sink", prob0States);
storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates);
this->simplifiedModel = mergerResult.model;
psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
if (mergerResult.targetState) {
psiStates.set(mergerResult.targetState.get(), true);
}
std::string targetLabel = "target";
while (this->simplifiedModel->hasLabel(targetLabel)) {
targetLabel = "_" + targetLabel;
}
this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates));
// obtain the simplified formula for the simplified model
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> ("target");
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> (targetLabel);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula const>(storm::logic::Formula::getTrueFormula(), labelFormula, boost::none, storm::logic::TimeBound(formula.getSubformula().asBoundedUntilFormula().isUpperBoundStrict(), formula.getSubformula().asBoundedUntilFormula().getUpperBound()), storm::logic::TimeBoundType::Steps);
this->simplifiedFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula const>(boundedUntilFormula, formula.getOperatorInformation());
@ -138,12 +154,20 @@ namespace storm {
// obtain the resulting subsystem
std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector);
this->simplifiedModel->getStateLabeling().addLabel("target", targetStates);
this->simplifiedModel->getStateLabeling().addLabel("sink", infinityStates);
storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector);
this->simplifiedModel = mergerResult.model;
targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false);
if (mergerResult.targetState) {
targetStates.set(mergerResult.targetState.get(), true);
}
std::string targetLabel = "target";
while (this->simplifiedModel->hasLabel(targetLabel)) {
targetLabel = "_" + targetLabel;
}
this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates));
// obtain the simplified formula for the simplified model
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> ("target");
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula const> (targetLabel);
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula const>(labelFormula, storm::logic::FormulaContext::Reward);
this->simplifiedFormula = std::make_shared<storm::logic::RewardOperatorFormula const>(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation);
@ -180,7 +204,8 @@ namespace storm {
// obtain the resulting subsystem
std::vector<std::string> rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first);
storm::transformer::GoalStateMerger<SparseModelType> goalStateMerger(this->originalModel);
this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector);
storm::transformer::GoalStateMerger<SparseModelType>::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector);
this->simplifiedModel = mergerResult.model;
// obtain the simplified formula for the simplified model
this->simplifiedFormula = storm::logic::CloneVisitor().clone(formula);

Write Preview
Loading…
Cancel
Save