From 4d74ec501adbb8c0515a836db2d75f18a02f3f3b Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 19 Sep 2018 08:55:56 +0200
Subject: [PATCH] substitute formulas in properties after parsing

---
 src/storm-parsers/api/properties.cpp       | 2 +-
 src/storm-parsers/parser/FormulaParser.cpp | 9 ---------
 src/storm/storage/prism/Program.cpp        | 8 ++++++++
 src/storm/storage/prism/Program.h          | 7 +++++++
 4 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/src/storm-parsers/api/properties.cpp b/src/storm-parsers/api/properties.cpp
index 68b68e990..b4108b805 100644
--- a/src/storm-parsers/api/properties.cpp
+++ b/src/storm-parsers/api/properties.cpp
@@ -58,7 +58,7 @@ namespace storm {
         std::vector <storm::jani::Property> parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional <std::set<std::string>> const &propertyFilter) {
             storm::parser::FormulaParser formulaParser(program);
             auto formulas = parseProperties(formulaParser, inputString, propertyFilter);
-            return substituteConstantsInProperties(formulas, program.getConstantsSubstitution());
+            return substituteConstantsInProperties(formulas, program.getConstantsFormulasSubstitution());
         }
 
         std::vector <storm::jani::Property> parsePropertiesForSymbolicModelDescription(std::string const &inputString, storm::storage::SymbolicModelDescription const &modelDescription, boost::optional <std::set<std::string>> const &propertyFilter) {
diff --git a/src/storm-parsers/parser/FormulaParser.cpp b/src/storm-parsers/parser/FormulaParser.cpp
index 0f44d469b..78cf2ad3c 100644
--- a/src/storm-parsers/parser/FormulaParser.cpp
+++ b/src/storm-parsers/parser/FormulaParser.cpp
@@ -32,20 +32,11 @@ namespace storm {
         }
 
         FormulaParser::FormulaParser(storm::prism::Program const& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(program.getManager().getSharedPointer())) {
-            this->addFormulasAsIdentifiers(program);
         }
 
         FormulaParser::FormulaParser(storm::prism::Program& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(program.getManager().getSharedPointer())) {
-            this->addFormulasAsIdentifiers(program);
         }
 
-        void FormulaParser::addFormulasAsIdentifiers(storm::prism::Program const& program) {
-            // Make the formulas of the program available to the parser.
-            for (auto const& formula : program.getFormulas()) {
-                this->addIdentifierExpression(formula.getName(), formula.getExpression());
-            }
-        }
-        
         FormulaParser::FormulaParser(FormulaParser const& other) : FormulaParser(other.manager) {
             other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); });
         }
diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index 67e822ab3..c89da44fe 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -333,6 +333,14 @@ namespace storm {
             return constantsSubstitution;
         }
         
+        std::map<storm::expressions::Variable, storm::expressions::Expression> Program::getConstantsFormulasSubstitution() const {
+            auto result = getConstantsSubstitution();
+            for (auto const& formula : this->getFormulas()) {
+                result.emplace(formula.getExpressionVariable(), formula.getExpression());
+            }
+            return result;
+        }
+        
         std::size_t Program::getNumberOfConstants() const {
             return this->getConstants().size();
         }
diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h
index aaefada9e..151388cbb 100644
--- a/src/storm/storage/prism/Program.h
+++ b/src/storm/storage/prism/Program.h
@@ -138,6 +138,13 @@ namespace storm {
              */
             std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsSubstitution() const;
             
+            /*!
+             * Retrieves a mapping of all defined constants and formula variables to their defining expressions
+             *
+             * @return A mapping from constants and formulas to their expressions.
+             */
+            std::map<storm::expressions::Variable, storm::expressions::Expression> getConstantsFormulasSubstitution() const;
+            
             /*!
              * Retrieves all constants defined in the program.
              *