diff --git a/src/ir/Module.h b/src/ir/Module.h new file mode 100644 index 000000000..d61a42add --- /dev/null +++ b/src/ir/Module.h @@ -0,0 +1,24 @@ +/* + * Module.h + * + * Created on: 04.01.2013 + * Author: chris + */ + +#ifndef MODULE_H_ +#define MODULE_H_ + +namespace storm { + +namespace ir { + +class Module { + +}; + +} + +} + + +#endif /* MODULE_H_ */ diff --git a/src/ir/Program.h b/src/ir/Program.h new file mode 100644 index 000000000..70797f40f --- /dev/null +++ b/src/ir/Program.h @@ -0,0 +1,35 @@ +/* + * Program.h + * + * Created on: 04.01.2013 + * Author: chris + */ + +#ifndef PROGRAM_H_ +#define PROGRAM_H_ + +#include "src/ir/expressions/ConstantExpression.h" +#include "Module.h" +#include "RewardModel.h" + +namespace storm { + +namespace ir { + +class Program { +public: + enum ModelType {DTMC, CTMC, MDP, CTMDP} modelType; + std::map undefinedConstantExpressions; + std::vector modules; + std::map rewards; + + std::string toString() { + return std::string("prog!"); + } +}; + +} + +} + +#endif /* PROGRAM_H_ */ diff --git a/src/ir/RewardModel.h b/src/ir/RewardModel.h new file mode 100644 index 000000000..b53194668 --- /dev/null +++ b/src/ir/RewardModel.h @@ -0,0 +1,24 @@ +/* + * RewardModel.h + * + * Created on: 04.01.2013 + * Author: chris + */ + +#ifndef REWARDMODEL_H_ +#define REWARDMODEL_H_ + +namespace storm { + +namespace ir { + +class RewardModel { + +}; + +} + +} + + +#endif /* REWARDMODEL_H_ */ diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h new file mode 100644 index 000000000..5d36598b2 --- /dev/null +++ b/src/ir/expressions/BooleanConstantExpression.h @@ -0,0 +1,66 @@ +/* + * BooleanConstantExpression.h + * + * Created on: 04.01.2013 + * Author: chris + */ + +#ifndef BOOLEANCONSTANTEXPRESSION_H_ +#define BOOLEANCONSTANTEXPRESSION_H_ + +#include "ConstantExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class BooleanConstantExpression : public ConstantExpression { +public: + BooleanConstantExpression(std::string constantName) : ConstantExpression(constantName) { + defined = false; + value = false; + } + + virtual ~BooleanConstantExpression() { + + } + + virtual std::string toString() const { + std::string result = this->constantName; + if (defined) { + result += "[" + boost::lexical_cast(value) + "]"; + } + return result; + } + + bool isDefined() { + return defined; + } + + bool getValue() { + return value; + } + + void define(bool value) { + defined = true; + this->value = value; + } + + bool value; + bool defined; +}; + +} + +} + +} + +BOOST_FUSION_ADAPT_STRUCT( + storm::ir::expressions::BooleanConstantExpression, + (std::string, constantName) +) + +#endif /* BOOLEANCONSTANTEXPRESSION_H_ */ diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h new file mode 100644 index 000000000..6969965ae --- /dev/null +++ b/src/ir/expressions/DoubleConstantExpression.h @@ -0,0 +1,66 @@ +/* + * DoubleConstantExpression.h + * + * Created on: 04.01.2013 + * Author: chris + */ + +#ifndef DOUBLECONSTANTEXPRESSION_H_ +#define DOUBLECONSTANTEXPRESSION_H_ + +#include "ConstantExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class DoubleConstantExpression : public ConstantExpression { +public: + DoubleConstantExpression(std::string constantName) : ConstantExpression(constantName) { + defined = false; + value = 0.0; + } + + virtual ~DoubleConstantExpression() { + + } + + virtual std::string toString() const { + std::string result = this->constantName; + if (defined) { + result += "[" + boost::lexical_cast(value) + "]"; + } + return result; + } + + bool isDefined() { + return defined; + } + + double getValue() { + return value; + } + + void define(double value) { + defined = true; + this->value = value; + } + + double value; + bool defined; +}; + +} + +} + +} + +BOOST_FUSION_ADAPT_STRUCT( + storm::ir::expressions::DoubleConstantExpression, + (std::string, constantName) +) + +#endif /* DOUBLECONSTANTEXPRESSION_H_ */ diff --git a/src/ir/expressions/Expressions.h b/src/ir/expressions/Expressions.h index 868fff365..5a69dc34c 100644 --- a/src/ir/expressions/Expressions.h +++ b/src/ir/expressions/Expressions.h @@ -17,5 +17,8 @@ #include "UnaryBooleanFunctionExpression.h" #include "UnaryNumericalFunctionExpression.h" #include "VariableExpression.h" +#include "BooleanConstantExpression.h" +#include "IntegerConstantExpression.h" +#include "DoubleConstantExpression.h" #endif /* EXPRESSIONS_H_ */ diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h new file mode 100644 index 000000000..d0df521af --- /dev/null +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -0,0 +1,66 @@ +/* + * IntegerConstantExpression.h + * + * Created on: 04.01.2013 + * Author: chris + */ + +#ifndef INTEGERCONSTANTEXPRESSION_H_ +#define INTEGERCONSTANTEXPRESSION_H_ + +#include "ConstantExpression.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +class IntegerConstantExpression : public ConstantExpression { +public: + IntegerConstantExpression(std::string constantName) : ConstantExpression(constantName) { + defined = false; + value = 0; + } + + virtual ~IntegerConstantExpression() { + + } + + virtual std::string toString() const { + std::string result = this->constantName; + if (defined) { + result += "[" + boost::lexical_cast(value) + "]"; + } + return result; + } + + bool isDefined() { + return defined; + } + + int getValue() { + return value; + } + + void define(int value) { + defined = true; + this->value = value; + } + + int value; + bool defined; +}; + +} + +} + +} + +BOOST_FUSION_ADAPT_STRUCT( + storm::ir::expressions::IntegerConstantExpression, + (std::string, constantName) +) + +#endif /* INTEGERCONSTANTEXPRESSION_H_ */ diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index a8073bb95..61bf5b63f 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -9,13 +9,12 @@ #define PRISMPARSER_H_ #include -#include -#include -#include +#include #include #include #include "src/ir/expressions/Expressions.h" +#include "src/ir/Program.h" namespace storm { @@ -29,85 +28,211 @@ class PrismParser { public: void test() { - std::string str = "const int ab = 10;"; - std::string::const_iterator iter = str.begin(); - std::string::const_iterator end = str.end(); - prismGrammar grammar; + std::string testInput = ""; + // storm::ir::Program* result = getProgram(testInput); + getProgram(testInput); + +/* std::cout << "Resulting program:" << std::endl; + std::cout << "-------------------------\n"; + std::cout << result->toString() << std::endl; + std::cout << "-------------------------\n"; */ + } - storm::ir::expressions::BaseExpression* result; - bool r = phrase_parse(iter, end, grammar, ascii::space, result); + void getProgram(std::string inputString) { + using qi::_val; + using qi::int_; + using qi::_r1; + using qi::_1; + using phoenix::ref; + using phoenix::val; - std::cout << r << std::endl; + prismGrammar grammar; + std::string::const_iterator it = inputString.begin(); + std::string::const_iterator end = inputString.end(); + storm::ir::Program result; - if (r && iter == end) { - std::cout << "-------------------------\n"; - std::cout << "Parsing succeeded\n"; - std::cout << "result = " << result << std::endl; - std::cout << "-------------------------\n"; + int resultInt = 0; + std::string input = "asdf"; + bool r = phrase_parse(it, end, grammar(phoenix::val(input)), ascii::space, resultInt); + + if (r && it == end) { + std::cout << "Parsing successful!" << std::endl; } else { - std::string rest(iter, end); + std::string rest(it, end); std::cout << "-------------------------\n"; std::cout << "Parsing failed\n"; - std::cout << "stopped at: " << rest << "\"\n"; + std::cout << "stopped at: \"" << rest << "\"\n"; std::cout << "-------------------------\n"; } } private: - struct keywords_ : qi::symbols { - keywords_() { - add - ("dtmc", 1) - ("ctmc", 2) - ("mdp", 3) - ("ctmdp", 4) - ("const", 5) - ("int", 6) - ("bool", 7) - ("module", 8) - ("endmodule", 9) - ("rewards", 10) - ("endrewards", 11) - ("true", 12) - ("false", 13) - ; - } - }; - - struct variables_ : qi::symbols { - // Intentionally left empty. This map is filled during parsing. - }; - - struct modules_ : qi::symbols { - // Intentionally left empty. This map is filled during parsing. - }; - template - struct prismGrammar : qi::grammar { + struct prismGrammar : qi::grammar { prismGrammar() : prismGrammar::base_type(start) { - // identifierName %= qi::lexeme[qi::char_("a-zA-Z_") >> *qi::char_("a-zA-Z_0-9")]; - // integerConstantDefinition %= qi::lit("const") >> qi::lit("int") >> identifierName >> "=" >> qi::int_ >> ";"; - - start %= literalExpression; + using qi::_val; + using qi::int_; + using qi::_r1; + using qi::_1; + using phoenix::ref; + + // start = constantDefinitionList(phoenix::ref(qi::_r1), phoenix::ref(qi::_r1)); + start = qi::lit(qi::_r1) >> int_; + constantDefinitionList = qi::int_; + + variableDefinition %= (booleanVariableDefinition | integerVariableDefinition); + booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") >> qi::lit(";"))[phoenix::bind(booleanVariables_.add, qi::_1, phoenix::new_(qi::_1)), phoenix::bind(allVariables_.add, qi::_1, phoenix::new_(qi::_1)), qi::_val = phoenix::new_(qi::_1)]; + integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") >> integerConstantExpression >> qi::lit("..") >> integerConstantExpression >> qi::lit("]") >> qi::lit(";"))[phoenix::bind(integerVariables_.add, qi::_1, phoenix::new_(qi::_1)), phoenix::bind(allVariables_.add, qi::_1, phoenix::new_(qi::_1)), qi::_val = phoenix::new_(qi::_1)]; + + constantDefinition %= (definedConstantDefinition | undefinedConstantDefinition); + definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); + undefinedConstantDefinition %= (undefinedBooleanConstantDefinition | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition); + definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") >> booleanLiteralExpression >> qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2]; + definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit("=") >> integerLiteralExpression >> qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2]; + definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") >> doubleLiteralExpression >> qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2]; + undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, phoenix::new_(qi::_1)), phoenix::bind(allConstants_.add, qi::_1, phoenix::new_(qi::_1)), qi::_val = phoenix::new_(qi::_1)]; + undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, phoenix::new_(qi::_1)), phoenix::bind(allConstants_.add, qi::_1, phoenix::new_(qi::_1)), qi::_val = phoenix::new_(qi::_1)]; + undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, phoenix::new_(qi::_1)), phoenix::bind(allConstants_.add, qi::_1, phoenix::new_(qi::_1)), qi::_val = phoenix::new_(qi::_1)]; + + expression %= (booleanExpression | integerExpression | doubleExpression); + + booleanExpression %= orExpression; + orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR)]; + andExpression = atomicBooleanExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> atomicBooleanExpression)[qi::_val = phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND)]; + atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); + relativeExpression = (integerExpression >> relations_ >> integerExpression)[qi::_val = phoenix::new_(qi::_1, qi::_3, qi::_2)]; + + integerExpression %= integerPlusExpression; + integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS)]; + integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES)]; + atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerConstantExpression); + + doubleExpression %= doublePlusExpression; + doublePlusExpression = doubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> doubleMultExpression)[qi::_val = phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS)]; + doubleMultExpression %= atomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicDoubleExpression)[qi::_val = phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES)]; + atomicDoubleExpression %= (qi::lit("(") >> doubleExpression >> qi::lit(")") | doubleConstantExpression); literalExpression %= (booleanLiteralExpression | integerLiteralExpression | doubleLiteralExpression); booleanLiteralExpression = qi::bool_[qi::_val = phoenix::new_(qi::_1)]; integerLiteralExpression = qi::int_[qi::_val = phoenix::new_(qi::_1)]; doubleLiteralExpression = qi::double_[qi::_val = phoenix::new_(qi::_1)]; - } - qi::rule start; + constantExpression %= (booleanConstantExpression | integerConstantExpression | doubleConstantExpression); + booleanConstantExpression %= (booleanConstants_ | booleanLiteralExpression); + integerConstantExpression %= (integerConstants_ | integerLiteralExpression); + doubleConstantExpression %= (doubleConstants_ | doubleLiteralExpression); - // The expression rules. + variableExpression = (integerVariableExpression | booleanVariableExpression); + integerVariableExpression = integerVariables_; + booleanVariableExpression = booleanVariables_; + + freeIdentifierName %= qi::lexeme[(qi::alpha >> *(qi::alnum)) - allVariables_ - allConstants_]; + } + + // The starting point of the grammar. + qi::rule start; + + qi::rule constantDefinitionList; + + qi::rule variableDefinition; + qi::rule booleanVariableDefinition; + qi::rule integerVariableDefinition; + + qi::rule constantDefinition; + qi::rule undefinedConstantDefinition; + qi::rule definedConstantDefinition; + qi::rule undefinedBooleanConstantDefinition; + qi::rule undefinedIntegerConstantDefinition; + qi::rule undefinedDoubleConstantDefinition; + qi::rule definedBooleanConstantDefinition; + qi::rule definedIntegerConstantDefinition; + qi::rule definedDoubleConstantDefinition; + + qi::rule freeIdentifierName; + + // The starting point for arbitrary expressions. + qi::rule expression; + + // Rules with boolean result type. + qi::rule booleanExpression; + qi::rule orExpression; + qi::rule andExpression; + qi::rule atomicBooleanExpression; + qi::rule relativeExpression; + + // Rules with integer result type. + qi::rule integerExpression; + qi::rule integerPlusExpression; + qi::rule integerMultExpression; + qi::rule atomicIntegerExpression; + + // Rules with double result type. + qi::rule doubleExpression; + qi::rule doublePlusExpression; + qi::rule doubleMultExpression; + qi::rule atomicDoubleExpression; + + // Rules for variable recognition. + qi::rule variableExpression; + qi::rule booleanVariableExpression; + qi::rule integerVariableExpression; + + // Rules for constant recognition. + qi::rule constantExpression; + qi::rule booleanConstantExpression; + qi::rule integerConstantExpression; + qi::rule doubleConstantExpression; + + // Rules for literal recognition. qi::rule literalExpression; qi::rule booleanLiteralExpression; qi::rule integerLiteralExpression; qi::rule doubleLiteralExpression; - // qi::rule integerConstantDefinition; - // qi::rule identifierName; - + struct keywordsStruct : qi::symbols { + keywordsStruct() { + add + ("dtmc", 1) + ("ctmc", 2) + ("mdp", 3) + ("ctmdp", 4) + ("const", 5) + ("int", 6) + ("bool", 7) + ("module", 8) + ("endmodule", 9) + ("rewards", 10) + ("endrewards", 11) + ("true", 12) + ("false", 13) + ; + } + } keywords_; + + struct relationalOperatorStruct : qi::symbols { + relationalOperatorStruct() { + add + ("==", storm::ir::expressions::BinaryRelationExpression::EQUAL) + ("<", storm::ir::expressions::BinaryRelationExpression::LESS) + ("<=", storm::ir::expressions::BinaryRelationExpression::LESS_OR_EQUAL) + (">", storm::ir::expressions::BinaryRelationExpression::GREATER) + (">=", storm::ir::expressions::BinaryRelationExpression::GREATER_OR_EQUAL) + ; + } + } relations_; + + struct variablesStruct : qi::symbols { + // Intentionally left empty. This map is filled during parsing. + } integerVariables_, booleanVariables_, allVariables_ ; + + struct constantsStruct : qi::symbols { + // Intentionally left empty. This map is filled during parsing. + } integerConstants_, booleanConstants_, doubleConstants_, allConstants_; + + struct modulesStruct : qi::symbols { + // Intentionally left empty. This map is filled during parsing. + } modules_; }; };