Browse Source

Renamed dtmc folder to models, corrected namespace in contained classes and fixed includes in affected files.

Added DTMC class stub.
tempestpy_adaptions
dehnert 12 years ago
parent
commit
b7eaeab11f
  1. 16
      src/models/atomic_proposition.h
  2. 57
      src/models/dtmc.h
  3. 21
      src/models/labeling.h
  4. 4
      src/parser/read_lab_file.cpp
  5. 4
      src/parser/read_lab_file.h
  6. 6
      src/vector/bitvector.h
  7. 4
      test/parser/read_lab_file_test.cpp

16
src/dtmc/atomic_proposition.h → src/models/atomic_proposition.h

@ -13,7 +13,7 @@
namespace mrmc {
namespace dtmc {
namespace models {
//! An atomic proposition for DTMCs with a constant number of nodes
/*!
@ -27,11 +27,19 @@ class AtomicProposition {
\param nodeCount Amount of nodes that the DTMC has to label
*/
AtomicProposition(uint_fast32_t nodeCount) : nodes(nodeCount) {
//
// intentionally left empty
}
//! Copy Constructor
/*!
* Copy constructor. Performs a deep copy of this AtomicProposition object.
*/
AtomicProposition(const AtomicProposition& atomic_proposition) : nodes(atomic_proposition.nodes) {
// intentionally left empty
}
~AtomicProposition() {
//
// intentionally left empty
}
bool hasNodeLabel(uint_fast32_t nodeId) {
@ -47,7 +55,7 @@ class AtomicProposition {
mrmc::vector::BitVector nodes;
};
} // namespace dtmc
} // namespace models
} // namespace mrmc

57
src/models/dtmc.h

@ -0,0 +1,57 @@
/*
* dtmc.h
*
* Created on: 14.11.2012
* Author: Christian Dehnert
*/
#ifndef DTMC_H_
#define DTMC_H_
#include "labeling.h"
#include "src/sparse/static_sparse_matrix.h"
namespace mrmc {
namespace models {
/*! This class represents a discrete-time Markov chain (DTMC) whose states are
* labeled with atomic propositions.
*/
class Dtmc {
public:
//! Constructor
/*!
\param probability_matrix The transition probability function of the DTMC given by a matrix.
\param state_labeling The labeling that assigns a set of atomic propositions to each state.
*/
Dtmc(mrmc::sparse::StaticSparseMatrix* probability_matrix,
mrmc::models::Labeling* state_labeling) {
this->probability_matrix = probability_matrix;
this->state_labeling = state_labeling;
}
//! Copy Constructor
/*!
Copy Constructor. Creates an exact copy of the source DTMC. Modification of either DTMC does not affect the other.
@param dtmc A reference to the matrix that should be copied from
*/
Dtmc(const Dtmc &dtmc) : probability_matrix(dtmc.probability_matrix), state_labeling(dtmc.state_labeling) {
// intentionally left empty
}
private:
mrmc::sparse::StaticSparseMatrix* probability_matrix;
mrmc::models::Labeling* state_labeling;
};
} //namespace models
} //namespace mrmc
#endif /* DTMC_H_ */

21
src/dtmc/labeling.h → src/models/labeling.h

@ -37,12 +37,12 @@
namespace mrmc {
namespace dtmc {
namespace models {
/*! This class manages the objects of class atomic_proposition. Access is possible with the
* string identifiers which are used in the input.
*/
class labeling {
class Labeling {
public:
@ -50,7 +50,7 @@ class labeling {
* @param nodeCount The number of nodes; necessary for class AtomicProposition.
* @param propositionCount The number of atomic propositions.
*/
labeling(const uint_fast32_t nodeCount,
Labeling(const uint_fast32_t nodeCount,
const uint_fast32_t propositionCount) {
node_count = nodeCount;
proposition_count = propositionCount;
@ -61,7 +61,18 @@ class labeling {
}
}
virtual ~labeling() {
//! Copy Constructor
/*! Copy Constructor. Performs a deep copy of this Labeling object.
*
*/
Labeling(const Labeling& labeling) : node_count(labeling.node_count), proposition_count(labeling.proposition_count), propositions_current(labeling.propositions_current), proposition_map(labeling.proposition_map) {
propositions = new AtomicProposition*[proposition_count];
for (uint_fast32_t i = 0; i < proposition_count; ++i) {
propositions[i] = new AtomicProposition(*labeling.propositions[i]);
}
}
virtual ~Labeling() {
//deleting all the labeling vectors in the map.
MAP<std::string, AtomicProposition*>::iterator it;
for (uint_fast32_t i = 0; i < proposition_count; ++i) {
@ -146,7 +157,7 @@ class labeling {
AtomicProposition** propositions;
};
} //namespace dtmc
} //namespace models
} //namespace mrmc

4
src/parser/read_lab_file.cpp

@ -42,7 +42,7 @@ namespace parser {
* @param filename input .lab file's name.
* @return The pointer to the created labeling object.
*/
mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
mrmc::models::Labeling * read_lab_file(int node_count, const char * filename)
{
/* Note that this function uses strtok_r on char-array s.
* This function will modify this string.
@ -125,7 +125,7 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
pos++;
}
mrmc::dtmc::labeling* result = new mrmc::dtmc::labeling(node_count, proposition_count);
mrmc::models::Labeling* result = new mrmc::models::Labeling(node_count, proposition_count);
//Here, all propositions are to be declared...
for (proposition = STRTOK_FUNC(decl_buffer, sep, &saveptr);

4
src/parser/read_lab_file.h

@ -8,14 +8,14 @@
#ifndef READ_LAB_FILE_H_
#define READ_LAB_FILE_H_
#include "src/dtmc/labeling.h"
#include "src/models/labeling.h"
namespace mrmc {
namespace parser {
mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename);
mrmc::models::Labeling * read_lab_file(int node_count, const char * filename);
}
}

6
src/vector/bitvector.h

@ -26,7 +26,7 @@ class BitVector {
public:
//! Constructor
/*!
\param initial_length The initial size of the boolean Array. Can be changed later on via @resize()
\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;
@ -43,8 +43,8 @@ class BitVector {
//! Copy Constructor
/*!
Copy Constructor. Creates an exact copy of the source sparse matrix ssm. Modification of either matrix does not affect the other.
@param ssm A reference to the matrix that should be copied from
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)
{

4
test/parser/read_lab_file_test.cpp

@ -7,7 +7,7 @@
#include "gtest/gtest.h"
#include "MRMCConfig.h"
#include "src/dtmc/labeling.h"
#include "src/models/labeling.h"
#include "src/parser/read_lab_file.h"
#include "src/exceptions/file_IO_exception.h"
#include "src/exceptions/wrong_file_format.h"
@ -19,7 +19,7 @@ TEST(ReadLabFileTest, NonExistingFileTest) {
TEST(ReadLabFileTest, ParseTest) {
//This test is based on a test case from the original MRMC.
mrmc::dtmc::labeling* labeling = NULL;
mrmc::models::Labeling* labeling = NULL;
//Parsing the file
ASSERT_NO_THROW(labeling = mrmc::parser::read_lab_file(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));

Loading…
Cancel
Save