diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp
index 4b427b1dc..cb24e7d8b 100644
--- a/src/storm/logic/CloneVisitor.cpp
+++ b/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));
diff --git a/src/storm/logic/CloneVisitor.h b/src/storm/logic/CloneVisitor.h
index c03f2e4fc..4b1d620ee 100644
--- a/src/storm/logic/CloneVisitor.h
+++ b/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;
diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index 9dd2b0fba..fe3a1e41a 100644
--- a/src/storm/logic/Formula.cpp
+++ b/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;
}
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 91ccdf342..bd88374a3 100644
--- a/src/storm/logic/Formula.h
+++ b/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;
diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp
index 0aab5e04e..b3ad356db 100644
--- a/src/storm/logic/FormulaInformationVisitor.cpp
+++ b/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();
}
diff --git a/src/storm/logic/FormulaInformationVisitor.h b/src/storm/logic/FormulaInformationVisitor.h
index 134ad0bc4..7ba8b70b9 100644
--- a/src/storm/logic/FormulaInformationVisitor.h
+++ b/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;
diff --git a/src/storm/logic/FormulaVisitor.h b/src/storm/logic/FormulaVisitor.h
index f0abd0436..1eaf6791d 100644
--- a/src/storm/logic/FormulaVisitor.h
+++ b/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;
diff --git a/src/storm/logic/Formulas.h b/src/storm/logic/Formulas.h
index bba8afea0..bdda5c863 100644
--- a/src/storm/logic/Formulas.h
+++ b/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"
diff --git a/src/storm/logic/FormulasForwardDeclarations.h b/src/storm/logic/FormulasForwardDeclarations.h
index 3f3f1dfaf..170316fc7 100644
--- a/src/storm/logic/FormulasForwardDeclarations.h
+++ b/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;
diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp
index adc96728b..4bda466c4 100644
--- a/src/storm/logic/FragmentChecker.cpp
+++ b/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();
diff --git a/src/storm/logic/FragmentChecker.h b/src/storm/logic/FragmentChecker.h
index cb3ddb95d..485a205aa 100644
--- a/src/storm/logic/FragmentChecker.h
+++ b/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;
diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp
index 9b5b8b17e..46d7c4075 100644
--- a/src/storm/logic/FragmentSpecification.cpp
+++ b/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;
}
diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h
index 012716c78..aa48c0738 100644
--- a/src/storm/logic/FragmentSpecification.h
+++ b/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();
}
}
diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
index db8df4962..99eeb444b 100644
--- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
+++ b/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));
}
diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.h b/src/storm/logic/LiftableTransitionRewardsVisitor.h
index 9147ea3c7..c09f9c25b 100644
--- a/src/storm/logic/LiftableTransitionRewardsVisitor.h
+++ b/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;
diff --git a/src/storm/logic/QuantileFormula.cpp b/src/storm/logic/QuantileFormula.cpp
new file mode 100644
index 000000000..ea8677afd
--- /dev/null
+++ b/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;
+ }
+ }
+}
diff --git a/src/storm/logic/QuantileFormula.h b/src/storm/logic/QuantileFormula.h
new file mode 100644
index 000000000..2690171a5
--- /dev/null
+++ b/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;
+ };
+ }
+}
diff --git a/src/storm/logic/ToExpressionVisitor.cpp b/src/storm/logic/ToExpressionVisitor.cpp
index ddfe0ea6d..27ea1fa6b 100644
--- a/src/storm/logic/ToExpressionVisitor.cpp
+++ b/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.");
}
diff --git a/src/storm/logic/ToExpressionVisitor.h b/src/storm/logic/ToExpressionVisitor.h
index 4fe91bad3..345698f5a 100644
--- a/src/storm/logic/ToExpressionVisitor.h
+++ b/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;
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index 1aa2522fb..fce7562b3 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/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";
diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h
index 0bd1486f2..9a99a443a 100644
--- a/src/storm/storage/jani/JSONExporter.h
+++ b/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;