From 55999036d6b09a331295247b82cee1fe945f5a03 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 9 Sep 2020 11:54:21 +0200
Subject: [PATCH 1/4] Fixed warning

---
 src/storm/utility/shortestPaths.h | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/storm/utility/shortestPaths.h b/src/storm/utility/shortestPaths.h
index 60b206bca..ab3396a3f 100644
--- a/src/storm/utility/shortestPaths.h
+++ b/src/storm/utility/shortestPaths.h
@@ -47,7 +47,7 @@ namespace storm {
                     if (predecessorNode != rhs.predecessorNode) {
                         return predecessorNode < rhs.predecessorNode;
                     }
-                    return predecessorK < predecessorK;
+                    return predecessorK < rhs.predecessorK;
                 }
 
                 bool operator==(const Path<T>& rhs) const {

From 825454d4827c6597ae0d542b63a096de7866ec42 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 9 Sep 2020 14:52:36 +0200
Subject: [PATCH 2/4] Fixed warning

---
 src/storm/storage/jani/TemplateEdgeContainer.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/storm/storage/jani/TemplateEdgeContainer.cpp b/src/storm/storage/jani/TemplateEdgeContainer.cpp
index 81ce8f874..ee83d9f6a 100644
--- a/src/storm/storage/jani/TemplateEdgeContainer.cpp
+++ b/src/storm/storage/jani/TemplateEdgeContainer.cpp
@@ -3,10 +3,10 @@
 
 namespace storm {
     namespace jani {
-        TemplateEdgeContainer::TemplateEdgeContainer(TemplateEdgeContainer const &other) {
+        TemplateEdgeContainer::TemplateEdgeContainer(TemplateEdgeContainer const &other) : std::unordered_set<std::shared_ptr<TemplateEdge>>() {
             for (auto const& te : other) {
                 this->insert(std::make_shared<TemplateEdge>(*te));
             }
         }
     }
-}
\ No newline at end of file
+}

From 0e544a4c13dc48f7fb914e6654d9c651b24face1 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 9 Sep 2020 10:38:52 +0200
Subject: [PATCH 3/4] Enabled TimeOperatorFormulas for multi-objective model
 checking of MDPs.

---
 .../SparseMultiObjectivePreprocessor.cpp             | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
index 294a598ae..9f253bc38 100644
--- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
+++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
@@ -343,8 +343,6 @@ namespace storm {
     
                 template<typename SparseModelType>
                 void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) {
-                    // Time formulas are only supported for Markov automata
-                    STORM_LOG_THROW(data.model->isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata.");
                     
                     data.objectives.back()->lowerResultBound = storm::utility::zero<ValueType>();
                     
@@ -474,11 +472,15 @@ namespace storm {
                                 }
                             }
                             data.model->addRewardModel(rewardModelName, std::move(objectiveRewards));
-                        } else if (formula.isReachabilityTimeFormula() && data.model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                        } else if (formula.isReachabilityTimeFormula()) {
                             
-                            // build stateAction reward vector that only gives reward for relevant states
+                            // build state reward vector that only gives reward for relevant states
                             std::vector<typename SparseModelType::ValueType> timeRewards(data.model->getNumberOfStates(), storm::utility::zero<typename SparseModelType::ValueType>());
-                            storm::utility::vector::setVectorValues(timeRewards, dynamic_cast<storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType> const&>(*data.model).getMarkovianStates() & reachableFromInit, storm::utility::one<typename SparseModelType::ValueType>());
+                            if (data.model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                                storm::utility::vector::setVectorValues(timeRewards, dynamic_cast<storm::models::sparse::MarkovAutomaton<typename SparseModelType::ValueType> const&>(*data.model).getMarkovianStates() & reachableFromInit, storm::utility::one<typename SparseModelType::ValueType>());
+                            } else {
+                                storm::utility::vector::setVectorValues(timeRewards, reachableFromInit, storm::utility::one<typename SparseModelType::ValueType>());
+                            }
                             data.model->addRewardModel(rewardModelName, typename SparseModelType::RewardModelType(std::move(timeRewards)));
                         } else {
                             STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (data.model->isOfType(storm::models::ModelType::MarkovAutomaton) ?  "nor reachability time" : "") << ". This is not supported.");

From 33a6687721b3d79d7dae82ac29588152f7256e42 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 9 Sep 2020 16:00:46 +0200
Subject: [PATCH 4/4] Fixed deprecated operator= warnings

---
 src/storm/storage/jani/EdgeContainer.cpp         | 9 ++++++---
 src/storm/storage/jani/EdgeContainer.h           | 1 +
 src/storm/storage/jani/TemplateEdgeContainer.cpp | 8 ++++++++
 src/storm/storage/jani/TemplateEdgeContainer.h   | 1 +
 4 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/storm/storage/jani/EdgeContainer.cpp b/src/storm/storage/jani/EdgeContainer.cpp
index f2e3b9855..92e17afbc 100644
--- a/src/storm/storage/jani/EdgeContainer.cpp
+++ b/src/storm/storage/jani/EdgeContainer.cpp
@@ -67,9 +67,12 @@ namespace storm {
                     e.setTemplateEdge(map[e.getTemplateEdge()]);
                 }
             }
