diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index bcfa4a33a..a6a0b21dc 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -75,11 +75,11 @@ namespace storm { stateIsDeadlock = false; result.keptChoices.set(row, true); transitionCount += transitionsToMaybeStates; - if(hasTransitionToTarget) { + if (hasTransitionToTarget) { ++transitionCount; targetStateRequired = true; } - if(hasTransitionToSink) { + if (hasTransitionToSink) { ++transitionCount; sinkStateRequired = true; } @@ -90,14 +90,14 @@ namespace storm { } // Treat the target and sink states (if these states will exist) - if(targetStateRequired) { + if (targetStateRequired) { result.targetState = stateCount; ++stateCount; ++transitionCount; storm::utility::vector::setVectorValues(result.oldToNewStateIndexMapping, targetStates, *result.targetState); } - if(sinkStateRequired) { + if (sinkStateRequired) { result.sinkState = stateCount; ++stateCount; ++transitionCount; @@ -116,7 +116,7 @@ namespace storm { 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); + storm::storage::SparseMatrixBuilder builder(rowCount, stateCount, transitionCount, true, !origMatrix.hasTrivialRowGrouping(), origMatrix.hasTrivialRowGrouping() ? 0 : stateCount); uint_fast64_t currRow = 0; for (auto state : maybeStates) { @@ -138,10 +138,10 @@ namespace storm { 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(targetValue) { + if (targetValue) { builder.addNextValue(currRow, *resultData.targetState, storm::utility::simplify(*targetValue)); } - if(sinkValue) { + if (sinkValue) { builder.addNextValue(currRow, *resultData.sinkState, storm::utility::simplify(*sinkValue)); } ++currRow; @@ -149,13 +149,17 @@ namespace storm { } // Add the selfloops at target and sink - if(resultData.targetState) { - builder.newRowGroup(currRow); + if (resultData.targetState) { + if (!origMatrix.hasTrivialRowGrouping()) { + builder.newRowGroup(currRow); + } builder.addNextValue(currRow, *resultData.targetState, storm::utility::one()); ++currRow; } - if(resultData.sinkState) { - builder.newRowGroup(currRow); + if (resultData.sinkState) { + if (!origMatrix.hasTrivialRowGrouping()) { + builder.newRowGroup(currRow); + } builder.addNextValue(currRow, *resultData.sinkState, storm::utility::one()); ++currRow; } @@ -173,10 +177,10 @@ namespace storm { storm::storage::BitVector const& oldStatesWithLabel = originalModel.getStates(label); storm::storage::BitVector newStatesWithLabel = oldStatesWithLabel % maybeStates; newStatesWithLabel.resize(stateCount, false); - if (!oldStatesWithLabel.isDisjointFrom(targetStates)) { + if (!oldStatesWithLabel.isDisjointFrom(targetStates) && resultData.targetState.is_initialized()) { newStatesWithLabel.set(*resultData.targetState, true); } - if (!oldStatesWithLabel.isDisjointFrom(sinkStates)) { + if (!oldStatesWithLabel.isDisjointFrom(sinkStates) && resultData.sinkState.is_initialized()) { newStatesWithLabel.set(*resultData.sinkState, true); } labeling.addLabel(label, std::move(newStatesWithLabel)); @@ -227,10 +231,10 @@ namespace storm { 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) { + if (targetValue) { builder.addNextValue(row, *resultData.targetState, storm::utility::simplify(*targetValue)); } - if(sinkValue) { + if (sinkValue) { builder.addNextValue(row, *resultData.sinkState, storm::utility::simplify(*sinkValue)); } } diff --git a/src/storm/transformer/GoalStateMerger.h b/src/storm/transformer/GoalStateMerger.h index 4350e3ae1..bc9dadcda 100644 --- a/src/storm/transformer/GoalStateMerger.h +++ b/src/storm/transformer/GoalStateMerger.h @@ -37,7 +37,7 @@ namespace storm { * * Notes: * * 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. + * * the target (or sink) state will get a label iff it is reachable and 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. diff --git a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp index 912c7ccbb..972863b1b 100644 --- a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp @@ -42,7 +42,7 @@ namespace storm { this->simplifiedModel = mergerResult.model; statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); if (mergerResult.targetState) { - statesWithProbability01.first.set(mergerResult.targetState.get(), true); + statesWithProbability01.second.set(mergerResult.targetState.get(), true); } std::string targetLabel = "target"; while (this->simplifiedModel->hasLabel(targetLabel)) { @@ -56,7 +56,14 @@ namespace storm { this->simplifiedFormula = std::make_shared(eventuallyFormula, formula.getOperatorInformation()); // Eliminate all states for which all outgoing transitions are constant - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel); + storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); + if (mergerResult.targetState) { + considerForElimination.set(*mergerResult.targetState, false); + } + if (mergerResult.sinkState) { + considerForElimination.set(*mergerResult.sinkState, false); + } + this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination); return true; } @@ -90,7 +97,7 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, psiStates, prob0States); this->simplifiedModel = mergerResult.model; psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); if (mergerResult.targetState) { @@ -150,7 +157,14 @@ namespace storm { this->simplifiedFormula = std::make_shared(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation); // Eliminate all states for which all outgoing transitions are constant - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, rewardModelNameAsVector.front()); + storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); + if (mergerResult.targetState) { + considerForElimination.set(*mergerResult.targetState, false); + } + if (mergerResult.sinkState) { + considerForElimination.set(*mergerResult.sinkState, false); + } + this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination, rewardModelNameAsVector.front()); return true; } diff --git a/src/storm/transformer/SparseParametricMdpSimplifier.cpp b/src/storm/transformer/SparseParametricMdpSimplifier.cpp index c0e36e9d5..d84058637 100644 --- a/src/storm/transformer/SparseParametricMdpSimplifier.cpp +++ b/src/storm/transformer/SparseParametricMdpSimplifier.cpp @@ -47,9 +47,18 @@ namespace storm { storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, statesWithProbability01.second, statesWithProbability01.first); this->simplifiedModel = mergerResult.model; + statesWithProbability01.first = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); + if (mergerResult.sinkState) { + statesWithProbability01.first.set(mergerResult.sinkState.get(), true); + } + std::string sinkLabel = "sink"; + while (this->simplifiedModel->hasLabel(sinkLabel)) { + sinkLabel = "_" + sinkLabel; + } + this->simplifiedModel->getStateLabeling().addLabel(sinkLabel, std::move(statesWithProbability01.first)); statesWithProbability01.second = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); if (mergerResult.targetState) { - statesWithProbability01.first.set(mergerResult.targetState.get(), true); + statesWithProbability01.second.set(mergerResult.targetState.get(), true); } std::string targetLabel = "target"; while (this->simplifiedModel->hasLabel(targetLabel)) { @@ -63,11 +72,18 @@ namespace storm { this->simplifiedFormula = std::make_shared(eventuallyFormula, formula.getOperatorInformation()); // Eliminate all states for which all outgoing transitions are constant - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel); + storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); + if (mergerResult.targetState) { + considerForElimination.set(*mergerResult.targetState, false); + } + if (mergerResult.sinkState) { + considerForElimination.set(*mergerResult.sinkState, false); + } + this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination); // Eliminate the end components that do not contain a target or a sink state (only required if the probability is maximized) if(!minimizing) { - this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink")); + this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates(targetLabel) | this->simplifiedModel->getStates(sinkLabel)); } return true; @@ -105,7 +121,7 @@ namespace storm { // obtain the resulting subsystem storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); - typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, prob0States, psiStates); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, psiStates, prob0States); this->simplifiedModel = mergerResult.model; psiStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); if (mergerResult.targetState) { @@ -156,6 +172,16 @@ namespace storm { storm::transformer::GoalStateMerger goalStateMerger(this->originalModel); typename storm::transformer::GoalStateMerger::ReturnType mergerResult = goalStateMerger.mergeTargetAndSinkStates(maybeStates, targetStates, infinityStates, rewardModelNameAsVector); this->simplifiedModel = mergerResult.model; + infinityStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); + if (mergerResult.sinkState) { + infinityStates.set(mergerResult.sinkState.get(), true); + } + std::string sinkLabel = "sink"; + while (this->simplifiedModel->hasLabel(sinkLabel)) { + sinkLabel = "_" + sinkLabel; + } + this->simplifiedModel->getStateLabeling().addLabel(sinkLabel, std::move(infinityStates)); + targetStates = storm::storage::BitVector(this->simplifiedModel->getNumberOfStates(), false); if (mergerResult.targetState) { targetStates.set(mergerResult.targetState.get(), true); @@ -172,11 +198,18 @@ namespace storm { this->simplifiedFormula = std::make_shared(eventuallyFormula, rewardModelNameAsVector.front(), formula.getOperatorInformation(), storm::logic::RewardMeasureType::Expectation); // Eliminate all states for which all outgoing transitions are constant - this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, rewardModelNameAsVector.front()); + storm::storage::BitVector considerForElimination = ~this->simplifiedModel->getInitialStates(); + if (mergerResult.targetState) { + considerForElimination.set(*mergerResult.targetState, false); + } + if (mergerResult.sinkState) { + considerForElimination.set(*mergerResult.sinkState, false); + } + this->simplifiedModel = this->eliminateConstantDeterministicStates(*this->simplifiedModel, considerForElimination, rewardModelNameAsVector.front()); // Eliminate the end components in which no reward is collected (only required if rewards are minimized) if (minimizing) { - this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates("target") | this->simplifiedModel->getStates("sink"), rewardModelNameAsVector.front()); + this->simplifiedModel = this->eliminateNeutralEndComponents(*this->simplifiedModel, this->simplifiedModel->getStates(targetLabel) | this->simplifiedModel->getStates(sinkLabel), rewardModelNameAsVector.front()); } return true; } diff --git a/src/storm/transformer/SparseParametricModelSimplifier.cpp b/src/storm/transformer/SparseParametricModelSimplifier.cpp index 54fba2338..27b71ea27 100644 --- a/src/storm/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm/transformer/SparseParametricModelSimplifier.cpp @@ -97,15 +97,9 @@ namespace storm { } template - std::shared_ptr SparseParametricModelSimplifier::eliminateConstantDeterministicStates(SparseModelType const& model, boost::optional const& rewardModelName) { + std::shared_ptr SparseParametricModelSimplifier::eliminateConstantDeterministicStates(SparseModelType const& model, storm::storage::BitVector const& consideredStates, boost::optional const& rewardModelName) { storm::storage::SparseMatrix const& sparseMatrix = model.getTransitionMatrix(); - // Get the states without any label - storm::storage::BitVector considerForElimination(model.getNumberOfStates(), false); - for(auto const& label : model.getStateLabeling().getLabels()) { - considerForElimination |= model.getStateLabeling().getStates(label); - } - considerForElimination.complement(); // get the action-based reward values std::vector actionRewards; @@ -116,8 +110,8 @@ namespace storm { } // Find the states that are to be eliminated - storm::storage::BitVector selectedStates = considerForElimination; - for (auto state : considerForElimination) { + storm::storage::BitVector selectedStates = consideredStates; + for (auto state : consideredStates) { if (sparseMatrix.getRowGroupSize(state) == 1 && (!rewardModelName.is_initialized() || storm::utility::isConstant(actionRewards[sparseMatrix.getRowGroupIndices()[state]]))) { for (auto const& entry : sparseMatrix.getRowGroup(state)) { if(!storm::utility::isConstant(entry.getValue())) { diff --git a/src/storm/transformer/SparseParametricModelSimplifier.h b/src/storm/transformer/SparseParametricModelSimplifier.h index bf1d95214..ac1ae2949 100644 --- a/src/storm/transformer/SparseParametricModelSimplifier.h +++ b/src/storm/transformer/SparseParametricModelSimplifier.h @@ -56,9 +56,10 @@ namespace storm { * * there is no statelabel defined, and * * (if rewardModelName is given) the reward collected at the state is constant. * - * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given) + * The resulting model will only have the rewardModel with the provided name (or no reward model at all if no name was given). + * Labelings of eliminated states will be lost */ - static std::shared_ptr eliminateConstantDeterministicStates(SparseModelType const& model, boost::optional const& rewardModelName = boost::none); + static std::shared_ptr eliminateConstantDeterministicStates(SparseModelType const& model, storm::storage::BitVector const& consideredStates, boost::optional const& rewardModelName = boost::none); SparseModelType const& originalModel;