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

Big bunch of fixes, including memory leaks, bad code pathes, insufficent error reporting, uninitialized variables, etc, etc. 

Edited sparse/static_sparse_matrix.h, added an internal state enum to represent errors and the like.
tempestpy_adaptions
PBerger 13 years ago
parent
c10a0ee734
commit
1643901c5a
5 changed files with 299 additions and 221 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 34
      src/parser/read_lab_file.cpp
  2. 138
      src/parser/read_tra_file.cpp
  3. 174
      src/sparse/static_sparse_matrix.h
  4. 116
      test/parser/read_lab_file_test.cpp
  5. 58
      test/parser/read_tra_file_test.cpp

34
src/parser/read_lab_file.cpp
View File

@ -53,7 +53,7 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
FILE *P; FILE *P;
//TODO (Thomas Heinemann): handle files with lines that are longer than BUFFER_SIZE //TODO (Thomas Heinemann): handle files with lines that are longer than BUFFER_SIZE
//TODO (Thomas Heinemann): Throw errors if fgets return NULL in the declaration.
//TODO (Thomas Heinemann): Throw errors if fgets return NULL in the declaration. (fixed by Philipp. Or?)
char s[BUFFER_SIZE]; //String buffer char s[BUFFER_SIZE]; //String buffer
char *saveptr = NULL; //Buffer for strtok_r char *saveptr = NULL; //Buffer for strtok_r
@ -64,14 +64,14 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
if (P == NULL) { if (P == NULL) {
pantheios::log_ERROR("File could not be opened."); pantheios::log_ERROR("File could not be opened.");
throw mrmc::exceptions::file_IO_exception(); throw mrmc::exceptions::file_IO_exception();
return NULL;
} }
if (fgets(s, BUFFER_SIZE, P)) {
if (strcmp(s, "#DECLARATION\n")) {
fclose(P);
pantheios::log_ERROR("Wrong declaration section (\"#DECLARATION\" missing).");
throw mrmc::exceptions::wrong_file_format();
}
if (!fgets(s, BUFFER_SIZE, P) || strcmp(s, "#DECLARATION\n")) {
fclose(P);
pantheios::log_ERROR("Wrong declaration section (\"#DECLARATION\" missing).");
throw mrmc::exceptions::wrong_file_format();
return NULL;
} }
@ -104,6 +104,8 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
} else { } else {
pantheios::log_ERROR("EOF in the declaration section"); pantheios::log_ERROR("EOF in the declaration section");
throw mrmc::exceptions::wrong_file_format(); throw mrmc::exceptions::wrong_file_format();
delete[] decl_buffer;
return NULL;
} }
} while (need_next_iteration); } while (need_next_iteration);
@ -132,17 +134,18 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
result -> addProposition(proposition); result -> addProposition(proposition);
} }
// Free decl_buffer
delete[] decl_buffer;
saveptr = NULL; //resetting save pointer for strtok_r saveptr = NULL; //resetting save pointer for strtok_r
if (fgets(s, BUFFER_SIZE, P)) {
if (strcmp(s, "#END\n")) {
fclose(P);
delete result;
pantheios::log_ERROR("Wrong declaration section (\"#END\" missing).");
throw mrmc::exceptions::wrong_file_format();
}
if (!fgets(s, BUFFER_SIZE, P) || strcmp(s, "#END\n")) {
fclose(P);
delete result;
pantheios::log_ERROR("Wrong declaration section (\"#END\" missing).");
throw mrmc::exceptions::wrong_file_format();
return NULL;
} }
while (fgets(s, BUFFER_SIZE, P)) { while (fgets(s, BUFFER_SIZE, P)) {
@ -157,6 +160,7 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
delete result; delete result;
pantheios::log_ERROR("Line assigning propositions does not start with a node number."); pantheios::log_ERROR("Line assigning propositions does not start with a node number.");
throw mrmc::exceptions::wrong_file_format(); throw mrmc::exceptions::wrong_file_format();
return NULL;
} }
do { do {
token = STRTOK_FUNC(NULL, sep, &saveptr); token = STRTOK_FUNC(NULL, sep, &saveptr);
@ -169,9 +173,7 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
} }
fclose(P); fclose(P);
return result; return result;
} }
} //namespace parser } //namespace parser

