FormulaParser.h

Go to the documentation of this file.

#pragma once
 
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/jani/Property.h"
 
namespace storm {
namespace prism {
class Program;
}
 
namespace logic {
class Formula;
}
 
namespace parser {
 
// Forward-declare grammar.
class FormulaParserGrammar;
 
class FormulaParser {
   public:
    FormulaParser();
    explicit FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager);
    explicit FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager> const& manager);
    explicit FormulaParser(storm::prism::Program const& program);
    explicit FormulaParser(storm::prism::Program& program);
 
    FormulaParser(FormulaParser const& other);
    FormulaParser& operator=(FormulaParser const& other);

    std::shared_ptr<storm::logic::Formula const> parseSingleFormulaFromString(std::string const& formulaString) const;

    std::vector<storm::jani::Property> parseFromString(std::string const& propertyString) const;

    std::vector<storm::jani::Property> parseFromFile(std::string const& filename) const;

    void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression);
 
   private:
    // The manager used to parse expressions.
    std::shared_ptr<storm::expressions::ExpressionManager const> manager;
 
    // The grammar used to parse the input.
    std::shared_ptr<FormulaParserGrammar> grammar;
};
 
}  // namespace parser
}  // namespace storm