Browse Source

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

tempestpy_adaptions
dehnert 7 years ago
parent
commit
77a031aaeb
  1. 2
      src/storm-pgcl/parser/PgclParser.cpp
  2. 2
      src/storm/generator/VariableInformation.cpp
  3. 2
      src/storm/parser/ExpressionParser.cpp
  4. 2
      src/storm/parser/FormulaParser.cpp
  5. 2
      src/storm/parser/FormulaParserGrammar.cpp
  6. 2
      src/storm/parser/ImcaMarkovAutomatonParser.cpp
  7. 11
      src/storm/parser/PrismParser.cpp
  8. 7
      src/storm/parser/SpiritParserDefinitions.h
  9. 4
      src/storm/solver/TopologicalLinearEquationSolver.cpp
  10. 2
      src/storm/storage/BitVectorHashMap.cpp

2
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<PositionIteratorType> const& e) {

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

2
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<PositionIteratorType> const& e) {

2
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<PositionIteratorType> const& e) {

2
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.

2
src/storm/parser/ImcaMarkovAutomatonParser.cpp

@ -248,7 +248,7 @@ namespace storm {
try {
// Start parsing.
ImcaParserGrammar<ValueType> 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<PositionIteratorType> const& e) {

11
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<PositionIteratorType> const& e) {
// If the parser expected content different than the one provided, display information about the location of the error.

7
src/storm/parser/SpiritParserDefinitions.h

@ -6,6 +6,7 @@
// Include boost spirit.
#define BOOST_SPIRIT_USE_PHOENIX_V3
#define BOOST_SPIRIT_UNICODE
#include <boost/typeof/typeof.hpp>
#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix.hpp>
@ -21,6 +22,10 @@ typedef std::string::const_iterator BaseIteratorType;
typedef boost::spirit::line_pos_iterator<BaseIteratorType> 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_ */

4
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<double>(this->getMatrixRowCount()) / static_cast<double>(this->sortedSccDecomposition->size()) << "." << std::endl;
STORM_LOG_INFO("Found " << this->sortedSccDecomposition->size() << "SCCs. Average size is " << static_cast<double>(this->getMatrixRowCount()) / static_cast<double>(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

2
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<class ValueType, class Hash>

Loading…
Cancel
Save