|
@ -7,22 +7,24 @@ |
|
|
|
|
|
|
|
|
#include "src/parser/NonDeterministicSparseTransitionParser.h"
|
|
|
#include "src/parser/NonDeterministicSparseTransitionParser.h"
|
|
|
|
|
|
|
|
|
#include "src/utility/Settings.h"
|
|
|
|
|
|
#include "src/exceptions/FileIoException.h"
|
|
|
|
|
|
#include "src/exceptions/WrongFileFormatException.h"
|
|
|
|
|
|
#include "boost/integer/integer_mask.hpp"
|
|
|
|
|
|
|
|
|
#include <errno.h>
|
|
|
|
|
|
#include <time.h>
|
|
|
|
|
|
#include <sys/stat.h>
|
|
|
|
|
|
#include <fcntl.h>
|
|
|
|
|
|
#include <locale.h>
|
|
|
|
|
|
|
|
|
#include <cstdlib>
|
|
|
#include <cstdlib>
|
|
|
#include <cstdio>
|
|
|
#include <cstdio>
|
|
|
#include <cstring>
|
|
|
#include <cstring>
|
|
|
#include <clocale>
|
|
|
#include <clocale>
|
|
|
#include <iostream>
|
|
|
#include <iostream>
|
|
|
#include <errno.h>
|
|
|
|
|
|
#include <time.h>
|
|
|
|
|
|
#include <sys/stat.h>
|
|
|
|
|
|
#include <fcntl.h>
|
|
|
|
|
|
#include <locale.h>
|
|
|
|
|
|
|
|
|
#include <utility>
|
|
|
|
|
|
#include <string>
|
|
|
|
|
|
|
|
|
|
|
|
#include "src/utility/Settings.h"
|
|
|
|
|
|
#include "src/exceptions/FileIoException.h"
|
|
|
|
|
|
#include "src/exceptions/WrongFileFormatException.h"
|
|
|
|
|
|
#include "boost/integer/integer_mask.hpp"
|
|
|
#include "log4cplus/logger.h"
|
|
|
#include "log4cplus/logger.h"
|
|
|
#include "log4cplus/loggingmacros.h"
|
|
|
#include "log4cplus/loggingmacros.h"
|
|
|
extern log4cplus::Logger logger; |
|
|
extern log4cplus::Logger logger; |
|
@ -56,14 +58,14 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_ |
|
|
LOG4CPLUS_ERROR(logger, "Expected \"STATES\" but got \"" << std::string(buf, 0, 16) << "\"."); |
|
|
LOG4CPLUS_ERROR(logger, "Expected \"STATES\" but got \"" << std::string(buf, 0, 16) << "\"."); |
|
|
return 0; |
|
|
return 0; |
|
|
} |
|
|
} |
|
|
buf += 7; // skip "STATES "
|
|
|
|
|
|
|
|
|
buf += 7; // skip "STATES "
|
|
|
if (strtol(buf, &buf, 10) == 0) return 0; |
|
|
if (strtol(buf, &buf, 10) == 0) return 0; |
|
|
buf = trimWhitespaces(buf); |
|
|
buf = trimWhitespaces(buf); |
|
|
if (strncmp(buf, "TRANSITIONS ", 12) != 0) { |
|
|
if (strncmp(buf, "TRANSITIONS ", 12) != 0) { |
|
|
LOG4CPLUS_ERROR(logger, "Expected \"TRANSITIONS\" but got \"" << std::string(buf, 0, 16) << "\"."); |
|
|
LOG4CPLUS_ERROR(logger, "Expected \"TRANSITIONS\" but got \"" << std::string(buf, 0, 16) << "\"."); |
|
|
return 0; |
|
|
return 0; |
|
|
} |
|
|
} |
|
|
buf += 12; // skip "TRANSITIONS "
|
|
|
|
|
|
|
|
|
buf += 12; // skip "TRANSITIONS "
|
|
|
/*
|
|
|
/*
|
|
|
* Parse number of transitions. |
|
|
* Parse number of transitions. |
|
|
* We will not actually use this value, but we will compare it to the |
|
|
* We will not actually use this value, but we will compare it to the |
|
@ -98,7 +100,7 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_ |
|
|
parsed_nonzero += source - lastsource - 1; |
|
|
parsed_nonzero += source - lastsource - 1; |
|
|
} |
|
|
} |
|
|
lastsource = source; |
|
|
lastsource = source; |
|
|
buf = trimWhitespaces(buf); // Skip to name of choice
|
|
|
|
|
|
|
|
|
buf = trimWhitespaces(buf); // Skip to name of choice
|
|
|
buf += strcspn(buf, " \t\n\r"); // Skip name of choice.
|
|
|
buf += strcspn(buf, " \t\n\r"); // Skip name of choice.
|
|
|
|
|
|
|
|
|
/*
|
|
|
/*
|
|
@ -152,12 +154,11 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_ |
|
|
*/ |
|
|
*/ |
|
|
|
|
|
|
|
|
NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(std::string const &filename) |
|
|
NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(std::string const &filename) |
|
|
: matrix(nullptr) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
: matrix(nullptr) { |
|
|
/*
|
|
|
/*
|
|
|
* Enforce locale where decimal point is '.'. |
|
|
|
|
|
*/ |
|
|
|
|
|
setlocale( LC_NUMERIC, "C" ); |
|
|
|
|
|
|
|
|
* Enforce locale where decimal point is '.'. |
|
|
|
|
|
*/ |
|
|
|
|
|
setlocale(LC_NUMERIC, "C"); |
|
|
|
|
|
|
|
|
/*
|
|
|
/*
|
|
|
* Open file. |
|
|
* Open file. |
|
@ -174,8 +175,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s |
|
|
/*
|
|
|
/*
|
|
|
* If first pass returned zero, the file format was wrong. |
|
|
* If first pass returned zero, the file format was wrong. |
|
|
*/ |
|
|
*/ |
|
|
if (nonzero == 0) |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
if (nonzero == 0) { |
|
|
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format."); |
|
|
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format."); |
|
|
throw storm::exceptions::WrongFileFormatException(); |
|
|
throw storm::exceptions::WrongFileFormatException(); |
|
|
} |
|
|
} |
|
@ -227,13 +227,12 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s |
|
|
/*
|
|
|
/*
|
|
|
* Read all transitions from file. |
|
|
* Read all transitions from file. |
|
|
*/ |
|
|
*/ |
|
|
while (buf[0] != '\0') |
|
|
|
|
|
{ |
|
|
|
|
|
|
|
|
while (buf[0] != '\0') { |
|
|
/*
|
|
|
/*
|
|
|
* Read source node and choice name. |
|
|
* Read source node and choice name. |
|
|
*/ |
|
|
|
|
|
|
|
|
*/ |
|
|
source = checked_strtol(buf, &buf); |
|
|
source = checked_strtol(buf, &buf); |
|
|
buf = trimWhitespaces(buf); // Skip to name of choice
|
|
|
|
|
|
|
|
|
buf = trimWhitespaces(buf); // Skip to name of choice
|
|
|
choice = std::string(buf, strcspn(buf, " \t\n\r")); |
|
|
choice = std::string(buf, strcspn(buf, " \t\n\r")); |
|
|
|
|
|
|
|
|
/*
|
|
|
/*
|
|
@ -244,7 +243,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s |
|
|
for (uint_fast64_t node = lastsource + 1; node < source; node++) { |
|
|
for (uint_fast64_t node = lastsource + 1; node < source; node++) { |
|
|
hadDeadlocks = true; |
|
|
hadDeadlocks = true; |
|
|
if (fixDeadlocks) { |
|
|
if (fixDeadlocks) { |
|
|
this->rowMapping->insert( RowMapping::value_type( curRow, std::pair<uint_fast64_t,std::string>(node, "")) ); |
|
|
|
|
|
|
|
|
this->rowMapping->insert(RowMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(node, ""))); |
|
|
this->matrix->addNextValue(curRow, node, 1); |
|
|
this->matrix->addNextValue(curRow, node, 1); |
|
|
curRow++; |
|
|
curRow++; |
|
|
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); |
|
|
LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted."); |
|
@ -257,7 +256,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s |
|
|
/*
|
|
|
/*
|
|
|
* Add this source-choice pair to rowMapping. |
|
|
* Add this source-choice pair to rowMapping. |
|
|
*/ |
|
|
*/ |
|
|
this->rowMapping->insert( RowMapping::value_type( curRow, std::pair<uint_fast64_t,std::string>(source, choice)) ); |
|
|
|
|
|
|
|
|
this->rowMapping->insert(RowMapping::value_type(curRow, std::pair<uint_fast64_t, std::string>(source, choice))); |
|
|
|
|
|
|
|
|
/*
|
|
|
/*
|
|
|
* Skip name of choice. |
|
|
* Skip name of choice. |
|
@ -294,5 +293,5 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s |
|
|
this->matrix->finalize(); |
|
|
this->matrix->finalize(); |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
} //namespace parser
|
|
|
|
|
|
} //namespace storm
|
|
|
|
|
|
|
|
|
} // namespace parser
|
|
|
|
|
|
} // namespace storm
|