diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index cfb08fb79..0b2fad41a 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -161,6 +161,9 @@ namespace storm { } // Block the current initial state to search for the next one. + if (!blockingExpression.isInitialized()) { + break; + } solver->add(blockingExpression); } diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index c0026a98d..7eb2291c5 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -23,8 +23,9 @@ namespace storm { template PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(program.getManager(), options), program(program), rewardModels() { + STORM_LOG_TRACE("Creating next-state generator for PRISM program: " << program); STORM_LOG_THROW(!this->program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); - + // Only after checking validity of the program, we initialize the variable information. this->checkValid(program); this->variableInformation = VariableInformation(program); @@ -166,6 +167,9 @@ namespace storm { initialStateIndices.push_back(id); // Block the current initial state to search for the next one. + if (!blockingExpression.isInitialized()) { + break; + } solver->add(blockingExpression); } @@ -314,7 +318,7 @@ namespace storm { 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); @@ -445,7 +449,6 @@ namespace storm { 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); diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 7d54f18c6..f9f4350b9 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -65,6 +65,8 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << lineNumber << " of file " << filename << "."); } + STORM_LOG_TRACE("Parsed PRISM input: " << result); + return result; } diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h index 620432580..df8a61c21 100644 --- a/src/storage/prism/Module.h +++ b/src/storage/prism/Module.h @@ -104,7 +104,6 @@ namespace storm { */ std::set getAllExpressionVariables() const; - /*! * Retrieves a list of expressions that characterize the legal ranges of all variables declared by this * module. diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 4962157eb..acb17a17e 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -734,6 +734,12 @@ namespace storm { } } + // As we possibly delete some commands and some actions might be dropped from modules altogether, we need to + // maintain a list of actions that we need to remove in other modules. For example, if module A loses all [a] + // commands, we need to delete all [a] commands from all other modules as well. If we do not do that, we will + // remove the forced synchronization that was there before. + std::set actionIndicesToDelete; + // Now we can substitute the constants in all expressions appearing in the program. std::vector newBooleanVariables; newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables()); @@ -757,6 +763,9 @@ namespace storm { newModules.reserve(this->getNumberOfModules()); for (auto const& module : this->getModules()) { newModules.emplace_back(module.substitute(constantSubstitution)); + + // Determine the set of action indices that have been deleted entirely. + std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin())); } std::vector newRewardModels; @@ -773,7 +782,37 @@ namespace storm { newLabels.emplace_back(label.substitute(constantSubstitution)); } - return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct()); + // If we have to delete whole actions, do so now. + std::map newActionToIndexMap; + if (!actionIndicesToDelete.empty()) { + boost::container::flat_set actionsToKeep; + std::set_difference(this->getSynchronizingActionIndices().begin(), this->getSynchronizingActionIndices().end(), actionIndicesToDelete.begin(), actionIndicesToDelete.end(), std::inserter(actionsToKeep, actionsToKeep.begin())); + + // Insert the silent action as this is not contained in the synchronizing action indices. + actionsToKeep.insert(0); + + std::vector cleanedModules; + cleanedModules.reserve(this->getNumberOfModules()); + for (auto const& module : newModules) { + cleanedModules.emplace_back(module.restrictCommands(actionsToKeep)); + } + newModules = std::move(cleanedModules); + + std::vector cleanedRewardModels; + cleanedRewardModels.reserve(this->getNumberOfRewardModels()); + for (auto const& rewardModel : newRewardModels) { + cleanedRewardModels.emplace_back(rewardModel.restrictActionRelatedRewards(actionsToKeep)); + } + newRewardModels = std::move(cleanedRewardModels); + + for (auto const& entry : this->getActionNameToIndexMapping()) { + if (actionsToKeep.find(entry.second) != actionsToKeep.end()) { + newActionToIndexMap.emplace(entry.first, entry.second); + } + } + } + + return Program(this->manager, this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, actionIndicesToDelete.empty() ? this->getActionNameToIndexMapping() : newActionToIndexMap, newRewardModels, newLabels, newInitialConstruct, this->getOptionalSystemCompositionConstruct()); } void Program::checkValidity(Program::ValidityCheckLevel lvl) const { @@ -1153,17 +1192,19 @@ namespace storm { } Program Program::simplify() { + // Start by substituting the constants, because this will potentially erase some commands or even actions. + Program substitutedProgram = this->substituteConstants(); + std::vector newModules; - std::vector newConstants = this->getConstants(); - for (auto const& module : this->getModules()) { - // Remove identity assignments from the updates + std::vector newConstants = substitutedProgram.getConstants(); + for (auto const& module : substitutedProgram.getModules()) { + // Remove identity assignments from the updates. std::vector newCommands; for (auto const& command : module.getCommands()) { newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates()); } - // Substitute Variables by Global constants if possible. - + // Substitute variables by global constants if possible. std::map booleanVars; std::map integerVars; for (auto const& variable : module.getBooleanVariables()) { @@ -1179,11 +1220,11 @@ namespace storm { // Check all assignments. for (auto const& assignment : update.getAssignments()) { auto bit = booleanVars.find(assignment.getVariable()); - if(bit != booleanVars.end()) { + if (bit != booleanVars.end()) { booleanVars.erase(bit); } else { auto iit = integerVars.find(assignment.getVariable()); - if(iit != integerVars.end()) { + if (iit != integerVars.end()) { integerVars.erase(iit); } } @@ -1192,31 +1233,30 @@ namespace storm { } std::vector newBVars; - for(auto const& variable : module.getBooleanVariables()) { - if(booleanVars.count(variable.getExpressionVariable()) == 0) { + for (auto const& variable : module.getBooleanVariables()) { + if (booleanVars.find(variable.getExpressionVariable()) == booleanVars.end()) { newBVars.push_back(variable); } } std::vector newIVars; - for(auto const& variable : module.getIntegerVariables()) { - if(integerVars.count(variable.getExpressionVariable()) == 0) { + for (auto const& variable : module.getIntegerVariables()) { + if (integerVars.find(variable.getExpressionVariable()) == integerVars.end()) { newIVars.push_back(variable); } } newModules.emplace_back(module.getName(), newBVars, newIVars, newCommands); - for(auto const& entry : booleanVars) { + for (auto const& entry : booleanVars) { newConstants.emplace_back(entry.first, entry.second); } - for(auto const& entry : integerVars) { + for (auto const& entry : integerVars) { newConstants.emplace_back(entry.first, entry.second); } } - return replaceModulesAndConstantsInProgram(newModules, newConstants).substituteConstants(); - + return substitutedProgram.replaceModulesAndConstantsInProgram(newModules, newConstants); } Program Program::replaceModulesAndConstantsInProgram(std::vector const& newModules, std::vector const& newConstants) { diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp index 30c43728c..52ef5dc67 100644 --- a/src/storage/prism/RewardModel.cpp +++ b/src/storage/prism/RewardModel.cpp @@ -81,6 +81,24 @@ namespace storm { return true; } + RewardModel RewardModel::restrictActionRelatedRewards(boost::container::flat_set const& actionIndicesToKeep) const { + std::vector newStateActionRewards; + for (auto const& stateActionReward : this->getStateActionRewards()) { + if (actionIndicesToKeep.find(stateActionReward.getActionIndex()) != actionIndicesToKeep.end()) { + newStateActionRewards.emplace_back(stateActionReward); + } + } + + std::vector newTransitionRewards; + for (auto const& transitionReward : this->getTransitionRewards()) { + if (actionIndicesToKeep.find(transitionReward.getActionIndex()) != actionIndicesToKeep.end()) { + newTransitionRewards.emplace_back(transitionReward); + } + } + + return RewardModel(this->getName(), this->getStateRewards(), newStateActionRewards, newTransitionRewards, this->getFilename(), this->getLineNumber()); + } + std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel) { stream << "rewards"; if (rewardModel.getName() != "") { diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h index c62aff61a..01ab69508 100644 --- a/src/storage/prism/RewardModel.h +++ b/src/storage/prism/RewardModel.h @@ -4,6 +4,7 @@ #include #include #include +#include #include "src/storage/prism/StateReward.h" #include "src/storage/prism/StateActionReward.h" @@ -108,6 +109,14 @@ namespace storm { */ bool containsVariablesOnlyInRewardValueExpressions(std::set const& undefinedConstantVariables) const; + /*! + * Restricts all action-related rewards of the reward model to the ones with an action index in the provided set. + * + * @param actionIndicesToKeep The set of action indices to keep. + * @return The resulting reward model. + */ + RewardModel restrictActionRelatedRewards(boost::container::flat_set const& actionIndicesToKeep) const; + friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel); private: diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index 5956e72c9..c6d2f9c65 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -10,7 +10,7 @@ namespace storm { storm::prism::Program parseProgram(std::string const& path) { - storm::prism::Program program= storm::parser::PrismParser::parse(path).simplify().simplify(); + storm::prism::Program program = storm::parser::PrismParser::parse(path).simplify().simplify(); program.checkValidity(); return program; }