total reward formulas

Former-commit-id: 878065b902

examples/multi-objective/mdp/dpm/dpm100_numerical.pctl

@@ -1,3 +1,3 @@
- multi(R{"power"}min=? [ C<=100 ], R{"queue"}<=70 [ C<=100 ]); 
+ multi(R{"power"}min=? [ C<=100 ], R{"queue"}<=70 [ C<=100 ])
 // Note: The property file from http://www.prismmodelchecker.org/files/atva12mo/ does not provide a threshold for the second objective.
 // We pick a threshold that intersects the pareto curve.

src/logic/CloneVisitor.cpp

@@ -99,6 +99,10 @@ namespace storm {
             return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation()));
         }
         
+        boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const {
+            return std::static_pointer_cast<Formula>(std::make_shared<TotalRewardFormula>());
+        }
+        
         boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
             std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
             return std::static_pointer_cast<Formula>(std::make_shared<UnaryBooleanStateFormula>(f.getOperator(), subformula));

src/logic/CloneVisitor.h

@@ -29,6 +29,7 @@ namespace storm {
             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;
         };
@@ -37,4 +38,4 @@ namespace storm {
 }
 
 
-#endif /* STORM_LOGIC_CLONEVISITOR_H_ */
+#endif /* STORM_LOGIC_CLONEVISITOR_H_ */

src/logic/ComparisonType.h

@@ -14,7 +14,20 @@ namespace storm {
             inline bool isLowerBound(ComparisonType t) {
                 return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual);
             }
-            
+        
+            inline ComparisonType invert(ComparisonType t) {
+                switch(t) {
+                    case ComparisonType::Less:
+                        return ComparisonType::GreaterEqual;
+                    case ComparisonType::LessEqual:
+                        return ComparisonType::Greater;
+                    case ComparisonType::Greater:
+                        return ComparisonType::LessEqual;
+                    case ComparisonType::GreaterEqual:
+                        return ComparisonType::Less;
+                }
+            }
+        
             std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType);
 	}
 }

src/logic/Formula.cpp

@@ -133,6 +133,10 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isTotalRewardFormula() const {
+            return false;
+        }
+        
         bool Formula::isReachabilityTimeFormula() const {
             return false;
         }
@@ -363,6 +367,14 @@ namespace storm {
             return dynamic_cast<CumulativeRewardFormula const&>(*this);
         }
         
+        TotalRewardFormula& Formula::asTotalRewardFormula() {
+            return dynamic_cast<TotalRewardFormula&>(*this);
+        }
+        
+        TotalRewardFormula const& Formula::asTotalRewardFormula() const {
+            return dynamic_cast<TotalRewardFormula const&>(*this);
+        }
+        
         InstantaneousRewardFormula& Formula::asInstantaneousRewardFormula() {
             return dynamic_cast<InstantaneousRewardFormula&>(*this);
         }
@@ -470,4 +482,4 @@ namespace storm {
             return formula.writeToStream(out);
         }
     }
-}
+}

src/logic/Formula.h

@@ -76,6 +76,7 @@ namespace storm {
             virtual bool isInstantaneousRewardFormula() const;
             virtual bool isReachabilityRewardFormula() const;
             virtual bool isLongRunAverageRewardFormula() const;
+            virtual bool isTotalRewardFormula() const;
             
             // Expected time formulas.
             virtual bool isReachabilityTimeFormula() const;
@@ -169,6 +170,9 @@ namespace storm {
             CumulativeRewardFormula& asCumulativeRewardFormula();
             CumulativeRewardFormula const& asCumulativeRewardFormula() const;
             
+            TotalRewardFormula& asTotalRewardFormula();
+            TotalRewardFormula const& asTotalRewardFormula() const;
+            
             InstantaneousRewardFormula& asInstantaneousRewardFormula();
             InstantaneousRewardFormula const& asInstantaneousRewardFormula() const;
             
@@ -220,4 +224,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_LOGIC_FORMULA_H_ */
+#endif /* STORM_LOGIC_FORMULA_H_ */

src/logic/FormulaInformationVisitor.cpp

@@ -81,6 +81,10 @@ namespace storm {
             return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this)).setContainsRewardOperator();
         }
         
+        boost::any FormulaInformationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const {
+            return FormulaInformation();
+        }
+        
         boost::any FormulaInformationVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
             return f.getSubformula().accept(*this);
         }
@@ -90,4 +94,4 @@ namespace storm {
         }
 
     }
-}
+}

src/logic/FormulaInformationVisitor.h

@@ -28,6 +28,7 @@ namespace storm {
             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;
         };
@@ -36,4 +37,4 @@ namespace storm {
 }
 
 
-#endif /* STORM_LOGIC_FORMULAINFORMATIONVISITOR_H_ */
+#endif /* STORM_LOGIC_FORMULAINFORMATIONVISITOR_H_ */

