From 7f7778533a565c8568caaab98e6c31939f3233a5 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 2 Apr 2018 17:46:31 +0200 Subject: [PATCH] Typos --- .../modelchecker/dft/DFTModelChecker.cpp | 6 ++-- src/storm-dft/storage/dft/DFT.cpp | 29 +++++++++---------- src/storm/models/sparse/MarkovAutomaton.cpp | 14 ++++----- src/storm/utility/DirectEncodingExporter.cpp | 2 +- 4 files changed, 25 insertions(+), 26 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 31ba6789d..8d277d60d 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -54,14 +54,14 @@ namespace storm { case storm::storage::DFTElementType::AND: STORM_LOG_TRACE("top modularisation called AND"); dfts = dft.topModularisation(); - STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); + STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules."); nrK = dfts.size(); nrM = dfts.size(); break; case storm::storage::DFTElementType::OR: STORM_LOG_TRACE("top modularisation called OR"); dfts = dft.topModularisation(); - STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); + STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules."); nrK = 0; nrM = dfts.size(); invResults = true; @@ -69,7 +69,7 @@ namespace storm { case storm::storage::DFTElementType::VOT: STORM_LOG_TRACE("top modularisation called VOT"); dfts = dft.topModularisation(); - STORM_LOG_TRACE("Modularsation into " << dfts.size() << " submodules."); + STORM_LOG_TRACE("Modularisation into " << dfts.size() << " submodules."); nrK = std::static_pointer_cast const>(dft.getTopLevelGate())->threshold(); nrM = dfts.size(); if(nrK <= nrM/2) { diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 81784ea96..ad89354f3 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -293,22 +293,22 @@ namespace storm { } return max; } - + template DFT DFT::optimize() const { std::vector modIdea = findModularisationRewrite(); STORM_LOG_DEBUG("Modularisation idea: " << storm::utility::vector::toString(modIdea)); - + if (modIdea.empty()) { // No rewrite needed return *this; } - + std::vector> rewriteIds; rewriteIds.push_back(modIdea); - + storm::builder::DFTBuilder builder; - + // Accumulate elements which must be rewritten std::set rewriteSet; for (std::vector rewrites : rewriteIds) { @@ -320,7 +320,7 @@ namespace storm { builder.copyElement(elem); } } - + // Add rewritten elements for (std::vector rewrites : rewriteIds) { STORM_LOG_ASSERT(rewrites.size() > 1, "No rewritten elements."); @@ -359,7 +359,7 @@ namespace storm { STORM_LOG_ASSERT(false, "Dft type can not be rewritten."); break; } - + // Add parent with the new child newParent and all its remaining children childrenNames.clear(); childrenNames.push_back(newParentName); @@ -371,7 +371,7 @@ namespace storm { } builder.copyGate(originalParent, childrenNames); } - + builder.setTopLevel(mElements[mTopLevelIndex]->name()); // TODO use reference? DFT newDft = builder.build(); @@ -750,11 +750,10 @@ namespace storm { // suitable parent gate! - Lets check the independent submodules of the children auto const& children = std::static_pointer_cast>(e)->children(); for(auto const& child : children) { - - + auto ISD = std::static_pointer_cast>(child)->independentSubDft(true); // In the ISD, check for other children: - + std::vector rewrite = {e->id(), child->id()}; for(size_t isdElemId : ISD) { if(isdElemId == child->id()) continue; @@ -765,13 +764,13 @@ namespace storm { if(rewrite.size() > 2 && rewrite.size() < children.size() - 1) { return rewrite; } - - } + + } } - } + } return {}; } - + template std::tuple, std::vector, std::vector> DFT::getSortedParentAndDependencyIds(size_t index) const { diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 9c077e2c4..587a28a7b 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -181,7 +181,7 @@ namespace storm { // Get number of choices in current state uint_fast64_t numberChoices = this->getTransitionMatrix().getRowGroupIndices()[state + 1] - this->getTransitionMatrix().getRowGroupIndices()[state]; if (isMarkovianState(state)) { - STORM_LOG_ASSERT(numberChoices == 1, "Wrong number of choices for markovian state."); + STORM_LOG_ASSERT(numberChoices == 1, "Wrong number of choices for Markovian state."); } if (numberChoices > 1) { STORM_LOG_ASSERT(isProbabilisticState(state), "State is not probabilistic."); @@ -211,7 +211,7 @@ namespace storm { storm::storage::FlexibleSparseMatrix flexibleMatrix(this->getTransitionMatrix()); storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(this->getTransitionMatrix().transpose()); storm::solver::stateelimination::StateEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions); - + for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { STORM_LOG_ASSERT(!this->isHybridState(state), "State is hybrid."); if (this->isProbabilisticState(state)) { @@ -220,7 +220,7 @@ namespace storm { STORM_LOG_TRACE("Flexible matrix after eliminating state " << state << ":" << std::endl << flexibleMatrix); } } - + // Create the rate matrix for the CTMC storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, false); // Remember state to keep @@ -230,7 +230,7 @@ namespace storm { // State is eliminated and can be discarded keepStates.set(state, false); } else { - STORM_LOG_ASSERT(this->isMarkovianState(state), "State is not markovian."); + STORM_LOG_ASSERT(this->isMarkovianState(state), "State is not Markovian."); // Copy transitions for (uint_fast64_t row = flexibleMatrix.getRowGroupIndices()[state]; row < flexibleMatrix.getRowGroupIndices()[state + 1]; ++row) { for (auto const& entry : flexibleMatrix.getRow(row)) { @@ -240,20 +240,20 @@ namespace storm { } } } - + storm::storage::SparseMatrix rateMatrix = transitionMatrixBuilder.build(); rateMatrix = rateMatrix.getSubmatrix(false, keepStates, keepStates, false); STORM_LOG_TRACE("New CTMC matrix:" << std::endl << rateMatrix); // Construct CTMC storm::models::sparse::StateLabeling stateLabeling = this->getStateLabeling().getSubLabeling(keepStates); - + //TODO update reward models and choice labels according to kept states STORM_LOG_WARN_COND(this->getRewardModels().empty(), "Conversion of MA to CTMC does not preserve rewards."); std::unordered_map rewardModels = this->getRewardModels(); STORM_LOG_WARN_COND(!this->hasChoiceLabeling(), "Conversion of MA to CTMC does not preserve choice labels."); STORM_LOG_WARN_COND(!this->hasStateValuations(), "Conversion of MA to CTMC does not preserve choice labels."); STORM_LOG_WARN_COND(!this->hasChoiceOrigins(), "Conversion of MA to CTMC does not preserve choice labels."); - + return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels)); } diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index 9953a4108..ec29cbe1e 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -73,7 +73,7 @@ namespace storm { } if(rewardModelEntry.second.hasStateRewards()) { - os << rewardModelEntry.second.getStateRewardVector().at(group); + os << storm::utility::to_string(rewardModelEntry.second.getStateRewardVector().at(group)); } else { os << "0"; }