From 080b50a890b9c8c0907079fd583080a3757e6a27 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 26 Aug 2015 13:45:34 +0200 Subject: [PATCH] fixed bug in symbolic model generation Former-commit-id: 9b99c0d75f2c57e44999123e7de2a415fdd92202 --- src/builder/DdPrismModelBuilder.cpp | 53 +++++++++++++++++++-- src/builder/DdPrismModelBuilder.h | 14 ++++++ src/builder/ExplicitPrismModelBuilder.cpp | 2 +- src/models/sparse/NondeterministicModel.cpp | 2 +- src/settings/modules/GeneralSettings.h | 1 - src/storage/prism/Program.cpp | 11 ++++- src/storage/prism/Program.h | 10 ++++ 7 files changed, 85 insertions(+), 8 deletions(-) diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index c0b540c96..41adb09a2 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -118,7 +118,7 @@ namespace storm { columnMetaVariables.insert(variablePair.second); variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); - storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd(); + storm::dd::Add variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd() * manager->getRange(variablePair.second).toAdd(); variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); rowColumnMetaVariablePairs.push_back(variablePair); @@ -190,17 +190,18 @@ namespace storm { }; template - DdPrismModelBuilder::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels() { + DdPrismModelBuilder::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() { // Intentionally left empty. } template - DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()) { + DdPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates() { this->preserveFormula(formula); + this->setTerminalStatesFromFormula(formula); } template - DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels() { + DdPrismModelBuilder::Options::Options(std::vector> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; this->buildAllLabels = true; @@ -208,6 +209,9 @@ namespace storm { for (auto const& formula : formulas) { this->preserveFormula(*formula); } + if (formulas.size() == 1) { + this->setTerminalStatesFromFormula(*formulas.front()); + } } } @@ -240,6 +244,30 @@ namespace storm { } } + template + void DdPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { + if (formula.isAtomicExpressionFormula()) { + terminalStates = formula.asAtomicExpressionFormula().getExpression(); + } else if (formula.isAtomicLabelFormula()) { + terminalStates = formula.asAtomicLabelFormula().getLabel(); + } else if (formula.isEventuallyFormula()) { + storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); + if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { + this->setTerminalStatesFromFormula(sub); + } + } else if (formula.isUntilFormula()) { + storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula(); + if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { + this->setTerminalStatesFromFormula(right); + } + } else if (formula.isProbabilityOperatorFormula()) { + storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); + if (sub.isEventuallyFormula() || sub.isUntilFormula()) { + this->setTerminalStatesFromFormula(sub); + } + } + } + template void DdPrismModelBuilder::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) { std::map newConstantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); @@ -995,6 +1023,19 @@ namespace storm { if (program.getModelType() == storm::prism::Program::ModelType::MDP) { transitionMatrixBdd = transitionMatrixBdd.existsAbstract(generationInfo.allNondeterminismVariables); } + + // If we were asked to treat some states as terminal states, we cut away their transitions now. + if (options.terminalStates) { + storm::expressions::Expression terminalExpression; + if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) { + terminalExpression = boost::get(options.terminalStates.get()); + } else { + std::string const& labelName = boost::get(options.terminalStates.get()); + terminalExpression = preparedProgram.getLabelExpression(labelName); + } + // TODO + } + storm::dd::Bdd reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd); storm::dd::Add reachableStatesAdd = reachableStates.toAdd(); transitionMatrix *= reachableStatesAdd; @@ -1017,6 +1058,10 @@ namespace storm { // want to attach a lot of self-loops to the deadlock states. storm::dd::Add action = generationInfo.manager->getAddOne(); std::for_each(generationInfo.allNondeterminismVariables.begin(), generationInfo.allNondeterminismVariables.end(), [&action,&generationInfo] (storm::expressions::Variable const& metaVariable) { action *= !generationInfo.manager->getIdentity(metaVariable); } ); + // Make sure that global variables do not change along the introduced self-loops. + for (auto const& var : generationInfo.allGlobalVariables) { + action *= generationInfo.variableToIdentityMap.at(var); + } transitionMatrix += deadlockStates * globalModule.identity * action; } } else { diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 44fb6d2f8..20f6e76f0 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -71,6 +71,16 @@ namespace storm { */ void preserveFormula(storm::logic::Formula const& formula); + /*! + * Analyzes the given formula and sets an expression for the states states of the model that can be + * treated as terminal states. Note that this may interfere with checking properties different than the + * one provided. + * + * @param formula The formula used to (possibly) derive an expression for the terminal states of the + * model. + */ + void setTerminalStatesFromFormula(storm::logic::Formula const& formula); + // A flag that indicates whether or not all reward models are to be build. bool buildAllRewardModels; @@ -88,6 +98,10 @@ namespace storm { // An optional set of expressions for which labels need to be built. boost::optional> expressionLabels; + + // An optional expression or label that characterizes the terminal states of the model. If this is set, + // the outgoing transitions of these states are replaced with a self-loop. + boost::optional> terminalStates; }; /*! diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 3b9fb23a9..f4efe7195 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -181,7 +181,7 @@ namespace storm { } else { preparedProgram = 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 diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp index fd3f95f02..340400dde 100644 --- a/src/models/sparse/NondeterministicModel.cpp +++ b/src/models/sparse/NondeterministicModel.cpp @@ -55,7 +55,7 @@ namespace storm { template void NondeterministicModel::printModelInformationToStream(std::ostream& out) const { this->printModelInformationHeaderToStream(out); - out << "Choices: \t\t" << this->getNumberOfChoices() << std::endl; + out << "Choices: \t" << this->getNumberOfChoices() << std::endl; this->printModelInformationFooterToStream(out); } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 648b455ef..f10035c71 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -22,7 +22,6 @@ namespace storm { // An enumeration of all engines. enum class Engine { Sparse, Hybrid, Dd }; - /*! * Creates a new set of general settings that is managed by the given manager. * diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 18888c646..9859df52a 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -20,7 +20,7 @@ namespace storm { globalIntegerVariables(globalIntegerVariables), globalIntegerVariableToIndexMap(), formulas(formulas), formulaToIndexMap(), modules(modules), moduleToIndexMap(), rewardModels(rewardModels), rewardModelToIndexMap(), initialConstruct(initialConstruct), - labels(labels), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), + labels(labels), labelToIndexMap(), actionToIndexMap(actionToIndexMap), indexToActionMap(), actions(), synchronizingActionIndices(), actionIndicesToModuleIndexMap(), variableToModuleIndexMap() { @@ -325,6 +325,12 @@ namespace storm { return this->labels; } + storm::expressions::Expression const& Program::getLabelExpression(std::string const& label) const { + auto const& labelIndexPair = labelToIndexMap.find(label); + STORM_LOG_THROW(labelIndexPair != labelToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve expression for unknown label '" << label << "'."); + return this->labels[labelIndexPair->second].getStatePredicateExpression(); + } + std::size_t Program::getNumberOfLabels() const { return this->getLabels().size(); } @@ -382,6 +388,9 @@ namespace storm { for (uint_fast64_t formulaIndex = 0; formulaIndex < this->getNumberOfFormulas(); ++formulaIndex) { this->formulaToIndexMap[this->getFormulas()[formulaIndex].getName()] = formulaIndex; } + for (uint_fast64_t labelIndex = 0; labelIndex < this->getNumberOfLabels(); ++labelIndex) { + this->labelToIndexMap[this->getLabels()[labelIndex].getName()] = labelIndex; + } for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) { this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex; } diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h index eea245684..e4f64af8a 100644 --- a/src/storage/prism/Program.h +++ b/src/storage/prism/Program.h @@ -345,6 +345,13 @@ namespace storm { */ std::vector