Browse Source

reworked explicit Markov automaton generation a bit

Former-commit-id: 1ca8c9e828 [formerly 05ef68fdeb]
Former-commit-id: c0f5830754
main
dehnert 9 years ago
parent
commit
bba69684c9
  1. 65
      src/builder/ExplicitModelBuilder.cpp
  2. 6
      src/builder/ExplicitModelBuilder.h
  3. 35
      src/generator/Choice.cpp
  4. 7
      src/generator/Choice.h
  5. 13
      src/generator/JaniNextStateGenerator.cpp
  6. 40
      src/generator/NextStateGenerator.cpp
  7. 4
      src/generator/NextStateGenerator.h
  8. 2
      src/generator/PrismNextStateGenerator.cpp
  9. 10
      src/generator/StateBehavior.cpp
  10. 10
      src/generator/StateBehavior.h
  11. 9
      src/storage/BitVector.cpp
  12. 2
      src/storage/BitVector.h
  13. 7
      src/storage/Distribution.cpp
  14. 12
      src/storage/Distribution.h
  15. 76
      src/storage/SparseMatrix.cpp

65
src/builder/ExplicitModelBuilder.cpp

@ -169,16 +169,16 @@ namespace storm {
}
template <typename ValueType, typename RewardModelType, typename StateType>
void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>& choiceLabels , boost::optional<storm::storage::BitVector>& markovianChoices) {
void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildMatrices(storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<typename RewardModelType::ValueType>>& rewardModelBuilders, boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>& choiceLabels, boost::optional<storm::storage::BitVector>& markovianStates) {
// Create choice labels, if requested,
if (generator->getOptions().isBuildChoiceLabelsSet()) {
choiceLabels = std::vector<boost::container::flat_set<uint_fast64_t>>();
}
// 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<uint_fast64_t>());
}
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<storm::storage::BitVector> 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 <typename ValueType, typename RewardModelType, typename StateType>
void ExplicitModelBuilder<ValueType, RewardModelType, StateType>::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 <typename ValueType, typename RewardModelType, typename StateType>
storm::models::sparse::StateLabeling ExplicitModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling() {
return generator->label(stateStorage.stateToId, stateStorage.initialStateIndices, stateStorage.deadlockStateIndices);

6
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 <memory>
#include <utility>
@ -195,4 +195,4 @@ namespace storm {
} // namespace adapters
} // namespace storm
#endif /* STORM_BUILDER_ExplicitModelBuilder_H */
#endif /* STORM_BUILDER_EXPLICITMODELBUILDER_H */

35
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<typename ValueType, typename StateType>
void Choice<ValueType, StateType>::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 ValueType, typename StateType>
typename storm::storage::Distribution<ValueType, StateType>::iterator Choice<ValueType, StateType>::begin() {
return distribution.begin();

7
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_ */
#endif /* STORM_GENERATOR_CHOICE_H_ */

13
src/generator/JaniNextStateGenerator.cpp

@ -264,6 +264,7 @@ namespace storm {
}
// Get all choices for the state.
result.setExpanded();
std::vector<Choice<ValueType>> allChoices = getSilentActionChoices(locations, *this->state, stateToIdCallback);
std::vector<Choice<ValueType>> 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<ValueType>(edge.getActionIndex()));
// Determine the exit rate if it's a Markovian edge.
boost::optional<ValueType> exitRate;
if (edge.hasRate()) {
exitRate = this->evaluator.asRational(edge.getRate());
}
result.push_back(Choice<ValueType>(edge.getActionIndex(), static_cast<bool>(exitRate)));
Choice<ValueType>& 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;
}

40
src/generator/NextStateGenerator.cpp

@ -309,6 +309,46 @@ namespace storm {
return result;
}
template<typename ValueType, typename StateType>
void NextStateGenerator<ValueType, StateType>::postprocess(StateBehavior<ValueType, StateType>& 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<ValueType>& 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<typename ValueType, typename StateType>
storm::expressions::SimpleValuation NextStateGenerator<ValueType, StateType>::toValuation(CompressedState const& state) const {
return unpackStateIntoValuation(state, variableInformation, *expressionManager);

4
src/generator/NextStateGenerator.h

@ -196,6 +196,8 @@ namespace storm {
*/
storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices, std::vector<std::pair<std::string, storm::expressions::Expression>> labelsAndExpressions);
void postprocess(StateBehavior<ValueType, StateType>& result);
/// The options to be used for next-state generation.
NextStateGeneratorOptions options;
@ -220,4 +222,4 @@ namespace storm {
}
}
#endif /* STORM_GENERATOR_NEXTSTATEGENERATOR_H_ */
#endif /* STORM_GENERATOR_NEXTSTATEGENERATOR_H_ */

2
src/generator/PrismNextStateGenerator.cpp

@ -272,6 +272,8 @@ namespace storm {
result.addChoice(std::move(choice));
}
this->postprocess(result);
return result;
}

10
src/generator/StateBehavior.cpp

@ -50,6 +50,16 @@ namespace storm {
return choices.end();
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType, StateType>> const& StateBehavior<ValueType, StateType>::getChoices() const {
return choices;
}
template<typename ValueType, typename StateType>
std::vector<Choice<ValueType, StateType>>& StateBehavior<ValueType, StateType>::getChoices() {
return choices;
}
template<typename ValueType, typename StateType>
std::vector<ValueType> const& StateBehavior<ValueType, StateType>::getStateRewards() const {
return stateRewards;

10
src/generator/StateBehavior.h

@ -56,6 +56,16 @@ namespace storm {
*/
typename std::vector<Choice<ValueType, StateType>>::const_iterator end() const;
/*!
* Retrieves the vector of choices.
*/
std::vector<Choice<ValueType, StateType>> const& getChoices() const;
/*!
* Retrieves the vector of choices.
*/
std::vector<Choice<ValueType, StateType>>& getChoices();
/*!
* Retrieves the list of state rewards under selected reward models.
*/

9
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<decltype(newLength)>(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);

2
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,

7
src/storage/Distribution.cpp

@ -19,6 +19,13 @@ namespace storm {
// Intentionally left empty.
}
template<typename ValueType, typename StateType>
void Distribution<ValueType, StateType>::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<typename ValueType, typename StateType>
bool Distribution<ValueType, StateType>::equals(Distribution<ValueType, StateType> const& other, storm::utility::ConstantsComparator<ValueType> const& comparator) const {
// We need to check equality by ourselves, because we need to account for epsilon differences.

12
src/storage/Distribution.h

@ -5,8 +5,6 @@
#include <ostream>
#include <boost/container/flat_map.hpp>
#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_ */
#endif /* STORM_STORAGE_DISTRIBUTION_H_ */

76
src/storage/SparseMatrix.cpp

@ -660,64 +660,82 @@ namespace storm {
template<typename ValueType>
void SparseMatrix<ValueType>::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<MatrixEntry<index_type, value_type>> 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<MatrixEntry<index_type, value_type>> 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;
}
}
}
}

Loading…
Cancel
Save