diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index f4efe7195..fcffe1344 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -106,17 +106,17 @@ namespace storm {
}
template <typename ValueType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels() {
+ ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() {
// Intentionally left empty.
}
template <typename ValueType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()) {
+ ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates() {
this->preserveFormula(formula);
}
template <typename ValueType, typename IndexType>
- ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels() {
+ ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
this->buildAllLabels = true;
@@ -124,6 +124,33 @@ namespace storm {
for (auto const& formula : formulas) {
this->preserveFormula(*formula);
}
+ if (formulas.size() == 1) {
+ this->setTerminalStatesFromFormula(*formulas.front());
+ }
+ }
+ }
+
+ template <typename ValueType, typename IndexType>
+ void ExplicitPrismModelBuilder<ValueType, IndexType>::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) {
+ if (formula.isAtomicExpressionFormula()) {
+ terminalStates = formula.asAtomicExpressionFormula().getExpression();
+ } else if (formula.isAtomicLabelFormula()) {
+ terminalStates = formula.asAtomicLabelFormula().getLabel();
+ } else if (formula.isEventuallyFormula()) {
+ storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula();
+ if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) {
+ this->setTerminalStatesFromFormula(sub);
+ }
+ } else if (formula.isUntilFormula()) {
+ storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula();
+ if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) {
+ this->setTerminalStatesFromFormula(right);
+ }
+ } else if (formula.isProbabilityOperatorFormula()) {
+ storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula();
+ if (sub.isEventuallyFormula() || sub.isUntilFormula()) {
+ this->setTerminalStatesFromFormula(sub);
+ }
}
}
@@ -152,6 +179,9 @@ namespace storm {
// Extract all the expressions used in the formula.
std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula.getAtomicExpressionFormulas();
for (auto const& formula : atomicExpressionFormulas) {
+ if (!expressionLabels) {
+ expressionLabels = std::vector<storm::expressions::Expression>();
+ }
expressionLabels.get().push_back(formula.get()->getExpression());
}
}
@@ -528,7 +558,7 @@ namespace storm {
}
template <typename ValueType, typename IndexType>
- boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> ExplicitPrismModelBuilder<ValueType, IndexType>::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<ValueType>>& rewardModelBuilders) {
+ boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> ExplicitPrismModelBuilder<ValueType, IndexType>::buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression) {
// Create choice labels, if requested,
boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabels;
if (commandLabels) {
@@ -579,9 +609,16 @@ namespace storm {
STORM_LOG_TRACE("Exploring state with id " << stateIndex << ".");
unpackStateIntoEvaluator(currentState, variableInformation, evaluator);
- // Retrieve all choices for the current state.
- std::vector<Choice<ValueType>> allUnlabeledChoices = getUnlabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
- std::vector<Choice<ValueType>> allLabeledChoices = getLabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
+ // If a terminal expression was given, we check whether the current state needs to be explored further.
+ std::vector<Choice<ValueType>> allUnlabeledChoices;
+ std::vector<Choice<ValueType>> allLabeledChoices;
+ if (terminalExpression && evaluator.asBool(terminalExpression.get())) {
+ // Nothing to do in this case.
+ } else {
+ // Retrieve all choices for the current state.
+ allUnlabeledChoices = getUnlabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
+ allLabeledChoices = getLabeledTransitions(program, discreteTimeModel, stateInformation, variableInformation, currentState, commandLabels, evaluator, stateQueue, comparator);
+ }
uint_fast64_t totalNumberOfChoices = allUnlabeledChoices.size() + allLabeledChoices.size();
@@ -890,7 +927,18 @@ namespace storm {
rewardModelBuilders.emplace_back(deterministicModel, rewardModel.get().hasStateRewards(), rewardModel.get().hasStateActionRewards(), rewardModel.get().hasTransitionRewards());
}
- modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders);
+ // If we were asked to treat some states as terminal states, we cut away their transitions now.
+ boost::optional<storm::expressions::Expression> terminalExpression;
+ if (options.terminalStates) {
+ if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
+ terminalExpression = boost::get<storm::expressions::Expression>(options.terminalStates.get());
+ } else {
+ std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
+ terminalExpression = program.getLabelExpression(labelName);
+ }
+ }
+
+ modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders, terminalExpression);
modelComponents.transitionMatrix = transitionMatrixBuilder.build();
diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h
index 5fa7e363c..313b1652c 100644
--- a/src/builder/ExplicitPrismModelBuilder.h
+++ b/src/builder/ExplicitPrismModelBuilder.h
@@ -162,6 +162,16 @@ namespace storm {
*/
void preserveFormula(storm::logic::Formula const& formula);
+ /*!
+ * Analyzes the given formula and sets an expression for the states states of the model that can be
+ * treated as terminal states. Note that this may interfere with checking properties different than the
+ * one provided.
+ *
+ * @param formula The formula used to (possibly) derive an expression for the terminal states of the
+ * model.
+ */
+ void setTerminalStatesFromFormula(storm::logic::Formula const& formula);
+
// A flag that indicates whether or not command labels are to be built.
bool buildCommandLabels;
@@ -182,6 +192,10 @@ namespace storm {
// An optional set of expressions for which labels need to be built.
boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
+
+ // An optional expression or label that characterizes the terminal states of the model. If this is set,
+ // the outgoing transitions of these states are replaced with a self-loop.
+ boost::optional<boost::variant<storm::expressions::Expression, std::string>> terminalStates;
};
/*!
@@ -267,10 +281,11 @@ namespace storm {
* function.
* @param rewardModelBuilders A vector of reward model builders that is used to build the vector of selected
* reward models.
+ * @param terminalExpression If given, terminal states are not explored further.
* @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin
* and a vector containing the labels associated with each choice.
*/
- static boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<ValueType>>& rewardModelBuilders);
+ static boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> buildMatrices(storm::prism::Program const& program, VariableInformation const& variableInformation, std::vector<std::reference_wrapper<storm::prism::RewardModel const>> const& selectedRewardModels, StateInformation& stateInformation, bool commandLabels, bool deterministicModel, bool discreteTimeModel, storm::storage::SparseMatrixBuilder<ValueType>& transitionMatrixBuilder, std::vector<RewardModelBuilder<ValueType>>& rewardModelBuilders, boost::optional<storm::expressions::Expression> const& terminalExpression);
/*!
* Explores the state space of the given program and returns the components of the model as a result.
diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index 7a9ea6f3c..cfc88468b 100644
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@@ -224,7 +224,7 @@ namespace storm {
if (settings.isPropertySet()) {
storm::parser::FormulaParser formulaParser;
if (program) {
- storm::parser::FormulaParser formulaParser = storm::parser::FormulaParser(program.get().getManager().getSharedPointer());
+ formulaParser = storm::parser::FormulaParser(program.get().getManager().getSharedPointer());
}
// If the given property looks like a file (containing a dot and there exists a file with that name),
diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp
index 5a933a998..c67f808e0 100644
--- a/src/parser/ExpressionParser.cpp
+++ b/src/parser/ExpressionParser.cpp
@@ -5,7 +5,7 @@
namespace storm {
namespace parser {
- ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
+ ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
identifier.name("identifier");
@@ -144,7 +144,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
- return manager.boolean(false);
+ return manager->boolean(false);
}
storm::expressions::Expression ExpressionParser::createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -159,7 +159,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
- return manager.boolean(false);
+ return manager->boolean(false);
}
storm::expressions::Expression ExpressionParser::createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -173,7 +173,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
- return manager.boolean(false);
+ return manager->boolean(false);
}
storm::expressions::Expression ExpressionParser::createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -190,7 +190,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
- return manager.boolean(false);
+ return manager->boolean(false);
}
storm::expressions::Expression ExpressionParser::createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -205,7 +205,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
- return manager.boolean(false);
+ return manager->boolean(false);
}
storm::expressions::Expression ExpressionParser::createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -220,7 +220,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
- return manager.boolean(false);
+ return manager->boolean(false);
}
storm::expressions::Expression ExpressionParser::createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -235,7 +235,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
- return manager.boolean(false);
+ return manager->boolean(false);
}
storm::expressions::Expression ExpressionParser::createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -249,7 +249,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
- return manager.boolean(false);
+ return manager->boolean(false);
}
storm::expressions::Expression ExpressionParser::createUnaryExpression(boost::optional<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1) const {
@@ -268,7 +268,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
- return manager.boolean(false);
+ return manager->boolean(false);
}
storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(double value, bool& pass) const {
@@ -278,17 +278,17 @@ namespace storm {
}
if (this->createExpressions) {
- return manager.rational(value);
+ return manager->rational(value);
} else {
- return manager.boolean(false);
+ return manager->boolean(false);
}
}
storm::expressions::Expression ExpressionParser::createIntegerLiteralExpression(int value) const {
if (this->createExpressions) {
- return manager.integer(value);
+ return manager->integer(value);
} else {
- return manager.boolean(false);
+ return manager->boolean(false);
}
}
@@ -304,7 +304,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
- return manager.boolean(false);
+ return manager->boolean(false);
}
storm::expressions::Expression ExpressionParser::createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1) const {
@@ -319,7 +319,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
}
}
- return manager.boolean(false);
+ return manager->boolean(false);
}
storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const {
@@ -329,14 +329,14 @@ namespace storm {
if (expression == nullptr) {
if (allowBacktracking) {
pass = false;
- return manager.boolean(false);
+ return manager->boolean(false);
} else {
STORM_LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
}
}
return *expression;
} else {
- return manager.boolean(false);
+ return manager->boolean(false);
}
}
diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h
index 55df73e2a..19c129b4a 100644
--- a/src/parser/ExpressionParser.h
+++ b/src/parser/ExpressionParser.h
@@ -27,6 +27,9 @@ namespace storm {
*/
ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_, bool allowBacktracking = false);
+ ExpressionParser(ExpressionParser const& other) = default;
+ ExpressionParser& operator=(ExpressionParser const& other) = default;
+
/*!
* Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to
* expressions will be substituted wherever the key value appears in the parsed expression. After setting
@@ -172,7 +175,7 @@ namespace storm {
trueFalseOperatorStruct trueFalse_;
// The manager responsible for the expressions.
- storm::expressions::ExpressionManager const& manager;
+ std::shared_ptr<storm::expressions::ExpressionManager const> manager;
// A flag that indicates whether expressions should actually be generated or just a syntax check shall be
// performed.
diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp
index 5acbba56c..3aa9820d1 100644
--- a/src/parser/FormulaParser.cpp
+++ b/src/parser/FormulaParser.cpp
@@ -8,7 +8,238 @@
namespace storm {
namespace parser {
- FormulaParser::FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : FormulaParser::base_type(start), expressionParser(*manager, keywords_, true) {
+ 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()));
+
+ FormulaParserGrammar(FormulaParserGrammar const& other) = default;
+ FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = default;
+
+ /*!
+ * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used
+ * to substitute special identifiers in the formula by expressions.
+ *
+ * @param identifier The identifier that is supposed to be substituted.
+ * @param expression The expression it is to be substituted with.
+ */
+ void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression);
+
+ private:
+ struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
+ keywordsStruct() {
+ add
+ ("true", 1)
+ ("false", 2)
+ ("min", 3)
+ ("max", 4)
+ ("F", 5)
+ ("G", 6)
+ ("X", 7);
+ }
+ };
+
+ // A parser used for recognizing the keywords.
+ keywordsStruct keywords_;
+
+ struct relationalOperatorStruct : qi::symbols<char, storm::logic::ComparisonType> {
+ relationalOperatorStruct() {
+ add
+ (">=", storm::logic::ComparisonType::GreaterEqual)
+ (">", storm::logic::ComparisonType::Greater)
+ ("<=", storm::logic::ComparisonType::LessEqual)
+ ("<", storm::logic::ComparisonType::Less);
+ }
+ };
+
+ // A parser used for recognizing the operators at the "relational" precedence level.
+ relationalOperatorStruct relationalOperator_;
+
+ struct binaryBooleanOperatorStruct : qi::symbols<char, storm::logic::BinaryBooleanStateFormula::OperatorType> {
+ binaryBooleanOperatorStruct() {
+ add
+ ("&", storm::logic::BinaryBooleanStateFormula::OperatorType::And)
+ ("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or);
+ }
+ };
+
+ // A parser used for recognizing the operators at the "binary" precedence level.
+ binaryBooleanOperatorStruct binaryBooleanOperator_;
+
+ struct unaryBooleanOperatorStruct : qi::symbols<char, storm::logic::UnaryBooleanStateFormula::OperatorType> {
+ unaryBooleanOperatorStruct() {
+ add
+ ("!", storm::logic::UnaryBooleanStateFormula::OperatorType::Not);
+ }
+ };
+
+ // A parser used for recognizing the operators at the "unary" precedence level.
+ unaryBooleanOperatorStruct unaryBooleanOperator_;
+
+ struct optimalityOperatorStruct : qi::symbols<char, storm::logic::OptimalityType> {
+ optimalityOperatorStruct() {
+ add
+ ("min", storm::logic::OptimalityType::Minimize)
+ ("max", storm::logic::OptimalityType::Maximize);
+ }
+ };
+
+ // A parser used for recognizing the optimality operators.
+ optimalityOperatorStruct optimalityOperator_;
+
+ // Parser and manager used for recognizing expressions.
+ storm::parser::ExpressionParser expressionParser;
+
+ // Functor used for displaying error information.
+ struct ErrorHandler {
+ typedef qi::error_handler_result result_type;
+
+ template<typename T1, typename T2, typename T3, typename T4>
+ qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const {
+ std::stringstream whatAsString;
+ whatAsString << what;
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << whatAsString.str() << ".");
+ return qi::fail;
+ }
+ };
+
+ // An error handler function.
+ phoenix::function<ErrorHandler> handler;
+
+ // A symbol table that is a mapping from identifiers that can be used in expressions to the expressions
+ // they are to be replaced with.
+ qi::symbols<char, storm::expressions::Expression> identifiers_;
+
+ qi::rule<Iterator, std::vector<std::shared_ptr<storm::logic::Formula>>(), Skipper> start;
+
+ qi::rule<Iterator, std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>(), qi::locals<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
+ 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> steadyStateOperator;
+
+ 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<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<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;
+
+ // 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<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> 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::logic::OptimalityType>, 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::logic::OptimalityType>, 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::logic::OptimalityType>, 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::logic::OptimalityType>, 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);
+ };
+
+ FormulaParser::FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : manager(manager->getSharedPointer()), grammar(new FormulaParserGrammar(manager)) {
+ // Intentionally left empty.
+ }
+
+ FormulaParser::FormulaParser(FormulaParser const& other) : FormulaParser(other.manager) {
+ other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); });
+ }
+
+ FormulaParser& FormulaParser::operator=(FormulaParser const& other) {
+ this->manager = other.manager;
+ this->grammar = std::shared_ptr<FormulaParserGrammar>(new FormulaParserGrammar(this->manager));
+ other.identifiers_.for_each([=] (std::string const& name, storm::expressions::Expression const& expression) { this->addIdentifierExpression(name, expression); });
+ return *this;
+ }
+
+ std::shared_ptr<storm::logic::Formula> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) {
+ 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<storm::logic::Formula>> FormulaParser::parseFromFile(std::string const& filename) {
+ // 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<storm::logic::Formula>> formulas;
+
+ // Now try to parse the contents of the file.
+ try {
+ std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
+ formulas = parseFromString(fileContent);
+ } catch(std::exception& e) {
+ // In case of an exception properly close the file before passing exception.
+ inputFileStream.close();
+ throw e;
+ }
+
+ // Close the stream in case everything went smoothly and return result.
+ inputFileStream.close();
+ return formulas;
+ }
+
+ std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromString(std::string const& formulaString) {
+ PositionIteratorType first(formulaString.begin());
+ PositionIteratorType iter = first;
+ PositionIteratorType last(formulaString.end());
+
+ // Create empty result;
+ std::vector<std::shared_ptr<storm::logic::Formula>> result;
+
+ // Create grammar.
+ try {
+ // Start parsing.
+ bool succeeded = qi::phrase_parse(iter, last, *grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
+ STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse formula.");
+ STORM_LOG_DEBUG("Parsed formula successfully.");
+ } catch (qi::expectation_failure<PositionIteratorType> const& e) {
+ STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_);
+ }
+
+ return result;
+ }
+
+ void FormulaParser::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) {
+ // Record the mapping and hand it over to the grammar.
+ this->identifiers_.add(identifier, expression);
+ grammar->addIdentifierExpression(identifier, expression);
+ }
+
+ FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : FormulaParserGrammar::base_type(start), expressionParser(*manager, keywords_, true) {
// Register all variables so we can parse them in the expressions.
for (auto variableTypePair : *manager) {
identifiers_.add(variableTypePair.first.getName(), variableTypePair.first);
@@ -16,28 +247,28 @@ namespace storm {
// Set the identifier mapping to actually generate expressions.
expressionParser.setIdentifierMapping(&identifiers_);
- instantaneousRewardFormula = (qi::lit("I=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParser::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParser::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)];
+ instantaneousRewardFormula = (qi::lit("I=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)];
instantaneousRewardFormula.name("instantaneous reward formula");
- cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParser::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParser::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
+ cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
cumulativeRewardFormula.name("cumulative reward formula");
- reachabilityRewardFormula = (qi::lit("F") > stateFormula)[qi::_val = phoenix::bind(&FormulaParser::createReachabilityRewardFormula, phoenix::ref(*this), qi::_1)];
+ reachabilityRewardFormula = (qi::lit("F") > stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createReachabilityRewardFormula, phoenix::ref(*this), qi::_1)];
reachabilityRewardFormula.name("reachability reward formula");
rewardPathFormula = reachabilityRewardFormula | cumulativeRewardFormula | instantaneousRewardFormula;
rewardPathFormula.name("reward path formula");
- expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParser::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)];
+ expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)];
expressionFormula.name("expression formula");
label = qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]];
label.name("label");
- labelFormula = (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParser::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)];
+ labelFormula = (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)];
labelFormula.name("label formula");
- booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParser::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)];
+ booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)];
booleanLiteralFormula.name("boolean literal formula");
operatorFormula = probabilityOperator | rewardOperator | steadyStateOperator;
@@ -46,25 +277,25 @@ namespace storm {
atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula;
atomicStateFormula.name("atomic state formula");
- notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)];
+ notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)];
notStateFormula.name("negation formula");
- eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+ eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_2)];
eventuallyFormula.name("eventually formula");
- globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createGloballyFormula, phoenix::ref(*this), qi::_1)];
+ globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)];
globallyFormula.name("globally formula");
- nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createNextFormula, phoenix::ref(*this), qi::_1)];
+ nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
nextFormula.name("next formula");
pathFormulaWithoutUntil = eventuallyFormula | globallyFormula | nextFormula | stateFormula;
pathFormulaWithoutUntil.name("path formula");
- untilFormula = pathFormulaWithoutUntil[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParser::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
+ untilFormula = pathFormulaWithoutUntil[qi::_val = qi::_1] >> *(qi::lit("U") >> -timeBound >> pathFormulaWithoutUntil)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
untilFormula.name("until formula");
- conditionalFormula = untilFormula[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula)[qi::_val = phoenix::bind(&FormulaParser::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1)];
+ conditionalFormula = untilFormula[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1)];
conditionalFormula.name("conditional formula");
timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct<std::pair<double, double>>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct<std::pair<double, double>>(0, qi::_1)] | (qi::lit("<=") > qi::uint_)[qi::_val = qi::_1];
@@ -76,25 +307,25 @@ namespace storm {
operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::construct<std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>>(qi::_a, qi::_b, qi::_c)];
operatorInformation.name("operator information");
- steadyStateOperator = (qi::lit("LRA") > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+ steadyStateOperator = (qi::lit("LRA") > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
steadyStateOperator.name("long-run average operator");
rewardModelName = qi::lit("{\"") > label > qi::lit("\"}");
rewardModelName.name("reward model name");
- rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
+ rewardOperator = (qi::lit("R") > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
rewardOperator.name("reward operator");
- expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+ expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
expectedTimeOperator.name("expected time operator");
- probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+ probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
probabilityOperator.name("probability operator");
- andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
+ andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
andStateFormula.name("and state formula");
- orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
+ orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
orStateFormula.name("or state formula");
stateFormula = (orStateFormula);
@@ -154,60 +385,11 @@ namespace storm {
qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
}
- void FormulaParser::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) {
+ void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) {
this->identifiers_.add(identifier, expression);
}
- std::shared_ptr<storm::logic::Formula> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) {
- 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<storm::logic::Formula>> FormulaParser::parseFromFile(std::string const& filename) {
- // 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<storm::logic::Formula>> formulas;
-
- // Now try to parse the contents of the file.
- try {
- std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
- formulas = parseFromString(fileContent);
- } catch(std::exception& e) {
- // In case of an exception properly close the file before passing exception.
- inputFileStream.close();
- throw e;
- }
-
- // Close the stream in case everything went smoothly and return result.
- inputFileStream.close();
- return formulas;
- }
-
- std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromString(std::string const& formulaString) {
- PositionIteratorType first(formulaString.begin());
- PositionIteratorType iter = first;
- PositionIteratorType last(formulaString.end());
-
- // Create empty result;
- std::vector<std::shared_ptr<storm::logic::Formula>> result;
-
- // Create grammar.
- try {
- // Start parsing.
- bool succeeded = qi::phrase_parse(iter, last, *this, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result);
- STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse formula.");
- STORM_LOG_DEBUG("Parsed formula successfully.");
- } catch (qi::expectation_failure<PositionIteratorType> const& e) {
- STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, e.what_);
- }
-
- return result;
- }
-
- std::shared_ptr<storm::logic::Formula> FormulaParser::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<storm::logic::Formula>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
} else {
@@ -217,7 +399,7 @@ namespace storm {
}
}
- std::shared_ptr<storm::logic::Formula> FormulaParser::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<storm::logic::Formula>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
} else {
@@ -227,24 +409,24 @@ namespace storm {
}
}
- std::shared_ptr<storm::logic::Formula> FormulaParser::createReachabilityRewardFormula(std::shared_ptr<storm::logic::Formula> const& stateFormula) const {
+ 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<storm::logic::Formula> FormulaParser::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<storm::logic::Formula>(new storm::logic::AtomicExpressionFormula(expression));
}
- std::shared_ptr<storm::logic::Formula> FormulaParser::createBooleanLiteralFormula(bool literal) const {
+ 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<storm::logic::Formula> FormulaParser::createAtomicLabelFormula(std::string const& label) const {
+ 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<storm::logic::Formula> FormulaParser::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> 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());
@@ -257,15 +439,15 @@ namespace storm {
}
}
- std::shared_ptr<storm::logic::Formula> FormulaParser::createGloballyFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const {
+ 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<storm::logic::Formula> FormulaParser::createNextFormula(std::shared_ptr<storm::logic::Formula> const& subformula) const {
+ 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<storm::logic::Formula> FormulaParser::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> 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());
@@ -278,31 +460,31 @@ namespace storm {
}
}
- std::shared_ptr<storm::logic::Formula> FormulaParser::createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const {
+ 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<storm::logic::Formula> FormulaParser::createLongRunAverageOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, 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> FormulaParserGrammar::createLongRunAverageOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, 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<storm::logic::Formula> FormulaParser::createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::tuple<boost::optional<storm::logic::OptimalityType>, 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> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<std::string> const& rewardModelName, std::tuple<boost::optional<storm::logic::OptimalityType>, 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<storm::logic::Formula> FormulaParser::createExpectedTimeOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, 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> FormulaParserGrammar::createExpectedTimeOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, 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<storm::logic::Formula> FormulaParser::createProbabilityOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
+ std::shared_ptr<storm::logic::Formula> FormulaParserGrammar::createProbabilityOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, 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<storm::logic::Formula> FormulaParser::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> 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<storm::logic::Formula> FormulaParser::createUnaryBooleanStateFormula(std::shared_ptr<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<storm::logic::Formula>(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula));
} else {
diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h
index ad8ea8459..895d84cd5 100644
--- a/src/parser/FormulaParser.h
+++ b/src/parser/FormulaParser.h
@@ -1,5 +1,5 @@
-#ifndef STORM_PARSER_PRCTLPARSER_H_
-#define STORM_PARSER_PRCTLPARSER_H_
+#ifndef STORM_PARSER_FORMULAPARSER_H_
+#define STORM_PARSER_FORMULAPARSER_H_
#include <sstream>
@@ -12,9 +12,15 @@
namespace storm {
namespace parser {
- class FormulaParser : public qi::grammar<Iterator, std::vector<std::shared_ptr<storm::logic::Formula>>(), Skipper> {
+ // Forward-declare grammar.
+ class FormulaParserGrammar;
+
+ class FormulaParser {
public:
FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager = std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager()));
+
+ FormulaParser(FormulaParser const& other);
+ FormulaParser& operator=(FormulaParser const& other);
/*!
* Parses the formula given by the provided string.
@@ -23,7 +29,7 @@ namespace storm {
* @return The resulting formula.
*/
std::shared_ptr<storm::logic::Formula> parseSingleFormulaFromString(std::string const& formulaString);
-
+
/*!
* Parses the formula given by the provided string.
*
@@ -31,7 +37,7 @@ namespace storm {
* @return The contained formulas.
*/
std::vector<std::shared_ptr<storm::logic::Formula>> parseFromString(std::string const& formulaString);
-
+
/*!
* Parses the formulas in the given file.
*
@@ -50,151 +56,17 @@ namespace storm {
void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression);
private:
- struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
- keywordsStruct() {
- add
- ("true", 1)
- ("false", 2)
- ("min", 3)
- ("max", 4)
- ("F", 5)
- ("G", 6)
- ("X", 7);
- }
- };
-
- // A parser used for recognizing the keywords.
- keywordsStruct keywords_;
-
- struct relationalOperatorStruct : qi::symbols<char, storm::logic::ComparisonType> {
- relationalOperatorStruct() {
- add
- (">=", storm::logic::ComparisonType::GreaterEqual)
- (">", storm::logic::ComparisonType::Greater)
- ("<=", storm::logic::ComparisonType::LessEqual)
- ("<", storm::logic::ComparisonType::Less);
- }
- };
-
- // A parser used for recognizing the operators at the "relational" precedence level.
- relationalOperatorStruct relationalOperator_;
-
- struct binaryBooleanOperatorStruct : qi::symbols<char, storm::logic::BinaryBooleanStateFormula::OperatorType> {
- binaryBooleanOperatorStruct() {
- add
- ("&", storm::logic::BinaryBooleanStateFormula::OperatorType::And)
- ("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or);
- }
- };
-
- // A parser used for recognizing the operators at the "binary" precedence level.
- binaryBooleanOperatorStruct binaryBooleanOperator_;
-
- struct unaryBooleanOperatorStruct : qi::symbols<char, storm::logic::UnaryBooleanStateFormula::OperatorType> {
- unaryBooleanOperatorStruct() {
- add
- ("!", storm::logic::UnaryBooleanStateFormula::OperatorType::Not);
- }
- };
-
- // A parser used for recognizing the operators at the "unary" precedence level.
- unaryBooleanOperatorStruct unaryBooleanOperator_;
-
- struct optimalityOperatorStruct : qi::symbols<char, storm::logic::OptimalityType> {
- optimalityOperatorStruct() {
- add
- ("min", storm::logic::OptimalityType::Minimize)
- ("max", storm::logic::OptimalityType::Maximize);
- }
- };
+ // The manager used to parse expressions.
+ std::shared_ptr<storm::expressions::ExpressionManager const> manager;
- // A parser used for recognizing the optimality operators.
- optimalityOperatorStruct optimalityOperator_;
-
- // Parser and manager used for recognizing expressions.
- storm::parser::ExpressionParser expressionParser;
-
- // Functor used for displaying error information.
- struct ErrorHandler {
- typedef qi::error_handler_result result_type;
-
- template<typename T1, typename T2, typename T3, typename T4>
- qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const {
- std::stringstream whatAsString;
- whatAsString << what;
- STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << whatAsString.str() << ".");
- return qi::fail;
- }
- };
-
- // An error handler function.
- phoenix::function<ErrorHandler> handler;
-
- // A symbol table that is a mapping from identifiers that can be used in expressions to the expressions
- // they are to be replaced with.
+ // Keep track of added identifier expressions.
qi::symbols<char, storm::expressions::Expression> identifiers_;
- qi::rule<Iterator, std::vector<std::shared_ptr<storm::logic::Formula>>(), Skipper> start;
-
- qi::rule<Iterator, std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>(), qi::locals<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
- 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> steadyStateOperator;
-
- 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<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<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;
-
- // 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<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> 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::logic::OptimalityType>, 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::logic::OptimalityType>, 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::logic::OptimalityType>, 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::logic::OptimalityType>, 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);
+ // The grammar used to parse the input.
+ std::shared_ptr<FormulaParserGrammar> grammar;
};
-
+
} // namespace parser
} // namespace storm
-#endif /* STORM_PARSER_PRCTLPARSER_H_ */
+#endif /* STORM_PARSER_FORMULAPARSER_H_ */