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

Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC into parser 

Conflicts:
	src/mrmc-cpp.cpp
	src/parser/read_tra_file.cpp
tempestpy_adaptions
gereon 12 years ago
parent
408290d72b eeddadc096
commit
3807591edd
5 changed files with 599 additions and 438 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. 12
      src/models/atomic_propositions_labeling.h
  2. 98
      src/models/backward_transitions.h
  3. 74
      src/mrmc-cpp.cpp
  4. 749
      src/sparse/static_sparse_matrix.h
  5. 28
      test/sparse/static_sparse_matrix_test.cpp

12
src/models/atomic_propositions_labeling.h
View File

@ -58,12 +58,8 @@ public:
* @param state_count The number of states of the model. * @param state_count The number of states of the model.
* @param ap_count The number of atomic propositions. * @param ap_count The number of atomic propositions.
*/ */
AtomicPropositionsLabeling(const uint_fast32_t state_count,
const uint_fast32_t ap_count) {
// add one for 1-bound indices
this->state_count = state_count + 1;
this->ap_count = ap_count;
this->aps_current = 0;
AtomicPropositionsLabeling(const uint_fast32_t state_count, const uint_fast32_t ap_count)
: state_count(state_count), ap_count(ap_count), aps_current(0) {
this->single_labelings = new SingleAtomicPropositionLabeling*[ap_count]; this->single_labelings = new SingleAtomicPropositionLabeling*[ap_count];
for (uint_fast32_t i = 0; i < ap_count; ++i) { for (uint_fast32_t i = 0; i < ap_count; ++i) {
this->single_labelings[i] = new SingleAtomicPropositionLabeling(state_count); this->single_labelings[i] = new SingleAtomicPropositionLabeling(state_count);
@ -75,8 +71,8 @@ public:
* Copy Constructor. Performs a deep copy of the given atomic proposition * Copy Constructor. Performs a deep copy of the given atomic proposition
* labeling. * labeling.
*/ */
AtomicPropositionsLabeling(const AtomicPropositionsLabeling& atomic_propositions_labeling) :
state_count(atomic_propositions_labeling.state_count),
AtomicPropositionsLabeling(const AtomicPropositionsLabeling& atomic_propositions_labeling)
: state_count(atomic_propositions_labeling.state_count),
ap_count(atomic_propositions_labeling.ap_count), ap_count(atomic_propositions_labeling.ap_count),
aps_current(atomic_propositions_labeling.aps_current), aps_current(atomic_propositions_labeling.aps_current),
name_to_labeling_map(atomic_propositions_labeling.name_to_labeling_map) { name_to_labeling_map(atomic_propositions_labeling.name_to_labeling_map) {

98
src/models/backward_transitions.h
View File

@ -8,7 +8,7 @@
#ifndef BACKWARD_TRANSITIONS_H_ #ifndef BACKWARD_TRANSITIONS_H_
#define BACKWARD_TRANSITIONS_H_ #define BACKWARD_TRANSITIONS_H_
#include <iterator>
#include <iostream>
#include "src/sparse/static_sparse_matrix.h" #include "src/sparse/static_sparse_matrix.h"
namespace mrmc { namespace mrmc {
@ -23,61 +23,57 @@ template <class T>
class BackwardTransitions { class BackwardTransitions {
public: public:
/*!
* Just typedef the iterator as a pointer to the index type.
*/
typedef const uint_fast64_t * const state_predecessor_iterator;
//! Constructor //! Constructor
/*! /*!
* Constructs a backward transitions object from the given sparse matrix * Constructs a backward transitions object from the given sparse matrix
* representing the (forward) transition relation. * representing the (forward) transition relation.
* @param transition_matrix The (1-based) matrix representing the transition
* @param transition_matrix The (0-based) matrix representing the transition
* relation. * relation.
*/ */
BackwardTransitions(mrmc::sparse::StaticSparseMatrix<T>* transition_matrix) {
this->state_indices_list = new uint_fast64_t[transition_matrix->getRowCount() + 2];
this->predecessor_list = new uint_fast64_t[transition_matrix->getNonZeroEntryCount()];
BackwardTransitions(mrmc::sparse::StaticSparseMatrix<T>* transitionMatrix)
: numberOfStates(transitionMatrix->getRowCount()),
numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
this->state_indices_list = new uint_fast64_t[numberOfStates + 1];
this->predecessor_list = new uint_fast64_t[numberOfNonZeroTransitions];
// First, we need to count how many backward transitions each state has. // First, we need to count how many backward transitions each state has.
// NOTE: We disregard the diagonal here, as we only consider "true" // NOTE: We disregard the diagonal here, as we only consider "true"
// predecessors. // predecessors.
// Start by counting all but the last row.
uint_fast64_t* row_indications = transition_matrix->getRowIndicationsPointer();
uint_fast64_t* column_indications = transition_matrix->getColumnIndicationsPointer();
for (uint_fast64_t i = 1; i < transition_matrix->getRowCount(); i++) {
for (uint_fast64_t j = row_indications[i]; j < row_indications[i + 1]; j++) {
this->state_indices_list[column_indications[j]]++;
}
uint_fast64_t* row_indications = transitionMatrix->getRowIndicationsPointer();
uint_fast64_t* column_indications = transitionMatrix->getColumnIndicationsPointer();
for (uint_fast64_t i = 0; i <= numberOfStates; i++) {
for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) {
this->state_indices_list[*rowIt + 1]++;
} }
// Add the last row individually, as the comparison bound in the for-loop
// is different in this case.
for (uint_fast64_t j = row_indications[transition_matrix->getRowCount()]; j < transition_matrix->getNonZeroEntryCount(); j++) {
this->state_indices_list[column_indications[j]]++;
} }
// Now compute the accumulated offsets. // Now compute the accumulated offsets.
for (uint_fast64_t i = 1; i < transition_matrix->getRowCount() + 1; i++) {
for (uint_fast64_t i = 1; i <= numberOfStates; i++) {
this->state_indices_list[i] = this->state_indices_list[i - 1] + this->state_indices_list[i]; this->state_indices_list[i] = this->state_indices_list[i - 1] + this->state_indices_list[i];
} }
// Put a sentinel element at the end of the indices list. This way, // Put a sentinel element at the end of the indices list. This way,
// for each state i the range of indices can be read off between // for each state i the range of indices can be read off between
// state_indices_list[i] and state_indices_list[i + 1]. // state_indices_list[i] and state_indices_list[i + 1].
this->state_indices_list[transition_matrix->getRowCount() + 1] = this->state_indices_list[transition_matrix->getRowCount()];
this->state_indices_list[numberOfStates + 1] = numberOfNonZeroTransitions;
// Create an array that stores the next index for each state. Initially // Create an array that stores the next index for each state. Initially
// this corresponds to the previously computed accumulated offsets. // this corresponds to the previously computed accumulated offsets.
uint_fast64_t* next_state_index_list = new uint_fast64_t[transition_matrix->getRowCount() + 1];
memcpy(next_state_index_list, state_indices_list, (transition_matrix->getRowCount() + 1) * sizeof(uint_fast64_t));
uint_fast64_t* next_state_index_list = new uint_fast64_t[numberOfStates + 1];
memcpy(next_state_index_list, state_indices_list, (numberOfStates + 1) * sizeof(uint_fast64_t));
// Now we are ready to actually fill in the list of predecessors for // Now we are ready to actually fill in the list of predecessors for
// every state. Again, we start by considering all but the last row. // every state. Again, we start by considering all but the last row.
for (uint_fast64_t i = 1; i < transition_matrix->getRowCount(); i++) {
for (uint_fast64_t j = row_indications[i]; j < row_indications[i + 1]; j++) {
this->predecessor_list[next_state_index_list[i]++] = column_indications[j];
for (uint_fast64_t i = 0; i <= numberOfStates; i++) {
for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) {
this->predecessor_list[next_state_index_list[*rowIt]++] = i;
} }
} }
// Add the last row individually, as the comparison bound in the for-loop
// is different in this case.
for (uint_fast64_t j = row_indications[transition_matrix->getRowCount()]; j < transition_matrix->getNonZeroEntryCount(); j++) {
this->state_indices_list[next_state_index_list[transition_matrix->getRowCount()]++] = column_indications[j];
}
} }
~BackwardTransitions() { ~BackwardTransitions() {
@ -89,26 +85,25 @@ public:
} }
} }
class const_iterator : public std::iterator<std::input_iterator_tag, uint_fast64_t> {
public:
const_iterator(uint_fast64_t* ptr) : ptr_(ptr) { }
const_iterator operator++() { const_iterator i = *this; ptr_++; return i; }
const_iterator operator++(int offset) { ptr_ += offset; return *this; }
const uint_fast64_t& operator*() { return *ptr_; }
const uint_fast64_t* operator->() { return ptr_; }
bool operator==(const const_iterator& rhs) { return ptr_ == rhs.ptr_; }
bool operator!=(const const_iterator& rhs) { return ptr_ != rhs.ptr_; }
private:
uint_fast64_t* ptr_;
};
const_iterator beginPredecessorIterator(uint_fast64_t state) const {
return const_iterator(&(this->predecessor_list[this->state_indices_list[state]]));
/*!
* Returns an iterator to the predecessors of the given states.
* @param state The state for which to get the predecessor iterator.
* @return An iterator to the predecessors of the given states.
*/
state_predecessor_iterator beginStatePredecessorIterator(uint_fast64_t state) const {
return this->predecessor_list + this->state_indices_list[state];
} }
const_iterator endPredecessorIterator(uint_fast64_t state) const {
return const_iterator(&(this->predecessor_list[this->state_indices_list[state + 1]]));
/*!
* Returns an iterator referring to the element after the predecessors of
* the given state.
* @param row The state for which to get the iterator.
* @return An iterator referring to the element after the predecessors of
* the given state.
*/
state_predecessor_iterator endStatePredecessorIterator(uint_fast64_t state) const {
return this->predecessor_list + this->state_indices_list[state + 1];
} }
private: private:
@ -121,6 +116,17 @@ private:
*/ */
uint_fast64_t* state_indices_list; uint_fast64_t* state_indices_list;
/*!
* Store the number of states to determine the highest index at which the
* state_indices_list may be accessed.
*/
uint_fast64_t numberOfStates;
/*!
* Store the number of non-zero transition entries to determine the highest
* index at which the predecessor_list may be accessed.
*/
uint_fast64_t numberOfNonZeroTransitions;
}; };
} // namespace models } // namespace models

74
src/mrmc-cpp.cpp
View File

@ -23,7 +23,7 @@
PANTHEIOS_EXTERN_C PAN_CHAR_T const PANTHEIOS_FE_PROCESS_IDENTITY[] = "mrmc-cpp"; PANTHEIOS_EXTERN_C PAN_CHAR_T const PANTHEIOS_FE_PROCESS_IDENTITY[] = "mrmc-cpp";
#include "MRMCConfig.h" #include "MRMCConfig.h"
#include "src/models/dtmc.h"
#include "src/sparse/static_sparse_matrix.h" #include "src/sparse/static_sparse_matrix.h"
#include "src/models/atomic_propositions_labeling.h" #include "src/models/atomic_propositions_labeling.h"
#include "src/parser/read_lab_file.h" #include "src/parser/read_lab_file.h"
@ -35,78 +35,14 @@ int main(int argc, char* argv[]) {
pantheios_be_file_setFilePath("log.all"); pantheios_be_file_setFilePath("log.all");
pantheios::log_INFORMATIONAL("MRMC-Cpp started."); pantheios::log_INFORMATIONAL("MRMC-Cpp started.");
if (argc < 2) {
if (argc < 3) {
std::cout << "Required argument #1 inputTraFile.tra not found!" << std::endl; std::cout << "Required argument #1 inputTraFile.tra not found!" << std::endl;
exit(-1); exit(-1);
} }
mrmc::sparse::StaticSparseMatrix<double> *ssm;
mrmc::sparse::StaticSparseMatrix<double> *ssmBack;
// 1. Create an instance of the platformstl::performance_counter. (On
// UNIX this will resolve to unixstl::performance_counter; on Win32 it
// will resolve to winstl::performance_counter.)
platformstl::performance_counter counter;
std::cout << "Building Matrix from File..." << std::endl;
// 2. Begin the measurement
counter.start();
ssm = mrmc::parser::read_tra_file(argv[1]);
//lab = mrmc::parser::read_lab_file(20302, "csl_unbounded_until_sim_06.lab");
counter.stop();
std::cout << "Loaded " << ssm->getNonZeroEntryCount() << " entries into (" << ssm->getRowCount() << " x " << ssm->getRowCount() << ")." << std::endl;
std::cout << "Time needed was " << (unsigned long long)counter.get_microseconds() << std::endl;
counter.start();
auto esm = ssm->toEigenSparseMatrix();
counter.stop();
std::cout << "Loaded " << esm->nonZeros() << " entries into (" << esm->rows() << " x " << esm->cols() << ")." << std::endl;
std::cout << "Time needed was " << (unsigned long long)counter.get_microseconds() << std::endl;
ssmBack = new mrmc::sparse::StaticSparseMatrix<double>(esm->rows());
counter.start();
ssmBack->initialize(*esm);
counter.stop();
std::cout << "Loaded " << ssmBack->getNonZeroEntryCount() << " entries into (" << ssmBack->getRowCount() << " x " << ssmBack->getRowCount() << ")." << std::endl;
std::cout << "Time needed was " << (unsigned long long)counter.get_microseconds() << std::endl;
delete ssm;
delete ssmBack;
std::cout << std::endl;
std::cout << ":: C-style vs. C++ Style Array init Showdown ::" << std::endl;
uint_fast64_t *iArray = NULL;
uint_fast32_t i = 0;
uint_fast32_t j = 0;
counter.start();
for (i = 0; i < 10000; ++i) {
iArray = (uint_fast64_t*)malloc(2097152 * sizeof(uint_fast64_t));
memset(iArray, 0, 2097152 * sizeof(uint_fast64_t));
free(iArray);
}
counter.stop();
std::cout << "C-style: " << (unsigned long long)counter.get_microseconds() << std::endl;
counter.start();
for (i = 0; i < 10000; ++i) {
iArray = new uint_fast64_t[2097152]();
delete[] iArray;
}
counter.stop();
std::cout << "Cpp-style: " << (unsigned long long)counter.get_microseconds() << std::endl;
mrmc::sparse::StaticSparseMatrix<double>* probMatrix = mrmc::parser::read_tra_file(argv[1]);
mrmc::models::AtomicPropositionsLabeling* labeling = mrmc::parser::read_lab_file(probMatrix->getRowCount(), argv[2]);
mrmc::models::Dtmc<double> dtmc(probMatrix, labeling);
return 0; return 0;
} }

749
src/sparse/static_sparse_matrix.h
File diff suppressed because it is too large
View File

28
test/sparse/static_sparse_matrix_test.cpp
View File

@ -29,10 +29,10 @@ TEST(StaticSparseMatrixTest, addNextValueTest) {
ASSERT_NO_THROW(ssm->initialize(1)); ASSERT_NO_THROW(ssm->initialize(1));
ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::Initialized); ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::Initialized);
ASSERT_THROW(ssm->addNextValue(0, 1, 1), mrmc::exceptions::out_of_range);
ASSERT_THROW(ssm->addNextValue(-1, 1, 1), mrmc::exceptions::out_of_range);
ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::Error); ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(1, 0, 1), mrmc::exceptions::out_of_range);
ASSERT_THROW(ssm->addNextValue(1, -1, 1), mrmc::exceptions::out_of_range);
ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::Error); ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::Error);
ASSERT_THROW(ssm->addNextValue(6, 1, 1), mrmc::exceptions::out_of_range); ASSERT_THROW(ssm->addNextValue(6, 1, 1), mrmc::exceptions::out_of_range);
@ -78,7 +78,7 @@ TEST(StaticSparseMatrixTest, Test) {
int position_row[50] = { int position_row[50] = {
2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
2, 2, 2, 2, /* first row empty, one full row � 25 minus the diagonal entry */
2, 2, 2, 2, /* first row empty, one full row ��� 25 minus the diagonal entry */
4, 4, /* one empty row, then first and last column */ 4, 4, /* one empty row, then first and last column */
13, 13, 13, 13, /* a few empty rows, middle columns */ 13, 13, 13, 13, /* a few empty rows, middle columns */
24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24, 24,
@ -151,10 +151,10 @@ TEST(StaticSparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest)
ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::ReadReady); ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1; int target = -1;
for (int row = 1; row <= 10; ++row) {
for (int col = 1; col <= 10; ++col) {
for (int row = 0; row < 10; ++row) {
for (int col = 0; col < 10; ++col) {
ASSERT_TRUE(ssm->getValue(row, col, &target)); ASSERT_TRUE(ssm->getValue(row, col, &target));
ASSERT_EQ(target, (row - 1) * 10 + col - 1);
ASSERT_EQ(target, row * 10 + col);
} }
} }
} }
@ -181,10 +181,10 @@ TEST(StaticSparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest)
ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::ReadReady); ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::ReadReady);
int target = -1; int target = -1;
for (int row = 1; row <= 10; ++row) {
for (int col = 1; col <= 10; ++col) {
for (int row = 0; row < 10; ++row) {
for (int col = 0; col < 10; ++col) {
ASSERT_TRUE(ssm->getValue(row, col, &target)); ASSERT_TRUE(ssm->getValue(row, col, &target));
ASSERT_EQ(target, (row - 1) * 10 + col - 1);
ASSERT_EQ(target, row * 10 + col);
} }
} }
} }
@ -231,7 +231,7 @@ TEST(StaticSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest
int target = -1; int target = -1;
for (auto &coeff: tripletList) { for (auto &coeff: tripletList) {
ASSERT_TRUE(ssm->getValue(coeff.row() + 1, coeff.col() + 1, &target));
ASSERT_TRUE(ssm->getValue(coeff.row(), coeff.col(), &target));
ASSERT_EQ(target, coeff.value()); ASSERT_EQ(target, coeff.value());
} }
} }
@ -278,7 +278,7 @@ TEST(StaticSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest
int target = -1; int target = -1;
for (auto &coeff: tripletList) { for (auto &coeff: tripletList) {
ASSERT_TRUE(ssm->getValue(coeff.row() + 1, coeff.col() + 1, &target));
ASSERT_TRUE(ssm->getValue(coeff.row(), coeff.col(), &target));
ASSERT_EQ(target, coeff.value()); ASSERT_EQ(target, coeff.value());
} }
} }
@ -294,9 +294,9 @@ TEST(StaticSparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest)
ASSERT_NO_THROW(ssm->initialize(100 - 10)); ASSERT_NO_THROW(ssm->initialize(100 - 10));
ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::Initialized); ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::Initialized);
for (uint_fast32_t row = 1; row <= 10; ++row) {
for (uint_fast32_t col = 1; col <= 10; ++col) {
ASSERT_NO_THROW(ssm->addNextValue(row, col, values[(row - 1) * 10 + (col - 1)]));
for (uint_fast32_t row = 0; row < 10; ++row) {
for (uint_fast32_t col = 0; col < 10; ++col) {
ASSERT_NO_THROW(ssm->addNextValue(row, col, values[row * 10 + col]));
} }
} }
ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::Initialized); ASSERT_EQ(ssm->getState(), mrmc::sparse::StaticSparseMatrix<int>::MatrixStatus::Initialized);

Write Preview
Loading…
Cancel
Save