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

Included new (smaller) test model. Bugfixes and improvements to BackwardTransitions class. Removed performance test code from main() function in favor for creating a simple DTMC from the input parameters.

tempestpy_adaptions
dehnert 12 years ago
parent
46e010075a
commit
12e6a945df
2 changed files with 46 additions and 106 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. 78
      src/models/backward_transitions.h
  2. 74
      src/mrmc-cpp.cpp

78
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,60 +23,67 @@ template <class T>
class BackwardTransitions { class BackwardTransitions {
public: public:
/*!
* Just typedef the iterator as a pointer to the index type.
*/
typedef uint_fast64_t* 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()),
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. // 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. // 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++) { 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 // Add the last row individually, as the comparison bound in the for-loop
// is different in this case. // 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. // 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]; 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] = numberOfNonZeroEntries;
// 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 i = 0; i < numberOfStates; i++) {
for (uint_fast64_t j = row_indications[i]; j < row_indications[i + 1]; j++) { 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 // Add the last row individually, as the comparison bound in the for-loop
// is different in this case. // 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<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]]));
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: private:
@ -121,6 +114,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 entries to determine the highest index at
* which the predecessor_list may be accessed.
*/
uint_fast64_t numberOfNonZeroEntries;
}; };
} // 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,80 +35,16 @@ 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));
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;
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);
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; return 0;
} }

Write Preview
Loading…
Cancel
Save