Browse Source

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

Conflicts:
	src/mrmc-cpp.cpp
main
gereon 13 years ago
parent
commit
2a9498d8d4
  1. 5
      CMakeLists.txt
  2. 4
      src/models/atomic_propositions_labeling.h
  3. 29
      src/models/backward_transitions.h
  4. 18
      src/models/dtmc.h
  5. 10
      src/mrmc-cpp.cpp
  6. 12
      src/parser/read_lab_file.cpp
  7. 21
      src/parser/read_tra_file.cpp
  8. 2
      src/reward/reward_model.h
  9. 10
      src/sparse/static_sparse_matrix.h
  10. 103
      src/vector/bitvector.h

5
CMakeLists.txt

@ -24,7 +24,7 @@ endif()
#Configurations for GCC
if(CMAKE_COMPILER_IS_GNUCC)
set (CMAKE_CXX_FLAGS "-std=c++0x -Wall -pedantic")
set (CMAKE_CXX_FLAGS "-std=c++0x -Wall -Werror -pedantic")
# Turn on popcnt instruction if possible
if (USE_POPCNT)
@ -123,12 +123,15 @@ else()
endif()
if(Boost_FOUND)
if (NOT BOOST_PROGRAM_OPTIONS_LIBRARY)
set(BOOST_PROGRAM_OPTIONS_LIBRARY "boost_program_options")
endif()
include_directories(${Boost_INCLUDE_DIRS})
if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL ""))
set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib")
endif ()
link_directories(${Boost_LIBRARY_DIRS})
endif(Boost_FOUND)

4
src/models/atomic_propositions_labeling.h

