From c76e0e8d4d63be0f7371807bd5e15499fd809c39 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 5 May 2014 14:41:17 +0200 Subject: [PATCH] Added class for initial construct of PRISM programs (to capture position information). Added more validity checks for programs and tests for them (not all though). Former-commit-id: cf4e985684a225d4f99e9ad58d7737cd67409e3e --- src/parser/PrismParser.cpp | 38 +-- src/parser/PrismParser.h | 16 +- src/storage/expressions/BaseExpression.cpp | 7 +- .../expressions/SubstitutionVisitor.cpp | 4 +- src/storage/expressions/TypeCheckVisitor.cpp | 12 +- src/storage/prism/Command.cpp | 2 +- src/storage/prism/Constant.cpp | 4 +- src/storage/prism/Formula.cpp | 4 +- src/storage/prism/InitialConstruct.cpp | 24 ++ src/storage/prism/InitialConstruct.h | 56 ++++ src/storage/prism/Label.cpp | 4 +- src/storage/prism/LocatedInformation.cpp | 4 +- src/storage/prism/Module.cpp | 3 +- src/storage/prism/Program.cpp | 265 ++++++++++++++---- src/storage/prism/Program.h | 35 +-- src/storage/prism/Update.cpp | 2 +- test/functional/parser/PrismParserTest.cpp | 184 ++++++------ 17 files changed, 442 insertions(+), 222 deletions(-) create mode 100644 src/storage/prism/InitialConstruct.cpp create mode 100644 src/storage/prism/InitialConstruct.h diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index ffda5e219..727579dff 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -5,7 +5,7 @@ namespace storm { namespace parser { - storm::prism::Program PrismParser::parse(std::string const& filename, bool typeCheck) { + storm::prism::Program PrismParser::parse(std::string const& filename) { // Open file and initialize result. std::ifstream inputFileStream(filename, std::ios::in); LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'."); @@ -15,7 +15,7 @@ namespace storm { // Now try to parse the contents of the file. try { std::string fileContent((std::istreambuf_iterator(inputFileStream)), (std::istreambuf_iterator())); - result = parseFromString(fileContent, filename, typeCheck); + result = parseFromString(fileContent, filename); } catch(std::exception& e) { // In case of an exception properly close the file before passing exception. inputFileStream.close(); @@ -27,7 +27,7 @@ namespace storm { return result; } - storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename, bool typeCheck) { + storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename) { PositionIteratorType first(input.begin()); PositionIteratorType iter = first; PositionIteratorType last(input.end()); @@ -38,17 +38,17 @@ namespace storm { // Create grammar. storm::parser::PrismParser grammar(filename, first); try { - // Now parse the content using phrase_parse in order to be able to supply a skipping parser. + // Start first run. bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in first pass."); - if (typeCheck) { - first = PositionIteratorType(input.begin()); - iter = first; - last = PositionIteratorType(input.end()); - grammar.moveToSecondRun(); - succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); - LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in second pass."); - } + + // Start second run. + first = PositionIteratorType(input.begin()); + iter = first; + last = PositionIteratorType(input.end()); + grammar.moveToSecondRun(); + succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); + LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in second pass."); } catch (qi::expectation_failure const& e) { // If the parser expected content different than the one provided, display information about the location of the error. std::size_t lineNumber = boost::spirit::get_line(e.first); @@ -162,7 +162,7 @@ namespace storm { >> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; rewardModelDefinition.name("reward model definition"); - initialStatesConstruct = (qi::lit("init") > expression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesExpression, phoenix::ref(*this), qi::_1, qi::_r1)]; + initialStatesConstruct = (qi::lit("init") > expression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)]; initialStatesConstruct.name("initial construct"); labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)]; @@ -264,13 +264,13 @@ namespace storm { return true; } - bool PrismParser::addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { - LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs."); - if (globalProgramInformation.hasInitialStatesExpression) { + bool PrismParser::addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { + LOG_THROW(!globalProgramInformation.hasInitialConstruct, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs."); + if (globalProgramInformation.hasInitialConstruct) { return false; } - globalProgramInformation.hasInitialStatesExpression = true; - globalProgramInformation.initialStatesExpression = initialStatesExpression; + globalProgramInformation.hasInitialConstruct = true; + globalProgramInformation.initialConstruct = storm::prism::InitialConstruct(initialStatesExpression, this->getFilename(), get_line(qi::_3)); return true; } @@ -762,7 +762,7 @@ namespace storm { } storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const { - return storm::prism::Program(globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, globalProgramInformation.hasInitialStatesExpression, globalProgramInformation.initialStatesExpression, globalProgramInformation.labels, this->getFilename()); + return storm::prism::Program(globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun); } } // namespace parser } // namespace storm diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 3312768c3..e1a9136ba 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -35,7 +35,9 @@ namespace storm { class GlobalProgramInformation { public: // Default construct the header information. - GlobalProgramInformation() : hasInitialStatesExpression(false), currentCommandIndex(0), currentUpdateIndex(0) {} + GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), modules(), rewardModels(), labels(),hasInitialConstruct(false), initialConstruct(storm::expressions::Expression::createFalse()), currentCommandIndex(0), currentUpdateIndex(0) { + // Intentionally left empty. + } // Members for all essential information that needs to be collected. storm::prism::Program::ModelType modelType; @@ -47,8 +49,8 @@ namespace storm { std::vector modules; std::vector rewardModels; std::vector labels; - storm::expressions::Expression initialStatesExpression; - bool hasInitialStatesExpression; + bool hasInitialConstruct; + storm::prism::InitialConstruct initialConstruct; // Counters to provide unique indexing for commands and updates. uint_fast64_t currentCommandIndex; @@ -61,20 +63,18 @@ namespace storm { * Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax. * * @param filename the name of the file to parse. - * @param typeCheck Sets whether the expressions are generated and therefore typechecked. * @return The resulting PRISM program. */ - static storm::prism::Program parse(std::string const& filename, bool typeCheck = true); + static storm::prism::Program parse(std::string const& filename); /*! * Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM syntax. * * @param input The input string to parse. * @param filename The name of the file from which the input was read. - * @param typeCheck Sets whether the expressions are generated and therefore typechecked. * @return The resulting PRISM program. */ - static storm::prism::Program parseFromString(std::string const& input, std::string const& filename, bool typeCheck = true); + static storm::prism::Program parseFromString(std::string const& input, std::string const& filename); private: struct modelTypeStruct : qi::symbols { @@ -263,7 +263,7 @@ namespace storm { // Helper methods used in the grammar. bool isValidIdentifier(std::string const& identifier); - bool addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); + bool addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation); storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const; storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const; diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp index b9734a9ad..bb4ea0921 100644 --- a/src/storage/expressions/BaseExpression.cpp +++ b/src/storage/expressions/BaseExpression.cpp @@ -53,7 +53,12 @@ namespace storm { } std::ostream& operator<<(std::ostream& stream, ExpressionReturnType const& enumValue) { - stream << static_cast::type>(enumValue); + switch (enumValue) { + case ExpressionReturnType::Undefined: stream << "undefined"; break; + case ExpressionReturnType::Bool: stream << "bool"; break; + case ExpressionReturnType::Int: stream << "int"; break; + case ExpressionReturnType::Double: stream << "double"; break; + } return stream; } diff --git a/src/storage/expressions/SubstitutionVisitor.cpp b/src/storage/expressions/SubstitutionVisitor.cpp index 402febc2e..7990ab4f9 100644 --- a/src/storage/expressions/SubstitutionVisitor.cpp +++ b/src/storage/expressions/SubstitutionVisitor.cpp @@ -182,7 +182,7 @@ namespace storm { } // Explicitly instantiate the class with map and unordered_map. - template class SubstitutionVisitor< std::map >; - template class SubstitutionVisitor< std::unordered_map >; + template class SubstitutionVisitor>; + template class SubstitutionVisitor>; } } diff --git a/src/storage/expressions/TypeCheckVisitor.cpp b/src/storage/expressions/TypeCheckVisitor.cpp index b1cd6a205..d5cef0381 100644 --- a/src/storage/expressions/TypeCheckVisitor.cpp +++ b/src/storage/expressions/TypeCheckVisitor.cpp @@ -45,28 +45,28 @@ namespace storm { void TypeCheckVisitor::visit(BooleanConstantExpression const* expression) { auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName()); LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'."); - LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected bool, but found " << expression->getReturnType() << "."); + LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'bool', but found '" << expression->getReturnType() << "'."); } template void TypeCheckVisitor::visit(DoubleConstantExpression const* expression) { auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName()); LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'."); - LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected double, but found " << expression->getReturnType() << "."); + LOG_THROW(identifierTypePair->second == ExpressionReturnType::Double, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'double', but found '" << expression->getReturnType() << "'."); } template void TypeCheckVisitor::visit(IntegerConstantExpression const* expression) { auto identifierTypePair = this->identifierToTypeMap.find(expression->getConstantName()); LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getConstantName() << "'."); - LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected int, but found " << expression->getReturnType() << "."); + LOG_THROW(identifierTypePair->second == ExpressionReturnType::Int, storm::exceptions::InvalidTypeException, "Type mismatch for constant '" << expression->getConstantName() << "': expected 'int', but found '" << expression->getReturnType() << "'."); } template void TypeCheckVisitor::visit(VariableExpression const* expression) { auto identifierTypePair = this->identifierToTypeMap.find(expression->getVariableName()); LOG_THROW(identifierTypePair != this->identifierToTypeMap.end(), storm::exceptions::InvalidArgumentException, "No type available for identifier '" << expression->getVariableName() << "'."); - LOG_THROW(identifierTypePair->second == ExpressionReturnType::Bool, storm::exceptions::InvalidTypeException, "Type mismatch for variable '" << expression->getVariableName() << "': expected " << identifierTypePair->first << ", but found " << expression->getReturnType() << "."); + LOG_THROW(identifierTypePair->second == expression->getReturnType(), storm::exceptions::InvalidTypeException, "Type mismatch for variable '" << expression->getVariableName() << "': expected '" << identifierTypePair->first << "', but found '" << expression->getReturnType() << "'."); } template @@ -93,5 +93,9 @@ namespace storm { void TypeCheckVisitor::visit(DoubleLiteralExpression const* expression) { // Intentionally left empty. } + + // Explicitly instantiate the class with map and unordered_map. + template class TypeCheckVisitor>; + template class TypeCheckVisitor>; } } \ No newline at end of file diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp index 4b36942df..4c1619732 100644 --- a/src/storage/prism/Command.cpp +++ b/src/storage/prism/Command.cpp @@ -51,5 +51,5 @@ namespace storm { stream << ";"; return stream; } - } // namespace ir + } // namespace prism } // namespace storm diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp index 641336c76..c02deea99 100644 --- a/src/storage/prism/Constant.cpp +++ b/src/storage/prism/Constant.cpp @@ -48,5 +48,5 @@ namespace storm { stream << ";"; return stream; } - } -} \ No newline at end of file + } // namespace prism +} // namespace storm \ No newline at end of file diff --git a/src/storage/prism/Formula.cpp b/src/storage/prism/Formula.cpp index fbda0c69d..a120078b8 100644 --- a/src/storage/prism/Formula.cpp +++ b/src/storage/prism/Formula.cpp @@ -26,5 +26,5 @@ namespace storm { stream << "formula " << formula.getName() << " = " << formula.getExpression() << ";"; return stream; } - } -} \ No newline at end of file + } // namespace prism +} // namespace storm \ No newline at end of file diff --git a/src/storage/prism/InitialConstruct.cpp b/src/storage/prism/InitialConstruct.cpp new file mode 100644 index 000000000..61c662843 --- /dev/null +++ b/src/storage/prism/InitialConstruct.cpp @@ -0,0 +1,24 @@ +#include "src/storage/prism/InitialConstruct.h" + +namespace storm { + namespace prism { + InitialConstruct::InitialConstruct(storm::expressions::Expression initialStatesExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), initialStatesExpression(initialStatesExpression) { + // Intentionally left empty. + } + + storm::expressions::Expression InitialConstruct::getInitialStatesExpression() const { + return this->initialStatesExpression; + } + + InitialConstruct InitialConstruct::substitute(std::map const& substitution) const { + return InitialConstruct(this->getInitialStatesExpression().substitute(substitution)); + } + + std::ostream& operator<<(std::ostream& stream, InitialConstruct const& initialConstruct) { + stream << "initial " << std::endl; + stream << "\t" << initialConstruct.getInitialStatesExpression() << std::endl; + stream << "endinitial" << std::endl; + return stream; + } + } // namespace prism +} // namespace storm \ No newline at end of file diff --git a/src/storage/prism/InitialConstruct.h b/src/storage/prism/InitialConstruct.h new file mode 100644 index 000000000..6f7f6adb9 --- /dev/null +++ b/src/storage/prism/InitialConstruct.h @@ -0,0 +1,56 @@ +#ifndef STORM_STORAGE_PRISM_INITIALCONSTRUCT_H_ +#define STORM_STORAGE_PRISM_INITIALCONSTRUCT_H_ + +#include + +#include "src/storage/prism/LocatedInformation.h" +#include "src/storage/expressions/Expression.h" +#include "src/utility/OsDetection.h" + +namespace storm { + namespace prism { + class InitialConstruct : public LocatedInformation { + public: + /*! + * Creates an initial construct with the given expression. + * + * @param initialStatesExpression An expression characterizing the initial states. + * @param filename The filename in which the command is defined. + * @param lineNumber The line number in which the command is defined. + */ + InitialConstruct(storm::expressions::Expression initialStatesExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0); + + // Create default implementations of constructors/assignment. + InitialConstruct() = default; + InitialConstruct(InitialConstruct const& other) = default; + InitialConstruct& operator=(InitialConstruct const& other)= default; +#ifndef WINDOWS + InitialConstruct(InitialConstruct&& other) = default; + InitialConstruct& operator=(InitialConstruct&& other) = default; +#endif + + /*! + * Retrieves the expression characterizing the initial states. + * + * @return The expression characterizing the initial states. + */ + storm::expressions::Expression getInitialStatesExpression() const; + + /*! + * Substitutes all identifiers in the constant according to the given map. + * + * @param substitution The substitution to perform. + * @return The resulting initial construct. + */ + InitialConstruct substitute(std::map const& substitution) const; + + friend std::ostream& operator<<(std::ostream& stream, InitialConstruct const& initialConstruct); + + private: + // An expression characterizing the initial states. + storm::expressions::Expression initialStatesExpression; + }; + } +} + +#endif /* STORM_STORAGE_PRISM_INITIALCONSTRUCT_H_ */ \ No newline at end of file diff --git a/src/storage/prism/Label.cpp b/src/storage/prism/Label.cpp index cb8a13f25..d11091cf0 100644 --- a/src/storage/prism/Label.cpp +++ b/src/storage/prism/Label.cpp @@ -22,5 +22,5 @@ namespace storm { stream << "label \"" << label.getName() << "\" = " << label.getStatePredicateExpression() << ";"; return stream; } - } -} \ No newline at end of file + } // namespace prism +} // namespace storm \ No newline at end of file diff --git a/src/storage/prism/LocatedInformation.cpp b/src/storage/prism/LocatedInformation.cpp index a5a493319..a3862d57a 100644 --- a/src/storage/prism/LocatedInformation.cpp +++ b/src/storage/prism/LocatedInformation.cpp @@ -21,5 +21,5 @@ namespace storm { void LocatedInformation::setLineNumber(uint_fast64_t lineNumber) { this->lineNumber = lineNumber; } - } -} \ No newline at end of file + } // namespace prism +} // namespace storm \ No newline at end of file diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index d7b3fb572..6f4becb0a 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -182,7 +182,6 @@ namespace storm { stream << "endmodule" << std::endl; return stream; } - - } // namespace ir + } // namespace prism } // namespace storm diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 5e024cd53..c29001b16 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -6,13 +6,41 @@ #include "exceptions/InvalidArgumentException.h" #include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/WrongFormatException.h" +#include "src/exceptions/InvalidTypeException.h" namespace storm { namespace prism { - Program::Program(ModelType modelType, std::vector const& constants, std::vector const& globalBooleanVariables, std::vector const& globalIntegerVariables, std::vector const& formulas, std::vector const& modules, std::vector const& rewardModels, bool hasInitialStatesExpression, storm::expressions::Expression const& initialStatesExpression, std::vector