diff --git a/src/storm-parsers/api/properties.cpp b/src/storm-parsers/api/properties.cpp
index 425fee410..0a33be5b2 100644
--- a/src/storm-parsers/api/properties.cpp
+++ b/src/storm-parsers/api/properties.cpp
@@ -17,7 +17,7 @@
namespace storm {
namespace api {
- boost::optional <std::set<std::string>> parsePropertyFilter(std::string const &propertyFilter) {
+ boost::optional<std::set<std::string>> parsePropertyFilter(std::string const& propertyFilter) {
if (propertyFilter == "all") {
return boost::none;
}
@@ -26,7 +26,7 @@ namespace storm {
return propertyNameSet;
}
- std::vector <storm::jani::Property> parseProperties(storm::parser::FormulaParser &formulaParser, std::string const &inputString, boost::optional <std::set<std::string>> const &propertyFilter) {
+ std::vector<storm::jani::Property> parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter) {
// If the given property is a file, we parse it as a file, otherwise we assume it's a property.
std::vector <storm::jani::Property> properties;
if (std::ifstream(inputString).good()) {
@@ -39,25 +39,25 @@ namespace storm {
return filterProperties(properties, propertyFilter);
}
- std::vector <storm::jani::Property> parseProperties(std::string const &inputString, boost::optional <std::set<std::string>> const &propertyFilter) {
+ std::vector<storm::jani::Property> parseProperties(std::string const& inputString, boost::optional <std::set<std::string>> const& propertyFilter) {
auto exprManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(exprManager);
return parseProperties(formulaParser, inputString, propertyFilter);
}
- std::vector <storm::jani::Property> parsePropertiesForJaniModel(std::string const &inputString, storm::jani::Model const &model, boost::optional <std::set<std::string>> const &propertyFilter) {
+ std::vector<storm::jani::Property> parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional <std::set<std::string>> const& propertyFilter) {
storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer());
auto formulas = parseProperties(formulaParser, inputString, propertyFilter);
return substituteConstantsInProperties(formulas, model.getConstantsSubstitution());
}
- std::vector <storm::jani::Property> parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional <std::set<std::string>> const &propertyFilter) {
+ std::vector<storm::jani::Property> parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional <std::set<std::string>> const& propertyFilter) {
storm::parser::FormulaParser formulaParser(program);
auto formulas = parseProperties(formulaParser, inputString, propertyFilter);
return substituteConstantsInProperties(formulas, program.getConstantsSubstitution());
}
- std::vector <storm::jani::Property> parsePropertiesForSymbolicModelDescription(std::string const &inputString, storm::storage::SymbolicModelDescription const &modelDescription, boost::optional <std::set<std::string>> const &propertyFilter) {
+ std::vector<storm::jani::Property> parsePropertiesForSymbolicModelDescription(std::string const& inputString, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional <std::set<std::string>> const& propertyFilter) {
std::vector <storm::jani::Property> result;
if (modelDescription.isPrismProgram()) {
result = storm::api::parsePropertiesForPrismProgram(inputString, modelDescription.asPrismProgram(), propertyFilter);
@@ -68,4 +68,4 @@ namespace storm {
return result;
}
}
-}
\ No newline at end of file
+}
diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp
index 2cd8773c9..31e436c2d 100644
--- a/src/storm-parsers/parser/FormulaParserGrammar.cpp
+++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp
@@ -133,7 +133,7 @@ namespace storm {
formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":");
formulaName.name("formula name");
- constantDefinition = (qi::lit("const") > qi::eps[qi::_a = true] > -(qi::lit("int") | qi::lit("double")[qi::_a = false]) >> identifier)[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a)];
+ constantDefinition = (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] | qi::lit("double")[qi::_a = ConstantDataType::Rational]) >> identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)];
constantDefinition.name("constant definition");
#pragma clang diagnostic push
@@ -208,15 +208,24 @@ namespace storm {
this->identifiers_.add(identifier, expression);
}
- void FormulaParserGrammar::addConstant(std::string const& name, bool integer) {
+ void FormulaParserGrammar::addConstant(std::string const& name, ConstantDataType type, boost::optional<storm::expressions::Expression> const& expression) {
STORM_LOG_ASSERT(manager, "Mutable expression manager required to define new constants.");
storm::expressions::Variable newVariable;
- if (integer) {
+ STORM_LOG_THROW(!manager->hasVariable(name), storm::exceptions::WrongFormatException, "Invalid constant definition '" << name << "' in property: variable already exists.");
+
+ if (type == ConstantDataType::Bool) {
+ newVariable = manager->declareBooleanVariable(name);
+ } else if (type == ConstantDataType::Integer) {
newVariable = manager->declareIntegerVariable(name);
} else {
newVariable = manager->declareRationalVariable(name);
}
- addIdentifierExpression(name, newVariable);
+
+ if (expression) {
+ addIdentifierExpression(name, expression.get());
+ } else {
+ addIdentifierExpression(name, newVariable);
+ }
}
bool FormulaParserGrammar::areConstantDefinitionsAllowed() const {
diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h
index c9d5ae020..c9f7e8327 100644
--- a/src/storm-parsers/parser/FormulaParserGrammar.h
+++ b/src/storm-parsers/parser/FormulaParserGrammar.h
@@ -145,7 +145,11 @@ namespace storm {
qi::rule<Iterator, std::vector<storm::jani::Property>(), Skipper> start;
- qi::rule<Iterator, qi::unused_type(), qi::locals<bool>, Skipper> constantDefinition;
+ enum class ConstantDataType {
+ Bool, Integer, Rational
+ };
+
+ qi::rule<Iterator, qi::unused_type(), qi::locals<ConstantDataType>, Skipper> constantDefinition;
qi::rule<Iterator, std::string(), Skipper> identifier;
qi::rule<Iterator, std::string(), Skipper> formulaName;
@@ -197,7 +201,7 @@ namespace storm {
boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
bool areConstantDefinitionsAllowed() const;
- void addConstant(std::string const& name, bool integer);
+ void addConstant(std::string const& name, ConstantDataType type, boost::optional<storm::expressions::Expression> const& expression);
void addProperty(std::vector<storm::jani::Property>& properties, boost::optional<std::string> const& name, std::shared_ptr<storm::logic::Formula const> const& formula);
std::shared_ptr<storm::logic::TimeBoundReference> createTimeBoundReference(storm::logic::TimeBoundType const& type, boost::optional<std::string> const& rewardModelName) const;
diff --git a/src/storm/api/properties.cpp b/src/storm/api/properties.cpp
index e5010d8b9..b1e36af86 100644
--- a/src/storm/api/properties.cpp
+++ b/src/storm/api/properties.cpp
@@ -13,7 +13,6 @@
namespace storm {
namespace api {
-
std::vector<storm::jani::Property> substituteConstantsInProperties(std::vector<storm::jani::Property> const& properties, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
std::vector<storm::jani::Property> preprocessedProperties;
for (auto const& property : properties) {
@@ -58,5 +57,6 @@ namespace storm {
}
return formulas;
}
+
}
}
diff --git a/src/storm/logic/AtomicExpressionFormula.cpp b/src/storm/logic/AtomicExpressionFormula.cpp
index b7af29bfb..6fe7b6fdb 100644
--- a/src/storm/logic/AtomicExpressionFormula.cpp
+++ b/src/storm/logic/AtomicExpressionFormula.cpp
@@ -24,6 +24,10 @@ namespace storm {
atomicExpressionFormulas.push_back(std::dynamic_pointer_cast<AtomicExpressionFormula const>(this->shared_from_this()));
}
+ void AtomicExpressionFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+ expression.gatherVariables(usedVariables);
+ }
+
std::ostream& AtomicExpressionFormula::writeToStream(std::ostream& out) const {
out << expression;
return out;
diff --git a/src/storm/logic/AtomicExpressionFormula.h b/src/storm/logic/AtomicExpressionFormula.h
index bf3a2982f..21168493b 100644
--- a/src/storm/logic/AtomicExpressionFormula.h
+++ b/src/storm/logic/AtomicExpressionFormula.h
@@ -22,7 +22,8 @@ namespace storm {
virtual std::ostream& writeToStream(std::ostream& out) const override;
virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
-
+ virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
+
private:
// The atomic expression represented by this node in the formula tree.
storm::expressions::Expression expression;
diff --git a/src/storm/logic/BinaryPathFormula.cpp b/src/storm/logic/BinaryPathFormula.cpp
index b6db33e01..5de44c0c5 100644
--- a/src/storm/logic/BinaryPathFormula.cpp
+++ b/src/storm/logic/BinaryPathFormula.cpp
@@ -33,6 +33,11 @@ namespace storm {
this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels);
}
+ void BinaryPathFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+ this->getLeftSubformula().gatherUsedVariables(usedVariables);
+ this->getRightSubformula().gatherUsedVariables(usedVariables);
+ }
+
bool BinaryPathFormula::hasQualitativeResult() const {
return false;
}
diff --git a/src/storm/logic/BinaryPathFormula.h b/src/storm/logic/BinaryPathFormula.h
index 82a93d344..13f2573cc 100644
--- a/src/storm/logic/BinaryPathFormula.h
+++ b/src/storm/logic/BinaryPathFormula.h
@@ -23,7 +23,8 @@ namespace storm {
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 void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
+
virtual bool hasQualitativeResult() const override;
virtual bool hasQuantitativeResult() const override;
diff --git a/src/storm/logic/BinaryStateFormula.cpp b/src/storm/logic/BinaryStateFormula.cpp
index 83535081c..b2f45e269 100644
--- a/src/storm/logic/BinaryStateFormula.cpp
+++ b/src/storm/logic/BinaryStateFormula.cpp
@@ -32,5 +32,10 @@ namespace storm {
this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels);
this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels);
}
+
+ void BinaryStateFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+ this->getLeftSubformula().gatherUsedVariables(usedVariables);
+ this->getRightSubformula().gatherUsedVariables(usedVariables);
+ }
}
}
diff --git a/src/storm/logic/BinaryStateFormula.h b/src/storm/logic/BinaryStateFormula.h
index 85c996342..67c85a0b1 100644
--- a/src/storm/logic/BinaryStateFormula.h
+++ b/src/storm/logic/BinaryStateFormula.h
@@ -21,6 +21,7 @@ namespace storm {
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 void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
private:
std::shared_ptr<Formula const> leftSubformula;
diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp
index 6054e7cd3..e06327511 100644
--- a/src/storm/logic/BoundedUntilFormula.cpp
+++ b/src/storm/logic/BoundedUntilFormula.cpp
@@ -84,6 +84,22 @@ namespace storm {
}
}
+ void BoundedUntilFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+ if (hasMultiDimensionalSubformulas()) {
+ for (unsigned i = 0; i < this->getDimension(); ++i) {
+ this->getLeftSubformula(i).gatherUsedVariables(usedVariables);
+ this->getRightSubformula(i).gatherUsedVariables(usedVariables);
+ this->getLowerBound(i).gatherVariables(usedVariables);
+ this->getUpperBound(i).gatherVariables(usedVariables);
+ }
+ } else {
+ this->getLeftSubformula().gatherUsedVariables(usedVariables);
+ this->getRightSubformula().gatherUsedVariables(usedVariables);
+ this->getLowerBound().gatherVariables(usedVariables);
+ this->getUpperBound().gatherVariables(usedVariables);
+ }
+ }
+
bool BoundedUntilFormula::hasQualitativeResult() const {
return false;
}
diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h
index eed5c5220..5ae10e8b5 100644
--- a/src/storm/logic/BoundedUntilFormula.h
+++ b/src/storm/logic/BoundedUntilFormula.h
@@ -24,7 +24,8 @@ namespace storm {
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 void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
+
virtual bool hasQualitativeResult() const override;
virtual bool hasQuantitativeResult() const override;
diff --git a/src/storm/logic/ConditionalFormula.cpp b/src/storm/logic/ConditionalFormula.cpp
index 31043e07b..a02af1877 100644
--- a/src/storm/logic/ConditionalFormula.cpp
+++ b/src/storm/logic/ConditionalFormula.cpp
@@ -49,6 +49,11 @@ namespace storm {
this->getConditionFormula().gatherReferencedRewardModels(referencedRewardModels);
}
+ void ConditionalFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+ this->getSubformula().gatherUsedVariables(usedVariables);
+ this->getConditionFormula().gatherUsedVariables(usedVariables);
+ }
+
bool ConditionalFormula::hasQualitativeResult() const {
return false;
}
diff --git a/src/storm/logic/ConditionalFormula.h b/src/storm/logic/ConditionalFormula.h
index 30af1a3a6..3a32b3463 100644
--- a/src/storm/logic/ConditionalFormula.h
+++ b/src/storm/logic/ConditionalFormula.h
@@ -28,7 +28,8 @@ namespace storm {
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 void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
+
virtual bool hasQualitativeResult() const override;
virtual bool hasQuantitativeResult() const override;
diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp
index bbf21cbf0..7abcdc7e4 100644
--- a/src/storm/logic/CumulativeRewardFormula.cpp
+++ b/src/storm/logic/CumulativeRewardFormula.cpp
@@ -47,6 +47,12 @@ namespace storm {
}
}
+ void CumulativeRewardFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+ for (unsigned i = 0; i < this->getDimension(); ++i) {
+ this->getBound(i).gatherVariables(usedVariables);
+ }
+ }
+
TimeBoundReference const& CumulativeRewardFormula::getTimeBoundReference() const {
STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
return getTimeBoundReference(0);
diff --git a/src/storm/logic/CumulativeRewardFormula.h b/src/storm/logic/CumulativeRewardFormula.h
index 4c436037e..cccd1ac9e 100644
--- a/src/storm/logic/CumulativeRewardFormula.h
+++ b/src/storm/logic/CumulativeRewardFormula.h
@@ -24,7 +24,8 @@ namespace storm {
virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
-
+ virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
+
virtual std::ostream& writeToStream(std::ostream& out) const override;
TimeBoundReference const& getTimeBoundReference() const;
diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index 3f871908e..62030b0ec 100644
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@@ -431,6 +431,12 @@ namespace storm {
return result;
}
+ std::set<storm::expressions::Variable> Formula::getUsedVariables() const {
+ std::set<storm::expressions::Variable> usedVariables;
+ this->gatherUsedVariables(usedVariables);
+ return usedVariables;
+ }
+
std::set<std::string> Formula::getReferencedRewardModels() const {
std::set<std::string> referencedRewardModels;
this->gatherReferencedRewardModels(referencedRewardModels);
@@ -480,7 +486,11 @@ namespace storm {
void Formula::gatherReferencedRewardModels(std::set<std::string>&) const {
return;
}
-
+
+ void Formula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+ return;
+ }
+
std::string Formula::toString() const {
std::stringstream str2;
writeToStream(str2);
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index a76dd0ef7..c9180b742 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -192,6 +192,7 @@ namespace storm {
std::vector<std::shared_ptr<AtomicExpressionFormula const>> getAtomicExpressionFormulas() const;
std::vector<std::shared_ptr<AtomicLabelFormula const>> getAtomicLabelFormulas() const;
+ std::set<storm::expressions::Variable> getUsedVariables() const;
std::set<std::string> getReferencedRewardModels() const;
std::shared_ptr<Formula const> asSharedPointer();
@@ -218,7 +219,8 @@ namespace storm {
virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const;
virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const;
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const;
-
+ virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const;
+
private:
// Currently empty.
};
diff --git a/src/storm/logic/InstantaneousRewardFormula.cpp b/src/storm/logic/InstantaneousRewardFormula.cpp
index f702ca578..37bdee1c9 100644
--- a/src/storm/logic/InstantaneousRewardFormula.cpp
+++ b/src/storm/logic/InstantaneousRewardFormula.cpp
@@ -60,6 +60,10 @@ namespace storm {
return value;
}
+ void InstantaneousRewardFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+ this->getBound().gatherVariables(usedVariables);
+ }
+
void InstantaneousRewardFormula::checkNoVariablesInBound(storm::expressions::Expression const& bound) {
STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-instant '" << bound << "' as it contains undefined constants.");
}
diff --git a/src/storm/logic/InstantaneousRewardFormula.h b/src/storm/logic/InstantaneousRewardFormula.h
index ee9b5b28f..69e5dd38f 100644
--- a/src/storm/logic/InstantaneousRewardFormula.h
+++ b/src/storm/logic/InstantaneousRewardFormula.h
@@ -35,6 +35,8 @@ namespace storm {
template <typename ValueType>
ValueType getBound() const;
+ virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
+
private:
static void checkNoVariablesInBound(storm::expressions::Expression const& bound);
diff --git a/src/storm/logic/OperatorFormula.cpp b/src/storm/logic/OperatorFormula.cpp
index 3b0fbcd1c..40ac6d307 100644
--- a/src/storm/logic/OperatorFormula.cpp
+++ b/src/storm/logic/OperatorFormula.cpp
@@ -85,6 +85,10 @@ namespace storm {
return !this->hasBound();
}
+ void OperatorFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+ this->getThreshold().gatherVariables(usedVariables);
+ }
+
std::ostream& OperatorFormula::writeToStream(std::ostream& out) const {
if (hasOptimalityType()) {
out << (getOptimalityType() == OptimizationDirection::Minimize ? "min" : "max");
diff --git a/src/storm/logic/OperatorFormula.h b/src/storm/logic/OperatorFormula.h
index 502cfaec6..a396f21ac 100644
--- a/src/storm/logic/OperatorFormula.h
+++ b/src/storm/logic/OperatorFormula.h
@@ -49,6 +49,8 @@ namespace storm {
virtual bool hasQualitativeResult() const override;
virtual bool hasQuantitativeResult() const override;
+ virtual void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
+
virtual std::ostream& writeToStream(std::ostream& out) const override;
protected:
diff --git a/src/storm/logic/UnaryPathFormula.cpp b/src/storm/logic/UnaryPathFormula.cpp
index fd9dd6ae8..6f3404d4f 100644
--- a/src/storm/logic/UnaryPathFormula.cpp
+++ b/src/storm/logic/UnaryPathFormula.cpp
@@ -26,6 +26,10 @@ namespace storm {
this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
}
+ void UnaryPathFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+ this->getSubformula().gatherUsedVariables(usedVariables);
+ }
+
bool UnaryPathFormula::hasQualitativeResult() const {
return false;
}
diff --git a/src/storm/logic/UnaryPathFormula.h b/src/storm/logic/UnaryPathFormula.h
index d1fd8e2c9..b78c3d6a3 100644
--- a/src/storm/logic/UnaryPathFormula.h
+++ b/src/storm/logic/UnaryPathFormula.h
@@ -22,7 +22,8 @@ namespace storm {
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 void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
+
virtual bool hasQualitativeResult() const override;
virtual bool hasQuantitativeResult() const override;
diff --git a/src/storm/logic/UnaryStateFormula.cpp b/src/storm/logic/UnaryStateFormula.cpp
index e46d3f345..b253ead87 100644
--- a/src/storm/logic/UnaryStateFormula.cpp
+++ b/src/storm/logic/UnaryStateFormula.cpp
@@ -27,6 +27,10 @@ namespace storm {
void UnaryStateFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
}
+
+ void UnaryStateFormula::gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const {
+ this->getSubformula().gatherUsedVariables(usedVariables);
+ }
}
}
diff --git a/src/storm/logic/UnaryStateFormula.h b/src/storm/logic/UnaryStateFormula.h
index ae26700a2..490e15d3d 100644
--- a/src/storm/logic/UnaryStateFormula.h
+++ b/src/storm/logic/UnaryStateFormula.h
@@ -20,6 +20,7 @@ namespace storm {
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 void gatherUsedVariables(std::set<storm::expressions::Variable>& usedVariables) const override;
private:
std::shared_ptr<Formula const> subformula;
diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp
index 1d31f4c6f..56eaa30ff 100644
--- a/src/storm/storage/expressions/Expression.cpp
+++ b/src/storm/storage/expressions/Expression.cpp
@@ -127,6 +127,10 @@ namespace storm {
return result;
}
+ void Expression::gatherVariables(std::set<storm::expressions::Variable>& variables) const {
+ this->getBaseExpression().gatherVariables(variables);
+ }
+
bool Expression::containsVariable(std::set<storm::expressions::Variable> const& variables) const {
std::set<storm::expressions::Variable> appearingVariables = this->getVariables();
std::set<storm::expressions::Variable> intersection;
diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h
index 5778f7214..262e09208 100644
--- a/src/storm/storage/expressions/Expression.h
+++ b/src/storm/storage/expressions/Expression.h
@@ -262,6 +262,14 @@ namespace storm {
*/
std::set<storm::expressions::Variable> getVariables() const;
+ /*!
+ * Retrieves the set of all variables that appear in the expression. These variables are added to the given
+ * set.
+ *
+ * @param variables The set to which to add the variables.
+ */
+ void gatherVariables(std::set<storm::expressions::Variable>& variables) const;
+
/*!
* Retrieves whether the expression contains any of the given variables.
*