From 5f64fd168b374387eb0106f22c8832de3b70759a Mon Sep 17 00:00:00 2001 From: gereon Date: Fri, 15 Mar 2013 13:03:59 +0100 Subject: [PATCH] Cleaned up structure of ExplicitModelAdapter. - added cpp file - returns complete models now (missing transition rewards...) --- src/adapters/ExplicitModelAdapter.h | 544 ++++------------------------ 1 file changed, 75 insertions(+), 469 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 8b8e5dee3..1010929a5 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -1,55 +1,44 @@ -/* - * IntermediateRepresentationAdapter.h +/* + * File: ExplicitModelAdapter.h + * Author: Gereon Kremer * - * Created on: 13.01.2013 - * Author: Christian Dehnert + * Created on March 15, 2013, 11:42 AM */ -#ifndef STORM_IR_EXPLICITMODELADAPTER_H_ -#define STORM_IR_EXPLICITMODELADAPTER_H_ +#ifndef EXPLICITMODELADAPTER_H +#define EXPLICITMODELADAPTER_H -#include "src/storage/SparseMatrix.h" -#include "src/utility/Settings.h" +#include +#include +#include +#include +#include -#include "src/ir/RewardModel.h" +#include "src/ir/Program.h" #include "src/ir/StateReward.h" #include "src/ir/TransitionReward.h" #include "src/models/AbstractModel.h" -#include "src/models/Dtmc.h" -#include "src/models/Ctmc.h" -#include "src/models/Mdp.h" - -#include -#include -#include -#include -#include -#include -#include -#include -#include - -typedef std::pair, std::vector> StateType; - -#include "log4cplus/logger.h" -#include "log4cplus/loggingmacros.h" -#include "ir/Program.h" -extern log4cplus::Logger logger; +#include "src/models/AtomicPropositionsLabeling.h" +#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.begin(); it != state->first.end(); ++it) { - boost::hash_combine(seed, *it); + for (auto it : state->first) { + boost::hash_combine(seed, it); } - for (auto it = state->second.begin(); it != state->second.end(); ++it) { - boost::hash_combine(seed, *it); + for (auto it : state->second) { + boost::hash_combine(seed, it); } return seed; } @@ -64,131 +53,47 @@ public: class ExplicitModelAdapter { public: - ExplicitModelAdapter(std::shared_ptr program) : program(program), allStates(), - stateToIndexMap(), booleanVariables(), integerVariables(), booleanVariableToIndexMap(), - integerVariableToIndexMap(), numberOfTransitions(0) { - - } - - std::shared_ptr toModel(std::string const & rewardModelName = "") { - - std::shared_ptr> matrix = this->toSparseMatrix(); - - std::shared_ptr stateLabeling = this->getStateLabeling(this->program->getLabels()); - std::shared_ptr> stateRewards = nullptr; - std::shared_ptr> transitionRewardMatrix = nullptr; - - if (rewardModelName != "") { - storm::ir::RewardModel rewardModel = this->program->getRewardModel(rewardModelName); - stateRewards = this->getStateRewards(rewardModel.getStateRewards()); - } - - switch (this->program->getModelType()) - { -/* std::shared_ptr> probabilityMatrix, - std::shared_ptr stateLabeling, - std::shared_ptr> stateRewards = nullptr, - std::shared_ptr> transitionRewardMatrix = nullptr -*/ - case storm::ir::Program::DTMC: - return std::shared_ptr(new storm::models::Dtmc(matrix, stateLabeling, stateRewards, transitionRewardMatrix)); - break; - case storm::ir::Program::CTMC: - return std::shared_ptr(new storm::models::Ctmc(matrix, stateLabeling, stateRewards, transitionRewardMatrix)); - break; - case storm::ir::Program::MDP: - return std::shared_ptr(new storm::models::Mdp(matrix, stateLabeling, stateRewards, transitionRewardMatrix)); - break; - case storm::ir::Program::CTMDP: - // Todo - //return std::shared_ptr(new storm::models::Ctmdp(matrix, stateLabeling, stateRewards, transitionRewardMatrix)); - break; - default: - // ERROR - break; - } - - return std::shared_ptr(nullptr); - } - - std::shared_ptr> toSparseMatrix() { - LOG4CPLUS_INFO(logger, "Creating sparse matrix for probabilistic program."); - - std::shared_ptr> resultMatrix = this->buildMatrix(); + ExplicitModelAdapter(std::shared_ptr program); + ~ExplicitModelAdapter(); - LOG4CPLUS_INFO(logger, "Created sparse matrix with " << resultMatrix->getRowCount() << " reachable states and " << resultMatrix->getNonZeroEntryCount() << " transitions."); - - this->clearReachableStateSpace(); - - return resultMatrix; - } + std::shared_ptr getModel(std::string const & rewardModelName = ""); private: - static void setValue(StateType* state, uint_fast64_t index, bool value) { - std::get<0>(*state)[index] = value; - } - static void setValue(StateType* state, uint_fast64_t index, int_fast64_t value) { - std::get<1>(*state)[index] = value; - } - - std::shared_ptr> getStateRewards(std::vector const & rewards) { - std::shared_ptr> results(new std::vector(this->allStates.size())); - for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { - for (auto reward: rewards) { - (*results)[index] = reward.getReward(this->allStates[index]); - } - } - return results; - } + // First some generic routines to operate on states. - std::shared_ptr getStateLabeling(std::map> labels) { - std::shared_ptr results(new storm::models::AtomicPropositionsLabeling(this->allStates.size(), labels.size())); - for (auto it: labels) { - results->addAtomicProposition(it.first); - } - for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { - for (auto label: labels) { - if (label.second->getValueAsBool(this->allStates[index])) { - results->addAtomicPropositionToState(label.first, index); - } - } - } - return results; - } - /*! - * Initializes all internal variables. + * 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. */ - void prepareAuxiliaryDatastructures() { - uint_fast64_t numberOfIntegerVariables = 0; - uint_fast64_t numberOfBooleanVariables = 0; - for (uint_fast64_t i = 0; i < program->getNumberOfModules(); ++i) { - numberOfIntegerVariables += program->getModule(i).getNumberOfIntegerVariables(); - numberOfBooleanVariables += program->getModule(i).getNumberOfBooleanVariables(); - } + 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); + /*! + * 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; - this->booleanVariables.resize(numberOfBooleanVariables); - this->integerVariables.resize(numberOfIntegerVariables); + /*! + * 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(); - uint_fast64_t nextBooleanVariableIndex = 0; - uint_fast64_t nextIntegerVariableIndex = 0; - for (uint_fast64_t i = 0; i < program->getNumberOfModules(); ++i) { - storm::ir::Module const& module = program->getModule(i); + std::shared_ptr> getStateRewards(std::vector const & rewards); + std::shared_ptr getStateLabeling(std::map> labels); - for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { - this->booleanVariables[nextBooleanVariableIndex] = module.getBooleanVariable(j); - this->booleanVariableToIndexMap[module.getBooleanVariable(j).getName()] = nextBooleanVariableIndex; - ++nextBooleanVariableIndex; - } - for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { - this->integerVariables[nextIntegerVariableIndex] = module.getIntegerVariable(j); - this->integerVariableToIndexMap[module.getIntegerVariable(j).getName()] = nextIntegerVariableIndex; - ++nextIntegerVariableIndex; - } - } - } - /*! * Retrieves all active command labeled by some label, ordered by modules. * @@ -202,106 +107,13 @@ private: * @param action Action label. * @return Active commands. */ - std::unique_ptr>> 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); - - std::shared_ptr> 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 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. - // This is how lambdas may look like in C++... - res->sort([](const std::list& a, const std::list& b){ 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* applyUpdate(StateType const * const state, storm::ir::Update const & update) { - StateType* newState = new StateType(*state); - for (auto assignedVariable : update.getBooleanAssignments()) { - setValue(newState, this->booleanVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsBool(state)); - } - for (auto assignedVariable : update.getIntegerAssignments()) { - setValue(newState, this->integerVariableToIndexMap[assignedVariable.first], assignedVariable.second.getExpression()->getValueAsInt(state)); - } - return newState; - } + std::unique_ptr>> getActiveCommandsByAction(StateType const * state, std::string& action); /*! * Generates all initial states and adds them to allStates. */ - void generateInitialStates() { - // Create a fresh state which can hold as many boolean and integer variables as there are. - this->allStates.clear(); - this->allStates.push_back(new StateType()); - this->allStates[0]->first.resize(this->booleanVariables.size()); - this->allStates[0]->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) { - // No initial value was given. - uint_fast64_t size = this->allStates.size(); - for (uint_fast64_t pos = 0; pos < size; pos++) { - // Duplicate each state, one with true and one with false. - this->allStates.push_back(new StateType(*this->allStates[pos])); - std::get<0>(*this->allStates[pos])[i] = false; - std::get<0>(*this->allStates[size + pos])[i] = true; - } - } else { - // Initial value was given. - bool initialValue = this->booleanVariables[i].getInitialValue()->getValueAsBool(this->allStates[0]); - for (auto it : this->allStates) { - std::get<0>(*it)[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. - uint_fast64_t size = this->allStates.size(); - int_fast64_t lower = this->integerVariables[i].getLowerBound()->getValueAsInt(this->allStates[0]); - int_fast64_t upper = this->integerVariables[i].getUpperBound()->getValueAsInt(this->allStates[0]); - - // Duplicate all states for all values in variable interval. - for (int_fast64_t value = lower; value <= upper; value++) { - for (uint_fast64_t pos = 0; pos < size; pos++) { - // If value is lower bound, we reuse the existing state, otherwise we create a new one. - if (value > lower) this->allStates.push_back(new StateType(*this->allStates[pos])); - // Set value to current state. - std::get<1>(*this->allStates[(value - lower) * size + pos])[i] = value; - } - } - } else { - // Initial value was given. - int_fast64_t initialValue = this->integerVariables[i].getInitialValue()->getValueAsInt(this->allStates[0]); - for (auto it : this->allStates) { - std::get<1>(*it)[i] = initialValue; - } - } - } - } - + void generateInitialStates(); + /*! * 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. @@ -311,171 +123,29 @@ private: * @param state Pointer to state, shall not be used afterwards. * @returns State id of given state. */ - uint_fast64_t 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; - } - } + 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) { - 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(); - - // 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)); - - // 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); - } - } - } - } - } - + 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 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. - 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, update); - // 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); - } - } - } - } - 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.emplace_back(); - std::map* states = &res.back(); - - // Now add our final result states to our global result. - for (auto it : resultStates) { - uint_fast64_t newStateID = this->getOrAddStateId(it.first); - (*states)[newStateID] = it.second; - } - this->numberOfTransitions += states->size(); - } - } - - } + 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. */ - std::shared_ptr> buildDTMCMatrix(std::map>> intermediate) { - std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size())); - // 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 : intermediate[state]) { - for (auto elem : choice) { - set.insert(elem.first); - } - } - numberOfTransitions += set.size(); - } - std::cout << "Building DTMC matrix with " << numberOfTransitions << " transitions." << std::endl; - // Now build matrix. - result->initialize(numberOfTransitions); - for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { - if (intermediate[state].size() > 1) { - std::cout << "Warning: state " << state << " has " << intermediate[state].size() << " overlapping guards in dtmc" << std::endl; - } - // Combine choices to one map. - std::map map; - for (auto choice : intermediate[state]) { - for (auto elem : choice) { - map[elem.first] += elem.second; - } - } - // Scale probabilities by number of choices. - double factor = 1.0 / intermediate[state].size(); - for (auto it : map) { - result->addNextValue(state, it.first, it.second * factor); - } - - } - result->finalize(); - return result; - } + std::shared_ptr> buildDeterministicMatrix(); /*! * Create matrix from intermediate mapping, assuming it is a mdp model. @@ -483,23 +153,7 @@ private: * @param choices Overall number of choices for all nodes. * @return result matrix. */ - std::shared_ptr> buildMDPMatrix(std::map>> intermediate, uint_fast64_t choices) { - std::cout << "Building MDP matrix with " << this->numberOfTransitions << " transitions." << std::endl; - std::shared_ptr> result(new storm::storage::SparseMatrix(allStates.size(), choices)); - // Build matrix. - result->initialize(this->numberOfTransitions); - uint_fast64_t nextRow = 0; - for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { - for (auto choice : intermediate[state]) { - for (auto it : choice) { - result->addNextValue(nextRow, it.first, it.second); - } - nextRow++; - } - } - result->finalize(); - return result; - } + std::shared_ptr> buildNondeterministicMatrix(); /*! * Build matrix from model. Starts with all initial states and explores the reachable state space. @@ -507,73 +161,25 @@ private: * Afterwards, we transform this map into the actual matrix. * @return result matrix. */ - std::shared_ptr> buildMatrix() { - this->prepareAuxiliaryDatastructures(); - this->allStates.clear(); - this->stateToIndexMap.clear(); - this->numberOfTransitions = 0; - uint_fast64_t choices; - std::map>> intermediate; - - this->generateInitialStates(); - for (uint_fast64_t curIndex = 0; curIndex < this->allStates.size(); curIndex++) - { - this->addUnlabeledTransitions(curIndex, intermediate[curIndex]); - this->addLabeledTransitions(curIndex, intermediate[curIndex]); - - choices += intermediate[curIndex].size(); - if (intermediate[curIndex].size() == 0) { - // This is a deadlock state. - if (storm::settings::instance()->isSet("fix-deadlocks")) { - this->numberOfTransitions++; - intermediate[curIndex].emplace_back(); - intermediate[curIndex].back()[curIndex] = 1; - } else { - LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state."); - throw storm::exceptions::WrongFileFormatException() << "Error while creating sparse matrix from probabilistic program: found deadlock state."; - } - } - } - - - switch (this->program->getModelType()) { - case storm::ir::Program::DTMC: - case storm::ir::Program::CTMC: - return this->buildDTMCMatrix(intermediate); - case storm::ir::Program::MDP: - case storm::ir::Program::CTMDP: - return this->buildMDPMatrix(intermediate, choices); - default: - LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: We can't handle this model type."); - throw storm::exceptions::WrongFileFormatException() << "Error while creating sparse matrix from probabilistic program: We can't handle this model type."; - break; - } - return std::shared_ptr>(nullptr); - } - - /*! - * Free all StateType objects and clear maps. - */ - void clearReachableStateSpace() { - for (auto it : allStates) { - delete it; - } - allStates.clear(); - stateToIndexMap.clear(); - } + void buildIntermediateRepresentation(); + // Program that should be converted. std::shared_ptr program; - std::vector allStates; - std::unordered_map stateToIndexMap; std::vector booleanVariables; std::vector integerVariables; - std::unordered_map booleanVariableToIndexMap; - std::unordered_map integerVariableToIndexMap; + std::map booleanVariableToIndexMap; + std::map integerVariableToIndexMap; + + // Members that are filled during the conversion. + std::vector allStates; + std::unordered_map stateToIndexMap; uint_fast64_t numberOfTransitions; + uint_fast64_t numberOfChoices; + std::map>> transitionMap; }; } // namespace adapters - } // namespace storm -#endif /* STORM_IR_EXPLICITMODELADAPTER_H_ */ +#endif /* EXPLICITMODELADAPTER_H */ +