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

Implemented first run for NonDeterministicTransitionParser 

the first run checks the syntax and calculates
* overall number of nondeterministic choices, i.e. number of rows
* overall number of transitions, i.e. nonzero elements
* maximum node id, i.e. number of columns
tempestpy_adaptions
gereon 12 years ago
parent
82ff9f3891
commit
b8f1ddd5da
2 changed files with 81 additions and 49 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. 128
      src/parser/NonDeterministicSparseTransitionParser.cpp
  2. 2
      src/parser/NonDeterministicSparseTransitionParser.h

128
src/parser/NonDeterministicSparseTransitionParser.cpp
View File

@ -6,9 +6,12 @@
*/
#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 <cstdlib>
#include <cstdio>
#include <cstring>
@ -25,34 +28,33 @@
extern log4cplus::Logger logger;
namespace storm {
namespace parser{
namespace parser {
/*!
* @brief Perform first pass through the file and obtain number of
* non-zero cells and maximum node id.
* @brief Perform first pass through the file and obtain overall number of
* choices, number of non-zero cells and maximum node id.
*
* This method does the first pass through the transition file.
*
* This method does the first pass through the .tra file and computes
* the number of non-zero elements that are not diagonal elements,
* which correspondents to the number of transitions that are not
* self-loops.
* (Diagonal elements are treated in a special way).
* It also calculates the maximum node id and stores it in maxnode.
* It also stores the maximum number of nondeterministic choices for a
* single single node in maxchoices.
* It computes the overall number of nondeterministic choices, i.e. the
* number of rows in the matrix that should be created.
* It also calculates the overall number of non-zero cells, i.e. the number
* of elements the matrix has to hold, and the maximum node id, i.e. the
* number of columns of the matrix.
*
* @return The number of non-zero elements that are not on the diagonal
* @param buf Data to scan. Is expected to be some char array.
* @param choices Overall number of choices.
* @param maxnode Is set to highest id of all nodes.
* @return The number of non-zero elements.
*/
std::unique_ptr<std::vector<uint_fast64_t>> NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t &maxnode, uint_fast64_t &maxchoice) {
std::unique_ptr<std::vector<uint_fast64_t>> non_zero = std::unique_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>());
uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode) {
/*
* check file header and extract number of transitions
* Check file header and extract number of transitions.
*/
buf = strchr(buf, '\n') + 1; // skip format hint
if (strncmp(buf, "STATES ", 7) != 0) {
LOG4CPLUS_ERROR(logger, "Expected \"STATES\" but got \"" << std::string(buf, 0, 16) << "\".");
return nullptr;
return 0;
}
buf += 7; // skip "STATES "
if (strtol(buf, &buf, 10) == 0) return 0;
@ -62,49 +64,79 @@ std::unique_ptr<std::vector<uint_fast64_t>> NonDeterministicSparseTransitionPars
return 0;
}
buf += 12; // skip "TRANSITIONS "
strtol(buf, &buf, 10);
/*
* Parse number of transitions.
* We will not actually use this value, but we will compare it to the
* number of transitions we count and issue a warning if this parsed
* vlaue is wrong.
*/
uint_fast64_t parsed_nonzero = strtol(buf, &buf, 10);
/*
* check all transitions for non-zero diagonal entrys
* Read all transitions.
*/
uint_fast64_t row, col, ndchoice;
uint_fast64_t source, target;
uint_fast64_t lastsource = 0;
uint_fast64_t nonzero = 0;
double val;
choices = 0;
maxnode = 0;
maxchoice = 0;
while (buf[0] != '\0') {
/*
* read row and column
* Read source node and choice.
* Check if current source node is larger than current maximum node id.
* Increase number of choices.
* Check if we have skipped any source node, i.e. if any node has no
* outgoing transitions. If so, increase nonzero (and
* parsed_nonzero).
*/
row = checked_strtol(buf, &buf);
ndchoice = checked_strtol(buf, &buf);
col = checked_strtol(buf, &buf);
/*
* check if one is larger than the current maximum id
*/
if (row > maxnode) maxnode = row;
if (col > maxnode) maxnode = col;
/*
* check if nondeterministic choice is larger than current maximum
*/
if (ndchoice > maxchoice)
{
maxchoice = ndchoice;
while (non_zero->size() < maxchoice) non_zero->push_back(0);
source = checked_strtol(buf, &buf);
if (source > maxnode) maxnode = source;
choices++;
if (source > lastsource + 1) {
nonzero += source - lastsource - 1;
parsed_nonzero += source - lastsource - 1;
}
buf += strcspn(buf, " \t\n\r"); // Skip name of choice.
/*
* read value.
* if row == col, we have a diagonal element which is treated separately and this non_zero must be decreased.
* Read all targets for this choice.
*/
val = checked_strtod(buf, &buf);
if ((val < 0.0) || (val > 1.0)) {
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
return 0;
}
if (row != col) (*non_zero)[ndchoice-1]++;
buf = trimWhitespaces(buf);
while (buf[0] == '*') {
buf++;
/*
* Read target node and transition value.
* Check if current target node is larger than current maximum node id.
* Check if the transition value is a valid probability.
*/
target = checked_strtol(buf, &buf);
if (target > maxnode) maxnode = target;
val = checked_strtod(buf, &buf);
if ((val < 0.0) || (val > 1.0)) {
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
return 0;
}
/*
* Increase number of non-zero values.
*/
nonzero++;
/*
* Proceed to beginning of next line.
*/
buf = trimWhitespaces(buf);
}
}
return non_zero;
/*
* Check if the number of transitions given in the file is correct.
*/
if (nonzero != parsed_nonzero) {
LOG4CPLUS_WARN(logger, "File states to have " << parsed_nonzero << " transitions, but I counted " << nonzero << ". Maybe want to fix your file?");
}
return nonzero;
}
@ -135,12 +167,12 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
* perform first pass, i.e. count entries that are not zero and not on the diagonal
*/
uint_fast64_t maxnode, maxchoices;
std::unique_ptr<std::vector<uint_fast64_t>> non_zero = this->firstPass(file.data, maxnode, maxchoices);
uint_fast64_t non_zero = this->firstPass(file.data, maxnode, maxchoices);
/*
* if first pass returned zero, the file format was wrong
*/
if (non_zero == nullptr)
if (non_zero == 0)
{
LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format.");
throw storm::exceptions::WrongFileFormatException();

2
src/parser/NonDeterministicSparseTransitionParser.h
View File

@ -27,7 +27,7 @@ class NonDeterministicSparseTransitionParser : public Parser {
private:
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix;
std::unique_ptr<std::vector<uint_fast64_t>> firstPass(char* buf, uint_fast64_t &maxnode, uint_fast64_t &maxchoice);
uint_fast64_t firstPass(char* buf, uint_fast64_t& choices, uint_fast64_t& maxnode);
};

Write Preview
Loading…
Cancel
Save