diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h index 8aca54125..d88dbf33b 100644 --- a/src/ir/expressions/DoubleLiteral.h +++ b/src/ir/expressions/DoubleLiteral.h @@ -10,6 +10,8 @@ #include "src/ir/expressions/BaseExpression.h" +#include "boost/lexical_cast.hpp" + namespace storm { namespace ir { diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp new file mode 100644 index 000000000..f3348cb19 --- /dev/null +++ b/src/parser/PrismParser.cpp @@ -0,0 +1,115 @@ +/* + * PrismParser.cpp + * + * Created on: 11.01.2013 + * Author: chris + */ + +#include "PrismParser.h" +#include "src/utility/OsDetection.h" + +// If the parser fails due to ill-formed data, this exception is thrown. +#include "src/exceptions/WrongFileFormatException.h" + +// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. +#include +#include + +// Needed for file IO. +#include +#include + +// Some typedefs and namespace definitions to reduce code size. +typedef std::istreambuf_iterator base_iterator_type; +typedef boost::spirit::multi_pass forward_iterator_type; +typedef boost::spirit::classic::position_iterator2 pos_iterator_type; +namespace qi = boost::spirit::qi; +namespace phoenix = boost::phoenix; + +namespace storm { + +namespace parser { + +/*! + * Opens the given file for parsing, invokes the helper function to parse the actual content and + * closes the file properly, even if an exception is thrown in the parser. In this case, the + * exception is passed on to the caller. + */ +std::shared_ptr PrismParser::parseFile(std::string const& filename) const { + // Open file and initialize result. + std::ifstream inputFileStream(filename, std::ios::in); + std::shared_ptr result(nullptr); + + // Now try to parse the contents of the file. + try { + result = std::shared_ptr(parse(inputFileStream, filename)); + } 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 result; +} + +/*! + * Passes iterators to the input stream to the Boost spirit parser and thereby parses the input. + * If the parser throws an expectation failure exception, i.e. expected input different than the one + * provided, this is caught and displayed properly before the exception is passed on. + */ +std::shared_ptr PrismParser::parse(std::istream& inputStream, std::string const& filename) const { + // Prepare iterators to input. + base_iterator_type in_begin(inputStream); + forward_iterator_type fwd_begin = boost::spirit::make_default_multi_pass(in_begin); + forward_iterator_type fwd_end; + pos_iterator_type position_begin(fwd_begin, fwd_end, filename); + pos_iterator_type position_end; + + // Prepare resulting intermediate representation of input. + std::shared_ptr result(new storm::ir::Program()); + + // In order to instantiate the grammar, we have to pass the type of the skipping parser. + // As this is more complex, we let Boost figure out the actual type for us. + prismGrammar> *(qi::char_ - qi::eol) >> qi::eol)> grammar; + try { + // Now parse the content using phrase_parse in order to be able to supply a skipping + // parser. + phrase_parse(position_begin, position_end, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, *result); + } catch(const qi::expectation_failure& e) { + // If the parser expected content different than the one provided, display information + // about the location of the error. + const boost::spirit::classic::file_position_base& pos = e.first.get_position(); + + // Construct the error message including a caret display of the position in the + // erroneous line. + std::stringstream msg; + msg << pos.file << ", line " << pos.line << ", column " << pos.column + << ": parse error: expected " << e.what_ << std::endl << "\t" + << e.first.get_currentline() << std::endl << "\t"; + int i = 0; + for (i = 0; i < pos.column; ++i) { + msg << "-"; + } + msg << "^"; + for (; i < 80; ++i) { + msg << "-"; + } + msg << std::endl; + +// On Mac OS, exception messages are not displayed in case an exception is propagated to the +// operating system, so we need to display the message ourselves. +#if defined(MACOSX) + std::cout << msg.str(); +#endif + // Now propagate exception. + throw storm::exceptions::WrongFileFormatException() << msg.str(); + } + + return result; + } + +} // namespace parser + +} // namespace storm diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 582f2dafb..a06c26dea 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -5,85 +5,76 @@ * Author: Christian Dehnert */ -#ifndef PRISMPARSER_H_ -#define PRISMPARSER_H_ +#ifndef STORM_PARSER_PRISMPARSER_H_ +#define STORM_PARSER_PRISMPARSER_H_ +// Used for Boost spirit. #include #include #include -#include -#include -#include -#include +// All classes of the intermediate representation are used. #include "src/ir/IR.h" +// Used for file input. #include -#include -#include namespace storm { namespace parser { +// Use some namespace shortcuts, to reduce code size. namespace qi = boost::spirit::qi; -namespace ascii = boost::spirit::ascii; namespace phoenix = boost::phoenix; -typedef std::istreambuf_iterator base_iterator_type; -typedef boost::spirit::multi_pass forward_iterator_type; -typedef boost::spirit::classic::position_iterator2 pos_iterator_type; - +/*! + * This class parses the format of the PRISM model checker into an intermediate representation. + */ class PrismParser { - public: - void test(std::string const& fileName) { - std::ifstream inputFileStream(fileName, std::ios::in); - getProgram(inputFileStream, fileName); - inputFileStream.close(); - } - - void getProgram(std::istream& inputStream, std::string const& fileName) { - base_iterator_type in_begin(inputStream); - - forward_iterator_type fwd_begin = boost::spirit::make_default_multi_pass(in_begin); - forward_iterator_type fwd_end; - - pos_iterator_type position_begin(fwd_begin, fwd_end, fileName); - pos_iterator_type position_end; - - storm::ir::Program result; - prismGrammar> *(qi::char_ - qi::eol) >> qi::eol)> grammar; - try { - phrase_parse(position_begin, position_end, grammar, ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); - } catch(const qi::expectation_failure& e) { - const boost::spirit::classic::file_position_base& pos = e.first.get_position(); - std::stringstream msg; - msg << pos.file << ", line " << pos.line << ", column " << pos.column << ": parse error: expected " << e.what_ << std::endl << "\t" << e.first.get_currentline() << std::endl << "\t"; - int i = 0; - for (i = 0; i < pos.column; ++i) { - msg << "-"; - } - msg << "^"; - for (; i < 80; ++i) { - msg << "-"; - } - msg << std::endl; - std::cout << msg.str(); - throw storm::exceptions::WrongFileFormatException() << msg.str(); - } - - std::cout << result.toString(); - } + /*! + * Parses the given file into the intermediate representation assuming it complies with the + * PRISM syntax. + * @param filename the name of the file to parse. + * @return a shared pointer to the intermediate representation of the PRISM file. + */ + std::shared_ptr parseFile(std::string const& filename) const; private: + /*! + * Parses the given input stream into the intermediate representation assuming it complies with + * the PRISM syntax. + * @param inputStream the input stream to parse. + * @param filename the name of the file the input stream belongs to. Used for diagnostics. + * @return a shared pointer to the intermediate representation of the PRISM file. + */ + std::shared_ptr parse(std::istream& inputStream, std::string const& filename) const; + + /*! + * The Boost spirit grammar for the PRISM language. Returns the intermediate representation of + * the input that complies with the PRISM syntax. + */ template struct prismGrammar : qi::grammar>, std::map>, std::map>, std::map, std::map>>, Skipper> { + /* + * The constructor of the grammar. It defines all rules of the grammar and the corresponding + * semantic actions that take care of constructing the intermediate representation during + * parsing. + * + * Note: The grammar takes care of some semantic checks already. For example, in places + * where we necessarily require a constant expression, this is enforced by not allowing + * variables as subexpressions. Also, variable names are by definition unique and it is + * ensured that variables and constants are properly declared. + * TODO: It should be ensured that updates of a command only refer to variables of the + * current module. + */ prismGrammar() : prismGrammar::base_type(start) { - freeIdentifierName %= qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_'))) - booleanVariables_ - integerVariables_ - allConstants_]]; + // This rule defines all identifiers that have not been previously used. + freeIdentifierName %= qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_'))) - booleanVariableNames_ - integerVariableNames_ - allConstantNames_ - labelNames_ - moduleNames_ - keywords_]]; freeIdentifierName.name("unused identifier"); + // This block defines all literal expressions. booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; booleanLiteralExpression.name("boolean literal"); integerLiteralExpression = qi::int_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; @@ -93,6 +84,7 @@ private: literalExpression %= (booleanLiteralExpression | integerLiteralExpression | doubleLiteralExpression); literalExpression.name("literal"); + // This block defines all expressions that are variables. integerVariableExpression %= integerVariables_; integerVariableExpression.name("integer variable"); booleanVariableExpression %= booleanVariables_; @@ -100,6 +92,7 @@ private: variableExpression %= (integerVariableExpression | booleanVariableExpression); variableExpression.name("variable"); + // This block defines all atomic expressions that are constant, i.e. literals and constants. booleanConstantExpression %= (booleanConstants_ | booleanLiteralExpression); booleanConstantExpression.name("boolean constant or literal"); integerConstantExpression %= (integerConstants_ | integerLiteralExpression); @@ -109,6 +102,7 @@ private: constantExpression %= (booleanConstantExpression | integerConstantExpression | doubleConstantExpression); constantExpression.name("constant or literal"); + // This block defines all expressions of integral type. atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerConstantExpression); atomicIntegerExpression.name("integer expression"); integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; @@ -118,6 +112,7 @@ private: integerExpression %= integerPlusExpression; integerExpression.name("integer expression"); + // This block defines all expressions of integral type that are by syntax constant. That is, they are evaluable given the values for all constants. constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); constantAtomicIntegerExpression.name("constant integer expression"); constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; @@ -170,8 +165,10 @@ private: expression.name("expression"); // This block defines all entities that are needed for parsing labels. - labelDefinition = (qi::lit("label") >> freeIdentifierName >> qi::lit("=") >> booleanExpression >> qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_2))]; + labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> freeIdentifierName >> -qi::lit("\"") >> qi::lit("=") >> booleanExpression >> qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_2)), phoenix::bind(labelNames_.add, qi::_1, qi::_1)]; + labelDefinition.name("label declaration"); labelDefinitionList %= *labelDefinition(qi::_r1); + labelDefinitionList.name("label declaration list"); // This block defines all entities that are needed for parsing a reward model. stateRewardDefinition = (booleanExpression > qi::lit(":") > constantDoubleExpression >> qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2)]; @@ -212,23 +209,23 @@ private: variableDefinition.name("variable declaration"); // This block defines all entities that are needed for parsing a module. - moduleDefinition = (qi::lit("module") > freeIdentifierName > *(booleanVariableDefinition[phoenix::push_back(qi::_a, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_b, qi::_1)]) > +commandDefinition > qi::lit("endmodule"))[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_3)]; + moduleDefinition = (qi::lit("module") > freeIdentifierName > *(booleanVariableDefinition[phoenix::push_back(qi::_a, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_b, qi::_1)]) > +commandDefinition > qi::lit("endmodule"))[phoenix::bind(moduleNames_.add, qi::_1, qi::_1), qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_3)]; moduleDefinition.name("module"); moduleDefinitionList %= +moduleDefinition; moduleDefinitionList.name("module list"); // This block defines all entities that are needed for parsing constant definitions. - 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]; + definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") > booleanLiteralExpression > qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; definedBooleanConstantDefinition.name("defined boolean constant declaration"); - 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]; + definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit("=") > integerLiteralExpression > qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; definedIntegerConstantDefinition.name("defined integer constant declaration"); - 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]; + definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") > doubleLiteralExpression > qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; definedDoubleConstantDefinition.name("defined double constant declaration"); - undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(booleanConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)]; + undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); - undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(integerConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(integerConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)]; + undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(integerConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); - undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(doubleConstantInfo_.add, qi::_1, qi::_a), phoenix::bind(doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstants_.add, qi::_1, qi::_a)]; + undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; undefinedDoubleConstantDefinition.name("undefined double constant declaration"); definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); definedConstantDefinition.name("defined constant declaration"); @@ -250,31 +247,37 @@ private: qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; qi::rule(), Skipper> moduleDefinitionList; + // Rules for module definition. qi::rule, std::vector>, Skipper> moduleDefinition; + // Rules for variable definitions. qi::rule variableDefinition; qi::rule, std::shared_ptr>, Skipper> booleanVariableDefinition; qi::rule, std::shared_ptr>, Skipper> integerVariableDefinition; + // Rules for command definitions. qi::rule, Skipper> commandDefinition; - qi::rule(), Skipper> updateListDefinition; qi::rule updateDefinition; qi::rule(), Skipper> assignmentDefinitionList; qi::rule assignmentDefinition; + // Rules for variable/command names. qi::rule integerVariableName; qi::rule booleanVariableName; qi::rule commandName; + // Rules for reward definitions. qi::rule&), Skipper> rewardDefinitionList; qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; qi::rule stateRewardDefinition; qi::rule, Skipper> transitionRewardDefinition; + // Rules for label definitions. qi::rule>&), Skipper> labelDefinitionList; qi::rule>&), Skipper> labelDefinition; + // Rules for constant definitions. qi::rule(), Skipper> constantDefinition; qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; qi::rule(), Skipper> definedConstantDefinition; @@ -338,6 +341,7 @@ private: qi::rule(), Skipper> integerLiteralExpression; qi::rule(), Skipper> doubleLiteralExpression; + // A structure defining the keywords that are not allowed to be chosen as identifiers. struct keywordsStruct : qi::symbols { keywordsStruct() { add @@ -358,6 +362,8 @@ private: } } keywords_; + // A structure mapping the textual representation of a model type to the model type + // representation of the intermediate representation. struct modelTypeStruct : qi::symbols { modelTypeStruct() { add @@ -369,6 +375,8 @@ private: } } modelType_; + // A structure mapping the textual representation of a binary relation to the representation + // of the intermediate representation. struct relationalOperatorStruct : qi::symbols { relationalOperatorStruct() { add @@ -381,33 +389,13 @@ private: } } relations_; - struct variablesStruct : qi::symbols> { - // Intentionally left empty. This map is filled during parsing. - } integerVariables_, booleanVariables_; - - struct entityNamesStruct : qi::symbols { - // Intentionally left empty. This map is filled during parsing. - } integerVariableNames_, booleanVariableNames_, commandNames_; - - struct constantsStruct : qi::symbols> { - // Intentionally left empty. This map is filled during parsing. - } integerConstants_, booleanConstants_, doubleConstants_, allConstants_; - - struct undefinedBooleanConstantsTypesStruct : qi::symbols> { - // Intentionally left empty. This map is filled during parsing. - } booleanConstantInfo_; - - struct undefinedIntegerConstantsTypesStruct : qi::symbols> { - // Intentionally left empty. This map is filled during parsing. - } integerConstantInfo_; - - struct undefinedDoubleConstantsTypesStruct : qi::symbols> { - // Intentionally left empty. This map is filled during parsing. - } doubleConstantInfo_; + // Structures mapping variable and constant names to the corresponding expression nodes of + // the intermediate representation. + struct qi::symbols> integerVariables_, booleanVariables_; + struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_; - struct modulesStruct : qi::symbols { - // Intentionally left empty. This map is filled during parsing. - } modules_; + // A structure representing the identity function over identifier names. + struct qi::symbols integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_; }; }; @@ -415,4 +403,4 @@ private: } // namespace storm -#endif /* PRISMPARSER_H_ */ +#endif /* STORM_PARSER_PRISMPARSER_H_ */ diff --git a/src/storm.cpp b/src/storm.cpp index faba3559b..c4c75d09a 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -241,7 +241,7 @@ int main(const int argc, const char* argv[]) { // testChecking(); storm::parser::PrismParser parser; - parser.test("test.input"); + parser.parseFile("test.input"); cleanUp(); return 0;