logic: Added QuantileFormulas.

src/storm/logic/CloneVisitor.cpp

@@ -108,6 +108,11 @@ namespace storm {
             return std::static_pointer_cast<Formula>(std::make_shared<MultiObjectiveFormula>(subformulas));
         }
         
+        boost::any CloneVisitor::visit(QuantileFormula 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<QuantileFormula>(f.getBoundVariables(), subformula));
+        }
+        
         boost::any CloneVisitor::visit(NextFormula 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<NextFormula>(subformula));

src/storm/logic/CloneVisitor.h

@@ -26,6 +26,7 @@ namespace storm {
             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(QuantileFormula 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;

src/storm/logic/Formula.cpp

@@ -23,6 +23,10 @@ namespace storm {
             return false;
         }
         
+        bool Formula::isQuantileFormula() const {
+            return false;
+        }
+        
         bool Formula::isBinaryStateFormula() const {
             return false;
         }

src/storm/logic/Formula.h

@@ -48,6 +48,7 @@ namespace storm {
             virtual bool isUnaryBooleanStateFormula() const;
             
             virtual bool isMultiObjectiveFormula() const;
+            virtual bool isQuantileFormula() const;
 
             // Operator formulas.
             virtual bool isOperatorFormula() const;

src/storm/logic/FormulaInformationVisitor.cpp

@@ -93,6 +93,10 @@ namespace storm {
             return result;
         }
         
+        boost::any FormulaInformationVisitor::visit(QuantileFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+        
         boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const {
             return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)).setContainsNextFormula();
         }

src/storm/logic/FormulaInformationVisitor.h

@@ -25,6 +25,7 @@ namespace storm {
             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(QuantileFormula 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;

src/storm/logic/FormulaVisitor.h

@@ -26,6 +26,7 @@ namespace storm {
             virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(QuantileFormula const& f, boost::any const& data) const = 0;
             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;

src/storm/logic/Formulas.h

@@ -19,6 +19,7 @@
 #include "storm/logic/StateFormula.h"
 #include "storm/logic/LongRunAverageOperatorFormula.h"
 #include "storm/logic/MultiObjectiveFormula.h"
+#include "storm/logic/QuantileFormula.h"
 #include "storm/logic/TimeOperatorFormula.h"
 #include "storm/logic/TotalRewardFormula.h"
 #include "storm/logic/UnaryBooleanStateFormula.h"

src/storm/logic/FormulasForwardDeclarations.h

@@ -21,6 +21,7 @@ namespace storm {
         class LongRunAverageOperatorFormula;
         class LongRunAverageRewardFormula;
         class MultiObjectiveFormula;
+        class QuantileFormula;
         class NextFormula;
         class OperatorFormula;
         struct OperatorInformation;

src/storm/logic/FragmentChecker.cpp

@@ -27,6 +27,9 @@ namespace storm {
             if (specification.isMultiObjectiveFormulaAtTopLevelRequired()) {
                 result &= f.isMultiObjectiveFormula();
             }
+            if (specification.isQuantileFormulaAtTopLevelRequired()) {
+                result &= f.isQuantileFormula();
+            }
             
             return result;
         }
@@ -229,6 +232,14 @@ namespace storm {
             return result;
         }
         
+        boost::any FragmentChecker::visit(QuantileFormula const& f, boost::any const& data) const {
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            if (!inherited.getSpecification().areQuantileFormulasAllowed()) {
+                return false;
+            }
+            return f.getSubformula().accept(*this, data);
+        }
+        
         boost::any FragmentChecker::visit(NextFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areNextFormulasAllowed();

src/storm/logic/FragmentChecker.h

@@ -26,6 +26,7 @@ namespace storm {
             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(QuantileFormula 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;

src/storm/logic/FragmentSpecification.cpp

@@ -110,6 +110,27 @@ namespace storm {
             return multiObjective;
         }
         
+        FragmentSpecification quantiles() {
+            FragmentSpecification quantiles = propositional();
+            
+            quantiles.setQuantileFormulasAllowed(true);
+            quantiles.setQuantileFormulaAtTopLevelRequired(true);
+            quantiles.setProbabilityOperatorsAllowed(true);
+            quantiles.setRewardOperatorsAllowed(true);
+            quantiles.setBoundedUntilFormulasAllowed(true);
+            quantiles.setStepBoundedUntilFormulasAllowed(true);
+            quantiles.setTimeBoundedUntilFormulasAllowed(true);
+            quantiles.setRewardBoundedUntilFormulasAllowed(true);
+            quantiles.setStepBoundedCumulativeRewardFormulasAllowed(true);
+            quantiles.setTimeBoundedCumulativeRewardFormulasAllowed(true);
+            quantiles.setRewardBoundedCumulativeRewardFormulasAllowed(true);
+            quantiles.setCumulativeRewardFormulasAllowed(true);
+            quantiles.setMultiDimensionalBoundedUntilFormulasAllowed(true);
+            quantiles.setMultiDimensionalCumulativeRewardFormulasAllowed(true);
+    
+            return quantiles;
+        }
+        
         FragmentSpecification::FragmentSpecification() {
             probabilityOperator = false;
             rewardOperator = false;
@@ -117,6 +138,7 @@ namespace storm {
             longRunAverageOperator = false;
             
             multiObjectiveFormula = false;
+            quantileFormula = false;
             
             globallyFormula = false;
             reachabilityProbabilityFormula = false;
@@ -162,6 +184,7 @@ namespace storm {
             operatorAtTopLevelRequired = false;
             multiObjectiveFormulaAtTopLevelRequired = false;
             operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false;
+            quantileFormulaAtTopLevelRequired = false;
             
             rewardAccumulation = false;
         }
@@ -215,6 +238,15 @@ namespace storm {
             return *this;
         }
         
+        bool FragmentSpecification::areQuantileFormulasAllowed() const {
+            return quantileFormula;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setQuantileFormulasAllowed( bool newValue) {
+            this->quantileFormula = newValue;
+            return *this;
+        }
+        
         bool FragmentSpecification::areGloballyFormulasAllowed() const {
             return globallyFormula;
         }
@@ -566,7 +598,16 @@ namespace storm {
             operatorsAtTopLevelOfMultiObjectiveFormulasRequired = newValue;
             return *this;
         }
-        
+
+        bool FragmentSpecification::isQuantileFormulaAtTopLevelRequired() const {
+            return quantileFormulaAtTopLevelRequired;
+        }
+
+        FragmentSpecification& FragmentSpecification::setQuantileFormulaAtTopLevelRequired(bool newValue) {
+            quantileFormulaAtTopLevelRequired = newValue;
+            return *this;
+        }
+
         bool FragmentSpecification::isRewardAccumulationAllowed() const {
             return rewardAccumulation;
         }

src/storm/logic/FragmentSpecification.h

@@ -33,6 +33,9 @@ namespace storm {
             
             bool areMultiObjectiveFormulasAllowed() const;
             FragmentSpecification& setMultiObjectiveFormulasAllowed( bool newValue);
+            
+            bool areQuantileFormulasAllowed() const;
+            FragmentSpecification& setQuantileFormulasAllowed( bool newValue);
 
             bool areGloballyFormulasAllowed() const;
             FragmentSpecification& setGloballyFormulasAllowed(bool newValue);
@@ -145,6 +148,9 @@ namespace storm {
             bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const;
             FragmentSpecification& setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue);
             
+            bool isQuantileFormulaAtTopLevelRequired() const;
+            FragmentSpecification& setQuantileFormulaAtTopLevelRequired(bool newValue);
+            
             bool isRewardAccumulationAllowed() const;
             FragmentSpecification& setRewardAccumulationAllowed(bool newValue);
 
@@ -161,6 +167,7 @@ namespace storm {
             bool longRunAverageOperator;
             
             bool multiObjectiveFormula;
+            bool quantileFormula;
             
             bool globallyFormula;
             bool reachabilityProbabilityFormula;
@@ -204,6 +211,7 @@ namespace storm {
             bool qualitativeOperatorResults;
             bool operatorAtTopLevelRequired;
             bool multiObjectiveFormulaAtTopLevelRequired;
+            bool quantileFormulaAtTopLevelRequired;
             bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
             
             bool rewardAccumulation;
@@ -232,6 +240,9 @@ namespace storm {
         
         // Multi-Objective formulas.
         FragmentSpecification multiObjective();
+        
+        // Quantile formulas.
+        FragmentSpecification quantiles();
 
     }
 }

src/storm/logic/LiftableTransitionRewardsVisitor.cpp

@@ -95,6 +95,10 @@ namespace storm {
             return result;
         }
         
+        boost::any LiftableTransitionRewardsVisitor::visit(QuantileFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+        
         boost::any LiftableTransitionRewardsVisitor::visit(NextFormula const& f, boost::any const& data) const {
             return boost::any_cast<bool>(f.getSubformula().accept(*this, data));
         }

src/storm/logic/LiftableTransitionRewardsVisitor.h

@@ -32,6 +32,7 @@ namespace storm {
             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(QuantileFormula 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;

src/storm/logic/QuantileFormula.cpp

@@ -0,0 +1,96 @@
+#include "storm/logic/QuantileFormula.h"
+
+#include "storm/logic/FormulaVisitor.h"
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace logic {
+    
+        QuantileFormula::QuantileFormula(std::vector<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> const& boundVariables, std::shared_ptr<Formula const> subformula) : boundVariables(boundVariables), subformula(subformula) {
+            STORM_LOG_THROW(!boundVariables.empty(), storm::exceptions::InvalidArgumentException, "Quantile formula without bound variables are invalid.");
+        }
+        
+        QuantileFormula::~QuantileFormula() {
+            // Intentionally left empty
+        }
+        
+        bool QuantileFormula::isQuantileFormula() const {
+            return true;
+        }
+        
+        bool QuantileFormula::hasQuantitativeResult() const {
+            return true;
+        }
+        
+        bool QuantileFormula::hasNumericalResult() const {
+            return !isMultiDimensional();
+        }
+        
+        bool QuantileFormula::hasParetoCurveResult() const {
+            return isMultiDimensional();
+        }
+        
+        Formula const& QuantileFormula::getSubformula() const {
+            return *subformula;
+        }
+        
+        uint64_t QuantileFormula::getDimension() const {
+            return boundVariables.size();
+        }
+        
+        bool QuantileFormula::isMultiDimensional() const {
+            return getDimension() > 1;
+        }
+        
+        storm::expressions::Variable const& QuantileFormula::getBoundVariable() const {
+            STORM_LOG_THROW(boundVariables.size() == 1, storm::exceptions::InvalidArgumentException, "Requested unique bound variables. However, there are multiple bound variables defined.");
+            return boundVariables.front().second;
+        }
+        
+        storm::expressions::Variable const& QuantileFormula::getBoundVariable(uint64_t index) const {
+            STORM_LOG_THROW(index < boundVariables.size(), storm::exceptions::InvalidArgumentException, "Requested bound variable with index" << index << ". However, there are only " << boundVariables.size() << " bound variables.");
+            return boundVariables[index].second;
+        }
+        
+        std::vector<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> const& QuantileFormula::getBoundVariables() const {
+            return boundVariables;
+        }
+        
+        storm::solver::OptimizationDirection const& QuantileFormula::getOptimizationDirection() const {
+            STORM_LOG_THROW(boundVariables.size() == 1, storm::exceptions::InvalidArgumentException, "Requested unique optimization direction of the bound variables. However, there are multiple bound variables defined.");
+            return boundVariables.front().first;
+        }
+        
+        storm::solver::OptimizationDirection const& QuantileFormula::getOptimizationDirection(uint64_t index) const {
+            STORM_LOG_THROW(index < boundVariables.size(), storm::exceptions::InvalidArgumentException, "Requested optimization direction with index" << index << ". However, there are only " << boundVariables.size() << " bound variables.");
+            return boundVariables[index].first;
+        }
+        
+        boost::any QuantileFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
+        void QuantileFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            subformula->gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+        }
+        
+        void QuantileFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
+            subformula->gatherAtomicLabelFormulas(atomicLabelFormulas);
+        }
+        
+        void QuantileFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
+            subformula->gatherReferencedRewardModels(referencedRewardModels);
+        }
+        
+        std::ostream& QuantileFormula::writeToStream(std::ostream& out) const {
+            out << "quantile(";
+            for (auto const& bv : boundVariables) {
+                out << bv.first << " " << bv.second.getName() << ", ";
+            }
+            subformula->writeToStream(out);
+            out << ")";
+            return out;
+        }
+    }
+}

src/storm/logic/QuantileFormula.h

@@ -0,0 +1,41 @@
+#pragma once
+
+#include "storm/logic/Formula.h"
+#include "storm/solver/OptimizationDirection.h"
+
+namespace storm {
+    namespace logic {
+        class QuantileFormula : public Formula {
+        public:
+            QuantileFormula(std::vector<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> const& boundVariables, std::shared_ptr<Formula const> subformula);
+            
+            virtual ~QuantileFormula();
+            
+            virtual bool isQuantileFormula() const override;
+            
+            virtual bool hasQuantitativeResult() const override; // Result is numerical or a pareto curve
+            virtual bool hasNumericalResult() const; // Result is numerical
+            virtual bool hasParetoCurveResult() const; // Result is a pareto curve
+            
+            Formula const& getSubformula() const;
+            uint64_t getDimension() const;
+            bool isMultiDimensional() const;
+            
+            storm::expressions::Variable const& getBoundVariable() const;
+            storm::expressions::Variable const& getBoundVariable(uint64_t index) const;
+            std::vector<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> const& getBoundVariables() const;
+            storm::solver::OptimizationDirection const& getOptimizationDirection() const;
+            storm::solver::OptimizationDirection const& getOptimizationDirection(uint64_t index) const;
+            
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+            virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+            virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
+            virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+        private:
+            std::vector<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> boundVariables;
+            std::shared_ptr<Formula const> subformula;
+        };
+    }
+}

src/storm/logic/ToExpressionVisitor.cpp

@@ -87,6 +87,10 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
         }
         
+        boost::any ToExpressionVisitor::visit(QuantileFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
         boost::any ToExpressionVisitor::visit(NextFormula const&, boost::any const&) const {
             STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
         }

src/storm/logic/ToExpressionVisitor.h

@@ -26,6 +26,7 @@ namespace storm {
             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(QuantileFormula 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;

src/storm/storage/jani/JSONExporter.cpp

@@ -411,6 +411,10 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a multi-objective formula");
         }
         
+        boost::any FormulaToJaniJson::visit(storm::logic::QuantileFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a Quantile formula");
+        }
+        
         boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const {
             modernjson::json opDecl;
             opDecl["op"] = "U";

src/storm/storage/jani/JSONExporter.h

@@ -64,6 +64,7 @@ namespace storm {
             virtual boost::any visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::MultiObjectiveFormula const& f, boost::any const& data) const;
+            virtual boost::any visit(storm::logic::QuantileFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::NextFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const;