From 84f1b192b449ddbaa8e1fce97623758fe6237ee8 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 30 Sep 2013 16:39:11 +0200 Subject: [PATCH] Added globally unique indexes to updates in IR. Finalized support for labeled values in ExplicitModelAdapter. Modified tests to comply with the new usage of ExplicitModelAdapter. Former-commit-id: f6d5a33d6ddae7ba947eb1da1d391e5c54915c62 --- src/adapters/ExplicitModelAdapter.cpp | 397 ------------------- src/adapters/ExplicitModelAdapter.h | 183 +++++++-- src/ir/Command.cpp | 2 +- src/ir/Update.cpp | 12 +- src/ir/Update.h | 20 +- src/parser/prismparser/PrismGrammar.cpp | 8 +- src/parser/prismparser/PrismGrammar.h | 443 +++++++++++----------- src/parser/prismparser/VariableState.cpp | 341 +++++++++-------- src/parser/prismparser/VariableState.h | 370 +++++++++--------- src/storage/LabeledValues.h | 42 +- test/functional/parser/ParsePrismTest.cpp | 11 +- 11 files changed, 801 insertions(+), 1028 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index f29b757f7..56c684753 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -1,403 +1,6 @@ -#include "src/adapters/ExplicitModelAdapter.h" - -#include "src/storage/SparseMatrix.h" #include "src/settings/Settings.h" -#include "src/exceptions/WrongFormatException.h" - -#include "src/ir/Program.h" -#include "src/ir/RewardModel.h" -#include "src/ir/StateReward.h" -#include "src/ir/TransitionReward.h" - -#include "src/models/AbstractModel.h" -#include "src/models/Dtmc.h" -#include "src/models/Ctmc.h" -#include "src/models/Mdp.h" -#include "src/models/Ctmdp.h" - -#include -#include -#include - -#include -#include bool ExplicitModelAdapterOptionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool { instance->addOption(storm::settings::OptionBuilder("ExplicitModelAdapter", "constants", "", "Specifies the constant replacements to use in Explicit Models").addArgument(storm::settings::ArgumentBuilder::createStringArgument("constantString", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3").setDefaultValueString("").build()).build()); return true; }); - -namespace storm { - namespace adapters { - - - - -// std::vector ExplicitModelAdapter::getStateRewards(std::vector const& rewards) { -// std::vector result(this->allStates.size()); -// for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { -// result[index] = 0; -// for (auto const& reward : rewards) { -// // Add this reward to the state if the state is included in the state reward. -// if (reward.getStatePredicate()->getValueAsBool(this->allStates[index]) == true) { -// result[index] += reward.getRewardValue()->getValueAsDouble(this->allStates[index]); -// } -// } -// } -// return result; -// } - -// storm::models::AtomicPropositionsLabeling ExplicitModelAdapter::getStateLabeling(std::map> labels) { -// storm::models::AtomicPropositionsLabeling results(this->allStates.size(), labels.size() + 1); -// // Initialize labeling. -// for (auto const& labelExpressionPair : labels) { -// results.addAtomicProposition(labelExpressionPair.first); -// } -// for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { -// for (auto const& labelExpressionPair: labels) { -// // Add label to state, if the corresponding expression is true. -// if (labelExpressionPair.second->getValueAsBool(this->allStates[index])) { -// results.addAtomicPropositionToState(labelExpressionPair.first, index); -// } -// } -// } -// -// // Also label the initial state with the special label "init". -// results.addAtomicProposition("init"); -// StateType* initialState = this->getInitialState(); -// uint_fast64_t initialIndex = this->stateToIndexMap[initialState]; -// results.addAtomicPropositionToState("init", initialIndex); -// delete initialState; -// -// return results; -// } - -// boost::optional>> ExplicitModelAdapter::getActiveCommandsByAction(StateType const* state, std::string const& action) { -// boost::optional>> result((std::vector>())); -// -// // Iterate over all modules. -// for (uint_fast64_t i = 0; i < this->program.getNumberOfModules(); ++i) { -// storm::ir::Module const& module = this->program.getModule(i); -// -// // If the module has no command labeled with the given action, we can skip this module. -// if (!module.hasAction(action)) { -// continue; -// } -// -// std::set const& commandIndices = module.getCommandsByAction(action); -// std::list commands; -// -// // 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::ir::Command const& command = module.getCommand(commandIndex); -// if (command.getGuard()->getValueAsBool(state)) { -// commands.push_back(command); -// } -// } -// -// // If there was no enabled command although the module has some command with the required action label, -// // we must not return anything. -// if (commands.size() == 0) { -// return boost::optional>>(); -// } -// -// result.get().push_back(std::move(commands)); -// } -// return result; -// } - -// void ExplicitModelAdapter::addUnlabeledTransitions(uint_fast64_t stateIndex, std::list>, std::map>>& transitionList) { -// StateType const* state = this->allStates[stateIndex]; -// -// // Iterate over all modules. -// for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { -// storm::ir::Module const& module = program.getModule(i); -// -// // Iterate over all commands. -// for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) { -// storm::ir::Command const& command = module.getCommand(j); -// -// // Only consider unlabeled commands. -// if (command.getActionName() != "") continue; -// // Skip the command, if it is not enabled. -// if (!command.getGuard()->getValueAsBool(state)) continue; -// -// // Add a new choice for the state. -// transitionList.emplace_back(); -// -// // Add the index of the current command to the labeling of the choice. -// transitionList.back().first.second.emplace_back(command.getGlobalIndex()); -// -// // Create an alias for all target states for convenience. -// std::map& targetStates = transitionList.back().second; -// -// // Also keep track of the total probability leaving the state. -// double probabilitySum = 0; -// -// // Iterate over all updates of the current command. -// for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { -// storm::ir::Update const& update = command.getUpdate(k); -// -// // Obtain target state index. -// uint_fast64_t newTargetStateIndex = this->getOrAddStateIndex(this->applyUpdate(state, update)); -// -// probabilitySum += update.getLikelihoodExpression()->getValueAsDouble(state); -// -// // Check, if we already saw this state in another update and, if so, add up probabilities. -// auto stateIt = targetStates.find(newTargetStateIndex); -// if (stateIt == targetStates.end()) { -// targetStates[newTargetStateIndex] = update.getLikelihoodExpression()->getValueAsDouble(state); -// this->numberOfTransitions++; -// } else { -// targetStates[newTargetStateIndex] += update.getLikelihoodExpression()->getValueAsDouble(state); -// } -// } -// -// if (std::abs(1 - probabilitySum) > this->precision) { -// LOG4CPLUS_ERROR(logger, "Sum of update probabilities should be one for command:\n\t" << command.toString()); -// throw storm::exceptions::WrongFormatException() << "Sum of update probabilities should be one for command:\n\t" << command.toString(); -// } -// } -// } -// } - -// void ExplicitModelAdapter::addLabeledTransitions(uint_fast64_t stateIndex, std::list>, std::map>>& transitionList) { -// for (std::string const& action : this->program.getActions()) { -// StateType* currentState = this->allStates[stateIndex]; -// boost::optional>> optionalActiveCommandLists = this->getActiveCommandsByAction(currentState, action); -// -// // Only process this action label, if there is at least one feasible solution. -// if (optionalActiveCommandLists) { -// std::vector> const& activeCommandList = optionalActiveCommandLists.get(); -// std::vector::const_iterator> iteratorList(activeCommandList.size()); -// -// // Initialize the list of iterators. -// for (size_t i = 0; i < activeCommandList.size(); ++i) { -// iteratorList[i] = activeCommandList[i].cbegin(); -// } -// -// // As long as there is one feasible combination of commands, keep on expanding it. -// bool done = false; -// while (!done) { -// std::unordered_map* currentTargetStates = new std::unordered_map(); -// std::unordered_map* newTargetStates = new std::unordered_map(); -// (*currentTargetStates)[new StateType(*currentState)] = 1.0; -// -// // 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. -// double probabilitySum = 0; -// for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { -// storm::ir::Command const& command = *iteratorList[i]; -// -// for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { -// storm::ir::Update const& update = command.getUpdate(j); -// -// for (auto const& stateProbabilityPair : *currentTargetStates) { -// StateType* newTargetState = this->applyUpdate(stateProbabilityPair.first, currentState, update); -// probabilitySum += stateProbabilityPair.second * update.getLikelihoodExpression()->getValueAsDouble(currentState); -// -// auto existingStateProbabilityPair = newTargetStates->find(newTargetState); -// if (existingStateProbabilityPair == newTargetStates->end()) { -// (*newTargetStates)[newTargetState] = stateProbabilityPair.second * update.getLikelihoodExpression()->getValueAsDouble(currentState); -// } else { -// existingStateProbabilityPair->second += stateProbabilityPair.second * update.getLikelihoodExpression()->getValueAsDouble(currentState); -// } -// } -// } -// -// // 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(); -// } -// } -// -// // 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. -// transitionList.emplace_back(std::make_pair(std::make_pair(action, std::list()), std::map())); -// -// // Add the commands that were involved in creating this distribution to the labeling. -// for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { -// transitionList.back().first.second.push_back(iteratorList[i]->getGlobalIndex()); -// } -// -// // Now create the actual distribution. -// std::map& states = transitionList.back().second; -// for (auto const& stateProbabilityPair : *newTargetStates) { -// uint_fast64_t newStateIndex = this->getOrAddStateIndex(stateProbabilityPair.first); -// states[newStateIndex] = stateProbabilityPair.second; -// } -// this->numberOfTransitions += states.size(); -// -// // Dispose of the temporary maps. -// delete currentTargetStates; -// delete newTargetStates; -// -// // Now, check whether there is one more command combination to consider. -// bool movedIterator = false; -// for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) { -// ++iteratorList[j]; -// if (iteratorList[j] != activeCommandList[j].end()) { -// movedIterator = true; -// } else { -// // Reset the iterator to the beginning of the list. -// iteratorList[j] = activeCommandList[j].begin(); -// } -// } -// -// done = !movedIterator; -// } -// } -// } -// } - -// storm::storage::SparseMatrix ExplicitModelAdapter::buildDeterministicMatrix() { -// // Note: this->numberOfTransitions may be meaningless here, as we need to combine all nondeterministic -// // choices for all states into one determinstic one, which might reduce the number of transitions. -// // Hence, we compute the correct number now. -// uint_fast64_t numberOfTransitions = 0; -// for (uint_fast64_t state = 0; state < this->allStates.size(); ++state) { -// // Collect all target nodes in a set to get the number of distinct nodes. -// std::set set; -// for (auto const& choice : transitionMap[state]) { -// for (auto const& targetStates : choice.second) { -// set.insert(targetStates.first); -// } -// } -// numberOfTransitions += set.size(); -// } -// -// LOG4CPLUS_INFO(logger, "Building deterministic transition matrix: " << allStates.size() << " x " << allStates.size() << " with " << numberOfTransitions << " transitions."); -// -// this->choiceLabeling.clear(); -// this->choiceLabeling.reserve(allStates.size()); -// -// // Now build the actual matrix. -// storm::storage::SparseMatrix result(allStates.size()); -// result.initialize(numberOfTransitions); -// if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { -// this->transitionRewards.reset(std::move(storm::storage::SparseMatrix(allStates.size()))); -// this->transitionRewards.get().initialize(numberOfTransitions); -// } -// -// for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { -// if (transitionMap[state].size() > 1) { -// LOG4CPLUS_WARN(logger, "State " << state << " has " << transitionMap[state].size() << " overlapping guards in deterministic model."); -// } -// -// // Combine nondeterministic choices into one by weighting them equally. -// std::map map; -// std::map rewardMap; -// std::list commandList; -// for (auto const& choice : transitionMap[state]) { -// commandList.insert(commandList.end(), choice.first.second.begin(), choice.first.second.end()); -// for (auto const& targetStates : choice.second) { -// map[targetStates.first] += targetStates.second; -// if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { -// for (auto const& reward : this->rewardModel->getTransitionRewards()) { -// if (reward.getStatePredicate()->getValueAsBool(this->allStates[state]) == true) { -// rewardMap[targetStates.first] += reward.getRewardValue()->getValueAsDouble(this->allStates[state]); -// } -// } -// } -// } -// } -// // Make sure that each command is only added once to the label of the transition. -// commandList.sort(); -// commandList.unique(); -// -// // Add the labeling for the behaviour of the current state. -// this->choiceLabeling.emplace_back(std::move(commandList)); -// -// // Scale probabilities by number of choices. -// double factor = 1.0 / transitionMap[state].size(); -// for (auto& targetStates : map) { -// result.addNextValue(state, targetStates.first, targetStates.second * factor); -// if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { -// this->transitionRewards.get().addNextValue(state, targetStates.first, rewardMap[targetStates.first] * factor); -// } -// } -// -// } -// -// result.finalize(); -// return result; -// } - -// storm::storage::SparseMatrix ExplicitModelAdapter::buildNondeterministicMatrix() { -// LOG4CPLUS_INFO(logger, "Building nondeterministic transition matrix: " << this->numberOfChoices << " x " << allStates.size() << " with " << this->numberOfTransitions << " transitions."); -// storm::storage::SparseMatrix result(this->numberOfChoices, allStates.size()); -// result.initialize(this->numberOfTransitions); -// if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { -// this->transitionRewards.reset(storm::storage::SparseMatrix(this->numberOfChoices, allStates.size())); -// this->transitionRewards.get().initialize(this->numberOfTransitions); -// } -// this->choiceIndices.clear(); -// this->choiceIndices.reserve(allStates.size() + 1); -// this->choiceLabeling.clear(); -// this->choiceLabeling.reserve(allStates.size()); -// -// // Now build the actual matrix. -// uint_fast64_t nextRow = 0; -// this->choiceIndices.push_back(0); -// for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { -// this->choiceIndices.push_back(this->choiceIndices[state] + transitionMap[state].size()); -// for (auto const& choice : transitionMap[state]) { -// this->choiceLabeling.emplace_back(std::move(choice.first.second)); -// for (auto const& targetStates : choice.second) { -// result.addNextValue(nextRow, targetStates.first, targetStates.second); -// if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { -// double rewardValue = 0; -// for (auto const& reward : this->rewardModel->getTransitionRewards()) { -// if (reward.getStatePredicate()->getValueAsBool(this->allStates[state]) == true) { -// rewardValue = reward.getRewardValue()->getValueAsDouble(this->allStates[state]); -// } -// } -// this->transitionRewards.get().addNextValue(nextRow, targetStates.first, rewardValue); -// } -// } -// ++nextRow; -// } -// } -// -// result.finalize(); -// return result; -// } - -// void ExplicitModelAdapter::buildTransitionMap() { -// LOG4CPLUS_DEBUG(logger, "Creating transition map from program."); -// this->clearInternalState(); -// this->allStates.clear(); -// this->allStates.push_back(this->getInitialState()); -// stateToIndexMap[this->allStates[0]] = 0; -// -// for (uint_fast64_t state = 0; state < this->allStates.size(); ++state) { -// this->addUnlabeledTransitions(state, this->transitionMap[state]); -// this->addLabeledTransitions(state, this->transitionMap[state]); -// -// this->numberOfChoices += this->transitionMap[state].size(); -// -// // Check whether the current state is a deadlock state and treat it accordingly. -// if (this->transitionMap[state].size() == 0) { -// if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { -// ++this->numberOfTransitions; -// ++this->numberOfChoices; -// this->transitionMap[state].emplace_back(); -// this->transitionMap[state].back().second[state] = 1; -// } else { -// LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); -// throw storm::exceptions::WrongFormatException() << "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."; -// } -// } -// } -// -// LOG4CPLUS_DEBUG(logger, "Finished creating transition map."); -// } - - } // namespace adapters -} // namespace storm diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index f82b4dcee..20d2c1133 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -75,10 +75,20 @@ namespace storm { // A structure holding information about a particular choice. template struct Choice { + public: 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::iterator begin() { + return distribution.begin(); + } + /*! * Returns an iterator to the first element of this choice. * @@ -88,6 +98,15 @@ namespace storm { 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::iterator end() { + return distribution.end(); + } + /*! * Returns an iterator that points past the elements of this choice. * @@ -97,6 +116,31 @@ namespace storm { return distribution.cend(); } + /*! + * Returns an iterator to the element with the given key, if there is one. Otherwise, the iterator points to + * distribution.end(). + * + * @param value The value to find. + * @return An iterator to the element with the given key, if there is one. + */ + typename std::map::iterator find(uint_fast64_t value) { + return distribution.find(value); + } + + /*! + * 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, Choice const& choice) { + out << "<"; + for (auto const& stateProbabilityPair : choice.distribution) { + out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", "; + } + out << ">"; + return out; + } + /*! * Adds the given label to the labels associated with this choice. * @@ -106,6 +150,68 @@ namespace storm { choiceLabels.insert(label); } + /*! + * Adds the given label set to the labels associated with this choice. + * + * @param labelSet The label set to associate with this choice. + */ + void addChoiceLabels(std::set const& labelSet) { + for (uint_fast64_t label : labelSet) { + addChoiceLabel(label); + } + } + + /*! + * Retrieves the set of labels associated with this choice. + * + * @return The set of labels associated with this choice. + */ + std::set const& getChoiceLabels() const { + return choiceLabels; + } + + /*! + * Retrieves the action label of this choice. + * + * @return The action label of this choice. + */ + std::string const& getActionLabel() const { + return actionLabel; + } + + /*! + * Retrieves the entry in the choice that is associated with the given state and creates one if none exists, + * yet. + * + * @param state The state for which to add the entry. + * @return A reference to the entry that is associated with the given state. + */ + ValueType& getOrAddEntry(uint_fast64_t state) { + auto stateProbabilityPair = distribution.find(state); + + if (stateProbabilityPair == distribution.end()) { + distribution[state] = ValueType(); + } + return distribution.at(state); + } + + /*! + * Retrieves the entry in the choice that is associated with the given state and creates one if none exists, + * yet. + * + * @param state The state for which to add the entry. + * @return A reference to the entry that is associated with the given state. + */ + ValueType const& getOrAddEntry(uint_fast64_t state) const { + auto stateProbabilityPair = distribution.find(state); + + if (stateProbabilityPair == distribution.end()) { + distribution[state] = ValueType(); + } + return distribution.at(state); + } + + private: // The distribution that is associated with the choice. std::map distribution; @@ -116,25 +222,34 @@ namespace storm { std::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, std::set const& labels) { - auto stateProbabilityPair = choice.distribution.find(state); - - if (stateProbabilityPair == choice.distribution.end()) { - choice.distribution[state] = probability; - } else { - choice.distribution[state] += probability; - } + 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, 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); + auto& labeledEntry = choice.getOrAddEntry(state); + labeledEntry.addValue(probability, labels); } template @@ -794,13 +909,10 @@ namespace storm { // Obtain target state index. 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. + // Update the choice by adding the probability/target state to it. 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); + addProbabilityToChoice(choice, targetStateIndex, probabilityToAdd, {update.getGlobalIndex()}); } // Check that the resulting distribution is in fact a distribution. @@ -952,38 +1064,29 @@ namespace storm { // Then, based on whether the model is deterministic or not, either add the choices individually // or compose them to one choice. if (deterministicModel) { - std::map globalDistribution; + Choice globalChoice(""); std::set allChoiceLabels; // Combine all the choices and scale them with the total number of choices of the current state. for (auto const& choice : allUnlabeledChoices) { - allChoiceLabels.insert(choice.choiceLabels.begin(), choice.choiceLabels.end()); + globalChoice.addChoiceLabels(choice.getChoiceLabels()); 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; - } + globalChoice.getOrAddEntry(stateProbabilityPair.first) += stateProbabilityPair.second / totalNumberOfChoices; } } for (auto const& choice : allLabeledChoices) { + globalChoice.addChoiceLabels(choice.getChoiceLabels()); 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; - } + globalChoice.getOrAddEntry(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); + choiceLabels.push_back(globalChoice.getChoiceLabels()); - for (auto const& stateProbabilityPair : globalDistribution) { + for (auto const& stateProbabilityPair : globalChoice) { transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); } @@ -995,7 +1098,7 @@ namespace storm { // First, process all unlabeled choices. for (auto const& choice : allUnlabeledChoices) { std::map stateToRewardMap; - choiceLabels.emplace_back(std::move(choice.choiceLabels)); + choiceLabels.emplace_back(std::move(choice.getChoiceLabels())); for (auto const& stateProbabilityPair : choice) { transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); @@ -1003,7 +1106,7 @@ namespace storm { // 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)); + stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates.at(currentState))); } } @@ -1020,7 +1123,7 @@ namespace storm { // Then, process all labeled choices. for (auto const& choice : allLabeledChoices) { std::map stateToRewardMap; - choiceLabels.emplace_back(std::move(choice.choiceLabels)); + choiceLabels.emplace_back(std::move(choice.getChoiceLabels())); for (auto const& stateProbabilityPair : choice) { transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); @@ -1028,7 +1131,7 @@ namespace storm { // 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)); + stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates.at(currentState))); } } @@ -1141,11 +1244,11 @@ namespace storm { static std::vector buildStateRewards(std::vector const& rewards, StateInformation const& stateInformation) { std::vector result(stateInformation.reachableStates.size()); for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { - result[index] = 0; + result[index] = ValueType(0); for (auto const& reward : rewards) { // Add this reward to the state if the state is included in the state reward. if (reward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates[index])) { - result[index] += reward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates[index]); + result[index] += ValueType(reward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates[index])); } } } diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp index db701239d..80e698b64 100644 --- a/src/ir/Command.cpp +++ b/src/ir/Command.cpp @@ -31,7 +31,7 @@ namespace storm { } this->updates.reserve(oldCommand.getNumberOfUpdates()); for (Update const& update : oldCommand.updates) { - this->updates.emplace_back(update, renaming, variableState); + this->updates.emplace_back(update, variableState.getNextGlobalUpdateIndex(), renaming, variableState); } } diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp index 1c66789c6..cade7f022 100644 --- a/src/ir/Update.cpp +++ b/src/ir/Update.cpp @@ -14,16 +14,16 @@ namespace storm { namespace ir { - Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments() { + Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments(), globalIndex() { // Nothing to do here. } - Update::Update(std::shared_ptr const& likelihoodExpression, std::map const& booleanAssignments, std::map const& integerAssignments) - : likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments) { + Update::Update(uint_fast64_t globalIndex, std::shared_ptr const& likelihoodExpression, std::map const& booleanAssignments, std::map const& integerAssignments) + : likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) { // Nothing to do here. } - Update::Update(Update const& update, std::map const& renaming, storm::parser::prism::VariableState const& variableState) { + Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState) : globalIndex(newGlobalIndex) { for (auto const& variableAssignmentPair : update.booleanAssignments) { if (renaming.count(variableAssignmentPair.first) > 0) { this->booleanAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, variableState); @@ -81,6 +81,10 @@ namespace storm { return variableAssignmentPair->second; } + uint_fast64_t Update::getGlobalIndex() const { + return this->globalIndex; + } + std::string Update::toString() const { std::stringstream result; result << likelihoodExpression->toString() << " : "; diff --git a/src/ir/Update.h b/src/ir/Update.h index 4fe4b05be..df7d4a258 100644 --- a/src/ir/Update.h +++ b/src/ir/Update.h @@ -38,20 +38,22 @@ namespace storm { * Creates an update with the given expression specifying the likelihood and the mapping of * variable to their assignments. * + * @param globalIndex The global index of the update. * @param likelihoodExpression An expression specifying the likelihood of this update. * @param assignments A map of variable names to their assignments. */ - Update(std::shared_ptr const& likelihoodExpression, std::map const& booleanAssignments, std::map const& integerAssignments); + Update(uint_fast64_t globalIndex, std::shared_ptr const& likelihoodExpression, std::map const& booleanAssignments, std::map const& integerAssignments); /*! * Creates a copy of the given update and performs the provided renaming. * - * update The update that is to be copied. - * renaming A mapping from names that are to be renamed to the names they are to be + * @param update The update that is to be copied. + * @param newGlobalIndex The global index of the resulting update. + * @param renaming A mapping from names that are to be renamed to the names they are to be * replaced with. * @param variableState An object knowing about the variables in the system. */ - Update(Update const& update, std::map const& renaming, storm::parser::prism::VariableState const& variableState); + Update(Update const& update, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState); /*! * Retrieves the expression for the likelihood of this update. @@ -102,6 +104,13 @@ namespace storm { */ storm::ir::Assignment const& getIntegerAssignment(std::string const& variableName) const; + /*! + * Retrieves the global index of the update, that is, a unique index over all modules. + * + * @return The global index of the update. + */ + uint_fast64_t getGlobalIndex() const; + /*! * Retrieves a string representation of this update. * @@ -118,6 +127,9 @@ namespace storm { // A mapping of integer variable names to their assignments in this update. std::map integerAssignments; + + // The global index of the update. + uint_fast64_t globalIndex; }; } // namespace ir diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index 99dbf0efd..0caa9b6aa 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -111,8 +111,9 @@ TransitionReward createTransitionReward(std::string const& label, std::shared_pt void createRewardModel(std::string const& name, std::vector& stateRewards, std::vector& transitionRewards, std::map& mapping) { mapping[name] = RewardModel(name, stateRewards, transitionRewards); } -Update createUpdate(std::shared_ptr likelihood, std::map const& bools, std::map const& ints) { - return Update(likelihood, bools, ints); +Update PrismGrammar::createUpdate(std::shared_ptr likelihood, std::map const& bools, std::map const& ints) { + this->state->nextGlobalUpdateIndex++; + return Update(this->state->getNextGlobalUpdateIndex() - 1, likelihood, bools, ints); } Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr guard, std::vector const& updates) { this->state->nextGlobalCommandIndex++; @@ -166,8 +167,7 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl assignmentDefinition.name("assignment"); assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; assignmentDefinitionList.name("assignment list"); - updateDefinition = ( - ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)]; + updateDefinition = (ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)]; updateDefinition.name("update"); updateListDefinition = +updateDefinition % "+"; updateListDefinition.name("update list"); diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index d953d67fa..7dd8e80a0 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -1,12 +1,12 @@ -/* +/* * File: PrismGrammar.h * Author: nafur * * Created on April 30, 2013, 5:20 PM */ -#ifndef PRISMGRAMMAR_H -#define PRISMGRAMMAR_H +#ifndef STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H +#define STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H // All classes of the intermediate representation are used. #include "src/ir/IR.h" @@ -25,227 +25,236 @@ #include namespace storm { -namespace parser { -namespace prism { - -using namespace storm::ir; -using namespace storm::ir::expressions; - -struct GlobalVariableInformation { - std::vector booleanVariables; - std::vector integerVariables; - std::map booleanVariableToIndexMap; - std::map integerVariableToIndexMap; -}; - -/*! - * The Boost spirit grammar for the PRISM language. Returns the intermediate representation of - * the input that complies with the PRISM syntax. - */ -class PrismGrammar : public qi::grammar< - Iterator, - Program(), - qi::locals< - std::map>, - std::map>, - std::map>, - GlobalVariableInformation, - std::map, - std::map> - >, - Skipper> { -public: - /*! - * Default constructor that creates an empty and functional grammar. - */ - PrismGrammar(); - - /*! - * Puts all sub-grammars into the mode for performing the second run. A two-run model was chosen - * because modules can involve variables that are only declared afterwards, so the first run - * creates all variables and the second one tries to parse the full model. - */ - void prepareForSecondRun(); - - /*! - * Resets all sub-grammars, i.e. puts them into an initial state. - */ - void resetGrammars(); - -private: - - std::shared_ptr state; - struct qi::symbols moduleMap_; - - // The starting point of the grammar. - qi::rule< - Iterator, - Program(), - qi::locals< + namespace parser { + namespace prism { + + using namespace storm::ir; + using namespace storm::ir::expressions; + + struct GlobalVariableInformation { + std::vector booleanVariables; + std::vector integerVariables; + std::map booleanVariableToIndexMap; + std::map integerVariableToIndexMap; + }; + + /*! + * The Boost spirit grammar for the PRISM language. Returns the intermediate representation of + * the input that complies with the PRISM syntax. + */ + class PrismGrammar : public qi::grammar< + Iterator, + Program(), + qi::locals< + std::map>, + std::map>, + std::map>, + GlobalVariableInformation, + std::map, + std::map> + >, + Skipper> { + public: + /*! + * Default constructor that creates an empty and functional grammar. + */ + PrismGrammar(); + + /*! + * Puts all sub-grammars into the mode for performing the second run. A two-run model was chosen + * because modules can involve variables that are only declared afterwards, so the first run + * creates all variables and the second one tries to parse the full model. + */ + void prepareForSecondRun(); + + /*! + * Resets all sub-grammars, i.e. puts them into an initial state. + */ + void resetGrammars(); + + private: + + std::shared_ptr state; + struct qi::symbols moduleMap_; + + // The starting point of the grammar. + qi::rule< + Iterator, + Program(), + qi::locals< std::map>, std::map>, std::map>, GlobalVariableInformation, std::map, std::map> - >, - Skipper> start; - qi::rule modelTypeDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; - qi::rule(), Skipper> moduleDefinitionList; - - // Rules for global variable definitions - qi::rule globalVariableDefinitionList; - - // Rules for module definition. - qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; - qi::rule>, Skipper> moduleRenaming; - - // Rules for variable definitions. - qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; - qi::rule&, std::map&, bool), qi::locals>, Skipper> booleanVariableDefinition; - qi::rule&, std::map&, bool), qi::locals>, Skipper> integerVariableDefinition; - - // Rules for command definitions. - qi::rule, Skipper> commandDefinition; - qi::rule(), Skipper> updateListDefinition; - qi::rule, std::map>, Skipper> updateDefinition; - qi::rule&, std::map&), Skipper> assignmentDefinitionList; - qi::rule&, std::map&), Skipper> assignmentDefinition; - - // Rules for variable/command names. - qi::rule commandName; - qi::rule unassignedLocalBooleanVariableName; - qi::rule unassignedLocalIntegerVariableName; - - // Rules for reward definitions. - qi::rule&), Skipper> rewardDefinitionList; - qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; - qi::rule stateRewardDefinition; - qi::rule, Skipper> transitionRewardDefinition; - - // Rules for label definitions. - qi::rule>&), Skipper> labelDefinitionList; - qi::rule>&), Skipper> labelDefinition; - - // Rules for constant definitions. - qi::rule(), Skipper> constantDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; - qi::rule(), Skipper> definedConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; - qi::rule(), Skipper> definedBooleanConstantDefinition; - qi::rule(), Skipper> definedIntegerConstantDefinition; - qi::rule(), Skipper> definedDoubleConstantDefinition; - - // Rules for variable recognition. - qi::rule(), Skipper> booleanVariableCreatorExpression; - qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; - - storm::parser::prism::keywordsStruct keywords_; - storm::parser::prism::modelTypeStruct modelType_; - storm::parser::prism::relationalOperatorStruct relations_; - - /*! - * Adds a constant of type integer with the given name and value. - * - * @param name The name of the constant. - * @param value An expression definining the value of the constant. - */ - std::shared_ptr addIntegerConstant(std::string const& name, std::shared_ptr const& value); - - /*! - * Adds a label with the given name and expression to the given label-to-expression map. - * - * @param name The name of the label. - * @param expression The expression associated with the label. - * @param nameToExpressionMap The map to which the label is added. - */ - void addLabel(std::string const& name, std::shared_ptr const& value, std::map>& nameToExpressionMap); - - /*! - * Adds a boolean assignment for the given variable with the given expression and adds it to the - * provided variable-to-assignment map. - * - * @param variable The name of the variable that the assignment targets. - * @param expression The expression that is assigned to the variable. - * @param variableToAssignmentMap The map to which the assignment is added. - */ - void addBooleanAssignment(std::string const& variable, std::shared_ptr const& expression, std::map& variableToAssignmentMap); - - /*! - * Adds a boolean assignment for the given variable with the given expression and adds it to the - * provided variable-to-assignment map. - * - * @param variable The name of the variable that the assignment targets. - * @param expression The expression that is assigned to the variable. - * @param variableToAssignmentMap The map to which the assignment is added. - */ - void addIntegerAssignment(std::string const& variable, std::shared_ptr const& value, std::map& variableToAssignmentMap); - - /*! - * Creates a module by renaming, i.e. takes the module given by the old name, creates a new module - * with the given name which renames all identifiers according to the given mapping. - * - * @param name The name of the new module. - * @param oldName The name of the module that is to be copied (modulo renaming). - * @param renaming A mapping from identifiers to their new names. - */ - Module renameModule(std::string const& name, std::string const& oldName, std::map const& renaming); - - /*! - * Creates a new module with the given name, boolean and integer variables and commands. - * - * @param name The name of the module to create. - * @param booleanVariables The boolean variables of the module. - * @param integerVariables The integer variables of the module. - * @param booleanVariableToLocalIndexMap A mapping of boolean variables to module-local indices. - * @param integerVariableToLocalIndexMap A mapping of boolean variables to module-local indices. - * @param commands The commands associated with this module. - */ - Module createModule(std::string const& name, std::vector const& booleanVariables, std::vector const& integerVariables, std::map const& booleanVariableToLocalIndexMap, std::map const& integerVariableToLocalIndexMap, std::vector const& commands); - - /*! - * Creates an integer variable with the given name, domain and initial value and adds it to the - * provided list of integer variables and the given mappings. - * - * @param name The name of the integer variable. - * @param lower The expression that defines the lower bound of the domain. - * @param upper The expression that defines the upper bound of the domain. - * @param init The expression that defines the initial value of the variable. - * @param integerVariableToGlobalIndexMap A mapping of integer variables to global indices. - * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not. - */ - void createIntegerVariable(std::string const& name, std::shared_ptr const& lower, std::shared_ptr const& upper, std::shared_ptr const& init, std::vector& integerVariables, std::map& integerVariableToGlobalIndexMap, bool isGlobalVariable); - - /*! - * Creates an boolean variable with the given name and initial value and adds it to the - * provided list of boolean variables and the given mappings. - * - * @param name The name of the boolean variable. - * @param init The expression that defines the initial value of the variable. - * @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices. - * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not. - */ - void createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& booleanVariables, std::map& booleanVariableToGlobalIndexMap, bool isGlobalVariable); - - /*! - * Creates a command with the given label, guard and updates. - * - * @param label The label of the command. - * @param guard The guard of the command. - * @param updates The updates associated with the command. - */ - Command createCommand(std::string const& label, std::shared_ptr guard, std::vector const& updates); - -}; - - -} // namespace prism -} // namespace parser + >, + Skipper> start; + qi::rule modelTypeDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; + qi::rule(), Skipper> moduleDefinitionList; + + // Rules for global variable definitions + qi::rule globalVariableDefinitionList; + + // Rules for module definition. + qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; + qi::rule>, Skipper> moduleRenaming; + + // Rules for variable definitions. + qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; + qi::rule&, std::map&, bool), qi::locals>, Skipper> booleanVariableDefinition; + qi::rule&, std::map&, bool), qi::locals>, Skipper> integerVariableDefinition; + + // Rules for command definitions. + qi::rule, Skipper> commandDefinition; + qi::rule(), Skipper> updateListDefinition; + qi::rule, std::map>, Skipper> updateDefinition; + qi::rule&, std::map&), Skipper> assignmentDefinitionList; + qi::rule&, std::map&), Skipper> assignmentDefinition; + + // Rules for variable/command names. + qi::rule commandName; + qi::rule unassignedLocalBooleanVariableName; + qi::rule unassignedLocalIntegerVariableName; + + // Rules for reward definitions. + qi::rule&), Skipper> rewardDefinitionList; + qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; + qi::rule stateRewardDefinition; + qi::rule, Skipper> transitionRewardDefinition; + + // Rules for label definitions. + qi::rule>&), Skipper> labelDefinitionList; + qi::rule>&), Skipper> labelDefinition; + + // Rules for constant definitions. + qi::rule(), Skipper> constantDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; + qi::rule(), Skipper> definedConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; + qi::rule(), Skipper> definedBooleanConstantDefinition; + qi::rule(), Skipper> definedIntegerConstantDefinition; + qi::rule(), Skipper> definedDoubleConstantDefinition; + + // Rules for variable recognition. + qi::rule(), Skipper> booleanVariableCreatorExpression; + qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; + + storm::parser::prism::keywordsStruct keywords_; + storm::parser::prism::modelTypeStruct modelType_; + storm::parser::prism::relationalOperatorStruct relations_; + + /*! + * Adds a constant of type integer with the given name and value. + * + * @param name The name of the constant. + * @param value An expression definining the value of the constant. + */ + std::shared_ptr addIntegerConstant(std::string const& name, std::shared_ptr const& value); + + /*! + * Adds a label with the given name and expression to the given label-to-expression map. + * + * @param name The name of the label. + * @param expression The expression associated with the label. + * @param nameToExpressionMap The map to which the label is added. + */ + void addLabel(std::string const& name, std::shared_ptr const& value, std::map>& nameToExpressionMap); + + /*! + * Adds a boolean assignment for the given variable with the given expression and adds it to the + * provided variable-to-assignment map. + * + * @param variable The name of the variable that the assignment targets. + * @param expression The expression that is assigned to the variable. + * @param variableToAssignmentMap The map to which the assignment is added. + */ + void addBooleanAssignment(std::string const& variable, std::shared_ptr const& expression, std::map& variableToAssignmentMap); + + /*! + * Adds a boolean assignment for the given variable with the given expression and adds it to the + * provided variable-to-assignment map. + * + * @param variable The name of the variable that the assignment targets. + * @param expression The expression that is assigned to the variable. + * @param variableToAssignmentMap The map to which the assignment is added. + */ + void addIntegerAssignment(std::string const& variable, std::shared_ptr const& value, std::map& variableToAssignmentMap); + + /*! + * Creates a module by renaming, i.e. takes the module given by the old name, creates a new module + * with the given name which renames all identifiers according to the given mapping. + * + * @param name The name of the new module. + * @param oldName The name of the module that is to be copied (modulo renaming). + * @param renaming A mapping from identifiers to their new names. + */ + Module renameModule(std::string const& name, std::string const& oldName, std::map const& renaming); + + /*! + * Creates a new module with the given name, boolean and integer variables and commands. + * + * @param name The name of the module to create. + * @param booleanVariables The boolean variables of the module. + * @param integerVariables The integer variables of the module. + * @param booleanVariableToLocalIndexMap A mapping of boolean variables to module-local indices. + * @param integerVariableToLocalIndexMap A mapping of boolean variables to module-local indices. + * @param commands The commands associated with this module. + */ + Module createModule(std::string const& name, std::vector const& booleanVariables, std::vector const& integerVariables, std::map const& booleanVariableToLocalIndexMap, std::map const& integerVariableToLocalIndexMap, std::vector const& commands); + + /*! + * Creates an integer variable with the given name, domain and initial value and adds it to the + * provided list of integer variables and the given mappings. + * + * @param name The name of the integer variable. + * @param lower The expression that defines the lower bound of the domain. + * @param upper The expression that defines the upper bound of the domain. + * @param init The expression that defines the initial value of the variable. + * @param integerVariableToGlobalIndexMap A mapping of integer variables to global indices. + * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not. + */ + void createIntegerVariable(std::string const& name, std::shared_ptr const& lower, std::shared_ptr const& upper, std::shared_ptr const& init, std::vector& integerVariables, std::map& integerVariableToGlobalIndexMap, bool isGlobalVariable); + + /*! + * Creates an boolean variable with the given name and initial value and adds it to the + * provided list of boolean variables and the given mappings. + * + * @param name The name of the boolean variable. + * @param init The expression that defines the initial value of the variable. + * @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices. + * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not. + */ + void createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& booleanVariables, std::map& booleanVariableToGlobalIndexMap, bool isGlobalVariable); + + /*! + * Creates a command with the given label, guard and updates. + * + * @param label The label of the command. + * @param guard The guard of the command. + * @param updates The updates associated with the command. + */ + Command createCommand(std::string const& label, std::shared_ptr guard, std::vector const& updates); + + /*! + * Creates an update with the given likelihood and the given assignments to boolean and integer variables, respectively. + * + * @param likelihood The likelihood of this update being executed. + * @param booleanAssignments The assignments to boolean variables this update involves. + * @param integerAssignments The assignments to integer variables this update involves. + */ + Update createUpdate(std::shared_ptr likelihood, std::map const& booleanAssignments, std::map const& integerAssignments); + + }; + + + } // namespace prism + } // namespace parser } // namespace storm -#endif /* PRISMGRAMMAR_H */ +#endif /* STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H */ diff --git a/src/parser/prismparser/VariableState.cpp b/src/parser/prismparser/VariableState.cpp index fd2e5e217..045b4dee6 100644 --- a/src/parser/prismparser/VariableState.cpp +++ b/src/parser/prismparser/VariableState.cpp @@ -2,172 +2,177 @@ #include "src/exceptions/InvalidArgumentException.h" namespace storm { -namespace parser { -namespace prism { - -using namespace storm::ir; -using namespace storm::ir::expressions; - -template -struct SymbolDump { - SymbolDump(std::ostream& out) : out(out) {} - void operator() (std::basic_string s, T elem) { - this->out << "\t" << s << " -> " << elem << std::endl; - } -private: - std::ostream& out; -}; -template -std::ostream& operator<<(std::ostream& out, qi::symbols& symbols) { - out << "Dumping symbol table" << std::endl; - SymbolDump dump(out); - symbols.for_each(dump); - return out; -} -std::ostream& operator<<(std::ostream& out, VariableState::variableNamesStruct& symbols) { - SymbolDump dump(out); - symbols.for_each(dump); - return out; -} - - -VariableState::VariableState(bool firstRun) : firstRun(firstRun), keywords(), nextLocalBooleanVariableIndex(0), nextLocalIntegerVariableIndex(0), nextGlobalBooleanVariableIndex(0), nextGlobalIntegerVariableIndex(0), nextGlobalCommandIndex(0) { - // Nothing to do here. -} - -uint_fast64_t VariableState::getNextLocalBooleanVariableIndex() const { - return this->nextLocalBooleanVariableIndex; -} - -uint_fast64_t VariableState::getNextLocalIntegerVariableIndex() const { - return this->nextLocalIntegerVariableIndex; -} - -uint_fast64_t VariableState::getNextGlobalBooleanVariableIndex() const { - return this->nextGlobalBooleanVariableIndex; -} - -uint_fast64_t VariableState::getNextGlobalIntegerVariableIndex() const { - return this->nextGlobalIntegerVariableIndex; -} - -uint_fast64_t VariableState::getNextGlobalCommandIndex() const { - return this->nextGlobalCommandIndex; -} - -uint_fast64_t VariableState::addBooleanVariable(std::string const& name) { - if (firstRun) { - LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextGlobalBooleanVariableIndex << "."); - this->booleanVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextGlobalBooleanVariableIndex, name))); - this->booleanVariableNames_.add(name, name); - ++this->nextGlobalBooleanVariableIndex; - ++this->nextLocalBooleanVariableIndex; - return this->nextGlobalBooleanVariableIndex - 1; - } else { - std::shared_ptr variableExpression = this->booleanVariables_.at(name); - if (variableExpression != nullptr) { - return variableExpression->getGlobalVariableIndex(); - } else { - LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist."); - throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist."; - } - } -} - -uint_fast64_t VariableState::addIntegerVariable(std::string const& name) { - if (firstRun) { - LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextGlobalIntegerVariableIndex << "."); - this->integerVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextGlobalIntegerVariableIndex, name))); - this->integerVariableNames_.add(name, name); - ++this->nextGlobalIntegerVariableIndex; - ++this->nextLocalIntegerVariableIndex; - return this->nextGlobalIntegerVariableIndex - 1; - } else { - std::shared_ptr variableExpression = this->integerVariables_.at(name); - if (variableExpression != nullptr) { - return variableExpression->getGlobalVariableIndex(); - } else { - LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist."); - throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist."; - } - } -} - -std::shared_ptr VariableState::getBooleanVariableExpression(std::string const& name) const { - std::shared_ptr const* variableExpression = this->booleanVariables_.find(name); - if (variableExpression != nullptr) { - return *variableExpression; - } else { - if (firstRun) { - LOG4CPLUS_TRACE(logger, "Trying to retrieve boolean variable " << name << " that was not yet created; returning dummy instead."); - return std::shared_ptr(new VariableExpression(BaseExpression::bool_, name)); - } else { - LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist."); - throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist."; - } - } -} - -std::shared_ptr VariableState::getIntegerVariableExpression(std::string const& name) const { - std::shared_ptr const* variableExpression = this->integerVariables_.find(name); - if (variableExpression != nullptr) { - return *variableExpression; - } else { - if (firstRun) { - LOG4CPLUS_TRACE(logger, "Trying to retrieve integer variable " << name << " that was not yet created; returning dummy instead."); - return std::shared_ptr(new VariableExpression(BaseExpression::int_, name)); - } else { - LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist."); - throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist."; - } - } -} - -std::shared_ptr VariableState::getVariableExpression(std::string const& name) const { - std::shared_ptr const* variableExpression = this->integerVariables_.find(name); - if (variableExpression != nullptr) { - return *variableExpression; - } - - variableExpression = this->booleanVariables_.find(name); - if (variableExpression != nullptr) { - return *variableExpression; - } - LOG4CPLUS_ERROR(logger, "Variable " << name << " does not exist."); - throw storm::exceptions::InvalidArgumentException() << "Variable " << name << " does not exist."; -} - -void VariableState::clearLocalVariables() { - this->localBooleanVariables_.clear(); - this->localIntegerVariables_.clear(); - this->nextLocalBooleanVariableIndex = 0; - this->nextLocalIntegerVariableIndex = 0; -} - -bool VariableState::isFreeIdentifier(std::string const& identifier) const { - if (this->integerVariableNames_.find(identifier) != nullptr) return false; - if (this->allConstantNames_.find(identifier) != nullptr) return false; - if (this->labelNames_.find(identifier) != nullptr) return false; - if (this->moduleNames_.find(identifier) != nullptr) return false; - if (this->keywords.find(identifier) != nullptr) return false; - return true; -} - -bool VariableState::isIdentifier(std::string const& identifier) const { - if (this->allConstantNames_.find(identifier) != nullptr) return false; - if (this->keywords.find(identifier) != nullptr) return false; - return true; -} - -void VariableState::prepareForSecondRun() { - integerConstants_.clear(); - booleanConstants_.clear(); - doubleConstants_.clear(); - allConstantNames_.clear(); - this->firstRun = false; - nextGlobalCommandIndex = 0; -} - -} // namespace prism -} // namespace parser + namespace parser { + namespace prism { + + using namespace storm::ir; + using namespace storm::ir::expressions; + + template + struct SymbolDump { + SymbolDump(std::ostream& out) : out(out) {} + void operator() (std::basic_string s, T elem) { + this->out << "\t" << s << " -> " << elem << std::endl; + } + private: + std::ostream& out; + }; + template + std::ostream& operator<<(std::ostream& out, qi::symbols& symbols) { + out << "Dumping symbol table" << std::endl; + SymbolDump dump(out); + symbols.for_each(dump); + return out; + } + std::ostream& operator<<(std::ostream& out, VariableState::variableNamesStruct& symbols) { + SymbolDump dump(out); + symbols.for_each(dump); + return out; + } + + + VariableState::VariableState(bool firstRun) : firstRun(firstRun), keywords(), nextLocalBooleanVariableIndex(0), nextLocalIntegerVariableIndex(0), nextGlobalBooleanVariableIndex(0), nextGlobalIntegerVariableIndex(0), nextGlobalCommandIndex(0), nextGlobalUpdateIndex(0) { + // Nothing to do here. + } + + uint_fast64_t VariableState::getNextLocalBooleanVariableIndex() const { + return this->nextLocalBooleanVariableIndex; + } + + uint_fast64_t VariableState::getNextLocalIntegerVariableIndex() const { + return this->nextLocalIntegerVariableIndex; + } + + uint_fast64_t VariableState::getNextGlobalBooleanVariableIndex() const { + return this->nextGlobalBooleanVariableIndex; + } + + uint_fast64_t VariableState::getNextGlobalIntegerVariableIndex() const { + return this->nextGlobalIntegerVariableIndex; + } + + uint_fast64_t VariableState::getNextGlobalCommandIndex() const { + return this->nextGlobalCommandIndex; + } + + uint_fast64_t VariableState::getNextGlobalUpdateIndex() const { + return this->nextGlobalUpdateIndex; + } + + uint_fast64_t VariableState::addBooleanVariable(std::string const& name) { + if (firstRun) { + LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextGlobalBooleanVariableIndex << "."); + this->booleanVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextGlobalBooleanVariableIndex, name))); + this->booleanVariableNames_.add(name, name); + ++this->nextGlobalBooleanVariableIndex; + ++this->nextLocalBooleanVariableIndex; + return this->nextGlobalBooleanVariableIndex - 1; + } else { + std::shared_ptr variableExpression = this->booleanVariables_.at(name); + if (variableExpression != nullptr) { + return variableExpression->getGlobalVariableIndex(); + } else { + LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist."); + throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist."; + } + } + } + + uint_fast64_t VariableState::addIntegerVariable(std::string const& name) { + if (firstRun) { + LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextGlobalIntegerVariableIndex << "."); + this->integerVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextGlobalIntegerVariableIndex, name))); + this->integerVariableNames_.add(name, name); + ++this->nextGlobalIntegerVariableIndex; + ++this->nextLocalIntegerVariableIndex; + return this->nextGlobalIntegerVariableIndex - 1; + } else { + std::shared_ptr variableExpression = this->integerVariables_.at(name); + if (variableExpression != nullptr) { + return variableExpression->getGlobalVariableIndex(); + } else { + LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist."); + throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist."; + } + } + } + + std::shared_ptr VariableState::getBooleanVariableExpression(std::string const& name) const { + std::shared_ptr const* variableExpression = this->booleanVariables_.find(name); + if (variableExpression != nullptr) { + return *variableExpression; + } else { + if (firstRun) { + LOG4CPLUS_TRACE(logger, "Trying to retrieve boolean variable " << name << " that was not yet created; returning dummy instead."); + return std::shared_ptr(new VariableExpression(BaseExpression::bool_, name)); + } else { + LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist."); + throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist."; + } + } + } + + std::shared_ptr VariableState::getIntegerVariableExpression(std::string const& name) const { + std::shared_ptr const* variableExpression = this->integerVariables_.find(name); + if (variableExpression != nullptr) { + return *variableExpression; + } else { + if (firstRun) { + LOG4CPLUS_TRACE(logger, "Trying to retrieve integer variable " << name << " that was not yet created; returning dummy instead."); + return std::shared_ptr(new VariableExpression(BaseExpression::int_, name)); + } else { + LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist."); + throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist."; + } + } + } + + std::shared_ptr VariableState::getVariableExpression(std::string const& name) const { + std::shared_ptr const* variableExpression = this->integerVariables_.find(name); + if (variableExpression != nullptr) { + return *variableExpression; + } + + variableExpression = this->booleanVariables_.find(name); + if (variableExpression != nullptr) { + return *variableExpression; + } + LOG4CPLUS_ERROR(logger, "Variable " << name << " does not exist."); + throw storm::exceptions::InvalidArgumentException() << "Variable " << name << " does not exist."; + } + + void VariableState::clearLocalVariables() { + this->localBooleanVariables_.clear(); + this->localIntegerVariables_.clear(); + this->nextLocalBooleanVariableIndex = 0; + this->nextLocalIntegerVariableIndex = 0; + } + + bool VariableState::isFreeIdentifier(std::string const& identifier) const { + if (this->integerVariableNames_.find(identifier) != nullptr) return false; + if (this->allConstantNames_.find(identifier) != nullptr) return false; + if (this->labelNames_.find(identifier) != nullptr) return false; + if (this->moduleNames_.find(identifier) != nullptr) return false; + if (this->keywords.find(identifier) != nullptr) return false; + return true; + } + + bool VariableState::isIdentifier(std::string const& identifier) const { + if (this->allConstantNames_.find(identifier) != nullptr) return false; + if (this->keywords.find(identifier) != nullptr) return false; + return true; + } + + void VariableState::prepareForSecondRun() { + integerConstants_.clear(); + booleanConstants_.clear(); + doubleConstants_.clear(); + allConstantNames_.clear(); + this->firstRun = false; + nextGlobalCommandIndex = 0; + nextGlobalUpdateIndex = 0; + } + + } // namespace prism + } // namespace parser } // namespace storm diff --git a/src/parser/prismparser/VariableState.h b/src/parser/prismparser/VariableState.h index fe10d86cf..deccd4da4 100644 --- a/src/parser/prismparser/VariableState.h +++ b/src/parser/prismparser/VariableState.h @@ -1,12 +1,12 @@ -/* +/* * File: VariableState.h * Author: nafur * * Created on April 10, 2013, 4:43 PM */ -#ifndef VARIABLESTATE_H -#define VARIABLESTATE_H +#ifndef STORM_PARSER_PRISMPARSER_VARIABLESTATE_H +#define STORM_PARSER_PRISMPARSER_VARIABLESTATE_H #include @@ -15,183 +15,193 @@ #include "Tokens.h" namespace storm { - -namespace parser { - -namespace prism { - -using namespace storm::ir; -using namespace storm::ir::expressions; - -template -std::ostream& operator<<(std::ostream& out, qi::symbols& symbols); - -/*! - * This class contains the internal state that is needed for parsing a PRISM model. - */ -class VariableState { -public: - /*! - * Creates a new variable state object. By default, this object will be set to a state in which - * it is ready for performing a first run on some input. The first run creates all variables - * while the second one checks for the correct usage of variables in expressions. - * - * @param firstRun If set, this object will be in a state ready for performing the first run. If - * set to false, this object will assume that it has all variable data already. - */ - VariableState(bool firstRun = true); - - /*! - * Indicator, if we are still in the first run. - */ - bool firstRun; - - /*! - * A parser for all reserved keywords. - */ - keywordsStruct keywords; - - /*! - * Internal counter for the local index of the next new boolean variable. - */ - uint_fast64_t nextLocalBooleanVariableIndex; - - /*! - * Retrieves the next free local index for a boolean variable. - * - * @return The next free local index for a boolean variable. - */ - uint_fast64_t getNextLocalBooleanVariableIndex() const; - - /*! - * Internal counter for the local index of the next new integer variable. - */ - uint_fast64_t nextLocalIntegerVariableIndex; - - /*! - * Retrieves the next free global index for a integer variable. - * - * @return The next free global index for a integer variable. - */ - uint_fast64_t getNextLocalIntegerVariableIndex() const; - - /*! - * Internal counter for the index of the next new boolean variable. - */ - uint_fast64_t nextGlobalBooleanVariableIndex; - - /*! - * Retrieves the next free global index for a boolean variable. - * - * @return The next free global index for a boolean variable. - */ - uint_fast64_t getNextGlobalBooleanVariableIndex() const; - - /*! - * Internal counter for the index of the next new integer variable. - */ - uint_fast64_t nextGlobalIntegerVariableIndex; - - /*! - * Retrieves the next free global index for a integer variable. - * - * @return The next free global index for a integer variable. - */ - uint_fast64_t getNextGlobalIntegerVariableIndex() const; - - /*! - * Internal counter for the index of the next command. - */ - uint_fast64_t nextGlobalCommandIndex; - - /*! - * Retrieves the next free global index for a command. - * - * @return The next free global index for a command. - */ - uint_fast64_t getNextGlobalCommandIndex() const; - - // Structures mapping variable and constant names to the corresponding expression nodes of - // the intermediate representation. - struct qi::symbols> integerVariables_, booleanVariables_; - struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_; - - // A structure representing the identity function over identifier names. - struct variableNamesStruct : qi::symbols { } - integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, - localBooleanVariables_, localIntegerVariables_, assignedBooleanVariables_, assignedIntegerVariables_, - globalBooleanVariables_, globalIntegerVariables_; - - /*! - * Adds a new boolean variable with the given name. - * - * @param name The name of the variable. - * @return The global index of the variable. - */ - uint_fast64_t addBooleanVariable(std::string const& name); - - /*! - * Adds a new integer variable with the given name. - * - * @param name The name of the variable. - * @return The global index of the variable. - */ - uint_fast64_t addIntegerVariable(std::string const& name); - - /*! - * Retrieves the variable expression for the boolean variable with the given name. - * - * @param name The name of the boolean variable for which to retrieve the variable expression. - * @return The variable expression for the boolean variable with the given name. - */ - std::shared_ptr getBooleanVariableExpression(std::string const& name) const; - - /*! - * Retrieves the variable expression for the integer variable with the given name. - * - * @param name The name of the integer variable for which to retrieve the variable expression. - * @return The variable expression for the integer variable with the given name. - */ - std::shared_ptr getIntegerVariableExpression(std::string const& name) const; - - /*! - * Retrieve the variable expression for the variable with the given name. - * - * @param name The name of the variable for which to retrieve the variable expression. - * @return The variable expression for the variable with the given name. - */ - std::shared_ptr getVariableExpression(std::string const& name) const; - - /*! - * Clears all local variables. - */ - void clearLocalVariables(); - - /*! - * Check if the given string is a free identifier. - * - * @param identifier A string to be checked. - * @return True iff the given string is a free identifier. - */ - bool isFreeIdentifier(std::string const& identifier) const; - - /*! - * Check if given string is a valid identifier. - * - * @param identifier A string to be checked. - * @return True iff the given string is an identifier. - */ - bool isIdentifier(std::string const& identifier) const; - - /*! - * Prepare state to proceed to second parser run. Currently, this clears the constants. - */ - void prepareForSecondRun(); -}; - -} // namespace prism -} // namespace parser + namespace parser { + namespace prism { + + using namespace storm::ir; + using namespace storm::ir::expressions; + + template + std::ostream& operator<<(std::ostream& out, qi::symbols& symbols); + + /*! + * This class contains the internal state that is needed for parsing a PRISM model. + */ + class VariableState { + public: + /*! + * Creates a new variable state object. By default, this object will be set to a state in which + * it is ready for performing a first run on some input. The first run creates all variables + * while the second one checks for the correct usage of variables in expressions. + * + * @param firstRun If set, this object will be in a state ready for performing the first run. If + * set to false, this object will assume that it has all variable data already. + */ + VariableState(bool firstRun = true); + + /*! + * Indicator, if we are still in the first run. + */ + bool firstRun; + + /*! + * A parser for all reserved keywords. + */ + keywordsStruct keywords; + + /*! + * Internal counter for the local index of the next new boolean variable. + */ + uint_fast64_t nextLocalBooleanVariableIndex; + + /*! + * Retrieves the next free local index for a boolean variable. + * + * @return The next free local index for a boolean variable. + */ + uint_fast64_t getNextLocalBooleanVariableIndex() const; + + /*! + * Internal counter for the local index of the next new integer variable. + */ + uint_fast64_t nextLocalIntegerVariableIndex; + + /*! + * Retrieves the next free global index for a integer variable. + * + * @return The next free global index for a integer variable. + */ + uint_fast64_t getNextLocalIntegerVariableIndex() const; + + /*! + * Internal counter for the index of the next new boolean variable. + */ + uint_fast64_t nextGlobalBooleanVariableIndex; + + /*! + * Retrieves the next free global index for a boolean variable. + * + * @return The next free global index for a boolean variable. + */ + uint_fast64_t getNextGlobalBooleanVariableIndex() const; + + /*! + * Internal counter for the index of the next new integer variable. + */ + uint_fast64_t nextGlobalIntegerVariableIndex; + + /*! + * Retrieves the next free global index for a integer variable. + * + * @return The next free global index for a integer variable. + */ + uint_fast64_t getNextGlobalIntegerVariableIndex() const; + + /*! + * Internal counter for the index of the next command. + */ + uint_fast64_t nextGlobalCommandIndex; + + /*! + * Retrieves the next free global index for a command. + * + * @return The next free global index for a command. + */ + uint_fast64_t getNextGlobalCommandIndex() const; + + /*! + * Internal counter for the index of the next update. + */ + uint_fast64_t nextGlobalUpdateIndex; + + /*! + * Retrieves the next free global index for an update. + * + * @return The next free global index for an update. + */ + uint_fast64_t getNextGlobalUpdateIndex() const; + + // Structures mapping variable and constant names to the corresponding expression nodes of + // the intermediate representation. + struct qi::symbols> integerVariables_, booleanVariables_; + struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_; + + // A structure representing the identity function over identifier names. + struct variableNamesStruct : qi::symbols { } + integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, + localBooleanVariables_, localIntegerVariables_, assignedBooleanVariables_, assignedIntegerVariables_, + globalBooleanVariables_, globalIntegerVariables_; + + /*! + * Adds a new boolean variable with the given name. + * + * @param name The name of the variable. + * @return The global index of the variable. + */ + uint_fast64_t addBooleanVariable(std::string const& name); + + /*! + * Adds a new integer variable with the given name. + * + * @param name The name of the variable. + * @return The global index of the variable. + */ + uint_fast64_t addIntegerVariable(std::string const& name); + + /*! + * Retrieves the variable expression for the boolean variable with the given name. + * + * @param name The name of the boolean variable for which to retrieve the variable expression. + * @return The variable expression for the boolean variable with the given name. + */ + std::shared_ptr getBooleanVariableExpression(std::string const& name) const; + + /*! + * Retrieves the variable expression for the integer variable with the given name. + * + * @param name The name of the integer variable for which to retrieve the variable expression. + * @return The variable expression for the integer variable with the given name. + */ + std::shared_ptr getIntegerVariableExpression(std::string const& name) const; + + /*! + * Retrieve the variable expression for the variable with the given name. + * + * @param name The name of the variable for which to retrieve the variable expression. + * @return The variable expression for the variable with the given name. + */ + std::shared_ptr getVariableExpression(std::string const& name) const; + + /*! + * Clears all local variables. + */ + void clearLocalVariables(); + + /*! + * Check if the given string is a free identifier. + * + * @param identifier A string to be checked. + * @return True iff the given string is a free identifier. + */ + bool isFreeIdentifier(std::string const& identifier) const; + + /*! + * Check if given string is a valid identifier. + * + * @param identifier A string to be checked. + * @return True iff the given string is an identifier. + */ + bool isIdentifier(std::string const& identifier) const; + + /*! + * Prepare state to proceed to second parser run. Currently, this clears the constants. + */ + void prepareForSecondRun(); + }; + + } // namespace prism + } // namespace parser } // namespace storm -#endif /* VARIABLESTATE_H */ +#endif /* STORM_PARSER_PRISMPARSER_VARIABLESTATE_H */ diff --git a/src/storage/LabeledValues.h b/src/storage/LabeledValues.h index e8abf35c4..25f39d9b5 100644 --- a/src/storage/LabeledValues.h +++ b/src/storage/LabeledValues.h @@ -25,7 +25,7 @@ namespace storm { /*! * Default-constructs an empty object. */ - LabeledValues() : valueLabelList() { + explicit LabeledValues() : valueLabelList() { // Intentionally left empty. } @@ -34,7 +34,7 @@ namespace storm { * * @param value The probability to sto */ - LabeledValues(ValueType value) : valueLabelList() { + explicit LabeledValues(ValueType value) : valueLabelList() { addValue(value); } @@ -105,20 +105,20 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, LabeledValues const& labeledValues) { out << "["; for (auto const& element : labeledValues) { - out << element.first << "("; + out << element.first << " ("; for (auto const& label : element.second) { out << label << ", "; } - out << ")"; + out << ") "; } out << "]"; return out; } /*! - * Adds all labeled probabilities of the given object to the current one. + * Adds all labeled values of the given object to the current one. * - * @param labeledProbabilities The labeled probabilities to add to the object. + * @param labeledValues The labeled values to add to the object. */ LabeledValues& operator+=(LabeledValues const& labeledValues) { for (auto const& valueLabelListPair : labeledValues) { @@ -127,6 +127,36 @@ namespace storm { 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. * diff --git a/test/functional/parser/ParsePrismTest.cpp b/test/functional/parser/ParsePrismTest.cpp index 3cf963872..63eca2d31 100644 --- a/test/functional/parser/ParsePrismTest.cpp +++ b/test/functional/parser/ParsePrismTest.cpp @@ -14,10 +14,8 @@ TEST(ParsePrismTest, parseCrowds5_5) { ASSERT_TRUE(storm::settings::Settings::getInstance()->isSet("fixDeadlocks")); storm::ir::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.pm")); - storm::adapters::ExplicitModelAdapter adapter(program); - - std::shared_ptr> model = adapter.getModel()->as>(); - + std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program); + ASSERT_EQ(model->getNumberOfStates(), 8607ull); ASSERT_EQ(model->getNumberOfTransitions(), 15113ull); } @@ -25,11 +23,10 @@ TEST(ParsePrismTest, parseCrowds5_5) { TEST(ParsePrismTest, parseTwoDice) { storm::ir::Program program; ASSERT_NO_THROW(program = storm::parser::PrismParserFromFile(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.nm")); - storm::adapters::ExplicitModelAdapter adapter(program); - std::shared_ptr> model = adapter.getModel()->as>(); + std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(program); ASSERT_EQ(model->getNumberOfStates(), 169ull); - ASSERT_EQ(model->getNumberOfChoices(), 254ull); + ASSERT_EQ(model->as>()->getNumberOfChoices(), 254ull); ASSERT_EQ(model->getNumberOfTransitions(), 436ull); }