From b6d085a92da7c4cfdd17b7972f685cfa7d763397 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 30 Apr 2017 14:46:52 +0200 Subject: [PATCH] fixes and improvements for the new goal state merger --- src/storm/transformer/GoalStateMerger.cpp | 25 +++++++++++++++---- src/storm/transformer/GoalStateMerger.h | 1 + .../SparseParametricDtmcSimplifier.cpp | 10 ++++---- .../SparseParametricMdpSimplifier.cpp | 10 ++++---- 4 files changed, 31 insertions(+), 15 deletions(-) diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index 9b67ca078..bcfa4a33a 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -30,7 +30,7 @@ namespace storm { auto result = initialize(maybeStates, targetStates, sinkStates); - auto transitionMatrix = buildTransitionMatrix(maybeStates, targetStates, sinkStates, result.first, result.second); + auto transitionMatrix = buildTransitionMatrix(maybeStates, result.first, result.second); auto labeling = buildStateLabeling(maybeStates, targetStates, sinkStates, result.first); auto rewardModels = buildRewardModels(maybeStates, result.first, selectedRewardModels); @@ -169,7 +169,7 @@ namespace storm { 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()) { + for (auto const& label : originalModel.getStateLabeling().getLabels()) { storm::storage::BitVector const& oldStatesWithLabel = originalModel.getStates(label); storm::storage::BitVector newStatesWithLabel = oldStatesWithLabel % maybeStates; newStatesWithLabel.resize(stateCount, false); @@ -199,19 +199,19 @@ namespace storm { auto origRewardModel = originalModel.getRewardModel(rewardModelName); boost::optional> stateRewards; - if (origRewardModel.hasStateRewards) { + if (origRewardModel.hasStateRewards()) { stateRewards = storm::utility::vector::filterVector(origRewardModel.getStateRewardVector(), maybeStates); stateRewards->resize(stateCount, storm::utility::zero()); } boost::optional> stateActionRewards; - if (origRewardModel.hasStateActionRewards) { + if (origRewardModel.hasStateActionRewards()) { stateActionRewards = storm::utility::vector::filterVector(origRewardModel.getStateActionRewardVector(), resultData.keptChoices); stateActionRewards->resize(choiceCount, storm::utility::zero()); } boost::optional> transitionRewards; - if (origRewardModel.hasTransitionRewards) { + if (origRewardModel.hasTransitionRewards()) { storm::storage::SparseMatrixBuilder builder(choiceCount, stateCount, 0, true); for (auto const& row : resultData.keptChoices) { boost::optional targetValue, sinkValue; @@ -256,6 +256,20 @@ namespace storm { return std::make_shared> (std::move(transitionMatrix), std::move(labeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels)); } + template <> + std::shared_ptr> GoalStateMerger>::buildOutputModel(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map::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 exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), maybeStates); + exitRates.resize(stateCount, storm::utility::one()); + + return std::make_shared> (std::move(transitionMatrix), std::move(labeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels)); + } + template std::shared_ptr GoalStateMerger::buildOutputModel(storm::storage::BitVector const& maybeStates, GoalStateMerger::ReturnType const& resultData, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels) const { @@ -267,6 +281,7 @@ namespace storm { template class GoalStateMerger>; template class GoalStateMerger>; template class GoalStateMerger>; + template class GoalStateMerger>; template class GoalStateMerger>; template class GoalStateMerger>; diff --git a/src/storm/transformer/GoalStateMerger.h b/src/storm/transformer/GoalStateMerger.h index 9bf2347b4..4350e3ae1 100644 --- a/src/storm/transformer/GoalStateMerger.h +++ b/src/storm/transformer/GoalStateMerger.h @@ -41,6 +41,7 @@ namespace storm { * * 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. + * * The order of the maybeStates will not be affected (i.e. s_1 < s_2 in the input model implies s'_1 < s'_2 in the output model). */ ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels = std::vector()) const; diff --git a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp index af3265da9..912c7ccbb 100644 --- a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp @@ -38,7 +38,7 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first); + typename storm::transformer::GoalStateMerger::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) { @@ -90,7 +90,7 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates); this->simplifiedModel = mergerResult.model; psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); if (mergerResult.targetState) { @@ -132,7 +132,7 @@ namespace storm { // obtain the resulting subsystem std::vector rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); this->simplifiedModel = mergerResult.model; targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); if (mergerResult.targetState) { @@ -142,7 +142,7 @@ namespace storm { while (this->simplifiedModel->hasLabel(targetLabel)) { targetLabel = "_" + targetLabel; } - this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates)); + this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(targetStates)); // obtain the simplified formula for the simplified model auto labelFormula = std::make_shared (targetLabel); @@ -175,7 +175,7 @@ namespace storm { // obtain the resulting subsystem std::vector rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); this->simplifiedModel = mergerResult.model; // obtain the simplified formula for the simplified model diff --git a/src/storm/transformer/SparseParametricMdpSimplifier.cpp b/src/storm/transformer/SparseParametricMdpSimplifier.cpp index b08124c2b..c0e36e9d5 100644 --- a/src/storm/transformer/SparseParametricMdpSimplifier.cpp +++ b/src/storm/transformer/SparseParametricMdpSimplifier.cpp @@ -45,7 +45,7 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first); + typename storm::transformer::GoalStateMerger::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) { @@ -105,7 +105,7 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates); this->simplifiedModel = mergerResult.model; psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); if (mergerResult.targetState) { @@ -154,7 +154,7 @@ namespace storm { // obtain the resulting subsystem std::vector rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); this->simplifiedModel = mergerResult.model; targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); if (mergerResult.targetState) { @@ -164,7 +164,7 @@ namespace storm { while (this->simplifiedModel->hasLabel(targetLabel)) { targetLabel = "_" + targetLabel; } - this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(psiStates)); + this->simplifiedModel->getStateLabeling().addLabel(targetLabel, std::move(targetStates)); // obtain the simplified formula for the simplified model auto labelFormula = std::make_shared (targetLabel); @@ -204,7 +204,7 @@ namespace storm { // obtain the resulting subsystem std::vector rewardModelNameAsVector(1, formula.hasRewardModelName() ? formula.getRewardModelName() : this->originalModel.getRewardModels().begin()->first); storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); this->simplifiedModel = mergerResult.model; // obtain the simplified formula for the simplified model