-
-
-
+        }
+        
+        EdgeContainer& EdgeContainer::operator=(EdgeContainer const& other) {
+            EdgeContainer otherCpy(other);
+            this->templates = std::move(other.templates);
+            this->edges = std::move(other.edges);
         }
 
         void EdgeContainer::finalize(Model const& containingModel) {
diff --git a/src/storm/storage/jani/EdgeContainer.h b/src/storm/storage/jani/EdgeContainer.h
index bf1e0cbe9..dc2cb8b69 100644
--- a/src/storm/storage/jani/EdgeContainer.h
+++ b/src/storm/storage/jani/EdgeContainer.h
@@ -91,6 +91,7 @@ namespace storm {
 
             EdgeContainer() = default;
             EdgeContainer(EdgeContainer const& other);
+            EdgeContainer& operator=(EdgeContainer const& other);
 
             void clearConcreteEdges();
             std::vector<Edge> const& getConcreteEdges() const;
diff --git a/src/storm/storage/jani/TemplateEdgeContainer.cpp b/src/storm/storage/jani/TemplateEdgeContainer.cpp
index ee83d9f6a..66d93a4fb 100644
--- a/src/storm/storage/jani/TemplateEdgeContainer.cpp
+++ b/src/storm/storage/jani/TemplateEdgeContainer.cpp
@@ -8,5 +8,13 @@ namespace storm {
                 this->insert(std::make_shared<TemplateEdge>(*te));
             }
         }
+        
+        TemplateEdgeContainer& TemplateEdgeContainer::operator=(const TemplateEdgeContainer& other) {
+            this->clear();
+            for (auto const& te : other) {
+                this->insert(std::make_shared<TemplateEdge>(*te));
+            }
+            return *this;
+        }
     }
 }
diff --git a/src/storm/storage/jani/TemplateEdgeContainer.h b/src/storm/storage/jani/TemplateEdgeContainer.h
index 293302594..12dd6050f 100644
--- a/src/storm/storage/jani/TemplateEdgeContainer.h
+++ b/src/storm/storage/jani/TemplateEdgeContainer.h
@@ -11,6 +11,7 @@ namespace storm {
         struct TemplateEdgeContainer : public std::unordered_set<std::shared_ptr<TemplateEdge>>   {
             TemplateEdgeContainer() = default;
             TemplateEdgeContainer(TemplateEdgeContainer const& other);
+            TemplateEdgeContainer& operator=(TemplateEdgeContainer const& other);
         };
     }
 }
\ No newline at end of file