diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 6b597260e..090994bb9 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -1,10 +1,3 @@ -/* - * File: ExplicitModelAdapter.h - * Author: Christian Dehnert - * - * Created on March 15, 2013, 11:42 AM - */ - #ifndef STORM_ADAPTERS_EXPLICITMODELADAPTER_H #define STORM_ADAPTERS_EXPLICITMODELADAPTER_H @@ -13,12 +6,15 @@ #include #include #include +#include #include #include #include #include "src/storage/prism/Program.h" #include "src/storage/expressions/SimpleValuation.h" +#include "storm/storage/expressions/ExprTkEvaluator.h" +#include "src/storage/BitVectorHashMap.h" #include "src/utility/PrismUtility.h" #include "src/models/AbstractModel.h" #include "src/models/Dtmc.h" @@ -39,31 +35,60 @@ namespace storm { template class ExplicitModelAdapter { public: - typedef storm::expressions::SimpleValuation StateType; - typedef storm::expressions::SimpleValuationPointerHash StateHash; - typedef storm::expressions::SimpleValuationPointerCompare StateCompare; - typedef storm::expressions::SimpleValuationPointerLess StateLess; + typedef storm::storage::BitVector StateType; // A structure holding information about the reachable state space. struct StateInformation { - StateInformation() : reachableStates(), stateToIndexMap() { + StateInformation(uint64_t bitsPerState) : reachableStates(), stateToIndexMap(bitsPerState, 100000) { // Intentionally left empty. } - // A list of reachable states. - std::vector reachableStates; + // The number of bits of each state. + uint64_t bitsPerState; + + // A list of reachable states as indices in the stateToIndexMap. + std::vector reachableStates; - // A list of initial states. - std::vector initialStateIndices; + // A list of initial states in terms of their global indices. + std::vector initialStateIndices; - // A mapping from states to indices in the list of reachable states. - std::unordered_map stateToIndexMap; + // A mapping from reachable states to their indices. + storm::storage::BitVectorHashMap stateToIndexMap; }; // A structure storing information about the used variables of the program. struct VariableInformation { - // A mapping of (integer) variable to their lower/upper bounds. - std::map> variableToBoundsMap; + uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) { + auto const& booleanIndex = booleanVariableToIndexMap.find(variable); + if (booleanIndex != booleanVariableToIndexMap.end()) { + return std::get<2>(booleanVariables[booleanIndex]); + } + auto const& integerIndex = integerVariableToIndexMap.find(variable); + if (integerIndex != integerVariableToIndexMap.end()) { + return std::get<4>(integerVariables[integerIndex]); + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable."); + } + + uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) { + auto const& integerIndex = integerVariableToIndexMap.find(variable); + if (integerIndex != integerVariableToIndexMap.end()) { + return std::get<5>(integerVariables[integerIndex]); + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable."); + } + + std::map booleanVariableToIndexMap; + + // The list of boolean variables. Along with the variable we store its initial value and bit offset in + // the state. + std::vector> booleanVariables; + + std::map integerVariableToIndexMap; + + // The list of integer variables. Along with the variable, we store its initial value, lower and upper + // bound, the bit offset in the state and the bit width. + std::vector> integerVariables; }; // A structure holding the individual components of a model. @@ -149,6 +174,20 @@ namespace storm { } private: + void unpackState(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExprTkEvaluator& evaluator) { + for (auto const& booleanVariable : variableInformation.booleanVariables) { + if (currentState.get(std::get<2>(booleanVariable))) { + evaluator.setBoolean(std::get<0>(booleanVariable), true); + } else { + evaluator.setBooleanValue(std::get<0>(booleanVariable), false); + } + } + for (auto const& integerVariable : variableInformation.integerVariables) { + int_fast64_t value = currentState.getAsInt(std::get<4>(integerVariable), std::get<5>(integerVariable)); + evaluator.setIntegerValue(std::get<0>(integerVariable), value); + } + } + /*! * Applies an update to the given state and returns the resulting new state object. This methods does not * modify the given state but returns a new one. @@ -201,20 +240,18 @@ namespace storm { * @param stateInformation The information about the already explored part of the reachable state space. * @return A pair indicating whether the state was already discovered before and the state id of the state. */ - static std::pair getOrAddStateIndex(StateType* state, StateInformation& stateInformation) { + static uint32_t getOrAddStateIndex(StateType const& state, StateInformation& stateInformation, std::queue& stateQueue) { + uint32_t newIndex = stateInformation.reachableStates.size(); + // Check, if the state was already registered. - auto indexIt = stateInformation.stateToIndexMap.find(state); - - if (indexIt == stateInformation.stateToIndexMap.end()) { - // The state has not been seen, yet, so add it to the list of all reachable states. - stateInformation.stateToIndexMap[state] = stateInformation.reachableStates.size(); - stateInformation.reachableStates.push_back(state); - return std::make_pair(false, stateInformation.stateToIndexMap[state]); - } else { - // The state was already encountered. Delete the copy of the old state and return its index. - delete state; - return std::make_pair(true, indexIt->second); + std::pair actualIndexBucketPair = stateInformation.stateToIndexMap.findOrAdd(state, newIndex); + + if (actualIndexBucketPair.first == newIndex) { + stateQueue.insert(actualIndexBucketPair.second); + reachableStates.push_back(actualIndexBucketPair.second); } + + return actualIndexBucketPair.first; } /*! @@ -476,33 +513,36 @@ namespace storm { std::vector> choiceLabels; // Initialize a queue and insert the initial state. - std::queue stateQueue; - StateType* initialState = new StateType(program.getManager().getSharedPointer()); + std::queue stateQueue; + StateType initialState(stateInformation.bitsPerState); // We need to initialize the values of the variables to their initial value. - for (auto const& booleanVariable : program.getGlobalBooleanVariables()) { - initialState->setBooleanValue(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool()); + for (auto const& booleanVariable : variableInformation.booleanVariables) { + initialState.set(std::get<2>(booleanVariable), std::get<1>(booleanVariable)); } - for (auto const& integerVariable : program.getGlobalIntegerVariables()) { - initialState->setIntegerValue(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt()); + for (auto const& integerVariable : variableInformation.integerVariables) { + initialState.set(std::get<4>(integerVariable), std::get<5>(integerVariable), std::get<1>(integerVariable) - std::get<2>(integerVariable)); } for (auto const& module : program.getModules()) { for (auto const& booleanVariable : module.getBooleanVariables()) { - initialState->setBooleanValue(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool()); + initialState.set(std::get<2>(booleanVariable), std::get<1>(booleanVariable)); } for (auto const& integerVariable : module.getIntegerVariables()) { - initialState->setIntegerValue(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt()); + initialState.set(std::get<4>(integerVariable), std::get<5>(integerVariable), std::get<1>(integerVariable) - std::get<2>(integerVariable)); } } - std::pair addIndexPair = getOrAddStateIndex(initialState, stateInformation); - stateInformation.initialStateIndices.push_back(addIndexPair.second); - stateQueue.push(stateInformation.stateToIndexMap[initialState]); + // Insert the initial state in the global state to index mapping and state queue. + getOrAddStateIndex(initialState, stateInformation, stateQueue); // Now explore the current state until there is no more reachable state. uint_fast64_t currentRow = 0; + storm::expressions::ExprTkEvaluator evaluator(program.getManager()); while (!stateQueue.empty()) { - uint_fast64_t currentState = stateQueue.front(); + // Get the current state and unpack it. + std::size_t currentStateIndex = stateQueue.front(); + storm::storage::BitVector currentState = stateInformation.stateToIndexMap.getBucket(currentStateIndex); + unpackState(currentState, variableInformation, evaluator); // Retrieve all choices for the current state. std::vector> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue); @@ -651,18 +691,40 @@ namespace storm { static ModelComponents buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel) { ModelComponents modelComponents; + uint_fast64_t bitOffset = 0; VariableInformation variableInformation; + for (auto const& booleanVariable : program.getGlobalBooleanVariables()) { + variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset); + ++bitOffset; + booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1; + } for (auto const& integerVariable : program.getGlobalIntegerVariables()) { - variableInformation.variableToBoundsMap[integerVariable.getName()] = std::make_pair(integerVariable.getLowerBoundExpression().evaluateAsInt(), integerVariable.getUpperBoundExpression().evaluateAsInt()); + int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); + int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound))); + variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth); + bitOffset += bitwidth; + integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1; } for (auto const& module : program.getModules()) { + for (auto const& booleanVariable : module.getBooleanVariables()) { + variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset); + ++bitOffset; + booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1; + } for (auto const& integerVariable : module.getIntegerVariables()) { - variableInformation.variableToBoundsMap[integerVariable.getName()] = std::make_pair(integerVariable.getLowerBoundExpression().evaluateAsInt(), integerVariable.getUpperBoundExpression().evaluateAsInt()); + int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); + int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound))); + variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth); + bitOffset += bitwidth; + integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1; } } // Create the structure for storing the reachable state space. - StateInformation stateInformation; + uint64_t bitsPerState = ((bitOffset / 64) + 1) * 64; + StateInformation stateInformation(bitsPerState); // Determine whether we have to combine different choices to one or whether this model can have more than // one choice per state. diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 238237087..4f568e2bb 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -397,7 +397,7 @@ namespace storm { } } - storm::storage::BitVector BitVector::get(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) { + storm::storage::BitVector BitVector::get(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) const { uint64_t numberOfBuckets = numberOfBits >> 6; uint64_t index = bitIndex >> 6; STORM_LOG_ASSERT(index + numberOfBuckets <= this->bucketCount(), "Argument is out-of-range."); @@ -408,6 +408,34 @@ namespace storm { return result; } + uint_fast64_t BitVector::getAsInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) const { + uint64_t bucket = bitIndex >> 6; + uint64_t bitIndexInBucket = bitIndex & mod64mask; + + uint64_t mask = (1ull << (64 - bitIndexInBucket + 1)) - 1; + + if (bitIndexInBucket + numberOfBits < 64) { + // If the value stops before the end of the bucket, we need to erase some lower bits. + mask &= !((1ull << (64 - (bitIndexInBucket - numberOfBits + 1))) - 1); + return bucketVector[bucket] & mask; + } else if (bitIndexInBucket + numberOfBits > 64) { + // In this case, the integer "crosses" the bucket line. + uint64_t result = bucketVector[bucket] & mask; + result <<= (64 - bitIndexInBucket); + + ++bucket; + numberOfBits -= (64 - bitIndexInBucket); + mask = !(1ull << (64 - numberOfBits)); + uint64_t lowerBits = bucketVector[bucket] & mask; + result |= (lowerBits >> (64 - numberOfBits)); + + return result; + } else { + // In this case, it suffices to take the current mask. + return bucketVector[bucket] & mask; + } + } + bool BitVector::empty() const { for (auto& element : bucketVector) { if (element != 0) { diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index 27779ea81..d8fc7e51a 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -347,7 +347,16 @@ namespace storm { * @param numberOfBits The number of bits to get. This value must be a multiple of 64. * @return A new bit vector holding the selected bits. */ - storm::storage::BitVector get(uint_fast64_t bitIndex, uint_fast64_t numberOfBits); + storm::storage::BitVector get(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) const; + + /*! + * Retrieves the content of the current bit vector at the given index for the given number of bits as an + * unsigned integer value. + * + * @param bitIndex The index of the first bit to get. + * @param numberOfBits The number of bits to get. This value must be less or equal than 64. + */ + uint_fast64_t getAsInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) const; /*! * Retrieves whether no bits are set to true in this bit vector. diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp index 0b4ab22ac..c40588125 100644 --- a/src/storage/BitVectorHashMap.cpp +++ b/src/storage/BitVectorHashMap.cpp @@ -55,7 +55,7 @@ namespace storm { } template - ValueType BitVectorHashMap::findOrAdd(storm::storage::BitVector const& key, ValueType value) { + std::pair BitVectorHashMap::findOrAdd(storm::storage::BitVector const& key, ValueType value) { // If the load of the map is too high, we increase the size. if (numberOfElements >= loadFactor * *currentSizeIterator) { this->increaseSize(); @@ -66,7 +66,7 @@ namespace storm { while (isBucketOccupied(bucket)) { if (buckets.matches(bucket * bucketSize, key)) { - return values[bucket]; + return std::make_pair(values[bucket], bucket); } bucket += hasher2(key); bucket %= *currentSizeIterator; @@ -84,7 +84,12 @@ namespace storm { occupied.set(bucket); values[bucket] = value; ++numberOfElements; - return value; + return std::make_pair(value, bucket); + } + + template + storm::storage::BitVector BitVectorHashMap::getBucket(std::size_t bucket) const { + return buckets.get(bucket * bucketSize, bucketSize); } template class BitVectorHashMap; diff --git a/src/storage/BitVectorHashMap.h b/src/storage/BitVectorHashMap.h index a6894219a..aac31a183 100644 --- a/src/storage/BitVectorHashMap.h +++ b/src/storage/BitVectorHashMap.h @@ -35,7 +35,15 @@ namespace storm { * @param value The value that is inserted if the key is not already found in the map. * @return The found value if the key is already contained in the map and the provided new value otherwise. */ - ValueType findOrAdd(storm::storage::BitVector const& key, ValueType value); + std::pair findOrAdd(storm::storage::BitVector const& key, ValueType value); + + /*! + * Retrieves the key stored in the given bucket (if any). + * + * @param bucket The index of the bucket. + * @return The content of the named bucket. + */ + storm::storage::BitVector getBucket(std::size_t bucket) const; /*! * Retrieves the size of the map in terms of the number of key-value pairs it stores. diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp index c6cb4fcfb..0dcb42e06 100644 --- a/src/storage/prism/Update.cpp +++ b/src/storage/prism/Update.cpp @@ -5,6 +5,7 @@ namespace storm { namespace prism { Update::Update(uint_fast64_t globalIndex, storm::expressions::Expression const& likelihoodExpression, std::vector const& assignments, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), likelihoodExpression(likelihoodExpression), assignments(assignments), variableToAssignmentIndexMap(), globalIndex(globalIndex) { + std::sort(assignments.begin(), assignments.end(), [] (storm::prism::Assignment const& assignment1, storm::prism::Assignment const& assignment2) { return assignment1.getVariable() < assignment2.getVariable(); } ); this->createAssignmentMapping(); }