sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Splitted PrismParser class into header and implementation file. Commented both files properly. Cleaned interface of PrismParser.

tempestpy_adaptions
dehnert 12 years ago
parent
f52201466c
commit
4b7c6a8941
4 changed files with 195 additions and 90 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/ir/expressions/DoubleLiteral.h
  2. 115
      src/parser/PrismParser.cpp
  3. 166
      src/parser/PrismParser.h
  4. 2
      src/storm.cpp

2
src/ir/expressions/DoubleLiteral.h
View File

@ -10,6 +10,8 @@
#include "src/ir/expressions/BaseExpression.h"
#include "boost/lexical_cast.hpp"
namespace storm {
namespace ir {

115
src/parser/PrismParser.cpp
View File

@ -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 <boost/spirit/include/classic_position_iterator.hpp>
#include <boost/spirit/include/support_multi_pass.hpp>
// Needed for file IO.
#include <fstream>
#include <iomanip>
// Some typedefs and namespace definitions to reduce code size.
typedef std::istreambuf_iterator<char> base_iterator_type;
typedef boost::spirit::multi_pass<base_iterator_type> forward_iterator_type;
typedef boost::spirit::classic::position_iterator2<forward_iterator_type> 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<storm::ir::Program> PrismParser::parseFile(std::string const& filename) const {
// Open file and initialize result.
std::ifstream inputFileStream(filename, std::ios::in);
std::shared_ptr<storm::ir::Program> result(nullptr);
// Now try to parse the contents of the file.
try {
result = std::shared_ptr<storm::ir::Program>(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<storm::ir::Program> 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<storm::ir::Program> 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<pos_iterator_type, BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(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<pos_iterator_type>& 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<std::string>& 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

166
src/parser/PrismParser.h
View File

@ -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 <boost/typeof/typeof.hpp>
#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix.hpp>
#include <boost/spirit/include/support_multi_pass.hpp>
#include <boost/spirit/include/classic_position_iterator.hpp>
#include <boost/fusion/include/adapt_struct.hpp>
#include <boost/fusion/include/io.hpp>
// All classes of the intermediate representation are used.
#include "src/ir/IR.h"
// Used for file input.
#include <istream>
#include <fstream>
#include <iomanip>
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<char> base_iterator_type;
typedef boost::spirit::multi_pass<base_iterator_type> forward_iterator_type;
typedef boost::spirit::classic::position_iterator2<forward_iterator_type> 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<pos_iterator_type, BOOST_TYPEOF(ascii::space | qi::lit("//") >> *(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<pos_iterator_type>& e) {
const boost::spirit::classic::file_position_base<std::string>& 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<storm::ir::Program> 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<storm::ir::Program> 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<typename Iterator, typename Skipper>
struct prismGrammar : qi::grammar<Iterator, storm::ir::Program(), qi::locals<std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>, std::map<std::string, storm::ir::RewardModel>, std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>>>, 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<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BooleanLiteral>(qi::_1))];
booleanLiteralExpression.name("boolean literal");
integerLiteralExpression = qi::int_[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::IntegerLiteral>(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<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(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<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(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<std::pair<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>>>(qi::_1, qi::_2))];
labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> freeIdentifierName >> -qi::lit("\"") >> qi::lit("=") >> booleanExpression >> qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>>>(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<storm::ir::StateReward>(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<storm::ir::Module>(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<storm::ir::Module>(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<std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>(phoenix::new_<storm::ir::expressions::BooleanConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>>(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<std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>(phoenix::new_<storm::ir::expressions::BooleanConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>>(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<std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>(phoenix::new_<storm::ir::expressions::IntegerConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>>(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<std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>(phoenix::new_<storm::ir::expressions::IntegerConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>>(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<std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>(phoenix::new_<storm::ir::expressions::DoubleConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>>(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<std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>(phoenix::new_<storm::ir::expressions::DoubleConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>>(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<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>&), Skipper> constantDefinitionList;
qi::rule<Iterator, std::vector<storm::ir::Module>(), Skipper> moduleDefinitionList;
// Rules for module definition.
qi::rule<Iterator, storm::ir::Module(), qi::locals<std::vector<storm::ir::BooleanVariable>, std::vector<storm::ir::IntegerVariable>>, Skipper> moduleDefinition;
// Rules for variable definitions.
qi::rule<Iterator, qi::unused_type(), Skipper> variableDefinition;
qi::rule<Iterator, storm::ir::BooleanVariable(), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> booleanVariableDefinition;
qi::rule<Iterator, storm::ir::IntegerVariable(), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> integerVariableDefinition;
// Rules for command definitions.
qi::rule<Iterator, storm::ir::Command(), qi::locals<std::string>, Skipper> commandDefinition;
qi::rule<Iterator, std::vector<storm::ir::Update>(), Skipper> updateListDefinition;
qi::rule<Iterator, storm::ir::Update(), Skipper> updateDefinition;
qi::rule<Iterator, std::vector<storm::ir::Assignment>(), Skipper> assignmentDefinitionList;
qi::rule<Iterator, storm::ir::Assignment(), Skipper> assignmentDefinition;
// Rules for variable/command names.
qi::rule<Iterator, std::string(), Skipper> integerVariableName;
qi::rule<Iterator, std::string(), Skipper> booleanVariableName;
qi::rule<Iterator, std::string(), Skipper> commandName;
// Rules for reward definitions.
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::RewardModel>&), Skipper> rewardDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::RewardModel>&), qi::locals<std::vector<storm::ir::StateReward>, std::vector<storm::ir::TransitionReward>>, Skipper> rewardDefinition;
qi::rule<Iterator, storm::ir::StateReward(), Skipper> stateRewardDefinition;
qi::rule<Iterator, storm::ir::TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
// Rules for label definitions.
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>>&), Skipper> labelDefinitionList;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>>&), Skipper> labelDefinition;
// Rules for constant definitions.
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> constantDefinition;
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> definedConstantDefinition;
@ -338,6 +341,7 @@ private:
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> integerLiteralExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), Skipper> doubleLiteralExpression;
// A structure defining the keywords that are not allowed to be chosen as identifiers.
struct keywordsStruct : qi::symbols<char, unsigned> {
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<char, storm::ir::Program::ModelType> {
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<char, storm::ir::expressions::BinaryRelationExpression::RelationType> {
relationalOperatorStruct() {
add
@ -381,33 +389,13 @@ private:
}
} relations_;
struct variablesStruct : qi::symbols<char, std::shared_ptr<storm::ir::expressions::BaseExpression>> {
// Intentionally left empty. This map is filled during parsing.
} integerVariables_, booleanVariables_;
struct entityNamesStruct : qi::symbols<char, std::string> {
// Intentionally left empty. This map is filled during parsing.
} integerVariableNames_, booleanVariableNames_, commandNames_;
struct constantsStruct : qi::symbols<char, std::shared_ptr<storm::ir::expressions::BaseExpression>> {
// Intentionally left empty. This map is filled during parsing.
} integerConstants_, booleanConstants_, doubleConstants_, allConstants_;
struct undefinedBooleanConstantsTypesStruct : qi::symbols<char, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> {
// Intentionally left empty. This map is filled during parsing.
} booleanConstantInfo_;
struct undefinedIntegerConstantsTypesStruct : qi::symbols<char, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> {
// Intentionally left empty. This map is filled during parsing.
} integerConstantInfo_;
struct undefinedDoubleConstantsTypesStruct : qi::symbols<char, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> {
// 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<char, std::shared_ptr<storm::ir::expressions::BaseExpression>> integerVariables_, booleanVariables_;
struct qi::symbols<char, std::shared_ptr<storm::ir::expressions::BaseExpression>> integerConstants_, booleanConstants_, doubleConstants_;
struct modulesStruct : qi::symbols<char, unsigned> {
// Intentionally left empty. This map is filled during parsing.
} modules_;
// A structure representing the identity function over identifier names.
struct qi::symbols<char, std::string> integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_;
};
};
@ -415,4 +403,4 @@ private:
} // namespace storm
#endif /* PRISMPARSER_H_ */
#endif /* STORM_PARSER_PRISMPARSER_H_ */

2
src/storm.cpp
View File

@ -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;

Write Preview
Loading…
Cancel
Save