diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 63dddd452..14254eae5 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -34,20 +34,7 @@ bool ExplicitModelAdapterOptionsRegistered = storm::settings::Settings::register namespace storm { 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(); - } - - void ExplicitModelAdapter::defineUndefinedConstants(std::string const& constantDefinitionString) { + void ExplicitModelAdapter::defineUndefinedConstants(storm::ir::Program& program, std::string const& constantDefinitionString) { if (!constantDefinitionString.empty()) { // Parse the string that defines the undefined constants of the model and make sure that it contains exactly // one value for each undefined constant of the model. @@ -103,7 +90,7 @@ namespace storm { } } - void ExplicitModelAdapter::undefineUndefinedConstants() { + void ExplicitModelAdapter::undefineUndefinedConstants(storm::ir::Program& program) { for (auto nameExpressionPair : program.getBooleanUndefinedConstantExpressionsMap()) { nameExpressionPair.second->undefine(); } @@ -115,64 +102,58 @@ namespace storm { } } - std::shared_ptr> ExplicitModelAdapter::getModel(std::string const& constantDefinitionString, std::string const& rewardModelName) { - // Start by defining the remaining constants in the model. - this->defineUndefinedConstants(constantDefinitionString); + ExplicitModelAdapter::StateInformation ExplicitModelAdapter::exploreReachableStateSpace(storm::ir::Program const& program) { + StateInformation stateInformation; - // Initialize reward model. - this->rewardModel = nullptr; - if (rewardModelName != "") { - this->rewardModel = std::unique_ptr(new storm::ir::RewardModel(this->program.getRewardModel(rewardModelName))); - } + // Initialize a queue, insert the starting state and explore the current state until there is no more reachable state. - // State expansion, build temporary map, compute transition rewards. - this->buildTransitionMap(); + return stateInformation; + } + + ExplicitModelAdapter::ModelComponents ExplicitModelAdapter::buildModelComponents(storm::ir::Program const& program, std::string const& rewardModelName) { + ModelComponents modelComponents; - // Compute labeling. - storm::models::AtomicPropositionsLabeling stateLabeling = this->getStateLabeling(this->program.getLabels()); + // Start by exploring the state space. + StateInformation stateInformation = exploreReachableStateSpace(program); - // Compute state rewards. - boost::optional> stateRewards; - if ((this->rewardModel != nullptr) && this->rewardModel->hasStateRewards()) { - stateRewards.reset(this->getStateRewards(this->rewardModel->getStateRewards())); - } + // Then build the transition matrix for the reachable states. + + // Now build the state labeling. + + // Finally, construct the state rewards. + + return modelComponents; + } + + std::shared_ptr> ExplicitModelAdapter::translateProgram(storm::ir::Program program, std::string const& constantDefinitionString, std::string const& rewardModelName) { + // Start by defining the undefined constants in the model. + defineUndefinedConstants(program, constantDefinitionString); + + ModelComponents modelComponents = buildModelComponents(program, rewardModelName); std::shared_ptr> result; - // Build and return actual model. - switch (this->program.getModelType()) - { + switch (program.getModelType()) { case storm::ir::Program::DTMC: - { - storm::storage::SparseMatrix matrix = this->buildDeterministicMatrix(); - result = std::shared_ptr>(new storm::models::Dtmc(matrix, stateLabeling, stateRewards, this->transitionRewards, this->choiceLabeling)); + result = std::shared_ptr>(new storm::models::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); break; - } case storm::ir::Program::CTMC: - { - storm::storage::SparseMatrix matrix = this->buildDeterministicMatrix(); - result = std::shared_ptr>(new storm::models::Ctmc(matrix, stateLabeling, stateRewards, this->transitionRewards, this->choiceLabeling)); + result = std::shared_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); + break; break; - } case storm::ir::Program::MDP: - { - storm::storage::SparseMatrix matrix = this->buildNondeterministicMatrix(); - result = std::shared_ptr>(new storm::models::Mdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards, this->choiceLabeling)); + result = std::shared_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); break; - } case storm::ir::Program::CTMDP: - { - storm::storage::SparseMatrix matrix = this->buildNondeterministicMatrix(); - result = std::shared_ptr>(new storm::models::Ctmdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards, this->choiceLabeling)); + result = std::shared_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), std::move(modelComponents.stateRewards), std::move(modelComponents.transitionRewardMatrix), std::move(modelComponents.choiceLabeling))); break; - } default: LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type."); throw storm::exceptions::WrongFormatException() << "Error while creating model from probabilistic program: cannot handle this model type."; break; } - + // Undefine the constants so that the program can be used again somewhere else. - undefineUndefinedConstants(); + undefineUndefinedConstants(program); return result; } @@ -192,492 +173,479 @@ namespace storm { 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; + StateType* ExplicitModelAdapter::applyUpdate(storm::ir::Program const& program, StateType const* state, storm::ir::Update const& update) { + return applyUpdate(program, state, state, update); } - storm::models::AtomicPropositionsLabeling ExplicitModelAdapter::getStateLabeling(std::map> labels) { - storm::models::AtomicPropositionsLabeling results(this->allStates.size(), labels.size() + 1); - // Initialize labeling. - for (auto const& labelExpressionPair : labels) { - results.addAtomicProposition(labelExpressionPair.first); - } - for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { - for (auto const& labelExpressionPair: labels) { - // Add label to state, if the corresponding expression is true. - if (labelExpressionPair.second->getValueAsBool(this->allStates[index])) { - results.addAtomicPropositionToState(labelExpressionPair.first, index); - } - } - } - - // Also label the initial state with the special label "init". - results.addAtomicProposition("init"); - StateType* initialState = this->getInitialState(); - uint_fast64_t initialIndex = this->stateToIndexMap[initialState]; - results.addAtomicPropositionToState("init", initialIndex); - delete initialState; - - return results; - } - - void ExplicitModelAdapter::initializeVariables() { - uint_fast64_t numberOfIntegerVariables = 0; - uint_fast64_t numberOfBooleanVariables = 0; - - // Count number of variables. - numberOfBooleanVariables += program.getNumberOfGlobalBooleanVariables(); - numberOfIntegerVariables += program.getNumberOfGlobalIntegerVariables(); - for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { - numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); - numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); - } - - this->booleanVariables.resize(numberOfBooleanVariables); - this->integerVariables.resize(numberOfIntegerVariables); - - // Create variables. - for (uint_fast64_t i = 0; i < program.getNumberOfGlobalBooleanVariables(); ++i) { - storm::ir::BooleanVariable var = program.getGlobalBooleanVariable(i); - this->booleanVariables[var.getGlobalIndex()] = var; - this->booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + StateType* ExplicitModelAdapter::applyUpdate(storm::ir::Program const& program, StateType const* state, StateType const* baseState, storm::ir::Update const& update) { + StateType* newState = new StateType(*state); + for (auto variableAssignmentPair : update.getBooleanAssignments()) { + setValue(newState, program.getGlobalIndexOfBooleanVariable(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsBool(baseState)); } - for (uint_fast64_t i = 0; i < program.getNumberOfGlobalIntegerVariables(); ++i) { - storm::ir::IntegerVariable var = program.getGlobalIntegerVariable(i); - this->integerVariables[var.getGlobalIndex()] = var; - this->integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); - } - for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { - storm::ir::Module const& module = program.getModule(i); - - for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { - storm::ir::BooleanVariable var = module.getBooleanVariable(j); - this->booleanVariables[var.getGlobalIndex()] = var; - this->booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); - } - for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { - storm::ir::IntegerVariable var = module.getIntegerVariable(j); - this->integerVariables[var.getGlobalIndex()] = var; - this->integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); - } + for (auto variableAssignmentPair : update.getIntegerAssignments()) { + setValue(newState, program.getGlobalIndexOfIntegerVariable(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsInt(baseState)); } + return newState; } - 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; - } +// 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; +// } - StateType* ExplicitModelAdapter::applyUpdate(StateType const* state, storm::ir::Update const& update) const { - return this->applyUpdate(state, state, update); - } +// storm::models::AtomicPropositionsLabeling ExplicitModelAdapter::getStateLabeling(std::map> labels) { +// storm::models::AtomicPropositionsLabeling results(this->allStates.size(), labels.size() + 1); +// // Initialize labeling. +// for (auto const& labelExpressionPair : labels) { +// results.addAtomicProposition(labelExpressionPair.first); +// } +// for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { +// for (auto const& labelExpressionPair: labels) { +// // Add label to state, if the corresponding expression is true. +// if (labelExpressionPair.second->getValueAsBool(this->allStates[index])) { +// results.addAtomicPropositionToState(labelExpressionPair.first, index); +// } +// } +// } +// +// // Also label the initial state with the special label "init". +// results.addAtomicProposition("init"); +// StateType* initialState = this->getInitialState(); +// uint_fast64_t initialIndex = this->stateToIndexMap[initialState]; +// results.addAtomicPropositionToState("init", initialIndex); +// delete initialState; +// +// return results; +// } - 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; - } +// void ExplicitModelAdapter::initializeVariables() { +// uint_fast64_t numberOfIntegerVariables = 0; +// uint_fast64_t numberOfBooleanVariables = 0; +// +// // Count number of variables. +// numberOfBooleanVariables += program.getNumberOfGlobalBooleanVariables(); +// numberOfIntegerVariables += program.getNumberOfGlobalIntegerVariables(); +// for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { +// numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); +// numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); +// } +// +// this->booleanVariables.resize(numberOfBooleanVariables); +// this->integerVariables.resize(numberOfIntegerVariables); +// +// // Create variables. +// for (uint_fast64_t i = 0; i < program.getNumberOfGlobalBooleanVariables(); ++i) { +// storm::ir::BooleanVariable var = program.getGlobalBooleanVariable(i); +// this->booleanVariables[var.getGlobalIndex()] = var; +// this->booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); +// } +// for (uint_fast64_t i = 0; i < program.getNumberOfGlobalIntegerVariables(); ++i) { +// storm::ir::IntegerVariable var = program.getGlobalIntegerVariable(i); +// this->integerVariables[var.getGlobalIndex()] = var; +// this->integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); +// } +// for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { +// storm::ir::Module const& module = program.getModule(i); +// +// for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { +// storm::ir::BooleanVariable var = module.getBooleanVariable(j); +// this->booleanVariables[var.getGlobalIndex()] = var; +// this->booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); +// } +// for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { +// storm::ir::IntegerVariable var = module.getIntegerVariable(j); +// this->integerVariables[var.getGlobalIndex()] = var; +// this->integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); +// } +// } +// } - 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; - } +// 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; +// } - uint_fast64_t ExplicitModelAdapter::getOrAddStateIndex(StateType* state) { - // Check, if the state was already registered. - auto indexIt = this->stateToIndexMap.find(state); - - if (indexIt == this->stateToIndexMap.end()) { - // The state has not been seen, yet, so add it to the list of all reachable states. - allStates.push_back(state); - stateToIndexMap[state] = allStates.size() - 1; - return allStates.size() - 1; - } else { - // The state was already encountered. Delete the copy of the old state and return its index. - delete state; - return indexIt->second; - } - } +// static StateType* ExplicitModelAdapter::getInitialState() { +// StateType* initialState = new StateType(); +// initialState->first.resize(this->booleanVariables.size()); +// initialState->second.resize(this->integerVariables.size()); +// +// // Start with boolean variables. +// for (uint_fast64_t i = 0; i < this->booleanVariables.size(); ++i) { +// // Check if an initial value is given +// if (this->booleanVariables[i].getInitialValue().get() == nullptr) { +// // If no initial value was given, we assume that the variable is initially false. +// std::get<0>(*initialState)[i] = false; +// } else { +// // Initial value was given. +// bool initialValue = this->booleanVariables[i].getInitialValue()->getValueAsBool(nullptr); +// std::get<0>(*initialState)[i] = initialValue; +// } +// } +// +// // Now process integer variables. +// for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) { +// // Check if an initial value was given. +// if (this->integerVariables[i].getInitialValue().get() == nullptr) { +// // No initial value was given, so we assume that the variable initially has the least value it can take. +// std::get<1>(*initialState)[i] = this->integerVariables[i].getLowerBound()->getValueAsInt(nullptr); +// } else { +// // Initial value was given. +// int_fast64_t initialValue = this->integerVariables[i].getInitialValue()->getValueAsInt(nullptr); +// std::get<1>(*initialState)[i] = initialValue; +// } +// } +// +// LOG4CPLUS_DEBUG(logger, "Generated initial state."); +// return initialState; +// } - 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(); - } - } - } - } +// static uint_fast64_t ExplicitModelAdapter::getOrAddStateIndex(StateType* state) { +// // Check, if the state was already registered. +// auto indexIt = this->stateToIndexMap.find(state); +// +// if (indexIt == this->stateToIndexMap.end()) { +// // The state has not been seen, yet, so add it to the list of all reachable states. +// allStates.push_back(state); +// stateToIndexMap[state] = allStates.size() - 1; +// return allStates.size() - 1; +// } else { +// // The state was already encountered. Delete the copy of the old state and return its index. +// delete state; +// return indexIt->second; +// } +// } - void ExplicitModelAdapter::addLabeledTransitions(uint_fast64_t stateIndex, std::list>, std::map>>& transitionList) { - for (std::string const& action : this->program.getActions()) { - StateType* currentState = this->allStates[stateIndex]; - boost::optional>> optionalActiveCommandLists = this->getActiveCommandsByAction(currentState, action); - - // Only process this action label, if there is at least one feasible solution. - if (optionalActiveCommandLists) { - std::vector> const& activeCommandList = optionalActiveCommandLists.get(); - std::vector::const_iterator> iteratorList(activeCommandList.size()); - - // Initialize the list of iterators. - for (size_t i = 0; i < activeCommandList.size(); ++i) { - iteratorList[i] = activeCommandList[i].cbegin(); - } - - // As long as there is one feasible combination of commands, keep on expanding it. - bool done = false; - while (!done) { - std::unordered_map* currentTargetStates = new std::unordered_map(); - std::unordered_map* newTargetStates = new std::unordered_map(); - (*currentTargetStates)[new StateType(*currentState)] = 1.0; - - // FIXME: This does not check whether a global variable is written multiple times. While the - // behaviour for this is undefined anyway, a warning should be issued in that case. - double probabilitySum = 0; - for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { - storm::ir::Command const& command = *iteratorList[i]; - - for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { - storm::ir::Update const& update = command.getUpdate(j); - - for (auto const& stateProbabilityPair : *currentTargetStates) { - StateType* newTargetState = this->applyUpdate(stateProbabilityPair.first, currentState, update); - probabilitySum += stateProbabilityPair.second * update.getLikelihoodExpression()->getValueAsDouble(currentState); - - auto existingStateProbabilityPair = newTargetStates->find(newTargetState); - if (existingStateProbabilityPair == newTargetStates->end()) { - (*newTargetStates)[newTargetState] = stateProbabilityPair.second * update.getLikelihoodExpression()->getValueAsDouble(currentState); - } else { - existingStateProbabilityPair->second += stateProbabilityPair.second * update.getLikelihoodExpression()->getValueAsDouble(currentState); - } - } - } - - // If there is one more command to come, shift the target states one time step back. - if (i < iteratorList.size() - 1) { - for (auto const& stateProbabilityPair : *currentTargetStates) { - delete stateProbabilityPair.first; - } - delete currentTargetStates; - currentTargetStates = newTargetStates; - newTargetStates = new std::unordered_map(); - } - } - - // At this point, we applied all commands of the current command combination and newTargetStates - // contains all target states and their respective probabilities. That means we are now ready to - // add the choice to the list of transitions. - transitionList.emplace_back(std::make_pair(std::make_pair(action, std::list()), std::map())); - - // Add the commands that were involved in creating this distribution to the labeling. - for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { - transitionList.back().first.second.push_back(iteratorList[i]->getGlobalIndex()); - } - - // Now create the actual distribution. - std::map& states = transitionList.back().second; - for (auto const& stateProbabilityPair : *newTargetStates) { - uint_fast64_t newStateIndex = this->getOrAddStateIndex(stateProbabilityPair.first); - states[newStateIndex] = stateProbabilityPair.second; - } - this->numberOfTransitions += states.size(); - - // Dispose of the temporary maps. - delete currentTargetStates; - delete newTargetStates; - - // Now, check whether there is one more command combination to consider. - bool movedIterator = false; - for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) { - ++iteratorList[j]; - if (iteratorList[j] != activeCommandList[j].end()) { - movedIterator = true; - } else { - // Reset the iterator to the beginning of the list. - iteratorList[j] = activeCommandList[j].begin(); - } - } - - done = !movedIterator; - } - } - } - } +// 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(); +// } +// } +// } +// } - 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; - } +// void ExplicitModelAdapter::addLabeledTransitions(uint_fast64_t stateIndex, std::list>, std::map>>& transitionList) { +// for (std::string const& action : this->program.getActions()) { +// StateType* currentState = this->allStates[stateIndex]; +// boost::optional>> optionalActiveCommandLists = this->getActiveCommandsByAction(currentState, action); +// +// // Only process this action label, if there is at least one feasible solution. +// if (optionalActiveCommandLists) { +// std::vector> const& activeCommandList = optionalActiveCommandLists.get(); +// std::vector::const_iterator> iteratorList(activeCommandList.size()); +// +// // Initialize the list of iterators. +// for (size_t i = 0; i < activeCommandList.size(); ++i) { +// iteratorList[i] = activeCommandList[i].cbegin(); +// } +// +// // As long as there is one feasible combination of commands, keep on expanding it. +// bool done = false; +// while (!done) { +// std::unordered_map* currentTargetStates = new std::unordered_map(); +// std::unordered_map* newTargetStates = new std::unordered_map(); +// (*currentTargetStates)[new StateType(*currentState)] = 1.0; +// +// // FIXME: This does not check whether a global variable is written multiple times. While the +// // behaviour for this is undefined anyway, a warning should be issued in that case. +// double probabilitySum = 0; +// for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { +// storm::ir::Command const& command = *iteratorList[i]; +// +// for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { +// storm::ir::Update const& update = command.getUpdate(j); +// +// for (auto const& stateProbabilityPair : *currentTargetStates) { +// StateType* newTargetState = this->applyUpdate(stateProbabilityPair.first, currentState, update); +// probabilitySum += stateProbabilityPair.second * update.getLikelihoodExpression()->getValueAsDouble(currentState); +// +// auto existingStateProbabilityPair = newTargetStates->find(newTargetState); +// if (existingStateProbabilityPair == newTargetStates->end()) { +// (*newTargetStates)[newTargetState] = stateProbabilityPair.second * update.getLikelihoodExpression()->getValueAsDouble(currentState); +// } else { +// existingStateProbabilityPair->second += stateProbabilityPair.second * update.getLikelihoodExpression()->getValueAsDouble(currentState); +// } +// } +// } +// +// // If there is one more command to come, shift the target states one time step back. +// if (i < iteratorList.size() - 1) { +// for (auto const& stateProbabilityPair : *currentTargetStates) { +// delete stateProbabilityPair.first; +// } +// delete currentTargetStates; +// currentTargetStates = newTargetStates; +// newTargetStates = new std::unordered_map(); +// } +// } +// +// // At this point, we applied all commands of the current command combination and newTargetStates +// // contains all target states and their respective probabilities. That means we are now ready to +// // add the choice to the list of transitions. +// transitionList.emplace_back(std::make_pair(std::make_pair(action, std::list()), std::map())); +// +// // Add the commands that were involved in creating this distribution to the labeling. +// for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { +// transitionList.back().first.second.push_back(iteratorList[i]->getGlobalIndex()); +// } +// +// // Now create the actual distribution. +// std::map& states = transitionList.back().second; +// for (auto const& stateProbabilityPair : *newTargetStates) { +// uint_fast64_t newStateIndex = this->getOrAddStateIndex(stateProbabilityPair.first); +// states[newStateIndex] = stateProbabilityPair.second; +// } +// this->numberOfTransitions += states.size(); +// +// // Dispose of the temporary maps. +// delete currentTargetStates; +// delete newTargetStates; +// +// // Now, check whether there is one more command combination to consider. +// bool movedIterator = false; +// for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) { +// ++iteratorList[j]; +// if (iteratorList[j] != activeCommandList[j].end()) { +// movedIterator = true; +// } else { +// // Reset the iterator to the beginning of the list. +// iteratorList[j] = activeCommandList[j].begin(); +// } +// } +// +// done = !movedIterator; +// } +// } +// } +// } - storm::storage::SparseMatrix ExplicitModelAdapter::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; - } +// 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; +// } - 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."); - } +// 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::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(); - } +// void ExplicitModelAdapter::buildTransitionMap() { +// LOG4CPLUS_DEBUG(logger, "Creating transition map from program."); +// this->clearInternalState(); +// this->allStates.clear(); +// this->allStates.push_back(this->getInitialState()); +// stateToIndexMap[this->allStates[0]] = 0; +// +// for (uint_fast64_t state = 0; state < this->allStates.size(); ++state) { +// this->addUnlabeledTransitions(state, this->transitionMap[state]); +// this->addLabeledTransitions(state, this->transitionMap[state]); +// +// this->numberOfChoices += this->transitionMap[state].size(); +// +// // Check whether the current state is a deadlock state and treat it accordingly. +// if (this->transitionMap[state].size() == 0) { +// if (storm::settings::Settings::getInstance()->isSet("fixDeadlocks")) { +// ++this->numberOfTransitions; +// ++this->numberOfChoices; +// this->transitionMap[state].emplace_back(); +// this->transitionMap[state].back().second[state] = 1; +// } else { +// LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."); +// throw storm::exceptions::WrongFormatException() << "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option."; +// } +// } +// } +// +// LOG4CPLUS_DEBUG(logger, "Finished creating transition map."); +// } } // namespace adapters } // namespace storm diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 31072c314..c5bf02ed3 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -59,22 +59,31 @@ namespace storm { 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(); + // A structure holding information about the reachable state space. + struct StateInformation { + std::vector reachableStates; + std::unordered_map stateToIndexMap; + }; + + // A structure holding the individual components of a model. + struct ModelComponents { + ModelComponents() : transitionMatrix(), stateLabeling(), nondeterministicChoiceIndices(), stateRewards(), transitionRewardMatrix(), choiceLabeling() { + // Intentionally left empty. + } + + storm::storage::SparseMatrix transitionMatrix; + storm::models::AtomicPropositionsLabeling stateLabeling; + std::vector nondeterministicChoiceIndices; + std::vector stateRewards; + storm::storage::SparseMatrix transitionRewardMatrix; + std::vector> choiceLabeling; + }; /*! * 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 program The program to translate. * @param constantDefinitionString A string that contains a comma-separated definition of all undefined * constants in the model. * @param rewardModelName The name of reward model to be added to the model. This must be either a reward @@ -82,27 +91,9 @@ namespace storm { * rewards. * @return The explicit model that was given by the probabilistic program. */ - std::shared_ptr> getModel(std::string const& constantDefinitionString = "", std::string const& rewardModelName = ""); + static std::shared_ptr> translateProgram(storm::ir::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = ""); private: - /*! - * Private copy constructor to disable copy-construction (and move-construction) of this class. - * - * @param other The object to copy-construct from. - */ - ExplicitModelAdapter(ExplicitModelAdapter const& other); - /*! - * Private copy-assignment to disable copy-assignment (and move-assignment) of this class. - * - * @param other The object to copy-assign from. - */ - ExplicitModelAdapter operator=(ExplicitModelAdapter const& other); - - /*! - * The precision that is to be used for sanity checks internally. - */ - double precision; - /*! * Sets some boolean variable in the given state object. * @@ -133,29 +124,50 @@ namespace storm { * Applies an update to the given state and returns the resulting new state object. This methods does not * modify the given state but returns a new one. * + * @param program The program in which the variables of the update are declared. * @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; + static StateType* applyUpdate(storm::ir::Program const& program, StateType const* state, storm::ir::Update const& update); /*! * Applies an update to the given state and returns the resulting new state object. The update is evaluated * over the variable values of the given base state. This methods does not modify the given state but * returns a new one. * - * @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. + * @param program The program in which the variables of the update are declared. + * @param state The state to which to apply the update. + * @param baseState The state used for evaluating the update. + * @param update The update to apply. * @return The resulting state. */ - StateType* applyUpdate(StateType const* state, StateType const* baseState, storm::ir::Update const& update) const; + static StateType* applyUpdate(storm::ir::Program const& program, StateType const* state, StateType const* baseState, storm::ir::Update const& update); /*! - * Prepares internal data structures associated with the variables in the program that are used during the - * translation. + * Defines the undefined constants of the given program using the given string. + * + * @param program The program in which to define the constants. + * @param constantDefinitionString A comma-separated list of constant definitions. */ - void initializeVariables(); + static void defineUndefinedConstants(storm::ir::Program& program, std::string const& constantDefinitionString); + + /*! + * Undefines all previously defined constants in the given program. + * + * @param program The program in which to undefine the constants. + */ + static void undefineUndefinedConstants(storm::ir::Program& program); + + /*! + * Explores the state space of the given program and returns the components of the model as a result. + * + * @param program The program whose state space to explore. + * @param rewardModelName The name of the reward model that is to be considered. If empty, no reward model + * is considered. + * @return A structure containing the components of the resulting model. + */ + static ModelComponents buildModelComponents(storm::ir::Program const& program, std::string const& rewardModelName); /*! * Retrieves the state rewards for every reachable state based on the given state rewards. @@ -163,7 +175,7 @@ namespace storm { * @param rewards The rewards to use. * @return The reward values for every (reachable) state. */ - std::vector getStateRewards(std::vector const& rewards); +// static std::vector getStateRewards(std::vector const& rewards); /*! * Computes the labels for every reachable state based on a list of available labels. @@ -171,7 +183,7 @@ namespace storm { * @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); +// static 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 @@ -188,14 +200,14 @@ namespace storm { * @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); +// static boost::optional>> getActiveCommandsByAction(StateType const* state, std::string const& action); /*! * Generates the initial state. * * @return The initial state. */ - StateType* getInitialState(); +// static StateType* getInitialState(); /*! * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to @@ -206,7 +218,7 @@ namespace storm { * @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); +// static uint_fast64_t getOrAddStateIndex(StateType* state); /*! * Expands all unlabeled (i.e. independent) transitions of the given state and adds them to the transition list. @@ -214,7 +226,7 @@ namespace storm { * @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); +// static 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. @@ -222,46 +234,26 @@ namespace storm { * @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); +// static 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(); +// static 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(); +// static 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(); - - /*! - * Defines the undefined constants of the program using the given string. - * - * @param constantDefinitionString A comma-separated list of constant definitions. - */ - void defineUndefinedConstants(std::string const& constantDefinitionString); - - /*! - * Sets all values of program constants to undefined again. - */ - void undefineUndefinedConstants(); - - // Program that is to be converted. - storm::ir::Program program; +// void buildTransitionMap(); // List of all boolean variables. std::vector booleanVariables; diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp index d997e8cbd..782d9cb7a 100644 --- a/src/ir/Program.cpp +++ b/src/ir/Program.cpp @@ -215,5 +215,13 @@ namespace storm { return this->doubleUndefinedConstantExpressions; } + uint_fast64_t Program::getGlobalIndexOfBooleanVariable(std::string const& variableName) const { + return this->globalBooleanVariableToIndexMap.at(variableName); + } + + uint_fast64_t Program::getGlobalIndexOfIntegerVariable(std::string const& variableName) const { + return this->globalIntegerVariableToIndexMap.at(variableName); + } + } // namespace ir } // namepsace storm diff --git a/src/ir/Program.h b/src/ir/Program.h index 6e31feaa6..6789edaae 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -233,6 +233,20 @@ namespace storm { */ std::map> const& getDoubleUndefinedConstantExpressionsMap() const; + /*! + * Retrieves the global index of the given boolean variable. + * + * @param variableName The name of the boolean variable whose index to retrieve. + */ + uint_fast64_t getGlobalIndexOfBooleanVariable(std::string const& variableName) const; + + /*! + * Retrieves the global index of the integer boolean variable. + * + * @param variableName The name of the integer variable whose index to retrieve. + */ + uint_fast64_t getGlobalIndexOfIntegerVariable(std::string const& variableName) const; + private: // The type of the model. ModelType modelType; diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h index c8670566c..fa34a1cf3 100644 --- a/src/models/AbstractModel.h +++ b/src/models/AbstractModel.h @@ -300,6 +300,15 @@ class AbstractModel: public std::enable_shared_from_this> { return this->getTransitionMatrix().getNonZeroEntryCount(); } + /*! + * Retrieves the initial states of the model. + * + * @return The initial states of the model represented by a bit vector. + */ + storm::storage::BitVector const& getInitialStates() const { + return this->getLabeledStates("init"); + } + /*! * Returns a bit vector in which exactly those bits are set to true that * correspond to a state labeled with the given atomic proposition. diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index e566dfe7d..d1ccb492d 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -32,15 +32,14 @@ namespace models { */ class AtomicPropositionsLabeling { -public: - +public: /*! * Constructs an empty atomic propositions labeling for the given number of states and amount of atomic propositions. * * @param stateCount The number of states of the model. * @param apCountMax The number of atomic propositions. */ - AtomicPropositionsLabeling(const uint_fast64_t stateCount, uint_fast64_t const apCountMax) + AtomicPropositionsLabeling(const uint_fast64_t stateCount = 0, uint_fast64_t const apCountMax = 0) : stateCount(stateCount), apCountMax(apCountMax), apsCurrent(0), singleLabelings() { singleLabelings.reserve(apCountMax); } diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 25935c1fd..728ac1265 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -351,7 +351,7 @@ public: * * @param other The Matrix from which to copy the content */ - storm::storage::SparseMatrix& operator=(const SparseMatrix & other) { + storm::storage::SparseMatrix& operator=(SparseMatrix const& other) { this->rowCount = other.rowCount; this->colCount = other.colCount; this->nonZeroEntryCount = other.nonZeroEntryCount; diff --git a/src/storm.cpp b/src/storm.cpp index da0bde007..5489e3d13 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -330,10 +330,9 @@ int main(const int argc, const char* argv[]) { delete modelchecker; } } else if (s->isSet("symbolic")) { - std::string const arg = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString(); - storm::adapters::ExplicitModelAdapter adapter(storm::parser::PrismParserFromFile(arg)); - std::string const constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString(); - std::shared_ptr> model = adapter.getModel(constants); + std::string const& programFile = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString(); + std::string const& constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString(); + std::shared_ptr> model = storm::adapters::ExplicitModelAdapter::translateProgram(storm::parser::PrismParserFromFile(programFile), constants); model->printModelInformationToStream(std::cout); // Enable the following lines to test the MinimalLabelSetGenerator.