The labels of the models are now only built if no property was given or the given property contains the label.

Former-commit-id: d5ce5a2e1e

src/builder/ExplicitPrismModelBuilder.cpp

@@ -62,9 +62,18 @@ namespace storm {
             
 
         template <typename ValueType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildRewards(false), rewardModelName(), constantDefinitions() {
-            // FIXME: buildRewards should be something like formula.containsRewardOperator()
-            // FIXME: The necessary labels need to be computed properly.
+        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildRewards(formula.containsRewardOperator()), rewardModelName(), constantDefinitions(), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
+            // Extract all the labels used in the formula.
+            std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas();
+            for (auto const& formula : atomicLabelFormulas) {
+                labelsToBuild.get().insert(formula.get()->getLabel());
+            }
+            
+            // Extract all the expressions used in the formula.
+            std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula.getAtomicExpressionFormulas();
+            for (auto const& formula : atomicExpressionFormulas) {
+                expressionLabels.get().push_back(formula.get()->getExpression());
+            }
         }
 
         template <typename ValueType, typename IndexType>
@@ -129,7 +138,25 @@ namespace storm {
                 }
             }
             
-            ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, options.buildCommandLabels);
+            // 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) {
+                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) {
+                for (auto const& expression : options.expressionLabels.get()) {
+                    std::stringstream stream;
+                    stream << expression;
+                    std::string name = stream.str();
+                    if (!preparedProgram.hasLabel(name)) {
+                        preparedProgram.addLabel(name, expression);
+                    }
+                }
+            }
+            
+            ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, options);
             
             std::unique_ptr<storm::models::AbstractModel<ValueType>> result;
             switch (program.getModelType()) {
@@ -647,7 +674,7 @@ namespace storm {
         }
         
         template <typename ValueType, typename IndexType>
-        typename ExplicitPrismModelBuilder<ValueType, IndexType>::ModelComponents ExplicitPrismModelBuilder<ValueType, IndexType>::buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel, bool commandLabels) {
+        typename ExplicitPrismModelBuilder<ValueType, IndexType>::ModelComponents ExplicitPrismModelBuilder<ValueType, IndexType>::buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel, Options const& options) {
             ModelComponents modelComponents;
             
             uint_fast64_t bitOffset = 0;
@@ -693,7 +720,7 @@ namespace storm {
             // Build the transition and reward matrices.
             storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
             storm::storage::SparseMatrixBuilder<ValueType> transitionRewardMatrixBuilder(0, 0, 0, false, !deterministicModel, 0);
-            modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, commandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, transitionRewardMatrixBuilder);
+            modelComponents.choiceLabeling = buildMatrices(program, variableInformation, rewardModel.getTransitionRewards(), stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, transitionRewardMatrixBuilder);
             
             // Finalize the resulting matrices.
             modelComponents.transitionMatrix = transitionMatrixBuilder.build();

src/builder/ExplicitPrismModelBuilder.h

@@ -154,6 +154,12 @@ namespace storm {
                 
                 // An optional mapping that, if given, contains defining expressions for undefined constants.
                 boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> constantDefinitions;
+                
+                // An optional set of labels that, if given, restricts the labels that are built.
+                boost::optional<std::set<std::string>> labelsToBuild;
+                
+                // An optional set of expressions for which labels need to be built.
+                boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
             };
             
             /*!
@@ -249,9 +255,10 @@ namespace storm {
              *
              * @param program The program whose state space to explore.
              * @param rewardModel The reward model that is to be considered.
+             * @param options A set of options used to customize the building process.
              * @return A structure containing the components of the resulting model.
              */
-            static ModelComponents buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel, bool commandLabels = false);
+            static ModelComponents buildModelComponents(storm::prism::Program const& program, storm::prism::RewardModel const& rewardModel, Options const& options);
             
             /*!
              * Builds the state labeling for the given program.

src/logic/BinaryPathFormula.cpp

@@ -18,12 +18,20 @@ namespace storm {
             return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula();
         }
         
-        bool BinaryPathFormula::hasProbabilityOperator() const {
-            return this->getLeftSubformula().hasProbabilityOperator() || this->getRightSubformula().hasProbabilityOperator();
+        bool BinaryPathFormula::containsProbabilityOperator() const {
+            return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator();
         }
         
-        bool BinaryPathFormula::hasNestedProbabilityOperators() const {
-            return this->getLeftSubformula().Formula::hasNestedProbabilityOperators() || this->getRightSubformula().hasNestedProbabilityOperators();
+        bool BinaryPathFormula::containsNestedProbabilityOperators() const {
+            return this->getLeftSubformula().containsNestedProbabilityOperators() || this->getRightSubformula().containsNestedProbabilityOperators();
+        }
+        
+        bool BinaryPathFormula::containsRewardOperator() const {
+            return this->getLeftSubformula().containsRewardOperator() || this->getRightSubformula().containsRewardOperator();
+        }
+        
+        bool BinaryPathFormula::containsNestedRewardOperators() const {
+            return this->getLeftSubformula().containsNestedRewardOperators() || this->getRightSubformula().containsNestedRewardOperators();
         }
         
         Formula const& BinaryPathFormula::getLeftSubformula() const {

src/logic/BinaryPathFormula.h

@@ -19,8 +19,10 @@ namespace storm {
             
             virtual bool isPctlPathFormula() const override;
             virtual bool isLtlFormula() const override;
-            virtual bool hasProbabilityOperator() const override;
-            virtual bool hasNestedProbabilityOperators() const override;
+            virtual bool containsProbabilityOperator() const override;
+            virtual bool containsNestedProbabilityOperators() const override;
+            virtual bool containsRewardOperator() const override;
+            virtual bool containsNestedRewardOperators() const override;
             
             Formula const& getLeftSubformula() const;
             Formula const& getRightSubformula() const;

src/logic/BinaryStateFormula.cpp

@@ -18,12 +18,20 @@ namespace storm {
             return this->getLeftSubformula().isLtlFormula() && this->getRightSubformula().isLtlFormula();
         }
         
-        bool BinaryStateFormula::hasProbabilityOperator() const {
-            return this->getLeftSubformula().hasProbabilityOperator() || this->getRightSubformula().hasProbabilityOperator();
+        bool BinaryStateFormula::containsProbabilityOperator() const {
+            return this->getLeftSubformula().containsProbabilityOperator() || this->getRightSubformula().containsProbabilityOperator();
         }
         
-        bool BinaryStateFormula::hasNestedProbabilityOperators() const {
-            return this->getLeftSubformula().hasNestedProbabilityOperators() || this->getRightSubformula().hasNestedProbabilityOperators();
+        bool BinaryStateFormula::containsNestedProbabilityOperators() const {
+            return this->getLeftSubformula().containsNestedProbabilityOperators() || this->getRightSubformula().containsNestedProbabilityOperators();
+        }
+        
+        bool BinaryStateFormula::containsRewardOperator() const {
+            return this->getLeftSubformula().containsRewardOperator() || this->getRightSubformula().containsRewardOperator();
+        }
+        
+        bool BinaryStateFormula::containsNestedRewardOperators() const {
+            return this->containsNestedRewardOperators() || this->getRightSubformula().containsNestedRewardOperators();
         }
         
         Formula const& BinaryStateFormula::getLeftSubformula() const {

src/logic/BinaryStateFormula.h

@@ -17,8 +17,10 @@ namespace storm {
 
             virtual bool isPctlStateFormula() const override;
             virtual bool isLtlFormula() const override;
-            virtual bool hasProbabilityOperator() const override;
-            virtual bool hasNestedProbabilityOperators() const override;
+            virtual bool containsProbabilityOperator() const override;
+            virtual bool containsNestedProbabilityOperators() const override;
+            virtual bool containsRewardOperator() const override;
+            virtual bool containsNestedRewardOperators() const override;
             
             Formula const& getLeftSubformula() const;
             Formula const& getRightSubformula() const;

src/logic/ExpectedTimeOperatorFormula.cpp

@@ -26,12 +26,12 @@ namespace storm {
             return this->getSubformula().isPctlStateFormula();
         }
         
-        bool ExpectedTimeOperatorFormula::hasProbabilityOperator() const {
-            return this->getSubformula().hasProbabilityOperator();
+        bool ExpectedTimeOperatorFormula::containsProbabilityOperator() const {
+            return this->getSubformula().containsProbabilityOperator();
         }
         
-        bool ExpectedTimeOperatorFormula::hasNestedProbabilityOperators() const {
-            return this->getSubformula().hasNestedProbabilityOperators();
+        bool ExpectedTimeOperatorFormula::containsNestedProbabilityOperators() const {
+            return this->getSubformula().containsNestedProbabilityOperators();
         }
         
         ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {

src/logic/ExpectedTimeOperatorFormula.h

@@ -20,8 +20,8 @@ namespace storm {
             virtual bool isExpectedTimeOperatorFormula() const override;
             
             virtual bool isPctlStateFormula() const override;
-            virtual bool hasProbabilityOperator() const override;
-            virtual bool hasNestedProbabilityOperators() const override;
+            virtual bool containsProbabilityOperator() const override;
+            virtual bool containsNestedProbabilityOperators() const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
         };

src/logic/Formula.cpp

@@ -138,11 +138,19 @@ namespace storm {
             return false;
         }
         
-        bool Formula::hasProbabilityOperator() const {
+        bool Formula::containsProbabilityOperator() const {
             return false;
         }
         
-        bool Formula::hasNestedProbabilityOperators() const {
+        bool Formula::containsNestedProbabilityOperators() const {
+            return false;
+        }
+        
+        bool Formula::containsRewardOperator() const {
+            return false;
+        }
+        
+        bool Formula::containsNestedRewardOperators() const {
             return false;
         }
         

src/logic/Formula.h

@@ -83,8 +83,10 @@ namespace storm {
             virtual bool isPltlFormula() const;
             virtual bool isLtlFormula() const;
             virtual bool isPropositionalFormula() const;
-            virtual bool hasProbabilityOperator() const;
-            virtual bool hasNestedProbabilityOperators() const;
+            virtual bool containsProbabilityOperator() const;
+            virtual bool containsNestedProbabilityOperators() const;
+            virtual bool containsRewardOperator() const;
+            virtual bool containsNestedRewardOperators() const;
             
             static std::shared_ptr<Formula const> getTrueFormula();
             

src/logic/LongRunAverageOperatorFormula.cpp

@@ -26,12 +26,12 @@ namespace storm {
             return this->getSubformula().isPctlStateFormula();
         }
         
-        bool LongRunAverageOperatorFormula::hasProbabilityOperator() const {
-            return this->getSubformula().hasProbabilityOperator();
+        bool LongRunAverageOperatorFormula::containsProbabilityOperator() const {
+            return this->getSubformula().containsProbabilityOperator();
         }
         
-        bool LongRunAverageOperatorFormula::hasNestedProbabilityOperators() const {
-            return this->getSubformula().hasNestedProbabilityOperators();
+        bool LongRunAverageOperatorFormula::containsNestedProbabilityOperators() const {
+            return this->getSubformula().containsNestedProbabilityOperators();
         }
         
         LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {

src/logic/LongRunAverageOperatorFormula.h

@@ -20,8 +20,8 @@ namespace storm {
             virtual bool isLongRunAverageOperatorFormula() const override;
             
             virtual bool isPctlStateFormula() const override;
-            virtual bool hasProbabilityOperator() const override;
-            virtual bool hasNestedProbabilityOperators() const override;
+            virtual bool containsProbabilityOperator() const override;
+            virtual bool containsNestedProbabilityOperators() const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
         };

src/logic/ProbabilityOperatorFormula.cpp

@@ -30,12 +30,12 @@ namespace storm {
             return this->getSubformula().isLtlFormula();
         }
         
-        bool ProbabilityOperatorFormula::hasProbabilityOperator() const {
+        bool ProbabilityOperatorFormula::containsProbabilityOperator() const {
             return true;
         }
         
-        bool ProbabilityOperatorFormula::hasNestedProbabilityOperators() const {
-            return this->getSubformula().hasProbabilityOperator();
+        bool ProbabilityOperatorFormula::containsNestedProbabilityOperators() const {
+            return this->getSubformula().containsProbabilityOperator();
         }
         
         ProbabilityOperatorFormula::ProbabilityOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {

src/logic/ProbabilityOperatorFormula.h

@@ -19,8 +19,8 @@ namespace storm {
             
             virtual bool isPctlStateFormula() const override;
             virtual bool isPltlFormula() const override;
-            virtual bool hasProbabilityOperator() const override;
-            virtual bool hasNestedProbabilityOperators() const override;
+            virtual bool containsProbabilityOperator() const override;
+            virtual bool containsNestedProbabilityOperators() const override;
             
             virtual bool isProbabilityOperatorFormula() const override;
             

src/logic/RewardOperatorFormula.cpp

@@ -26,6 +26,14 @@ namespace storm {
             return this->getSubformula().isRewardPathFormula();
         }
         
+        bool RewardOperatorFormula::containsRewardOperator() const {
+            return true;
+        }
+        
+        bool RewardOperatorFormula::containsNestedRewardOperators() const {
+            return this->getSubformula().containsRewardOperator();
+        }
+        
         RewardOperatorFormula::RewardOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {
             // Intentionally left empty.
         }

src/logic/RewardOperatorFormula.h

@@ -18,8 +18,10 @@ namespace storm {
             }
             
             virtual bool isRewardOperatorFormula() const override;
-            
+
             virtual bool isPctlStateFormula() const override;
+            virtual bool containsRewardOperator() const override;
+            virtual bool containsNestedRewardOperators() const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
         };

src/logic/UnaryPathFormula.cpp

@@ -18,12 +18,20 @@ namespace storm {
             return this->getSubformula().isLtlFormula();
         }
         
-        bool UnaryPathFormula::hasProbabilityOperator() const {
-            return this->getSubformula().hasProbabilityOperator();
+        bool UnaryPathFormula::containsProbabilityOperator() const {
+            return this->getSubformula().containsProbabilityOperator();
         }
         
-        bool UnaryPathFormula::hasNestedProbabilityOperators() const {
-            return this->getSubformula().hasNestedProbabilityOperators();
+        bool UnaryPathFormula::containsNestedProbabilityOperators() const {
+            return this->getSubformula().containsNestedProbabilityOperators();
+        }
+        
+        bool UnaryPathFormula::containsRewardOperator() const {
+            return this->getSubformula().containsRewardOperator();
+        }
+        
+        bool UnaryPathFormula::containsNestedRewardOperators() const {
+            return this->getSubformula().containsNestedRewardOperators();
         }
         
         Formula const& UnaryPathFormula::getSubformula() const {

src/logic/UnaryPathFormula.h

@@ -19,8 +19,10 @@ namespace storm {
             
             virtual bool isPctlPathFormula() const override;
             virtual bool isLtlFormula() const override;
-            virtual bool hasProbabilityOperator() const override;
-            virtual bool hasNestedProbabilityOperators() const override;
+            virtual bool containsProbabilityOperator() const override;
+            virtual bool containsNestedProbabilityOperators() const override;
+            virtual bool containsRewardOperator() const override;
+            virtual bool containsNestedRewardOperators() const override;
             
             Formula const& getSubformula() const;
             

src/logic/UnaryStateFormula.cpp

@@ -22,12 +22,20 @@ namespace storm {
             return this->getSubformula().isLtlFormula();
         }
         
-        bool UnaryStateFormula::hasProbabilityOperator() const {
-            return getSubformula().hasProbabilityOperator();
+        bool UnaryStateFormula::containsProbabilityOperator() const {
+            return getSubformula().containsProbabilityOperator();
         }
         
-        bool UnaryStateFormula::hasNestedProbabilityOperators() const {
-            return getSubformula().hasNestedProbabilityOperators();
+        bool UnaryStateFormula::containsNestedProbabilityOperators() const {
+            return getSubformula().containsNestedProbabilityOperators();
+        }
+        
+        bool UnaryStateFormula::containsRewardOperator() const {
+            return this->getSubformula().containsRewardOperator();
+        }
+        
+        bool UnaryStateFormula::containsNestedRewardOperators() const {
+            return this->getSubformula().containsNestedRewardOperators();
         }
         
         Formula const& UnaryStateFormula::getSubformula() const {

src/logic/UnaryStateFormula.h

@@ -18,8 +18,10 @@ namespace storm {
             virtual bool isPropositionalFormula() const override;
             virtual bool isPctlStateFormula() const override;
             virtual bool isLtlFormula() const override;
-            virtual bool hasProbabilityOperator() const override;
-            virtual bool hasNestedProbabilityOperators() const override;
+            virtual bool containsProbabilityOperator() const override;
+            virtual bool containsNestedProbabilityOperators() const override;
+            virtual bool containsRewardOperator() const override;
+            virtual bool containsNestedRewardOperators() const override;
             
             Formula const& getSubformula() const;
             

src/storage/prism/Program.cpp

@@ -196,6 +196,11 @@ namespace storm {
             return this->rewardModels[index];
         }
         
+        bool Program::hasLabel(std::string const& labelName) const {
+            auto it = std::find_if(labels.begin(), labels.end(), [&labelName] (storm::prism::Label const& label) { return label.getName() == labelName; } );
+            return it != labels.end();
+        }
+        
         std::vector<Label> const& Program::getLabels() const {
             return this->labels;
         }
@@ -227,6 +232,9 @@ namespace storm {
                     newLabels.emplace_back(*it);
                 }
             }
+            
+            // Move the new labels in place.
+            this->labels = std::move(newLabels);
         }
         
         Program Program::restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) const {

src/storage/prism/Program.h

@@ -296,6 +296,14 @@ namespace storm {
              */
             RewardModel const& getRewardModel(uint_fast64_t index) const;
             
+            /*!
+             * Checks whether the program has a label with the given name.
+             *
+             * @param labelName The label of the program.
+             * @return True iff the label of the program.
+             */
+            bool hasLabel(std::string const& labelName) const;
+            
             /*!
              * Retrieves all labels that are defined by the probabilitic program.
              *