From cc7d44dd157ea3c59d2b3831dee72e1813e81d2a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 29 Jan 2015 21:19:49 +0100
Subject: [PATCH 1/2] Added proper canHandle method to propositional model
 checker.

Former-commit-id: 4af714e31a33e6c967823915f6d00027f1005537
---
 .../propositional/SparsePropositionalModelChecker.cpp        | 5 +++++
 .../propositional/SparsePropositionalModelChecker.h          | 1 +
 2 files changed, 6 insertions(+)

diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
index 565546adf..aa8c4e058 100644
--- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
+++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
@@ -15,6 +15,11 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        template<typename ValueType>
+        bool SparsePropositionalModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const {
+            return formula.isPropositionalFormula();
+        }
+        
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparsePropositionalModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
             if (stateFormula.isTrueFormula()) {
diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.h b/src/modelchecker/propositional/SparsePropositionalModelChecker.h
index c6309e4f0..d3a9011ce 100644
--- a/src/modelchecker/propositional/SparsePropositionalModelChecker.h
+++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.h
@@ -14,6 +14,7 @@ namespace storm {
             explicit SparsePropositionalModelChecker(storm::models::AbstractModel<ValueType> const& model);
             
             // The implemented methods of the AbstractModelChecker interface.
+            virtual bool canHandle(storm::logic::Formula const& formula) const override;
             virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
             virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
             

From 9cf82bcd98ff23c9c63c54a615b3468a76c9f4ed Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 30 Jan 2015 10:59:11 +0100
Subject: [PATCH 2/2] Added conversion from transition-based rewards to
 state-based rewards to enable proper treatment in bisimulation minimization

Former-commit-id: d0c31094bdc5d781b070e91c743416ca7b40fa73
---
 src/models/AbstractModel.h | 13 +++++++++++++
 src/utility/cli.h          |  4 ++++
 2 files changed, 17 insertions(+)

diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index b115e2551..76efcdb07 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -11,7 +11,11 @@
 #include "src/storage/SparseMatrix.h"
 #include "src/storage/Scheduler.h"
 #include "src/storage/StronglyConnectedComponentDecomposition.h"
+#include "src/utility/macros.h"
 #include "src/utility/Hash.h"
+#include "src/utility/vector.h"
+
+#include "src/exceptions/InvalidOperationException.h"
 
 namespace storm {
 namespace models {
@@ -329,6 +333,15 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
             return static_cast<bool>(choiceLabeling);
         }
 
+    void convertTransitionRewardsToStateRewards() {
+        STORM_LOG_THROW(this->hasTransitionRewards(), storm::exceptions::InvalidOperationException, "Cannot reduce non-existant transition rewards to state rewards.");
+        if (this->hasStateRewards()) {
+            storm::utility::vector::addVectorsInPlace(stateRewardVector.get(), transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get()));
+        } else {
+            this->stateRewardVector = transitionMatrix.getPointwiseProductRowSumVector(transitionRewardMatrix.get());
+        }
+    }
+    
 		/*!
 		 * Retrieves the size of the internal representation of the model in memory.
 		 * @return the size of the internal representation of the model in memory
diff --git a/src/utility/cli.h b/src/utility/cli.h
index de987e365..07fb2fbd5 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -288,6 +288,10 @@ namespace storm {
                     STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs.");
                     std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->template as<storm::models::Dtmc<double>>();
                     
+                    if (dtmc->hasTransitionRewards()) {
+                        dtmc->convertTransitionRewardsToStateRewards();
+                    }
+                    
                     std::cout << "Performing bisimulation minimization... ";
                     storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, boost::optional<std::set<std::string>>(), true, storm::settings::bisimulationSettings().isWeakBisimulationSet(), true);
                     model = bisimulationDecomposition.getQuotient();