138
src/parser/read_tra_file.cpp
View File

@ -93,79 +93,79 @@ static uint_fast32_t make_first_pass(FILE* p) {
*/ */
sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) { sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
FILE *p = NULL;
char s[BUFFER_SIZE];
uint_fast32_t rows, non_zero;
sparse::StaticSparseMatrix<double> *sp = NULL;
p = fopen(filename, "r");
if(p==NULL) {
pantheios::log_ERROR("File ", filename, " was not readable (Does it exist?)");
throw exceptions::file_IO_exception("mrmc::read_tra_file: Error opening file! (Does it exist?)");
}
non_zero = make_first_pass(p);
//Set file reader back to the beginning
rewind(p);
//Reading No. of states
if (fgets(s, BUFFER_SIZE, p) != NULL) {
if (sscanf( s, "STATES %d", &rows) == 0) {
pantheios::log_WARNING(pantheios::integer(rows));
(void)fclose(p);
throw mrmc::exceptions::wrong_file_format();
}
}
/* Reading No. of transitions
* Note that the result is not used in this function as make_first_pass()
* computes the relevant number (non_zero)
*/
if (fgets(s, BUFFER_SIZE, p) != NULL) {
uint_fast32_t nnz=0;
if (sscanf( s, "TRANSITIONS %d", &nnz) == 0) {
(void)fclose(p);
throw mrmc::exceptions::wrong_file_format();
}
}
FILE *p = NULL;
char s[BUFFER_SIZE];
uint_fast32_t rows, non_zero;
sparse::StaticSparseMatrix<double> *sp = NULL;
p = fopen(filename, "r");
if(p == NULL) {
pantheios::log_ERROR("File ", filename, " was not readable (Does it exist?)");
throw exceptions::file_IO_exception("mrmc::read_tra_file: Error opening file! (Does it exist?)");
return NULL;
}
non_zero = make_first_pass(p);
//Set file reader back to the beginning
rewind(p);
//Reading No. of states
if ((fgets(s, BUFFER_SIZE, p) == NULL) || (sscanf(s, "STATES %d", &rows) == 0)) {
pantheios::log_WARNING(pantheios::integer(rows));
(void)fclose(p);
throw mrmc::exceptions::wrong_file_format();
return NULL;
}
/* Reading No. of transitions
* Note that the result is not used in this function as make_first_pass()
* computes the relevant number (non_zero)
*/
uint_fast32_t nnz=0;
if ((fgets(s, BUFFER_SIZE, p) == NULL) || (sscanf(s, "TRANSITIONS %d", &nnz) == 0)) {
(void)fclose(p);
throw mrmc::exceptions::wrong_file_format();
return NULL;
}
pantheios::log_DEBUG("Creating matrix with ", pantheios::log_DEBUG("Creating matrix with ",
pantheios::integer(rows), " rows and ", pantheios::integer(rows), " rows and ",
pantheios::integer(non_zero), " Non-Zero-Elements"); pantheios::integer(non_zero), " Non-Zero-Elements");
/* Creating matrix
* Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
* non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
*/
sp = new sparse::StaticSparseMatrix<double>(rows,non_zero);
sp->initialize();
if ( NULL == sp ) {
throw std::bad_alloc();
return NULL;
}
//Reading transitions (one per line) and saving the results in the matrix
while (NULL != fgets( s, BUFFER_SIZE, p ))
{
uint_fast32_t row=0, col=0;
double val = 0.0;
if (sscanf( s, "%d%d%lf", &row, &col, &val) != 3) {
delete sp;
(void)fclose(p);
throw mrmc::exceptions::wrong_file_format();
}
pantheios::log_DEBUG("Write value ",
pantheios::real(val),
" to position ",
pantheios::integer(row), " x ",
pantheios::integer(col));
sp->addNextValue(row,col,val);
}
(void)fclose(p);
pantheios::log_DEBUG("Finalizing Matrix");
sp->finalize();
return sp;
/* Creating matrix
* Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
* non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
*/
sp = new sparse::StaticSparseMatrix<double>(rows,non_zero);
if ( NULL == sp ) {
throw std::bad_alloc();
return NULL;
}
sp->initialize();
//Reading transitions (one per line) and saving the results in the matrix
while (NULL != fgets(s, BUFFER_SIZE, p )) {
uint_fast32_t row=0, col=0;
double val = 0.0;
if (sscanf(s, "%d%d%lf", &row, &col, &val) != 3) {
(void)fclose(p);
throw mrmc::exceptions::wrong_file_format();
// Delete Matrix to free allocated memory
delete sp;
return NULL;
}
pantheios::log_DEBUG("Write value ",
pantheios::real(val),
" to position ",
pantheios::integer(row), " x ",
pantheios::integer(col));
sp->addNextValue(row,col,val);
}
(void)fclose(p);
pantheios::log_DEBUG("Finalizing Matrix");
sp->finalize();
return sp;
} }
} //namespace parser } //namespace parser

