From 6f2916d557e2d367a6aa1bcfa33f6f837f2caf0c Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 14 Jan 2015 18:06:47 +0100 Subject: [PATCH] Adapted the explicit model generator to the new hash map. Surprise: doesn't work yet. Former-commit-id: dc60f568bfe6f13bced1d82687555e43c0fc3ef7 --- src/adapters/ExplicitModelAdapter.h | 266 ++++++++---------- src/storage/BitVector.cpp | 6 +- src/storage/BitVector.h | 6 +- src/storage/BitVectorHashMap.cpp | 47 ++-- src/storage/BitVectorHashMap.h | 25 +- src/storage/LabeledValues.h | 211 -------------- .../expressions/ExprtkExpressionEvaluator.cpp | 10 +- .../expressions/ExprtkExpressionEvaluator.h | 17 +- src/storage/expressions/Variable.cpp | 4 + src/storage/expressions/Variable.h | 8 + src/utility/PrismUtility.h | 37 +-- src/utility/constants.h | 28 -- 12 files changed, 206 insertions(+), 459 deletions(-) delete mode 100644 src/storage/LabeledValues.h diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 090994bb9..07620491b 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -13,7 +13,7 @@ #include "src/storage/prism/Program.h" #include "src/storage/expressions/SimpleValuation.h" -#include "storm/storage/expressions/ExprTkEvaluator.h" +#include "src/storage/expressions/ExprtkExpressionEvaluator.h" #include "src/storage/BitVectorHashMap.h" #include "src/utility/PrismUtility.h" #include "src/models/AbstractModel.h" @@ -58,37 +58,56 @@ namespace storm { // A structure storing information about the used variables of the program. struct VariableInformation { - uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) { + struct BooleanVariableInformation { + BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) { + // Intentionally left empty. + } + + storm::expressions::Variable variable; + bool initialValue; + uint_fast64_t bitOffset; + }; + + struct IntegerVariableInformation { + IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) { + // Intentionally left empty. + } + + storm::expressions::Variable variable; + int_fast64_t initialValue; + int_fast64_t lowerBound; + int_fast64_t upperBound; + uint_fast64_t bitOffset; + uint_fast64_t bitWidth; + }; + + uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const { auto const& booleanIndex = booleanVariableToIndexMap.find(variable); if (booleanIndex != booleanVariableToIndexMap.end()) { - return std::get<2>(booleanVariables[booleanIndex]); + return booleanVariables[booleanIndex].bitOffset; } auto const& integerIndex = integerVariableToIndexMap.find(variable); if (integerIndex != integerVariableToIndexMap.end()) { - return std::get<4>(integerVariables[integerIndex]); + return integerVariables[integerIndex].bitOffset; } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable."); } - uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) { + uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const { auto const& integerIndex = integerVariableToIndexMap.find(variable); if (integerIndex != integerVariableToIndexMap.end()) { - return std::get<5>(integerVariables[integerIndex]); + return integerVariables[integerIndex].bitWidth; } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable."); } + // The list of boolean variables. 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::vector booleanVariables; + // The list of integer variables. 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; + std::vector integerVariables; }; // A structure holding the individual components of a model. @@ -174,17 +193,12 @@ namespace storm { } private: - void unpackState(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExprTkEvaluator& evaluator) { + static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExprtkExpressionEvaluator& 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); - } + evaluator.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset)); } 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); + evaluator.setIntegerValue(integerVariable.variable, currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound); } } @@ -196,8 +210,8 @@ namespace storm { * @params update The update to apply. * @return The resulting state. */ - static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, storm::prism::Update const& update) { - return applyUpdate(variableInformation, state, state, update); + static StateType applyUpdate(VariableInformation const& variableInformation, StateType const& state, storm::prism::Update const& update, storm::expressions::ExprtkExpressionEvaluator const& evaluator) { + return applyUpdate(variableInformation, state, state, update, evaluator); } /*! @@ -210,23 +224,33 @@ namespace storm { * @param update The update to apply. * @return The resulting state. */ - static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, StateType const* baseState, storm::prism::Update const& update) { - StateType* newState = new StateType(*state); - - int_fast64_t newValue = 0; - for (auto const& assignment : update.getAssignments()) { - if (assignment.getExpression().hasBooleanType()) { - newState->setBooleanValue(assignment.getVariable(), assignment.getExpression().evaluateAsBool(baseState)); - } else if (assignment.getExpression().hasIntegerType()) { - newValue = assignment.getExpression().evaluateAsInt(baseState); - auto const& boundsPair = variableInformation.variableToBoundsMap.find(assignment.getVariableName()); - STORM_LOG_THROW(boundsPair->second.first <= newValue && newValue <= boundsPair->second.second, storm::exceptions::InvalidArgumentException, "Invalid value " << newValue << " for variable '" << assignment.getVariableName() << "'."); - newState->setIntegerValue(assignment.getVariable(), newValue); - } else { - STORM_LOG_ASSERT(false, "Invalid type '" << assignment.getExpression().getType() << "' of assignment."); + static StateType applyUpdate(VariableInformation const& variableInformation, StateType const& state, StateType const& baseState, storm::prism::Update const& update, storm::expressions::ExprtkExpressionEvaluator const& evaluator) { + StateType newState(state); + + auto assignmentIt = update.getAssignments().begin(); + auto assignmentIte = update.getAssignments().end(); + + // Iterate over all boolean assignments and carry them out. + auto boolIt = variableInformation.booleanVariables.begin(); + for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) { + while (assignmentIt->getVariable() != boolIt->variable) { + ++boolIt; } + newState.set(boolIt->bitOffset, evaluator.asBool(assignmentIt->getExpression())); } + // Iterate over all integer assignments and carry them out. + auto integerIt = variableInformation.integerVariables.begin(); + for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) { + while (assignmentIt->getVariable() != integerIt->variable) { + ++integerIt; + } + newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, evaluator.asInt(assignmentIt->getExpression()) - integerIt->lowerBound); + } + + // Check that we processed all assignments. + STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed."); + return newState; } @@ -244,11 +268,11 @@ namespace storm { uint32_t newIndex = stateInformation.reachableStates.size(); // Check, if the state was already registered. - std::pair actualIndexBucketPair = stateInformation.stateToIndexMap.findOrAdd(state, newIndex); + std::pair actualIndexBucketPair = stateInformation.stateToIndexMap.findOrAddAndGetBucket(state, newIndex); if (actualIndexBucketPair.first == newIndex) { - stateQueue.insert(actualIndexBucketPair.second); - reachableStates.push_back(actualIndexBucketPair.second); + stateQueue.push(actualIndexBucketPair.second); + stateInformation.reachableStates.push_back(actualIndexBucketPair.second); } return actualIndexBucketPair.first; @@ -270,7 +294,7 @@ namespace storm { * @param actionIndex The index of the action label to select. * @return A list of lists of active commands or nothing. */ - static boost::optional>>> getActiveCommandsByActionIndex(storm::prism::Program const& program, StateType const* state, uint_fast64_t const& actionIndex) { + static boost::optional>>> getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExprtkExpressionEvaluator const& evaluator, uint_fast64_t const& actionIndex) { boost::optional>>> result((std::vector>>())); // Iterate over all modules. @@ -295,7 +319,7 @@ namespace storm { // Look up commands by their indices and add them if the guard evaluates to true in the given state. for (uint_fast64_t commandIndex : commandIndices) { storm::prism::Command const& command = module.getCommand(commandIndex); - if (command.getGuardExpression().evaluateAsBool(state)) { + if (evaluator.asBool(command.getGuardExpression())) { commands.push_back(command); } } @@ -311,10 +335,8 @@ namespace storm { return result; } - static std::vector> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue) { + static std::vector> getUnlabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue) { std::vector> result; - - StateType const* currentState = stateInformation.reachableStates[stateIndex]; // Iterate over all modules. for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { @@ -328,7 +350,7 @@ namespace storm { if (command.isLabeled()) continue; // Skip the command, if it is not enabled. - if (!command.getGuardExpression().evaluateAsBool(currentState)) { + if (!evaluator.asBool(command.getGuardExpression())) { continue; } @@ -336,25 +358,17 @@ namespace storm { Choice& choice = result.back(); choice.addChoiceLabel(command.getGlobalIndex()); - double probabilitySum = 0; // Iterate over all updates of the current command. + double probabilitySum = 0; for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { storm::prism::Update const& update = command.getUpdate(k); - // Obtain target state index. - std::pair flagTargetStateIndexPair = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update), stateInformation); - - // If the state has not been discovered yet, add it to the queue of states to be explored. - if (!flagTargetStateIndexPair.first) { - stateQueue.push(flagTargetStateIndexPair.second); - } + // Obtain target state index and add it to the list of known states. If it has not yet been + // seen, we also add it to the set of states that have yet to be explored. + uint32_t stateIndex = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update, evaluator), stateInformation, stateQueue); // Update the choice by adding the probability/target state to it. - double probabilityToAdd = update.getLikelihoodExpression().evaluateAsDouble(currentState); - probabilitySum += probabilityToAdd; - boost::container::flat_set labels; - labels.insert(update.getGlobalIndex()); - addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityToAdd, labels); + choice.addProbability(stateIndex, evaluator.asDouble(update.getLikelihoodExpression())); } // Check that the resulting distribution is in fact a distribution. @@ -365,12 +379,11 @@ namespace storm { return result; } - static std::vector> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue) { + static std::vector> getLabeledTransitions(storm::prism::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, storm::expressions::ExprtkExpressionEvaluator const& evaluator, std::queue& stateQueue) { std::vector> result; for (uint_fast64_t actionIndex : program.getActionIndices()) { - StateType const* currentState = stateInformation.reachableStates[stateIndex]; - boost::optional>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, currentState, actionIndex); + boost::optional>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, evaluator, actionIndex); // Only process this action label, if there is at least one feasible solution. if (optionalActiveCommandLists) { @@ -385,9 +398,9 @@ namespace storm { // As long as there is one feasible combination of commands, keep on expanding it. bool done = false; while (!done) { - std::unordered_map, StateHash, StateCompare>* currentTargetStates = new std::unordered_map, StateHash, StateCompare>(); - std::unordered_map, StateHash, StateCompare>* newTargetStates = new std::unordered_map, StateHash, StateCompare>(); - (*currentTargetStates)[new StateType(*currentState)] = storm::storage::LabeledValues(1.0); + std::unordered_map* currentTargetStates = new std::unordered_map(); + std::unordered_map* newTargetStates = new std::unordered_map(); + currentTargetStates->emplace(currentState, storm::utility::one()); // FIXME: This does not check whether a global variable is written multiple times. While the // behaviour for this is undefined anyway, a warning should be issued in that case. @@ -398,40 +411,17 @@ namespace storm { storm::prism::Update const& update = command.getUpdate(j); for (auto const& stateProbabilityPair : *currentTargetStates) { - StateType* newTargetState = applyUpdate(variableInformation, stateProbabilityPair.first, currentState, update); - - storm::storage::LabeledValues newProbability; - - double updateProbability = update.getLikelihoodExpression().evaluateAsDouble(currentState); - for (auto const& valueLabelSetPair : stateProbabilityPair.second) { - // Copy the label set, so we can modify it. - boost::container::flat_set newLabelSet = valueLabelSetPair.second; - newLabelSet.insert(update.getGlobalIndex()); - - newProbability.addValue(valueLabelSetPair.first * updateProbability, newLabelSet); - } - - auto existingStateProbabilityPair = newTargetStates->find(newTargetState); - if (existingStateProbabilityPair == newTargetStates->end()) { - (*newTargetStates)[newTargetState] = newProbability; - } else { - existingStateProbabilityPair->second += newProbability; - - // If the state was already seen in one of the other updates, we need to delete this copy. - delete newTargetState; - } + // Compute the new state under the current update and add it to the set of new target states. + StateType newTargetState = applyUpdate(variableInformation, stateProbabilityPair.first, currentState, update, evaluator); + newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asDouble(update.getLikelihoodExpression())); } } // If there is one more command to come, shift the target states one time step back. if (i < iteratorList.size() - 1) { - for (auto const& stateProbabilityPair : *currentTargetStates) { - delete stateProbabilityPair.first; - } - delete currentTargetStates; currentTargetStates = newTargetStates; - newTargetStates = new std::unordered_map, StateHash, StateCompare>(); + newTargetStates = new std::unordered_map(); } } @@ -450,17 +440,8 @@ namespace storm { double probabilitySum = 0; for (auto const& stateProbabilityPair : *newTargetStates) { - std::pair flagTargetStateIndexPair = getOrAddStateIndex(stateProbabilityPair.first, stateInformation); - - // If the state has not been discovered yet, add it to the queue of states to be explored. - if (!flagTargetStateIndexPair.first) { - stateQueue.push(flagTargetStateIndexPair.second); - } - - for (auto const& probabilityLabelPair : stateProbabilityPair.second) { - addProbabilityToChoice(choice, flagTargetStateIndexPair.second, probabilityLabelPair.first, probabilityLabelPair.second); - probabilitySum += probabilityLabelPair.first; - } + uint32_t actualIndex = getOrAddStateIndex(stateProbabilityPair.first, stateInformation, stateQueue); + choice.addProbability(actualIndex, stateProbabilityPair.second); } // Check that the resulting distribution is in fact a distribution. @@ -518,18 +499,10 @@ namespace storm { // We need to initialize the values of the variables to their initial value. for (auto const& booleanVariable : variableInformation.booleanVariables) { - initialState.set(std::get<2>(booleanVariable), std::get<1>(booleanVariable)); + initialState.set(booleanVariable.bitOffset, booleanVariable.initialValue); } 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.set(std::get<2>(booleanVariable), std::get<1>(booleanVariable)); - } - for (auto const& integerVariable : module.getIntegerVariables()) { - initialState.set(std::get<4>(integerVariable), std::get<5>(integerVariable), std::get<1>(integerVariable) - std::get<2>(integerVariable)); - } + initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast(integerVariable.initialValue - integerVariable.lowerBound)); } // Insert the initial state in the global state to index mapping and state queue. @@ -537,16 +510,17 @@ namespace storm { // Now explore the current state until there is no more reachable state. uint_fast64_t currentRow = 0; - storm::expressions::ExprTkEvaluator evaluator(program.getManager()); + storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager()); while (!stateQueue.empty()) { // 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); + std::size_t currentStateBucket = stateQueue.front(); + std::pair stateValuePair = stateInformation.stateToIndexMap.getBucketAndValue(currentStateBucket); + storm::storage::BitVector const& currentState = stateValuePair.first; + unpackStateIntoEvaluator(currentState, variableInformation, evaluator); // Retrieve all choices for the current state. - std::vector> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue); - std::vector> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState, stateQueue); + std::vector> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState, evaluator, stateQueue); + std::vector> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState, evaluator, stateQueue); uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size(); @@ -556,7 +530,7 @@ namespace storm { if (!storm::settings::generalSettings().isDontFixDeadlocksSet()) { // Insert empty choice labeling for added self-loop transitions. choiceLabels.push_back(boost::container::flat_set()); - transitionMatrixBuilder.addNextValue(currentRow, currentState, storm::utility::constantOne()); + transitionMatrixBuilder.addNextValue(currentRow, stateValuePair.second, storm::utility::one()); ++currentRow; } else { LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); @@ -567,8 +541,7 @@ namespace storm { // or compose them to one choice. if (deterministicModel) { Choice globalChoice; - std::map stateToRewardMap; - boost::container::flat_set allChoiceLabels; + std::map stateToRewardMap; // Combine all the choices and scale them with the total number of choices of the current state. for (auto const& choice : allUnlabeledChoices) { @@ -578,8 +551,8 @@ namespace storm { // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { - if (!transitionReward.isLabeled() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) { - stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState))); + if (!transitionReward.isLabeled() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { + stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); } } } @@ -591,8 +564,8 @@ namespace storm { // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { - if (transitionReward.getActionIndex() == choice.getActionIndex() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) { - stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState))); + if (transitionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { + stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); } } } @@ -629,8 +602,8 @@ namespace storm { // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { - if (!transitionReward.isLabeled() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) { - stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState))); + if (!transitionReward.isLabeled() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { + stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); } } @@ -656,8 +629,8 @@ namespace storm { // Now add all rewards that match this choice. for (auto const& transitionReward : transitionRewards) { - if (transitionReward.getActionIndex() == choice.getActionIndex() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) { - stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState))); + if (transitionReward.getActionIndex() == choice.getActionIndex() && evaluator.asBool(transitionReward.getStatePredicateExpression())) { + stateToRewardMap[stateProbabilityPair.first] += ValueType(evaluator.asDouble(transitionReward.getRewardValueExpression())); } } @@ -696,7 +669,7 @@ namespace storm { for (auto const& booleanVariable : program.getGlobalBooleanVariables()) { variableInformation.booleanVariables.emplace_back(booleanVariable.getExpressionVariable(), booleanVariable.getInitialValueExpression().evaluateAsBool(), bitOffset); ++bitOffset; - booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1; + variableInformation.booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1; } for (auto const& integerVariable : program.getGlobalIntegerVariables()) { int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); @@ -704,13 +677,13 @@ namespace storm { 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; + variableInformation.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; + variableInformation.booleanVariableToIndexMap[booleanVariable.getExpressionVariable()] = variableInformation.booleanVariables.size() - 1; } for (auto const& integerVariable : module.getIntegerVariables()) { int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt(); @@ -718,7 +691,7 @@ namespace storm { 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; + variableInformation.integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1; } } @@ -743,12 +716,7 @@ namespace storm { modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation); // Finally, construct the state rewards. - modelComponents.stateRewards = buildStateRewards(rewardModel.getStateRewards(), stateInformation); - - // After everything has been created, we can delete the states. - for (auto state : stateInformation.reachableStates) { - delete state; - } + modelComponents.stateRewards = buildStateRewards(program, variableInformation, rewardModel.getStateRewards(), stateInformation); return modelComponents; } @@ -762,6 +730,8 @@ namespace storm { * @return The state labeling of the given program. */ static storm::models::AtomicPropositionsLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) { + storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager()); + std::vector const& labels = program.getLabels(); storm::models::AtomicPropositionsLabeling result(stateInformation.reachableStates.size(), labels.size() + 1); @@ -772,8 +742,10 @@ namespace storm { } for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { for (auto const& label : labels) { + unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getValue(stateInformation.reachableStates[index]), variableInformation, evaluator); + // Add label to state, if the corresponding expression is true. - if (label.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates[index])) { + if (evaluator.asBool(label.getStatePredicateExpression())) { result.addAtomicPropositionToState(label.getName(), index); } } @@ -795,14 +767,18 @@ namespace storm { * @param stateInformation Information about the state space. * @return A vector containing the state rewards for the state space. */ - static std::vector buildStateRewards(std::vector const& rewards, StateInformation const& stateInformation) { + static std::vector buildStateRewards(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector const& rewards, StateInformation const& stateInformation) { + storm::expressions::ExprtkExpressionEvaluator evaluator(program.getManager()); + std::vector result(stateInformation.reachableStates.size()); for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { result[index] = ValueType(0); for (auto const& reward : rewards) { + unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getValue(stateInformation.reachableStates[index]), variableInformation, evaluator); + // Add this reward to the state if the state is included in the state reward. - if (reward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates[index])) { - result[index] += ValueType(reward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates[index])); + if (evaluator.asBool(reward.getStatePredicateExpression())) { + result[index] += ValueType(evaluator.asDouble(reward.getRewardValueExpression())); } } } diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index f6598a7a2..9c458ea7b 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -131,7 +131,7 @@ namespace storm { return *this; } - bool BitVector::operator==(BitVector const& other) { + bool BitVector::operator==(BitVector const& other) const { // If the lengths of the vectors do not match, they are considered unequal. if (this->bitCount != other.bitCount) return false; @@ -146,7 +146,7 @@ namespace storm { return true; } - bool BitVector::operator!=(BitVector const& other) { + bool BitVector::operator!=(BitVector const& other) const { return !(*this == other); } @@ -648,7 +648,7 @@ namespace storm { } namespace std { - std::size_t hash::operator()(storm::storage::BitVector const& bv) { + std::size_t hash::operator()(storm::storage::BitVector const& bv) const { return boost::hash_range(bv.bucketVector.begin(), bv.bucketVector.end()); } } \ No newline at end of file diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index f5b0f6de9..0312f39f9 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -138,7 +138,7 @@ namespace storm { * @param other The bitvector with which to compare the current one. * @return True iff the other bit vector is semantically the same as the current one. */ - bool operator==(BitVector const& other); + bool operator==(BitVector const& other) const; /*! * Compares the given bit vector with the current one. @@ -146,7 +146,7 @@ namespace storm { * @param other The bitvector with which to compare the current one. * @return True iff the other bit vector is semantically not the same as the current one. */ - bool operator!=(BitVector const& other); + bool operator!=(BitVector const& other) const; /*! * Assigns the contents of the given bit vector to the current bit vector via a deep copy. @@ -494,7 +494,7 @@ namespace storm { namespace std { template <> struct hash { - std::size_t operator()(storm::storage::BitVector const& bv); + std::size_t operator()(storm::storage::BitVector const& bv) const; }; } diff --git a/src/storage/BitVectorHashMap.cpp b/src/storage/BitVectorHashMap.cpp index 1bb77bc6b..d02ce69a2 100644 --- a/src/storage/BitVectorHashMap.cpp +++ b/src/storage/BitVectorHashMap.cpp @@ -21,7 +21,7 @@ namespace storm { } template - bool BitVectorHashMap::isBucketOccupied(uint_fast64_t bucket) { + bool BitVectorHashMap::isBucketOccupied(uint_fast64_t bucket) const { return occupied.get(bucket); } @@ -66,37 +66,48 @@ namespace storm { this->increaseSize(); } + std::pair flagBucketPair = this->findBucket(key); + if (flagBucketPair.first) { + return std::make_pair(values[flagBucketPair.second], flagBucketPair.second); + } else { + // Insert the new bits into the bucket. + buckets.set(flagBucketPair.second * bucketSize, key); + occupied.set(flagBucketPair.second); + values[flagBucketPair.second] = value; + ++numberOfElements; + return std::make_pair(value, flagBucketPair.second); + } + } + + template + ValueType BitVectorHashMap::getValue(storm::storage::BitVector const& key) const { + std::pair flagBucketPair = this->findBucket(key); + STORM_LOG_ASSERT(flagBucketPair.first, "Unknown key."); + return flagBucketPair.second; + } + + template + std::pair BitVectorHashMap::findBucket(storm::storage::BitVector const& key) const { uint_fast64_t initialHash = hasher1(key) % *currentSizeIterator; uint_fast64_t bucket = initialHash; while (isBucketOccupied(bucket)) { if (buckets.matches(bucket * bucketSize, key)) { - return std::make_pair(values[bucket], bucket); + return std::make_pair(true, bucket); } bucket += hasher2(key); bucket %= *currentSizeIterator; - - // If we arrived at the original position, this means that we have visited all possible locations, but - // could not find a suitable position. This implies that we have to enlarge the map in order to resolve - // the issue. - if (bucket == initialHash) { - this->increaseSize(); - } } - - // Insert the new bits into the bucket. - buckets.set(bucket * bucketSize, key); - occupied.set(bucket); - values[bucket] = value; - ++numberOfElements; - return std::make_pair(value, bucket); + + return std::make_pair(false, bucket); } template - storm::storage::BitVector BitVectorHashMap::getBucket(std::size_t bucket) const { - return buckets.get(bucket * bucketSize, bucketSize); + std::pair BitVectorHashMap::getBucketAndValue(std::size_t bucket) const { + return std::make_pair(buckets.get(bucket * bucketSize, bucketSize), values[bucket]); } template class BitVectorHashMap; + template class BitVectorHashMap; } } diff --git a/src/storage/BitVectorHashMap.h b/src/storage/BitVectorHashMap.h index bea8fcbbc..9d6ea299f 100644 --- a/src/storage/BitVectorHashMap.h +++ b/src/storage/BitVectorHashMap.h @@ -50,12 +50,20 @@ namespace storm { std::pair findOrAddAndGetBucket(storm::storage::BitVector const& key, ValueType value); /*! - * Retrieves the key stored in the given bucket (if any). + * Retrieves the key stored in the given bucket (if any) and the value it is mapped to. * * @param bucket The index of the bucket. - * @return The content of the named bucket. + * @return The content and value of the named bucket. */ - storm::storage::BitVector getBucket(std::size_t bucket) const; + std::pair getBucketAndValue(std::size_t bucket) const; + + /*! + * Retrieves the value associated with the given key (if any). If the key does not exist, the behaviour is + * undefined. + * + * @return The value associated with the given key (if any). + */ + ValueType getValue(storm::storage::BitVector const& key) const; /*! * Retrieves the size of the map in terms of the number of key-value pairs it stores. @@ -78,7 +86,16 @@ namespace storm { * @param bucket The bucket to check. * @return True iff the bucket is occupied. */ - bool isBucketOccupied(uint_fast64_t bucket); + bool isBucketOccupied(uint_fast64_t bucket) const; + + /*! + * Searches for the bucket into which the given key can be inserted. + * + * @param key The key to search for. + * @return A pair whose first component indicates whether the key is already contained in the map and whose + * second component indicates in which bucket the key is stored/is supposed to be stored. + */ + std::pair findBucket(storm::storage::BitVector const& key) const; /*! * Increases the size of the hash map and performs the necessary rehashing of all entries. diff --git a/src/storage/LabeledValues.h b/src/storage/LabeledValues.h deleted file mode 100644 index 58f58f68b..000000000 --- a/src/storage/LabeledValues.h +++ /dev/null @@ -1,211 +0,0 @@ -/* - * LabeledValues.h - * - * Created on: 26.09.2013 - * Author: Christian Dehnert - */ - -#ifndef STORM_STORAGE_LABELEDVALUES_H -#define STORM_STORAGE_LABELEDVALUES_H - -#include -#include - -namespace storm { - namespace utility { - template - static ValueType constantZero(); - } - - namespace storage { - // This class provides the functionality to store a list of values, each of which is labeled with possibly several - // labels. - template - class LabeledValues { - public: - /*! - * Default-constructs an empty object. - */ - explicit LabeledValues() : valueLabelList() { - // Intentionally left empty. - } - - /*! - * Constructs an object that stores the single probability value without any label. - * - * @param value The probability to sto - */ - explicit LabeledValues(ValueType value) : valueLabelList() { - addValue(value); - } - - /*! - * Adds an (unlabeled) value to the list of labeled values. - * - * @param value The value to add. - * @return A reference to the list of labels that is associated with the given value. - */ - boost::container::flat_set& addValue(ValueType value) { - valueLabelList.emplace_back(value, boost::container::flat_set()); - return valueLabelList.back().second; - } - - /*! - * Adds a labeled value to the list of labeled values. - * - * @param value The value to add. - * @param labels The labels to associate with this value. - * @return A reference to the list of labels that is associated with the given value. - */ - boost::container::flat_set& addValue(ValueType value, boost::container::flat_set const& labels) { - valueLabelList.emplace_back(value, labels); - return valueLabelList.back().second; - } - - /*! - * Returns an iterator pointing to the first labeled probability. - * - * @return An iterator pointing to the first labeled probability. - */ - typename std::list>>::iterator begin() { - return valueLabelList.begin(); - } - - /*! - * Returns an iterator pointing past the last labeled probability. - * - * @return An iterator pointing past the last labeled probability. - */ - typename std::list>>::const_iterator end() { - return valueLabelList.end(); - } - - /*! - * Returns a const iterator pointing to the first labeled probability. - * - * @return A const iterator pointing to the first labeled probability. - */ - typename std::list>>::const_iterator begin() const { - return valueLabelList.begin(); - } - - /*! - * Returns a const iterator pointing past the last labeled probability. - * - * @return A const iterator pointing past the last labeled probability. - */ - typename std::list>>::const_iterator end() const { - return valueLabelList.end(); - } - - /*! - * Inserts the contents of this object to the given output stream. - * - * @param out The stream in which to insert the contents. - */ - friend std::ostream& operator<<(std::ostream& out, LabeledValues const& labeledValues) { - out << "["; - for (auto const& element : labeledValues) { - out << element.first << " ("; - for (auto const& label : element.second) { - out << label << ", "; - } - out << ") "; - } - out << "]"; - return out; - } - - /*! - * Adds all labeled values of the given object to the current one. - * - * @param labeledValues The labeled values to add to the object. - */ - LabeledValues& operator+=(LabeledValues const& labeledValues) { - for (auto const& valueLabelListPair : labeledValues) { - this->valueLabelList.push_back(valueLabelListPair); - } - return *this; - } - - /*! - * Divides the values by the given value. - * - * @param value The value by which to divide. - * @return A collection of labeled values that have the same labels as the current object, but whose values - * are divided by the given one. - */ - LabeledValues operator/(ValueType value) const { - LabeledValues result; - for (auto const& valueLabelListPair : valueLabelList) { - result.addValue(valueLabelListPair.first / value, valueLabelListPair.second); - } - return result; - } - - /*! - * Divides the values by the given unsigned integer value. - * - * @param value The unsigned integer value by which to divide. - * @return A collection of labeled values that have the same labels as the current object, but whose values - * are divided by the given one. - */ - LabeledValues operator/(uint_fast64_t value) const { - LabeledValues result; - for (auto const& valueLabelListPair : valueLabelList) { - result.addValue(valueLabelListPair.first / value, valueLabelListPair.second); - } - return result; - } - - /*! - * Converts the object into the value type by returning the sum. - * - * @return The sum of the values. - */ - operator ValueType() const { - return this->getSum(); - } - - /*! - * Retrieves the number of separate entries in this object. - * - * @return The number of separate entries in this object. - */ - size_t size() const { - return this->valueLabelList.size(); - } - - private: - // The actual storage used to store the list of values and the associated labels. - std::list>> valueLabelList; - - /*! - * Returns the sum of the values. - * - * @return The sum of the values. - */ - ValueType getSum() const { - ValueType sum = storm::utility::constantZero(); - for (auto const& valueLabelListPair : *this) { - sum += valueLabelListPair.first; - } - return sum; - } - }; - - /*! - * Computes the hash value of a given labeled probabilities object. - * - * @param labeledProbabilities The labeled probabilities object for which to compute the hash value. - * @return A hash value for the labeled probabilities object. - */ - template - std::size_t hash_value(LabeledValues const& labeledValues) { - return labeledValues.size(); - } - - } -} - -#endif /* STORM_STORAGE_LABELEDVALUES_H */ diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp index 7c11c4fc5..83b3e725d 100644 --- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -17,7 +17,7 @@ namespace storm { symbolTable.add_constants(); } - bool ExprtkExpressionEvaluator::asBool(Expression const& expression) { + bool ExprtkExpressionEvaluator::asBool(Expression const& expression) const { BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get(); auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); if (expressionPair == this->compiledExpressions.end()) { @@ -27,7 +27,7 @@ namespace storm { return expressionPair->second.value() == ValueType(1); } - int_fast64_t ExprtkExpressionEvaluator::asInt(Expression const& expression) { + int_fast64_t ExprtkExpressionEvaluator::asInt(Expression const& expression) const { BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get(); auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); if (expressionPair == this->compiledExpressions.end()) { @@ -37,7 +37,7 @@ namespace storm { return static_cast(expressionPair->second.value()); } - double ExprtkExpressionEvaluator::asDouble(Expression const& expression) { + double ExprtkExpressionEvaluator::asDouble(Expression const& expression) const { BaseExpression const* expressionPtr = expression.getBaseExpressionPointer().get(); auto const& expressionPair = this->compiledExpressions.find(expression.getBaseExpressionPointer().get()); if (expressionPair == this->compiledExpressions.end()) { @@ -47,11 +47,11 @@ namespace storm { return static_cast(expressionPair->second.value()); } - ExprtkExpressionEvaluator::CompiledExpressionType& ExprtkExpressionEvaluator::getCompiledExpression(BaseExpression const* expression) { + ExprtkExpressionEvaluator::CompiledExpressionType& ExprtkExpressionEvaluator::getCompiledExpression(BaseExpression const* expression) const { std::pair result = this->compiledExpressions.emplace(expression, CompiledExpressionType()); CompiledExpressionType& compiledExpression = result.first->second; compiledExpression.register_symbol_table(symbolTable); - bool parsingOk = parser.compile(stringTranslator.toString(expression), compiledExpression); + bool parsingOk = parser.compile(ToExprtkStringVisitor().toString(expression), compiledExpression); return compiledExpression; } diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.h b/src/storage/expressions/ExprtkExpressionEvaluator.h index 8aa771130..41cc313c3 100644 --- a/src/storage/expressions/ExprtkExpressionEvaluator.h +++ b/src/storage/expressions/ExprtkExpressionEvaluator.h @@ -21,9 +21,9 @@ namespace storm { */ ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager); - bool asBool(Expression const& expression); - int_fast64_t asInt(Expression const& expression); - double asDouble(Expression const& expression); + bool asBool(Expression const& expression) const; + int_fast64_t asInt(Expression const& expression) const; + double asDouble(Expression const& expression) const; void setBooleanValue(storm::expressions::Variable const& variable, bool value); void setIntegerValue(storm::expressions::Variable const& variable, int_fast64_t value); @@ -39,16 +39,16 @@ namespace storm { * * @param expression The expression that is to be compiled. */ - CompiledExpressionType& getCompiledExpression(BaseExpression const* expression); + CompiledExpressionType& getCompiledExpression(BaseExpression const* expression) const; // The expression manager that is used by this evaluator. std::shared_ptr manager; // The parser used. - exprtk::parser parser; + mutable exprtk::parser parser; // The symbol table used. - exprtk::symbol_table symbolTable; + mutable exprtk::symbol_table symbolTable; // The actual data that is fed into the expression. std::vector booleanValues; @@ -56,10 +56,7 @@ namespace storm { std::vector rationalValues; // A mapping of expressions to their compiled counterpart. - CacheType compiledExpressions; - - // A translator that can be used for transforming an expression into the correct string format. - ToExprtkStringVisitor stringTranslator; + mutable CacheType compiledExpressions; }; } } diff --git a/src/storage/expressions/Variable.cpp b/src/storage/expressions/Variable.cpp index a5f425215..64c7174ca 100644 --- a/src/storage/expressions/Variable.cpp +++ b/src/storage/expressions/Variable.cpp @@ -10,6 +10,10 @@ namespace storm { bool Variable::operator==(Variable const& other) const { return manager == other.manager && index == other.index; } + + bool Variable::operator!=(Variable const& other) const { + return !(*this == other); + } bool Variable::operator<(Variable const& other) const { return this->getIndex() < other.getIndex(); diff --git a/src/storage/expressions/Variable.h b/src/storage/expressions/Variable.h index c3a18eab0..f3a271760 100644 --- a/src/storage/expressions/Variable.h +++ b/src/storage/expressions/Variable.h @@ -41,6 +41,14 @@ namespace storm { */ bool operator==(Variable const& other) const; + /*! + * Checks the two variables for inequality. + * + * @param other The variable to compare with. + * @return True iff the two variables are different. + */ + bool operator!=(Variable const& other) const; + /*! * Checks whether the variable appears earlier in the total ordering of variables. * diff --git a/src/utility/PrismUtility.h b/src/utility/PrismUtility.h index e54932538..b3a78c364 100644 --- a/src/utility/PrismUtility.h +++ b/src/utility/PrismUtility.h @@ -1,7 +1,6 @@ #ifndef STORM_UTILITY_PRISMUTILITY #define STORM_UTILITY_PRISMUTILITY -#include "src/storage/LabeledValues.h" #include "src/storage/prism/Program.h" #include "src/utility/macros.h" #include "src/exceptions/InvalidArgumentException.h" @@ -10,7 +9,7 @@ namespace storm { namespace utility { namespace prism { // A structure holding information about a particular choice. - template> + template> struct Choice { public: Choice(uint_fast64_t actionIndex = 0) : distribution(), actionIndex(actionIndex), choiceLabels() { @@ -148,6 +147,10 @@ namespace storm { return distribution.at(state); } + void addProbability(KeyType state, ValueType value) { + distribution[state] += value; + } + private: // The distribution that is associated with the choice. std::map distribution; @@ -159,36 +162,6 @@ namespace storm { boost::container::flat_set choiceLabels; }; - /*! - * Adds the target state and probability to the given choice and ignores the labels. This function overloads with - * other functions to ensure the proper treatment of labels. - * - * @param choice The choice to which to add the target state and probability. - * @param state The target state of the probability. - * @param probability The probability to reach the target state in one step. - * @param labels A set of labels that is supposed to be associated with this state and probability. NOTE: this - * is ignored by this particular function but not by the overloaded functions. - */ - template - void addProbabilityToChoice(Choice& choice, uint_fast64_t state, ValueType probability, boost::container::flat_set const& labels) { - choice.getOrAddEntry(state) += probability; - } - - /*! - * Adds the target state and probability to the given choice and labels it accordingly. This function overloads - * with other functions to ensure the proper treatment of labels. - * - * @param choice The choice to which to add the target state and probability. - * @param state The target state of the probability. - * @param probability The probability to reach the target state in one step. - * @param labels A set of labels that is supposed to be associated with this state and probability. - */ - template - void addProbabilityToChoice(Choice>& choice, uint_fast64_t state, ValueType probability, boost::container::flat_set const& labels) { - auto& labeledEntry = choice.getOrAddEntry(state); - labeledEntry.addValue(probability, labels); - } - static std::map parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) { std::map constantDefinitions; std::set definedConstants; diff --git a/src/utility/constants.h b/src/utility/constants.h index a857e40ba..c956eecb9 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -20,7 +20,6 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/storage/BitVector.h" -#include "src/storage/LabeledValues.h" namespace storm { @@ -73,15 +72,6 @@ inline double constantZero() { return 0.0; } -/*! - * Template specialization for LabeledValues. - * @return A LabeledValues object that represents a value of 0. - */ -template<> -inline storm::storage::LabeledValues constantZero() { - return storm::storage::LabeledValues(0.0); -} - /*! @endcond */ /*! @@ -131,15 +121,6 @@ inline double constantOne() { return 1.0; } -/*! - * Template specialization for LabeledValues. - * @return A LabeledValues object that represents a value of 1. - */ -template<> -inline storm::storage::LabeledValues constantOne() { - return storm::storage::LabeledValues(1.0); -} - /*! @endcond */ /*! @@ -191,15 +172,6 @@ inline double constantInfinity() { return std::numeric_limits::infinity(); } -/*! - * Template specialization for LabeledValues. - * @return Value Infinity, fit to the type LabeledValues. - */ -template<> -inline storm::storage::LabeledValues constantInfinity() { - return storm::storage::LabeledValues(std::numeric_limits::infinity()); -} - /*! @endcond */