better check whether transition rewards can be scaled and lifted to action rewards

src/storm/api/builder.h

@@ -110,7 +110,7 @@ namespace storm {
 
         template<typename ValueType>
         std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool jit = false, bool doctor = false) {
-            storm::builder::BuilderOptions options(formulas);
+            storm::builder::BuilderOptions options(formulas, model);
             return buildSparseModel<ValueType>(model, options, jit, doctor);
         }
         

src/storm/builder/BuilderOptions.cpp

@@ -1,7 +1,7 @@
 #include "storm/builder/BuilderOptions.h"
 
 #include "storm/logic/Formulas.h"
-#include "storm/logic/FragmentSpecification.h"
+#include "storm/logic/LiftableTransitionRewardsVisitor.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/BuildSettings.h"
@@ -42,15 +42,15 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        BuilderOptions::BuilderOptions(storm::logic::Formula const& formula) : BuilderOptions() {
-            this->preserveFormula(formula);
+        BuilderOptions::BuilderOptions(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription) : BuilderOptions() {
+            this->preserveFormula(formula, modelDescription);
             this->setTerminalStatesFromFormula(formula);
         }
         
-        BuilderOptions::BuilderOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : BuilderOptions() {
+        BuilderOptions::BuilderOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::SymbolicModelDescription const& modelDescription) : BuilderOptions() {
             if (!formulas.empty()) {
                 for (auto const& formula : formulas) {
-                    this->preserveFormula(*formula);
+                    this->preserveFormula(*formula, modelDescription);
                 }
                 if (formulas.size() == 1) {
                     this->setTerminalStatesFromFormula(*formulas.front());
@@ -65,7 +65,7 @@ namespace storm {
             showProgressDelay = generalSettings.getShowProgressDelay();
         }
         
-        void BuilderOptions::preserveFormula(storm::logic::Formula const& formula) {
+        void BuilderOptions::preserveFormula(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription) {
             // If we already had terminal states, we need to erase them.
             if (hasTerminalStates()) {
                 clearTerminalStates();
@@ -89,9 +89,7 @@ namespace storm {
                 addLabel(formula->getExpression());
             }
             
-            storm::logic::FragmentSpecification transitionRewardScalingFragment = storm::logic::csl().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setLongRunAverageOperatorsAllowed(true).setMultiObjectiveFormulasAllowed(true).setTotalRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true);
-            scaleAndLiftTransitionRewards = scaleAndLiftTransitionRewards && formula.isInFragment(transitionRewardScalingFragment);
-            
+            scaleAndLiftTransitionRewards = scaleAndLiftTransitionRewards && storm::logic::LiftableTransitionRewardsVisitor(modelDescription).areTransitionRewardsLiftable(formula);
         }
         
         void BuilderOptions::setTerminalStatesFromFormula(storm::logic::Formula const& formula) {

src/storm/builder/BuilderOptions.h

@@ -8,6 +8,7 @@
 #include <boost/optional.hpp>
 
 #include "storm/storage/expressions/Expression.h"
+#include "storm/storage/SymbolicModelDescription.h"
 
 namespace storm {
     namespace expressions {
@@ -54,7 +55,7 @@ namespace storm {
              *
              * @param formula The formula based on which to choose the building options.
              */
-            BuilderOptions(storm::logic::Formula const& formula);
+            BuilderOptions(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription = storm::storage::SymbolicModelDescription());
             
             /*!
              * Creates an object representing the suggested building options assuming that the given formulas are
@@ -62,7 +63,7 @@ namespace storm {
              *
              * @param formula Thes formula based on which to choose the building options.
              */
-            BuilderOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
+            BuilderOptions(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::SymbolicModelDescription const& modelDescription = storm::storage::SymbolicModelDescription());
             
             /*!
              * Changes the options in a way that ensures that the given formula can be checked on the model once it
@@ -70,7 +71,7 @@ namespace storm {
              *
              * @param formula The formula that is to be ''preserved''.
              */
-            void preserveFormula(storm::logic::Formula const& formula);
+            void preserveFormula(storm::logic::Formula const& formula, storm::storage::SymbolicModelDescription const& modelDescription = storm::storage::SymbolicModelDescription());
             
             /*!
              * Analyzes the given formula and sets an expression for the states states of the model that can be

src/storm/logic/LiftableTransitionRewardsVisitor.cpp

@@ -0,0 +1,133 @@
+#include "storm/logic/LiftableTransitionRewardsVisitor.h"
+
+#include "storm/logic/Formulas.h"
+#include "storm/storage/jani/traverser/RewardModelInformation.h"
+
+namespace storm {
+    namespace logic {
+        
+        LiftableTransitionRewardsVisitor::LiftableTransitionRewardsVisitor(storm::storage::SymbolicModelDescription const& symbolicModelDescription) : symbolicModelDescription(symbolicModelDescription) {
+            // Intentionally left empty.
+        }
+        
+        bool LiftableTransitionRewardsVisitor::areTransitionRewardsLiftable(Formula const& f) const {
+            return boost::any_cast<bool>(f.accept(*this, boost::any()));
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const {
+            return true;
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(AtomicLabelFormula const&, boost::any const&) const {
+            return true;
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const {
+            return true;
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const {
+            return true;
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
+            for (unsigned i = 0; i < f.getDimension(); ++i) {
+                if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) {
+                    return false;
+                }
+            }
+            
+            bool result = true;
+            if (f.hasMultiDimensionalSubformulas()) {
+                for (unsigned i = 0; i < f.getDimension(); ++i) {
+                    result = result && boost::any_cast<bool>(f.getLeftSubformula(i).accept(*this, data));
+                    result = result && boost::any_cast<bool>(f.getRightSubformula(i).accept(*this, data));
+                }
+            } else {
+                result = result && boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data));
+                result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
+            }
+            return result;
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(ConditionalFormula const& f, boost::any const& data) const {
+            return !f.isConditionalRewardFormula() && boost::any_cast<bool>(f.getSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getConditionFormula().accept(*this, data));
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {
+            for (unsigned i = 0; i < f.getDimension(); ++i) {
+                if (f.getTimeBoundReference(i).isRewardBound() && rewardModelHasTransitionRewards(f.getTimeBoundReference(i).getRewardName())) {
+                    return false;
+                }
+            }
+            return true;
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const {
+            return true;
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const {
+            return true;
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
+            bool result = true;
+            for (auto const& subF : f.getSubformulas()){
+                result = result && boost::any_cast<bool>(subF->accept(*this, data));
+            }
+            return result;
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(NextFormula const& f, boost::any const& data) const {
+            return boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
+            return boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(TotalRewardFormula const&, boost::any const&) const {
+            return true;
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+        
+        boost::any LiftableTransitionRewardsVisitor::visit(UntilFormula const& f, boost::any const& data) const {
+            return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this));
+        }
+        
+        bool LiftableTransitionRewardsVisitor::rewardModelHasTransitionRewards(std::string const& rewardModelName) const {
+            if (symbolicModelDescription.isJaniModel()) {
+                return storm::jani::RewardModelInformation(symbolicModelDescription.asJaniModel(), rewardModelName).hasTransitionRewards();
+            } else if (symbolicModelDescription.isPrismProgram()) {
+                return symbolicModelDescription.asPrismProgram().getRewardModel(rewardModelName).hasTransitionRewards();
+            } else {
+                // No model given
+                return false;
+            }
+        }
+    }
+}

src/storm/logic/LiftableTransitionRewardsVisitor.h

@@ -0,0 +1,48 @@
+#pragma once
+
+#include "storm/logic/FormulaVisitor.h"
+#include "storm/logic/FormulaInformation.h"
+#include "storm/storage/SymbolicModelDescription.h"
+
+namespace storm {
+    
+    namespace logic {
+        
+        class LiftableTransitionRewardsVisitor : public FormulaVisitor {
+        public:
+            
+            LiftableTransitionRewardsVisitor(storm::storage::SymbolicModelDescription const& symbolicModelDescription = storm::storage::SymbolicModelDescription());
+            
+            /*!
+             * Returns true, when lifting transition rewards to action rewards (by scaling with the transition probability) preserves the given formula
+             */
+            bool areTransitionRewardsLiftable(Formula const& f) const;
+            
+            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ConditionalFormula 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(TimeOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(NextFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ProbabilityOperatorFormula 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;
+            virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
+        
+        private:
+            storm::storage::SymbolicModelDescription const& symbolicModelDescription;
+            bool rewardModelHasTransitionRewards(std::string const& rewardModelName) const;
+        };
+        
+    }
+}