From a08a403eec602da7361dd2fd083b529c9dd8f3d9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 27 Sep 2013 14:39:36 +0200 Subject: [PATCH] Ongoing refactoring work on ExplicitModelAdapter. Former-commit-id: 1212f84aadf964a4de2c7e4f3ecc2e9f9ccc3ac5 --- src/adapters/ExplicitModelAdapter.cpp | 252 +------ src/adapters/ExplicitModelAdapter.h | 893 ++++++++++++++++++++++-- src/models/AtomicPropositionsLabeling.h | 32 + src/storm.cpp | 4 +- 4 files changed, 859 insertions(+), 322 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 14254eae5..f29b757f7 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -22,10 +22,6 @@ #include #include -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -extern log4cplus::Logger logger; - 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; @@ -33,160 +29,9 @@ bool ExplicitModelAdapterOptionsRegistered = storm::settings::Settings::register namespace storm { namespace adapters { - - void ExplicitModelAdapter::defineUndefinedConstants(storm::ir::Program& program, std::string const& constantDefinitionString) { - if (!constantDefinitionString.empty()) { - // Parse the string that defines the undefined constants of the model and make sure that it contains exactly - // one value for each undefined constant of the model. - std::vector definitions; - boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); - for (auto& definition : definitions) { - boost::trim(definition); - - // Check whether the token could be a legal constant definition. - uint_fast64_t positionOfAssignmentOperator = definition.find('='); - if (positionOfAssignmentOperator == std::string::npos) { - throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error."; - } - - // Now extract the variable name and the value from the string. - std::string constantName = definition.substr(0, positionOfAssignmentOperator); - boost::trim(constantName); - std::string value = definition.substr(positionOfAssignmentOperator + 1); - boost::trim(value); - - // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. - if (program.hasUndefinedBooleanConstant(constantName)) { - if (value == "true") { - program.getUndefinedBooleanConstantExpression(constantName)->define(true); - } else if (value == "false") { - program.getUndefinedBooleanConstantExpression(constantName)->define(false); - } else { - throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << "."; - } - } else if (program.hasUndefinedIntegerConstant(constantName)) { - try { - int_fast64_t integerValue = std::stoi(value); - program.getUndefinedIntegerConstantExpression(constantName)->define(integerValue); - } catch (std::invalid_argument const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << "."; - } catch (std::out_of_range const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << " (value too big)."; - } - } else if (program.hasUndefinedDoubleConstant(constantName)) { - try { - double doubleValue = std::stod(value); - program.getUndefinedDoubleConstantExpression(constantName)->define(doubleValue); - } catch (std::invalid_argument const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << "."; - } catch (std::out_of_range const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << " (value too big)."; - } - - } else { - throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << "."; - } - } - } - } - - void ExplicitModelAdapter::undefineUndefinedConstants(storm::ir::Program& program) { - for (auto nameExpressionPair : program.getBooleanUndefinedConstantExpressionsMap()) { - nameExpressionPair.second->undefine(); - } - for (auto nameExpressionPair : program.getIntegerUndefinedConstantExpressionsMap()) { - nameExpressionPair.second->undefine(); - } - for (auto nameExpressionPair : program.getDoubleUndefinedConstantExpressionsMap()) { - nameExpressionPair.second->undefine(); - } - } - - ExplicitModelAdapter::StateInformation ExplicitModelAdapter::exploreReachableStateSpace(storm::ir::Program const& program) { - StateInformation stateInformation; - - // Initialize a queue, insert the starting state and explore the current state until there is no more reachable state. - - return stateInformation; - } - - ExplicitModelAdapter::ModelComponents ExplicitModelAdapter::buildModelComponents(storm::ir::Program const& program, std::string const& rewardModelName) { - ModelComponents modelComponents; - - // Start by exploring the state space. - StateInformation stateInformation = exploreReachableStateSpace(program); - - // Then build the transition matrix for the reachable states. - - // Now build the state labeling. - - // Finally, construct the state rewards. - - return modelComponents; - } - - std::shared_ptr> ExplicitModelAdapter::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; - 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))); - 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; - 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))); - 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))); - break; - default: - LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type."); - throw storm::exceptions::WrongFormatException() << "Error while creating model from probabilistic program: cannot handle this model type."; - break; - } + - // Undefine the constants so that the program can be used again somewhere else. - undefineUndefinedConstants(program); - - return result; - } - - void ExplicitModelAdapter::setValue(StateType* state, uint_fast64_t index, bool value) { - std::get<0>(*state)[index] = value; - } - - void ExplicitModelAdapter::setValue(StateType* state, uint_fast64_t index, int_fast64_t value) { - std::get<1>(*state)[index] = value; - } - - std::string ExplicitModelAdapter::toString(StateType const* state) { - std::stringstream ss; - for (unsigned int i = 0; i < state->first.size(); i++) ss << state->first[i] << "\t"; - for (unsigned int i = 0; i < state->second.size(); i++) ss << state->second[i] << "\t"; - return ss.str(); - } - - StateType* ExplicitModelAdapter::applyUpdate(storm::ir::Program const& program, StateType const* state, storm::ir::Update const& update) { - return applyUpdate(program, state, state, update); - } - StateType* ExplicitModelAdapter::applyUpdate(storm::ir::Program const& program, StateType const* state, StateType const* baseState, storm::ir::Update const& update) { - StateType* newState = new StateType(*state); - for (auto variableAssignmentPair : update.getBooleanAssignments()) { - setValue(newState, program.getGlobalIndexOfBooleanVariable(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsBool(baseState)); - } - for (auto variableAssignmentPair : update.getIntegerAssignments()) { - setValue(newState, program.getGlobalIndexOfIntegerVariable(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsInt(baseState)); - } - return newState; - } // std::vector ExplicitModelAdapter::getStateRewards(std::vector const& rewards) { // std::vector result(this->allStates.size()); @@ -227,48 +72,6 @@ namespace storm { // return results; // } -// void ExplicitModelAdapter::initializeVariables() { -// uint_fast64_t numberOfIntegerVariables = 0; -// uint_fast64_t numberOfBooleanVariables = 0; -// -// // Count number of variables. -// numberOfBooleanVariables += program.getNumberOfGlobalBooleanVariables(); -// numberOfIntegerVariables += program.getNumberOfGlobalIntegerVariables(); -// for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { -// numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); -// numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); -// } -// -// this->booleanVariables.resize(numberOfBooleanVariables); -// this->integerVariables.resize(numberOfIntegerVariables); -// -// // Create variables. -// for (uint_fast64_t i = 0; i < program.getNumberOfGlobalBooleanVariables(); ++i) { -// storm::ir::BooleanVariable var = program.getGlobalBooleanVariable(i); -// this->booleanVariables[var.getGlobalIndex()] = var; -// this->booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); -// } -// for (uint_fast64_t i = 0; i < program.getNumberOfGlobalIntegerVariables(); ++i) { -// storm::ir::IntegerVariable var = program.getGlobalIntegerVariable(i); -// this->integerVariables[var.getGlobalIndex()] = var; -// this->integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); -// } -// for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { -// storm::ir::Module const& module = program.getModule(i); -// -// for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { -// storm::ir::BooleanVariable var = module.getBooleanVariable(j); -// this->booleanVariables[var.getGlobalIndex()] = var; -// this->booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); -// } -// for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { -// storm::ir::IntegerVariable var = module.getIntegerVariable(j); -// this->integerVariables[var.getGlobalIndex()] = var; -// this->integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); -// } -// } -// } - // boost::optional>> ExplicitModelAdapter::getActiveCommandsByAction(StateType const* state, std::string const& action) { // boost::optional>> result((std::vector>())); // @@ -303,57 +106,6 @@ namespace storm { // return result; // } -// static StateType* ExplicitModelAdapter::getInitialState() { -// StateType* initialState = new StateType(); -// initialState->first.resize(this->booleanVariables.size()); -// initialState->second.resize(this->integerVariables.size()); -// -// // Start with boolean variables. -// for (uint_fast64_t i = 0; i < this->booleanVariables.size(); ++i) { -// // Check if an initial value is given -// if (this->booleanVariables[i].getInitialValue().get() == nullptr) { -// // If no initial value was given, we assume that the variable is initially false. -// std::get<0>(*initialState)[i] = false; -// } else { -// // Initial value was given. -// bool initialValue = this->booleanVariables[i].getInitialValue()->getValueAsBool(nullptr); -// std::get<0>(*initialState)[i] = initialValue; -// } -// } -// -// // Now process integer variables. -// for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) { -// // Check if an initial value was given. -// if (this->integerVariables[i].getInitialValue().get() == nullptr) { -// // No initial value was given, so we assume that the variable initially has the least value it can take. -// std::get<1>(*initialState)[i] = this->integerVariables[i].getLowerBound()->getValueAsInt(nullptr); -// } else { -// // Initial value was given. -// int_fast64_t initialValue = this->integerVariables[i].getInitialValue()->getValueAsInt(nullptr); -// std::get<1>(*initialState)[i] = initialValue; -// } -// } -// -// LOG4CPLUS_DEBUG(logger, "Generated initial state."); -// return initialState; -// } - -// static uint_fast64_t ExplicitModelAdapter::getOrAddStateIndex(StateType* state) { -// // Check, if the state was already registered. -// auto indexIt = this->stateToIndexMap.find(state); -// -// if (indexIt == this->stateToIndexMap.end()) { -// // The state has not been seen, yet, so add it to the list of all reachable states. -// allStates.push_back(state); -// stateToIndexMap[state] = allStates.size() - 1; -// return allStates.size() - 1; -// } else { -// // The state was already encountered. Delete the copy of the old state and return its index. -// delete state; -// return indexIt->second; -// } -// } - // void ExplicitModelAdapter::addUnlabeledTransitions(uint_fast64_t stateIndex, std::list>, std::map>>& transitionList) { // StateType const* state = this->allStates[stateIndex]; // @@ -468,7 +220,7 @@ namespace storm { // // 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()); diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index c5bf02ed3..70834ee9b 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -12,15 +12,29 @@ #include #include #include +#include #include #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 "src/models/AtomicPropositionsLabeling.h" #include "src/storage/SparseMatrix.h" +#include "src/settings/Settings.h" +#include "src/exceptions/WrongFormatException.h" + +#include + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" +extern log4cplus::Logger logger; namespace storm { namespace adapters { @@ -57,12 +71,19 @@ namespace storm { } }; + template class ExplicitModelAdapter { public: // A structure holding information about the reachable state space. struct StateInformation { + StateInformation() : reachableStates(), stateToIndexMap(), numberOfChoices(), numberOfTransitions(0) { + // Intentionally left empty. + } + std::vector reachableStates; - std::unordered_map stateToIndexMap; + std::unordered_map stateToIndexMap; + std::vector numberOfChoices; + uint_fast64_t numberOfTransitions; }; // A structure holding the individual components of a model. @@ -79,6 +100,25 @@ namespace storm { std::vector> choiceLabeling; }; + // A structure storing information about the used variables of the program. + struct VariableInformation { + VariableInformation() : booleanVariables(), booleanVariableToIndexMap(), integerVariables(), integerVariableToIndexMap() { + // Intentinally left empty. + } + + // List of all boolean variables. + std::vector booleanVariables; + + // A mapping of boolean variable names to their indices. + std::map booleanVariableToIndexMap; + + // List of all integer variables. + std::vector integerVariables; + + // A mapping of integer variable names to their indices. + std::map integerVariableToIndexMap; + }; + /*! * Convert the program given at construction time to an abstract model. The type of the model is the one * specified in the program. The given reward model name selects the rewards that the model will contain. @@ -91,7 +131,38 @@ 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; + 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))); + 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; + 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))); + 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))); + break; + default: + LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type."); + throw storm::exceptions::WrongFormatException() << "Error while creating model from probabilistic program: cannot handle this model type."; + break; + } + + // Undefine the constants so that the program can be used again somewhere else. + undefineUndefinedConstants(program); + + return result; + } private: /*! @@ -101,7 +172,9 @@ namespace storm { * @param index The index of the boolean variable to modify. * @param value The new value of the variable. */ - static void setValue(StateType* state, uint_fast64_t index, bool value); + static void setValue(StateType* state, uint_fast64_t index, bool value) { + std::get<0>(*state)[index] = value; + } /*! * Set some integer variable in the given state object. @@ -110,7 +183,9 @@ namespace storm { * @param index index of the integer variable to modify. * @param value The new value of the variable. */ - static void setValue(StateType* state, uint_fast64_t index, int_fast64_t value); + static void setValue(StateType* state, uint_fast64_t index, int_fast64_t value) { + std::get<1>(*state)[index] = value; + } /*! * Transforms a state into a somewhat readable string. @@ -118,73 +193,249 @@ namespace storm { * @param state The state to transform into a string. * @return A string representation of the state. */ - static std::string toString(StateType const* state); + static std::string toString(StateType const* state) { + std::stringstream ss; + for (unsigned int i = 0; i < state->first.size(); i++) ss << state->first[i] << "\t"; + for (unsigned int i = 0; i < state->second.size(); i++) ss << state->second[i] << "\t"; + return ss.str(); + } /*! * Applies an update to the given state and returns the resulting new state object. This methods does not * modify the given state but returns a new one. * - * @param program The program in which the variables of the update are declared. + * @param variableInformation A structure with information about the variables in the program. * @params state The state to which to apply the update. * @params update The update to apply. * @return The resulting state. */ - static StateType* applyUpdate(storm::ir::Program const& program, StateType const* state, storm::ir::Update const& update); + static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, storm::ir::Update const& update) { + return applyUpdate(variableInformation, state, state, update); + } /*! * Applies an update to the given state and returns the resulting new state object. The update is evaluated * over the variable values of the given base state. This methods does not modify the given state but * returns a new one. * - * @param program The program in which the variables of the update are declared. + * @param variableInformation A structure with information about the variables in the program. * @param state The state to which to apply the update. * @param baseState The state used for evaluating the update. * @param update The update to apply. * @return The resulting state. */ - static StateType* applyUpdate(storm::ir::Program const& program, StateType const* state, StateType const* baseState, storm::ir::Update const& update); + static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, StateType const* baseState, storm::ir::Update const& update) { + StateType* newState = new StateType(*state); + for (auto variableAssignmentPair : update.getBooleanAssignments()) { + setValue(newState, variableInformation.booleanVariableToIndexMap.at(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsBool(baseState)); + } + for (auto variableAssignmentPair : update.getIntegerAssignments()) { + setValue(newState, variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsInt(baseState)); + } + return newState; + } + /*! * Defines the undefined constants of the given program using the given string. * * @param program The program in which to define the constants. * @param constantDefinitionString A comma-separated list of constant definitions. */ - static void defineUndefinedConstants(storm::ir::Program& program, std::string const& constantDefinitionString); + static void defineUndefinedConstants(storm::ir::Program& program, std::string const& constantDefinitionString) { + if (!constantDefinitionString.empty()) { + // Parse the string that defines the undefined constants of the model and make sure that it contains exactly + // one value for each undefined constant of the model. + std::vector definitions; + boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + + // Check whether the token could be a legal constant definition. + uint_fast64_t positionOfAssignmentOperator = definition.find('='); + if (positionOfAssignmentOperator == std::string::npos) { + throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error."; + } + + // Now extract the variable name and the value from the string. + std::string constantName = definition.substr(0, positionOfAssignmentOperator); + boost::trim(constantName); + std::string value = definition.substr(positionOfAssignmentOperator + 1); + boost::trim(value); + + // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. + if (program.hasUndefinedBooleanConstant(constantName)) { + if (value == "true") { + program.getUndefinedBooleanConstantExpression(constantName)->define(true); + } else if (value == "false") { + program.getUndefinedBooleanConstantExpression(constantName)->define(false); + } else { + throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << "."; + } + } else if (program.hasUndefinedIntegerConstant(constantName)) { + try { + int_fast64_t integerValue = std::stoi(value); + program.getUndefinedIntegerConstantExpression(constantName)->define(integerValue); + } catch (std::invalid_argument const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << "."; + } catch (std::out_of_range const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << " (value too big)."; + } + } else if (program.hasUndefinedDoubleConstant(constantName)) { + try { + double doubleValue = std::stod(value); + program.getUndefinedDoubleConstantExpression(constantName)->define(doubleValue); + } catch (std::invalid_argument const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << "."; + } catch (std::out_of_range const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << " (value too big)."; + } + + } else { + throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << "."; + } + } + } + } /*! * Undefines all previously defined constants in the given program. * * @param program The program in which to undefine the constants. */ - static void undefineUndefinedConstants(storm::ir::Program& program); + static void undefineUndefinedConstants(storm::ir::Program& program) { + for (auto nameExpressionPair : program.getBooleanUndefinedConstantExpressionsMap()) { + nameExpressionPair.second->undefine(); + } + for (auto nameExpressionPair : program.getIntegerUndefinedConstantExpressionsMap()) { + nameExpressionPair.second->undefine(); + } + for (auto nameExpressionPair : program.getDoubleUndefinedConstantExpressionsMap()) { + nameExpressionPair.second->undefine(); + } + } /*! - * Explores the state space of the given program and returns the components of the model as a result. + * Generates the initial state of the given program. * - * @param program The program whose state space to explore. - * @param rewardModelName The name of the reward model that is to be considered. If empty, no reward model - * is considered. - * @return A structure containing the components of the resulting model. + * @param program The program for which to construct the initial state. + * @param variableInformation A structure with information about the variables in the program. + * @return The initial state. */ - static ModelComponents buildModelComponents(storm::ir::Program const& program, std::string const& rewardModelName); + static StateType* getInitialState(storm::ir::Program const& program, VariableInformation const& variableInformation) { + StateType* initialState = new StateType(); + initialState->first.resize(variableInformation.booleanVariables.size()); + initialState->second.resize(variableInformation.integerVariables.size()); + + // Start with boolean variables. + for (uint_fast64_t i = 0; i < variableInformation.booleanVariables.size(); ++i) { + // Check if an initial value is given + if (variableInformation.booleanVariables[i].getInitialValue().get() == nullptr) { + // If no initial value was given, we assume that the variable is initially false. + std::get<0>(*initialState)[i] = false; + } else { + // Initial value was given. + bool initialValue = variableInformation.booleanVariables[i].getInitialValue()->getValueAsBool(nullptr); + std::get<0>(*initialState)[i] = initialValue; + } + } + + // Now process integer variables. + for (uint_fast64_t i = 0; i < variableInformation.integerVariables.size(); ++i) { + // Check if an initial value was given. + if (variableInformation.integerVariables[i].getInitialValue().get() == nullptr) { + // No initial value was given, so we assume that the variable initially has the least value it can take. + std::get<1>(*initialState)[i] = variableInformation.integerVariables[i].getLowerBound()->getValueAsInt(nullptr); + } else { + // Initial value was given. + int_fast64_t initialValue = variableInformation.integerVariables[i].getInitialValue()->getValueAsInt(nullptr); + std::get<1>(*initialState)[i] = initialValue; + } + } + + LOG4CPLUS_DEBUG(logger, "Generated initial state."); + return initialState; + } /*! - * Retrieves the state rewards for every reachable state based on the given state rewards. + * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to + * the lists of all states with a new id. If the state was already known, the object that is pointed to by + * the given state pointer is deleted and the old state id is returned. Note that the pointer should not be + * used after invoking this method. * - * @param rewards The rewards to use. - * @return The reward values for every (reachable) state. + * @param state A pointer to a state for which to retrieve the index. This must not be used after the call. + * @param stateInformation The information about the already explored part of the reachable state space. + * @return A pair indicating whether the state was already discovered before and the state id of the state. */ -// static std::vector getStateRewards(std::vector const& rewards); + static std::pair getOrAddStateIndex(StateType* state, StateInformation& stateInformation) { + // Check, if the state was already registered. + auto indexIt = stateInformation.stateToIndexMap.find(state); + + if (indexIt == stateInformation.stateToIndexMap.end()) { + // The state has not been seen, yet, so add it to the list of all reachable states. + stateInformation.stateToIndexMap[state] = stateInformation.reachableStates.size(); + stateInformation.numberOfChoices.push_back(0); + stateInformation.reachableStates.push_back(state); + return std::make_pair(false, stateInformation.stateToIndexMap[state]); + } else { + // The state was already encountered. Delete the copy of the old state and return its index. + delete state; + return std::make_pair(true, indexIt->second); + } + } /*! - * Computes the labels for every reachable state based on a list of available labels. + * Expands all unlabeled (i.e. independent) transitions of the given state and adds newly discovered states + * to the given queue. * - * @param labels A mapping from label names to boolean expressions to use for the labeling. - * @return The resulting labeling. + * @param program The program that defines the transitions. + * @param stateInformation Provides information about the discovered state space. + * @param variableInformation A structure with information about the variables in the program. + * @param stateIndex The index of the state to expand. + * @param stateQueue The queue of states into which newly discovered states are inserted. */ -// static storm::models::AtomicPropositionsLabeling getStateLabeling(std::map> labels); - + static void exploreUnlabeledTransitions(storm::ir::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue) { + StateType const* currentState = stateInformation.reachableStates[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(currentState)) continue; + + ++stateInformation.numberOfChoices[stateIndex]; + + std::set targetStates; + + // 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. + std::pair flagAndTargetStateIndexPair = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update), stateInformation); + + // If the state has not yet been discovered, add it to the queue. + if (!flagAndTargetStateIndexPair.first) { + stateQueue.push(flagAndTargetStateIndexPair.second); + } + + // In any case, record that there is a transition to the newly found state to count the number + // of transitions correctly. + targetStates.insert(flagAndTargetStateIndexPair.second); + } + + stateInformation.numberOfTransitions += targetStates.size(); + } + } + } + /*! * Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by * modules. @@ -196,45 +447,572 @@ namespace storm { * module has a command with a relevant label, but no enabled one, nothing is returned to indicate that there * is no legal transition possible. * + * @param The program in which to search for active commands. * @param state The current state. * @param action The action label to select. * @return A list of lists of active commands or nothing. */ -// static boost::optional>> getActiveCommandsByAction(StateType const* state, std::string const& action); + static boost::optional>> getActiveCommandsByAction(storm::ir::Program const& program, StateType const* state, std::string const& action) { + boost::optional>> result((std::vector>())); + + // Iterate over all modules. + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::ir::Module const& module = 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; + } /*! - * Generates the initial state. + * Expands all labeled (i.e. synchronizing) transitions of the given state and adds newly discovered states + * to the given queue. * - * @return The initial state. + * @param program The program that defines the transitions. + * @param stateInformation Provides information about the discovered state space. + * @param variableInformation A structure with information about the variables in the program. + * @param stateIndex The index of the state to expand. + * @param stateQueue The queue of states into which newly discovered states are inserted. */ -// static StateType* getInitialState(); + static void exploreLabeledTransitions(storm::ir::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue) { + for (std::string const& action : program.getActions()) { + StateType const* currentState = stateInformation.reachableStates[stateIndex]; + boost::optional>> optionalActiveCommandLists = getActiveCommandsByAction(program, 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) { + ++stateInformation.numberOfChoices[stateIndex]; + + std::unordered_set* currentTargetStates = new std::unordered_set(); + std::unordered_set* newTargetStates = new std::unordered_set(); + currentTargetStates->insert(new StateType(*currentState)); + + // 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. + 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& targetState : *currentTargetStates) { + StateType* newTargetState = applyUpdate(variableInformation, targetState, currentState, update); + + auto existingState = newTargetStates->find(newTargetState); + if (existingState == newTargetStates->end()) { + newTargetStates->insert(newTargetState); + } else { + // If the state was already seen in one of the other updates, we need to delete this copy. + delete newTargetState; + } + } + } + + // If there is one more command to come, shift the target states one time step back. + if (i < iteratorList.size() - 1) { + for (auto const& state : *currentTargetStates) { + delete state; + } + delete currentTargetStates; + currentTargetStates = newTargetStates; + newTargetStates = new std::unordered_set(); + } + } + + // If there are states that have not yet been discovered, add them to the queue. + for (auto const& state : *newTargetStates) { + std::pair flagAndNewStateIndexPair = getOrAddStateIndex(state, stateInformation); + + if (!flagAndNewStateIndexPair.first) { + stateQueue.push(flagAndNewStateIndexPair.second); + } + } + + stateInformation.numberOfTransitions += newTargetStates->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; + } + } + } + } /*! - * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to - * the lists of all states with a new id. If the state was already known, the object that is pointed to by - * the given state pointer is deleted and the old state id is returned. Note that the pointer should not be - * used after invoking this method. + * Explores the reachable state space given by the program and returns a list of all states as well as a + * mapping from states to their indices. * - * @param state A pointer to a state for which to retrieve the index. This must not be used after the call. - * @return The state id of the given state. + * @param program The program whose state space to explore. + * @param variableInformation A structure with information about the variables in the program. + * @return A structure containing all reachable states and a mapping from states to their indices. */ -// static uint_fast64_t getOrAddStateIndex(StateType* state); + static StateInformation exploreReachableStateSpace(storm::ir::Program const& program, VariableInformation const& variableInformation) { + StateInformation stateInformation; + + // Initialize a queue and insert the initial state. + std::queue stateQueue; + StateType* initialState = getInitialState(program, variableInformation); + getOrAddStateIndex(initialState, stateInformation); + stateQueue.push(stateInformation.stateToIndexMap[initialState]); + + // Now explore the current state until there is no more reachable state. + while (!stateQueue.empty()) { + uint_fast64_t currentStateIndex = stateQueue.front(); + + exploreUnlabeledTransitions(program, stateInformation, variableInformation, currentStateIndex, stateQueue); + exploreLabeledTransitions(program, stateInformation, variableInformation, currentStateIndex, stateQueue); + + // If the state does not have any outgoing transitions, we fix this by adding a self-loop if the + // option was set. + if (stateInformation.numberOfChoices[currentStateIndex] == 0) { + if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { + ++stateInformation.numberOfTransitions; + ++stateInformation.numberOfChoices[currentStateIndex] = 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."; + } + } + + + // After exploring a state, remove it from the queue. + stateQueue.pop(); + } + + return stateInformation; + } /*! - * Expands all unlabeled (i.e. independent) transitions of the given state and adds them to the transition list. + * Aggregates information about the variables in the program. * - * @param stateIndex The state to expand. - * @params transitionList The current list of transitions for this state. + * @param program The program whose variables to aggregate. */ -// static void addUnlabeledTransitions(uint_fast64_t stateIndex, std::list>, std::map>>& transitionList); + static VariableInformation createVariableInformation(storm::ir::Program const& program) { + VariableInformation result; + + uint_fast64_t numberOfIntegerVariables = 0; + uint_fast64_t numberOfBooleanVariables = 0; + + // Count number of variables. + numberOfBooleanVariables += program.getNumberOfGlobalBooleanVariables(); + numberOfIntegerVariables += program.getNumberOfGlobalIntegerVariables(); + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); + numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); + } + + // Resize the variable vectors appropriately. + result.booleanVariables.resize(numberOfBooleanVariables); + result.integerVariables.resize(numberOfIntegerVariables); + + // Create variables. + for (uint_fast64_t i = 0; i < program.getNumberOfGlobalBooleanVariables(); ++i) { + storm::ir::BooleanVariable const& var = program.getGlobalBooleanVariable(i); + result.booleanVariables[var.getGlobalIndex()] = var; + result.booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + } + for (uint_fast64_t i = 0; i < program.getNumberOfGlobalIntegerVariables(); ++i) { + storm::ir::IntegerVariable const& var = program.getGlobalIntegerVariable(i); + result.integerVariables[var.getGlobalIndex()] = var; + result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + } + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::ir::Module const& module = program.getModule(i); + + for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { + storm::ir::BooleanVariable const& var = module.getBooleanVariable(j); + result.booleanVariables[var.getGlobalIndex()] = var; + result.booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + } + for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { + storm::ir::IntegerVariable const& var = module.getIntegerVariable(j); + result.integerVariables[var.getGlobalIndex()] = var; + result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + } + } + + return 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]; + + // 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(currentState)) continue; + + result.push_back(std::map()); + std::map& targetStates = result.back(); + + 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 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); + } + } + + // Check that the resulting distribution is in fact a distribution. + if (std::abs(1 - probabilitySum) > storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { + 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(); + } + } + } + + return 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]; + boost::optional>> optionalActiveCommandLists = getActiveCommandsByAction(program, 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. + 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 = applyUpdate(variableInformation, stateProbabilityPair.first, currentState, update); + + 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 the state was already seen in one of the other updates, we need to delete this copy. + delete newTargetState; + } + } + } + + // 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. + result.push_back(std::map()); + + // Now create the actual distribution. + std::map& targetStates = result.back(); + double probabilitySum = 0; + for (auto const& stateProbabilityPair : *newTargetStates) { + uint_fast64_t newStateIndex = stateInformation.stateToIndexMap.at(stateProbabilityPair.first); + targetStates[newStateIndex] = stateProbabilityPair.second; + probabilitySum += stateProbabilityPair.second; + } + + // Check that the resulting distribution is in fact a distribution. + if (std::abs(1 - probabilitySum) > storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) { + LOG4CPLUS_ERROR(logger, "Sum of update probabilities do not some to one for some command."); + throw storm::exceptions::WrongFormatException() << "Sum of update probabilities do not some to one for some command."; + } + + // 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; + } + } + } + + return result; + } /*! - * Expands all labeled (i.e. synchronizing) transitions of the given state and adds them to the transition list. * - * @param stateIndex The index of the state to expand. - * @param transitionList The current list of transitions for this state. */ -// static void addLabeledTransitions(uint_fast64_t stateIndex, std::list>, std::map>>& transitionList); + 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) { + std::vector nondeterministicChoiceIndices(stateInformation.reachableStates.size() + 1); + + // 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()); + + // 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 (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { + transitionMatrix.insertNextValue(currentRow, currentState, 1); + ++currentRow; + } 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."; + } + } else { + // 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; + + // 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& stateProbabilityPair : choice) { + auto existingStateProbabilityPair = globalDistribution.find(stateProbabilityPair.first); + if (existingStateProbabilityPair == globalDistribution.end()) { + globalDistribution[stateProbabilityPair.first] += stateProbabilityPair.second / allChoices.size(); + } else { + globalDistribution[stateProbabilityPair.first] = stateProbabilityPair.second / allChoices.size(); + } + } + } + + // Now add the resulting distribution as the only choice of the current state. + nondeterministicChoiceIndices[currentState] = currentRow; + + for (auto const& stateProbabilityPair : globalDistribution) { + transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + } + + ++currentRow; + } else { + // If the model is nondeterministic, we add all choices individually. + nondeterministicChoiceIndices[currentState] = currentRow; + for (auto const& choice : allChoices) { + for (auto const& stateProbabilityPair : choice) { + transitionMatrix.insertNextValue(currentRow, stateProbabilityPair.first, stateProbabilityPair.second); + } + ++currentRow; + } + } + } + } + + nondeterministicChoiceIndices[stateInformation.reachableStates.size()] = currentRow; + + return nondeterministicChoiceIndices; + } + + /*! + * Explores the state space of the given program and returns the components of the model as a result. + * + * @param program The program whose state space to explore. + * @param rewardModelName The name of the reward model that is to be considered. If empty, no reward model + * is considered. + * @return A structure containing the components of the resulting model. + */ + static ModelComponents buildModelComponents(storm::ir::Program const& program, std::string const& rewardModelName) { + ModelComponents modelComponents; + + VariableInformation variableInformation = createVariableInformation(program); + + // Start by exploring the state space. + StateInformation stateInformation = exploreReachableStateSpace(program, variableInformation); + + // Then build the transition and reward matrices for the reachable states. + bool deterministicModel = program.getModelType() == storm::ir::Program::DTMC || program.getModelType() == storm::ir::Program::CTMC; + if (deterministicModel) { + modelComponents.transitionMatrix = storm::storage::SparseMatrix(stateInformation.reachableStates.size()); + modelComponents.transitionMatrix.initialize(); + modelComponents.transitionRewardMatrix = storm::storage::SparseMatrix(stateInformation.reachableStates.size()); + modelComponents.transitionRewardMatrix.initialize(); + } else { + uint_fast64_t totalNumberOfChoices = 0; + for (auto numberOfChoices : stateInformation.numberOfChoices) { + totalNumberOfChoices += numberOfChoices; + } + modelComponents.transitionMatrix = storm::storage::SparseMatrix(totalNumberOfChoices, stateInformation.reachableStates.size()); + modelComponents.transitionMatrix.initialize(); + modelComponents.transitionRewardMatrix = storm::storage::SparseMatrix(totalNumberOfChoices); + modelComponents.transitionRewardMatrix.initialize(); + } + + storm::ir::RewardModel rewardModel = rewardModelName != "" ? program.getRewardModel(rewardModelName) : storm::ir::RewardModel(); + + modelComponents.nondeterministicChoiceIndices = buildTransitionMatrix(program, variableInformation, rewardModel, stateInformation, deterministicModel, modelComponents.transitionMatrix, modelComponents.transitionRewardMatrix); + + // Finalize the resulting matrices. + modelComponents.transitionMatrix.finalize(); + modelComponents.transitionRewardMatrix.finalize(); + + // Now build the state labeling. + modelComponents.stateLabeling = buildStateLabeling(program, variableInformation, stateInformation); + + // Finally, construct the state rewards. + modelComponents.stateRewards = buildStateRewards(rewardModel.getStateRewards(), stateInformation); + + // After everything has been created, we can delete the states. + for (auto state : stateInformation.reachableStates) { + delete state; + } + + return modelComponents; + } + + static storm::models::AtomicPropositionsLabeling buildStateLabeling(storm::ir::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) { + std::map> const& labels = program.getLabels(); + + storm::models::AtomicPropositionsLabeling result(stateInformation.reachableStates.size(), labels.size() + 1); + + // Initialize labeling. + for (auto const& labelExpressionPair : labels) { + result.addAtomicProposition(labelExpressionPair.first); + } + for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) { + for (auto const& labelExpressionPair: labels) { + // Add label to state, if the corresponding expression is true. + if (labelExpressionPair.second->getValueAsBool(stateInformation.reachableStates[index])) { + result.addAtomicPropositionToState(labelExpressionPair.first, index); + } + } + } + + // Also label the initial state with the special label "init". + result.addAtomicProposition("init"); + StateType* initialState = getInitialState(program, variableInformation); + uint_fast64_t initialIndex = stateInformation.stateToIndexMap.at(initialState); + result.addAtomicPropositionToState("init", initialIndex); + delete initialState; + + return result; + } + + 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; + 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]); + } + } + } + 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. @@ -255,35 +1033,10 @@ namespace storm { */ // void buildTransitionMap(); - // List of all boolean variables. - std::vector booleanVariables; - - // List of all integer variables. - std::vector integerVariables; - - // A mapping of boolean variable names to their indices. - std::map booleanVariableToIndexMap; - - // A mapping of integer variable names to their indices. - std::map integerVariableToIndexMap; - //// Members that are filled during the conversion. // The selected reward model. std::unique_ptr rewardModel; - // A list of all reachable states. - std::vector allStates; - - // A mapping of states to their indices (within the list of all states). - std::unordered_map stateToIndexMap; - - // The number of transitions. - uint_fast64_t numberOfTransitions; - - // The number of choices in a nondeterminstic model. (This corresponds to the number of rows of the matrix - // used to represent the nondeterministic model.) - uint_fast64_t numberOfChoices; - // The number of choices for each state of a nondeterministic model. std::vector choiceIndices; diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index d1ccb492d..9ad1dfb86 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -88,6 +88,38 @@ public: singleLabelings(std::move(atomicPropositionsLabeling.singleLabelings)) { // Intentionally left empty. } + + /*! + * Assignment operator that copies the contents of the right-hand-side to the current labeling. + * + * @param other The atomic propositions labeling to copy. + */ + AtomicPropositionsLabeling& operator=(AtomicPropositionsLabeling const& other) { + if (this != &other) { + this->stateCount = other.stateCount; + this->apCountMax = other.apCountMax; + this->apsCurrent = other.apsCurrent; + this->nameToLabelingMap = other.nameToLabelingMap; + this->singleLabelings = other.singleLabelings; + } + return *this; + } + + /*! + * Assignment operator that moves the contents of the right-hand-side to the current labeling. + * + * @param other The atomic propositions labeling to move. + */ + AtomicPropositionsLabeling& operator=(AtomicPropositionsLabeling&& other) { + if (this != &other) { + this->stateCount = other.stateCount; + this->apCountMax = other.apCountMax; + this->apsCurrent = other.apsCurrent; + this->nameToLabelingMap = std::move(other.nameToLabelingMap); + this->singleLabelings = std::move(other.singleLabelings); + } + return *this; + } /*! * (Empty) destructor. diff --git a/src/storm.cpp b/src/storm.cpp index 5489e3d13..724ce03dd 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) {