From 95b2c829f1658f799329e39cd77ebb0bf7c77e17 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Fri, 24 Jan 2020 18:25:42 +0100
Subject: [PATCH] introduced observation labels in prism

---
 src/storm/storage/prism/Label.cpp |  8 ++++++++
 src/storm/storage/prism/Label.h   | 32 +++++++++++++++++++++++++++++++
 2 files changed, 40 insertions(+)

diff --git a/src/storm/storage/prism/Label.cpp b/src/storm/storage/prism/Label.cpp
index 3475930c2..4f07baeb9 100644
--- a/src/storm/storage/prism/Label.cpp
+++ b/src/storm/storage/prism/Label.cpp
@@ -23,5 +23,13 @@ namespace storm {
             stream << "label \"" << label.getName() << "\" = " << label.getStatePredicateExpression() << ";";
             return stream;
         }
+
+        ObservationLabel::ObservationLabel(std::string const& name, storm::expressions::Expression const& statePredicateExpression, std::string const& filename, uint_fast64_t lineNumber) : Label(name, statePredicateExpression, filename, lineNumber) {
+            // Intentionally left empty.
+        }
+
+        ObservationLabel ObservationLabel::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+            return ObservationLabel(this->getName(), this->getStatePredicateExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
+        }
     } // namespace prism
 } // namespace storm
diff --git a/src/storm/storage/prism/Label.h b/src/storm/storage/prism/Label.h
index eb07e7013..298e5b721 100644
--- a/src/storm/storage/prism/Label.h
+++ b/src/storm/storage/prism/Label.h
@@ -68,6 +68,38 @@ namespace storm {
             // A predicate that needs to be satisfied by states for the label to be attached.
             storm::expressions::Expression statePredicateExpression;
         };
+
+        class ObservationLabel : public Label {
+        public:
+            /*!
+             * Creates a label with the given name and state predicate expression.
+             *
+             * @param name The name of the label.
+             * @param statePredicateExpression The predicate that needs to hold before taking a transition with the previously
+             * specified name in order to obtain the reward.
+             * @param filename The filename in which the transition reward is defined.
+             * @param lineNumber The line number in which the transition reward is defined.
+             */
+            ObservationLabel(std::string const& name, storm::expressions::Expression const& statePredicateExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+
+            // Create default implementations of constructors/assignment.
+            ObservationLabel() = default;
+            ObservationLabel(ObservationLabel const& other) = default;
+            ObservationLabel& operator=(ObservationLabel const& other)= default;
+            ObservationLabel(ObservationLabel&& other) = default;
+            ObservationLabel& operator=(ObservationLabel&& other) = default;
+
+            /*!
+            * Substitutes all identifiers in the expression of the label according to the given map.
+            *
+            * @param substitution The substitution to perform.
+            * @return The resulting label.
+            */
+            ObservationLabel substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
+
+        };
+
+
     } // namespace prism
 } // namespace storm