eliminate reward accumulations whenever possible

src/storm-cli-utilities/model-handling.h

@@ -18,10 +18,12 @@
 
 #include "storm/storage/SymbolicModelDescription.h"
 #include "storm/storage/jani/Property.h"
+#include "storm/logic/RewardAccumulationEliminationVisitor.h"
 
 #include "storm/models/ModelBase.h"
 
 #include "storm/exceptions/OptionParserException.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
 
@@ -382,6 +384,7 @@ namespace storm {
             
             std::pair<std::shared_ptr<storm::models::ModelBase>, bool> result = std::make_pair(model, false);
             if (model->isSparseModel()) {
+                STORM_LOG_THROW((std::is_same<BuildValueType, ExportValueType>::value), storm::exceptions::UnexpectedException, "Build-Value Type and ExportValueType should be the same in the sparse engine.");
                 result = preprocessSparseModel<BuildValueType>(result.first->as<storm::models::sparse::Model<BuildValueType>>(), input);
             } else {
                 STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
@@ -396,6 +399,29 @@ namespace storm {
             return result;
         }
         
+        template <typename ModelType>
+        storm::jani::Property preprocessProperty(std::shared_ptr<ModelType> const& model, storm::jani::Property const& property) {
+            storm::logic::RewardAccumulationEliminationVisitor<typename ModelType::RewardModelType> v(model->getRewardModels(), model->getType());
+            auto formula = v.eliminateRewardAccumulations(*property.getFilter().getFormula());
+            auto states = v.eliminateRewardAccumulations(*property.getFilter().getStatesFormula());
+            storm::jani::FilterExpression fe(formula, property.getFilter().getFilterType(), states);
+            return storm::jani::Property(property.getName(), fe, property.getComment());
+        }
+        
+        template <storm::dd::DdType DdType, typename ValueType>
+        std::vector<storm::jani::Property> preprocessProperties(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input) {
+            std::vector<storm::jani::Property> resultProperties;
+            for (auto const& property : input.properties) {
+                if (model->isSparseModel()) {
+                    resultProperties.push_back(preprocessProperty(model->as<storm::models::sparse::Model<ValueType>>(), property));
+                } else {
+                    STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type.");
+                    resultProperties.push_back(preprocessProperty(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), property));
+                }
+            }
+            return resultProperties;
+        }
+        
         void printComputingCounterexample(storm::jani::Property const& property) {
             STORM_PRINT("Computing counterexample for property " << *property.getRawFormula() << " ..." << std::endl);
         }
@@ -670,7 +696,7 @@ namespace storm {
         }
         
         template <storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
-        std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) {
+        std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput& input, storm::settings::modules::CoreSettings::Engine engine) {
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
             auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             std::shared_ptr<storm::models::ModelBase> model;
@@ -690,6 +716,9 @@ namespace storm {
                     model = preprocessingResult.first;
                     model->printModelInformationToStream(std::cout);
                 }
+                if (!input.properties.empty()) {
+                    input.properties = preprocessProperties<DdType, VerificationValueType>(model, input);
+                }
                 exportModel<DdType, BuildValueType>(model, input);
             }
             return model;
@@ -708,15 +737,16 @@ namespace storm {
             } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
                 verifyWithExplorationEngine<VerificationValueType>(input);
             } else {
-                std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, engine);
+                SymbolicInput preprocessedInput = input;
+                std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(preprocessedInput, engine);
 
                 if (model) {
                     if (coreSettings.isCounterexampleSet()) {
                         auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-                        generateCounterexamples<VerificationValueType>(model, input);
+                        generateCounterexamples<VerificationValueType>(model, preprocessedInput);
                     } else {
                         auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-                        verifyModel<DdType, VerificationValueType>(model, input, coreSettings);
+                        verifyModel<DdType, VerificationValueType>(model, preprocessedInput, coreSettings);
                     }
                 }
             }

src/storm/logic/CloneVisitor.cpp

