diff --git a/src/models/backward_transitions.h b/src/models/backward_transitions.h index 8a4aca260..0934518a7 100644 --- a/src/models/backward_transitions.h +++ b/src/models/backward_transitions.h @@ -8,7 +8,7 @@ #ifndef BACKWARD_TRANSITIONS_H_ #define BACKWARD_TRANSITIONS_H_ -#include +#include #include "src/sparse/static_sparse_matrix.h" namespace mrmc { @@ -23,60 +23,67 @@ template class BackwardTransitions { public: + /*! + * Just typedef the iterator as a pointer to the index type. + */ + typedef uint_fast64_t* state_predecessor_iterator; + //! Constructor /*! * Constructs a backward transitions object from the given sparse matrix * 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. */ - BackwardTransitions(mrmc::sparse::StaticSparseMatrix* 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* transitionMatrix) + : numberOfStates(transitionMatrix->getRowCount()), + numberOfNonZeroEntries(transitionMatrix->getNonZeroEntryCount()) { + this->state_indices_list = new uint_fast64_t[numberOfStates + 1]; + this->predecessor_list = new uint_fast64_t[numberOfNonZeroEntries]; // First, we need to count how many backward transitions each state has. // NOTE: We disregard the diagonal here, as we only consider "true" // 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++) { + uint_fast64_t* row_indications = transitionMatrix->getRowIndicationsPointer(); + uint_fast64_t* column_indications = transitionMatrix->getColumnIndicationsPointer(); + for (uint_fast64_t i = 0; i < numberOfStates; i++) { for (uint_fast64_t j = row_indications[i]; j < row_indications[i + 1]; j++) { - this->state_indices_list[column_indications[j]]++; + this->state_indices_list[column_indications[j] + 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]]++; + for (uint_fast64_t j = row_indications[numberOfStates]; j < numberOfNonZeroEntries + 1; j++) { + this->state_indices_list[column_indications[j] + 1]++; } // 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 + 1; 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, // for each state i the range of indices can be read off between // 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] = numberOfNonZeroEntries; // Create an array that stores the next index for each state. Initially // 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 // 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 i = 0; i < numberOfStates; 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]; + this->predecessor_list[next_state_index_list[column_indications[j]]++] = 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]; + for (uint_fast64_t j = row_indications[numberOfStates]; j < numberOfNonZeroEntries; j++) { + this->predecessor_list[next_state_index_list[transitionMatrix->getRowCount()]++] = column_indications[j]; } } @@ -89,26 +96,12 @@ public: } } - class const_iterator : public std::iterator { - 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]])); + 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]])); + state_predecessor_iterator endStatePredecessorIterator(uint_fast64_t state) const { + return this->predecessor_list + this->state_indices_list[state + 1]; } private: @@ -121,6 +114,17 @@ private: */ 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 entries to determine the highest index at + * which the predecessor_list may be accessed. + */ + uint_fast64_t numberOfNonZeroEntries; }; } // namespace models diff --git a/src/mrmc-cpp.cpp b/src/mrmc-cpp.cpp index d28bcb2d0..e9db4cd67 100644 --- a/src/mrmc-cpp.cpp +++ b/src/mrmc-cpp.cpp @@ -23,7 +23,7 @@ PANTHEIOS_EXTERN_C PAN_CHAR_T const PANTHEIOS_FE_PROCESS_IDENTITY[] = "mrmc-cpp"; #include "MRMCConfig.h" - +#include "src/models/dtmc.h" #include "src/sparse/static_sparse_matrix.h" #include "src/models/atomic_propositions_labeling.h" #include "src/parser/read_lab_file.h" @@ -35,80 +35,16 @@ int main(int argc, char* argv[]) { pantheios_be_file_setFilePath("log.all"); pantheios::log_INFORMATIONAL("MRMC-Cpp started."); - if (argc < 2) { + if (argc < 3) { std::cout << "Required argument #1 inputTraFile.tra not found!" << std::endl; exit(-1); } - mrmc::sparse::StaticSparseMatrix *ssm; - mrmc::sparse::StaticSparseMatrix *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; + mrmc::sparse::StaticSparseMatrix* probMatrix = mrmc::parser::read_tra_file(argv[1]); + mrmc::models::AtomicPropositionsLabeling* labeling = mrmc::parser::read_lab_file(probMatrix->getRowCount(), argv[2]); + mrmc::models::Dtmc dtmc(probMatrix, labeling); - ssmBack = new mrmc::sparse::StaticSparseMatrix(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)); - for (j = 0; j < 2097152; ++j) { - iArray[j] = 0; - } - 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; return 0; }