From 6a33f845122b14213b6d61f00ee84c8e08e440a4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 11 Jan 2013 00:12:28 +0100 Subject: [PATCH] Another step towards PRISM model parsing: small models get recognized correctly. --- src/ir/Program.h | 2 ++ src/ir/RewardModel.h | 8 +++++++- src/ir/StateReward.h | 2 +- src/ir/TransitionReward.h | 2 +- src/parser/PrismParser.h | 17 +++++++++-------- test.input | 11 ++++++++++- 6 files changed, 30 insertions(+), 12 deletions(-) diff --git a/src/ir/Program.h b/src/ir/Program.h index 2ee72c08d..e2b94af57 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -12,6 +12,8 @@ #include "Module.h" #include "RewardModel.h" +#include + namespace storm { namespace ir { diff --git a/src/ir/RewardModel.h b/src/ir/RewardModel.h index 746eea70e..21c08fa75 100644 --- a/src/ir/RewardModel.h +++ b/src/ir/RewardModel.h @@ -8,6 +8,8 @@ #ifndef REWARDMODEL_H_ #define REWARDMODEL_H_ +#include + namespace storm { namespace ir { @@ -22,8 +24,12 @@ public: } + RewardModel(RewardModel const& other) : rewardModelName(other.rewardModelName), stateRewards(other.stateRewards), transitionRewards(other.transitionRewards) { + + } + std::string toString() { - std::string result = "rewards \"" + rewardModelName + "\n"; + std::string result = "rewards \"" + rewardModelName + "\"\n"; for (auto reward : stateRewards) { result += reward.toString() + "\n"; } diff --git a/src/ir/StateReward.h b/src/ir/StateReward.h index 2a0d23b69..9128c74ff 100644 --- a/src/ir/StateReward.h +++ b/src/ir/StateReward.h @@ -25,7 +25,7 @@ public: } std::string toString() { - return statePredicate->toString() + ": " + rewardValue->toString() + ";"; + return "\t" + statePredicate->toString() + ": " + rewardValue->toString() + ";"; } private: diff --git a/src/ir/TransitionReward.h b/src/ir/TransitionReward.h index 2181d5b05..d444560ec 100644 --- a/src/ir/TransitionReward.h +++ b/src/ir/TransitionReward.h @@ -25,7 +25,7 @@ public: } std::string toString() { - return "[" + commandName + "] " + statePredicate->toString() + ": " + rewardValue->toString() + ";"; + return "\t[" + commandName + "] " + statePredicate->toString() + ": " + rewardValue->toString() + ";"; } private: diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 67046b0ec..74735e5c9 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -58,7 +58,8 @@ 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) << " " << "^- here"; + 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; throw storm::exceptions::WrongFileFormatException() << msg.str(); } @@ -70,7 +71,7 @@ private: struct prismGrammar : qi::grammar>, std::map>, std::map>, std::map>, Skipper> { prismGrammar() : prismGrammar::base_type(start) { - freeIdentifierName %= qi::lexeme[(qi::alpha >> *(qi::alnum)) - allVariables_ - allConstants_]; + freeIdentifierName %= qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))] - allVariables_ - allConstants_; booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; integerLiteralExpression = qi::int_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; @@ -122,8 +123,8 @@ private: expression %= (booleanExpression | integerExpression | constantDoubleExpression); stateRewardDefinition = (booleanExpression > qi::lit(":") > constantDoubleExpression >> qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2)]; - transitionRewardDefinition = (qi::lit("[") > commandName > qi::lit("]") > booleanExpression > qi::lit(":") > constantDoubleExpression > qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, 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"))[qi::_r1[qi::_1] = phoenix::construct(qi::_1, qi::_a, qi::_b)]; + 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)))]; rewardDefinitionList = *rewardDefinition(qi::_r1); // This block defines auxiliary entities that are used to check whether a certain variable exist. @@ -151,9 +152,9 @@ private: 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(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), qi::_r1[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)]; - undefinedIntegerConstantDefinition = (qi::lit("const") > qi::lit("int") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), qi::_r1[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)]; - undefinedDoubleConstantDefinition = (qi::lit("const") > qi::lit("double") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), qi::_r1[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)]; + 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)]; + 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)]; + 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)]; definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); @@ -189,7 +190,7 @@ private: qi::rule&), Skipper> rewardDefinitionList; qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; qi::rule stateRewardDefinition; - qi::rule transitionRewardDefinition; + qi::rule, Skipper> transitionRewardDefinition; qi::rule(), Skipper> constantDefinition; qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; diff --git a/test.input b/test.input index e2e86d63a..1b6636c6b 100644 --- a/test.input +++ b/test.input @@ -1,5 +1,9 @@ dtmc +const bool sic; +const int i; +const double e; + module die // local state @@ -14,6 +18,11 @@ d : [0..6] init 0; [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3); [] 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); +[] s=7 -> 1 : (s'=7); endmodule + +rewards "coin_flips" + [] s<7 : 1; + s>3 : 1; +endrewards