Browse Source

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

tempestpy_adaptions
gereon 12 years ago
parent
commit
d7fd833104
  1. 21
      CMakeLists.txt
  2. 18
      src/models/atomic_propositions_labeling.h
  3. 100
      src/models/backward_transitions.h
  4. 74
      src/mrmc-cpp.cpp
  5. 2
      src/parser/read_tra_file.cpp
  6. 817
      src/sparse/static_sparse_matrix.h
  7. 30
      test/sparse/static_sparse_matrix_test.cpp

21
CMakeLists.txt

@ -6,19 +6,24 @@ project (MRMC-cpp CXX C)
set (MRMC_CPP_VERSION_MAJOR 1)
set (MRMC_CPP_VERSION_MINOR 0)
option(DEBUG "Sets whether the DEBUG mode is used" ON)
option(DEFINE_UNIX "Defines the UNIX flag for compilation." OFF)
option(USE_POPCNT "Sets whether the popcnt instruction is going to be used." OFF)
if (DEBUG)
set (CMAKE_BUILD_TYPE "DEBUG")
else()
set (CMAKE_BUILD_TYPE "RELEASE")
endif()
#Configurations for GCC
if(CMAKE_COMPILER_IS_GNUCC)
set(MRMC_GCC_NO_DEBUG_SYMBOLS OFF CACHE BOOL "Whether debug symbols should be included in MRMC with GCC, set ON for better performance")
#Using C++11
set (CMAKE_CXX_FLAGS "-std=c++0x")
set (CMAKE_CXX_FLAGS "-std=c++0x -Wall -pedantic")
#Debug symbols
if (NOT MRMC_GCC_NO_DEBUG_SYMBOLS)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -g")
message(STATUS "Using Debug Symbols for GCC")
endif()
# Turn on popcnt instruction if possible
if (USE_POPCNT)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -msse4.2")
endif(USE_POPCNT)
endif()
# configure a header file to pass some of the CMake settings

18
src/models/atomic_propositions_labeling.h

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

100
src/models/backward_transitions.h

@ -8,7 +8,7 @@
#ifndef BACKWARD_TRANSITIONS_H_
#define BACKWARD_TRANSITIONS_H_
#include <iterator>
#include <iostream>
#include "src/sparse/static_sparse_matrix.h"
namespace mrmc {
@ -23,63 +23,61 @@ template <class T>
class BackwardTransitions {
public:
/*!
* Just typedef the iterator as a pointer to the index type.
*/
typedef const uint_fast64_t * const 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<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.
// 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++) {
for (uint_fast64_t j = row_indications[i]; j < row_indications[i + 1]; j++) {
this->state_indices_list[column_indications[j]]++;
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.
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];
}
// 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] = numberOfNonZeroTransitions;
// 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 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];
}
}
//! Destructor
/*!
* Destructor. Frees the internal storage.
*/
~BackwardTransitions() {
if (this->predecessor_list != NULL) {
delete[] this->predecessor_list;
@ -89,26 +87,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:
@ -121,6 +118,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 transition entries to determine the highest
* index at which the predecessor_list may be accessed.
*/
uint_fast64_t numberOfNonZeroTransitions;
};
} // namespace models

74
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<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;
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);
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;
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;
}

2
src/parser/read_tra_file.cpp

@ -135,7 +135,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
* 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);
sp = new sparse::StaticSparseMatrix<double>(rows + 1);
if ( NULL == sp ) {
throw std::bad_alloc();
return NULL;

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

30
test/sparse/static_sparse_matrix_test.cpp

@ -29,10 +29,10 @@ TEST(StaticSparseMatrixTest, addNextValueTest) {
ASSERT_NO_THROW(ssm->initialize(1));
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_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_THROW(ssm->addNextValue(6, 1, 1), mrmc::exceptions::out_of_range);
@ -78,7 +78,7 @@ TEST(StaticSparseMatrixTest, Test) {
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, /* 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 */
13, 13, 13, 13, /* a few empty rows, middle columns */
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);
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_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);
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_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;
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());
}
}
@ -278,7 +278,7 @@ TEST(StaticSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest
int target = -1;
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());
}
}
@ -294,9 +294,9 @@ TEST(StaticSparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest)
ASSERT_NO_THROW(ssm->initialize(100 - 10));
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);
@ -311,4 +311,4 @@ TEST(StaticSparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest)
ASSERT_EQ(values[row * 10 + col], esm->coeff(row, col));
}
}
}
}
Loading…
Cancel
Save