@ -78,8 +78,7 @@ public:
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(
*atomic_propositions_labeling.single_labelings[i]);
this->single_labelings[i] = new SingleAtomicPropositionLabeling(*atomic_propositions_labeling.single_labelings[i]);
}
}
@ -89,7 +88,6 @@ public:
*/
virtual ~AtomicPropositionsLabeling() {
// delete all the single atomic proposition labelings in the map
MAP<std::string, SingleAtomicPropositionLabeling*>::iterator it;
for (uint_fast32_t i = 0; i < ap_count; ++i) {
delete this->single_labelings[i];
this->single_labelings[i] = NULL;

29
src/models/backward_transitions.h

@ -35,43 +35,47 @@ public:
* @param transition_matrix The (0-based) matrix representing the transition
* relation.
*/
BackwardTransitions(mrmc::sparse::StaticSparseMatrix<T>* transitionMatrix)
: numberOfStates(transitionMatrix->getRowCount()),
numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
this->state_indices_list = new uint_fast64_t[numberOfStates + 1];
BackwardTransitions(mrmc::sparse::StaticSparseMatrix<T>* transitionMatrix) {
numberOfNonZeroTransitions = transitionMatrix->getNonZeroEntryCount();
this->predecessor_list = new uint_fast64_t[numberOfNonZeroTransitions];
numberOfStates = transitionMatrix->getRowCount();
this->state_indices_list = new uint_fast64_t[numberOfStates + 1];
// First, we need to count how many backward transitions each state has.
// NOTE: We disregard the diagonal here, as we only consider "true"
// predecessors.
for (uint_fast64_t i = 0; i <= numberOfStates; i++) {
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]++;
}
}
// Now compute the accumulated offsets.
for (uint_fast64_t i = 1; i <= numberOfStates; 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[numberOfStates + 1] = numberOfNonZeroTransitions;
this->state_indices_list[numberOfStates] = 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[numberOfStates + 1];
memcpy(next_state_index_list, state_indices_list, (numberOfStates + 1) * sizeof(uint_fast64_t));
uint_fast64_t* next_state_index_list = new uint_fast64_t[numberOfStates];
memcpy(next_state_index_list, state_indices_list, numberOfStates * 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 = 0; i <= numberOfStates; i++) {
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;
}
}
// Now we can dispose of the auxiliary array.
delete[] next_state_index_list;
}
//! Destructor
@ -79,10 +83,10 @@ public:
* Destructor. Frees the internal storage.
*/
~BackwardTransitions() {
if (this->predecessor_list != NULL) {
if (this->predecessor_list != nullptr) {
delete[] this->predecessor_list;
}
if (this->state_indices_list != NULL) {
if (this->state_indices_list != nullptr) {
delete[] this->state_indices_list;
}
}
@ -96,7 +100,6 @@ public:
return this->predecessor_list + this->state_indices_list[state];
}
/*!
* Returns an iterator referring to the element after the predecessors of
* the given state.

18
src/models/dtmc.h

@ -38,9 +38,8 @@ public:
* @param state_labeling The labeling that assigns a set of atomic
* propositions to each state.
*/
Dtmc(mrmc::sparse::StaticSparseMatrix<T>* probability_matrix,
mrmc::models::AtomicPropositionsLabeling* state_labeling) :
backward_transitions(probability_matrix) {
Dtmc(mrmc::sparse::StaticSparseMatrix<T>* probability_matrix, mrmc::models::AtomicPropositionsLabeling* state_labeling)
: backward_transitions(probability_matrix) {
this->probability_matrix = probability_matrix;
this->state_labeling = state_labeling;
}
@ -55,6 +54,19 @@ public:
pantheios::log_DEBUG("Copy constructor of DTMC invoked.");
}
//! Destructor
/*!
* Destructor. Frees the matrix and labeling associated with this DTMC.
*/
~Dtmc() {
if (this->probability_matrix != nullptr) {
delete this->probability_matrix;
}
if (this->state_labeling != nullptr) {
delete this->state_labeling;
}
}
/*!
* Returns the state space size of the DTMC.
* @return The size of the state space of the DTMC.

10
src/mrmc-cpp.cpp

@ -42,12 +42,12 @@ int main(const int argc, const char* argv[]) {
try
{
s = mrmc::settings::Settings::instance(argc, argv, NULL);
s = mrmc::settings::Settings::instance(argc, argv, nullptr);
}
catch (mrmc::exceptions::InvalidSettings)
{
std::cout << "Could not recover from settings error, terminating." << std::endl << std::endl;
std::cout << mrmc::settings::help << std::endl;
std::cout << "Could not recover from settings error, terminating." << std::endl;
delete s;
return 1;
}
@ -66,7 +66,11 @@ int main(const int argc, const char* argv[]) {
mrmc::models::AtomicPropositionsLabeling* labeling = mrmc::parser::read_lab_file(probMatrix->getRowCount(), s->getString("labfile").c_str());
mrmc::models::Dtmc<double> dtmc(probMatrix, labeling);
dtmc.printModelInformationToStream(std::cout);
if (s != nullptr) {
delete s;
}
return 0;
}

12
src/parser/read_lab_file.cpp

@ -19,15 +19,20 @@
#include <pantheios/pantheios.hpp>
#include <pantheios/inserters/integer.hpp>
#include <iostream>
#ifdef WIN32
# define STRTOK_FUNC strtok_s
#else
# define STRTOK_FUNC strtok_r
#endif
// Only disable the warning if we are not using GCC, because
// GCC does not know this pragma and raises a warning
#ifndef __GNUG__
// Disable C4996 - This function or variable may be unsafe.
#pragma warning(disable:4996)
#endif
namespace mrmc {
@ -150,7 +155,7 @@ mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const c
while (fgets(s, BUFFER_SIZE, P)) {
char * token = NULL;
uint_fast32_t node = 0;
unsigned int node = 0;
/* First token has to be a number identifying the node,
* hence it is treated differently from the other tokens.
*/
@ -167,9 +172,8 @@ mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const c
if (token == NULL) {
break;
}
result->addAtomicPropositionToState(token, node);
result->addAtomicPropositionToState(token, static_cast<uint_fast64_t>(node));
} while (token != NULL);
}
fclose(P);

21
src/parser/read_tra_file.cpp

