tempest/src/parser/prismparser/PrismGrammar.h

#ifndef STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_
#define	STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_

// Include files for file input.
#include <istream>
#include <memory>

// Include boost spirit.
#include <boost/typeof/typeof.hpp>
#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix.hpp>

// Include headers for spirit iterators. Needed for diagnostics and input stream iteration.
#include <boost/spirit/include/classic_position_iterator.hpp>
#include <boost/spirit/include/support_multi_pass.hpp>

namespace qi = boost::spirit::qi;
namespace phoenix = boost::phoenix;

typedef std::string::const_iterator BaseIteratorType;
typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType;
typedef PositionIteratorType Iterator;
typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper;
typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2;
typedef boost::spirit::unused_type Unused;

#include "src/parser/prismparser/Tokens.h"

#include "src/storage/prism/Program.h"
#include "src/storage/expressions/Expression.h"
using namespace storm::prism;
using namespace storm::expressions;

namespace storm {
    namespace parser {
        namespace prism {
            class PrismGrammar : public qi::grammar<Iterator, Program(), Skipper> {
            public:
                /*!
                 * Default constructor that creates an empty and functional grammar.
                 */
                PrismGrammar();
                
            private:
                // The starting point of the grammar.
                qi::rule<Iterator, Program(), Skipper> start;
                
                // Rules for model type.
                qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition;
                
                // Rules for global constant definitions.
                qi::rule<Iterator, qi::unused_type(std::set<std::string>&, std::set<std::string>&, std::set<std::string>&, std::map<std::string, storm::expression::Expression>&, std::map<std::string, storm::expression::Expression>&, std::map<std::string, storm::expression::Expression>&), Skipper> constantDefinitionList;
                
                // Rules for global variable definitions
                qi::rule<Iterator, qi::unused_type(std::map<std::string, BooleanVariable>&, std::map<std::string, IntegerVariable>), Skipper> globalVariableDefinitionList;
                
                // Rules for modules definition.
                qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
                qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
                qi::rule<Iterator, Module(), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming;
                
                // Rules for variable definitions.
                qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, std::map<std::string, uint_fast64_t>&), Skipper> variableDefinition;
                qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::map<std::string, uint_fast64_t>&, bool), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> booleanVariableDefinition;
                qi::rule<Iterator, qi::unused_type(std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, bool), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> integerVariableDefinition;
                
                // Rules for command definitions.
                qi::rule<Iterator, Command(), qi::locals<std::string>, Skipper> commandDefinition;
                qi::rule<Iterator, std::vector<Update>(), Skipper> updateListDefinition;
                qi::rule<Iterator, Update(), qi::locals<std::map<std::string, Assignment>, std::map<std::string, Assignment>>, Skipper> updateDefinition;
                qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinitionList;
                qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinition;
                
                // Rules for variable/command names.
                qi::rule<Iterator, std::string(), Skipper> commandName;
                qi::rule<Iterator, std::string(), Skipper> unassignedLocalBooleanVariableName;
                qi::rule<Iterator, std::string(), Skipper> unassignedLocalIntegerVariableName;
                