src/logic/FormulaVisitor.h

@@ -27,6 +27,7 @@ namespace storm {
             virtual boost::any visit(NextFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(UntilFormula const& f, boost::any const& data) const = 0;
         };
@@ -34,4 +35,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_LOGIC_FORMULAVISITOR_H_ */
+#endif /* STORM_LOGIC_FORMULAVISITOR_H_ */

src/logic/Formulas.h

@@ -20,6 +20,7 @@
 #include "src/logic/LongRunAverageOperatorFormula.h"
 #include "src/logic/MultiObjectiveFormula.h"
 #include "src/logic/TimeOperatorFormula.h"
+#include "src/logic/TotalRewardFormula.h"
 #include "src/logic/UnaryBooleanStateFormula.h"
 #include "src/logic/UnaryPathFormula.h"
 #include "src/logic/UnaryStateFormula.h"
@@ -27,4 +28,4 @@
 #include "src/logic/ConditionalFormula.h"
 #include "src/logic/ProbabilityOperatorFormula.h"
 #include "src/logic/RewardOperatorFormula.h"
-#include "src/logic/ComparisonType.h"
+#include "src/logic/ComparisonType.h"

src/logic/FormulasForwardDeclarations.h

@@ -27,6 +27,7 @@ namespace storm {
         class ProbabilityOperatorFormula;
         class RewardOperatorFormula;
         class StateFormula;
+        class TotalRewardFormula;
         class UnaryBooleanStateFormula;
         class UnaryPathFormula;
         class UnaryStateFormula;
@@ -34,4 +35,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_LOGIC_FORMULASFORWARDDECLARATIONS_H_ */
+#endif /* STORM_LOGIC_FORMULASFORWARDDECLARATIONS_H_ */

src/logic/FragmentChecker.cpp

@@ -216,6 +216,11 @@ namespace storm {
             return result;
         }
         
+        boost::any FragmentChecker::visit(TotalRewardFormula const& f, boost::any const& data) const {
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            return inherited.getSpecification().areTotalRewardFormulasAllowed();
+        }
+        
         boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areUnaryBooleanStateFormulasAllowed();
@@ -235,4 +240,4 @@ namespace storm {
             return result;
         }
     }
-}
+}

src/logic/FragmentChecker.h

@@ -29,6 +29,7 @@ namespace storm {
             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;
         };
@@ -37,4 +38,4 @@ namespace storm {
 }
 
 
-#endif /* STORM_LOGIC_FRAGMENTCHECKER_H_ */
+#endif /* STORM_LOGIC_FRAGMENTCHECKER_H_ */

src/logic/FragmentSpecification.cpp

@@ -94,9 +94,9 @@ namespace storm {
             multiObjective.setRewardOperatorsAllowed(true);
             multiObjective.setReachabilityRewardFormulasAllowed(true);
             multiObjective.setCumulativeRewardFormulasAllowed(true);
+            multiObjective.setTotalRewardFormulasAllowed(true);
             multiObjective.setBoundedUntilFormulasAllowed(true);
-            multiObjective.setStepBoundedUntilFormulasAllowed(true);
- //           multiObjective.setTimeBoundedUntilFormulasAllowed(true); //probably better to activate this only when an MA is given...
+            
 
             return multiObjective;
         }
