diff --git a/src/ir/Assignment.h b/src/ir/Assignment.h index 308d1f27f..e6069d48f 100644 --- a/src/ir/Assignment.h +++ b/src/ir/Assignment.h @@ -35,7 +35,7 @@ public: } std::string toString() { - return variableName + "' = " + expression->toString(); + return "(" + variableName + "' = " + expression->toString() + ")"; } private: diff --git a/src/ir/BooleanVariable.h b/src/ir/BooleanVariable.h index 051982316..eccf92078 100644 --- a/src/ir/BooleanVariable.h +++ b/src/ir/BooleanVariable.h @@ -18,7 +18,7 @@ public: } - BooleanVariable(std::string variableName) : Variable(variableName) { + BooleanVariable(std::string variableName, std::shared_ptr initialValue = nullptr) : Variable(variableName, initialValue) { } @@ -27,7 +27,12 @@ public: } virtual std::string toString() { - return getVariableName() + ": bool;"; + std::string result = getVariableName() + ": bool"; + if (this->getInitialValue() != nullptr) { + result += " init " + this->getInitialValue()->toString(); + } + result += ";"; + return result; } }; diff --git a/src/ir/IR.h b/src/ir/IR.h index c919ca128..029e88fed 100644 --- a/src/ir/IR.h +++ b/src/ir/IR.h @@ -16,6 +16,8 @@ #include "BooleanVariable.h" #include "IntegerVariable.h" #include "Module.h" +#include "StateReward.h" +#include "TransitionReward.h" #include "RewardModel.h" #include "Program.h" diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h index 0e8ab9521..abde92cb3 100644 --- a/src/ir/IntegerVariable.h +++ b/src/ir/IntegerVariable.h @@ -16,11 +16,11 @@ namespace ir { class IntegerVariable : public Variable { public: - IntegerVariable() { + IntegerVariable() : lowerBound(nullptr), upperBound(nullptr) { } - IntegerVariable(std::string variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound) : Variable(variableName), lowerBound(lowerBound), upperBound(upperBound) { + IntegerVariable(std::string variableName, std::shared_ptr lowerBound, std::shared_ptr upperBound, std::shared_ptr initialValue = nullptr) : Variable(variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) { } @@ -29,7 +29,12 @@ public: } virtual std::string toString() { - return getVariableName() + ": int[" + lowerBound->toString() + ".." + upperBound->toString() + "];"; + std::string result = getVariableName() + ": [" + lowerBound->toString() + ".." + upperBound->toString() + "]"; + if (this->getInitialValue() != nullptr) { + result += " init " + this->getInitialValue()->toString(); + } + result += ";"; + return result; } private: diff --git a/src/ir/Module.h b/src/ir/Module.h index 02966a5a1..a1046db76 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -34,7 +34,6 @@ public: for (auto variable : booleanVariables) { result += "\t" + variable.toString() + "\n"; } - result += "\n"; for (auto variable : integerVariables) { result += "\t" + variable.toString() + "\n"; } diff --git a/src/ir/Program.h b/src/ir/Program.h index 16e213cab..2ee72c08d 100644 --- a/src/ir/Program.h +++ b/src/ir/Program.h @@ -19,9 +19,9 @@ namespace ir { class Program { public: - enum ModelType {DTMC, CTMC, MDP, CTMDP}; + enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP}; - Program() : modelType(DTMC), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards() { + Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards() { } @@ -30,6 +30,12 @@ public: } + Program(ModelType modelType, std::map> booleanUndefinedConstantExpressions, std::map> integerUndefinedConstantExpressions, std::map> doubleUndefinedConstantExpressions, std::vector modules) + : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards() { + + } + + Program(ModelType modelType, std::vector modules) : modelType(modelType), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(modules), rewards() { } @@ -37,10 +43,11 @@ public: std::string toString() { std::string result = ""; switch (modelType) { - case DTMC: result += "dtmc\n"; break; - case CTMC: result += "ctmc\n"; break; - case MDP: result += "mdp\n"; break; - case CTMDP: result += "ctmdp\n"; break; + case UNDEFINED: result += "undefined\n\n"; break; + case DTMC: result += "dtmc\n\n"; break; + case CTMC: result += "ctmc\n\n"; break; + case MDP: result += "mdp\n\n"; break; + case CTMDP: result += "ctmdp\n\n"; break; } for (auto element : booleanUndefinedConstantExpressions) { result += "const bool " + element.first + ";\n"; @@ -51,8 +58,15 @@ public: for (auto element : doubleUndefinedConstantExpressions) { result += "const double " + element.first + ";\n"; } + result += "\n"; for (auto mod : modules) { result += mod.toString(); + result += "\n"; + } + + for (auto rewardModel : rewards) { + result += rewardModel.second.toString(); + result +="\n"; } return result; diff --git a/src/ir/RewardModel.h b/src/ir/RewardModel.h index 16cb70f62..746eea70e 100644 --- a/src/ir/RewardModel.h +++ b/src/ir/RewardModel.h @@ -13,7 +13,31 @@ namespace storm { namespace ir { class RewardModel { - +public: + RewardModel() : rewardModelName(""), stateRewards(), transitionRewards() { + + } + + RewardModel(std::string rewardModelName, std::vector stateRewards, std::vector transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { + + } + + std::string toString() { + std::string result = "rewards \"" + rewardModelName + "\n"; + for (auto reward : stateRewards) { + result += reward.toString() + "\n"; + } + for (auto reward : transitionRewards) { + result += reward.toString() + "\n"; + } + result += "endrewards\n"; + return result; + } + +private: + std::string rewardModelName; + std::vector stateRewards; + std::vector transitionRewards; }; } diff --git a/src/ir/StateReward.h b/src/ir/StateReward.h new file mode 100644 index 000000000..2a0d23b69 --- /dev/null +++ b/src/ir/StateReward.h @@ -0,0 +1,40 @@ +/* + * StateReward.h + * + * Created on: Jan 10, 2013 + * Author: chris + */ + +#ifndef STATEREWARD_H_ +#define STATEREWARD_H_ + +#include "expressions/BaseExpression.h" + +namespace storm { + +namespace ir { + +class StateReward { +public: + StateReward() : statePredicate(nullptr), rewardValue(nullptr) { + + } + + StateReward(std::shared_ptr statePredicate, std::shared_ptr rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) { + + } + + std::string toString() { + return statePredicate->toString() + ": " + rewardValue->toString() + ";"; + } + +private: + std::shared_ptr statePredicate; + std::shared_ptr rewardValue; +}; + +} + +} + +#endif /* STATEREWARD_H_ */ diff --git a/src/ir/TransitionReward.h b/src/ir/TransitionReward.h new file mode 100644 index 000000000..2181d5b05 --- /dev/null +++ b/src/ir/TransitionReward.h @@ -0,0 +1,41 @@ +/* + * TransitionReward.h + * + * Created on: Jan 10, 2013 + * Author: chris + */ + +#ifndef TRANSITIONREWARD_H_ +#define TRANSITIONREWARD_H_ + +#include "expressions/BaseExpression.h" + +namespace storm { + +namespace ir { + +class TransitionReward { +public: + TransitionReward() : commandName(""), statePredicate(nullptr), rewardValue(nullptr) { + + } + + TransitionReward(std::string commandName, std::shared_ptr statePredicate, std::shared_ptr rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) { + + } + + std::string toString() { + return "[" + commandName + "] " + statePredicate->toString() + ": " + rewardValue->toString() + ";"; + } + +private: + std::string commandName; + std::shared_ptr statePredicate; + std::shared_ptr rewardValue; +}; + +} + +} + +#endif /* TRANSITIONREWARD_H_ */ diff --git a/src/ir/Variable.h b/src/ir/Variable.h index abb62df35..c015bb98b 100644 --- a/src/ir/Variable.h +++ b/src/ir/Variable.h @@ -14,11 +14,11 @@ namespace ir { class Variable { public: - Variable() { + Variable() : variableName(""), initialValue(nullptr) { } - Variable(std::string variableName) : variableName(variableName) { + Variable(std::string variableName, std::shared_ptr initialValue = nullptr) : variableName(variableName), initialValue(initialValue) { } @@ -34,8 +34,13 @@ public: return variableName; } + std::shared_ptr getInitialValue() { + return initialValue; + } + private: std::string variableName; + std::shared_ptr initialValue; }; } diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h index 47bd531bd..8ab6aba44 100644 --- a/src/ir/expressions/BinaryRelationExpression.h +++ b/src/ir/expressions/BinaryRelationExpression.h @@ -35,7 +35,7 @@ public: virtual std::string toString() const { std::string result = left->toString(); switch (relation) { - case EQUAL: result += " == "; break; + case EQUAL: result += " = "; break; case LESS: result += " < "; break; case LESS_OR_EQUAL: result += " <= "; break; case GREATER: result += " > "; break; diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 5706a2273..67046b0ec 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -8,13 +8,20 @@ #ifndef PRISMPARSER_H_ #define PRISMPARSER_H_ +#include #include #include +#include +#include #include #include #include "src/ir/IR.h" +#include +#include +#include + namespace storm { namespace parser { @@ -26,43 +33,43 @@ namespace phoenix = boost::phoenix; class PrismParser { public: - void test() { - std::string testInput = "" \ - "" \ - "const bool d; const int c; const double x;" \ - "module test " \ - " a : bool;" \ - "endmodule" \ - "module test2 endmodule"; - getProgram(testInput); + void test(std::string const& fileName) { + std::ifstream inputFileStream(fileName, std::ios::in); + getProgram(inputFileStream, fileName); + inputFileStream.close(); } - void getProgram(std::string inputString) { + 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; + storm::ir::Program result; - prismGrammar grammar(result); - std::string::const_iterator it = inputString.begin(); - std::string::const_iterator end = inputString.end(); - - storm::ir::Program realResult; - bool r = phrase_parse(it, end, grammar, ascii::space, realResult); - - if (r && it == end) { - std::cout << "Parsing successful!" << std::endl; - std::cout << realResult.toString() << std::endl; - } else { - std::string rest(it, end); - std::cout << "-------------------------\n"; - std::cout << "Parsing failed\n"; - std::cout << "stopped at: \"" << rest << "\"\n"; - std::cout << "-------------------------\n"; + 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 << "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"; + throw storm::exceptions::WrongFileFormatException() << msg.str(); } + + std::cout << result.toString(); } private: - template - struct prismGrammar : qi::grammar { + template + struct prismGrammar : qi::grammar>, std::map>, std::map>, std::map>, Skipper> { - prismGrammar(storm::ir::Program& program) : prismGrammar::base_type(start), program(program) { + prismGrammar() : prismGrammar::base_type(start) { freeIdentifierName %= qi::lexeme[(qi::alpha >> *(qi::alnum)) - allVariables_ - allConstants_]; booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; @@ -84,120 +91,167 @@ private: integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; integerExpression %= integerPlusExpression; - atomicDoubleExpression %= (qi::lit("(") >> doubleExpression >> qi::lit(")") | doubleConstantExpression); - doubleMultExpression %= atomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicDoubleExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; - doublePlusExpression %= doubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> doubleMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; - doubleExpression %= doublePlusExpression; + constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); + constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; + constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + constantIntegerExpression %= constantIntegerPlusExpression; + + // 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); + constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))]; + constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))]; + constantDoubleExpression %= constantDoublePlusExpression; + // This block defines all expressions of type boolean. relativeExpression = (integerExpression >> relations_ >> integerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, qi::_3, qi::_2))]; - atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); - andExpression = atomicBooleanExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> atomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))]; + atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanConstantExpression); + notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))]; + andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))]; orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))]; booleanExpression %= orExpression; - expression %= (booleanExpression | integerExpression | doubleExpression); + // 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))]; + constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); + constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))]; + constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))]; + constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))]; + constantBooleanExpression %= constantOrExpression; - booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") >> qi::lit(";"))[qi::_val = phoenix::construct(qi::_1), 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("[") >> integerConstantExpression >> qi::lit("..") >> integerConstantExpression >> qi::lit("]") >> qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2, qi::_3), 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)]; - variableDefinition = (booleanVariableDefinition | integerVariableDefinition); + // 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); - 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)), 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::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::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 | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition); - // constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition); + 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)]; + rewardDefinitionList = *rewardDefinition(qi::_r1); + // This block defines auxiliary entities that are used to check whether a certain variable exist. integerVariableName %= integerVariableNames_; booleanVariableName %= booleanVariableNames_; + commandName %= commandNames_; - assignmentDefinition = (qi::lit("(") >> integerVariableName >> qi::lit("'") >> integerExpression >> qi::lit(")"))[qi::_val = phoenix::construct(qi::_1, qi::_2)] | (qi::lit("(") >> booleanVariableName >> qi::lit("'") >> booleanExpression >> qi::lit(")"))[qi::_val = phoenix::construct(qi::_1, qi::_2)]; + // 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)]; assignmentDefinitionList %= assignmentDefinition % "&"; - updateDefinition = (doubleConstantExpression >> qi::lit(":") >> assignmentDefinitionList)[qi::_val = phoenix::construct(qi::_1, qi::_2)]; - updateListDefinition = +updateDefinition; - commandDefinition = (qi::lit("[") >> freeIdentifierName >> qi::lit("]") >> booleanExpression >> qi::lit("->") >> updateListDefinition >> qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2, qi::_3)]; + updateDefinition = (constantDoubleExpression > qi::lit(":") > assignmentDefinitionList)[qi::_val = phoenix::construct(qi::_1, qi::_2)]; + updateListDefinition = +updateDefinition % "+"; + 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)]; - 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)]; + // 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)]; + variableDefinition = (booleanVariableDefinition | integerVariableDefinition); - moduleDefinitionList = +moduleDefinition; + // 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)]; + moduleDefinitionList %= +moduleDefinition; + + // 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]; + 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)]; + definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); + undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); + constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); - start = (*(definedConstantDefinition | (undefinedBooleanConstantDefinition[phoenix::push_back(qi::_a, qi::_1)] | undefinedIntegerConstantDefinition[phoenix::push_back(qi::_b, qi::_1)] | undefinedDoubleConstantDefinition[phoenix::push_back(qi::_c, qi::_1)])) >> moduleDefinitionList)[qi::_val = phoenix::construct(storm::ir::Program::ModelType::DTMC, qi::_a, qi::_b, qi::_c, qi::_1)]; + // 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)]; } // The starting point of the grammar. - qi::rule>,std::vector>,std::vector>>, ascii::space_type> start; - qi::rule constantDefinitionList; - qi::rule(), ascii::space_type> moduleDefinitionList; + qi::rule>, std::map>, std::map>, std::map>, Skipper> start; + qi::rule modelTypeDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; + qi::rule(), Skipper> moduleDefinitionList; - qi::rule, std::vector>, ascii::space_type> moduleDefinition; + qi::rule, std::vector>, Skipper> moduleDefinition; - qi::rule variableDefinition; - qi::rule>, ascii::space_type> booleanVariableDefinition; - qi::rule>, ascii::space_type> integerVariableDefinition; + qi::rule variableDefinition; + qi::rule, std::shared_ptr>, Skipper> booleanVariableDefinition; + qi::rule, std::shared_ptr>, Skipper> integerVariableDefinition; - qi::rule commandDefinition; + qi::rule, Skipper> commandDefinition; - qi::rule(), ascii::space_type> updateListDefinition; - qi::rule updateDefinition; - qi::rule(), ascii::space_type> assignmentDefinitionList; - qi::rule assignmentDefinition; + qi::rule(), Skipper> updateListDefinition; + qi::rule updateDefinition; + qi::rule(), Skipper> assignmentDefinitionList; + qi::rule assignmentDefinition; - qi::rule integerVariableName; - qi::rule booleanVariableName; + qi::rule integerVariableName; + qi::rule booleanVariableName; + qi::rule commandName; - qi::rule(), ascii::space_type> constantDefinition; - qi::rule undefinedConstantDefinition; - qi::rule(), ascii::space_type> definedConstantDefinition; - qi::rule>, ascii::space_type> undefinedBooleanConstantDefinition; - qi::rule>, ascii::space_type> undefinedIntegerConstantDefinition; - qi::rule>, ascii::space_type> undefinedDoubleConstantDefinition; - qi::rule(), ascii::space_type> definedBooleanConstantDefinition; - qi::rule(), ascii::space_type> definedIntegerConstantDefinition; - qi::rule(), ascii::space_type> definedDoubleConstantDefinition; + qi::rule&), Skipper> rewardDefinitionList; + qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; + qi::rule stateRewardDefinition; + qi::rule transitionRewardDefinition; - qi::rule freeIdentifierName; + qi::rule(), Skipper> constantDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; + qi::rule(), Skipper> definedConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; + qi::rule(), Skipper> definedBooleanConstantDefinition; + qi::rule(), Skipper> definedIntegerConstantDefinition; + qi::rule(), Skipper> definedDoubleConstantDefinition; + + qi::rule freeIdentifierName; // The starting point for arbitrary expressions. - qi::rule(), ascii::space_type> expression; + qi::rule(), Skipper> expression; // Rules with boolean result type. - qi::rule(), ascii::space_type> booleanExpression; - qi::rule(), ascii::space_type> orExpression; - qi::rule(), ascii::space_type> andExpression; - qi::rule(), ascii::space_type> atomicBooleanExpression; - qi::rule(), ascii::space_type> relativeExpression; + qi::rule(), Skipper> booleanExpression; + qi::rule(), Skipper> orExpression; + qi::rule(), Skipper> andExpression; + qi::rule(), Skipper> notExpression; + qi::rule(), Skipper> atomicBooleanExpression; + qi::rule(), Skipper> relativeExpression; + qi::rule(), Skipper> constantBooleanExpression; + qi::rule(), Skipper> constantOrExpression; + qi::rule(), Skipper> constantAndExpression; + qi::rule(), Skipper> constantNotExpression; + qi::rule(), Skipper> constantAtomicBooleanExpression; + qi::rule(), Skipper> constantRelativeExpression; // Rules with integer result type. - qi::rule(), ascii::space_type> integerExpression; - qi::rule(), ascii::space_type> integerPlusExpression; - qi::rule(), ascii::space_type> integerMultExpression; - qi::rule(), ascii::space_type> atomicIntegerExpression; + qi::rule(), Skipper> integerExpression; + qi::rule(), Skipper> integerPlusExpression; + qi::rule(), Skipper> integerMultExpression; + qi::rule(), Skipper> atomicIntegerExpression; + qi::rule(), Skipper> constantIntegerExpression; + qi::rule(), Skipper> constantIntegerPlusExpression; + qi::rule(), Skipper> constantIntegerMultExpression; + qi::rule(), Skipper> constantAtomicIntegerExpression; // Rules with double result type. - qi::rule(), ascii::space_type> doubleExpression; - qi::rule(), ascii::space_type> doublePlusExpression; - qi::rule(), ascii::space_type> doubleMultExpression; - qi::rule(), ascii::space_type> atomicDoubleExpression; + qi::rule(), Skipper> constantDoubleExpression; + qi::rule(), Skipper> constantDoublePlusExpression; + qi::rule(), Skipper> constantDoubleMultExpression; + qi::rule(), Skipper> constantAtomicDoubleExpression; // Rules for variable recognition. - qi::rule(), ascii::space_type> variableExpression; - qi::rule(), ascii::space_type> booleanVariableExpression; - qi::rule(), ascii::space_type> integerVariableExpression; + qi::rule(), Skipper> variableExpression; + qi::rule(), Skipper> booleanVariableExpression; + qi::rule(), Skipper> integerVariableExpression; // Rules for constant recognition. - qi::rule(), ascii::space_type> constantExpression; - qi::rule(), ascii::space_type> booleanConstantExpression; - qi::rule(), ascii::space_type> integerConstantExpression; - qi::rule(), ascii::space_type> doubleConstantExpression; + qi::rule(), Skipper> constantExpression; + qi::rule(), Skipper> booleanConstantExpression; + qi::rule(), Skipper> integerConstantExpression; + qi::rule(), Skipper> doubleConstantExpression; // Rules for literal recognition. - qi::rule(), ascii::space_type> literalExpression; - qi::rule(), ascii::space_type> booleanLiteralExpression; - qi::rule(), ascii::space_type> integerLiteralExpression; - qi::rule(), ascii::space_type> doubleLiteralExpression; + qi::rule(), Skipper> literalExpression; + qi::rule(), Skipper> booleanLiteralExpression; + qi::rule(), Skipper> integerLiteralExpression; + qi::rule(), Skipper> doubleLiteralExpression; struct keywordsStruct : qi::symbols { keywordsStruct() { @@ -219,10 +273,21 @@ private: } } keywords_; + struct modelTypeStruct : qi::symbols { + modelTypeStruct() { + add + ("dtmc", storm::ir::Program::ModelType::DTMC) + ("ctmc", storm::ir::Program::ModelType::CTMC) + ("mdp", storm::ir::Program::ModelType::MDP) + ("ctmdp", storm::ir::Program::ModelType::CTMDP) + ; + } + } modelType_; + struct relationalOperatorStruct : qi::symbols { relationalOperatorStruct() { add - ("==", storm::ir::expressions::BinaryRelationExpression::EQUAL) + ("=", storm::ir::expressions::BinaryRelationExpression::EQUAL) ("<", storm::ir::expressions::BinaryRelationExpression::LESS) ("<=", storm::ir::expressions::BinaryRelationExpression::LESS_OR_EQUAL) (">", storm::ir::expressions::BinaryRelationExpression::GREATER) @@ -235,9 +300,9 @@ private: // Intentionally left empty. This map is filled during parsing. } integerVariables_, booleanVariables_, allVariables_; - struct variableNamesStruct : qi::symbols { + struct entityNamesStruct : qi::symbols { // Intentionally left empty. This map is filled during parsing. - } integerVariableNames_, booleanVariableNames_; + } integerVariableNames_, booleanVariableNames_, commandNames_; struct booleanVariableTypesStruct : qi::symbols { // Intentionally left empty. This map is filled during parsing. @@ -266,8 +331,6 @@ private: struct modulesStruct : qi::symbols { // Intentionally left empty. This map is filled during parsing. } modules_; - - storm::ir::Program& program; }; }; diff --git a/src/storm.cpp b/src/storm.cpp index 0a08d6064..faba3559b 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(); + parser.test("test.input"); cleanUp(); return 0; diff --git a/test.input b/test.input new file mode 100644 index 000000000..e2e86d63a --- /dev/null +++ b/test.input @@ -0,0 +1,19 @@ +dtmc + +module die + +// local state +s : [0..7] init 0; +// value of the dice +d : [0..6] init 0; + +[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2); +[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4); +[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6); +[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1); +[] 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); + +endmodule