transformer: Added functionality to also translate expected time formulas to expected rewards.

src/storm/api/transformation.h

@@ -13,21 +13,24 @@ namespace storm {
         
         /*!
          * Transforms the given continuous model to a discrete time model.
-         * If such a transformation does not preserve one of the given formulas, an error is issued.
+         * If such a transformation does not preserve one of the given formulas, a warning is issued.
          */
         template <typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteTimeSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+        std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>>  transformContinuousToDiscreteTimeSparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
             
             storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType> transformer;
             
-            for (auto const& formula : formulas) {
-                STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << ".");
+            std::string timeRewardName = "_time";
+            while(model->hasRewardModel(timeRewardName)) {
+                timeRewardName += "_";
             }
+            auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName)
+            STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties.");
             
             if (model->isOfType(storm::models::ModelType::Ctmc)) {
-                return transformer.transform(*model->template as<storm::models::sparse::Ctmc<ValueType>>());
+                return std::make_pair(transformer.transform(*model->template as<storm::models::sparse::Ctmc<ValueType>>()), newFormulas);
             } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
-                return transformer.transform(*model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
+                return std::make_pair(transformer.transform(*model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()), newFormulas);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model->getType() << " to a discrete time model is not supported");
             }
@@ -40,18 +43,21 @@ namespace storm {
          * If such a transformation does not preserve one of the given formulas, an error is issued.
          */
         template <typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model<ValueType>&& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+        std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> transformContinuousToDiscreteTimeSparseModel(storm::models::sparse::Model<ValueType>&& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
             
             storm::transformer::ContinuousToDiscreteTimeModelTransformer<ValueType> transformer;
             
-            for (auto const& formula : formulas) {
-                STORM_LOG_THROW(transformer.preservesFormula(*formula), storm::exceptions::InvalidOperationException, "Transformation to discrete time model does not preserve formula " << *formula << ".");
+             std::string timeRewardName = "_time";
+            while(model.hasRewardModel(timeRewardName)) {
+                timeRewardName += "_";
             }
-            
+            auto newFormulas = transformer.checkAndTransformFormulas(formulas, timeRewardName)
+            STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(), "Transformation of a " << model->getType() << " to a discrete time model does not preserve all properties.");
+           
             if (model.isOfType(storm::models::ModelType::Ctmc)) {
-                return transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>()));
+                return std::make_pair(transformer.transform(std::move(*model.template as<storm::models::sparse::Ctmc<ValueType>>())), newFormulas);
             } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) {
-                return transformer.transform(std::move(*model.template as<storm::models::sparse::MarkovAutomaton<ValueType>>()));
+                return std::make_pair(transformer.transform(std::move(*model.template as<storm::models::sparse::MarkovAutomaton<ValueType>>())), newFormulas);
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of a " << model.getType() << " to a discrete time model is not supported.");
             }

src/storm/logic/ExpectedTimeToExpectedRewardVisitor.cpp

@@ -0,0 +1,28 @@
+#include "storm/logic/ExpectedTimeToExpectedRewardVisitor.h"
+#include "storm/logic/Formulas.h"
+
+#include "storm/utility/macros.h"
+
+#include "storm/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace logic {
+
+        ExpectedTimeToExpectedRewardVisitor::ExpectedTimeToExpectedRewardVisitor(std::string const& timeRewardModelName) : timeRewardModelName(timeRewardModelName) {
+            // Intentionally left empty
+        }
+        
+        std::shared_ptr<Formula> ExpectedTimeToExpectedRewardVisitor::substitute(Formula const& f) const {
+            boost::any result = f.accept(*this, boost::any());
+            return boost::any_cast<std::shared_ptr<Formula>>(result);
+        }
+ 
+        boost::any ExpectedTimeToExpectedRewardVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(f.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected eventually formula within time operator. Got " << f << " instead.");
+            std::shared_ptr<Formula> subsubformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, data));
+            STORM_LOG_THROW(f.getSubformula().isReachabilityTimeFormula(), storm::exceptions::InvalidPropertyException, "Expected time path formula within time operator. Got " << f << " instead.");
+            std::shared_ptr<Formula> subformula = std::make_shared<EventuallyFormula>(subsubformula, storm::logic::FormulaContext::Reward);
+            return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, timeRewardModelName, f.getOperatorInformation()));
+        }
+    }
+}

src/storm/logic/ExpectedTimeToExpectedRewardVisitor.h

@@ -0,0 +1,25 @@
+#pragma once
+
+#include <map>
+
+#include "storm/logic/CloneVisitor.h"
+
+#include "storm/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace logic {
+        
+        class ExpectedTimeToExpectedRewardVisitor : public CloneVisitor {
+        public:
+            ExpectedTimeToExpectedRewardVisitor(std::string const& timeRewardModelName);
+            
+            std::shared_ptr<Formula> substitute(Formula const& f) const;
+            
+            virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
+
+        private:
+            std::string const& timeRewardModelName;
+        };
+        
+    }
+}

src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.cpp

@@ -5,7 +5,7 @@
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/logic/Formulas.h"
 #include "storm/logic/FragmentSpecification.h"
-#include "storm/logic/CloneVisitor.h"
+#include "storm/logic/ExpectedTimeToExpectedRewardVisitor.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
 
@@ -93,7 +93,22 @@ namespace storm {
             fragment.setReachabilityRewardFormulasAllowed(true);
             return formula.isInFragment(fragment);
         }
-        
+  
+        template <typename ValueType, typename RewardModelType>
+        std::vector<std::shared_ptr<storm::logic::Formula const>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::checkAndTransformFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& timeRewardName) {
+            std::vector<std::shared_ptr<storm::logic::Formula const>> result;
+            storm::logic::ExpectedTimeToExpectedRewardVisitor v(timeRewardName);
+            for (auto const& f : formulas) {
+                // Translate expected time formulas
+                auto newF = v.substitute(*f);
+                if(preservesFormula(*newF)) {
+                    result.push_back(newF);
+                } else {
+                    STORM_LOG_INFO("Continuous to discrete time transformation does not preserve formula " << *f);
+                }
+            }
+            return result;
+        }
   
         template <typename ValueType, typename RewardModelType>
         std::shared_ptr<storm::models::sparse::Mdp<ValueType, RewardModelType>> ContinuousToDiscreteTimeModelTransformer<ValueType, RewardModelType>::transform(storm::models::sparse::MarkovAutomaton<ValueType, RewardModelType> const& ma, boost::optional<std::string> const& timeRewardModelName) {

src/storm/transformer/ContinuousToDiscreteTimeModelTransformer.h

@@ -18,7 +18,13 @@ namespace storm {
 
             // If this method returns true, the given formula is preserced by the transformation
             static bool preservesFormula(storm::logic::Formula const& formula);
-        
+            
+            // Checks whether the given formulas are preserved.
+            // Expected time formulas are translated to expected reward formulas.
+            // The returned vector only contains formulas that are preserved by the transformation.
+            static std::vector<std::shared_ptr<storm::logic::Formula const>> checkAndTransformFormulas(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& timeRewardName);
+            
+            
             // Transforms the given CTMC to its underlying (aka embedded) DTMC.
             // A reward model for time is added if a corresponding reward model name is given
             static std::shared_ptr<storm::models::sparse::Dtmc<ValueType, RewardModelType>> transform(storm::models::sparse::Ctmc<ValueType, RewardModelType> const& ctmc, boost::optional<std::string> const& timeRewardModelName = boost::none);