From bba69684c98ed80b9efbf4bbd1eaa4ffeb34086c Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 16 Sep 2016 13:31:50 +0200 Subject: [PATCH] reworked explicit Markov automaton generation a bit Former-commit-id: 1ca8c9e82839a95b456aec3d83c354323ab0c646 [formerly 05ef68fdeb08ebe0e779b705ee649955e872c90b] Former-commit-id: c0f5830754c2da5707038edf95f3078a36c28f98 --- src/builder/ExplicitModelBuilder.cpp | 65 +++++-------------- src/builder/ExplicitModelBuilder.h | 6 +- src/generator/Choice.cpp | 35 +++++++++++ src/generator/Choice.h | 7 ++- src/generator/JaniNextStateGenerator.cpp | 13 +++- src/generator/NextStateGenerator.cpp | 40 ++++++++++++ src/generator/NextStateGenerator.h | 4 +- src/generator/PrismNextStateGenerator.cpp | 2 + src/generator/StateBehavior.cpp | 10 +++ src/generator/StateBehavior.h | 10 +++ src/storage/BitVector.cpp | 9 ++- src/storage/BitVector.h | 2 +- src/storage/Distribution.cpp | 7 +++ src/storage/Distribution.h | 12 ++-- src/storage/SparseMatrix.cpp | 76 ++++++++++++++--------- 15 files changed, 200 insertions(+), 98 deletions(-) diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index 8d2164f9f..42321169f 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -169,16 +169,16 @@ namespace storm { } template - void ExplicitModelBuilder::buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional>>& choiceLabels , boost::optional& markovianChoices) { + void ExplicitModelBuilder::buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional>>& choiceLabels, boost::optional& markovianStates) { // Create choice labels, if requested, if (generator->getOptions().isBuildChoiceLabelsSet()) { choiceLabels = std::vector>(); } - // Create markovian states bit vector, if required + // Create markovian states bit vector, if required. if (generator->getModelType() == storm::generator::ModelType::MA) { - // The BitVector will be resized when the correct size is known - markovianChoices = storm::storage::BitVector(); + // The bit vector will be resized when the correct size is known. + markovianStates = storm::storage::BitVector(1000); } // Create a callback for the next-state generator to enable it to request the index of states. @@ -229,9 +229,9 @@ namespace storm { choiceLabels.get().push_back(boost::container::flat_set()); } - if (generator->getModelType() == storm::generator::ModelType::MA) { - markovianChoices->enlargeLiberally(currentRow+1, false); - markovianChoices->set(currentRow); + if (markovianStates) { + markovianStates.get().grow(currentRowGroup + 1, false); + markovianStates.get().set(currentRowGroup); } if (!generator->isDeterministicModel()) { @@ -278,9 +278,9 @@ namespace storm { } // If we keep track of the Markovian choices, store whether the current one is Markovian. - if( markovianChoices && choice.isMarkovian() ) { - markovianChoices->enlargeLiberally(currentRow+1, false); - markovianChoices->set(currentRow); + if (markovianStates && choice.isMarkovian()) { + markovianStates.get().grow(currentRowGroup + 1, false); + markovianStates.get().set(currentRowGroup); } // Add the probabilistic behavior to the matrix. @@ -302,9 +302,9 @@ namespace storm { } } - if (markovianChoices) { - // We now know the correct size - markovianChoices->resize(currentRow, false); + if (markovianStates) { + // Since we now know the correct size, cut the bit vector to the correct length. + markovianStates->resize(currentRowGroup, false); } // If the exploration order was not breadth-first, we need to fix the entries in the matrix according to @@ -348,9 +348,9 @@ namespace storm { } boost::optional markovianChoices; - buildMatrices(transitionMatrixBuilder, rewardModelBuilders, modelComponents.choiceLabeling, markovianChoices); + buildMatrices(transitionMatrixBuilder, rewardModelBuilders, modelComponents.choiceLabeling, modelComponents.markovianStates); modelComponents.transitionMatrix = transitionMatrixBuilder.build(); - + // Now finalize all reward models. for (auto& rewardModelBuilder : rewardModelBuilders) { modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount())); @@ -367,44 +367,9 @@ namespace storm { } } - if (generator->getModelType() == storm::generator::ModelType::MA) { - STORM_LOG_ASSERT(markovianChoices, "No information regarding markovian choices available."); - buildMarkovianStates(modelComponents, *markovianChoices); - } - return modelComponents; } - template - void ExplicitModelBuilder::buildMarkovianStates(ModelComponents& modelComponents, storm::storage::BitVector const& markovianChoices) const { - modelComponents.markovianStates = storm::storage::BitVector(modelComponents.transitionMatrix.getRowGroupCount(), false); - // Check for each state whether it contains a markovian choice. - for (uint_fast64_t state = 0; state < modelComponents.transitionMatrix.getRowGroupCount(); ++state ) { - uint_fast64_t firstChoice = modelComponents.transitionMatrix.getRowGroupIndices()[state]; - uint_fast64_t markovianChoice = markovianChoices.getNextSetIndex(firstChoice); - if (markovianChoice < modelComponents.transitionMatrix.getRowGroupIndices()[state+1]) { - // Found a markovian choice. Assert that there is not a second one. - STORM_LOG_THROW(markovianChoices.getNextSetIndex(markovianChoice+1) >= modelComponents.transitionMatrix.getRowGroupIndices()[state+1], storm::exceptions::WrongFormatException, "Multiple Markovian choices defined for some state"); - modelComponents.markovianStates->set(state); - // Swap the first choice and the found markovian choice (if they are not equal) - if (firstChoice != markovianChoice) { - modelComponents.transitionMatrix.swapRows(firstChoice, markovianChoice); - for (auto& rewardModel : modelComponents.rewardModels) { - if (rewardModel.second.hasStateActionRewards()) { - std::swap(rewardModel.second.getStateActionRewardVector()[firstChoice], rewardModel.second.getStateActionRewardVector()[markovianChoice]); - } - if (rewardModel.second.hasTransitionRewards()) { - rewardModel.second.getTransitionRewardMatrix().swapRows(firstChoice, markovianChoice); - } - } - if (modelComponents.choiceLabeling) { - std::swap(modelComponents.choiceLabeling.get()[firstChoice], modelComponents.choiceLabeling.get()[markovianChoice]); - } - } - } - } - } - template storm::models::sparse::StateLabeling ExplicitModelBuilder::buildStateLabeling() { return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices); diff --git a/src/builder/ExplicitModelBuilder.h b/src/builder/ExplicitModelBuilder.h index bb404f088..83ca54f6c 100644 --- a/src/builder/ExplicitModelBuilder.h +++ b/src/builder/ExplicitModelBuilder.h @@ -1,5 +1,5 @@ -#ifndef STORM_BUILDER_ExplicitModelBuilder_H -#define STORM_BUILDER_ExplicitModelBuilder_H +#ifndef STORM_BUILDER_EXPLICITMODELBUILDER_H +#define STORM_BUILDER_EXPLICITMODELBUILDER_H #include #include @@ -195,4 +195,4 @@ namespace storm { } // namespace adapters } // namespace storm -#endif /* STORM_BUILDER_ExplicitModelBuilder_H */ +#endif /* STORM_BUILDER_EXPLICITMODELBUILDER_H */ diff --git a/src/generator/Choice.cpp b/src/generator/Choice.cpp index 4337fffd4..151716340 100644 --- a/src/generator/Choice.cpp +++ b/src/generator/Choice.cpp @@ -4,6 +4,9 @@ #include "src/utility/constants.h" +#include "src/utility/macros.h" +#include "src/exceptions/InvalidOperationException.h" + namespace storm { namespace generator { @@ -12,6 +15,38 @@ namespace storm { // Intentionally left empty. } + template + void Choice::add(Choice const& other) { + STORM_LOG_THROW(this->markovian == other.markovian, storm::exceptions::InvalidOperationException, "Type of choices do not match."); + STORM_LOG_THROW(this->actionIndex == other.actionIndex, storm::exceptions::InvalidOperationException, "Action index of choices do not match."); + STORM_LOG_THROW(this->rewards.size() == other.rewards.size(), storm::exceptions::InvalidOperationException, "Reward value sizes of choices do not match."); + + // Add the elements to the distribution. + this->distribution.add(other.distribution); + + // Update the total mass of the choice. + this->totalMass += other.totalMass; + + // Add all reward values. + auto otherRewIt = other.rewards.begin(); + for (auto& rewardValue : this->rewards) { + rewardValue += *otherRewIt; + } + + // Join label sets. + if (this->labels) { + if (other.labels) { + LabelSet newLabelSet; + std::set_union(this->labels.get().begin(), this->labels.get().end(), other.labels.get().begin(), other.labels.get().end(), std::inserter(newLabelSet, newLabelSet.begin())); + this->labels = std::move(newLabelSet); + } + } else { + if (other.labels) { + this->labels = std::move(other.labels); + } + } + } + template typename storm::storage::Distribution::iterator Choice::begin() { return distribution.begin(); diff --git a/src/generator/Choice.h b/src/generator/Choice.h index bd20af0f0..ca4e9e748 100644 --- a/src/generator/Choice.h +++ b/src/generator/Choice.h @@ -25,6 +25,11 @@ namespace storm { Choice(Choice&& other) = default; Choice& operator=(Choice&& other) = default; + /*! + * Adds the given choice to the current one. + */ + void add(Choice const& other); + /*! * Returns an iterator to the distribution associated with this choice. * @@ -152,4 +157,4 @@ namespace storm { } } -#endif /* STORM_GENERATOR_CHOICE_H_ */ \ No newline at end of file +#endif /* STORM_GENERATOR_CHOICE_H_ */ diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 0df974f3b..b3f8f6561 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -264,6 +264,7 @@ namespace storm { } // Get all choices for the state. + result.setExpanded(); std::vector> allChoices = getSilentActionChoices(locations, *this->state, stateToIdCallback); std::vector> allLabeledChoices = getNonsilentActionChoices(locations, *this->state, stateToIdCallback); for (auto& choice : allLabeledChoices) { @@ -323,7 +324,8 @@ namespace storm { result.addChoice(std::move(choice)); } - result.setExpanded(); + this->postprocess(result); + return result; } @@ -348,7 +350,13 @@ namespace storm { continue; } - result.push_back(Choice(edge.getActionIndex())); + // Determine the exit rate if it's a Markovian edge. + boost::optional exitRate; + if (edge.hasRate()) { + exitRate = this->evaluator.asRational(edge.getRate()); + } + + result.push_back(Choice(edge.getActionIndex(), static_cast(exitRate))); Choice& choice = result.back(); // Iterate over all updates of the current command. @@ -360,6 +368,7 @@ namespace storm { // Update the choice by adding the probability/target state to it. ValueType probability = this->evaluator.asRational(destination.getProbability()); + probability = exitRate ? exitRate.get() * probability : probability; choice.addProbability(stateIndex, probability); probabilitySum += probability; } diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp index fccf7b783..a7fa2a044 100644 --- a/src/generator/NextStateGenerator.cpp +++ b/src/generator/NextStateGenerator.cpp @@ -309,6 +309,46 @@ namespace storm { return result; } + template + void NextStateGenerator::postprocess(StateBehavior& result) { + // If the model we build is a Markov Automaton, we postprocess the choices to sum all Markovian choices + // and make the Markovian choice the very first one (if there is any). + bool foundPreviousMarkovianChoice = false; + if (this->getModelType() == ModelType::MA) { + uint64_t numberOfChoicesToDelete = 0; + + for (uint_fast64_t index = 0; index + numberOfChoicesToDelete < result.getNumberOfChoices();) { + Choice& choice = result.getChoices()[index]; + + if (choice.isMarkovian()) { + if (foundPreviousMarkovianChoice) { + // If there was a previous Markovian choice, we need to sum them. Note that we can assume + // that the previous Markovian choice is the very first one in the choices vector. + result.getChoices().front().add(choice); + + // Swap the choice to the end to indicate it can be removed. + std::swap(choice, result.getChoices().back()); + ++numberOfChoicesToDelete; + } else { + // If there is no previous Markovian choice, just move the Markovian choice to the front. + if (index != 0) { + std::swap(result.getChoices().front(), choice); + foundPreviousMarkovianChoice = true; + } + ++index; + } + } else { + ++index; + } + } + + // Finally remove the choices that were added to other Markovian choices. + if (numberOfChoicesToDelete > 0) { + result.getChoices().resize(result.getChoices().size() - numberOfChoicesToDelete); + } + } + } + template storm::expressions::SimpleValuation NextStateGenerator::toValuation(CompressedState const& state) const { return unpackStateIntoValuation(state, variableInformation, *expressionManager); diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index 553e7871d..b2989b256 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -196,6 +196,8 @@ namespace storm { */ storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices, std::vector> labelsAndExpressions); + void postprocess(StateBehavior& result); + /// The options to be used for next-state generation. NextStateGeneratorOptions options; @@ -220,4 +222,4 @@ namespace storm { } } -#endif /* STORM_GENERATOR_NEXTSTATEGENERATOR_H_ */ \ No newline at end of file +#endif /* STORM_GENERATOR_NEXTSTATEGENERATOR_H_ */ diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 6c24cd00b..94d7a0f0a 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -272,6 +272,8 @@ namespace storm { result.addChoice(std::move(choice)); } + this->postprocess(result); + return result; } diff --git a/src/generator/StateBehavior.cpp b/src/generator/StateBehavior.cpp index 8ad2c1e91..ecd770941 100644 --- a/src/generator/StateBehavior.cpp +++ b/src/generator/StateBehavior.cpp @@ -50,6 +50,16 @@ namespace storm { return choices.end(); } + template + std::vector> const& StateBehavior::getChoices() const { + return choices; + } + + template + std::vector>& StateBehavior::getChoices() { + return choices; + } + template std::vector const& StateBehavior::getStateRewards() const { return stateRewards; diff --git a/src/generator/StateBehavior.h b/src/generator/StateBehavior.h index 1082e9045..f6219c996 100644 --- a/src/generator/StateBehavior.h +++ b/src/generator/StateBehavior.h @@ -56,6 +56,16 @@ namespace storm { */ typename std::vector>::const_iterator end() const; + /*! + * Retrieves the vector of choices. + */ + std::vector> const& getChoices() const; + + /*! + * Retrieves the vector of choices. + */ + std::vector>& getChoices(); + /*! * Retrieves the list of state rewards under selected reward models. */ diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index d7676c973..c806b29da 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -253,11 +253,10 @@ namespace storm { } } - void BitVector::enlargeLiberally(uint_fast64_t minimumLength, bool init) { - if(minimumLength > this->size()) { - uint_fast64_t newLength = this->bucketCount(); - newLength = std::max(newLength, static_cast(1u)) << 6; - while(newLength < minimumLength) { + void BitVector::grow(uint_fast64_t minimumLength, bool init) { + if (minimumLength > bitCount) { + uint_fast64_t newLength = bitCount; + while (newLength < minimumLength) { newLength = newLength << 1; } resize(newLength, init); diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 6ae966379..c8b81709f 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -243,7 +243,7 @@ namespace storm { * @param minimumLength The minimum number of bits that the bit vector should hold. * @param init The truth value to which to initialize newly created bits. */ - void enlargeLiberally(uint_fast64_t minimumLength, bool init = false); + void grow(uint_fast64_t minimumLength, bool init = false); /*! * Performs a logical "and" with the given bit vector. In case the sizes of the bit vectors do not match, diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp index 78e4a477d..4c2816467 100644 --- a/src/storage/Distribution.cpp +++ b/src/storage/Distribution.cpp @@ -19,6 +19,13 @@ namespace storm { // Intentionally left empty. } + template + void Distribution::add(Distribution const& other) { + container_type newDistribution; + std::set_union(this->distribution.begin(), this->distribution.end(), other.distribution.begin(), other.distribution.end(), std::inserter(newDistribution, newDistribution.begin())); + this->distribution = std::move(newDistribution); + } + template bool Distribution::equals(Distribution const& other, storm::utility::ConstantsComparator const& comparator) const { // We need to check equality by ourselves, because we need to account for epsilon differences. diff --git a/src/storage/Distribution.h b/src/storage/Distribution.h index ba61f0fbd..88e008108 100644 --- a/src/storage/Distribution.h +++ b/src/storage/Distribution.h @@ -5,8 +5,6 @@ #include #include -#include "src/utility/OsDetection.h" - #include "src/storage/sparse/StateType.h" namespace storm { @@ -31,11 +29,13 @@ namespace storm { Distribution(Distribution const& other) = default; Distribution& operator=(Distribution const& other) = default; - -#ifndef WINDOWS Distribution(Distribution&& other) = default; Distribution& operator=(Distribution&& other) = default; -#endif + + /*! + * Adds the given distribution to the current one. + */ + void add(Distribution const& other); /*! * Checks whether the two distributions specify the same probabilities to go to the same states. @@ -154,4 +154,4 @@ namespace std { } -#endif /* STORM_STORAGE_DISTRIBUTION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_DISTRIBUTION_H_ */ diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 3d1e16796..401fc4082 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -660,64 +660,82 @@ namespace storm { template void SparseMatrix::swapRows(index_type const& row1, index_type const& row2) { - if(row1==row2) { + if (row1 == row2) { return; } - // Get the index of the row that has more / less entries than the other + // Get the index of the row that has more / less entries than the other. index_type largerRow = getRow(row1).getNumberOfEntries() > getRow(row2).getNumberOfEntries() ? row1 : row2; index_type smallerRow = largerRow == row1 ? row2 : row1; index_type rowSizeDifference = getRow(largerRow).getNumberOfEntries() - getRow(smallerRow).getNumberOfEntries(); - // Save contents of larger row - std::vector> largerRowContents(getRow(largerRow).begin(), getRow(largerRow).end()); - if(largerRow < smallerRow) { - auto writeIt = getRows(largerRow, smallerRow+1).begin(); - // write smaller row in its new position - for(auto& smallerRowEntry : getRow(smallerRow)) { + // Save contents of larger row. + auto copyRow = getRow(largerRow); + std::vector> largerRowContents(copyRow.begin(), copyRow.end()); + + if (largerRow < smallerRow) { + auto writeIt = getRows(largerRow, smallerRow + 1).begin(); + + // Write smaller row to its new position. + for (auto& smallerRowEntry : getRow(smallerRow)) { *writeIt = std::move(smallerRowEntry); ++writeIt; } - if(!storm::utility::isZero(rowSizeDifference)) { - // write the intermediate rows into their correct position - for(auto& intermediateRowEntry : getRows(largerRow+1, smallerRow)) { + + // Write the intermediate rows into their correct position. + if (!storm::utility::isZero(rowSizeDifference)) { + for (auto& intermediateRowEntry : getRows(largerRow + 1, smallerRow)) { *writeIt = std::move(intermediateRowEntry); ++writeIt; } } - // write the larger row - for(auto& largerRowEntry : largerRowContents) { + + // Write the larger row to its new position. + for (auto& largerRowEntry : largerRowContents) { *writeIt = std::move(largerRowEntry); ++writeIt; } - STORM_LOG_ASSERT(writeIt == getRow(smallerRow).end(), "Unexpected position of write iterator"); - //Update row indications - for(index_type row = largerRow +1; row <= smallerRow; ++row) { - rowIndications[row] -= rowSizeDifference; + + STORM_LOG_ASSERT(writeIt == getRow(smallerRow).end(), "Unexpected position of write iterator."); + + // Update the row indications to account for the shift of indices at where the rows now start. + if (!storm::utility::isZero(rowSizeDifference)) { + for (index_type row = largerRow + 1; row <= smallerRow; ++row) { + rowIndications[row] -= rowSizeDifference; + } } } else { - auto writeIt = getRows(smallerRow, largerRow+1).end() -1; - // write smaller row in its new position - for(auto smallerRowEntryIt = getRow(smallerRow).end() -1; smallerRowEntryIt != getRow(smallerRow).begin()-1; --smallerRowEntryIt) { + auto writeIt = getRows(smallerRow, largerRow + 1).end() - 1; + + // Write smaller row to its new position + auto copyRow = getRow(smallerRow); + for (auto smallerRowEntryIt = copyRow.end() - 1; smallerRowEntryIt != copyRow.begin() - 1; --smallerRowEntryIt) { *writeIt = std::move(*smallerRowEntryIt); --writeIt; } - if(!storm::utility::isZero(rowSizeDifference)) { - // write the intermediate rows into their correct position - for(auto intermediateRowEntryIt = getRows(smallerRow+1, largerRow).end() -1; intermediateRowEntryIt != getRows(smallerRow+1, largerRow).begin()-1; --intermediateRowEntryIt) { + + // Write the intermediate rows into their correct position. + if (!storm::utility::isZero(rowSizeDifference)) { + for (auto intermediateRowEntryIt = getRows(smallerRow + 1, largerRow).end() - 1; intermediateRowEntryIt != getRows(smallerRow + 1, largerRow).begin() - 1; --intermediateRowEntryIt) { *writeIt = std::move(*intermediateRowEntryIt); --writeIt; } } - // write the larger row - for(auto largerRowEntryIt = largerRowContents.rbegin(); largerRowEntryIt != largerRowContents.rend(); ++largerRowEntryIt) { + + // Write the larger row to its new position. + for (auto largerRowEntryIt = largerRowContents.rbegin(); largerRowEntryIt != largerRowContents.rend(); ++largerRowEntryIt) { *writeIt = std::move(*largerRowEntryIt); --writeIt; } - STORM_LOG_ASSERT(writeIt == getRow(smallerRow).begin()-1, "Unexpected position of write iterator"); - //Update row indications - for(index_type row = smallerRow +1; row <= largerRow; ++row) { - rowIndications[row] += rowSizeDifference; + + STORM_LOG_ASSERT(writeIt == getRow(smallerRow).begin() - 1, "Unexpected position of write iterator."); + + // Update row indications. + // Update the row indications to account for the shift of indices at where the rows now start. + if (!storm::utility::isZero(rowSizeDifference)) { + for (index_type row = smallerRow + 1; row <= largerRow; ++row) { + rowIndications[row] += rowSizeDifference; + } } } }