fixed correct parsing of prism formulas

src/storm-parsers/parser/PrismParser.cpp

@@ -431,8 +431,8 @@ namespace storm {
             // Only register formula in second run.
             // This is necessary because the resulting type of the formula is only known in the second run.
             // This prevents the parser from accepting formulas that depend on future formulas.
-            storm::expressions::Variable variable;
             if (this->secondRun) {
+                storm::expressions::Variable variable;
                 try {
                     if (expression.hasIntegerType()) {
                          variable = manager->declareIntegerVariable(formulaName);
@@ -450,8 +450,10 @@ namespace storm {
                         STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << formulaName << "'.");
                     }
                 }
+                return storm::prism::Formula(variable, expression, this->getFilename());
+            } else {
+                return storm::prism::Formula(formulaName, expression, this->getFilename());
             }
-            return storm::prism::Formula(variable, expression, this->getFilename());
         }
         
         storm::prism::Label PrismParser::createLabel(std::string const& labelName, storm::expressions::Expression expression) const {

src/storm/storage/prism/Formula.cpp

@@ -2,16 +2,24 @@
 
 namespace storm {
     namespace prism {
-        Formula::Formula(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), expression(expression) {
+        Formula::Formula(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(variable.getName()), variable(variable), expression(expression) {
+            // Intentionally left empty.
+        }
+        
+        Formula::Formula(std::string const& name, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(name), expression(expression) {
             // Intentionally left empty.
         }
         
         std::string const& Formula::getName() const {
-            return this->variable.getName();
+            return this->name;
+        }
+        
+        bool Formula::hasExpressionVariable() const {
+            return this->variable.is_initialized();
         }
         
         storm::expressions::Variable const& Formula::getExpressionVariable() const {
-            return this->variable;
+            return this->variable.get();
         }
         
         storm::expressions::Expression const& Formula::getExpression() const {
@@ -19,12 +27,16 @@ namespace storm {
         }
         
         storm::expressions::Type const& Formula::getType() const {
-            assert(this->getExpressionVariable().getType() ==  this->getExpression().getType());
+            assert(!hasExpressionVariable() || this->getExpressionVariable().getType() ==  this->getExpression().getType());
             return this->getExpressionVariable().getType();
         }
         
         Formula Formula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return Formula(this->getExpressionVariable(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
+            if (hasExpressionVariable()) {
+                return Formula(this->getExpressionVariable(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
+            } else {
+                return Formula(this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
+            }
         }
         
         std::ostream& operator<<(std::ostream& stream, Formula const& formula) {

src/storm/storage/prism/Formula.h

@@ -2,6 +2,7 @@
 #define STORM_STORAGE_PRISM_FORMULA_H_
 
 #include <map>
+#include <boost/optional.hpp>
 
 #include "storm/storage/prism/LocatedInformation.h"
 #include "storm/storage/expressions/Expression.h"
@@ -13,14 +14,24 @@ namespace storm {
         class Formula : public LocatedInformation {
         public:
             /*!
-             * Creates a formula with the given name and expression.
+             * Creates a formula with the given placeholder variable and expression.
              *
-             * @param placeholder The placeholder variable that is used in expressions to represent this formula.
+             * @param variable The placeholder variable that is used in expressions to represent this formula.
              * @param expression The expression associated with this formula.
              * @param filename The filename in which the transition reward is defined.
              * @param lineNumber The line number in which the transition reward is defined.
              */
             Formula(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+
+            /*!
+             * Creates a formula with the given name
+             *
+             * @param name the name of the formula.
+             * @param expression The expression associated with this formula.
+             * @param filename The filename in which the transition reward is defined.
+             * @param lineNumber The line number in which the transition reward is defined.
+             */
+            Formula(std::string const& name, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
             
             // Create default implementations of constructors/assignment.
             Formula() = default;
@@ -36,6 +47,12 @@ namespace storm {
              */
             std::string const& getName() const;
             
+            /*!
+             * Retrieves wheter a placeholder variable is used in expressions to represent this formula.
+             *
+             */
+            bool hasExpressionVariable() const;
+            
             /*!
              * Retrieves the placeholder variable that is used in expressions to represent this formula.
              *
@@ -69,7 +86,10 @@ namespace storm {
             
         private:
             // The name of the formula.
-            storm::expressions::Variable variable;
+            std::string name;
+            
+            // Expression variable that is used as a placeholder for this formula
+            boost::optional<storm::expressions::Variable> variable;
             
             // A predicate that needs to be satisfied by states for the label to be attached.
             storm::expressions::Expression expression;

src/storm/storage/prism/Program.cpp

@@ -1048,6 +1048,17 @@ namespace storm {
             std::set<storm::expressions::Variable> variablesAndConstants;
             std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
             
+            // Collect the formula placeholders and check formulas
+            for (auto const& formula : this->getFormulas()) {
+                std::set<storm::expressions::Variable> containedVariables = formula.getExpression().getVariables();
+                bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
+                STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers.");
+                if (formula.hasExpressionVariable()) {
+                    all.insert(formula.getExpressionVariable());
+                    variablesAndConstants.insert(formula.getExpressionVariable());
+                }
+            }
+            
             // Check the commands of the modules.
             bool hasProbabilisticCommand = false;
             bool hasMarkovianCommand = false;
@@ -1217,13 +1228,6 @@ namespace storm {
                 STORM_LOG_THROW(label.getStatePredicateExpression().hasBooleanType(), storm::exceptions::WrongFormatException, "Error in " << label.getFilename() << ", line " << label.getLineNumber() << ": label predicate must evaluate to type 'bool'.");
             }
             
-            // Check the formulas.
-            for (auto const& formula : this->getFormulas()) {
-                std::set<storm::expressions::Variable> containedVariables = formula.getExpression().getVariables();
-                bool isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedVariables.begin(), containedVariables.end());
-                STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << formula.getFilename() << ", line " << formula.getLineNumber() << ": formula expression refers to unknown identifiers.");
-            }
-            
             if(lvl >= Program::ValidityCheckLevel::READYFORPROCESSING) {
                 // We check for each global variable and each labeled command, whether there is at most one instance writing to that variable.
                 std::set<std::pair<std::string, std::string>> globalBVarsWrittenToByCommand;