@ -26,8 +26,12 @@ namespace mrmc {
namespace parser{
// Only disable the warning if we are not using GCC, because
// GCC does not know this pragma and raises a warning
#ifndef __GNUG__
// Disable C4996 - This function or variable may be unsafe.
#pragma warning(disable:4996)
#endif
/*!
* This method does the first pass through the .tra file and computes
@ -46,7 +50,7 @@ static uint_fast32_t make_first_pass(FILE* p) {
throw exceptions::file_IO_exception ("make_first_pass: File not readable (this should be checked before calling this function!)");
}
char s[BUFFER_SIZE]; //String buffer
uint_fast32_t rows=0, non_zero=0;
int rows=0, non_zero=0;
//Reading No. of states
if (fgets(s, BUFFER_SIZE, p) != NULL) {
@ -69,7 +73,7 @@ static uint_fast32_t make_first_pass(FILE* p) {
//And increase number of transitions
while (NULL != fgets( s, BUFFER_SIZE, p ))
{
uint_fast32_t row=0, col=0;
int row=0, col=0;
double val=0.0;
if (sscanf( s, "%d%d%lf", &row, &col, &val ) != 3) {
(void)fclose(p);
@ -80,7 +84,7 @@ static uint_fast32_t make_first_pass(FILE* p) {
--non_zero;
}
}
return non_zero;
return static_cast<uint_fast64_t>(non_zero);
}
@ -95,7 +99,8 @@ static uint_fast32_t make_first_pass(FILE* p) {
sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
FILE *p = NULL;
char s[BUFFER_SIZE];
uint_fast32_t rows, non_zero;
uint_fast64_t non_zero = 0;
int rows = 0;
sparse::StaticSparseMatrix<double> *sp = NULL;
p = fopen(filename, "r");
@ -121,7 +126,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
* 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;
int nnz = 0;
if ((fgets(s, BUFFER_SIZE, p) == NULL) || (sscanf(s, "TRANSITIONS %d", &nnz) == 0)) {
(void)fclose(p);
throw mrmc::exceptions::wrong_file_format();
@ -135,7 +140,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 + 1);
sp = new sparse::StaticSparseMatrix<double>(static_cast<uint_fast64_t>(rows) + 1);
if ( NULL == sp ) {
throw std::bad_alloc();
return NULL;
@ -144,7 +149,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
//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;
int row=0, col=0;
double val = 0.0;
if (sscanf(s, "%d%d%lf", &row, &col, &val) != 3) {
(void)fclose(p);
@ -158,7 +163,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
" to position ",
pantheios::integer(row), " x ",
pantheios::integer(col));
sp->addNextValue(row,col,val);
sp->addNextValue(static_cast<uint_fast64_t>(row),static_cast<uint_fast64_t>(col),static_cast<uint_fast64_t>(val));
}
(void)fclose(p);

2
src/reward/reward_model.h

@ -27,7 +27,7 @@ class RewardModel {
typedef const DataClass& crDataClass;
public:
RewardModel(const uint_fast32_t state_count, const DataClass& null_value) : null_value(null_value), state_count(state_count) {
RewardModel(const uint_fast32_t state_count, const DataClass& null_value) : state_count(state_count), null_value(null_value) {
this->reward_vector = new VectorImpl<DataClass, std::allocator<DataClass>>(this->state_count);
// init everything to zero

10
src/sparse/static_sparse_matrix.h

@ -56,11 +56,7 @@ public:
* @param rows The number of rows of the matrix
*/
StaticSparseMatrix(uint_fast64_t rows)
: internalStatus(MatrixStatus::UnInitialized),
currentSize(0), lastRow(0), valueStorage(nullptr),
diagonalStorage(nullptr), columnIndications(nullptr),
rowIndications(nullptr), rowCount(rows), nonZeroEntryCount(0) { }
: rowCount(rows), nonZeroEntryCount(0), valueStorage(nullptr), diagonalStorage(nullptr), columnIndications(nullptr), rowIndications(nullptr), internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { }
//! Copy Constructor
/*!
* Copy Constructor. Performs a deep copy of the given sparse matrix.
@ -322,7 +318,7 @@ public:
// Fill in the missing entries in the row_indications array.
// (Can happen because of empty rows at the end.)
if (lastRow != rowCount) {
for (uint_fast64_t i = lastRow + 1; i <= rowCount; ++i) {
for (uint_fast64_t i = lastRow + 1; i < rowCount; ++i) {
rowIndications[i] = currentSize;
}
}
@ -331,7 +327,7 @@ public:
// array. This eases iteration work, as now the indices of row i
// are always between row_indications[i] and row_indications[i + 1],
// also for the first and last row.
rowIndications[rowCount + 1] = nonZeroEntryCount;
rowIndications[rowCount] = nonZeroEntryCount;
setState(MatrixStatus::ReadReady);
}

103
src/vector/bitvector.h

@ -13,6 +13,8 @@
#include "src/exceptions/invalid_argument.h"
#include "src/exceptions/out_of_range.h"
#include <iostream>
namespace mrmc {
namespace vector {
@ -23,14 +25,39 @@ namespace vector {
Does NOT perform index bound checks!
*/
class BitVector {
public:
class constIndexIterator {
constIndexIterator(uint_fast64_t* bucketPtr, uint_fast64_t* endBucketPtr) : bucketPtr(bucketPtr), endBucketPtr(endBucketPtr), offset(0), currentBitInByte(0) { }
constIndexIterator& operator++() {
do {
uint_fast64_t remainingInBucket = *bucketPtr >> ++currentBitInByte;
if (remainingInBucket != 0) {
while ((remainingInBucket & 1) == 0) {
remainingInBucket >>= 1;
++currentBitInByte;
}
}
offset <<= 6; ++bucketPtr; currentBitInByte = 0;
} while (bucketPtr != endBucketPtr);
return *this;
}
uint_fast64_t operator*() { return offset + currentBitInByte; }
bool operator!=(constIndexIterator& rhs) { return bucketPtr != rhs.bucketPtr; }
private:
uint_fast64_t* bucketPtr;
uint_fast64_t* endBucketPtr;
uint_fast64_t offset;
uint_fast8_t currentBitInByte;
};
public:
//! Constructor
/*!
\param initial_length The initial size of the boolean Array. Can be changed later on via BitVector::resize()
*/
BitVector(uint_fast64_t initial_length) {
bucket_count = initial_length / 64;
if (initial_length % 64 != 0) {
bucket_count = initial_length >> 6;
if ((initial_length & mod64mask) != 0) {
++bucket_count;
}
bucket_array = new uint_fast64_t[bucket_count]();
@ -46,11 +73,12 @@ class BitVector {
Copy Constructor. Creates an exact copy of the source bit vector bv. Modification of either bit vector does not affect the other.
@param bv A reference to the bit vector that should be copied from
*/
BitVector(const BitVector &bv) : bucket_count(bv.bucket_count)
{
BitVector(const BitVector &bv) :
bucket_count(bv.bucket_count) {
pantheios::log_DEBUG("BitVector::CopyCTor: Using Copy() Ctor.");
bucket_array = new uint_fast64_t[bucket_count]();
memcpy(bucket_array, bv.bucket_array, sizeof(uint_fast64_t) * bucket_count);
memcpy(bucket_array, bv.bucket_array,
sizeof(uint_fast64_t) * bucket_count);
}
~BitVector() {
@ -63,11 +91,13 @@ class BitVector {
uint_fast64_t* tempArray = new uint_fast64_t[new_length]();
// 64 bit/entries per uint_fast64_t
uint_fast64_t copySize = (new_length <= (bucket_count * 64)) ? (new_length/64) : (bucket_count);
uint_fast64_t copySize =
(new_length <= (bucket_count << 6)) ?
(new_length >> 6) : (bucket_count);
memcpy(tempArray, bucket_array, sizeof(uint_fast64_t) * copySize);
bucket_count = new_length / 64;
if (new_length % 64 != 0) {
bucket_count = new_length >> 6;
if ((new_length & mod64mask) != 0) {
++bucket_count;
}
@ -76,12 +106,12 @@ class BitVector {
}
void set(const uint_fast64_t index, const bool value) {
uint_fast64_t bucket = index / 64;
uint_fast64_t bucket = index >> 6;
// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one.
// MSVC: C4334, use 1i64 or cast to __int64.
// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?)
uint_fast64_t mask = 1;
mask = mask << (index % 64);
mask = mask << (index & mod64mask);
if (value) {
bucket_array[bucket] |= mask;
} else {
@ -90,19 +120,21 @@ class BitVector {
}
bool get(const uint_fast64_t index) {
uint_fast64_t bucket = index / 64;
uint_fast64_t bucket = index >> 6;
// Taking the step with mask is crucial as we NEED a 64bit shift, not a 32bit one.
// MSVC: C4334, use 1i64 or cast to __int64.
// result of 32-bit shift implicitly converted to 64 bits (was 64-bit shift intended?)
uint_fast64_t mask = 1;
mask = mask << (index % 64);
mask = mask << (index & mod64mask);
return ((bucket_array[bucket] & mask) == mask);
}
// Operators
BitVector operator &(BitVector const &bv) {
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count;
BitVector result(minSize * 64);
uint_fast64_t minSize =
(bv.bucket_count < this->bucket_count) ?
bv.bucket_count : this->bucket_count;
BitVector result(minSize << 6);
for (uint_fast64_t i = 0; i < minSize; ++i) {
result.bucket_array[i] = this->bucket_array[i] & bv.bucket_array[i];
}
@ -110,8 +142,10 @@ class BitVector {
return result;
}
BitVector operator |(BitVector const &bv) {
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count;
BitVector result(minSize * 64);
uint_fast64_t minSize =
(bv.bucket_count < this->bucket_count) ?
bv.bucket_count : this->bucket_count;
BitVector result(minSize << 6);
for (uint_fast64_t i = 0; i < minSize; ++i) {
result.bucket_array[i] = this->bucket_array[i] | bv.bucket_array[i];
}
@ -120,8 +154,10 @@ class BitVector {
}
BitVector operator ^(BitVector const &bv) {
uint_fast64_t minSize = (bv.bucket_count < this->bucket_count) ? bv.bucket_count : this->bucket_count;
BitVector result(minSize * 64);
uint_fast64_t minSize =
(bv.bucket_count < this->bucket_count) ?
bv.bucket_count : this->bucket_count;
BitVector result(minSize << 6);
for (uint_fast64_t i = 0; i < minSize; ++i) {
result.bucket_array[i] = this->bucket_array[i] ^ bv.bucket_array[i];
}
@ -130,7 +166,7 @@ class BitVector {
}
BitVector operator ~() {
BitVector result(this->bucket_count * 64);
BitVector result(this->bucket_count << 6);
for (uint_fast64_t i = 0; i < this->bucket_count; ++i) {
result.bucket_array[i] = ~this->bucket_array[i];
}
@ -138,15 +174,30 @@ class BitVector {
return result;
}
BitVector implies(BitVector& other) {
if (other.getSize() != this->getSize()) {
pantheios::log_ERROR(
"BitVector::implies: Throwing invalid argument exception for connecting bit vectors of different size.");
throw mrmc::exceptions::invalid_argument();
}
BitVector result(this->bucket_count << 6);
for (uint_fast64_t i = 0; i < this->bucket_count; ++i) {
result.bucket_array[i] = ~this->bucket_array[i]
| other.bucket_array[i];
}
return result;
}
/*!
* Returns the number of bits that are set (to one) in this bit vector.
* @return The number of bits that are set (to one) in this bit vector.
*/
uint_fast64_t getNumberOfSetBits() {
uint_fast64_t set_bits = 0;
for (uint_fast64_t i = 0; i < bucket_count; i++) {
for (uint_fast64_t i = 0; i < bucket_count; ++i) {
#ifdef __GNUG__ // check if we are using g++ and use built-in function if available
set_bits += __builtin_popcount (this->bucket_array[i]);
set_bits += __builtin_popcountll(this->bucket_array[i]);
#else
uint_fast32_t cnt;
uint_fast64_t bitset = this->bucket_array[i];
@ -159,6 +210,10 @@ class BitVector {
return set_bits;
}
uint_fast64_t getSize() {
return bucket_count;
}
/*!
* Returns the size of the bit vector in memory measured in bytes.
* @return The size of the bit vector in memory measured in bytes.
@ -167,12 +222,14 @@ class BitVector {
return sizeof(*this) + sizeof(uint_fast64_t) * bucket_count;
}
private:
private:
uint_fast64_t bucket_count;
/*! Array containing the boolean bits for each node, 64bits/64nodes per element */
uint_fast64_t* bucket_array;
static const uint_fast64_t mod64mask = (1 << 6) - 1;
};
} // namespace vector

Loading…
Cancel
Save