diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 70834ee9b..f82b4dcee 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -1,6 +1,6 @@ /* * File: ExplicitModelAdapter.h - * Author: Gereon Kremer + * Author: Christian Dehnert * * Created on March 15, 2013, 11:42 AM */ @@ -27,6 +27,7 @@ #include "src/models/Ctmdp.h" #include "src/models/AtomicPropositionsLabeling.h" #include "src/storage/SparseMatrix.h" +#include "src/storage/LabeledValues.h" #include "src/settings/Settings.h" #include "src/exceptions/WrongFormatException.h" @@ -71,6 +72,71 @@ namespace storm { } }; + // A structure holding information about a particular choice. + template + struct Choice { + Choice(std::string const& actionLabel) : distribution(), actionLabel(actionLabel), choiceLabels() { + // Intentionally left empty. + } + + /*! + * Returns an iterator to the first element of this choice. + * + * @return An iterator to the first element of this choice. + */ + typename std::map::const_iterator begin() const { + return distribution.cbegin(); + } + + /*! + * Returns an iterator that points past the elements of this choice. + * + * @return An iterator that points past the elements of this choice. + */ + typename std::map::const_iterator end() const { + return distribution.cend(); + } + + /*! + * Adds the given label to the labels associated with this choice. + * + * @param label The label to associate with this choice. + */ + void addChoiceLabel(uint_fast64_t label) { + choiceLabels.insert(label); + } + + // The distribution that is associated with the choice. + std::map distribution; + + // The label of the choice. + std::string actionLabel; + + // The labels that are associated with this choice. + std::set choiceLabels; + }; + + template + void addProbabilityToChoice(Choice& choice, uint_fast64_t state, ValueType probability, std::set const& labels) { + auto stateProbabilityPair = choice.distribution.find(state); + + if (stateProbabilityPair == choice.distribution.end()) { + choice.distribution[state] = probability; + } else { + choice.distribution[state] += probability; + } + } + + template + void addProbabilityToChoice(Choice>& choice, uint_fast64_t state, ValueType probability, std::set const& labels) { + auto stateProbabilityPair = choice.distribution.find(state); + + if (stateProbabilityPair == choice.distribution.end()) { + choice.distribution[state] = storm::storage::LabeledValues(); + } + choice.distribution[state].addValue(probability); + } + template class ExplicitModelAdapter { public: @@ -80,9 +146,16 @@ namespace storm { // Intentionally left empty. } + // A list of reachable states. std::vector reachableStates; + + // A mapping from states to indices in the list of reachable states. std::unordered_map stateToIndexMap; + + // A vector storing the number of choices for each state. std::vector numberOfChoices; + + // The total number of transitions discovered. uint_fast64_t numberOfTransitions; }; @@ -92,12 +165,23 @@ namespace storm { // Intentionally left empty. } - storm::storage::SparseMatrix transitionMatrix; + // The transition matrix. + storm::storage::SparseMatrix transitionMatrix; + + // The state labeling. storm::models::AtomicPropositionsLabeling stateLabeling; + + // A vector indicating at which row the choices for a particular state begin. std::vector nondeterministicChoiceIndices; - std::vector stateRewards; - storm::storage::SparseMatrix transitionRewardMatrix; - std::vector> choiceLabeling; + + // The state reward vector. + std::vector stateRewards; + + // A matrix storing the reward for particular transitions. + storm::storage::SparseMatrix transitionRewardMatrix; + + // A vector that stores a labeling for each choice. + std::vector> choiceLabeling; }; // A structure storing information about the used variables of the program. @@ -131,26 +215,25 @@ namespace storm { * rewards. * @return The explicit model that was given by the probabilistic program. */ - static std::shared_ptr> translateProgram(storm::ir::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") { + static std::shared_ptr> translateProgram(storm::ir::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") { // Start by defining the undefined constants in the model. defineUndefinedConstants(program, constantDefinitionString); ModelComponents modelComponents = buildModelComponents(program, rewardModelName); - std::shared_ptr> result; + std::shared_ptr> result; switch (program.getModelType()) { case storm::ir::Program::DTMC: - result = std::shared_ptr>(new storm::models::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); break; case storm::ir::Program::CTMC: - result = std::shared_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); - break; + result = std::shared_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); break; case storm::ir::Program::MDP: - result = std::shared_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); break; case storm::ir::Program::CTMDP: - result = std::shared_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); + result = std::shared_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); break; default: LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type."); @@ -681,8 +764,8 @@ namespace storm { return result; } - static std::list> getUnlabeledTransitions(storm::ir::Program const& program, StateInformation const& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex) { - std::list> result; + static std::list> getUnlabeledTransitions(storm::ir::Program const& program, StateInformation const& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex) { + std::list> result; StateType const* currentState = stateInformation.reachableStates[stateIndex]; @@ -699,8 +782,9 @@ namespace storm { // Skip the command, if it is not enabled. if (!command.getGuard()->getValueAsBool(currentState)) continue; - result.push_back(std::map()); - std::map& targetStates = result.back(); + result.push_back(Choice("")); + Choice& choice = result.back(); + choice.addChoiceLabel(command.getGlobalIndex()); double probabilitySum = 0; // Iterate over all updates of the current command. @@ -711,13 +795,12 @@ namespace storm { uint_fast64_t targetStateIndex = stateInformation.stateToIndexMap.at(applyUpdate(variableInformation, currentState, update)); // Check, if we already saw this state in another update and, if so, add up probabilities. - probabilitySum += update.getLikelihoodExpression()->getValueAsDouble(currentState); - auto stateIt = targetStates.find(targetStateIndex); - if (stateIt == targetStates.end()) { - targetStates[targetStateIndex] = update.getLikelihoodExpression()->getValueAsDouble(currentState); - } else { - targetStates[targetStateIndex] += update.getLikelihoodExpression()->getValueAsDouble(currentState); - } + double probabilityToAdd = update.getLikelihoodExpression()->getValueAsDouble(currentState); + probabilitySum += probabilityToAdd; + std::set labels; + // FIXME: We have to retrieve the index of the update here, which is currently not possible. + // labels.insert(update.getGlobalIndex()); + addProbabilityToChoice(choice, targetStateIndex, probabilityToAdd, labels); } // Check that the resulting distribution is in fact a distribution. @@ -731,8 +814,8 @@ namespace storm { return result; } - static std::list> getLabeledTransitions(storm::ir::Program const& program, StateInformation const& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex) { - std::list> result; + static std::list> getLabeledTransitions(storm::ir::Program const& program, StateInformation const& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex) { + std::list> result; for (std::string const& action : program.getActions()) { StateType const* currentState = stateInformation.reachableStates[stateIndex]; @@ -791,14 +874,21 @@ namespace storm { // At this point, we applied all commands of the current command combination and newTargetStates // contains all target states and their respective probabilities. That means we are now ready to // add the choice to the list of transitions. - result.push_back(std::map()); - + result.push_back(Choice(action)); + // Now create the actual distribution. - std::map& targetStates = result.back(); + Choice& choice = result.back(); + + // Add the labels of all commands to this choice. + for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { + choice.addChoiceLabel(iteratorList[i]->getGlobalIndex()); + } + double probabilitySum = 0; + std::set labels; for (auto const& stateProbabilityPair : *newTargetStates) { uint_fast64_t newStateIndex = stateInformation.stateToIndexMap.at(stateProbabilityPair.first); - targetStates[newStateIndex] = stateProbabilityPair.second; + addProbabilityToChoice(choice, newStateIndex, stateProbabilityPair.second, labels); probabilitySum += stateProbabilityPair.second; } @@ -835,22 +925,24 @@ namespace storm { /*! * */ - static std::vector buildTransitionMatrix(storm::ir::Program const& program, VariableInformation const& variableInformation, storm::ir::RewardModel const& rewardModel, StateInformation const& stateInformation, bool deterministicModel, storm::storage::SparseMatrix& transitionMatrix, storm::storage::SparseMatrix& transitionRewardMatrix) { + static std::pair, std::vector>> buildMatrices(storm::ir::Program const& program, VariableInformation const& variableInformation, std::vector const& transitionRewards, StateInformation const& stateInformation, bool deterministicModel, storm::storage::SparseMatrix& transitionMatrix, storm::storage::SparseMatrix& transitionRewardMatrix) { std::vector nondeterministicChoiceIndices(stateInformation.reachableStates.size() + 1); + std::vector> choiceLabels; // Add transitions and rewards for all states. uint_fast64_t currentRow = 0; for (uint_fast64_t currentState = 0; currentState < stateInformation.reachableStates.size(); ++currentState) { // Retrieve all choices for the current state. - std::list> allChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState); - std::list> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState); - allChoices.insert(allChoices.end(), allLabeledChoices.begin(), allLabeledChoices.end()); + std::list> allUnlabeledChoices = getUnlabeledTransitions(program, stateInformation, variableInformation, currentState); + std::list> allLabeledChoices = getLabeledTransitions(program, stateInformation, variableInformation, currentState); + + uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size(); // If the current state does not have a single choice, we equip it with a self-loop if that was // requested and issue an error otherwise. - if (allChoices.size() == 0) { + if (totalNumberOfChoices == 0) { if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { - transitionMatrix.insertNextValue(currentRow, currentState, 1); + transitionMatrix.insertNextValue(currentRow, currentState, storm::utility::constGetOne()); ++currentRow; } else { LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); @@ -861,21 +953,35 @@ namespace storm { // or compose them to one choice. if (deterministicModel) { std::map globalDistribution; + std::set allChoiceLabels; // Combine all the choices and scale them with the total number of choices of the current state. - for (auto const& choice : allChoices) { + for (auto const& choice : allUnlabeledChoices) { + allChoiceLabels.insert(choice.choiceLabels.begin(), choice.choiceLabels.end()); + for (auto const& stateProbabilityPair : choice) { + auto existingStateProbabilityPair = globalDistribution.find(stateProbabilityPair.first); + if (existingStateProbabilityPair == globalDistribution.end()) { + globalDistribution[stateProbabilityPair.first] += stateProbabilityPair.second / totalNumberOfChoices; + } else { + globalDistribution[stateProbabilityPair.first] = stateProbabilityPair.second / totalNumberOfChoices; + } + } + } + for (auto const& choice : allLabeledChoices) { for (auto const& stateProbabilityPair : choice) { auto existingStateProbabilityPair = globalDistribution.find(stateProbabilityPair.first); if (existingStateProbabilityPair == globalDistribution.end()) { - globalDistribution[stateProbabilityPair.first] += stateProbabilityPair.second / allChoices.size(); + globalDistribution[stateProbabilityPair.first] += stateProbabilityPair.second / totalNumberOfChoices; } else { - globalDistribution[stateProbabilityPair.first] = stateProbabilityPair.second / allChoices.size(); + globalDistribution[stateProbabilityPair.first] = stateProbabilityPair.second / totalNumberOfChoices; } } } + // Now add the resulting distribution as the only choice of the current state. nondeterministicChoiceIndices[currentState] = currentRow; + choiceLabels.push_back(allChoiceLabels); for (auto const& stateProbabilityPair : globalDistribution) { transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); @@ -885,10 +991,54 @@ namespace storm { } else { // If the model is nondeterministic, we add all choices individually. nondeterministicChoiceIndices[currentState] = currentRow; - for (auto const& choice : allChoices) { + + // First, process all unlabeled choices. + for (auto const& choice : allUnlabeledChoices) { + std::map stateToRewardMap; + choiceLabels.emplace_back(std::move(choice.choiceLabels)); + + for (auto const& stateProbabilityPair : choice) { + transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + + // Now add all rewards that match this choice. + for (auto const& transitionReward : transitionRewards) { + if (transitionReward.getActionName() == "" && transitionReward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates.at(currentState))) { + stateToRewardMap[stateProbabilityPair.first] += transitionReward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates.at(currentState)); + } + } + + } + + // Add all transition rewards to the matrix. + for (auto const& stateRewardPair : stateToRewardMap) { + transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); + } + + ++currentRow; + } + + // Then, process all labeled choices. + for (auto const& choice : allLabeledChoices) { + std::map stateToRewardMap; + choiceLabels.emplace_back(std::move(choice.choiceLabels)); + for (auto const& stateProbabilityPair : choice) { transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + + // Now add all rewards that match this choice. + for (auto const& transitionReward : transitionRewards) { + if (transitionReward.getActionName() == "" && transitionReward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates.at(currentState))) { + stateToRewardMap[stateProbabilityPair.first] += transitionReward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates.at(currentState)); + } + } + } + + // Add all transition rewards to the matrix. + for (auto const& stateRewardPair : stateToRewardMap) { + transitionRewardMatrix.insertNextValue(currentRow, stateRewardPair.first, stateRewardPair.second); + } + ++currentRow; } } @@ -897,7 +1047,7 @@ namespace storm { nondeterministicChoiceIndices[stateInformation.reachableStates.size()] = currentRow; - return nondeterministicChoiceIndices; + return std::make_pair(nondeterministicChoiceIndices, choiceLabels); } /*! @@ -934,9 +1084,13 @@ namespace storm { modelComponents.transitionRewardMatrix.initialize(); } - storm::ir::RewardModel rewardModel = rewardModelName != "" ? program.getRewardModel(rewardModelName) : storm::ir::RewardModel(); + // Get the selected reward model or create an empty one if none is selected. + storm::ir::RewardModel const& rewardModel = rewardModelName != "" ? program.getRewardModel(rewardModelName) : storm::ir::RewardModel(); - modelComponents.nondeterministicChoiceIndices = buildTransitionMatrix(program, variableInformation, rewardModel, stateInformation, deterministicModel, modelComponents.transitionMatrix, modelComponents.transitionRewardMatrix); + // Build the transition and reward matrices. + std::pair, std::vector>> nondeterministicChoiceIndicesAndChoiceLabelsPair = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, deterministicModel, modelComponents.transitionMatrix, modelComponents.transitionRewardMatrix); + modelComponents.nondeterministicChoiceIndices = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.first); + modelComponents.choiceLabeling = std::move(nondeterministicChoiceIndicesAndChoiceLabelsPair.second); // Finalize the resulting matrices. modelComponents.transitionMatrix.finalize(); @@ -997,63 +1151,6 @@ namespace storm { } return result; } - - /*! - * Retrieves the state rewards for every reachable state based on the given state rewards. - * - * @param rewards The rewards to use. - * @return The reward values for every (reachable) state. - */ -// static std::vector getStateRewards(std::vector const& rewards); - - /*! - * Computes the labels for every reachable state based on a list of available labels. - * - * @param labels A mapping from label names to boolean expressions to use for the labeling. - * @return The resulting labeling. - */ -// static storm::models::AtomicPropositionsLabeling getStateLabeling(std::map> labels); - - /*! - * Builds the transition matrix of a deterministic model from the current list of transitions. - * - * @return The transition matrix. - */ -// static storm::storage::SparseMatrix buildDeterministicMatrix(); - - /*! - * Builds the transition matrix of a nondeterministic model from the current list of transitions. - * - * @return result The transition matrix. - */ -// static storm::storage::SparseMatrix buildNondeterministicMatrix(); - - /*! - * Generate the (internal) list of all transitions of the model. - */ -// void buildTransitionMap(); - - //// Members that are filled during the conversion. - // The selected reward model. - std::unique_ptr rewardModel; - - // The number of choices for each state of a nondeterministic model. - std::vector choiceIndices; - - // The result of the translation of transition rewards to a sparse matrix (if any). - boost::optional> transitionRewards; - - // A labeling for the choices of each state. - std::vector> choiceLabeling; - - /*! - * Maps a source state to a list of probability distributions over target states. Each distribution - * corresponds to an unlabeled command or a feasible combination of labeled commands. Therefore, each - * distribution is represented by a structure that contains the label of the participating commands, a list - * of labels associated with that particular command combination and a mapping from target states to their - * probabilities. - */ - std::map>, std::map>>> transitionMap; }; } // namespace adapters diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 53d95449e..d2e24cbbd 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -29,7 +29,7 @@ class AbstractDeterministicModel: public AbstractModel { */ AbstractDeterministicModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { } @@ -43,7 +43,7 @@ class AbstractDeterministicModel: public AbstractModel { */ AbstractDeterministicModel(storm::storage::SparseMatrix&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) { @@ -116,13 +116,13 @@ class AbstractDeterministicModel: public AbstractModel { * @return void */ virtual void setStateIdBasedChoiceLabeling() override { - std::vector> newChoiceLabeling; + std::vector> newChoiceLabeling; size_t stateCount = this->getNumberOfStates(); newChoiceLabeling.resize(stateCount); for (size_t state = 0; state < stateCount; ++state) { - newChoiceLabeling.at(state).push_back(state); + newChoiceLabeling.at(state).insert(state); } this->choiceLabeling.reset(newChoiceLabeling); diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index fa34a1cf3..5a67c3e98 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -71,7 +71,7 @@ class AbstractModel: public std::enable_shared_from_this> { */ AbstractModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling) { if (optionalStateRewardVector) { @@ -95,7 +95,7 @@ class AbstractModel: public std::enable_shared_from_this> { */ AbstractModel(storm::storage::SparseMatrix&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) : + boost::optional>>&& optionalChoiceLabeling) : transitionMatrix(std::move(transitionMatrix)), choiceLabeling(std::move(optionalChoiceLabeling)), stateLabeling(std::move(stateLabeling)), stateRewardVector(std::move(optionalStateRewardVector)), transitionRewardMatrix(std::move(optionalTransitionRewardMatrix)) { @@ -359,7 +359,7 @@ class AbstractModel: public std::enable_shared_from_this> { * Returns the labels for the choices of the model, if there are any. * @return The labels for the choices of the model. */ - std::vector> const& getChoiceLabeling() const { + std::vector> const& getChoiceLabeling() const { return choiceLabeling.get(); } @@ -538,7 +538,7 @@ protected: storm::storage::SparseMatrix transitionMatrix; /*! The labeling that is associated with the choices for each state. */ - boost::optional>> choiceLabeling; + boost::optional>> choiceLabeling; private: /*! The labeling of the states of the model. */ storm::models::AtomicPropositionsLabeling stateLabeling; diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 9e01e224f..bb6b0fd37 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -34,7 +34,7 @@ class AbstractNondeterministicModel: public AbstractModel { std::vector const& nondeterministicChoiceIndices, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { this->nondeterministicChoiceIndices = nondeterministicChoiceIndices; } @@ -54,7 +54,7 @@ class AbstractNondeterministicModel: public AbstractModel { std::vector&& nondeterministicChoiceIndices, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)), nondeterministicChoiceIndices(std::move(nondeterministicChoiceIndices)) { @@ -225,7 +225,7 @@ class AbstractNondeterministicModel: public AbstractModel { * @return void */ virtual void setStateIdBasedChoiceLabeling() override { - std::vector> newChoiceLabeling; + std::vector> newChoiceLabeling; size_t stateCount = this->getNumberOfStates(); size_t choiceCount = this->getNumberOfChoices(); @@ -233,7 +233,7 @@ class AbstractNondeterministicModel: public AbstractModel { for (size_t state = 0; state < stateCount; ++state) { for (size_t choice = this->nondeterministicChoiceIndices.at(state); choice < this->nondeterministicChoiceIndices.at(state + 1); ++choice) { - newChoiceLabeling.at(choice).push_back(state); + newChoiceLabeling.at(choice).insert(state); } } diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index 9ad1dfb86..f4ba0de50 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -40,7 +40,7 @@ public: * @param apCountMax The number of atomic propositions. */ AtomicPropositionsLabeling(const uint_fast64_t stateCount = 0, uint_fast64_t const apCountMax = 0) - : stateCount(stateCount), apCountMax(apCountMax), apsCurrent(0), singleLabelings() { + : stateCount(stateCount), apCountMax(apCountMax), apsCurrent(0), nameToLabelingMap(), singleLabelings() { singleLabelings.reserve(apCountMax); } @@ -159,7 +159,7 @@ public: * @return True if the proposition is registered within the labeling, false otherwise. */ bool containsAtomicProposition(std::string const& ap) const { - return (nameToLabelingMap.count(ap) != 0); + return nameToLabelingMap.find(ap) != nameToLabelingMap.end(); } /*! @@ -279,8 +279,7 @@ public: } } - std::unordered_map const& getNameToLabelingMap() const - { + std::unordered_map const& getNameToLabelingMap() const { return this->nameToLabelingMap; } diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index 9febcfb5f..787649540 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -37,7 +37,7 @@ public: */ Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractDeterministicModel(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { // Intentionally left empty. } @@ -52,7 +52,7 @@ public: */ Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractDeterministicModel(std::move(rateMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) { diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index f80525602..c8966357c 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -42,7 +42,7 @@ public: std::vector const& nondeterministicChoiceIndices, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { if (!this->checkValidityOfProbabilityMatrix()) { @@ -65,7 +65,7 @@ public: std::vector&& nondeterministicChoiceIndices, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractNondeterministicModel(std::move(probabilityMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) { diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index 0254204bb..849a42344 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -43,7 +43,7 @@ public: */ Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractDeterministicModel(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); @@ -69,7 +69,7 @@ public: */ Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractDeterministicModel(std::move(probabilityMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) { diff --git a/src/models/Mdp.h b/src/models/Mdp.h index 5e0d99955..cb988c90b 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -48,7 +48,7 @@ public: std::vector const& nondeterministicChoiceIndices, boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, - boost::optional>> const& optionalChoiceLabeling) + boost::optional>> const& optionalChoiceLabeling) : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); @@ -70,7 +70,7 @@ public: std::vector&& nondeterministicChoiceIndices, boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, - boost::optional>>&& optionalChoiceLabeling) + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class : AbstractNondeterministicModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) { diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index 03744401b..ec357b3bf 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -58,7 +58,7 @@ DeterministicModelParserResultContainer parseDeterministicModel(std::str storm::models::Dtmc DeterministicModelParserAsDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { DeterministicModelParserResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); - return storm::models::Dtmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Dtmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } /*! @@ -69,7 +69,7 @@ storm::models::Dtmc DeterministicModelParserAsDtmc(std::string const & t storm::models::Ctmc DeterministicModelParserAsCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { DeterministicModelParserResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); - return storm::models::Ctmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Ctmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } } /* namespace parser */ diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index bbe39ae02..536a6ec88 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -58,7 +58,7 @@ NondeterministicModelParserResultContainer parseNondeterministicModel(st storm::models::Mdp NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } /*! @@ -69,7 +69,7 @@ storm::models::Mdp NondeterministicModelParserAsMdp(std::string const & storm::models::Ctmdp NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); + return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } } /* namespace parser */ diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index d36b4d647..d8c19f523 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -343,7 +343,7 @@ public: * @return A reference to the current bit vector corresponding to the logical "and" * of the two bit vectors. */ - BitVector operator&=(BitVector const& bv) { + BitVector& operator&=(BitVector const& bv) { uint_fast64_t minSize = (bv.bucketCount < this->bucketCount) ? bv.bucketCount : this->bucketCount; for (uint_fast64_t i = 0; i < minSize; ++i) { diff --git a/src/storage/LabeledProbabilities.h b/src/storage/LabeledProbabilities.h deleted file mode 100644 index 262f1fc4c..000000000 --- a/src/storage/LabeledProbabilities.h +++ /dev/null @@ -1,79 +0,0 @@ -/* - * LabeledProbabilities.h - * - * Created on: 26.09.2013 - * Author: Christian Dehnert - */ - -#ifndef STORM_STORAGE_LABELEDPROBABILITIES_H -#define STORM_STORAGE_LABELEDPROBABILITIES_H - -namespace storm { - namespace storage { - - // This class provides the functionality to store a list of probabilities, each of which is labeled with a list - // of labels. - template - class LabeledProbabilities { - public: - /*! - * Default-constructs an empty object. - */ - LabeledProbabilities() : probabilityLabelList() { - // Intentionally left empty. - } - - /*! - * Adds a probability to the list of labeled probabilities. - * - * @return A reference to the list of labels that is associated with the given probability. - */ - Container& addProbability(ValueType probability) { - probabilityLabelList.emplace_back(probability, Container()); - return probabilityLabelList.back().second; - } - - /*! - * Returns an iterator pointing to the first labeled probability. - * - * @return An iterator pointing to the first labeled probability. - */ - Container>>::iterator begin() { - return probabilityLabelList.begin(); - } - - /*! - * Returns an iterator pointing past the last labeled probability. - * - * @return An iterator pointing past the last labeled probability. - */ - Container>>::const_iterator end() { - return probabilityLabelList.end(); - } - - /*! - * Returns a const iterator pointing to the first labeled probability. - * - * @return A const iterator pointing to the first labeled probability. - */ - Container>>::const_iterator begin() const { - return probabilityLabelList.begin(); - } - - /*! - * Returns a const iterator pointing past the last labeled probability. - * - * @return A const iterator pointing past the last labeled probability. - */ - Container>>::const_iterator end() const { - return probabilityLabelList.end(); - } - - private: - // The actual storage used to store the list of probabilities and the associated labels. - Container>> probabilityLabelList; - }; - } -} - -#endif /* STORM_STORAGE_LABELEDPROBABILITIES_H */ diff --git a/src/storage/LabeledValues.h b/src/storage/LabeledValues.h new file mode 100644 index 000000000..e8abf35c4 --- /dev/null +++ b/src/storage/LabeledValues.h @@ -0,0 +1,180 @@ +/* + * LabeledValues.h + * + * Created on: 26.09.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_STORAGE_LABELEDVALUES_H +#define STORM_STORAGE_LABELEDVALUES_H + +#include + +namespace storm { + namespace utility { + template + static ValueType constGetZero(); + } + + 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. + */ + LabeledValues() : valueLabelList() { + // Intentionally left empty. + } + + /*! + * Constructs an object that stores the single probability value without any label. + * + * @param value The probability to sto + */ + 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. + */ + std::set& addValue(ValueType value) { + valueLabelList.emplace_back(value, std::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. + */ + std::set& addValue(ValueType value, std::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 probabilities of the given object to the current one. + * + * @param labeledProbabilities The labeled probabilities to add to the object. + */ + LabeledValues& operator+=(LabeledValues const& labeledValues) { + for (auto const& valueLabelListPair : labeledValues) { + this->valueLabelList.push_back(valueLabelListPair); + } + return *this; + } + + /*! + * 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::constGetZero(); + 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/storm.cpp b/src/storm.cpp index 724ce03dd..69072ba12 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -332,8 +332,8 @@ int main(const int argc, const char* argv[]) { } else if (s->isSet("symbolic")) { std::string const& programFile = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString(); std::string const& constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString(); - std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(storm::parser::PrismParserFromFile(programFile), constants); - // model->printModelInformationToStream(std::cout); + std::shared_ptr>> model = storm::adapters::ExplicitModelAdapter>::translateProgram(storm::parser::PrismParserFromFile(programFile), constants); + model->printModelInformationToStream(std::cout); // Enable the following lines to test the MinimalLabelSetGenerator. // if (model->getType() == storm::models::MDP) { diff --git a/src/utility/ConstTemplates.h b/src/utility/ConstTemplates.h index 20704e3c1..71b489c3d 100644 --- a/src/utility/ConstTemplates.h +++ b/src/utility/ConstTemplates.h @@ -20,6 +20,7 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/storage/BitVector.h" +#include "src/storage/LabeledValues.h" namespace storm { @@ -46,7 +47,7 @@ static inline _Scalar constGetZero() { */ /*! - * Template specification for int_fast32_t + * Template specialization for int_fast32_t * @return Value 0, fit to the type int_fast32_t */ template <> @@ -55,7 +56,7 @@ inline int_fast32_t constGetZero() { } /*! - * Template specification for uint_fast64_t + * Template specialization for uint_fast64_t * @return Value 0, fit to the type uint_fast64_t */ template <> @@ -64,13 +65,22 @@ inline uint_fast64_t constGetZero() { } /*! - * Template specification for double + * Template specialization for double * @return Value 0.0, fit to the type double */ template <> inline double constGetZero() { return 0.0; } + +/*! + * Template specialization for LabeledValues. + * @return A LabeledValues object that represents a value of 0. + */ +template<> +inline storm::storage::LabeledValues constGetZero() { + return storm::storage::LabeledValues(0.0); +} /*! @endcond */ @@ -91,11 +101,11 @@ static inline _Scalar constGetOne() { } /*! @cond TEMPLATE_SPECIALIZATION - * (By default, the template specifications are not included in the documentation) + * (By default, the template specializations are not included in the documentation) */ /*! - * Template specification for int_fast32_t + * Template specialization for int_fast32_t * @return Value 1, fit to the type int_fast32_t */ template<> @@ -104,7 +114,7 @@ inline int_fast32_t constGetOne() { } /*! - * Template specification for uint_fast64_t + * Template specialization for uint_fast64_t * @return Value 1, fit to the type uint_fast61_t */ template<> @@ -113,7 +123,7 @@ inline uint_fast64_t constGetOne() { } /*! - * Template specification for double + * Template specialization for double * @return Value 1.0, fit to the type double */ template<> @@ -121,6 +131,15 @@ inline double constGetOne() { return 1.0; } +/*! + * Template specialization for LabeledValues. + * @return A LabeledValues object that represents a value of 1. + */ +template<> +inline storm::storage::LabeledValues constGetOne() { + return storm::storage::LabeledValues(1.0); +} + /*! @endcond */ /*! @@ -140,11 +159,11 @@ static inline _Scalar constGetInfinity() { } /*! @cond TEMPLATE_SPECIALIZATION - * (By default, the template specifications are not included in the documentation) + * (By default, the template specializations are not included in the documentation) */ /*! - * Template specification for int_fast32_t + * Template specialization for int_fast32_t * @return Value Infinity, fit to the type uint_fast32_t */ template<> @@ -154,7 +173,7 @@ inline int_fast32_t constGetInfinity() { } /*! - * Template specification for uint_fast64_t + * Template specialization for uint_fast64_t * @return Value Infinity, fit to the type uint_fast64_t */ template<> @@ -164,7 +183,7 @@ inline uint_fast64_t constGetInfinity() { } /*! - * Template specification for double + * Template specialization for double * @return Value Infinity, fit to the type double */ template<> @@ -172,11 +191,19 @@ inline double constGetInfinity() { return std::numeric_limits::infinity(); } +/*! + * Template specialization for LabeledValues. + * @return Value Infinity, fit to the type LabeledValues. + */ +template<> +inline storm::storage::LabeledValues constGetInfinity() { + return storm::storage::LabeledValues(std::numeric_limits::infinity()); +} + /*! @endcond */ } //namespace utility } //namespace storm - #endif /* STORM_UTILITY_CONSTTEMPLATES_H_ */