started working on the github issues by Linda

src/storm-parsers/parser/FormulaParserGrammar.cpp

@@ -133,7 +133,7 @@ namespace storm {
             formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":");
             formulaName.name("formula name");
             
-            constantDefinition = (qi::lit("const") > qi::eps[qi::_a = true] > -(qi::lit("int") | qi::lit("double")[qi::_a = false]) >> identifier)[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a)];
+            constantDefinition = (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] | qi::lit("double")[qi::_a = ConstantDataType::Rational]) >> identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)];
             constantDefinition.name("constant definition");
             
 #pragma clang diagnostic push
@@ -208,16 +208,25 @@ namespace storm {
             this->identifiers_.add(identifier, expression);
         }
         
-        void FormulaParserGrammar::addConstant(std::string const& name, bool integer) {
+        void FormulaParserGrammar::addConstant(std::string const& name, ConstantDataType type, boost::optional<storm::expressions::Expression> const& expression) {
             STORM_LOG_ASSERT(manager, "Mutable expression manager required to define new constants.");
             storm::expressions::Variable newVariable;
-            if (integer) {
+            STORM_LOG_THROW(!manager->hasVariable(name), storm::exceptions::WrongFormatException, "Invalid constant definition '" << name << "' in property: variable already exists.");
+            
+            if (type == ConstantDataType::Bool) {
+                newVariable = manager->declareBooleanVariable(name);
+            } else if (type == ConstantDataType::Integer)  {
                 newVariable = manager->declareIntegerVariable(name);
             } else {
                 newVariable = manager->declareRationalVariable(name);
             }
+            
+            if (expression) {
+                addIdentifierExpression(name, expression.get());
+            } else {
                 addIdentifierExpression(name, newVariable);
             }
+        }
         
         bool FormulaParserGrammar::areConstantDefinitionsAllowed() const {
             return static_cast<bool>(manager);

src/storm-parsers/parser/FormulaParserGrammar.h

@@ -145,7 +145,11 @@ namespace storm {
             
             qi::rule<Iterator, std::vector<storm::jani::Property>(), Skipper> start;
             
-            qi::rule<Iterator, qi::unused_type(), qi::locals<bool>, Skipper> constantDefinition;
+            enum class ConstantDataType {
+                Bool, Integer, Rational
+            };
+            
+            qi::rule<Iterator, qi::unused_type(), qi::locals<ConstantDataType>, Skipper> constantDefinition;
             qi::rule<Iterator, std::string(), Skipper> identifier;
             qi::rule<Iterator, std::string(), Skipper> formulaName;
             
@@ -197,7 +201,7 @@ namespace storm {
             boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
 
             bool areConstantDefinitionsAllowed() const;
-            void addConstant(std::string const& name, bool integer);
+            void addConstant(std::string const& name, ConstantDataType type, boost::optional<storm::expressions::Expression> const& expression);
             void addProperty(std::vector<storm::jani::Property>& properties, boost::optional<std::string> const& name, std::shared_ptr<storm::logic::Formula const> const& formula);
 
             std::shared_ptr<storm::logic::TimeBoundReference> createTimeBoundReference(storm::logic::TimeBoundType const& type, boost::optional<std::string> const& rewardModelName) const;

src/storm/api/properties.cpp

@@ -13,7 +13,6 @@
 namespace storm {
     namespace api {
 
-        
         std::vector<storm::jani::Property> substituteConstantsInProperties(std::vector<storm::jani::Property> const& properties, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
             std::vector<storm::jani::Property> preprocessedProperties;
             for (auto const& property : properties) {
@@ -58,5 +57,6 @@ namespace storm {
             }
             return formulas;
         }
+        
     }
 }

src/storm/logic/AtomicExpressionFormula.cpp

@@ -24,6 +24,10 @@ namespace storm {
             atomicExpressionFormulas.push_back(std::dynamic_pointer_cast<AtomicExpressionFormula const>(this->shared_from_this()));
         }
         
+        void AtomicExpressionFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+            expression.gatherVariables(usedVariables);
+        }
+        
         std::ostream& AtomicExpressionFormula::writeToStream(std::ostream& out) const {
             out << expression;
             return out;

src/storm/logic/AtomicExpressionFormula.h

@@ -22,6 +22,7 @@ namespace storm {
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
 
         private:
             // The atomic expression represented by this node in the formula tree.

src/storm/logic/BinaryPathFormula.cpp

@@ -33,6 +33,11 @@ namespace storm {
             this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels);
         }
         
+        void BinaryPathFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+            this->getLeftSubformula().gatherUsedVariables(usedVariables);
+            this->getRightSubformula().gatherUsedVariables(usedVariables);
+        }
+        
         bool BinaryPathFormula::hasQualitativeResult() const {
             return false;
         }

src/storm/logic/BinaryPathFormula.h

@@ -23,6 +23,7 @@ namespace storm {
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
 
             virtual bool hasQualitativeResult() const override;
             virtual bool hasQuantitativeResult() const override;

src/storm/logic/BinaryStateFormula.cpp

@@ -32,5 +32,10 @@ namespace storm {
             this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels);
             this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels);
         }
+        
+        void BinaryStateFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+            this->getLeftSubformula().gatherUsedVariables(usedVariables);
+            this->getRightSubformula().gatherUsedVariables(usedVariables);
+        }
     }
 }

src/storm/logic/BinaryStateFormula.h

@@ -21,6 +21,7 @@ namespace storm {
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
 
         private:
             std::shared_ptr<Formula const> leftSubformula;

src/storm/logic/BoundedUntilFormula.cpp

@@ -84,6 +84,22 @@ namespace storm {
             }
         }
         
+        void BoundedUntilFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+            if (hasMultiDimensionalSubformulas()) {
+                for (unsigned i = 0; i < this->getDimension(); ++i) {
+                    this->getLeftSubformula(i).gatherUsedVariables(usedVariables);
+                    this->getRightSubformula(i).gatherUsedVariables(usedVariables);
+                    this->getLowerBound(i).gatherVariables(usedVariables);
+                    this->getUpperBound(i).gatherVariables(usedVariables);
+                }
+            } else {
+                this->getLeftSubformula().gatherUsedVariables(usedVariables);
+                this->getRightSubformula().gatherUsedVariables(usedVariables);
+                this->getLowerBound().gatherVariables(usedVariables);
+                this->getUpperBound().gatherVariables(usedVariables);
+            }
+        }
+        
         bool BoundedUntilFormula::hasQualitativeResult() const {
             return false;
         }

