diff --git a/examples/mdp/asynchronous_leader/leader3.nm b/examples/mdp/asynchronous_leader/leader3.nm index 25a3ec89d..9f093cc13 100644 --- a/examples/mdp/asynchronous_leader/leader3.nm +++ b/examples/mdp/asynchronous_leader/leader3.nm @@ -4,7 +4,7 @@ mdp -const N= 3; // number of processes +const int N = 3; // number of processes //---------------------------------------------------------------------------------------------------------------------------- module process1 diff --git a/resources/3rdparty/gtest-1.6.0/libgtest.a b/resources/3rdparty/gtest-1.6.0/libgtest.a index e11c98e0e..fc054f665 100644 Binary files a/resources/3rdparty/gtest-1.6.0/libgtest.a and b/resources/3rdparty/gtest-1.6.0/libgtest.a differ diff --git a/resources/3rdparty/gtest-1.6.0/libgtest_main.a b/resources/3rdparty/gtest-1.6.0/libgtest_main.a index f03a4f225..07eb295c8 100644 Binary files a/resources/3rdparty/gtest-1.6.0/libgtest_main.a and b/resources/3rdparty/gtest-1.6.0/libgtest_main.a differ diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 5f5c14d03..55d476e47 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -15,8 +15,6 @@ #include "src/models/Mdp.h" #include "src/models/Ctmdp.h" -typedef std::pair, std::vector> StateType; - #include #include "log4cplus/logger.h" @@ -24,548 +22,561 @@ typedef std::pair, std::vector> StateType; extern log4cplus::Logger logger; namespace storm { - -namespace adapters { - - ExplicitModelAdapter::ExplicitModelAdapter(storm::ir::Program program) : program(program), - booleanVariables(), integerVariables(), booleanVariableToIndexMap(), integerVariableToIndexMap(), - allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionMap() { - // Get variables from program. - this->initializeVariables(); - storm::settings::Settings* s = storm::settings::Settings::getInstance(); - this->precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); - } - - ExplicitModelAdapter::~ExplicitModelAdapter() { - this->clearInternalState(); - } - - std::shared_ptr> ExplicitModelAdapter::getModel(std::string const & rewardModelName) { - // Initialize rewardModel. - this->rewardModel = nullptr; - if (rewardModelName != "") { - this->rewardModel = std::unique_ptr(new storm::ir::RewardModel(this->program.getRewardModel(rewardModelName))); - } - - // State expansion, build temporary map, compute transition rewards. - this->buildTransitionMap(); - - // Compute labeling. - storm::models::AtomicPropositionsLabeling stateLabeling = this->getStateLabeling(this->program.getLabels()); - - // Compute state rewards. - boost::optional> stateRewards; - if ((this->rewardModel != nullptr) && this->rewardModel->hasStateRewards()) { - stateRewards.reset(this->getStateRewards(this->rewardModel->getStateRewards())); - } - - // Build and return actual model. - switch (this->program.getModelType()) - { - case storm::ir::Program::DTMC: - { - storm::storage::SparseMatrix matrix = this->buildDeterministicMatrix(); - return std::shared_ptr>(new storm::models::Dtmc(matrix, stateLabeling, stateRewards, this->transitionRewards)); - break; - } - case storm::ir::Program::CTMC: - { - storm::storage::SparseMatrix matrix = this->buildDeterministicMatrix(); - return std::shared_ptr>(new storm::models::Ctmc(matrix, stateLabeling, stateRewards, this->transitionRewards)); - break; - } - case storm::ir::Program::MDP: - { - storm::storage::SparseMatrix matrix = this->buildNondeterministicMatrix(); - return std::shared_ptr>(new storm::models::Mdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards)); - break; - } - case storm::ir::Program::CTMDP: - { - storm::storage::SparseMatrix matrix = this->buildNondeterministicMatrix(); - return std::shared_ptr>(new storm::models::Ctmdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards)); - break; - } - default: - LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: We can't handle this model type."); - throw storm::exceptions::WrongFormatException() << "Error while creating model from probabilistic program: We can't handle this model type."; - break; - } - } - - void ExplicitModelAdapter::setValue(StateType* const state, uint_fast64_t const index, bool const value) { - std::get<0>(*state)[index] = value; - } - - void ExplicitModelAdapter::setValue(StateType* const state, uint_fast64_t const index, int_fast64_t const value) { - std::get<1>(*state)[index] = value; - } - - std::string ExplicitModelAdapter::toString(StateType const * 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(); - } - - std::vector ExplicitModelAdapter::getStateRewards(std::vector const & rewards) { - std::vector results(this->allStates.size()); - for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { - results[index] = 0; - for (auto 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) { - results[index] += reward.getRewardValue()->getValueAsDouble(this->allStates[index]); + namespace adapters { + + ExplicitModelAdapter::ExplicitModelAdapter(storm::ir::Program program) : program(program), booleanVariables(), + integerVariables(), booleanVariableToIndexMap(), integerVariableToIndexMap(), allStates(), stateToIndexMap(), + numberOfTransitions(0), numberOfChoices(0), choiceLabeling(), transitionMap() { + // Get variables from program. + this->initializeVariables(); + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + this->precision = s->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); + } + + ExplicitModelAdapter::~ExplicitModelAdapter() { + this->clearInternalState(); + } + + std::shared_ptr> ExplicitModelAdapter::getModel(std::string const& rewardModelName) { + // Initialize reward model. + this->rewardModel = nullptr; + if (rewardModelName != "") { + this->rewardModel = std::unique_ptr(new storm::ir::RewardModel(this->program.getRewardModel(rewardModelName))); + } + + // State expansion, build temporary map, compute transition rewards. + this->buildTransitionMap(); + + // Compute labeling. + storm::models::AtomicPropositionsLabeling stateLabeling = this->getStateLabeling(this->program.getLabels()); + + // Compute state rewards. + boost::optional> stateRewards; + if ((this->rewardModel != nullptr) && this->rewardModel->hasStateRewards()) { + stateRewards.reset(this->getStateRewards(this->rewardModel->getStateRewards())); + } + + // Build and return actual model. + switch (this->program.getModelType()) + { + case storm::ir::Program::DTMC: + { + storm::storage::SparseMatrix matrix = this->buildDeterministicMatrix(); + return std::shared_ptr>(new storm::models::Dtmc(matrix, stateLabeling, stateRewards, this->transitionRewards, this->choiceLabeling)); + break; } - } - } - return results; - } - - storm::models::AtomicPropositionsLabeling ExplicitModelAdapter::getStateLabeling(std::map> labels) { - storm::models::AtomicPropositionsLabeling results(this->allStates.size(), labels.size() + 1); - // Initialize labeling. - for (auto it : labels) { - results.addAtomicProposition(it.first); - } - for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { - for (auto label: labels) { - // Add label to state, if guard is true. - if (label.second->getValueAsBool(this->allStates[index])) { - results.addAtomicPropositionToState(label.first, index); - } - } - } + case storm::ir::Program::CTMC: + { + storm::storage::SparseMatrix matrix = this->buildDeterministicMatrix(); + return std::shared_ptr>(new storm::models::Ctmc(matrix, stateLabeling, stateRewards, this->transitionRewards, this->choiceLabeling)); + break; + } + case storm::ir::Program::MDP: + { + storm::storage::SparseMatrix matrix = this->buildNondeterministicMatrix(); + return std::shared_ptr>(new storm::models::Mdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards, this->choiceLabeling)); + break; + } + case storm::ir::Program::CTMDP: + { + storm::storage::SparseMatrix matrix = this->buildNondeterministicMatrix(); + return std::shared_ptr>(new storm::models::Ctmdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards, this->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; + } + } - // Also label the initial state. - results.addAtomicProposition("init"); - StateType* initialState = this->getInitialState(); - uint_fast64_t initialIndex = this->stateToIndexMap[initialState]; - results.addAtomicPropositionToState("init", initialIndex); - delete initialState; + void ExplicitModelAdapter::setValue(StateType* state, uint_fast64_t index, bool value) { + std::get<0>(*state)[index] = value; + } - return results; - } - - void ExplicitModelAdapter::initializeVariables() { - uint_fast64_t numberOfIntegerVariables = 0; - uint_fast64_t numberOfBooleanVariables = 0; - // Count number of variables. - for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { - numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); - numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); - } - - this->booleanVariables.resize(numberOfBooleanVariables); - this->integerVariables.resize(numberOfIntegerVariables); - - // Create variables. - 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(); - } - } - } - - /*! - * Retrieves all active command labeled by some label, ordered by modules. - * - * This function will iterate over all modules and retrieve all commands that are labeled with the given action and active for the current state. - * The result will be a list of lists of commands. - * - * For each module that has appropriately labeled commands, there will be a list. - * If none of these commands is active, this list is empty. - * Note the difference between *no list* and *empty list*: Modules that produce no list are not relevant for this action while an empty list means, that it is not possible to do anything with this label. - * @param state Current state. - * @param action Action label. - * @return Active commands. - */ - std::unique_ptr>> ExplicitModelAdapter::getActiveCommandsByAction(StateType const * state, std::string& action) { - std::unique_ptr>> res = std::unique_ptr>>(new std::list>()); - - // 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, skip this module. - if (!module.hasAction(action)) { - continue; + 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(); + } + + 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); + } + } } - std::set const& ids = module.getCommandsByAction(action); - std::list commands; - - // Look up commands by their id. Add, if guard holds. - for (uint_fast64_t id : ids) { - storm::ir::Command const& cmd = module.getCommand(id); - if (cmd.getGuard()->getValueAsBool(state)) { - commands.push_back(module.getCommand(id)); - } - } - res->push_back(commands); - } - // Sort the result in the vague hope that having small lists at the beginning will speed up the expanding. - res->sort([] (const std::list& a, const std::list& b) -> bool { return a.size() < b.size(); }); - return res; - } - - /*! - * Apply an update to the given state and return resulting state. - * @params state Current state. - * @params update Update to be applied. - * @return Resulting state. - */ - StateType* ExplicitModelAdapter::applyUpdate(StateType const * const state, storm::ir::Update const& update) const { - return this->applyUpdate(state, state, update); - } - - StateType* ExplicitModelAdapter::applyUpdate(StateType const * const state, StateType const * const baseState, storm::ir::Update const& update) const { - StateType* newState = new StateType(*state); - for (auto assignedVariable : update.getBooleanAssignments()) { - setValue(newState, this->booleanVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsBool(baseState)); - } - for (auto assignedVariable : update.getIntegerAssignments()) { - setValue(newState, this->integerVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsInt(baseState)); - } - return newState; - } - - /*! - * Generates the initial state. - */ - 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); + // 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; + } + + void ExplicitModelAdapter::initializeVariables() { + uint_fast64_t numberOfIntegerVariables = 0; + uint_fast64_t numberOfBooleanVariables = 0; + + // Count number of variables. + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); + numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); + } + + this->booleanVariables.resize(numberOfBooleanVariables); + this->integerVariables.resize(numberOfIntegerVariables); + + // Create variables. + 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>())); + + // 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; + } + + StateType* ExplicitModelAdapter::applyUpdate(StateType const* state, storm::ir::Update const& update) const { + return this->applyUpdate(state, state, update); + } + + StateType* ExplicitModelAdapter::applyUpdate(StateType const* state, StateType const* baseState, storm::ir::Update const& update) const { + StateType* newState = new StateType(*state); + for (auto assignedVariable : update.getBooleanAssignments()) { + setValue(newState, this->booleanVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsBool(baseState)); + } + for (auto assignedVariable : update.getIntegerAssignments()) { + setValue(newState, this->integerVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsInt(baseState)); + } + return newState; + } + + 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; + } + + 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 { - // 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; - } - - /*! - * Retrieves the state id of the given state. - * If the state has not been hit yet, it will be added to allStates and given a new id. - * In this case, the pointer must not be deleted, as it is used within allStates. - * If the state is already known, the pointer is deleted and the old state id is returned. - * Hence, the given state pointer should not be used afterwards. - * @param state Pointer to state, shall not be used afterwards. - * @returns State id of given state. - */ - uint_fast64_t ExplicitModelAdapter::getOrAddStateId(StateType * state) { - // Check, if we already know this state at all. - auto indexIt = this->stateToIndexMap.find(state); - if (indexIt == this->stateToIndexMap.end()) { - // No, add to allStates, initialize index. - allStates.push_back(state); - stateToIndexMap[state] = allStates.size()-1; - return allStates.size()-1; - } else { - // Yes, obtain index and delete state object. - delete state; - return indexIt->second; - } - } - - /*! - * Expands all unlabeled transitions for a given state and adds them to the given list of results. - * @params state State to be explored. - * @params res Intermediate transition map. - */ - void ExplicitModelAdapter::addUnlabeledTransitions(const uint_fast64_t stateID, std::list>>& res) { - const StateType* state = this->allStates[stateID]; - // 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; - // Omit, if command is not active. - if (!command.getGuard()->getValueAsBool(state)) continue; - - // Add a new map and get pointer. - res.emplace_back(); - std::map* states = &res.back().second; - double probSum = 0; - - // Iterate over all updates. - for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { - // Obtain new state id. - storm::ir::Update const& update = command.getUpdate(k); - uint_fast64_t newStateId = this->getOrAddStateId(this->applyUpdate(state, update)); - - probSum += update.getLikelihoodExpression()->getValueAsDouble(state); - // Check, if we already know this state, add up probabilities for every state. - auto stateIt = states->find(newStateId); - if (stateIt == states->end()) { - (*states)[newStateId] = update.getLikelihoodExpression()->getValueAsDouble(state); - this->numberOfTransitions++; - } else { - (*states)[newStateId] += update.getLikelihoodExpression()->getValueAsDouble(state); - } - } - if (std::abs(1 - probSum) > 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(); - } - } - } - } - - /*! - * Explores reachable state from given state by using labeled transitions. - * Found transitions are stored in given map. - * @param stateID State to be explored. - * @param res Intermediate transition map. - */ - void ExplicitModelAdapter::addLabeledTransitions(const uint_fast64_t stateID, std::list>>& res) { - // Create a copy of the current state, as we will free intermediate states... - for (std::string action : this->program.getActions()) { - StateType* state = new StateType(*this->allStates[stateID]); - std::unique_ptr>> cmds = this->getActiveCommandsByAction(state, action); - - // Start with current state - std::unordered_map resultStates; - resultStates[state] = 1.0; - - for (std::list module : *cmds) { - if (resultStates.size() == 0) break; - std::unordered_map newStates; - - // Iterate over all commands within this module. - for (storm::ir::Command command : module) { - // Iterate over all updates of this command. - double probSum = 0; - for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { - storm::ir::Update const update = command.getUpdate(k); - - // Iterate over all resultStates. - for (auto it : resultStates) { - // Apply the new update and get resulting state. - StateType* newState = this->applyUpdate(it.first, this->allStates[stateID], update); - probSum += it.second * update.getLikelihoodExpression()->getValueAsDouble(it.first); - // Insert the new state into newStates array. - // Take care of calculation of likelihood, combine identical states. - auto s = newStates.find(newState); - if (s == newStates.end()) { - newStates[newState] = it.second * update.getLikelihoodExpression()->getValueAsDouble(it.first); - } else { - newStates[newState] += it.second * update.getLikelihoodExpression()->getValueAsDouble(it.first); - } - } - } - if (std::abs(1 - probSum) > 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(); - } - } - for (auto it: resultStates) { - delete it.first; - } - // Move new states to resultStates. - resultStates.clear(); - resultStates.insert(newStates.begin(), newStates.end()); - } - - if (resultStates.size() > 0) { - res.push_back(std::make_pair(action, std::map())); - std::map* states = &res.back().second; - - // Now add our final result states to our global result. - for (auto const& it : resultStates) { - uint_fast64_t newStateID = this->getOrAddStateId(it.first); - (*states)[newStateID] = it.second; - } - this->numberOfTransitions += states->size(); - } - } - - } - - /*! - * Create matrix from intermediate mapping, assuming it is a dtmc model. - * @param intermediate Intermediate representation of transition mapping. - * @return result matrix. - */ - storm::storage::SparseMatrix ExplicitModelAdapter::buildDeterministicMatrix() { - // ***** ATTENTION ***** - // this->numberOfTransitions is meaningless, as we combine all choices into one for each state. - // Hence, we compute the correct number of transitions 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 number of distinct nodes. - std::set set; - for (auto choice : transitionMap[state]) { - for (auto elem : choice.second) { - set.insert(elem.first); - } - } - numberOfTransitions += set.size(); - } - LOG4CPLUS_INFO(logger, "Building deterministic transition matrix: " << allStates.size() << " x " << allStates.size() << " with " << numberOfTransitions << " transitions."); - // Now build 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 choices to one map. - std::map map; - std::map rewardMap; - for (auto choice : transitionMap[state]) { - for (auto elem : choice.second) { - map[elem.first] += elem.second; - if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { - for (auto reward : this->rewardModel->getTransitionRewards()) { - if (reward.getStatePredicate()->getValueAsBool(this->allStates[state]) == true) { - rewardMap[elem.first] += reward.getRewardValue()->getValueAsDouble(this->allStates[state]); + // 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]; + + // 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 (int 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; + + 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); + } + } } - } - } - } - } - // Scale probabilities by number of choices. - double factor = 1.0 / transitionMap[state].size(); - for (auto it : map) { - result.addNextValue(state, it.first, it.second * factor); - if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { - this->transitionRewards.get().addNextValue(state, it.first, rewardMap[it.first] * factor); - } - } - - } - result.finalize(); - return result; - } - - /*! - * Create matrix from intermediate mapping, assuming it is a mdp model. - * @param intermediate Intermediate representation of transition mapping. - * @param choices Overall number of choices for all nodes. - * @return result matrix. - */ - 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()); - // Build matrix. - uint_fast64_t nextRow = 0; - for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { - this->choiceIndices.push_back(transitionMap[state].size()); - for (auto choice : transitionMap[state]) { - for (auto it : choice.second) { - result.addNextValue(nextRow, it.first, it.second); - if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { - double rewardValue = 0; - for (auto reward : this->rewardModel->getTransitionRewards()) { - if (reward.getStatePredicate()->getValueAsBool(this->allStates[state]) == true) { - rewardValue = reward.getRewardValue()->getValueAsDouble(this->allStates[state]); + + // 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(); } - } - this->transitionRewards.get().addNextValue(nextRow, it.first, rewardValue); - } - } - nextRow++; - } - } - result.finalize(); - return result; - } - - /*! - * Build matrix from model. Starts with all initial states and explores the reachable state space. - * While exploring, the transitions are stored in a temporary map. - * Afterwards, we transform this map into the actual matrix. - * @return result matrix. - */ - void ExplicitModelAdapter::buildTransitionMap() { - LOG4CPLUS_DEBUG(logger, "Starting to create transition map from program..."); - this->clearInternalState(); - this->allStates.clear(); - this->allStates.push_back(this->getInitialState()); - stateToIndexMap[this->allStates[0]] = 0; + } + + // 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; + } + } + } + } - for (uint_fast64_t curIndex = 0; curIndex < this->allStates.size(); curIndex++) - { - this->addUnlabeledTransitions(curIndex, this->transitionMap[curIndex]); - this->addLabeledTransitions(curIndex, this->transitionMap[curIndex]); - - this->numberOfChoices += this->transitionMap[curIndex].size(); - if (this->transitionMap[curIndex].size() == 0) { - // This is a deadlock state. - if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { - this->numberOfTransitions++; - this->numberOfChoices++; - this->transitionMap[curIndex].emplace_back(); - this->transitionMap[curIndex].back().second[curIndex] = 1; - } else { - LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state."); - throw storm::exceptions::WrongFormatException() << "Error while creating sparse matrix from probabilistic program: found deadlock state."; - } - } - } - LOG4CPLUS_DEBUG(logger, "Finished creating transition map."); - } - - void ExplicitModelAdapter::clearInternalState() { - for (auto it : allStates) { - delete it; - } - allStates.clear(); - stateToIndexMap.clear(); - this->numberOfTransitions = 0; - this->numberOfChoices = 0; - this->choiceIndices.clear(); - this->transitionRewards.reset(); - this->transitionMap.clear(); - } - -} // namespace adapters - + 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."); + } + + void ExplicitModelAdapter::clearInternalState() { + for (auto it : allStates) { + delete it; + } + allStates.clear(); + stateToIndexMap.clear(); + this->numberOfTransitions = 0; + this->numberOfChoices = 0; + this->choiceIndices.clear(); + this->transitionRewards.reset(); + this->transitionMap.clear(); + } + + } // namespace adapters } // namespace storm diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 18b07b942..78f36f9c0 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -5,8 +5,8 @@ * Created on March 15, 2013, 11:42 AM */ -#ifndef EXPLICITMODELADAPTER_H -#define EXPLICITMODELADAPTER_H +#ifndef STORM_ADAPTERS_EXPLICITMODELADAPTER_H +#define STORM_ADAPTERS_EXPLICITMODELADAPTER_H #include #include @@ -23,226 +23,272 @@ #include "src/storage/SparseMatrix.h" namespace storm { -namespace adapters { - -/*! - * Model state, represented by the values of all variables. - */ -typedef std::pair, std::vector> StateType; - -class StateHash { -public: - std::size_t operator()(StateType* state) const { - size_t seed = 0; - for (auto it : state->first) { - boost::hash_combine(seed, it); - } - for (auto it : state->second) { - boost::hash_combine(seed, it); - } - return seed; - } -}; - -class StateCompare { -public: - bool operator()(StateType* state1, StateType* state2) const { - return *state1 == *state2; - } -}; - -class ExplicitModelAdapter { -public: - /*! - * Initialize adapter with given program. - */ - ExplicitModelAdapter(storm::ir::Program program); - ~ExplicitModelAdapter(); - - /*! - * Convert program to an AbstractModel. - * The model will be of the type specified in the program. - * The model will contain rewards that are specified by the given reward model. - * @param rewardModelName Name of reward model to be added to the model. - * @return Model resulting from the program. - */ - std::shared_ptr> getModel(std::string const & rewardModelName = ""); - -private: - // Copying/Moving is disabled for this class - ExplicitModelAdapter(ExplicitModelAdapter const& other) {} - ExplicitModelAdapter(ExplicitModelAdapter && other) {} - - double precision; - - /*! - * Set some boolean variable in the given state object. - * @param state State to be changed. - * @param index Index of boolean variable. - * @param value New value. - */ - static void setValue(StateType* const state, uint_fast64_t const index, bool const value); - /*! - * Set some integer variable in the given state object. - * @param state State to be changed. - * @param index Index of integer variable. - * @param value New value. - */ - static void setValue(StateType* const state, uint_fast64_t const index, int_fast64_t const value); - /*! - * Transforms a state into a somewhat readable string. - * @param state State. - * @return String representation of the state. - */ - static std::string toString(StateType const * const state); - /*! - * Apply an update to the given state and return the resulting new state object. - * This methods creates a copy of the given state. - * @params state Current state. - * @params update Update to be applied. - * @return Resulting state. - */ - StateType* applyUpdate(StateType const * const state, storm::ir::Update const& update) const; - /*! - * Apply an update to a given state and return the resulting new state object. - * Updates are done using the variable values from a given baseState. - * @params state State to be updated. - * @params baseState State used for update variables. - * @params update Update to be applied. - * @return Resulting state. - */ - StateType* applyUpdate(StateType const * const state, StateType const * const baseState, storm::ir::Update const& update) const; - - /*! - * Reads and combines variables from all program modules and stores them. - * Also creates a map to obtain a variable index from a variable map efficiently. - */ - void initializeVariables(); - - /*! - * Calculate state reward for every reachable state based on given reward models. - * @param rewards List of state reward models. - * @return Reward for every state. - */ - std::vector getStateRewards(std::vector const & rewards); - - /*! - * Determines the labels for every reachable state, based on a list of available labels. - * @param labels Mapping from label names to boolean expressions. - * @returns The resulting labeling. - */ - storm::models::AtomicPropositionsLabeling getStateLabeling(std::map> labels); - - /*! - * Retrieves all active command labeled by some label, ordered by modules. - * - * This function will iterate over all modules and retrieve all commands that are labeled with the given action and active for the current state. - * The result will be a list of lists of commands. - * - * For each module that has appropriately labeled commands, there will be a list. - * If none of these commands is active, this list is empty. - * Note the difference between *no list* and *empty list*: Modules that produce no list are not relevant for this action while an empty list means, that it is not possible to do anything with this label. - * @param state Current state. - * @param action Action label. - * @return Active commands. - */ - std::unique_ptr>> getActiveCommandsByAction(StateType const * state, std::string& action); - - /*! - * Generates the initial state. - * - * @return The initial state. - */ - StateType* getInitialState(); - - /*! - * Retrieves the state id of the given state. - * If the state has not been hit yet, it will be added to allStates and given a new id. - * In this case, the pointer must not be deleted, as it is used within allStates. - * If the state is already known, the pointer is deleted and the old state id is returned. - * Hence, the given state pointer should not be used afterwards. - * @param state Pointer to state, shall not be used afterwards. - * @returns State id of given state. - */ - uint_fast64_t getOrAddStateId(StateType * state); - - /*! - * Expands all unlabeled transitions for a given state and adds them to the given list of results. - * @params state State to be explored. - * @params res Intermediate transition map. - */ - void addUnlabeledTransitions(const uint_fast64_t stateID, std::list>>& res); - - /*! - * Explores reachable state from given state by using labeled transitions. - * Found transitions are stored in given map. - * @param stateID State to be explored. - * @param res Intermediate transition map. - */ - void addLabeledTransitions(const uint_fast64_t stateID, std::list>>& res); - - /*! - * Create matrix from intermediate mapping, assuming it is a dtmc model. - * @param intermediate Intermediate representation of transition mapping. - * @return result matrix. - */ - storm::storage::SparseMatrix buildDeterministicMatrix(); - - /*! - * Create matrix from intermediate mapping, assuming it is a mdp model. - * @param intermediate Intermediate representation of transition mapping. - * @param choices Overall number of choices for all nodes. - * @return result matrix. - */ - storm::storage::SparseMatrix buildNondeterministicMatrix(); - - /*! - * Generate internal transition map from given model. - * Starts with all initial states and explores the reachable state space. - */ - void buildTransitionMap(); - - /*! - * Clear all members that are initialized during the computation. - */ - void clearInternalState(); - - // Program that should be converted. - storm::ir::Program program; - // List of all boolean variables. - std::vector booleanVariables; - // List of all integer variables. - std::vector integerVariables; - // Maps boolean variable names to their index. - std::map booleanVariableToIndexMap; - // Maps integer variable names to their index. - std::map integerVariableToIndexMap; - - //// Members that are filled during the conversion. - // Selected reward model. - std::unique_ptr rewardModel; - // List of all reachable states. - std::vector allStates; - // Maps states to their index (within allStates). - std::unordered_map stateToIndexMap; - // Number of transitions. - uint_fast64_t numberOfTransitions; - // Number of choices. (Is number of rows in matrix of nondeterministic model.) - uint_fast64_t numberOfChoices; - // Number of choices for each state. - std::vector choiceIndices; - // Rewards for transitions. - boost::optional> transitionRewards; - - /*! - * Maps a source node to a list of probability distributions over target nodes. - * Each such distribution corresponds to an unlabeled command or a feasible combination of labeled commands. - * Therefore, each distribution is represented by a label and a mapping from target nodes to their probabilities. - */ - std::map>>> transitionMap; -}; - -} // namespace adapters + namespace adapters { + + /*! + * A state of the model, i.e. a valuation of all variables. + */ + typedef std::pair, std::vector> StateType; + + /*! + * A helper class that provides the functionality to compute a hash value for states of the model. + */ + class StateHash { + public: + std::size_t operator()(StateType* state) const { + size_t seed = 0; + for (auto it : state->first) { + boost::hash_combine(seed, it); + } + for (auto it : state->second) { + boost::hash_combine(seed, it); + } + return seed; + } + }; + + /*! + * A helper class that provides the functionality to compare states of the model. + */ + class StateCompare { + public: + bool operator()(StateType* state1, StateType* state2) const { + return *state1 == *state2; + } + }; + + class ExplicitModelAdapter { + public: + /*! + * Initializes the adapter with the given program. + * + * @param program The program from which to build the explicit model. + */ + ExplicitModelAdapter(storm::ir::Program program); + + /*! + * Destroys the adapter. + */ + ~ExplicitModelAdapter(); + + /*! + * 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. + * + * @param rewardModelName The name of reward model to be added to the model. This must be either a reward + * model of the program or the empty string. In the latter case, the constructed model will contain no + * rewards. + * @return The explicit model that was given by the probabilistic program. + */ + std::shared_ptr> getModel(std::string const& rewardModelName = ""); + + private: + // Copying/Moving is disabled for this class + ExplicitModelAdapter(ExplicitModelAdapter const& other) { } + ExplicitModelAdapter(ExplicitModelAdapter && other) { } + + /*! + * The precision that is to be used for sanity checks internally. + */ + double precision; + + /*! + * Sets some boolean variable in the given state object. + * + * @param state The state to modify. + * @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); + + /*! + * Set some integer variable in the given state object. + * + * @param state The state to modify. + * @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); + + /*! + * Transforms a state into a somewhat readable string. + * + * @param state The state to transform into a string. + * @return A string representation of the state. + */ + static std::string toString(StateType const* state); + + /*! + * 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. + * + * @params state The state to which to apply the update. + * @params update The update to apply. + * @return The resulting state. + */ + StateType* applyUpdate(StateType const* state, storm::ir::Update const& update) const; + + /*! + * 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. + * + * @params state The state to which to apply the update. + * @params baseState The state used for evaluating the update. + * @params update The update to apply. + * @return The resulting state. + */ + StateType* applyUpdate(StateType const* state, StateType const* baseState, storm::ir::Update const& update) const; + + /*! + * Prepares internal data structures associated with the variables in the program that are used during the + * translation. + */ + void initializeVariables(); + + /*! + * 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. + */ + 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. + */ + storm::models::AtomicPropositionsLabeling getStateLabeling(std::map> labels); + + /*! + * Retrieves all commands that are labeled with the given label and enabled in the given state, grouped by + * modules. + * + * This function will iterate over all modules and retrieve all commands that are labeled with the given + * action and active (i.e. enabled) in the current state. The result is a list of lists of commands in which + * the inner lists contain all commands of exactly one module. If a module does not have *any* (including + * disabled) commands, there will not be a list of commands of that module in the result. If, however, the + * 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 state The current state. + * @param action The action label to select. + * @return A list of lists of active commands or nothing. + */ + boost::optional>> getActiveCommandsByAction(StateType const* state, std::string const& action); + + /*! + * Generates the initial state. + * + * @return The initial state. + */ + StateType* getInitialState(); + + /*! + * 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 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. + */ + uint_fast64_t getOrAddStateIndex(StateType* state); + + /*! + * Expands all unlabeled (i.e. independent) transitions of the given state and adds them to the transition list. + * + * @param stateIndex The state to expand. + * @params transitionList The current list of transitions for this state. + */ + void addUnlabeledTransitions(uint_fast64_t stateIndex, std::list>, std::map>>& transitionList); + + /*! + * 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. + */ + void addLabeledTransitions(uint_fast64_t stateIndex, std::list>, std::map>>& transitionList); + + /*! + * Builds the transition matrix of a deterministic model from the current list of transitions. + * + * @return The transition matrix. + */ + storm::storage::SparseMatrix buildDeterministicMatrix(); + + /*! + * Builds the transition matrix of a nondeterministic model from the current list of transitions. + * + * @return result The transition matrix. + */ + storm::storage::SparseMatrix buildNondeterministicMatrix(); + + /*! + * Generate the (internal) list of all transitions of the model. + */ + void buildTransitionMap(); + + /*! + * Clear all members that are initialized during the computation. + */ + void clearInternalState(); + + // Program that is to be converted. + storm::ir::Program program; + + // 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; + + // The result of the translation of transition rewards to a sparse matrix (if any). + boost::optional> transitionRewards; + + // A labeling for the choices of each state. + std::vector> choiceLabeling; + + /*! + * Maps a source state to a list of probability distributions over target states. Each distribution + * corresponds to an unlabeled command or a feasible combination of labeled commands. Therefore, each + * distribution is represented by a structure that contains the label of the participating commands, a list + * of labels associated with that particular command combination and a mapping from target states to their + * probabilities. + */ + std::map>, std::map>>> transitionMap; + }; + + } // namespace adapters } // namespace storm -#endif /* EXPLICITMODELADAPTER_H */ +#endif /* STORM_ADAPTERS_EXPLICITMODELADAPTER_H */ diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp index b1e4fe8ef..db701239d 100644 --- a/src/ir/Command.cpp +++ b/src/ir/Command.cpp @@ -18,13 +18,13 @@ namespace storm { // Nothing to do here. } - Command::Command(std::string const& actionName, std::shared_ptr guardExpression, std::vector const& updates) - : actionName(actionName), guardExpression(guardExpression), updates(updates) { + Command::Command(uint_fast64_t globalIndex, std::string const& actionName, std::shared_ptr guardExpression, std::vector const& updates) + : actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex) { // Nothing to do here. } - Command::Command(Command const& oldCommand, std::map const& renaming, storm::parser::prism::VariableState const& variableState) - : actionName(oldCommand.getActionName()), guardExpression(oldCommand.guardExpression->clone(renaming, variableState)) { + Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState) + : actionName(oldCommand.getActionName()), guardExpression(oldCommand.guardExpression->clone(renaming, variableState)), globalIndex(newGlobalIndex) { auto renamingPair = renaming.find(this->actionName); if (renamingPair != renaming.end()) { this->actionName = renamingPair->first; @@ -51,6 +51,10 @@ namespace storm { return this->updates[index]; } + uint_fast64_t Command::getGlobalIndex() const { + return this->globalIndex; + } + std::string Command::toString() const { std::stringstream result; result << "[" << actionName << "] " << guardExpression->toString() << " -> "; diff --git a/src/ir/Command.h b/src/ir/Command.h index c2045afd8..4682ccda2 100644 --- a/src/ir/Command.h +++ b/src/ir/Command.h @@ -38,21 +38,23 @@ namespace storm { /*! * Creates a command with the given name, guard and updates. * + * @param globalIndex The global index of the command. * @param actionName The action name of the command. * @param guardExpression the expression that defines the guard of the command. * @param updates A list of updates that is associated with this command. */ - Command(std::string const& actionName, std::shared_ptr guardExpression, std::vector const& updates); + Command(uint_fast64_t globalIndex, std::string const& actionName, std::shared_ptr guardExpression, std::vector const& updates); /*! * Creates a copy of the given command and performs the provided renaming. * * @param oldCommand The command to copy. + * @param newGlobalIndex The global index of the copy of the command. * @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. */ - Command(Command const& oldCommand, std::map const& renaming, storm::parser::prism::VariableState const& variableState); + Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map const& renaming, storm::parser::prism::VariableState const& variableState); /*! * Retrieves the action name of this command. @@ -82,6 +84,13 @@ namespace storm { */ storm::ir::Update const& getUpdate(uint_fast64_t index) const; + /*! + * Retrieves the global index of the command, that is, a unique index over all modules. + * + * @return The global index of the command. + */ + uint_fast64_t getGlobalIndex() const; + /*! * Retrieves a string representation of this command. * @@ -98,6 +107,9 @@ namespace storm { // The list of updates of the command. std::vector updates; + + // The global index of the command. + uint_fast64_t globalIndex; }; } // namespace ir diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index e9d904dbf..3d92acd10 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -72,7 +72,8 @@ namespace storm { // Now we are ready to clone all commands and rename them if requested. this->commands.reserve(oldModule.getNumberOfCommands()); for (Command const& command : oldModule.commands) { - this->commands.emplace_back(command, renaming, variableState); + this->commands.emplace_back(command, variableState.getNextGlobalCommandIndex(), renaming, variableState); + variableState.nextGlobalCommandIndex++; } this->collectActions(); diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h index 2cc6fe8d4..b76211a92 100644 --- a/src/models/AbstractDeterministicModel.h +++ b/src/models/AbstractDeterministicModel.h @@ -28,8 +28,9 @@ class AbstractDeterministicModel: public AbstractModel { * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ AbstractDeterministicModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) - : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, + boost::optional>> const& optionalChoiceLabeling) + : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { } /*! Constructs an abstract determinstic model from the given parameters. @@ -41,9 +42,11 @@ class AbstractDeterministicModel: public AbstractModel { * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ AbstractDeterministicModel(storm::storage::SparseMatrix&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, - boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix) + boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class - : AbstractModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix)) { + : AbstractModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), + std::move(optionalChoiceLabeling)) { // Intentionally left empty. } diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index 83e4bbc4a..27aef7480 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -18,7 +18,7 @@ namespace models { * @brief Enumeration of all supported types of models. */ enum ModelType { - Unknown, DTMC, CTMC, MDP, CTMDP + Unknown, DTMC, CTMC, MDP, UPDATE_LABELED_MDP, CTMDP }; /*! @@ -44,7 +44,8 @@ class AbstractModel: public std::enable_shared_from_this> { : transitionMatrix(other.transitionMatrix), stateLabeling(other.stateLabeling), stateRewardVector(other.stateRewardVector), - transitionRewardMatrix(other.transitionRewardMatrix) { + transitionRewardMatrix(other.transitionRewardMatrix), + choiceLabeling(other.choiceLabeling) { // Intentionally left empty. } @@ -56,7 +57,8 @@ class AbstractModel: public std::enable_shared_from_this> { : transitionMatrix(std::move(other.transitionMatrix)), stateLabeling(std::move(other.stateLabeling)), stateRewardVector(std::move(other.stateRewardVector)), - transitionRewardMatrix(std::move(other.transitionRewardMatrix)) { + transitionRewardMatrix(std::move(other.transitionRewardMatrix)), + choiceLabeling(std::move(other.choiceLabeling)) { // Intentionally left empty. } @@ -67,17 +69,22 @@ class AbstractModel: public std::enable_shared_from_this> { * propositions to each state. * @param stateRewardVector The reward values associated with the states. * @param transitionRewardMatrix The reward values associated with the transitions of the model. + * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ AbstractModel(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, + boost::optional>> const& optionalChoiceLabeling) : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling) { - if (optionalStateRewardVector) { // Boost::Optional + if (optionalStateRewardVector) { this->stateRewardVector.reset(optionalStateRewardVector.get()); } - if (optionalTransitionRewardMatrix) { // Boost::Optional + if (optionalTransitionRewardMatrix) { this->transitionRewardMatrix.reset(optionalTransitionRewardMatrix.get()); } + if (optionalChoiceLabeling) { + this->choiceLabeling.reset(optionalChoiceLabeling.get()); + } } /*! Constructs an abstract model from the given transition matrix and @@ -89,9 +96,11 @@ class AbstractModel: public std::enable_shared_from_this> { * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ AbstractModel(storm::storage::SparseMatrix&& transitionMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, - boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix) : + boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, + boost::optional>>&& optionalChoiceLabeling) : transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), - stateRewardVector(std::move(optionalStateRewardVector)), transitionRewardMatrix(std::move(optionalTransitionRewardMatrix)) { } + stateRewardVector(std::move(optionalStateRewardVector)), transitionRewardMatrix(std::move(optionalTransitionRewardMatrix)), + choiceLabeling(std::move(optionalChoiceLabeling)) { } /*! * Destructor. @@ -507,6 +516,9 @@ private: /*! The transition-based rewards of the model. */ boost::optional> transitionRewardMatrix; + + /*! The labeling that is associated with the choices for each state. */ + boost::optional>> choiceLabeling; }; } // namespace models diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h index 59f1632fb..013ab5448 100644 --- a/src/models/AbstractNondeterministicModel.h +++ b/src/models/AbstractNondeterministicModel.h @@ -26,14 +26,16 @@ class AbstractNondeterministicModel: public AbstractModel { * @param choiceIndices A mapping from states to rows in the transition matrix. * @param stateRewardVector The reward values associated with the states. * @param transitionRewardMatrix The reward values associated with the transitions of the model. + * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ AbstractNondeterministicModel( storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, std::vector const& nondeterministicChoiceIndices, boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix) - : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { + boost::optional> const& optionalTransitionRewardMatrix, + boost::optional>> const& optionalChoiceLabeling) + : AbstractModel(transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { this->nondeterministicChoiceIndices = nondeterministicChoiceIndices; } @@ -51,10 +53,11 @@ class AbstractNondeterministicModel: public AbstractModel { storm::models::AtomicPropositionsLabeling&& stateLabeling, std::vector&& nondeterministicChoiceIndices, boost::optional>&& optionalStateRewardVector, - boost::optional>&& optionalTransitionRewardMatrix) + boost::optional>&& optionalTransitionRewardMatrix, + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class - : AbstractModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix)), - nondeterministicChoiceIndices(std::move(nondeterministicChoiceIndices)) { + : AbstractModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), + std::move(optionalChoiceLabeling)), nondeterministicChoiceIndices(std::move(nondeterministicChoiceIndices)) { // Intentionally left empty. } diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h index faf16c0ec..9febcfb5f 100644 --- a/src/models/Ctmc.h +++ b/src/models/Ctmc.h @@ -36,8 +36,9 @@ public: * propositions to each state. */ Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) - : AbstractDeterministicModel(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, + boost::optional>> const& optionalChoiceLabeling) + : AbstractDeterministicModel(rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { // Intentionally left empty. } @@ -50,9 +51,11 @@ public: * propositions to each state. */ Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, - boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix) + boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class - : AbstractDeterministicModel(std::move(rateMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix)) { + : AbstractDeterministicModel(std::move(rateMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), + std::move(optionalChoiceLabeling)) { // Intentionally left empty. } diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h index b5763da25..f80525602 100644 --- a/src/models/Ctmdp.h +++ b/src/models/Ctmdp.h @@ -41,8 +41,10 @@ public: storm::models::AtomicPropositionsLabeling const& stateLabeling, std::vector const& nondeterministicChoiceIndices, boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix) - : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix) { + boost::optional> const& optionalTransitionRewardMatrix, + boost::optional>> const& optionalChoiceLabeling) + : AbstractNondeterministicModel(probabilityMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, + optionalChoiceLabeling) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; @@ -62,9 +64,11 @@ public: storm::models::AtomicPropositionsLabeling&& stateLabeling, std::vector&& nondeterministicChoiceIndices, boost::optional>&& optionalStateRewardVector, - boost::optional>&& optionalTransitionRewardMatrix) + boost::optional>&& optionalTransitionRewardMatrix, + boost::optional>> const& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class - : AbstractNondeterministicModel(std::move(probabilityMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix)) { + : AbstractNondeterministicModel(std::move(probabilityMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), + std::move(optionalChoiceLabeling)) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h index f3eb385b9..0254204bb 100644 --- a/src/models/Dtmc.h +++ b/src/models/Dtmc.h @@ -42,8 +42,9 @@ public: * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, - boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix) - : AbstractDeterministicModel(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix) { + boost::optional> const& optionalStateRewardVector, boost::optional> const& optionalTransitionRewardMatrix, + boost::optional>> const& optionalChoiceLabeling) + : AbstractDeterministicModel(probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; @@ -67,9 +68,11 @@ public: * @param transitionRewardMatrix The reward values associated with the transitions of the model. */ Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::AtomicPropositionsLabeling&& stateLabeling, - boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix) + boost::optional>&& optionalStateRewardVector, boost::optional>&& optionalTransitionRewardMatrix, + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class - : AbstractDeterministicModel(std::move(probabilityMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix)) { + : AbstractDeterministicModel(std::move(probabilityMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), + std::move(optionalChoiceLabeling)) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; diff --git a/src/models/Mdp.h b/src/models/Mdp.h index ffe10cde7..5e0d99955 100644 --- a/src/models/Mdp.h +++ b/src/models/Mdp.h @@ -31,20 +31,25 @@ class Mdp : public storm::models::AbstractNondeterministicModel { public: /*! - * Constructs a MDP object from the given transition probability matrix and - * the given labeling of the states. + * Constructs a MDP object from the given transition probability matrix and the given labeling of the states. * All values are copied. - * @param probabilityMatrix The transition probability relation of the - * MDP given by a matrix. - * @param stateLabeling The labeling that assigns a set of atomic - * propositions to each state. + * + * @param probabilityMatrix The transition probability relation of the MDP given by a matrix. + * @param stateLabeling The labeling that assigns a set of atomic propositions to each state. + * @param nondeterministicChoiceIndices The row indices in the sparse matrix at which the nondeterministic + * choices of a given state begin. + * @param optionalStateRewardVector A vector assigning rewards to states. + * @param optionalTransitionRewardVector A sparse matrix that represents an assignment of rewards to the transitions. + * @param optionalChoiceLabeling A vector that represents the labels associated with each nondeterministic choice of + * a state. */ Mdp(storm::storage::SparseMatrix const& transitionMatrix, storm::models::AtomicPropositionsLabeling const& stateLabeling, std::vector const& nondeterministicChoiceIndices, boost::optional> const& optionalStateRewardVector, - boost::optional> const& optionalTransitionRewardMatrix) - : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix) { + boost::optional> const& optionalTransitionRewardMatrix, + boost::optional>> const& optionalChoiceLabeling) + : AbstractNondeterministicModel(transitionMatrix, stateLabeling, nondeterministicChoiceIndices, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; @@ -64,9 +69,11 @@ public: storm::models::AtomicPropositionsLabeling&& stateLabeling, std::vector&& nondeterministicChoiceIndices, boost::optional>&& optionalStateRewardVector, - boost::optional>&& optionalTransitionRewardMatrix) + boost::optional>&& optionalTransitionRewardMatrix, + boost::optional>>&& optionalChoiceLabeling) // The std::move call must be repeated here because otherwise this calls the copy constructor of the Base Class - : AbstractNondeterministicModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix)) { + : AbstractNondeterministicModel(std::move(transitionMatrix), std::move(stateLabeling), std::move(nondeterministicChoiceIndices), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), + std::move(optionalChoiceLabeling)) { if (!this->checkValidityOfProbabilityMatrix()) { LOG4CPLUS_ERROR(logger, "Probability matrix is invalid."); throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid."; diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp index af38c1a7f..03744401b 100644 --- a/src/parser/DeterministicModelParser.cpp +++ b/src/parser/DeterministicModelParser.cpp @@ -58,7 +58,7 @@ DeterministicModelParserResultContainer parseDeterministicModel(std::str storm::models::Dtmc DeterministicModelParserAsDtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { DeterministicModelParserResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); - return storm::models::Dtmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards)); + return storm::models::Dtmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } /*! @@ -69,7 +69,7 @@ storm::models::Dtmc DeterministicModelParserAsDtmc(std::string const & t storm::models::Ctmc DeterministicModelParserAsCtmc(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { DeterministicModelParserResultContainer parserResult(std::move(parseDeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); - return storm::models::Ctmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards)); + return storm::models::Ctmc(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } } /* namespace parser */ diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp index f59e17862..bbe39ae02 100644 --- a/src/parser/NondeterministicModelParser.cpp +++ b/src/parser/NondeterministicModelParser.cpp @@ -58,7 +58,7 @@ NondeterministicModelParserResultContainer parseNondeterministicModel(st storm::models::Mdp NondeterministicModelParserAsMdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards)); + return storm::models::Mdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } /*! @@ -69,7 +69,7 @@ storm::models::Mdp NondeterministicModelParserAsMdp(std::string const & storm::models::Ctmdp NondeterministicModelParserAsCtmdp(std::string const & transitionSystemFile, std::string const & labelingFile, std::string const & stateRewardFile, std::string const & transitionRewardFile) { NondeterministicModelParserResultContainer parserResult = parseNondeterministicModel(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile); - return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards)); + return storm::models::Ctmdp(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(parserResult.rowMapping), std::move(parserResult.stateRewards), std::move(parserResult.transitionRewards), boost::optional>>()); } } /* namespace parser */ diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index 2b59fdf5d..8d3ed0fc8 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -108,8 +108,9 @@ void createRewardModel(std::string name, std::vector& stateRewards, Update createUpdate(std::shared_ptr likelihood, std::map& bools, std::map ints) { return Update(likelihood, bools, ints); } -Command createCommand(std::string& label, std::shared_ptr guard, std::vector& updates) { - return Command(label, guard, updates); +Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr guard, std::vector const& updates) { + this->state->nextGlobalCommandIndex++; + return Command(this->state->getNextGlobalCommandIndex() - 1, label, guard, updates); } Program createProgram( Program::ModelType modelType, @@ -164,7 +165,7 @@ PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new Variabl qi::lit("[") > -( (FreeIdentifierGrammar::instance(this->state)[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1] ) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit("->") > updateListDefinition > qi::lit(";") - )[qi::_val = phoenix::bind(&createCommand, qi::_a, qi::_2, qi::_3)]; + )[qi::_val = phoenix::bind(&PrismGrammar::createCommand, this, qi::_a, qi::_2, qi::_3)]; commandDefinition.name("command"); // This block defines all entities that are needed for parsing variable definitions. diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index 5731e35c7..bb0b9e8f7 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -215,6 +215,16 @@ private: * @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices. */ void createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& booleanVariables, std::map& booleanVariableToGlobalIndexMap); + + /*! + * 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); + }; diff --git a/src/parser/prismparser/VariableState.cpp b/src/parser/prismparser/VariableState.cpp index b5f61648e..fd2e5e217 100644 --- a/src/parser/prismparser/VariableState.cpp +++ b/src/parser/prismparser/VariableState.cpp @@ -31,7 +31,7 @@ std::ostream& operator<<(std::ostream& out, VariableState::variableNamesStruct& } -VariableState::VariableState(bool firstRun) : firstRun(firstRun), keywords(), nextLocalBooleanVariableIndex(0), nextLocalIntegerVariableIndex(0), nextGlobalBooleanVariableIndex(0), nextGlobalIntegerVariableIndex(0) { +VariableState::VariableState(bool firstRun) : firstRun(firstRun), keywords(), nextLocalBooleanVariableIndex(0), nextLocalIntegerVariableIndex(0), nextGlobalBooleanVariableIndex(0), nextGlobalIntegerVariableIndex(0), nextGlobalCommandIndex(0) { // Nothing to do here. } @@ -51,6 +51,10 @@ 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 << "."); @@ -161,6 +165,7 @@ void VariableState::prepareForSecondRun() { doubleConstants_.clear(); allConstantNames_.clear(); this->firstRun = false; + nextGlobalCommandIndex = 0; } } // namespace prism diff --git a/src/parser/prismparser/VariableState.h b/src/parser/prismparser/VariableState.h index 1ca299c43..1895eefe0 100644 --- a/src/parser/prismparser/VariableState.h +++ b/src/parser/prismparser/VariableState.h @@ -99,6 +99,18 @@ public: */ 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_;