diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index 7e53dde92..0909b25de 100644
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@@ -220,17 +220,18 @@ namespace storm {
}
// Then proceed to parsing the property (if given), since the model we are building may depend on the property.
- std::vector<std::shared_ptr<const storm::logic::Formula>> formulas;
+ std::vector<std::shared_ptr<storm::logic::Formula>> parsedFormulas;
if (settings.isPropertySet()) {
std::string properties = settings.getProperty();
if(program) {
- formulas = storm::parseFormulasForProgram(properties, program.get());
+ parsedFormulas = storm::parseFormulasForProgram(properties, program.get());
} else {
- formulas = storm::parseFormulasForExplicit(properties);
+ parsedFormulas = storm::parseFormulasForExplicit(properties);
}
}
+ std::vector<std::shared_ptr<const storm::logic::Formula>> formulas(parsedFormulas.begin(), parsedFormulas.end());
if (settings.isSymbolicSet()) {
#ifdef STORM_HAVE_CARL
diff --git a/src/logic/ComparisonType.h b/src/logic/ComparisonType.h
index ccfff25b6..b91b2432b 100644
--- a/src/logic/ComparisonType.h
+++ b/src/logic/ComparisonType.h
@@ -5,16 +5,17 @@
namespace storm {
namespace logic {
- enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual };
-
- inline bool isStrict(ComparisonType t) {
- return (t == ComparisonType::Less || t == ComparisonType::Greater);
- }
-
- inline bool isLowerBound(ComparisonType t) {
- return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual);
- }
- std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType);
+ enum class ComparisonType { Less, LessEqual, Greater, GreaterEqual };
+
+ inline bool isStrict(ComparisonType t) {
+ return (t == ComparisonType::Less || t == ComparisonType::Greater);
+ }
+
+ inline bool isLowerBound(ComparisonType t) {
+ return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual);
+ }
+
+ std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType);
}
}
diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp
index 5997c957d..39fad071d 100644
--- a/src/logic/OperatorFormula.cpp
+++ b/src/logic/OperatorFormula.cpp
@@ -10,14 +10,22 @@ namespace storm {
return static_cast<bool>(bound);
}
- ComparisonType const& OperatorFormula::getComparisonType() const {
+ ComparisonType OperatorFormula::getComparisonType() const {
return comparisonType.get();
}
+ void OperatorFormula::setComparisonType(ComparisonType t) {
+ comparisonType = boost::optional<ComparisonType>(t);
+ }
+
double OperatorFormula::getBound() const {
return bound.get();
}
+ void OperatorFormula::setBound(double b) {
+ bound = boost::optional<double>(b);
+ }
+
bool OperatorFormula::hasOptimalityType() const {
return static_cast<bool>(optimalityType);
}
diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h
index 8bdc14d21..a059ddb8b 100644
--- a/src/logic/OperatorFormula.h
+++ b/src/logic/OperatorFormula.h
@@ -18,8 +18,10 @@ namespace storm {
}
bool hasBound() const;
- ComparisonType const& getComparisonType() const;
+ ComparisonType getComparisonType() const;
+ void setComparisonType(ComparisonType);
double getBound() const;
+ void setBound(double);
bool hasOptimalityType() const;
OptimizationDirection const& getOptimalityType() const;
diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp
index 96ceee55f..e3c0c9718 100644
--- a/src/parser/FormulaParser.cpp
+++ b/src/parser/FormulaParser.cpp
@@ -10,7 +10,7 @@
namespace storm {
namespace parser {
- class FormulaParserGrammar : public qi::grammar<Iterator, std::vector<std::shared_ptr<const storm::logic::Formula>>(), Skipper> {
+ class FormulaParserGrammar : public qi::grammar<Iterator, std::vector<std::shared_ptr<storm::logic::Formula>>(), Skipper> {
public:
FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager = std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager()));
@@ -95,66 +95,66 @@ namespace storm {
// they are to be replaced with.
qi::symbols<char, storm::expressions::Expression> identifiers_;
- qi::rule<Iterator, std::vector<std::shared_ptr<const storm::logic::Formula>>(), Skipper> start;
+ qi::rule<Iterator, std::vector<std::shared_ptr<storm::logic::Formula>>(), Skipper> start;
qi::rule<Iterator, std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> probabilityOperator;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> rewardOperator;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> expectedTimeOperator;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> longRunAverageOperator;
-
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> simpleFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> stateFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> pathFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> pathFormulaWithoutUntil;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> simplePathFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> atomicStateFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> operatorFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> probabilityOperator;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> rewardOperator;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> expectedTimeOperator;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> longRunAverageOperator;
+
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> simpleFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> stateFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> pathFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> pathFormulaWithoutUntil;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> simplePathFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> atomicStateFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> operatorFormula;
qi::rule<Iterator, std::string(), Skipper> label;
qi::rule<Iterator, std::string(), Skipper> rewardModelName;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> andStateFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> orStateFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> notStateFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> labelFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> expressionFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), qi::locals<bool>, Skipper> booleanLiteralFormula;
-
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> conditionalFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> eventuallyFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> nextFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> globallyFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> untilFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> andStateFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> orStateFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> notStateFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> labelFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> expressionFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), qi::locals<bool>, Skipper> booleanLiteralFormula;
+
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> conditionalFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> eventuallyFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> nextFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> globallyFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> untilFormula;
qi::rule<Iterator, boost::variant<std::pair<double, double>, uint_fast64_t>(), Skipper> timeBound;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> rewardPathFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> cumulativeRewardFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> reachabilityRewardFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> instantaneousRewardFormula;
- qi::rule<Iterator, std::shared_ptr<const storm::logic::Formula>(), Skipper> longRunAverageRewardFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> rewardPathFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> cumulativeRewardFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> reachabilityRewardFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> instantaneousRewardFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> longRunAverageRewardFormula;
// Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
// Methods that actually create the expression objects.
- std::shared_ptr<const storm::logic::Formula> createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
- std::shared_ptr<const storm::logic::Formula> createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
- std::shared_ptr<const storm::logic::Formula> createReachabilityRewardFormula(std::shared_ptr<const storm::logic::Formula> const& stateFormula) const;
- std::shared_ptr<const storm::logic::Formula> createLongRunAverageRewardFormula() const;
- std::shared_ptr<const storm::logic::Formula> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;
- std::shared_ptr<const storm::logic::Formula> createBooleanLiteralFormula(bool literal) const;
- std::shared_ptr<const storm::logic::Formula> createAtomicLabelFormula(std::string const& label) const;
- std::shared_ptr<const storm::logic::Formula> createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<const storm::logic::Formula> const& subformula) const;
- std::shared_ptr<const storm::logic::Formula> createGloballyFormula(std::shared_ptr<const storm::logic::Formula> const& subformula) const;
- std::shared_ptr<const storm::logic::Formula> createNextFormula(std::shared_ptr<const storm::logic::Formula> const& subformula) const;
- std::shared_ptr<const storm::logic::Formula> createUntilFormula(std::shared_ptr<const storm::logic::Formula> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<const storm::logic::Formula> const& rightSubformula);
- std::shared_ptr<const storm::logic::Formula> createConditionalFormula(std::shared_ptr<const storm::logic::Formula> const& leftSubformula, std::shared_ptr<const storm::logic::Formula> const& rightSubformula) const;
- std::shared_ptr<const storm::logic::Formula> createLongRunAverageOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<const storm::logic::Formula> const& subformula) const;
- std::shared_ptr<const storm::logic::Formula> createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<const storm::logic::Formula> const& subformula) const;
- std::shared_ptr<const storm::logic::Formula> createExpectedTimeOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<const storm::logic::Formula> const& subformula) const;
- std::shared_ptr<const storm::logic::Formula> createProbabilityOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<const storm::logic::Formula> const& subformula);
- std::shared_ptr<const storm::logic::Formula> createBinaryBooleanStateFormula(std::shared_ptr<const storm::logic::Formula> const& leftSubformula, std::shared_ptr<const storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
- std::shared_ptr<const storm::logic::Formula> createUnaryBooleanStateFormula(std::shared_ptr<const storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
+ std::shared_ptr<storm::logic::Formula> createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
+ std::shared_ptr<storm::logic::Formula> createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
+ std::shared_ptr<storm::logic::Formula> createReachabilityRewardFormula(std::shared_ptr<storm::logic::Formula> const& stateFormula) const;
+ std::shared_ptr<storm::logic::Formula> createLongRunAverageRewardFormula() const;
+ std::shared_ptr<storm::logic::Formula> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;
+ std::shared_ptr<storm::logic::Formula> createBooleanLiteralFormula(bool literal) const;
+ std::shared_ptr<storm::logic::Formula> createAtomicLabelFormula(std::string const& label) const;
+ std::shared_ptr<storm::logic::Formula> createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+ std::shared_ptr<storm::logic::Formula> createGloballyFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
+ std::shared_ptr<storm::logic::Formula> createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const;
+ std::shared_ptr<storm::logic::Formula> createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula);
+ std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const;
+ std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+ std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+ std::shared_ptr<storm::logic::Formula> createExpectedTimeOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+ std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
+ std::shared_ptr<storm::logic::Formula> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
+ std::shared_ptr<storm::logic::Formula> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
// An error handler function.
phoenix::function<SpiritErrorHandler> handler;
@@ -182,18 +182,18 @@ namespace storm {
return *this;
}
- std::shared_ptr<const storm::logic::Formula> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const {
- std::vector<std::shared_ptr<const storm::logic::Formula>> formulas = parseFromString(formulaString);
+ std::shared_ptr<storm::logic::Formula> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) const {
+ std::vector<std::shared_ptr<storm::logic::Formula>> formulas = parseFromString(formulaString);
STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead.");
return formulas.front();
}
- std::vector<std::shared_ptr<const storm::logic::Formula>> FormulaParser::parseFromFile(std::string const& filename) const {
+ std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromFile(std::string const& filename) const {
// Open file and initialize result.
std::ifstream inputFileStream(filename, std::ios::in);
STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
- std::vector<std::shared_ptr<const storm::logic::Formula>> formulas;
+ std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
// Now try to parse the contents of the file.
try {
@@ -210,13 +210,13 @@ namespace storm {
return formulas;
}
- std::vector<std::shared_ptr<const storm::logic::Formula>> FormulaParser::parseFromString(std::string const& formulaString) const {
+ std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromString(std::string const& formulaString) const {
PositionIteratorType first(formulaString.begin());
PositionIteratorType iter = first;
PositionIteratorType last(formulaString.end());
// Create empty result;
- std::vector<std::shared_ptr<const storm::logic::Formula>> result;
+ std::vector<std::shared_ptr<storm::logic::Formula>> result;
// Create grammar.
try {
@@ -390,108 +390,108 @@ namespace storm {
this->identifiers_.add(identifier, expression);
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const {
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const {
if (timeBound.which() == 0) {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
} else {
double timeBoundAsDouble = boost::get<double>(timeBound);
STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound.");
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(timeBoundAsDouble)));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(timeBoundAsDouble)));
}
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const {
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const {
if (timeBound.which() == 0) {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
} else {
double timeBoundAsDouble = boost::get<double>(timeBound);
STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound.");
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(timeBoundAsDouble)));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(timeBoundAsDouble)));
}
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createReachabilityRewardFormula(std::shared_ptr<const storm::logic::Formula> const& stateFormula) const {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::ReachabilityRewardFormula(stateFormula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createReachabilityRewardFormula(std::shared_ptr<storm::logic::Formula> const& stateFormula) const {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::ReachabilityRewardFormula(stateFormula));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createLongRunAverageRewardFormula() const {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::LongRunAverageRewardFormula());
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createLongRunAverageRewardFormula() const {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageRewardFormula());
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const {
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const {
STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::WrongFormatException, "Expected expression of boolean type.");
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::AtomicExpressionFormula(expression));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::AtomicExpressionFormula(expression));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::BooleanLiteralFormula(literal));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::BooleanLiteralFormula(literal));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::AtomicLabelFormula(label));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::AtomicLabelFormula(label));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<const storm::logic::Formula> const& subformula) const {
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createEventuallyFormula(boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& subformula) const {
if (timeBound) {
if (timeBound.get().which() == 0) {
std::pair<double, double> const& bounds = boost::get<std::pair<double, double>>(timeBound.get());
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second));
} else {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get()))));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get()))));
}
} else {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::EventuallyFormula(subformula));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::EventuallyFormula(subformula));
}
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createGloballyFormula(std::shared_ptr<const storm::logic::Formula> const& subformula) const {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::GloballyFormula(subformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createGloballyFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::GloballyFormula(subformula));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createNextFormula(std::shared_ptr<const storm::logic::Formula> const& subformula) const {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::NextFormula(subformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::NextFormula(subformula));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createUntilFormula(std::shared_ptr<const storm::logic::Formula> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<const storm::logic::Formula> const& rightSubformula) {
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, boost::optional<boost::variant<std::pair<double, double>, uint_fast64_t>> const& timeBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula) {
if (timeBound) {
if (timeBound.get().which() == 0) {
std::pair<double, double> const& bounds = boost::get<std::pair<double, double>>(timeBound.get());
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second));
} else {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get()))));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast<uint_fast64_t>(boost::get<uint_fast64_t>(timeBound.get()))));
}
} else {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::UntilFormula(leftSubformula, rightSubformula));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::UntilFormula(leftSubformula, rightSubformula));
}
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createConditionalFormula(std::shared_ptr<const storm::logic::Formula> const& leftSubformula, std::shared_ptr<const storm::logic::Formula> const& rightSubformula) const {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<const storm::logic::Formula> const& subformula) const {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<const storm::logic::Formula> const& subformula) const {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::RewardOperatorFormula(rewardModelName, std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(rewardModelName, std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<const storm::logic::Formula> const& subformula) const {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<const storm::logic::Formula> const& subformula) {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr<const storm::logic::Formula> const& leftSubformula, std::shared_ptr<const storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula));
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula));
}
- std::shared_ptr<const storm::logic::Formula> FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr<const storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType) {
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType) {
if (operatorType) {
- return std::shared_ptr<const storm::logic::Formula>(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula));
+ return std::shared_ptr<storm::logic::Formula>(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula));
} else {
return subformula;
}
diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h
index b791e96fc..68ee3c5ab 100644
--- a/src/parser/FormulaParser.h
+++ b/src/parser/FormulaParser.h
@@ -31,7 +31,7 @@ namespace storm {
* @param formulaString The formula as a string.
* @return The resulting formula.
*/
- std::shared_ptr<const storm::logic::Formula> parseSingleFormulaFromString(std::string const& formulaString) const;
+ std::shared_ptr<storm::logic::Formula> parseSingleFormulaFromString(std::string const& formulaString) const;
/*!
* Parses the formula given by the provided string.
@@ -39,7 +39,7 @@ namespace storm {
* @param formulaString The formula as a string.
* @return The contained formulas.
*/
- std::vector<std::shared_ptr<const storm::logic::Formula>> parseFromString(std::string const& formulaString) const;
+ std::vector<std::shared_ptr<storm::logic::Formula>> parseFromString(std::string const& formulaString) const;
/*!
* Parses the formulas in the given file.
@@ -47,7 +47,7 @@ namespace storm {
* @param filename The name of the file to parse.
* @return The contained formulas.
*/
- std::vector<std::shared_ptr<const storm::logic::Formula>> parseFromFile(std::string const& filename) const;
+ std::vector<std::shared_ptr<storm::logic::Formula>> parseFromFile(std::string const& filename) const;
/*!
* Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used
diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp
index 9a00c8f2c..a690af6f8 100644
--- a/src/utility/storm.cpp
+++ b/src/utility/storm.cpp
@@ -19,7 +19,7 @@ namespace storm {
* @param FormulaParser
* @return The formulas.
*/
- std::vector<std::shared_ptr<const storm::logic::Formula>> parseFormulas(storm::parser::FormulaParser & formulaParser, std::string const& inputString) {
+ std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulas(storm::parser::FormulaParser & formulaParser, std::string const& inputString) {
// If the given property looks like a file (containing a dot and there exists a file with that name),
// we try to parse it as a file, otherwise we assume it's a property.
if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) {
@@ -29,12 +29,12 @@ namespace storm {
}
}
- std::vector<std::shared_ptr<const storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString) {
+ std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString) {
storm::parser::FormulaParser formulaParser;
return parseFormulas(formulaParser, inputString);
}
- std::vector<std::shared_ptr<const storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program) {
+ std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program) {
storm::parser::FormulaParser formulaParser(program);
return parseFormulas(formulaParser, inputString);
}
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 6e4e82a18..7ffba8c85 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -81,8 +81,8 @@ namespace storm {
}
storm::prism::Program parseProgram(std::string const& path);
- std::vector<std::shared_ptr<const storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString);
- std::vector<std::shared_ptr<const storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
+ std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString);
+ std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>