diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index f7ccc7f19..9b67ca078 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -2,15 +2,18 @@ #include #include +#include #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 - std::shared_ptr GoalStateMerger::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector& targetStates, storm::storage::BitVector& sinkStates, std::vector const& selectedRewardModels) { + typename GoalStateMerger::ReturnType GoalStateMerger::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector 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 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(); - - // 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)); - - // Get the reward models - std::unordered_map 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()); - 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(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); + 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); + + result.first.model = buildOutputModel(maybeStates, result.first, std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); + + return result.first; } template - storm::storage::SparseMatrixBuilder GoalStateMerger::initializeTransitionMatrixBuilder(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional& newTargetState, boost::optional& newSinkState) { + std::pair::ReturnType, uint_fast64_t> GoalStateMerger::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const { storm::storage::SparseMatrix 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(maybeStates.size(), std::numeric_limits::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; + if (maybeStates.get(entry.getColumn())) { + ++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(hasTransitionToTarget) { - ++resNumTransitions; - targetStateRequired = true; - } - if(hasTransitionToSink) { - ++resNumTransitions; - sinkStateRequired = true; + if (keepThisRow) { + stateIsDeadlock = false; + result.keptChoices.set(row, true); + transitionCount += transitionsToMaybeStates; + if(hasTransitionToTarget) { + ++transitionCount; + targetStateRequired = true; + } + if(hasTransitionToSink) { + ++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(resNumActions, resNumStates, resNumTransitions, true, true, resNumStates); + return std::make_pair(std::move(result), std::move(transitionCount)); } template - storm::storage::SparseMatrix GoalStateMerger::buildTransitionMatrix(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional const& newTargetState, boost::optionalconst& newSinkState, storm::storage::SparseMatrixBuilder& builder) { + storm::storage::SparseMatrix GoalStateMerger::buildTransitionMatrix(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, uint_fast64_t transitionCount) const { - // Get a Mapping that yields for each column in the old matrix the corresponding column in the new matrix - std::vector oldToNewIndexMap(maybeStates.size(), std::numeric_limits::max()); // init with some invalid state - uint_fast64_t newStateIndex = 0; - for (auto maybeState : maybeStates) { - oldToNewIndexMap[maybeState] = newStateIndex; - ++newStateIndex; - } - - // Build the transition matrix storm::storage::SparseMatrix 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 builder(rowCount, stateCount, transitionCount, true, origMatrix.hasTrivialRowGrouping(), origMatrix.hasTrivialRowGrouping() ? 0 : stateCount); + uint_fast64_t currRow = 0; for (auto state : maybeStates) { - builder.newRowGroup(currRow); - auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state+1]; - for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) { - boost::optional targetProbability, sinkProbability; + if (!origMatrix.hasTrivialRowGrouping()) { + builder.newRowGroup(currRow); + } + auto const& endOfRowGroup = origMatrix.getRowGroupIndices()[state + 1]; + for (uint_fast64_t row = resultData.keptChoices.getNextSetIndex(origMatrix.getRowGroupIndices()[state]); row < endOfRowGroup; row = resultData.keptChoices.getNextSetIndex(row + 1)) { + boost::optional 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()); + builder.addNextValue(currRow, *resultData.targetState, storm::utility::one()); ++currRow; } - if(newSinkState) { + if(resultData.sinkState) { builder.newRowGroup(currRow); - builder.addNextValue(currRow, *newSinkState, storm::utility::one()); + builder.addNextValue(currRow, *resultData.sinkState, storm::utility::one()); ++currRow; } return builder.build(); } + + template + storm::models::sparse::StateLabeling GoalStateMerger::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 + std::unordered_map GoalStateMerger::buildRewardModels(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, std::vector 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 rewardModels; + for (auto rewardModelName : selectedRewardModels) { + auto origRewardModel = originalModel.getRewardModel(rewardModelName); + + boost::optional> stateRewards; + if (origRewardModel.hasStateRewards) { + stateRewards = storm::utility::vector::filterVector(origRewardModel.getStateRewardVector(), maybeStates); + stateRewards->resize(stateCount, storm::utility::zero()); + } + + boost::optional> stateActionRewards; + if (origRewardModel.hasStateActionRewards) { + stateActionRewards = storm::utility::vector::filterVector(origRewardModel.getStateActionRewardVector(), resultData.keptChoices); + stateActionRewards->resize(choiceCount, storm::utility::zero()); + } + + boost::optional> transitionRewards; + if (origRewardModel.hasTransitionRewards) { + storm::storage::SparseMatrixBuilder builder(choiceCount, stateCount, 0, true); + for (auto const& row : resultData.keptChoices) { + boost::optional 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> 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 { + + return std::make_shared(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); + } + 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 712eb9af6..9bf2347b4 100644 --- a/src/storm/transformer/GoalStateMerger.h +++ b/src/storm/transformer/GoalStateMerger.h @@ -3,56 +3,64 @@ #include #include #include +#include #include #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 class GoalStateMerger { public: + + struct ReturnType { + std::shared_ptr model; // The output model + boost::optional targetState; // The target state of the output model (if reachable) + boost::optional sinkState; // The sink state of the output model (if reachable) + std::vector 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 mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector& targetStates, storm::storage::BitVector& sinkStates, std::vector const& selectedRewardModels = std::vector()); + ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector const& selectedRewardModels = std::vector()) 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 initializeTransitionMatrixBuilder(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional& newTargetState, boost::optional& newSinkState); + std::pair 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 buildTransitionMatrix(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional const& newTargetState, boost::optional const& newSinkState, storm::storage::SparseMatrixBuilder& builder); - + storm::storage::SparseMatrix 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 buildRewardModels(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, std::vector const& selectedRewardModels) const; + std::shared_ptr buildOutputModel(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map&& rewardModels) const; }; } diff --git a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp index 9e10e1fda..af3265da9 100644 --- a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp @@ -38,12 +38,20 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger 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::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 ("target"); + auto labelFormula = std::make_shared (targetLabel); auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Probability); this->simplifiedFormula = std::make_shared(eventuallyFormula, formula.getOperatorInformation()); @@ -82,12 +90,20 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger 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::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 ("target"); + auto labelFormula = std::make_shared (targetLabel); auto boundedUntilFormula = std::make_shared(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(boundedUntilFormula, formula.getOperatorInformation()); @@ -116,12 +132,20 @@ 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); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); - this->simplifiedModel->getStateLabeling().addLabel("target", targetStates); - this->simplifiedModel->getStateLabeling().addLabel("sink", infinityStates); + 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) { + 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 ("target"); + auto labelFormula = std::make_shared (targetLabel); auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Reward); this->simplifiedFormula = std::make_shared(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation); @@ -151,7 +175,8 @@ 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); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); + storm::transformer::GoalStateMerger::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); diff --git a/src/storm/transformer/SparseParametricMdpSimplifier.cpp b/src/storm/transformer/SparseParametricMdpSimplifier.cpp index 192545b2d..b08124c2b 100644 --- a/src/storm/transformer/SparseParametricMdpSimplifier.cpp +++ b/src/storm/transformer/SparseParametricMdpSimplifier.cpp @@ -45,12 +45,20 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger 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::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 ("target"); + auto labelFormula = std::make_shared (targetLabel); auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Probability); this->simplifiedFormula = std::make_shared(eventuallyFormula, formula.getOperatorInformation()); @@ -97,12 +105,20 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger 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::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 ("target"); + auto labelFormula = std::make_shared (targetLabel); auto boundedUntilFormula = std::make_shared(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(boundedUntilFormula, formula.getOperatorInformation()); @@ -138,12 +154,20 @@ 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); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); - this->simplifiedModel->getStateLabeling().addLabel("target", targetStates); - this->simplifiedModel->getStateLabeling().addLabel("sink", infinityStates); + 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) { + 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 ("target"); + auto labelFormula = std::make_shared (targetLabel); auto eventuallyFormula = std::make_shared(labelFormula, storm::logic::FormulaContext::Reward); this->simplifiedFormula = std::make_shared(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation); @@ -180,7 +204,8 @@ 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); - this->simplifiedModel = goalStateMerger.mergeTargetAndSinkStates(maybeStates, noStates, zeroRewardStates, rewardModelNameAsVector); + storm::transformer::GoalStateMerger::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);