From 77a031aaeb0972187c38808194b02d7e00204768 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 3 Mar 2018 10:46:51 +0100 Subject: [PATCH] changed encoding of spirit parser, fixed an issue in variable information related to how many bits are necessary to store the state, changed some output formatting --- src/storm-pgcl/parser/PgclParser.cpp | 2 +- src/storm/generator/VariableInformation.cpp | 2 +- src/storm/parser/ExpressionParser.cpp | 2 +- src/storm/parser/FormulaParser.cpp | 2 +- src/storm/parser/FormulaParserGrammar.cpp | 2 +- src/storm/parser/ImcaMarkovAutomatonParser.cpp | 2 +- src/storm/parser/PrismParser.cpp | 11 +++++++---- src/storm/parser/SpiritParserDefinitions.h | 7 ++++++- src/storm/solver/TopologicalLinearEquationSolver.cpp | 4 ++-- src/storm/storage/BitVectorHashMap.cpp | 2 ++ 10 files changed, 23 insertions(+), 13 deletions(-) diff --git a/src/storm-pgcl/parser/PgclParser.cpp b/src/storm-pgcl/parser/PgclParser.cpp index 6ecde3054..2afe737be 100755 --- a/src/storm-pgcl/parser/PgclParser.cpp +++ b/src/storm-pgcl/parser/PgclParser.cpp @@ -40,7 +40,7 @@ namespace storm { storm::parser::PgclParser grammar(filename, first); try { // Start the parsing run. - bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); + bool succeeded = qi::phrase_parse(iter, last, grammar, storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing of PGCL program failed."); STORM_LOG_DEBUG("Parse of PGCL program finished."); } catch(qi::expectation_failure const& e) { diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index e691300c6..26bd2ecf8 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -114,7 +114,7 @@ namespace storm { uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const { uint_fast64_t result = totalBitOffset; - if (roundTo64Bit) { + if (roundTo64Bit & ((result & ((1ull << 6) - 1)) != 0)) { result = ((result >> 6) + 1) << 6; } return result; diff --git a/src/storm/parser/ExpressionParser.cpp b/src/storm/parser/ExpressionParser.cpp index f78e47d13..492fb337d 100644 --- a/src/storm/parser/ExpressionParser.cpp +++ b/src/storm/parser/ExpressionParser.cpp @@ -196,7 +196,7 @@ namespace storm { try { // Start parsing. - bool succeeded = qi::phrase_parse(iter, last, *this, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); + bool succeeded = qi::phrase_parse(iter, last, *this, storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse expression '" << expressionString << "'."); STORM_LOG_DEBUG("Parsed expression successfully."); } catch (qi::expectation_failure const& e) { diff --git a/src/storm/parser/FormulaParser.cpp b/src/storm/parser/FormulaParser.cpp index e592f141c..d9d7cd518 100644 --- a/src/storm/parser/FormulaParser.cpp +++ b/src/storm/parser/FormulaParser.cpp @@ -97,7 +97,7 @@ namespace storm { // Create grammar. try { // Start parsing. - bool succeeded = qi::phrase_parse(iter, last, *grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); + bool succeeded = qi::phrase_parse(iter, last, *grammar, storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse formula."); STORM_LOG_DEBUG("Parsed formula successfully."); } catch (qi::expectation_failure const& e) { diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 9e8191ad2..2cd8773c9 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -147,7 +147,7 @@ namespace storm { start = (qi::eps >> filterProperty[phoenix::push_back(qi::_val, qi::_1)] | qi::eps(phoenix::bind(&FormulaParserGrammar::areConstantDefinitionsAllowed, phoenix::ref(*this))) >> constantDefinition | qi::eps) - % +(qi::char_("\n;")) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; + % +(qi::char_("\n;")) >> qi::skip(storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; start.name("start"); // Enable the following lines to print debug output for most the rules. diff --git a/src/storm/parser/ImcaMarkovAutomatonParser.cpp b/src/storm/parser/ImcaMarkovAutomatonParser.cpp index 01cb93671..f55d09219 100644 --- a/src/storm/parser/ImcaMarkovAutomatonParser.cpp +++ b/src/storm/parser/ImcaMarkovAutomatonParser.cpp @@ -248,7 +248,7 @@ namespace storm { try { // Start parsing. ImcaParserGrammar grammar; - bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), components); + bool succeeded = qi::phrase_parse(iter, last, grammar, storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), components); STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Could not parse imca file."); STORM_LOG_DEBUG("Parsed imca file successfully."); } catch (qi::expectation_failure const& e) { diff --git a/src/storm/parser/PrismParser.cpp b/src/storm/parser/PrismParser.cpp index 18f42d39c..e54e02b18 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm/parser/PrismParser.cpp @@ -37,11 +37,13 @@ namespace storm { } storm::prism::Program PrismParser::parseFromString(std::string const& input, std::string const& filename, bool prismCompatibility) { - PositionIteratorType first(input.begin()); + bool hasByteOrderMark = input.size() >= 3 && input[0] == '\xEF' && input[1] == '\xBB' && input[2] == '\xBF'; + + PositionIteratorType first(hasByteOrderMark ? input.begin() + 3 : input.begin()); PositionIteratorType iter = first; PositionIteratorType last(input.end()); STORM_LOG_ASSERT(first != last, "Illegal input to PRISM parser."); - + // Create empty result; storm::prism::Program result; @@ -49,7 +51,8 @@ namespace storm { storm::parser::PrismParser grammar(filename, first, prismCompatibility); try { // Start first run. - bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); + storm::spirit_encoding::space_type space; + bool succeeded = qi::phrase_parse(iter, last, grammar, space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); STORM_LOG_THROW(succeeded, storm::exceptions::WrongFormatException, "Parsing failed in first pass."); STORM_LOG_DEBUG("First pass of parsing PRISM input finished."); @@ -58,7 +61,7 @@ namespace storm { 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::eoi)) >> (qi::eol | qi::eoi), result); + succeeded = qi::phrase_parse(iter, last, grammar, space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi), result); STORM_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. diff --git a/src/storm/parser/SpiritParserDefinitions.h b/src/storm/parser/SpiritParserDefinitions.h index 412a6bc37..d48d7a7a6 100644 --- a/src/storm/parser/SpiritParserDefinitions.h +++ b/src/storm/parser/SpiritParserDefinitions.h @@ -6,6 +6,7 @@ // Include boost spirit. #define BOOST_SPIRIT_USE_PHOENIX_V3 +#define BOOST_SPIRIT_UNICODE #include #include #include @@ -21,6 +22,10 @@ typedef std::string::const_iterator BaseIteratorType; typedef boost::spirit::line_pos_iterator PositionIteratorType; typedef PositionIteratorType Iterator; -typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi)) Skipper; +namespace storm { + namespace spirit_encoding = boost::spirit::unicode; +} + +typedef BOOST_TYPEOF(storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)) >> (qi::eol | qi::eoi)) Skipper; #endif /* STORM_PARSER_SPIRITPARSERDEFINITIONS_H_ */ diff --git a/src/storm/solver/TopologicalLinearEquationSolver.cpp b/src/storm/solver/TopologicalLinearEquationSolver.cpp index bd5313381..7568f3c65 100644 --- a/src/storm/solver/TopologicalLinearEquationSolver.cpp +++ b/src/storm/solver/TopologicalLinearEquationSolver.cpp @@ -68,9 +68,9 @@ namespace storm { storm::Environment sccSolverEnvironment = getEnvironmentForUnderlyingSolver(env, needAdaptPrecision); - std::cout << "Found " << this->sortedSccDecomposition->size() << "SCCs. Average size is " << static_cast(this->getMatrixRowCount()) / static_cast(this->sortedSccDecomposition->size()) << "." << std::endl; + STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << "SCCs. Average size is " << static_cast(this->getMatrixRowCount()) / static_cast(this->sortedSccDecomposition->size()) << "."); if (this->longestSccChainSize) { - std::cout << "Longest SCC chain size is " << this->longestSccChainSize.get() << std::endl; + STORM_LOG_INFO("Longest SCC chain size is " << this->longestSccChainSize.get() << "."); } // Handle the case where there is just one large SCC diff --git a/src/storm/storage/BitVectorHashMap.cpp b/src/storm/storage/BitVectorHashMap.cpp index 7bfe1595e..67c151bde 100644 --- a/src/storm/storage/BitVectorHashMap.cpp +++ b/src/storm/storage/BitVectorHashMap.cpp @@ -96,10 +96,12 @@ namespace storm { std::swap(oldValues, values); // Now iterate through the elements and reinsert them in the new storage. + uint64_t oldSize = numberOfElements; numberOfElements = 0; for (auto bucketIndex : oldOccupied) { findOrAddAndGetBucket(oldBuckets.get(bucketIndex * bucketSize, bucketSize), oldValues[bucketIndex]); } + STORM_LOG_ASSERT(oldSize == numberOfElements, "Size mismatch in rehashing. Size before was " << oldSize << " and new size is " << numberOfElements << "."); } template