src/storm/logic/BoundedUntilFormula.h

@@ -24,6 +24,7 @@ namespace storm {
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
 
             virtual bool hasQualitativeResult() const override;
             virtual bool hasQuantitativeResult() const override;

src/storm/logic/ConditionalFormula.cpp

@@ -49,6 +49,11 @@ namespace storm {
             this->getConditionFormula().gatherReferencedRewardModels(referencedRewardModels);
         }
         
+        void ConditionalFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+            this->getSubformula().gatherUsedVariables(usedVariables);
+            this->getConditionFormula().gatherUsedVariables(usedVariables);
+        }
+        
         bool ConditionalFormula::hasQualitativeResult() const {
             return false;
         }

src/storm/logic/ConditionalFormula.h

@@ -28,6 +28,7 @@ namespace storm {
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
 
             virtual bool hasQualitativeResult() const override;
             virtual bool hasQuantitativeResult() const override;

src/storm/logic/CumulativeRewardFormula.cpp

@@ -47,6 +47,12 @@ namespace storm {
             }
         }
         
+        void CumulativeRewardFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+            for (unsigned i = 0; i < this->getDimension(); ++i) {
+                this->getBound(i).gatherVariables(usedVariables);
+            }
+        }
+        
         TimeBoundReference const& CumulativeRewardFormula::getTimeBoundReference() const {
             STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
             return getTimeBoundReference(0);

src/storm/logic/CumulativeRewardFormula.h

@@ -24,6 +24,7 @@ namespace storm {
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
 
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
 
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             

src/storm/logic/Formula.cpp

@@ -431,6 +431,12 @@ namespace storm {
             return result;
         }
         
+        std::set<storm::expressions::Variable> Formula::getUsedVariables() const {
+            std::set<storm::expressions::Variable> usedVariables;
+            this->gatherUsedVariables(usedVariables);
+            return usedVariables;
+        }
+        
         std::set<std::string> Formula::getReferencedRewardModels() const {
             std::set<std::string> referencedRewardModels;
             this->gatherReferencedRewardModels(referencedRewardModels);
@@ -481,6 +487,10 @@ namespace storm {
             return;
         }
         
+        void Formula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+            return;
+        }
+        
         std::string Formula::toString() const {
             std::stringstream str2;
             writeToStream(str2);

src/storm/logic/Formula.h

@@ -192,6 +192,7 @@ namespace storm {
             
             std::vector<std::shared_ptr<AtomicExpressionFormula const>> getAtomicExpressionFormulas() const;
             std::vector<std::shared_ptr<AtomicLabelFormula const>> getAtomicLabelFormulas() const;
+            std::set<storm::expressions::Variable> getUsedVariables() const;
             std::set<std::string> getReferencedRewardModels() const;
             
             std::shared_ptr<Formula const> asSharedPointer();
@@ -218,6 +219,7 @@ namespace storm {
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const;
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const;
+            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const;
 
         private:
             // Currently empty.

src/storm/logic/InstantaneousRewardFormula.cpp

@@ -60,6 +60,10 @@ namespace storm {
             return value;
         }
         
+        void InstantaneousRewardFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+            this->getBound().gatherVariables(usedVariables);
+        }
+        
         void InstantaneousRewardFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) {
             STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-instant '" << bound << "' as it contains undefined constants.");
         }

src/storm/logic/InstantaneousRewardFormula.h

@@ -35,6 +35,8 @@ namespace storm {
             template <typename ValueType>
             ValueType getBound() const;
             
+            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
+            
         private:
             static void checkNoVariablesInBound(storm::expressions::Expression const& bound);
 

src/storm/logic/OperatorFormula.cpp

@@ -85,6 +85,10 @@ namespace storm {
             return !this->hasBound();
         }
         
+        void OperatorFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+            this->getThreshold().gatherVariables(usedVariables);
+        }
+        
         std::ostream& OperatorFormula::writeToStream(std::ostream& out) const {
             if (hasOptimalityType()) {
                 out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max");

src/storm/logic/OperatorFormula.h

@@ -49,6 +49,8 @@ namespace storm {
             virtual bool hasQualitativeResult() const override;
             virtual bool hasQuantitativeResult() const override;
             
+            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
+            
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
         protected:

src/storm/logic/UnaryPathFormula.cpp

@@ -26,6 +26,10 @@ namespace storm {
             this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
         }
         
+        void UnaryPathFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+            this->getSubformula().gatherUsedVariables(usedVariables);
+        }
+        
         bool UnaryPathFormula::hasQualitativeResult() const {
             return false;
         }

src/storm/logic/UnaryPathFormula.h

@@ -22,6 +22,7 @@ namespace storm {
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
 
             virtual bool hasQualitativeResult() const override;
             virtual bool hasQuantitativeResult() const override;

src/storm/logic/UnaryStateFormula.cpp

@@ -28,5 +28,9 @@ namespace storm {
             this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
         }
         
+        void UnaryStateFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+            this->getSubformula().gatherUsedVariables(usedVariables);
+        }
+
     }
 }

src/storm/logic/UnaryStateFormula.h

@@ -20,6 +20,7 @@ namespace storm {
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
 
         private:
             std::shared_ptr<Formula const> subformula;

src/storm/storage/expressions/Expression.cpp

@@ -127,6 +127,10 @@ namespace storm {
             return result;
 		}
         
+        void Expression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
+            this->getBaseExpression().gatherVariables(variables);
+        }
+        
         bool Expression::containsVariable(std::set<storm::expressions::Variable> const& variables) const {
             std::set<storm::expressions::Variable> appearingVariables = this->getVariables();
             std::set<storm::expressions::Variable> intersection;

src/storm/storage/expressions/Expression.h

@@ -262,6 +262,14 @@ namespace storm {
              */
             std::set<storm::expressions::Variable> getVariables() const;
 
+            /*!
+             * Retrieves the set of all variables that appear in the expression. These variables are added to the given
+             * set.
+             *
+             * @param variables The set to which to add the variables.
+             */
+            void gatherVariables(std::set<storm::expressions::Variable>& variables) const;
+            
             /*!
              * Retrieves whether the expression contains any of the given variables.
              *