diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp index bcb4a8f05..73357743c 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.cpp +++ b/src/modelchecker/reachability/SparseSccModelChecker.cpp @@ -12,6 +12,25 @@ namespace storm { namespace modelchecker { namespace reachability { + template + static ValueType&& simplify(ValueType&& value) { + // In the general case, we don't to anything here, but merely return the value. If something else is + // supposed to happen here, the templated function can be specialized for this particular type. + return std::forward(value); + } + + template + static storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry) { + simplify(matrixEntry.getValue()); + return std::move(matrixEntry); + } + + template + static storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry) { + matrixEntry.setValue(simplify(matrixEntry.getValue())); + return matrixEntry; + } + template ValueType SparseSccModelChecker::computeReachabilityProbability(storm::models::Dtmc const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // First, do some sanity checks to establish some required properties. @@ -54,7 +73,8 @@ namespace storm { template void SparseSccModelChecker::treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) { - if (level <= 3) { + // If the SCCs are still quite large, we try to split them further. + if (scc.getNumberOfSetBits() > SparseSccModelChecker::maximalSccSize) { // Here, we further decompose the SCC into sub-SCCs. storm::storage::StronglyConnectedComponentDecomposition decomposition(forwardTransitions, scc & ~entryStates, true, false); @@ -117,6 +137,7 @@ namespace storm { template void SparseSccModelChecker::eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions) { + bool hasSelfLoop = false; ValueType loopProbability = storm::utility::constantZero(); // Start by finding loop probability. @@ -125,17 +146,21 @@ namespace storm { if (entry.getColumn() >= state) { if (entry.getColumn() == state) { loopProbability = entry.getValue(); + hasSelfLoop = true; } break; } } - // Scale all entries in this row with (1 / (1 - loopProbability)). - loopProbability = 1 / (1 - loopProbability); - for (auto& entry : matrix.getRow(state)) { - entry.setValue(entry.getValue() * loopProbability); + // Scale all entries in this row with (1 / (1 - loopProbability)) only in case there was a self-loop. + if (hasSelfLoop) { + loopProbability = 1 / (1 - loopProbability); + simplify(loopProbability); + for (auto& entry : matrix.getRow(state)) { + entry.setValue(simplify(entry.getValue() * loopProbability)); + } + oneStepProbabilities[state] = simplify(oneStepProbabilities[state] * loopProbability); } - oneStepProbabilities[state] *= loopProbability; // Now connect the predecessors of the state being eliminated with its successors. typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state); @@ -185,20 +210,20 @@ namespace storm { break; } if (first2->getColumn() < first1->getColumn()) { - *result = *first2 * multiplyFactor; + *result = simplify(*first2 * multiplyFactor); ++first2; } else if (first1->getColumn() < first2->getColumn()) { *result = *first1; ++first1; } else { - *result = storm::storage::MatrixEntry::index_type, typename FlexibleSparseMatrix::value_type>(first1->getColumn(), first1->getValue() + multiplyFactor * first2->getValue()); + *result = storm::storage::MatrixEntry::index_type, typename FlexibleSparseMatrix::value_type>(first1->getColumn(), simplify(first1->getValue() + simplify(multiplyFactor * first2->getValue()))); ++first1; ++first2; } } for (; first2 != last2; ++first2) { if (first2->getColumn() != state) { - *result = *first2 * multiplyFactor; + *result = simplify(*first2 * multiplyFactor); } } @@ -206,7 +231,7 @@ namespace storm { predecessorForwardTransitions = std::move(newSuccessors); // Add the probabilities to go to a target state in just one step. - oneStepProbabilities[predecessor] += multiplyFactor * oneStepProbabilities[state]; + oneStepProbabilities[predecessor] = simplify(oneStepProbabilities[predecessor] + simplify(multiplyFactor * oneStepProbabilities[state])); } // Finally, we need to add the predecessor to the set of predecessors of every successor. diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h index ae3ff102e..775c7b3ca 100644 --- a/src/modelchecker/reachability/SparseSccModelChecker.h +++ b/src/modelchecker/reachability/SparseSccModelChecker.h @@ -26,9 +26,6 @@ namespace storm { template class SparseSccModelChecker { - private: - - public: static ValueType computeReachabilityProbability(storm::models::Dtmc const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates); @@ -36,6 +33,8 @@ namespace storm { static void treatScc(storm::models::Dtmc const& dtmc, FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level); static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix const& matrix, bool setAllValuesToOne = false); static void eliminateState(FlexibleSparseMatrix& matrix, std::vector& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions); + + static const uint_fast64_t maximalSccSize = 1000; }; } diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index d8a900d8b..83c8edd57 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -74,6 +74,9 @@ namespace storm { // At this point we know that a new option is about to come. Hence, we need to assign the current // cache content to the option that was active until now. setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->shortNameToOptions : this->longNameToOptions, argumentCache); + + // After the assignment, the argument cache needs to be cleared. + argumentCache.clear(); } else { optionActive = true; } @@ -110,7 +113,7 @@ namespace storm { } void SettingsManager::setFromConfigurationFile(std::string const& configFilename) { - LOG_ASSERT(false, "Not yet implemented"); + LOG_ASSERT(false, "Not yet implemented."); } void SettingsManager::printHelp(std::string const& hint) const {