diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0a5832d87..7587a3f22 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -11,8 +11,7 @@ file(GLOB_RECURSE STORM_SOURCES_CLI ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_MAIN_FILE ${PROJECT_SOURCE_DIR}/src/storm.cpp) file(GLOB_RECURSE STORM_ADAPTERS_FILES ${PROJECT_SOURCE_DIR}/src/adapters/*.h ${PROJECT_SOURCE_DIR}/src/adapters/*.cpp) file(GLOB_RECURSE STORM_BUILDER_FILES ${PROJECT_SOURCE_DIR}/src/builder/*.h ${PROJECT_SOURCE_DIR}/src/builder/*.cpp) -file(GLOB STORM_GENERATOR_FILES ${PROJECT_SOURCE_DIR}/src/generator/*.h ${PROJECT_SOURCE_DIR}/src/generator/*.cpp) -file(GLOB_RECURSE STORM_GENERATOR_PRISM_FILES ${PROJECT_SOURCE_DIR}/src/generator/prism/*.h ${PROJECT_SOURCE_DIR}/src/generator/prism/*.cpp) +file(GLOB_RECURSE STORM_GENERATOR_FILES ${PROJECT_SOURCE_DIR}/src/generator/*.h ${PROJECT_SOURCE_DIR}/src/generator/*.cpp) file(GLOB_RECURSE STORM_CLI_FILES ${PROJECT_SOURCE_DIR}/src/cli/*.h ${PROJECT_SOURCE_DIR}/src/cli/*.cpp) file(GLOB_RECURSE STORM_EXCEPTIONS_FILES ${PROJECT_SOURCE_DIR}/src/exceptions/*.h ${PROJECT_SOURCE_DIR}/src/exceptions/*.cpp) file(GLOB_RECURSE STORM_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/logic/*.h ${PROJECT_SOURCE_DIR}/src/logic/*.cpp) @@ -60,7 +59,6 @@ source_group(main FILES ${STORM_MAIN_FILE}) source_group(adapters FILES ${STORM_ADAPTERS_FILES}) source_group(builder FILES ${STORM_BUILDER_FILES}) source_group(generator FILES ${STORM_GENERATOR_FILES}) -source_group(generator\\prism FILES ${STORM_GENERATOR_PRISM_FILES}) source_group(cli FILES ${STORM_CLI_FILES}) source_group(exceptions FILES ${STORM_EXCEPTIONS_FILES}) source_group(logic FILES ${STORM_LOGIC_FILES}) diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 19b115c6e..039048111 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -66,33 +66,33 @@ namespace storm { storm::storage::SparseMatrixBuilder transitionRewardMatrixBuilder; }; - template - ExplicitPrismModelBuilder::StateInformation::StateInformation(uint_fast64_t numberOfStates) : valuations(numberOfStates) { + template + ExplicitPrismModelBuilder::StateInformation::StateInformation(uint_fast64_t numberOfStates) : valuations(numberOfStates) { // Intentionally left empty. } - template - ExplicitPrismModelBuilder::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), reachableStates() { + template + ExplicitPrismModelBuilder::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), bitsPerState(bitsPerState), numberOfStates() { // Intentionally left empty. } - template - ExplicitPrismModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { + template + ExplicitPrismModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { // Intentionally left empty. } - template - ExplicitPrismModelBuilder::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { + template + ExplicitPrismModelBuilder::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { // Intentionally left empty. } - template - ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates(), negatedTerminalStates() { + template + ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates(), negatedTerminalStates() { this->preserveFormula(formula); } - template - ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { + template + ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; this->buildAllLabels = true; @@ -106,8 +106,8 @@ namespace storm { } } - template - void ExplicitPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { + template + void ExplicitPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { if (formula.isAtomicExpressionFormula()) { terminalStates = formula.asAtomicExpressionFormula().getExpression(); } else if (formula.isAtomicLabelFormula()) { @@ -136,8 +136,8 @@ namespace storm { } } - template - void ExplicitPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { + template + void ExplicitPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { // If we already had terminal states, we need to erase them. if (terminalStates) { terminalStates.reset(); @@ -174,105 +174,108 @@ namespace storm { } } - template - void ExplicitPrismModelBuilder::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) { + template + void ExplicitPrismModelBuilder::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) { constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); } - template - typename ExplicitPrismModelBuilder::StateInformation const& ExplicitPrismModelBuilder::getStateInformation() const { - STORM_LOG_THROW(static_cast(stateInformation), storm::exceptions::InvalidOperationException, "The state information was not properly build."); - return stateInformation.get(); - } - - template - storm::prism::Program const& ExplicitPrismModelBuilder::getTranslatedProgram() const { - return preparedProgram.get(); - } - - template - std::shared_ptr> ExplicitPrismModelBuilder::translateProgram(storm::prism::Program program, Options const& options) { + template + ExplicitPrismModelBuilder::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : options(options), program(program) { // Start by defining the undefined constants in the model. if (options.constantDefinitions) { - preparedProgram = program.defineUndefinedConstants(options.constantDefinitions.get()); + this->program = program.defineUndefinedConstants(options.constantDefinitions.get()); } else { - preparedProgram = program; + this->program = program; } - + // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message. #ifdef STORM_HAVE_CARL // If the program either has undefined constants or we are building a parametric model, but the parameters // not only appear in the probabilities, we re - if (!std::is_same::value && preparedProgram->hasUndefinedConstants()) { + if (!std::is_same::value && this->program.hasUndefinedConstants()) { #else - if (preparedProgram->hasUndefinedConstants()) { + if (this->program->hasUndefinedConstants()) { #endif - std::vector> undefinedConstants = preparedProgram->getUndefinedConstants(); - std::stringstream stream; - bool printComma = false; - for (auto const& constant : undefinedConstants) { - if (printComma) { - stream << ", "; - } else { - printComma = true; + std::vector> undefinedConstants = this->program.getUndefinedConstants(); + std::stringstream stream; + bool printComma = false; + for (auto const& constant : undefinedConstants) { + if (printComma) { + stream << ", "; + } else { + printComma = true; + } + stream << constant.get().getName() << " (" << constant.get().getType() << ")"; } - stream << constant.get().getName() << " (" << constant.get().getType() << ")"; - } - stream << "."; - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); + stream << "."; + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str()); #ifdef STORM_HAVE_CARL - } else if (std::is_same::value && !preparedProgram->hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) { - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted."); + } else if (std::is_same::value && !this->program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted."); #endif - } - - // If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program. - if (options.labelsToBuild) { - if (!options.buildAllLabels) { - preparedProgram->filterLabels(options.labelsToBuild.get()); } - } - - // If we need to build labels for expressions that may appear in some formula, we need to add appropriate - // labels to the program. - if (options.expressionLabels) { - std::map constantsSubstitution = preparedProgram->getConstantsSubstitution(); - - for (auto const& expression : options.expressionLabels.get()) { - std::stringstream stream; - stream << expression.substitute(constantsSubstitution); - std::string name = stream.str(); - if (!preparedProgram->hasLabel(name)) { - preparedProgram->addLabel(name, expression); + + // If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program. + if (options.labelsToBuild) { + if (!options.buildAllLabels) { + this->program.filterLabels(options.labelsToBuild.get()); + } + } + + // If we need to build labels for expressions that may appear in some formula, we need to add appropriate + // labels to the program. + if (options.expressionLabels) { + std::map constantsSubstitution = this->program.getConstantsSubstitution(); + + for (auto const& expression : options.expressionLabels.get()) { + std::stringstream stream; + stream << expression.substitute(constantsSubstitution); + std::string name = stream.str(); + if (!this->program.hasLabel(name)) { + this->program.addLabel(name, expression); + } } } - } - - // Now that the program is fixed, we we need to substitute all constants with their concrete value. - preparedProgram = preparedProgram->substituteConstants(); - - STORM_LOG_DEBUG("Building representation of program:" << std::endl << *preparedProgram << std::endl); + + // Now that the program is fixed, we we need to substitute all constants with their concrete value. + this->program = program.substituteConstants(); + } + + template + typename ExplicitPrismModelBuilder::StateInformation const& ExplicitPrismModelBuilder::getStateInformation() const { + STORM_LOG_THROW(static_cast(stateInformation), storm::exceptions::InvalidOperationException, "The state information was not properly build."); + return stateInformation.get(); + } + + template + storm::prism::Program const& ExplicitPrismModelBuilder::getTranslatedProgram() const { + return program; + } + + template + std::shared_ptr> ExplicitPrismModelBuilder::translate() { + STORM_LOG_DEBUG("Building representation of program:" << std::endl << *program << std::endl); // Select the appropriate reward models (after the constants have been substituted). std::vector> selectedRewardModels; // First, we make sure that all selected reward models actually exist. for (auto const& rewardModelName : options.rewardModelsToBuild) { - STORM_LOG_THROW(rewardModelName.empty() || preparedProgram->hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'."); + STORM_LOG_THROW(rewardModelName.empty() || program.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'."); } - for (auto const& rewardModel : preparedProgram->getRewardModels()) { + for (auto const& rewardModel : program.getRewardModels()) { if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) { selectedRewardModels.push_back(rewardModel); } } // If no reward model was selected until now and a referenced reward model appears to be unique, we build // the only existing reward model (given that no explicit name was given for the referenced reward model). - if (selectedRewardModels.empty() && preparedProgram->getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") { - selectedRewardModels.push_back(preparedProgram->getRewardModel(0)); + if (selectedRewardModels.empty() && program.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") { + selectedRewardModels.push_back(program.getRewardModel(0)); } - ModelComponents modelComponents = buildModelComponents(*preparedProgram, selectedRewardModels, options); + ModelComponents modelComponents = buildModelComponents(*program, selectedRewardModels, options); std::shared_ptr> result; switch (program.getModelType()) { @@ -292,19 +295,9 @@ namespace storm { return result; } - - template - void ExplicitPrismModelBuilder::unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator) { - for (auto const& booleanVariable : variableInformation.booleanVariables) { - evaluator.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset)); - } - for (auto const& integerVariable : variableInformation.integerVariables) { - evaluator.setIntegerValue(integerVariable.variable, currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound); - } - } - - template - storm::expressions::SimpleValuation ExplicitPrismModelBuilder::unpackStateIntoValuation(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation) { + + template + storm::expressions::SimpleValuation ExplicitPrismModelBuilder::unpackStateIntoValuation(storm::storage::BitVector const& currentState) { storm::expressions::SimpleValuation result(variableInformation.manager.getSharedPointer()); for (auto const& booleanVariable : variableInformation.booleanVariables) { result.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset)); @@ -315,254 +308,26 @@ namespace storm { return result; } - template - typename ExplicitPrismModelBuilder::CompressedState ExplicitPrismModelBuilder::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator const& evaluator) { - return applyUpdate(variableInformation, state, state, update, evaluator); - } - - template - typename ExplicitPrismModelBuilder::CompressedState ExplicitPrismModelBuilder::applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator const& evaluator) { - CompressedState newState(state); - - auto assignmentIt = update.getAssignments().begin(); - auto assignmentIte = update.getAssignments().end(); - - // Iterate over all boolean assignments and carry them out. - auto boolIt = variableInformation.booleanVariables.begin(); - for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) { - while (assignmentIt->getVariable() != boolIt->variable) { - ++boolIt; - } - newState.set(boolIt->bitOffset, evaluator.asBool(assignmentIt->getExpression())); - } - - // Iterate over all integer assignments and carry them out. - auto integerIt = variableInformation.integerVariables.begin(); - for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) { - while (assignmentIt->getVariable() != integerIt->variable) { - ++integerIt; - } - int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression()); - STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); - newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); - STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); - } - - // Check that we processed all assignments. - STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed."); - - return newState; - } - - template - IndexType ExplicitPrismModelBuilder::getOrAddStateIndex(CompressedState const& state, InternalStateInformation& internalStateInformation, std::queue& stateQueue) { + template + StateType ExplicitPrismModelBuilder::getOrAddStateIndex(CompressedState const& state) { uint32_t newIndex = internalStateInformation.reachableStates.size(); // Check, if the state was already registered. std::pair actualIndexBucketPair = internalStateInformation.stateStorage.findOrAddAndGetBucket(state, newIndex); if (actualIndexBucketPair.first == newIndex) { - stateQueue.push(state); - internalStateInformation.reachableStates.push_back(state); + statesToExplore.push(state); + ++internalStateInformation.numberOfStates; } return actualIndexBucketPair.first; } - - template - boost::optional>>> ExplicitPrismModelBuilder::getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator const& evaluator, uint_fast64_t const& actionIndex) { - boost::optional>>> result((std::vector>>())); - - // Iterate over all modules. - for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { - storm::prism::Module const& module = program.getModule(i); - - // If the module has no command labeled with the given action, we can skip this module. - if (!module.hasActionIndex(actionIndex)) { - continue; - } - - std::set const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex); - - // If the module contains the action, but there is no command in the module that is labeled with - // this action, we don't have any feasible command combinations. - if (commandIndices.empty()) { - return boost::optional>>>(); - } - - std::vector> 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::prism::Command const& command = module.getCommand(commandIndex); - if (evaluator.asBool(command.getGuardExpression())) { - 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; - } - - template - std::vector> ExplicitPrismModelBuilder::getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator) { - std::vector> result; - - // Iterate over all modules. - for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { - storm::prism::Module const& module = program.getModule(i); - - // Iterate over all commands. - for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) { - storm::prism::Command const& command = module.getCommand(j); - - // Only consider unlabeled commands. - if (command.isLabeled()) continue; - - // Skip the command, if it is not enabled. - if (!evaluator.asBool(command.getGuardExpression())) { - continue; - } - - result.push_back(Choice(0, choiceLabeling)); - Choice& choice = result.back(); - - // Remember the command labels only if we were asked to. - if (choiceLabeling) { - choice.addChoiceLabel(command.getGlobalIndex()); - } - - // Iterate over all updates of the current command. - ValueType probabilitySum = storm::utility::zero(); - for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { - storm::prism::Update const& update = command.getUpdate(k); - - // Obtain target state index and add it to the list of known states. If it has not yet been - // seen, we also add it to the set of states that have yet to be explored. - uint32_t stateIndex = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update, evaluator), internalStateInformation, stateQueue); - - // Update the choice by adding the probability/target state to it. - ValueType probability = evaluator.asRational(update.getLikelihoodExpression()); - choice.addProbability(stateIndex, probability); - probabilitySum += probability; - } - - // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!discreteTimeModel || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); - } - } - - return result; - } - - template - std::vector> ExplicitPrismModelBuilder::getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator) { - std::vector> result; - - for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) { - boost::optional>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, evaluator, actionIndex); - - // 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->emplace(currentState, storm::utility::one()); - - for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { - storm::prism::Command const& command = *iteratorList[i]; - - for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { - storm::prism::Update const& update = command.getUpdate(j); - - for (auto const& stateProbabilityPair : *currentTargetStates) { - // Compute the new state under the current update and add it to the set of new target states. - CompressedState newTargetState = applyUpdate(variableInformation, stateProbabilityPair.first, currentState, update, evaluator); - newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression())); - } - } - - // If there is one more command to come, shift the target states one time step back. - if (i < iteratorList.size() - 1) { - delete currentTargetStates; - currentTargetStates = newTargetStates; - newTargetStates = new std::unordered_map(); - } - } - - // At this point, we applied all commands of the current command combination and newTargetStates - // contains all target states and their respective probabilities. That means we are now ready to - // add the choice to the list of transitions. - result.push_back(Choice(actionIndex, choiceLabeling)); - - // Now create the actual distribution. - Choice& choice = result.back(); - - // Remember the command labels only if we were asked to. - if (choiceLabeling) { - // Add the labels of all commands to this choice. - for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { - choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex()); - } - } - - ValueType probabilitySum = storm::utility::zero(); - for (auto const& stateProbabilityPair : *newTargetStates) { - uint32_t actualIndex = getOrAddStateIndex(stateProbabilityPair.first, internalStateInformation, stateQueue); - choice.addProbability(actualIndex, stateProbabilityPair.second); - probabilitySum += stateProbabilityPair.second; - } - - // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!discreteTimeModel || !comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); - - // Dispose of the temporary maps. - delete currentTargetStates; - delete newTargetStates; - - // Now, check whether there is one more command combination to consider. - bool movedIterator = false; - for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) { - ++iteratorList[j]; - if (iteratorList[j] != activeCommandList[j].end()) { - movedIterator = true; - } else { - // Reset the iterator to the beginning of the list. - iteratorList[j] = activeCommandList[j].begin(); - } - } - - done = !movedIterator; - } - } - } - - return result; - } - template - boost::optional>> ExplicitPrismModelBuilder::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, InternalStateInformation& internalStateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression) { + template + boost::optional>> ExplicitPrismModelBuilder::buildMatrices(std::vector> const& selectedRewardModels, InternalStateInformation& internalStateInformation, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression) { // Create choice labels, if requested, boost::optional>> choiceLabels; - if (commandLabels) { + if (options.buildCommandLabels) { choiceLabels = std::vector>(); } @@ -606,7 +371,7 @@ namespace storm { // Get the current state and unpack it. storm::storage::BitVector currentState = stateQueue.front(); stateQueue.pop(); - IndexType stateIndex = internalStateInformation.stateStorage.getValue(currentState); + StateType stateIndex = internalStateInformation.stateStorage.getValue(currentState); STORM_LOG_TRACE("Exploring state with id " << stateIndex << "."); unpackStateIntoEvaluator(currentState, variableInformation, evaluator); @@ -615,11 +380,7 @@ namespace storm { std::vector> allLabeledChoices; bool deadlockOnPurpose = false; if (terminalExpression && evaluator.asBool(terminalExpression.get())) { - //std::cout << unpackStateIntoValuation(currentState, variableInformation).toString(true) << std::endl; - //allUnlabeledChoices = getUnlabeledTransitions(program, discreteTimeModel, internalStateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator); - //allLabeledChoices = getLabeledTransitions(program, discreteTimeModel, internalStateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator); - - // Nothing to do in this case. + // Nothing to do in this case. deadlockOnPurpose = true; } else { // Retrieve all choices for the current state. @@ -886,8 +647,8 @@ namespace storm { return choiceLabels; } - template - typename ExplicitPrismModelBuilder::ModelComponents ExplicitPrismModelBuilder::buildModelComponents(storm::prism::Program const& program, std::vector> const& selectedRewardModels, Options const& options) { + template + typename ExplicitPrismModelBuilder::ModelComponents ExplicitPrismModelBuilder::buildModelComponents(storm::prism::Program const& program, std::vector> const& selectedRewardModels, Options const& options) { ModelComponents modelComponents; uint_fast64_t bitOffset = 0; @@ -991,8 +752,8 @@ namespace storm { return modelComponents; } - template - storm::models::sparse::StateLabeling ExplicitPrismModelBuilder::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, InternalStateInformation const& internalStateInformation) { + template + storm::models::sparse::StateLabeling ExplicitPrismModelBuilder::buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, InternalStateInformation const& internalStateInformation) { storm::expressions::ExpressionEvaluator evaluator(program.getManager()); std::vector const& labels = program.getLabels(); diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index 9bd62ad2b..5e4f5b2c5 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -22,9 +22,11 @@ #include "src/storage/SparseMatrix.h" #include "src/settings/SettingsManager.h" -#include "src/utility/constants.h" + #include "src/utility/prism.h" +#include "src/generator/VariableInformation.h" + namespace storm { namespace utility { template class ConstantsComparator; @@ -37,7 +39,7 @@ namespace storm { // Forward-declare classes. template struct RewardModelBuilder; - template, typename IndexType = uint32_t> + template, typename StateType = uint32_t> class ExplicitPrismModelBuilder { public: typedef storm::storage::BitVector CompressedState; @@ -47,16 +49,16 @@ namespace storm { InternalStateInformation(uint64_t bitsPerState); // This member stores all the states and maps them to their unique indices. - storm::storage::BitVectorHashMap stateStorage; + storm::storage::BitVectorHashMap stateStorage; // A list of initial states in terms of their global indices. - std::vector initialStateIndices; + std::vector initialStateIndices; // The number of bits of each state. uint64_t bitsPerState; - // A list of reachable states as indices in the stateToIndexMap. - std::vector reachableStates; + // The number of states that were found in the exploration so far. + uint_fast64_t numberOfStates; }; // A structure holding information about the reachable state space that can be retrieved from the outside. @@ -174,6 +176,13 @@ namespace storm { boost::optional> negatedTerminalStates; }; + /*! + * Creates a builder for the given program. + * + * @param program The program to build. + */ + ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options = Options()); + /*! * 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. @@ -184,7 +193,7 @@ namespace storm { * @param rewardModel The reward model that is to be built. * @return The explicit model that was given by the probabilistic program. */ - std::shared_ptr> translateProgram(storm::prism::Program program, Options const& options = Options()); + std::shared_ptr> translate(); /*! * If requested in the options, information about the variable valuations in the reachable states can be @@ -195,39 +204,14 @@ namespace storm { StateInformation const& getStateInformation() const; /*! - * Retrieves the program that was actually translated (i.e. including constant substitutions etc.). Note - * that this function may only be called after a succesful translation. + * Retrieves the program that was actually translated (i.e. including constant substitutions etc.). * * @return The translated program. */ storm::prism::Program const& getTranslatedProgram() const; private: - static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator& evaluator); - - static storm::expressions::SimpleValuation unpackStateIntoValuation(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation); - - /*! - * 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. - */ - static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator const& evaluator); - - /*! - * Applies an update to the given state and returns the resulting new state object. The update is evaluated - * over the variable values of the given base state. This methods does not modify the given state but - * returns a new one. - * - * @param state The state to which to apply the update. - * @param baseState The state used for evaluating the update. - * @param update The update to apply. - * @return The resulting state. - */ - static CompressedState applyUpdate(VariableInformation const& variableInformation, CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update, storm::expressions::ExpressionEvaluator const& evaluator); + storm::expressions::SimpleValuation unpackStateIntoValuation(storm::storage::BitVector const& currentState); /*! * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to @@ -239,29 +223,8 @@ namespace storm { * @param internalStateInformation The information about the already explored part of the reachable state space. * @return A pair indicating whether the state was already discovered before and the state id of the state. */ - static IndexType getOrAddStateIndex(CompressedState const& state, InternalStateInformation& internalStateInformation, std::queue& stateQueue); + StateType getOrAddStateIndex(CompressedState const& state); - /*! - * 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 The program in which to search for active commands. - * @param state The current state. - * @param actionIndex The index of the action label to select. - * @return A list of lists of active commands or nothing. - */ - static boost::optional>>> getActiveCommandsByActionIndex(storm::prism::Program const& program,storm::expressions::ExpressionEvaluator const& evaluator, uint_fast64_t const& actionIndex); - - static std::vector> getUnlabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator); - - static std::vector> getLabeledTransitions(storm::prism::Program const& program, bool discreteTimeModel, InternalStateInformation& internalStateInformation, VariableInformation const& variableInformation, storm::storage::BitVector const& currentState, bool choiceLabeling, storm::expressions::ExpressionEvaluator const& evaluator, std::queue& stateQueue, storm::utility::ConstantsComparator const& comparator); /*! * Builds the transition matrix and the transition reward matrix based for the given program. * @@ -279,7 +242,7 @@ namespace storm { * @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin * and a vector containing the labels associated with each choice. */ - static boost::optional>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector> const& selectedRewardModels, InternalStateInformation& internalStateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression); + boost::optional>> buildMatrices(std::vector> const& selectedRewardModels, InternalStateInformation& internalStateInformation, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression); /*! * Explores the state space of the given program and returns the components of the model as a result. @@ -289,7 +252,7 @@ namespace storm { * @param options A set of options used to customize the building process. * @return A structure containing the components of the resulting model. */ - ModelComponents buildModelComponents(storm::prism::Program const& program, std::vector> const& selectedRewardModels, Options const& options); + ModelComponents buildModelComponents(std::vector> const& selectedRewardModels); /*! * Builds the state labeling for the given program. @@ -299,14 +262,27 @@ namespace storm { * @param internalStateInformation Information about the state space of the program. * @return The state labeling of the given program. */ - static storm::models::sparse::StateLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, InternalStateInformation const& internalStateInformation); + storm::models::sparse::StateLabeling buildStateLabeling(); + + // The program to translate. The necessary transformations are performed upon construction of the builder. + storm::prism::Program program; + + // The options to be used for translating the program. + Options options; + + // The variable information. + storm::generator::VariableInformation variableInformation; + + // Internal information about the states that were explored. + InternalStateInformation internalStateInformation; // This member holds information about reachable states that can be retrieved from the outside after a // successful build. boost::optional stateInformation; - // This member holds the program that was most recently translated (if any). - boost::optional preparedProgram; + // A queue of states that still need to be explored. + std::queue statesToExplore; + }; } // namespace adapters diff --git a/src/generator/Choice.cpp b/src/generator/Choice.cpp index 3b6609ebd..8f42b7b3a 100644 --- a/src/generator/Choice.cpp +++ b/src/generator/Choice.cpp @@ -6,7 +6,7 @@ namespace storm { namespace generator { template - Choice::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero()), choiceReward(storm::utility::zero()) { + Choice::Choice(uint_fast64_t actionIndex, bool markovian) : markovian(markovian), actionIndex(actionIndex), distribution(), totalMass(storm::utility::zero()), choiceRewards() { // Intentionally left empty. } @@ -89,7 +89,7 @@ namespace storm { template void Choice::addChoiceReward(ValueType const& value) { - choiceReward += value; + choiceRewards.push_back(value); } template diff --git a/src/generator/Choice.h b/src/generator/Choice.h index 07eb6efbe..78287d62e 100644 --- a/src/generator/Choice.h +++ b/src/generator/Choice.h @@ -142,8 +142,8 @@ namespace storm { // The total probability mass (or rates) of this choice. ValueType totalMass; - // The reward value associated with this choice. - ValueType choiceReward; + // The reward values associated with this choice. + std::vector choiceRewards; // The labels that are associated with this choice. boost::optional choiceLabels; diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index 1fdc38cfb..cf89bd1e6 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -11,15 +11,15 @@ namespace storm { namespace generator { + typedef storm::storage::BitVector CompressedState; + template class NextStateGenerator { public: - typedef storm::storage::BitVector InternalStateType; - typedef StateType (*StateToIdCallback)(InternalStateType const&); - + typedef StateType (*StateToIdCallback)(CompressedState const&); + virtual std::vector getInitialStates(StateToIdCallback stateToIdCallback) = 0; - virtual std::vector> expand(StateType const& state, StateToIdCallback stateToIdCallback) = 0; - virtual ValueType getStateReward(StateType const& state) = 0; + virtual std::vector> expand(CompressedState const& state, StateToIdCallback stateToIdCallback) = 0; }; } } diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index 0acf4d8dd..f49aa1b29 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -1,22 +1,263 @@ #include "src/generator/PrismNextStateGenerator.h" +#include "src/utility/constants.h" +#include "src/utility/macros.h" +#include "src/exceptions/WrongFormatException.h" + namespace storm { namespace generator { template - PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program) : program(program) { + PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(), comparator() { // Intentionally left empty. } template - std::vector> PrismNextStateGenerator::expand(StateType const& state, typename NextStateGenerator::StateToIdCallback stateToIdCallback) { - // TODO + void PrismNextStateGenerator::addRewardModel(storm::prism::RewardModel const& rewardModel) { + selectedRewardModels.push_back(rewardModel); } template - ValueType PrismNextStateGenerator::getStateReward(StateType const& state) { + std::vector> PrismNextStateGenerator::expand(CompressedState const& state, typename NextStateGenerator::StateToIdCallback stateToIdCallback) { // TODO } + template + void PrismNextStateGenerator::unpackStateIntoEvaluator(storm::storage::BitVector const& state) { + for (auto const& booleanVariable : variableInformation.booleanVariables) { + evaluator.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset)); + } + for (auto const& integerVariable : variableInformation.integerVariables) { + evaluator.setIntegerValue(integerVariable.variable, state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound); + } + } + + template + CompressedState PrismNextStateGenerator::applyUpdate(CompressedState const& state, storm::prism::Update const& update) { + return applyUpdate(variableInformation, state, state, update); + } + + template + CompressedState PrismNextStateGenerator::applyUpdate(CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update) { + CompressedState newState(state); + + auto assignmentIt = update.getAssignments().begin(); + auto assignmentIte = update.getAssignments().end(); + + // Iterate over all boolean assignments and carry them out. + auto boolIt = variableInformation.booleanVariables.begin(); + for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasBooleanType(); ++assignmentIt) { + while (assignmentIt->getVariable() != boolIt->variable) { + ++boolIt; + } + newState.set(boolIt->bitOffset, evaluator.asBool(assignmentIt->getExpression())); + } + + // Iterate over all integer assignments and carry them out. + auto integerIt = variableInformation.integerVariables.begin(); + for (; assignmentIt != assignmentIte && assignmentIt->getExpression().hasIntegerType(); ++assignmentIt) { + while (assignmentIt->getVariable() != integerIt->variable) { + ++integerIt; + } + int_fast64_t assignedValue = evaluator.asInt(assignmentIt->getExpression()); + STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'."); + newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound); + STORM_LOG_ASSERT(static_cast(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ")."); + } + + // Check that we processed all assignments. + STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed."); + + return newState; + } + + template + boost::optional>>> PrismNextStateGenerator::getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex) { + boost::optional>>> result((std::vector>>())); + + // Iterate over all modules. + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::prism::Module const& module = program.getModule(i); + + // If the module has no command labeled with the given action, we can skip this module. + if (!module.hasActionIndex(actionIndex)) { + continue; + } + + std::set const& commandIndices = module.getCommandIndicesByActionIndex(actionIndex); + + // If the module contains the action, but there is no command in the module that is labeled with + // this action, we don't have any feasible command combinations. + if (commandIndices.empty()) { + return boost::optional>>>(); + } + + std::vector> 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::prism::Command const& command = module.getCommand(commandIndex); + if (evaluator.asBool(command.getGuardExpression())) { + 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; + } + + template + std::vector> PrismNextStateGenerator::getUnlabeledTransitions(CompressedState const& state, StateToIdCallback stateToIdCallback) { + std::vector> result; + + // Iterate over all modules. + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::prism::Module const& module = program.getModule(i); + + // Iterate over all commands. + for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) { + storm::prism::Command const& command = module.getCommand(j); + + // Only consider unlabeled commands. + if (command.isLabeled()) continue; + + // Skip the command, if it is not enabled. + if (!evaluator.asBool(command.getGuardExpression())) { + continue; + } + + result.push_back(Choice(0, buildChoiceLabeling)); + Choice& choice = result.back(); + + // Remember the command labels only if we were asked to. + if (buildChoiceLabeling) { + choice.addChoiceLabel(command.getGlobalIndex()); + } + + // Iterate over all updates of the current command. + ValueType probabilitySum = storm::utility::zero(); + for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { + storm::prism::Update const& update = command.getUpdate(k); + + // Obtain target state index and add it to the list of known states. If it has not yet been + // seen, we also add it to the set of states that have yet to be explored. + StateType stateIndex = stateToIdCallback(applyUpdate(state, update)); + + // Update the choice by adding the probability/target state to it. + ValueType probability = evaluator.asRational(update.getLikelihoodExpression()); + choice.addProbability(stateIndex, probability); + probabilitySum += probability; + } + + // Check that the resulting distribution is in fact a distribution. + STORM_LOG_THROW(!program.isDiscreteTimeModel() || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ")."); + } + } + + return result; + } + + template + std::vector> PrismNextStateGenerator::getLabeledTransitions(CompressedState const& state, StateToIdCallback stateToIdCallback) { + std::vector> result; + + for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) { + boost::optional>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(program, evaluator, actionIndex); + + // 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->emplace(state, storm::utility::one()); + + for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { + storm::prism::Command const& command = *iteratorList[i]; + + for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) { + storm::prism::Update const& update = command.getUpdate(j); + + for (auto const& stateProbabilityPair : *currentTargetStates) { + // Compute the new state under the current update and add it to the set of new target states. + CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, state, update); + newTargetStates->emplace(newTargetState, stateProbabilityPair.second * evaluator.asRational(update.getLikelihoodExpression())); + } + } + + // If there is one more command to come, shift the target states one time step back. + if (i < iteratorList.size() - 1) { + delete currentTargetStates; + currentTargetStates = newTargetStates; + newTargetStates = new std::unordered_map(); + } + } + + // At this point, we applied all commands of the current command combination and newTargetStates + // contains all target states and their respective probabilities. That means we are now ready to + // add the choice to the list of transitions. + result.push_back(Choice(actionIndex, buildChoiceLabeling)); + + // Now create the actual distribution. + Choice& choice = result.back(); + + // Remember the command labels only if we were asked to. + if (buildChoiceLabeling) { + // Add the labels of all commands to this choice. + for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { + choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex()); + } + } + + ValueType probabilitySum = storm::utility::zero(); + for (auto const& stateProbabilityPair : *newTargetStates) { + StateType actualIndex = stateToIdCallback(stateProbabilityPair.first); + choice.addProbability(actualIndex, stateProbabilityPair.second); + probabilitySum += stateProbabilityPair.second; + } + + // Check that the resulting distribution is in fact a distribution. + STORM_LOG_THROW(!program.isDiscreteTimeModel() || !comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); + + // Dispose of the temporary maps. + delete currentTargetStates; + delete newTargetStates; + + // Now, check whether there is one more command combination to consider. + bool movedIterator = false; + for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) { + ++iteratorList[j]; + if (iteratorList[j] != activeCommandList[j].end()) { + movedIterator = true; + } else { + // Reset the iterator to the beginning of the list. + iteratorList[j] = activeCommandList[j].begin(); + } + } + + done = !movedIterator; + } + } + } + + return result; + } } } \ No newline at end of file diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h index 1330d4420..f5fabe5f7 100644 --- a/src/generator/PrismNextStateGenerator.h +++ b/src/generator/PrismNextStateGenerator.h @@ -2,8 +2,10 @@ #define STORM_GENERATOR_PRISMNEXTSTATEGENERATOR_H_ #include "src/generator/NextStateGenerator.h" +#include "src/generator/VariableInformation.h" #include "src/storage/prism/Program.h" +#include "src/storage/expressions/ExpressionEvaluator.h" namespace storm { namespace generator { @@ -13,17 +15,97 @@ namespace storm { public: typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; - PrismNextStateGenerator(storm::prism::Program const& program); + PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling); - virtual std::vector getInitialStates(StateToIdCallback stateToIdCallback) = 0; - virtual std::vector> expand(StateType const& state, StateToIdCallback stateToIdCallback) override; - virtual ValueType getStateReward(StateType const& state) override; + /*! + * Adds a reward model to the list of selected reward models () + */ + void addRewardModel(storm::prism::RewardModel const& rewardModel); + virtual std::vector getInitialStates(StateToIdCallback stateToIdCallback) = 0; + virtual std::vector> expand(CompressedState const& state, StateToIdCallback stateToIdCallback) override; + private: + /*! + * Unpacks the compressed state into the evaluator. + * + * @param state The state to unpack. + */ + void unpackStateIntoEvaluator(CompressedState 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. + */ + CompressedState applyUpdate(CompressedState const& state, storm::prism::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. + * + * @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. + */ + CompressedState applyUpdate(CompressedState const& state, CompressedState const& baseState, storm::prism::Update const& update); + + /*! + * 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 The program in which to search for active commands. + * @param state The current state. + * @param actionIndex The index of the action label to select. + * @return A list of lists of active commands or nothing. + */ + boost::optional>>> getActiveCommandsByActionIndex(uint_fast64_t const& actionIndex); + + /*! + * Retrieves all unlabeled choices possible from the given state. + * + * @param state The state for which to retrieve the unlabeled choices. + * @return The unlabeled choices of the state. + */ + std::vector> getUnlabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); + + /*! + * Retrieves all labeled choices possible from the given state. + * + * @param state The state for which to retrieve the unlabeled choices. + * @return The labeled choices of the state. + */ + std::vector> getLabeledChoices(CompressedState const& state, StateToIdCallback stateToIdCallback); + // The program used for the generation of next states. - storm::prism::Program program; + storm::prism::Program const& program; + + // The reward models that need to be considered. + std::vector> selectedRewardModels; + + // A flag that stores whether or not to build the choice labeling. + bool buildChoiceLabeling; + + // Information about how the variables are packed + VariableInformation const& variableInformation; + // An evaluator used to evaluate expressions. + storm::expressions::ExpressionEvaluator evaluator; + // A comparator used to compare constants. + storm::utility::ConstantsComparator comparator; }; } diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp new file mode 100644 index 000000000..7f7ed357e --- /dev/null +++ b/src/generator/VariableInformation.cpp @@ -0,0 +1,42 @@ +#include "src/generator/prism/VariableInformation.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace generator { + + BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) { + // Intentionally left empty. + } + + IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) { + // Intentionally left empty. + } + + VariableInformation::VariableInformation(storm::expressions::ExpressionManager const& manager) : manager(manager) { + // Intentionally left empty. + } + + uint_fast64_t VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const { + auto const& booleanIndex = booleanVariableToIndexMap.find(variable); + if (booleanIndex != booleanVariableToIndexMap.end()) { + return booleanVariables[booleanIndex->second].bitOffset; + } + auto const& integerIndex = integerVariableToIndexMap.find(variable); + if (integerIndex != integerVariableToIndexMap.end()) { + return integerVariables[integerIndex->second].bitOffset; + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable."); + } + + uint_fast64_t VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const { + auto const& integerIndex = integerVariableToIndexMap.find(variable); + if (integerIndex != integerVariableToIndexMap.end()) { + return integerVariables[integerIndex->second].bitWidth; + } + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable."); + } + + } +} \ No newline at end of file diff --git a/src/generator/VariableInformation.h b/src/generator/VariableInformation.h new file mode 100644 index 000000000..c1f06e741 --- /dev/null +++ b/src/generator/VariableInformation.h @@ -0,0 +1,71 @@ +#ifndef STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ +#define STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ + +#include +#include + +#include "src/storage/expressions/Variable.h" + +namespace storm { + namespace generator { + + // A structure storing information about the boolean variables of the program. + struct BooleanVariableInformation { + BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset); + + // The boolean variable. + storm::expressions::Variable variable; + + // Its initial value. + bool initialValue; + + // Its bit offset in the compressed state. + uint_fast64_t bitOffset; + }; + + // A structure storing information about the integer variables of the program. + struct IntegerVariableInformation { + IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth); + + // The integer variable. + storm::expressions::Variable variable; + + // Its initial value. + int_fast64_t initialValue; + + // The lower bound of its range. + int_fast64_t lowerBound; + + // The upper bound of its range. + int_fast64_t upperBound; + + // Its bit offset in the compressed state. + uint_fast64_t bitOffset; + + // Its bit width in the compressed state. + uint_fast64_t bitWidth; + }; + + // A structure storing information about the used variables of the program. + struct VariableInformation { + VariableInformation(storm::expressions::ExpressionManager const& manager); + + // Provide methods to access the bit offset and width of variables in the compressed state. + uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const; + uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const; + + // The known boolean variables. + boost::container::flat_map booleanVariableToIndexMap; + std::vector booleanVariables; + + // The known integer variables. + boost::container::flat_map integerVariableToIndexMap; + std::vector integerVariables; + + storm::expressions::ExpressionManager const& manager; + }; + + } +} + +#endif /* STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ */ \ No newline at end of file diff --git a/src/generator/prism/VariableInformation.cpp b/src/generator/prism/VariableInformation.cpp deleted file mode 100644 index f648eda1b..000000000 --- a/src/generator/prism/VariableInformation.cpp +++ /dev/null @@ -1,44 +0,0 @@ -#include "src/generator/prism/VariableInformation.h" - -#include "src/utility/macros.h" -#include "src/exceptions/InvalidArgumentException.h" - -namespace storm { - namespace generator { - namespace prism { - - BooleanVariableInformation::BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset) : variable(variable), initialValue(initialValue), bitOffset(bitOffset) { - // Intentionally left empty. - } - - IntegerVariableInformation::IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), initialValue(initialValue), lowerBound(lowerBound), upperBound(upperBound), bitOffset(bitOffset), bitWidth(bitWidth) { - // Intentionally left empty. - } - - VariableInformation::VariableInformation(storm::expressions::ExpressionManager const& manager) : manager(manager) { - // Intentionally left empty. - } - - uint_fast64_t VariableInformation::getBitOffset(storm::expressions::Variable const& variable) const { - auto const& booleanIndex = booleanVariableToIndexMap.find(variable); - if (booleanIndex != booleanVariableToIndexMap.end()) { - return booleanVariables[booleanIndex->second].bitOffset; - } - auto const& integerIndex = integerVariableToIndexMap.find(variable); - if (integerIndex != integerVariableToIndexMap.end()) { - return integerVariables[integerIndex->second].bitOffset; - } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit index of unknown variable."); - } - - uint_fast64_t VariableInformation::getBitWidth(storm::expressions::Variable const& variable) const { - auto const& integerIndex = integerVariableToIndexMap.find(variable); - if (integerIndex != integerVariableToIndexMap.end()) { - return integerVariables[integerIndex->second].bitWidth; - } - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot look-up bit width of unknown variable."); - } - - } - } -} \ No newline at end of file diff --git a/src/generator/prism/VariableInformation.h b/src/generator/prism/VariableInformation.h deleted file mode 100644 index 56ac7bda2..000000000 --- a/src/generator/prism/VariableInformation.h +++ /dev/null @@ -1,73 +0,0 @@ -#ifndef STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ -#define STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ - -#include -#include - -#include "src/storage/expressions/Variable.h" - -namespace storm { - namespace generator { - namespace prism { - - // A structure storing information about the boolean variables of the program. - struct BooleanVariableInformation { - BooleanVariableInformation(storm::expressions::Variable const& variable, bool initialValue, uint_fast64_t bitOffset); - - // The boolean variable. - storm::expressions::Variable variable; - - // Its initial value. - bool initialValue; - - // Its bit offset in the compressed state. - uint_fast64_t bitOffset; - }; - - // A structure storing information about the integer variables of the program. - struct IntegerVariableInformation { - IntegerVariableInformation(storm::expressions::Variable const& variable, int_fast64_t initialValue, int_fast64_t lowerBound, int_fast64_t upperBound, uint_fast64_t bitOffset, uint_fast64_t bitWidth); - - // The integer variable. - storm::expressions::Variable variable; - - // Its initial value. - int_fast64_t initialValue; - - // The lower bound of its range. - int_fast64_t lowerBound; - - // The upper bound of its range. - int_fast64_t upperBound; - - // Its bit offset in the compressed state. - uint_fast64_t bitOffset; - - // Its bit width in the compressed state. - uint_fast64_t bitWidth; - }; - - // A structure storing information about the used variables of the program. - struct VariableInformation { - VariableInformation(storm::expressions::ExpressionManager const& manager); - - // Provide methods to access the bit offset and width of variables in the compressed state. - uint_fast64_t getBitOffset(storm::expressions::Variable const& variable) const; - uint_fast64_t getBitWidth(storm::expressions::Variable const& variable) const; - - // The known boolean variables. - boost::container::flat_map booleanVariableToIndexMap; - std::vector booleanVariables; - - // The known integer variables. - boost::container::flat_map integerVariableToIndexMap; - std::vector integerVariables; - - storm::expressions::ExpressionManager const& manager; - }; - - } - } -} - -#endif /* STORM_GENERATOR_PRISM_VARIABLEINFORMATION_H_ */ \ No newline at end of file diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index bf8caf4a8..0f5aea4a8 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -77,6 +77,10 @@ namespace storm { return modelType; } + bool Program::isDiscreteTimeModel() const { + return modelType == ModelType::DTMC || modelType == ModelType::MDP; + } + bool Program::hasUndefinedConstants() const { for (auto const& constant : this->getConstants()) { if (!constant.isDefined()) { diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index 45ac16b62..1d091c294 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -66,6 +66,18 @@ namespace storm { * @return The type of the model. */ ModelType getModelType() const; + + /*! + * Retrieves whether the model is a discrete-time model, i.e. a DTMC or an MDP. + * + * @return True iff the model is a discrete-time model. + */ + bool isDiscreteTimeModel() const; + + /*! + * Retrieves whether the model is one without nondeterministic choices, i.e. a DTMC or a CTMC. + */ + bool isDeterministicModel() const; /*! * Retrieves whether there are undefined constants of any type in the program.