174
src/sparse/static_sparse_matrix.h
View File

@ -26,13 +26,31 @@ namespace sparse {
template <class T> template <class T>
class StaticSparseMatrix { class StaticSparseMatrix {
public: public:
//! Status enum
/*!
An Enum representing the internal state of the Matrix.
After creating the Matrix using the Constructor, the Object is in state UnInitialized. After calling initialize(), that state changes to Initialized and after all entries have been entered and finalize() has been called, to ReadReady.
Should a critical error occur in any of the former functions, the state will change to Error.
@see getState()
@see isReadReady()
@see isInitialized()
@see hasError()
*/
enum MatrixStatus {
Error = -1,
UnInitialized = 0,
Initialized = 1,
ReadReady = 2,
};
//! Constructor //! Constructor
/*! /*!
\param rows Row-Count and therefore column-count of the symmetric matrix \param rows Row-Count and therefore column-count of the symmetric matrix
\param non_zero_entries The exact count of entries that will be submitted through addNextValue *excluding* those on the diagonal (A_{i,j} with i = j) \param non_zero_entries The exact count of entries that will be submitted through addNextValue *excluding* those on the diagonal (A_{i,j} with i = j)
*/ */
StaticSparseMatrix(uint_fast32_t rows, uint_fast32_t non_zero_entries) { StaticSparseMatrix(uint_fast32_t rows, uint_fast32_t non_zero_entries) {
setState(MatrixStatus::UnInitialized);
current_size = 0; current_size = 0;
storage_size = 0; storage_size = 0;
@ -48,6 +66,7 @@ class StaticSparseMatrix {
} }
~StaticSparseMatrix() { ~StaticSparseMatrix() {
setState(MatrixStatus::UnInitialized);
if (value_storage != NULL) { if (value_storage != NULL) {
//free(value_storage); //free(value_storage);
delete[] value_storage; delete[] value_storage;
@ -68,7 +87,7 @@ class StaticSparseMatrix {
//! Getter for saving matrix entry A_{row,col} to target //! Getter for saving matrix entry A_{row,col} to target
/*! /*!
Getter function for the matrix.
Getter function for the matrix. This function does not check the internal status for errors for performance reasons.
\param row 1-based index of the requested row \param row 1-based index of the requested row
\param col 1-based index of the requested column \param col 1-based index of the requested column
\param target pointer to where the result will be stored \param target pointer to where the result will be stored
@ -109,36 +128,42 @@ class StaticSparseMatrix {
Mandatory initialization of the matrix, must be called before using any other member function. Mandatory initialization of the matrix, must be called before using any other member function.
*/ */
void initialize() { void initialize() {
if (row_count == 0) {
if (internal_status != MatrixStatus::UnInitialized) {
pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing invalid state for status flag != 0 (is ", pantheios::integer(internal_status)," - Already initialized?");
throw mrmc::exceptions::invalid_state("StaticSparseMatrix::initialize: Invalid state for status flag != 0 - Already initialized?");
triggerErrorState();
} else if (row_count == 0) {
pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing invalid_argument for row_count = 0"); pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing invalid_argument for row_count = 0");
throw mrmc::exceptions::invalid_argument("mrmc::StaticSparseMatrix::initialize: Matrix with 0 rows is not reasonable"); throw mrmc::exceptions::invalid_argument("mrmc::StaticSparseMatrix::initialize: Matrix with 0 rows is not reasonable");
}
if (((row_count * row_count) - row_count) < non_zero_entry_count) {
triggerErrorState();
} else if (((row_count * row_count) - row_count) < non_zero_entry_count) {
pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing invalid_argument: More non-zero entries than entries in target matrix"); pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing invalid_argument: More non-zero entries than entries in target matrix");
throw mrmc::exceptions::invalid_argument("mrmc::StaticSparseMatrix::initialize: More non-zero entries than entries in target matrix"); throw mrmc::exceptions::invalid_argument("mrmc::StaticSparseMatrix::initialize: More non-zero entries than entries in target matrix");
}
storage_size = non_zero_entry_count;
last_row = 0;
triggerErrorState();
} else {
storage_size = non_zero_entry_count;
last_row = 0;
//value_storage = static_cast<T*>(calloc(storage_size, sizeof(*value_storage)));
value_storage = new (std::nothrow) T[storage_size]();
//value_storage = static_cast<T*>(calloc(storage_size, sizeof(*value_storage)));
value_storage = new (std::nothrow) T[storage_size]();
//column_indications = static_cast<uint_fast32_t*>(calloc(storage_size, sizeof(*column_indications)));
column_indications = new (std::nothrow) uint_fast32_t[storage_size]();
//column_indications = static_cast<uint_fast32_t*>(calloc(storage_size, sizeof(*column_indications)));
column_indications = new (std::nothrow) uint_fast32_t[storage_size]();
//row_indications = static_cast<uint_fast32_t*>(calloc(row_count + 1, sizeof(*row_indications)));
row_indications = new (std::nothrow) uint_fast32_t[row_count + 1]();
//row_indications = static_cast<uint_fast32_t*>(calloc(row_count + 1, sizeof(*row_indications)));
row_indications = new (std::nothrow) uint_fast32_t[row_count + 1]();
// row_count + 1 so that access with 1-based indices can be direct without the overhead of a -1 each time
//diagonal_storage = static_cast<T*>(calloc(row_count + 1, sizeof(*diagonal_storage)));
diagonal_storage = new (std::nothrow) T[row_count + 1]();
// row_count + 1 so that access with 1-based indices can be direct without the overhead of a -1 each time
//diagonal_storage = static_cast<T*>(calloc(row_count + 1, sizeof(*diagonal_storage)));
diagonal_storage = new (std::nothrow) T[row_count + 1]();
if ((value_storage == NULL) || (column_indications == NULL) || (row_indications == NULL) || (diagonal_storage == NULL)) {
pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing bad_alloc: memory allocation failed");
throw std::bad_alloc();
if ((value_storage == NULL) || (column_indications == NULL) || (row_indications == NULL) || (diagonal_storage == NULL)) {
pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing bad_alloc: memory allocation failed");
throw std::bad_alloc();
triggerErrorState();
} else {
setState(MatrixStatus::Initialized);
}
} }
} }
@ -151,6 +176,7 @@ class StaticSparseMatrix {
if ((row > row_count) || (col > row_count) || (row == 0) || (col == 0)) { if ((row > row_count) || (col > row_count) || (row == 0) || (col == 0)) {
pantheios::log_ERROR("StaticSparseMatrix::addNextValue: Throwing out_of_range: row or col not in 1 .. rows"); pantheios::log_ERROR("StaticSparseMatrix::addNextValue: Throwing out_of_range: row or col not in 1 .. rows");
throw mrmc::exceptions::out_of_range("mrmc::StaticSparseMatrix::addNextValue: row or col not in 1 .. rows"); throw mrmc::exceptions::out_of_range("mrmc::StaticSparseMatrix::addNextValue: row or col not in 1 .. rows");
triggerErrorState();
} }
if (row == col) { if (row == col) {
@ -172,18 +198,25 @@ class StaticSparseMatrix {
} }
void finalize() { void finalize() {
if (storage_size != current_size) {
if (!isInitialized()) {
pantheios::log_ERROR("StaticSparseMatrix::finalize: Throwing invalid state for internal state not Initialized (is ", pantheios::integer(internal_status)," - Already finalized?");
throw mrmc::exceptions::invalid_state("StaticSparseMatrix::finalize: Invalid state for internal state not Initialized - Already finalized?");
triggerErrorState();
} else if (storage_size != current_size) {
pantheios::log_ERROR("StaticSparseMatrix::finalize: Throwing invalid_state: Wrong call count for addNextValue"); pantheios::log_ERROR("StaticSparseMatrix::finalize: Throwing invalid_state: Wrong call count for addNextValue");
throw mrmc::exceptions::invalid_state("mrmc::StaticSparseMatrix::finalize: Wrong call count for addNextValue"); throw mrmc::exceptions::invalid_state("mrmc::StaticSparseMatrix::finalize: Wrong call count for addNextValue");
}
if (last_row != row_count) {
for (uint_fast32_t i = last_row; i < row_count; ++i) {
row_indications[i] = current_size;
triggerErrorState();
} else {
if (last_row != row_count) {
for (uint_fast32_t i = last_row; i < row_count; ++i) {
row_indications[i] = current_size;
}
} }
}
row_indications[row_count] = storage_size;
row_indications[row_count] = storage_size;
setState(MatrixStatus::ReadReady);
}
} }
uint_fast32_t getRowCount() const { uint_fast32_t getRowCount() const {
@ -194,29 +227,52 @@ class StaticSparseMatrix {
return value_storage; return value_storage;
} }
Eigen::SparseMatrix<T> toEigenSparseMatrix() {
typedef Eigen::Triplet<double> ETd;
std::vector<ETd> tripletList;
tripletList.reserve(non_zero_entry_count + row_count);
uint_fast32_t row_start;
uint_fast32_t row_end;
for (uint_fast32_t row = 1; row <= row_count; ++row) {
row_start = row_indications[row - 1];
row_end = row_indications[row];
while (row_start < row_end) {
tripletList.push_back(ETd(row - 1, column_indications[row_start] - 1, value_storage[row_start]));
++row_start;
}
}
for (uint_fast32_t i = 1; i <= row_count; ++i) {
tripletList.push_back(ETd(i, i, diagonal_storage[i]));
}
bool isReadReady() {
return (internal_status == MatrixStatus::ReadReady);
}
bool isInitialized() {
return (internal_status == MatrixStatus::Initialized || internal_status == MatrixStatus::ReadReady);
}
MatrixStatus getState() {
return internal_status;
}
bool hasError() {
return (internal_status == MatrixStatus::Error);
}
Eigen::SparseMatrix<T> toEigenSparseMatrix() {
Eigen::SparseMatrix<T> mat(row_count, row_count); Eigen::SparseMatrix<T> mat(row_count, row_count);
mat.setFromTriplets(tripletList.begin(), tripletList.end());
mat.makeCompressed();
if (!isReadReady()) {
pantheios::log_ERROR("StaticSparseMatrix::toEigenSparseMatrix: Throwing invalid state for internal state not ReadReady (is ", pantheios::integer(internal_status),").");
throw mrmc::exceptions::invalid_state("StaticSparseMatrix::toEigenSparseMatrix: Invalid state for internal state not ReadReady.");
triggerErrorState();
} else {
typedef Eigen::Triplet<double> ETd;
std::vector<ETd> tripletList;
tripletList.reserve(non_zero_entry_count + row_count);
uint_fast32_t row_start;
uint_fast32_t row_end;
for (uint_fast32_t row = 1; row <= row_count; ++row) {
row_start = row_indications[row - 1];
row_end = row_indications[row];
while (row_start < row_end) {
tripletList.push_back(ETd(row - 1, column_indications[row_start] - 1, value_storage[row_start]));
++row_start;
}
}
for (uint_fast32_t i = 1; i <= row_count; ++i) {
tripletList.push_back(ETd(i, i, diagonal_storage[i]));
}
mat.setFromTriplets(tripletList.begin(), tripletList.end());
mat.makeCompressed();
}
return mat; return mat;
} }
@ -237,6 +293,22 @@ class StaticSparseMatrix {
uint_fast32_t* column_indications; uint_fast32_t* column_indications;
/*! Array containing the row boundaries of valueStorage */ /*! Array containing the row boundaries of valueStorage */
uint_fast32_t* row_indications; uint_fast32_t* row_indications;
/*! Internal status enum, 0 for constructed, 1 for initialized and 2 for finalized, -1 on errors */
MatrixStatus internal_status;
/*! Sets the internal status to Error */
void triggerErrorState() {
setState(MatrixStatus::Error);
}
/*!
Sets the internal status to new_state iff the current state is not the Error state.
@param new_state the new state to be switched to
*/
void setState(const MatrixStatus new_state) {
internal_status = (internal_status == MatrixStatus::Error) ? internal_status : new_state;
}
}; };
} // namespace sparse } // namespace sparse

116
test/parser/read_lab_file_test.cpp
View File

@ -18,63 +18,65 @@ TEST(ReadLabFileTest, NonExistingFileTest) {
} }
TEST(ReadLabFileTest, ParseTest) { TEST(ReadLabFileTest, ParseTest) {
//This test is based on a test case from the original MRMC.
mrmc::dtmc::labeling* labeling;
//Parsing the file
ASSERT_NO_THROW(labeling = mrmc::parser::read_lab_file(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
//Checking whether all propositions are in the labelling
char phi[] = "phi", psi[] = "psi", smth[] = "smth";
ASSERT_TRUE(labeling->containsProposition(phi));
ASSERT_TRUE(labeling->containsProposition(psi));
ASSERT_TRUE(labeling->containsProposition(smth));
//Testing whether all and only the correct nodes are labeled with "phi"
ASSERT_TRUE(labeling->nodeHasProposition(phi,1));
ASSERT_TRUE(labeling->nodeHasProposition(phi,2));
ASSERT_TRUE(labeling->nodeHasProposition(phi,3));
ASSERT_TRUE(labeling->nodeHasProposition(phi,5));
ASSERT_TRUE(labeling->nodeHasProposition(phi,7));
ASSERT_TRUE(labeling->nodeHasProposition(phi,9));
ASSERT_TRUE(labeling->nodeHasProposition(phi,10));
ASSERT_TRUE(labeling->nodeHasProposition(phi,11));
ASSERT_FALSE(labeling->nodeHasProposition(phi,4));
ASSERT_FALSE(labeling->nodeHasProposition(phi,6));
//Testing whether all and only the correct nodes are labeled with "psi"
ASSERT_TRUE(labeling->nodeHasProposition(psi,6));
ASSERT_TRUE(labeling->nodeHasProposition(psi,7));
ASSERT_TRUE(labeling->nodeHasProposition(psi,8));
ASSERT_FALSE(labeling->nodeHasProposition(psi,1));
ASSERT_FALSE(labeling->nodeHasProposition(psi,2));
ASSERT_FALSE(labeling->nodeHasProposition(psi,3));
ASSERT_FALSE(labeling->nodeHasProposition(psi,4));
ASSERT_FALSE(labeling->nodeHasProposition(psi,5));
ASSERT_FALSE(labeling->nodeHasProposition(psi,9));
ASSERT_FALSE(labeling->nodeHasProposition(psi,10));
ASSERT_FALSE(labeling->nodeHasProposition(psi,11));
//Testing whether all and only the correct nodes are labeled with "smth"
ASSERT_TRUE(labeling->nodeHasProposition(smth,4));
ASSERT_TRUE(labeling->nodeHasProposition(smth,5));
ASSERT_FALSE(labeling->nodeHasProposition(smth,1));
ASSERT_FALSE(labeling->nodeHasProposition(smth,2));
ASSERT_FALSE(labeling->nodeHasProposition(smth,3));
ASSERT_FALSE(labeling->nodeHasProposition(smth,6));
ASSERT_FALSE(labeling->nodeHasProposition(smth,7));
ASSERT_FALSE(labeling->nodeHasProposition(smth,8));
ASSERT_FALSE(labeling->nodeHasProposition(smth,9));
ASSERT_FALSE(labeling->nodeHasProposition(smth,10));
ASSERT_FALSE(labeling->nodeHasProposition(smth,11));
//Deleting the labeling
delete labeling;
//This test is based on a test case from the original MRMC.
mrmc::dtmc::labeling* labeling = NULL;
//Parsing the file
ASSERT_NO_THROW(labeling = mrmc::parser::read_lab_file(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
//Checking whether all propositions are in the labelling
char phi[] = "phi", psi[] = "psi", smth[] = "smth";
if (labeling != NULL) {
ASSERT_TRUE(labeling->containsProposition(phi));
ASSERT_TRUE(labeling->containsProposition(psi));
ASSERT_TRUE(labeling->containsProposition(smth));
//Testing whether all and only the correct nodes are labeled with "phi"
ASSERT_TRUE(labeling->nodeHasProposition(phi,1));
ASSERT_TRUE(labeling->nodeHasProposition(phi,2));
ASSERT_TRUE(labeling->nodeHasProposition(phi,3));
ASSERT_TRUE(labeling->nodeHasProposition(phi,5));
ASSERT_TRUE(labeling->nodeHasProposition(phi,7));
ASSERT_TRUE(labeling->nodeHasProposition(phi,9));
ASSERT_TRUE(labeling->nodeHasProposition(phi,10));
ASSERT_TRUE(labeling->nodeHasProposition(phi,11));
ASSERT_FALSE(labeling->nodeHasProposition(phi,4));
ASSERT_FALSE(labeling->nodeHasProposition(phi,6));
//Testing whether all and only the correct nodes are labeled with "psi"
ASSERT_TRUE(labeling->nodeHasProposition(psi,6));
ASSERT_TRUE(labeling->nodeHasProposition(psi,7));
ASSERT_TRUE(labeling->nodeHasProposition(psi,8));
ASSERT_FALSE(labeling->nodeHasProposition(psi,1));
ASSERT_FALSE(labeling->nodeHasProposition(psi,2));
ASSERT_FALSE(labeling->nodeHasProposition(psi,3));
ASSERT_FALSE(labeling->nodeHasProposition(psi,4));
ASSERT_FALSE(labeling->nodeHasProposition(psi,5));
ASSERT_FALSE(labeling->nodeHasProposition(psi,9));
ASSERT_FALSE(labeling->nodeHasProposition(psi,10));
ASSERT_FALSE(labeling->nodeHasProposition(psi,11));
//Testing whether all and only the correct nodes are labeled with "smth"
ASSERT_TRUE(labeling->nodeHasProposition(smth,4));
ASSERT_TRUE(labeling->nodeHasProposition(smth,5));
ASSERT_FALSE(labeling->nodeHasProposition(smth,1));
ASSERT_FALSE(labeling->nodeHasProposition(smth,2));
ASSERT_FALSE(labeling->nodeHasProposition(smth,3));
ASSERT_FALSE(labeling->nodeHasProposition(smth,6));
ASSERT_FALSE(labeling->nodeHasProposition(smth,7));
ASSERT_FALSE(labeling->nodeHasProposition(smth,8));
ASSERT_FALSE(labeling->nodeHasProposition(smth,9));
ASSERT_FALSE(labeling->nodeHasProposition(smth,10));
ASSERT_FALSE(labeling->nodeHasProposition(smth,11));
//Deleting the labeling
delete labeling;
}
} }
TEST(ReadLabFileTest, WrongHeaderTest1) { TEST(ReadLabFileTest, WrongHeaderTest1) {

58
test/parser/read_tra_file_test.cpp
View File

@ -22,45 +22,47 @@ TEST(ReadTraFileTest, NonExistingFileTest) {
/* The following test case is based on one of the original MRMC test cases /* The following test case is based on one of the original MRMC test cases
*/ */
TEST(ReadTraFileTest, ParseFileTest1) { TEST(ReadTraFileTest, ParseFileTest1) {
pantheios::log_INFORMATIONAL("Started ParseFileTest1");
mrmc::sparse::StaticSparseMatrix<double> *result;
ASSERT_NO_THROW(result = mrmc::parser::read_tra_file(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
pantheios::log_INFORMATIONAL("Started ParseFileTest1");
mrmc::sparse::StaticSparseMatrix<double> *result = NULL;
ASSERT_NO_THROW(result = mrmc::parser::read_tra_file(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
double val = 0;
ASSERT_TRUE(result->getValue(1,1,&val));
ASSERT_EQ(val,0.080645161290322580645161290322581);
if (result != NULL) {
double val = 0;
ASSERT_TRUE(result->getValue(1,1,&val));
ASSERT_EQ(val,0.080645161290322580645161290322581);
ASSERT_TRUE(result->getValue(1,2,&val));
ASSERT_EQ(val,0.080645161290322580645161290322581);
ASSERT_TRUE(result->getValue(1,2,&val));
ASSERT_EQ(val,0.080645161290322580645161290322581);
//Transition 1->3 was not set in the file, so it is not to appear in the matrix!
ASSERT_FALSE(result->getValue(1,3,&val));
ASSERT_EQ(val,0);
//Transition 1->3 was not set in the file, so it is not to appear in the matrix!
ASSERT_FALSE(result->getValue(1,3,&val));
ASSERT_EQ(val,0);
ASSERT_TRUE(result->getValue(2,1,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2,1,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2,2,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2,2,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2,3,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2,3,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2,4,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(2,4,&val));
ASSERT_EQ(val,0.04032258064516129032258064516129);
ASSERT_TRUE(result->getValue(3,2,&val));
ASSERT_EQ(val,0.0806451612903225806451612903225812);
ASSERT_TRUE(result->getValue(3,2,&val));
ASSERT_EQ(val,0.0806451612903225806451612903225812);
ASSERT_TRUE(result->getValue(3,3,&val));
ASSERT_EQ(val,0);
ASSERT_TRUE(result->getValue(3,3,&val));
ASSERT_EQ(val,0);
ASSERT_TRUE(result->getValue(3,4,&val));
ASSERT_EQ(val,0.080645161290322580645161290322581);
ASSERT_TRUE(result->getValue(3,4,&val));
ASSERT_EQ(val,0.080645161290322580645161290322581);
ASSERT_TRUE(result->getValue(4,4,&val));
ASSERT_EQ(val,0);
delete result;
ASSERT_TRUE(result->getValue(4,4,&val));
ASSERT_EQ(val,0);
delete result;
}
} }
TEST(ReadTraFileTest, WrongFormatTestHeader1) { TEST(ReadTraFileTest, WrongFormatTestHeader1) {
Write Preview
Loading…
Cancel
Save