                // Rules for reward definitions.
                qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), Skipper> rewardDefinitionList;
                qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), qi::locals<std::vector<StateReward>, std::vector<TransitionReward>>, Skipper> rewardDefinition;
                qi::rule<Iterator, StateReward(), Skipper> stateRewardDefinition;
                qi::rule<Iterator, TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
                
                // Rules for label definitions.
                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BaseExpression>>&), Skipper> labelDefinitionList;
                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BaseExpression>>&), Skipper> labelDefinition;
                
                // Rules for constant definitions.
                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantDefinition;
                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BooleanConstantExpression>>&, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>&, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedConstantDefinition;
                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BooleanConstantExpression>>&), Skipper> undefinedBooleanConstantDefinition;
                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<IntegerConstantExpression>>&), Skipper> undefinedIntegerConstantDefinition;
                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<DoubleConstantExpression>>&), Skipper> undefinedDoubleConstantDefinition;
                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedBooleanConstantDefinition;
                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedIntegerConstantDefinition;
                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedDoubleConstantDefinition;
                
                // Rules for formula definitions.
                qi::rule<Iterator, qi::unused_type(), Skipper> formulaDefinitionList;
                qi::rule<Iterator, qi::unused_type(), Skipper> formulaDefinition;
                qi::rule<Iterator, qi::unused_type(), Skipper> constantIntegerFormulaDefinition;
                qi::rule<Iterator, qi::unused_type(), Skipper> integerFormulaDefinition;
                qi::rule<Iterator, qi::unused_type(), Skipper> constantDoubleFormulaDefinition;
                qi::rule<Iterator, qi::unused_type(), Skipper> constantBooleanFormulaDefinition;
                qi::rule<Iterator, qi::unused_type(), Skipper> booleanFormulaDefinition;

                // Rules for variable recognition.
                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableCreatorExpression;
                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<std::shared_ptr<BaseExpression>>, Skipper> integerVariableCreatorExpression;
                
                storm::parser::prism::keywordsStruct keywords_;
                storm::parser::prism::modelTypeStruct modelType_;
                storm::parser::prism::relationalOperatorStruct relations_;
                
                // A mapping from module names to the modules themselves so they can be looked up for renaming later.
                struct qi::symbols<char, Module> moduleMap_;
                
                /*!
                 * Adds a label with the given name and expression to the given label-to-expression map.
                 *
                 * @param name The name of the label.
                 * @param expression The expression associated with the label.
                 * @param nameToExpressionMap The map to which the label is added.
                 */
                void addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::unique_ptr<BaseExpression>>& nameToExpressionMap);
                
                /*!
                 * Adds a boolean assignment for the given variable with the given expression and adds it to the
                 * provided variable-to-assignment map.
                 *
                 * @param variable The name of the variable that the assignment targets.
                 * @param expression The expression that is assigned to the variable.
                 * @param variableToAssignmentMap The map to which the assignment is added.
                 */
                void addBooleanAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& expression, std::map<std::string, Assignment>& variableToAssignmentMap);
                
                /*!
                 * Adds a boolean assignment for the given variable with the given expression and adds it to the
                 * provided variable-to-assignment map.
                 *
                 * @param variable The name of the variable that the assignment targets.
                 * @param expression The expression that is assigned to the variable.
                 * @param variableToAssignmentMap The map to which the assignment is added.
                 */
                void addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& expression, std::map<std::string, Assignment>& variableToAssignmentMap);
                
                void addUndefinedBooleanConstant(std::string const& name, std::map<std::string, std::unique_ptr<BooleanConstantExpression>>& nameToExpressionMap);

                void addUndefinedIntegerConstant(std::string const& name, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>& nameToExpressionMap);

                void addUndefinedDoubleConstant(std::string const& name, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>& nameToExpressionMap);

                /*!
                 * Creates a module by renaming, i.e. takes the module given by the old name, creates a new module
                 * with the given name which renames all identifiers according to the given mapping.
                 *
                 * @param name The name of the new module.
                 * @param oldName The name of the module that is to be copied (modulo renaming).
                 * @param renaming A mapping from identifiers to their new names.
                 */
                Module renameModule(std::string const& name, std::string const& oldName, std::map<std::string, std::string> const& renaming);
                
                /*!
                 * Creates a new module with the given name, boolean and integer variables and commands.
                 *
                 * @param name The name of the module to create.
                 * @param booleanVariables The boolean variables of the module.
                 * @param integerVariables The integer variables of the module.
                 * @param booleanVariableToLocalIndexMap A mapping of boolean variables to module-local indices.
                 * @param integerVariableToLocalIndexMap A mapping of boolean variables to module-local indices.
                 * @param commands The commands associated with this module.
                 */
                Module createModule(std::string const& name, std::vector<BooleanVariable> const& booleanVariables, std::vector<IntegerVariable> const& integerVariables, std::map<std::string, uint_fast64_t> const& booleanVariableToLocalIndexMap, std::map<std::string, uint_fast64_t> const& integerVariableToLocalIndexMap, std::vector<storm::ir::Command> const& commands);
                
                /*!
                 * Creates an integer variable with the given name, domain and initial value and adds it to the
                 * provided list of integer variables and the given mappings.
                 *
                 * @param name The name of the integer variable.
                 * @param lower The expression that defines the lower bound of the domain.
                 * @param upper The expression that defines the upper bound of the domain.
                 * @param init The expression that defines the initial value of the variable.
                 * @param integerVariableToGlobalIndexMap A mapping of integer variables to global indices.
                 * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not.
                 */
                void createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& integerVariables, std::map<std::string, uint_fast64_t>& integerVariableToGlobalIndexMap, bool isGlobalVariable);
                
                /*!
                 * Creates an boolean variable with the given name and initial value and adds it to the
                 * provided list of boolean variables and the given mappings.
                 *
                 * @param name The name of the boolean variable.
                 * @param init The expression that defines the initial value of the variable.
                 * @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices.
                 * @param isGlobalVariable A flag indicating whether the variable is supposed to be global or not.
                 */
                void createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& booleanVariables, std::map<std::string, uint_fast64_t>& booleanVariableToGlobalIndexMap, bool isGlobalVariable);
                
                /*!
                 * Creates a command with the given label, guard and updates.
                 *
                 * @param label The label of the command.
                 * @param guard The guard of the command.
                 * @param updates The updates associated with the command.
                 */
                Command createCommand(std::string const& label, std::shared_ptr<BaseExpression> const& guard, std::vector<Update> const& updates);
                
                /*!
                 * Creates an update with the given likelihood and the given assignments to boolean and integer variables, respectively.
                 *
                 * @param likelihood The likelihood of this update being executed.
                 * @param booleanAssignments The assignments to boolean variables this update involves.
                 * @param integerAssignments The assignments to integer variables this update involves.
                 */
                Update createUpdate(std::shared_ptr<BaseExpression> const& likelihood, std::map<std::string, Assignment> const& booleanAssignments, std::map<std::string, Assignment> const& integerAssignments);
                
            };
            
            
        } // namespace prism
    } // namespace parser
} // namespace storm


#endif	/* STORM_PARSER_PRISMPARSER_PRISMGRAMMAR_H_ */