fixed bug in symbolic model generation

Former-commit-id: 9b99c0d75f

src/builder/DdPrismModelBuilder.cpp

@@ -118,7 +118,7 @@ namespace storm {
                         columnMetaVariables.insert(variablePair.second);
                         variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second);
                         
-                        storm::dd::Add<Type> variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first).toAdd();
+                        storm::dd::Add<Type> 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 <storm::dd::DdType Type>
-        DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels() {
+        DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() {
             // Intentionally left empty.
         }
         
         template <storm::dd::DdType Type>
-        DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
+        DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates() {
             this->preserveFormula(formula);
+            this->setTerminalStatesFromFormula(formula);
         }
         
         template <storm::dd::DdType Type>
-        DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels() {
+        DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> 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 <storm::dd::DdType Type>
+        void DdPrismModelBuilder<Type>::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 <storm::dd::DdType Type>
         void DdPrismModelBuilder<Type>::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
             std::map<storm::expressions::Variable, storm::expressions::Expression> 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<storm::expressions::Expression>(options.terminalStates.get());
+                } else {
+                    std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
+                    terminalExpression = preparedProgram.getLabelExpression(labelName);
+                }
+                // TODO
+            }
+            
             storm::dd::Bdd<Type> reachableStates = computeReachableStates(generationInfo, initialStates, transitionMatrixBdd);
             storm::dd::Add<Type> 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<Type> 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 {

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<std::vector<storm::expressions::Expression>> 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<boost::variant<storm::expressions::Expression, std::string>> terminalStates;
             };
             
             /*!

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

src/models/sparse/NondeterministicModel.cpp

@@ -55,7 +55,7 @@ namespace storm {
             template<typename ValueType, typename RewardModelType>
             void NondeterministicModel<ValueType, RewardModelType>::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);
             }
             

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.
                  *

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;
             }

src/storage/prism/Program.h

@@ -345,6 +345,13 @@ namespace storm {
              */
             std::vector<Label> const& getLabels() const;
             
+            /*!
+             * Retrieves the expression associated with the given label, if it exists.
+             *
+             * @param labelName The name of the label to retrieve.
+             */
+            storm::expressions::Expression const& getLabelExpression(std::string const& label) const;
+            
             /*!
              * Retrieves the number of labels in the program.
              *
@@ -480,6 +487,9 @@ namespace storm {
             // The labels that are defined for this model.
             std::vector<Label> labels;
             
+            // A mapping from labels to their indices.
+            std::map<std::string, uint_fast64_t> labelToIndexMap;
+            
             // A mapping from action names to their indices.
             std::map<std::string, uint_fast64_t> actionToIndexMap;