Merged master in parametricSystems.

Former-commit-id: 2fb547b6f9

src/modelchecker/propositional/SparsePropositionalModelChecker.cpp

@@ -18,6 +18,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()) {

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;
             

src/models/AbstractModel.h

@@ -12,7 +12,11 @@
 #include "src/storage/Scheduler.h"
 #include "src/storage/StronglyConnectedComponentDecomposition.h"
 #include "src/utility/ConstantsComparator.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 {
@@ -345,6 +349,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

src/stormParametric.cpp

@@ -160,6 +160,10 @@ void check() {
     std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now();
     std::cout << "Parsing and translating the model took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl;
     
+    if (model->hasTransitionRewards()) {
+        model->convertTransitionRewardsToStateRewards();
+    }
+    
     std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>();
         
     storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc);

src/utility/cli.h

@@ -292,6 +292,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();