@@ -123,8 +123,8 @@ namespace storm {
             return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation()));
         }
         
-        boost::any CloneVisitor::visit(TotalRewardFormula const&, boost::any const&) const {
-            return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>());
+        boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const&) const {
+            return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f));
         }
         
         boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {

src/storm/logic/RewardAccumulation.cpp

@@ -19,8 +19,8 @@ namespace storm {
             return exit;
         }
         
-        bool RewardAccumulation::implies(RewardAccumulation const& other) const {
-            return (!isStepsSet() || other.isStepsSet()) && (!isTimeSet() || other.isTimeSet()) && (!isExitSet() || other.isExitSet());
+        bool RewardAccumulation::isEmpty() const {
+            return !isStepsSet() && !isTimeSet() && !isExitSet();
         }
 
         std::ostream& operator<<(std::ostream& out, RewardAccumulation const& acc) {

src/storm/logic/RewardAccumulation.h

@@ -13,8 +13,9 @@ namespace storm {
             bool isTimeSet() const; // If set, state rewards are accumulated over time (assuming 0 time passes in discrete-time model states)
             bool isExitSet() const; // If set, state rewards are accumulated upon exiting the state
             
-            // Returns true, if every reward-type set in this RewardAccumulation is also set for the other RewardAccumulation
-            bool implies(RewardAccumulation const& other) const;
+            // Returns true iff accumulation for all types of reward is disabled.
+            bool isEmpty() const;
+            
         private:
             bool time, steps, exit;
         };

src/storm/logic/RewardAccumulationEliminationVisitor.cpp

@@ -0,0 +1,173 @@
+#include "storm/logic/RewardAccumulationEliminationVisitor.h"
+#include "storm/logic/Formulas.h"
+
+#include "storm/utility/macros.h"
+
+#include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+#include "storm/storage/dd/DdManager.h"
+#include "storm/storage/dd/Add.h"
+#include "storm/storage/dd/Bdd.h"
+
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/models/symbolic/StandardRewardModel.h"
+
+namespace storm {
+    namespace logic {
+
+        template <class RewardModelType>
+        RewardAccumulationEliminationVisitor<RewardModelType>::RewardAccumulationEliminationVisitor(std::unordered_map<std::string, RewardModelType> const& rewardModels, storm::models::ModelType const& modelType) : rewardModels(rewardModels) {
+            if (modelType == storm::models::ModelType::Dtmc || modelType == storm::models::ModelType::Mdp || modelType == storm::models::ModelType::S2pg) {
+                isDiscreteTimeModel = true;
+            } else if (modelType == storm::models::ModelType::Ctmc || modelType == storm::models::ModelType::MarkovAutomaton) {
+                isDiscreteTimeModel = false;
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unhandled model type " << modelType << ".");
+            }
+        }
+        
+        template <class RewardModelType>
+        std::shared_ptr<Formula> RewardAccumulationEliminationVisitor<RewardModelType>::eliminateRewardAccumulations(Formula const& f) const {
+            boost::any result = f.accept(*this, boost::any());
+            return boost::any_cast<std::shared_ptr<Formula>>(result);
+        }
+        
+        template <class RewardModelType>
+        boost::any RewardAccumulationEliminationVisitor<RewardModelType>::visit(BoundedUntilFormula const& f, boost::any const& data) const {
+            std::vector<boost::optional<TimeBound>> lowerBounds, upperBounds;
+            std::vector<TimeBoundReference> timeBoundReferences;
+            for (uint64_t i = 0; i < f.getDimension(); ++i) {
+                if (f.hasLowerBound(i)) {
+                    lowerBounds.emplace_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i)));
+                } else {
+                    lowerBounds.emplace_back();
+                }
+                if (f.hasUpperBound(i)) {
+                    upperBounds.emplace_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i)));
+                } else {
+                    upperBounds.emplace_back();
+                }
+                storm::logic::TimeBoundReference tbr = f.getTimeBoundReference(i);
+                if (tbr.hasRewardAccumulation() && canEliminate(tbr.getRewardAccumulation(), tbr.getRewardName())) {
+                    // Eliminate accumulation
+                    tbr = storm::logic::TimeBoundReference(tbr.getRewardName(), boost::none);
+                }
+                timeBoundReferences.push_back(std::move(tbr));
+            }
+            if (f.hasMultiDimensionalSubformulas()) {
+                std::vector<std::shared_ptr<Formula const>> leftSubformulas, rightSubformulas;
+                for (uint64_t i = 0; i < f.getDimension(); ++i) {
+                    leftSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula(i).accept(*this, data)));
+                    rightSubformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula(i).accept(*this, data)));
+                }
+                return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences));
+            } else {
+                std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
+                std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
+                return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, timeBoundReferences));
+            }
+        }
+        
+        template <class RewardModelType>
+        boost::any RewardAccumulationEliminationVisitor<RewardModelType>::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
+            boost::optional<storm::logic::RewardAccumulation> rewAcc;
+            STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator.");
+            auto rewName = boost::any_cast<boost::optional<std::string>>(data);
+            if (f.hasRewardAccumulation() && !canEliminate(f.getRewardAccumulation(), rewName)) {
+                rewAcc = f.getRewardAccumulation();
+            }
+
+            std::vector<TimeBound> bounds;
+            std::vector<TimeBoundReference> timeBoundReferences;
+            for (uint64_t i = 0; i < f.getDimension(); ++i) {
+                bounds.emplace_back(TimeBound(f.isBoundStrict(i), f.getBound(i)));
+                storm::logic::TimeBoundReference tbr = f.getTimeBoundReference(i);
+                if (tbr.hasRewardAccumulation() && canEliminate(tbr.getRewardAccumulation(), tbr.getRewardName())) {
+                    // Eliminate accumulation
+                    tbr = storm::logic::TimeBoundReference(tbr.getRewardName(), boost::none);
+                }
+                timeBoundReferences.push_back(std::move(tbr));
+            }
+            return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences, rewAcc));
+        }
+        
+        template <class RewardModelType>
+        boost::any RewardAccumulationEliminationVisitor<RewardModelType>::visit(EventuallyFormula const& f, boost::any const& data) const {
+           std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            if (f.hasRewardAccumulation()) {
+                if (f.isTimePathFormula()) {
+                    if (isDiscreteTimeModel && ((!f.getRewardAccumulation().isExitSet() && !f.getRewardAccumulation().isStepsSet()) || (f.getRewardAccumulation().isStepsSet() && f.getRewardAccumulation().isExitSet()))) {
+                        return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
+                    } else if (!isDiscreteTimeModel && (!f.getRewardAccumulation().isTimeSet() || f.getRewardAccumulation().isExitSet() || f.getRewardAccumulation().isStepsSet())) {
+                        return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
+                    }
+                } else if (f.isRewardPathFormula()) {
+                    STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator.");
+                    auto rewName = boost::any_cast<boost::optional<std::string>>(data);
+                    if (!canEliminate(f.getRewardAccumulation(), rewName)) {
+                        return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext(), f.getRewardAccumulation()));
+                    }
+                }
+            }
+            return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext()));
+        }
+        
+        template <class RewardModelType>
+        boost::any RewardAccumulationEliminationVisitor<RewardModelType>::visit(RewardOperatorFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, f.getOptionalRewardModelName()));
+            return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation()));
+        }
+        
+        template <class RewardModelType>
+        boost::any RewardAccumulationEliminationVisitor<RewardModelType>::visit(TotalRewardFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(!data.empty(), storm::exceptions::UnexpectedException, "Formula " << f << " does not seem to be a subformula of a reward operator.");
+            auto rewName = boost::any_cast<boost::optional<std::string>>(data);
+            if (f.hasRewardAccumulation() || canEliminate(f.getRewardAccumulation(), rewName)) {
+                return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>());
+            } else {
+                return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>(f.getRewardAccumulation()));
+            }
+        }
+        
+        template <class RewardModelType>
+        bool RewardAccumulationEliminationVisitor<RewardModelType>::canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const {
+            auto rewModelIt = rewardModels.end();
+            if (rewardModelName.is_initialized()){
+                rewModelIt = rewardModels.find(rewardModelName.get());
+                STORM_LOG_THROW(rewModelIt != rewardModels.end(), storm::exceptions::InvalidPropertyException, "Unable to find reward model with name " << rewardModelName.get());
+            } else if (rewardModels.size() == 1) {
+                rewModelIt = rewardModels.begin();
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Multiple reward models were defined but no reward model name was given for at least one property.");
+            }
+            RewardModelType const& rewardModel = rewModelIt->second;
+            if ((rewardModel.hasStateActionRewards() || rewardModel.hasTransitionRewards()) && !accumulation.isStepsSet()) {
+                return false;
+            }
+            if (rewardModel.hasStateRewards()) {
+                if (isDiscreteTimeModel) {
+                    if (!accumulation.isExitSet()) {
+                        return false;
+                    }
+                    // accumulating over time in discrete time models has no effect, i.e., the value of accumulation.isTimeSet() does not matter here.
+                } else {
+                    if (accumulation.isExitSet() || !accumulation.isTimeSet()) {
+                        return false;
+                    }
+                }
+            }
+            return true;
+        }
+        
+        template class RewardAccumulationEliminationVisitor<storm::models::sparse::StandardRewardModel<double>>;
+        template class RewardAccumulationEliminationVisitor<storm::models::sparse::StandardRewardModel<storm::RationalNumber>>;
+        template class RewardAccumulationEliminationVisitor<storm::models::sparse::StandardRewardModel<storm::RationalFunction>>;
+        template class RewardAccumulationEliminationVisitor<storm::models::sparse::StandardRewardModel<storm::Interval>>;
+        
+        template class RewardAccumulationEliminationVisitor<storm::models::symbolic::StandardRewardModel<storm::dd::DdType::CUDD, double>>;
+        template class RewardAccumulationEliminationVisitor<storm::models::symbolic::StandardRewardModel<storm::dd::DdType::Sylvan, double>>;
+        template class RewardAccumulationEliminationVisitor<storm::models::symbolic::StandardRewardModel<storm::dd::DdType::Sylvan, storm::RationalNumber>>;
+        template class RewardAccumulationEliminationVisitor<storm::models::symbolic::StandardRewardModel<storm::dd::DdType::Sylvan, storm::RationalFunction>>;
+
+    }
+}

src/storm/logic/RewardAccumulationEliminationVisitor.h

@@ -0,0 +1,39 @@
+#pragma once
+
+#include <unordered_map>
+#include <boost/optional.hpp>
+
+#include "storm/logic/CloneVisitor.h"
+#include "storm/logic/RewardAccumulation.h"
+#include "storm/models/ModelType.h"
+
+
+namespace storm {
+    namespace logic {
+        
+        template <class RewardModelType>
+        class RewardAccumulationEliminationVisitor : public CloneVisitor {
+        public:
+            RewardAccumulationEliminationVisitor(std::unordered_map<std::string, RewardModelType> const& rewardModels, storm::models::ModelType const& modelType);
+            
+            /*!
+             * Eliminates any reward accumulations of the formula, where the presence of the reward accumulation does not change the result of the formula
+             */
+            std::shared_ptr<Formula> eliminateRewardAccumulations(Formula const& f) const;
+           
+            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override;
+
+            
+        private:
+            bool canEliminate(storm::logic::RewardAccumulation const& accumulation, boost::optional<std::string> rewardModelName) const;
+            
+            std::unordered_map<std::string, RewardModelType> const& rewardModels;
+            bool isDiscreteTimeModel;
+        };
+        
+    }
+}