@@ -125,6 +125,7 @@ namespace storm {
             instantaneousRewardFormula = false;
             reachabilityRewardFormula = false;
             longRunAverageRewardFormula = false;
+            totalRewardFormula = false;
             
             conditionalProbabilityFormula = false;
             conditionalRewardFormula = false;
@@ -321,6 +322,16 @@ namespace storm {
             return *this;
         }
         
+        
+        bool FragmentSpecification::areTotalRewardFormulasAllowed() const {
+            return totalRewardFormula;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setTotalRewardFormulasAllowed(bool newValue) {
+            this->totalRewardFormula = newValue;
+            return *this;
+        }
+        
         bool FragmentSpecification::areConditionalProbabilityFormulasAllowed() const {
             return conditionalProbabilityFormula;
         }

src/logic/FragmentSpecification.h

@@ -69,6 +69,9 @@ namespace storm {
             
             bool areLongRunAverageRewardFormulasAllowed() const;
             FragmentSpecification& setLongRunAverageRewardFormulasAllowed(bool newValue);
+            
+            bool areTotalRewardFormulasAllowed() const;
+            FragmentSpecification& setTotalRewardFormulasAllowed(bool newValue);
 
             bool areConditionalProbabilityFormulasAllowed() const;
             FragmentSpecification& setConditionalProbabilityFormulasAllowed(bool newValue);
@@ -141,6 +144,7 @@ namespace storm {
             bool instantaneousRewardFormula;
             bool reachabilityRewardFormula;
             bool longRunAverageRewardFormula;
+            bool totalRewardFormula;
             
             bool conditionalProbabilityFormula;
             bool conditionalRewardFormula;
@@ -188,4 +192,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_LOGIC_FRAGMENTSPECIFICATION_H_ */
+#endif /* STORM_LOGIC_FRAGMENTSPECIFICATION_H_ */

src/logic/ToExpressionVisitor.cpp

@@ -98,6 +98,10 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
         }
         
+        boost::any ToExpressionVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
         boost::any ToExpressionVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
             storm::expressions::Expression subexpression = boost::any_cast<storm::expressions::Expression>(f.getSubformula().accept(*this, data));
             switch (f.getOperator()) {

src/logic/ToExpressionVisitor.h

@@ -29,6 +29,7 @@ namespace storm {
             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;
         };
@@ -37,4 +38,4 @@ namespace storm {
 }
 
 
-#endif /* STORM_LOGIC_TOEXPRESSIONVISITOR_H_ */
+#endif /* STORM_LOGIC_TOEXPRESSIONVISITOR_H_ */

src/logic/TotalRewardFormula.cpp

@@ -0,0 +1,28 @@
+#include "src/logic/TotalRewardFormula.h"
+
+#include "src/logic/FormulaVisitor.h"
+
+namespace storm {
+    namespace logic {
+        TotalRewardFormula::TotalRewardFormula() {
+            // Intentionally left empty.
+        }
+        
+        bool TotalRewardFormula::isTotalRewardFormula() const {
+            return true;
+        }
+        
+        bool TotalRewardFormula::isRewardPathFormula() const {
+            return true;
+        }
+        
+        boost::any TotalRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+
+        std::ostream& TotalRewardFormula::writeToStream(std::ostream& out) const {
+            out << "C";
+            return out;
+        }
+    }
+}

src/logic/TotalRewardFormula.h

@@ -0,0 +1,29 @@
+#ifndef STORM_LOGIC_TOTALREWARDFORMULA_H_
+#define STORM_LOGIC_TOTALREWARDFORMULA_H_
+
+#include <boost/variant.hpp>
+
+#include "src/logic/PathFormula.h"
+
+namespace storm {
+    namespace logic {
+        class TotalRewardFormula : public PathFormula {
+        public:
+            TotalRewardFormula();
+            
+            virtual ~TotalRewardFormula() {
+                // Intentionally left empty.
+            }
+
+            virtual bool isTotalRewardFormula() const override;
+            virtual bool isRewardPathFormula() const override;
+            
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_TOTALREWARDFORMULA_H_ */

src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp

@@ -29,7 +29,7 @@ namespace storm {
             //In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude this.
             if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
             if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
-            return checkTask.getFormula().isInFragment(storm::logic::multiObjective());
+            return checkTask.getFormula().isInFragment(storm::logic::multiObjective().setStepBoundedUntilFormulasAllowed(true));
         }
         
         template<typename SparseMdpModelType>

src/parser/FormulaParser.cpp

@@ -142,6 +142,7 @@ namespace storm {
             
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> rewardPathFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> cumulativeRewardFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> totalRewardFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> instantaneousRewardFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageRewardFormula;
             
@@ -153,6 +154,7 @@ namespace storm {
             // Methods that actually create the expression objects.
             std::shared_ptr<storm::logic::Formula const> createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
             std::shared_ptr<storm::logic::Formula const> createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
+            std::shared_ptr<storm::logic::Formula const> createTotalRewardFormula() const;
             std::shared_ptr<storm::logic::Formula const> createLongRunAverageRewardFormula() const;
             std::shared_ptr<storm::logic::Formula const> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;
             std::shared_ptr<storm::logic::Formula const> createBooleanLiteralFormula(bool literal) const;
@@ -269,7 +271,10 @@ namespace storm {
             cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
             cumulativeRewardFormula.name("cumulative reward formula");
             
-            rewardPathFormula = conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula;
+            totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))];
+            totalRewardFormula.name("total reward formula");
+            
+            rewardPathFormula = conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | totalRewardFormula;
             rewardPathFormula.name("reward path formula");
             
             expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)];
@@ -375,6 +380,7 @@ namespace storm {
             debug(expressionFormula);
             debug(rewardPathFormula);
             debug(cumulativeRewardFormula);
+            debug(totalRewardFormula);
             debug(instantaneousRewardFormula);
             debug(multiObjectiveFormula);
             */
@@ -402,6 +408,7 @@ namespace storm {
             qi::on_error<qi::fail>(expressionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(totalRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(multiObjectiveFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
         }
@@ -430,6 +437,10 @@ namespace storm {
             }
         }
         
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createTotalRewardFormula() const {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::TotalRewardFormula());
+        }
+        
         std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createLongRunAverageRewardFormula() const {
             return std::shared_ptr<storm::logic::Formula const>(new storm::logic::LongRunAverageRewardFormula());
         }