diff --git a/CMakeLists.txt b/CMakeLists.txt index df1e897f5..a52cf47ec 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -48,6 +48,10 @@ message(STATUS "GMMXX_INCLUDE_DIR is ${GMMXX_INCLUDE_DIR}") option(DEBUG "Sets whether the DEBUG mode is used" ON) option(USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON) option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." ON) +option(LINK_LIBCXXABI "Sets whether libc++abi should be linked" OFF) +set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.") +set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.") +set(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory.") # If the DEBUG option was turned on, we will target a debug version and a release version otherwise if (DEBUG) @@ -74,9 +78,12 @@ elseif(MSVC) # required for GMM to compile, ugly error directive in their code add_definitions(/D_SCL_SECURE_NO_DEPRECATE) else(CLANG) + # As CLANG is not set as a variable, we need to set it in case we have not matched another compiler. + set (CLANG ON) # Set standard flags for clang set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops") - set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE") + # TODO: activate -Werror asap + set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE") # Turn on popcnt instruction if desired (yes by default) if (USE_POPCNT) @@ -118,6 +125,11 @@ find_package(Doxygen REQUIRED) set(Boost_USE_STATIC_LIBS ON) set(Boost_USE_MULTITHREADED ON) set(Boost_USE_STATIC_RUNTIME OFF) + +# If a custom boost root directory was specified, we set the corresponding hint for the script to find it. +if(CUSTOM_BOOST_ROOT) + set(BOOST_ROOT "${CUSTOM_BOOST_ROOT}") +endif(CUSTOM_BOOST_ROOT) find_package(Boost REQUIRED COMPONENTS program_options) if(Boost_FOUND) @@ -138,6 +150,16 @@ include_directories(${EIGEN3_INCLUDE_DIR}) # Add GMMXX to the included directories include_directories(${GMMXX_INCLUDE_DIR}) +# Add custom additional include or link directories +if (ADDITIONAL_INCLUDE_DIRS) + message(STATUS "Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}") + include_directories(${ADDITIONAL_INCLUDE_DIRS}) +endif(ADDITIONAL_INCLUDE_DIRS) +if (ADDITIONAL_LINK_DIRS) + message(STATUS "Using additional link directories ${ADDITIONAL_LINK_DIRS}") + link_directories(${ADDITIONAL_LINK_DIRS}) +endif(ADDITIONAL_LINK_DIRS) + # Add the executables # Must be created *after* Boost was added because of LINK_DIRECTORIES add_executable(storm ${STORM_SOURCES} ${STORM_HEADERS}) @@ -147,6 +169,13 @@ add_executable(storm-tests ${STORM_TEST_SOURCES} ${STORM_TEST_HEADERS}) target_link_libraries(storm ${Boost_LIBRARIES}) target_link_libraries(storm-tests ${Boost_LIBRARIES}) +# Link against libc++abi if requested. May be needed to build on Linux systems using clang. +if (LINK_LIBCXXABI) + message (STATUS "Linking against libc++abi.") + target_link_libraries(storm "c++abi") + target_link_libraries(storm-tests "c++abi") +endif(LINK_LIBCXXABI) + # Add a target to generate API documentation with Doxygen if(DOXYGEN_FOUND) set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc") diff --git a/src/ir/Command.h b/src/ir/Command.h index 9a687eab6..c5bfee6d5 100644 --- a/src/ir/Command.h +++ b/src/ir/Command.h @@ -8,7 +8,8 @@ #ifndef COMMAND_H_ #define COMMAND_H_ -#include "IR.h" +#include "expressions/BaseExpression.h" +#include "Update.h" namespace storm { diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h index abde92cb3..78c638954 100644 --- a/src/ir/IntegerVariable.h +++ b/src/ir/IntegerVariable.h @@ -9,6 +9,7 @@ #define INTEGERVARIABLE_H_ #include "Variable.h" +#include "expressions/BaseExpression.h" namespace storm { diff --git a/src/ir/Module.h b/src/ir/Module.h index a1046db76..bb3142328 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -8,7 +8,9 @@ #ifndef MODULE_H_ #define MODULE_H_ -#include "IR.h" +#include "BooleanVariable.h" +#include "IntegerVariable.h" +#include "Command.h" namespace storm { @@ -44,14 +46,6 @@ public: return result; } - void addBooleanVariable(storm::ir::BooleanVariable variable) { - booleanVariables.push_back(variable); - } - - void addIntegerVariable(storm::ir::IntegerVariable variable) { - integerVariables.push_back(variable); - } - private: std::string moduleName; diff --git a/src/ir/Program.h b/src/ir/Program.h index e2b94af57..57a6ac11a 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -8,12 +8,13 @@ #ifndef PROGRAM_H_ #define PROGRAM_H_ -#include "src/ir/expressions/ConstantExpression.h" +#include "expressions/BaseExpression.h" +#include "expressions/BooleanConstantExpression.h" +#include "expressions/IntegerConstantExpression.h" +#include "expressions/DoubleConstantExpression.h" #include "Module.h" #include "RewardModel.h" -#include - namespace storm { namespace ir { @@ -27,8 +28,8 @@ public: } - Program(ModelType modelType, std::map> booleanUndefinedConstantExpressions, std::map> integerUndefinedConstantExpressions, std::map> doubleUndefinedConstantExpressions, std::vector modules, std::map rewards) - : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards) { + Program(ModelType modelType, std::map> booleanUndefinedConstantExpressions, std::map> integerUndefinedConstantExpressions, std::map> doubleUndefinedConstantExpressions, std::vector modules, std::map rewards, std::map> labels) + : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels) { } @@ -71,19 +72,11 @@ public: result +="\n"; } - return result; - } - - void addBooleanUndefinedConstantExpression(std::string constantName, std::shared_ptr constantExpression) { - booleanUndefinedConstantExpressions[constantName] = constantExpression; - } - - void addIntegerUndefinedConstantExpression(std::string constantName, std::shared_ptr constantExpression) { - integerUndefinedConstantExpressions[constantName] = constantExpression; - } + for (auto label : labels) { + result += "label " + label.first + " = " + label.second->toString() + ";\n"; + } - void addDoubleUndefinedConstantExpression(std::string constantName, std::shared_ptr constantExpression) { - doubleUndefinedConstantExpressions[constantName] = constantExpression; + return result; } private: @@ -93,6 +86,7 @@ private: std::map> doubleUndefinedConstantExpressions; std::vector modules; std::map rewards; + std::map> labels; }; } diff --git a/src/ir/Update.h b/src/ir/Update.h index e2751703a..1ea4b0dc1 100644 --- a/src/ir/Update.h +++ b/src/ir/Update.h @@ -8,7 +8,7 @@ #ifndef UPDATE_H_ #define UPDATE_H_ -#include "IR.h" +#include "expressions/BaseExpression.h" namespace storm { diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h index 9a1121503..5eceb7c6b 100644 --- a/src/ir/expressions/VariableExpression.h +++ b/src/ir/expressions/VariableExpression.h @@ -10,6 +10,8 @@ #include "src/ir/expressions/BaseExpression.h" +#include + namespace storm { namespace ir { @@ -20,8 +22,8 @@ class VariableExpression : public BaseExpression { public: std::string variableName; - VariableExpression(std::string variableName) { - this->variableName = variableName; + VariableExpression(std::string variableName) : variableName(variableName) { + } virtual ~VariableExpression() { diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 74735e5c9..582f2dafb 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -30,6 +30,10 @@ 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; + class PrismParser { public: @@ -40,14 +44,11 @@ public: } void getProgram(std::istream& inputStream, std::string const& fileName) { - typedef std::istreambuf_iterator base_iterator_type; base_iterator_type in_begin(inputStream); - typedef boost::spirit::multi_pass forward_iterator_type; forward_iterator_type fwd_begin = boost::spirit::make_default_multi_pass(in_begin); forward_iterator_type fwd_end; - typedef boost::spirit::classic::position_iterator2 pos_iterator_type; pos_iterator_type position_begin(fwd_begin, fwd_end, fileName); pos_iterator_type position_end; @@ -58,8 +59,17 @@ public: } catch(const qi::expectation_failure& e) { const boost::spirit::classic::file_position_base& pos = e.first.get_position(); std::stringstream msg; - msg << "parse error at file '" << pos.file << "' line " << pos.line << " column " << pos.column << std::endl << "'" << e.first.get_currentline() << "'" << std::endl << std::setw(pos.column + 1) << " " << "^------- here"; - std::cout << msg.str() << std::endl; + 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(); } @@ -68,104 +78,174 @@ public: private: template - struct prismGrammar : qi::grammar>, std::map>, std::map>, std::map>, Skipper> { + struct prismGrammar : qi::grammar>, std::map>, std::map>, std::map, std::map>>, Skipper> { prismGrammar() : prismGrammar::base_type(start) { - freeIdentifierName %= qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))] - allVariables_ - allConstants_; + freeIdentifierName %= qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_'))) - booleanVariables_ - integerVariables_ - allConstants_]]; + freeIdentifierName.name("unused identifier"); 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))]; + integerLiteralExpression.name("integer literal"); doubleLiteralExpression = qi::double_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; + doubleLiteralExpression.name("double literal"); literalExpression %= (booleanLiteralExpression | integerLiteralExpression | doubleLiteralExpression); + literalExpression.name("literal"); - integerVariableExpression = integerVariables_; - booleanVariableExpression = booleanVariables_; - variableExpression = (integerVariableExpression | booleanVariableExpression); + integerVariableExpression %= integerVariables_; + integerVariableExpression.name("integer variable"); + booleanVariableExpression %= booleanVariables_; + booleanVariableExpression.name("boolean variable"); + variableExpression %= (integerVariableExpression | booleanVariableExpression); + variableExpression.name("variable"); booleanConstantExpression %= (booleanConstants_ | booleanLiteralExpression); + booleanConstantExpression.name("boolean constant or literal"); integerConstantExpression %= (integerConstants_ | integerLiteralExpression); + integerConstantExpression.name("integer constant or literal"); doubleConstantExpression %= (doubleConstants_ | doubleLiteralExpression); + doubleConstantExpression.name("double constant or literal"); constantExpression %= (booleanConstantExpression | integerConstantExpression | doubleConstantExpression); + constantExpression.name("constant or literal"); 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))]; + integerMultExpression.name("integer expression"); integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + integerPlusExpression.name("integer expression"); integerExpression %= integerPlusExpression; + integerExpression.name("integer expression"); 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))]; + constantIntegerMultExpression.name("constant integer expression"); constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + constantIntegerPlusExpression.name("constant integer expression"); constantIntegerExpression %= constantIntegerPlusExpression; + constantIntegerExpression.name("constant integer expression"); // This block defines all expressions of type double that are by syntax constant. That is, they are evaluable given the values for all constants. constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression); + constantAtomicDoubleExpression.name("constant double expression"); constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; + constantDoubleMultExpression.name("constant double expression"); constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + constantDoublePlusExpression.name("constant double expression"); constantDoubleExpression %= constantDoublePlusExpression; + constantDoubleExpression.name("constant double expression"); // This block defines all expressions of type boolean. relativeExpression = (integerExpression >> relations_ >> integerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, qi::_3, qi::_2))]; + relativeExpression.name("boolean expression"); atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanConstantExpression); + atomicBooleanExpression.name("boolean expression"); notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))]; + notExpression.name("boolean expression"); andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))]; + andExpression.name("boolean expression"); orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))]; + orExpression.name("boolean expression"); booleanExpression %= orExpression; + booleanExpression.name("boolean expression"); // This block defines all expressions of type boolean that are by syntax constant. That is, they are evaluable given the values for all constants. constantRelativeExpression = (constantIntegerExpression >> relations_ >> constantIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, qi::_3, qi::_2))]; + constantRelativeExpression.name("constant boolean expression"); constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); + constantAtomicBooleanExpression.name("constant boolean expression"); constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))]; + constantNotExpression.name("constant boolean expression"); constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))]; + constantAndExpression.name("constant boolean expression"); constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))]; + constantOrExpression.name("constant boolean expression"); constantBooleanExpression %= constantOrExpression; + constantBooleanExpression.name("constant boolean expression"); // This block defines the general root of all expressions. Most of the time, however, you may want to start with a more specialized rule. expression %= (booleanExpression | integerExpression | constantDoubleExpression); + 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))]; + labelDefinitionList %= *labelDefinition(qi::_r1); + + // 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)]; + stateRewardDefinition.name("state reward definition"); transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit(":") > constantDoubleExpression > qi::lit(";"))[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; - rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > freeIdentifierName > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) > qi::lit("endrewards"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_a, qi::_b)))]; + transitionRewardDefinition.name("transition reward definition"); + rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > freeIdentifierName > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_a, qi::_b)))]; + rewardDefinition.name("reward definition"); rewardDefinitionList = *rewardDefinition(qi::_r1); + rewardDefinitionList.name("reward definition list"); // This block defines auxiliary entities that are used to check whether a certain variable exist. - integerVariableName %= integerVariableNames_; booleanVariableName %= booleanVariableNames_; + booleanVariableName.name("boolean variable"); + integerVariableName %= integerVariableNames_; + integerVariableName.name("integer variable"); commandName %= commandNames_; + commandName.name("command name"); // This block defines all entities that are needed for parsing a single command. assignmentDefinition = (qi::lit("(") >> integerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[qi::_val = phoenix::construct(qi::_1, qi::_2)] | (qi::lit("(") > booleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[qi::_val = phoenix::construct(qi::_1, qi::_2)]; + assignmentDefinition.name("assignment"); assignmentDefinitionList %= assignmentDefinition % "&"; + assignmentDefinitionList.name("assignment list"); updateDefinition = (constantDoubleExpression > qi::lit(":") > assignmentDefinitionList)[qi::_val = phoenix::construct(qi::_1, qi::_2)]; + updateDefinition.name("update"); updateListDefinition = +updateDefinition % "+"; + updateListDefinition.name("update list"); commandDefinition = (qi::lit("[") > -((freeIdentifierName[phoenix::bind(commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit("->") > updateListDefinition > qi::lit(";"))[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; + commandDefinition.name("command"); // This block defines all entities that are neede for parsing variable definitions. - booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_b), qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableInfo_.add, qi::_1, qi::_val)]; - integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2, qi::_3, qi::_b), qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableInfo_.add, qi::_1, qi::_val)]; + booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct(phoenix::val("hallo"), qi::_b), qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), std::cout << phoenix::val("here!"), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1)]; + booleanVariableDefinition.name("boolean variable declaration"); + integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2, qi::_3, qi::_b), qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1)]; + integerVariableDefinition.name("integer variable declaration"); variableDefinition = (booleanVariableDefinition | integerVariableDefinition); + 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.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.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.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.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.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.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.name("undefined double constant declaration"); definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); + definedConstantDefinition.name("defined constant declaration"); undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); + undefinedConstantDefinition.name("undefined constant declaration"); constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); + constantDefinitionList.name("constant declaration list"); // This block defines all entities that are needed for parsing a program. modelTypeDefinition = modelType_; - start = (modelTypeDefinition > constantDefinitionList(qi::_a, qi::_b, qi::_c) > moduleDefinitionList > rewardDefinitionList(qi::_d))[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d)]; + modelTypeDefinition.name("model type"); + start = (modelTypeDefinition > constantDefinitionList(qi::_a, qi::_b, qi::_c) > moduleDefinitionList > rewardDefinitionList(qi::_d) > labelDefinitionList(qi::_e))[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; + start.name("probabilistic program declaration"); } // The starting point of the grammar. - qi::rule>, std::map>, std::map>, std::map>, Skipper> start; + qi::rule>, std::map>, std::map>, std::map, std::map>>, Skipper> start; qi::rule modelTypeDefinition; qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; qi::rule(), Skipper> moduleDefinitionList; @@ -192,6 +272,9 @@ private: qi::rule stateRewardDefinition; qi::rule, Skipper> transitionRewardDefinition; + qi::rule>&), Skipper> labelDefinitionList; + qi::rule>&), Skipper> labelDefinition; + qi::rule(), Skipper> constantDefinition; qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; qi::rule(), Skipper> definedConstantDefinition; @@ -203,6 +286,7 @@ private: qi::rule(), Skipper> definedDoubleConstantDefinition; qi::rule freeIdentifierName; + qi::rule identifierName; // The starting point for arbitrary expressions. qi::rule(), Skipper> expression; @@ -299,20 +383,12 @@ private: struct variablesStruct : qi::symbols> { // Intentionally left empty. This map is filled during parsing. - } integerVariables_, booleanVariables_, allVariables_; + } integerVariables_, booleanVariables_; struct entityNamesStruct : qi::symbols { // Intentionally left empty. This map is filled during parsing. } integerVariableNames_, booleanVariableNames_, commandNames_; - struct booleanVariableTypesStruct : qi::symbols { - // Intentionally left empty. This map is filled during parsing. - } booleanVariableInfo_; - - struct integerVariableTypesStruct : qi::symbols { - // Intentionally left empty. This map is filled during parsing. - } integerVariableInfo_; - struct constantsStruct : qi::symbols> { // Intentionally left empty. This map is filled during parsing. } integerConstants_, booleanConstants_, doubleConstants_, allConstants_; diff --git a/test.input b/test.input index 1b6636c6b..5339a8416 100644 --- a/test.input +++ b/test.input @@ -1,11 +1,6 @@ dtmc -const bool sic; -const int i; -const double e; - module die - // local state s : [0..7] init 0; // value of the dice @@ -19,10 +14,11 @@ d : [0..6] init 0; [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5); [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6); [] s=7 -> 1 : (s'=7); - endmodule rewards "coin_flips" [] s<7 : 1; s>3 : 1; endrewards + +label test = s>2;