Browse Source

- Comments

- Support for std::unordered_map
- CMakeList.txt: enable C++11 for gcc; debug symbols only when Debug
version is created.
tempestpy_adaptions
Thomas Heinemann 12 years ago
committed by Lanchid
parent
commit
da8ed67224
  1. 8
      CMakeLists.txt
  2. 27
      src/dtmc/atomic_proposition.h
  3. 54
      src/dtmc/labeling.h
  4. 6
      src/parser/read_lab_file.cpp
  5. 6
      src/parser/read_tra_file.cpp

8
CMakeLists.txt

@ -7,9 +7,13 @@ set (MRMC_CPP_VERSION_MAJOR 1)
set (MRMC_CPP_VERSION_MINOR 0)
#Configurations for GCC
if(CMAKE_COMPILER_IS_GNUCC)
if(CMAKE_COMPILER_IS_GNUCC)
#Using C++11
set (CMAKE_CXX_FLAGS "-std=c++0x")
#Debug symbols
set (CMAKE_CXX_FLAGS "-g")
set (CMAKE_CXX_FLAGS_DEBUG "-g")
endif()
# configure a header file to pass some of the CMake settings

27
src/dtmc/atomic_proposition.h

@ -25,21 +25,19 @@ namespace dtmc {
class AtomicProposition {
public:
/*! Default Constructor
* Creates an uninitialized object
* Useful for array construction, afterwards, the initialize function has to be called.
*/
AtomicProposition() {
}
//! Constructor
/*!
\param nodeCount Amount of nodes that the DTMC has to label
*/
AtomicProposition(uint_fast32_t nodeCount) {
node_array = NULL;
initialize(nodeCount);
if (node_array == NULL) {
node_count = nodeCount;
int n = (int) std::ceil(nodeCount / 64.0);
node_array = new uint_fast64_t[n];
//Initialization with 0 is crucial!
memset(node_array, 0, n*sizeof(uint_fast64_t));
}
}
~AtomicProposition() {
@ -48,17 +46,6 @@ class AtomicProposition {
}
}
void initialize(uint_fast32_t nodeCount) {
if (node_array == NULL) {
node_count = nodeCount;
int n = (int) std::ceil(nodeCount / 64.0);
node_array = new uint_fast64_t[n];
//Initialization with 0 is crucial!
memset(node_array, 0, n*sizeof(uint_fast64_t));
}
}
bool hasNodeLabel(uint_fast32_t nodeId) {
int bucket = static_cast<int>(std::floor(nodeId / 64));
int bucket_place = nodeId % 64;

54
src/dtmc/labeling.h

@ -11,17 +11,23 @@
#include "atomic_proposition.h"
#define USE_STD_UNORDERED_MAP
/* Map types: By default, the boost hash map is used.
* When the macro DEFAULT_MAP is defined, the default C++ class (std::map)
* If the macro USE_STD_MAP is defined, the default C++ class (std::map)
* is used instead.
*/
#ifdef DEFAULT_MAP
#include <map>
#define MAP std::map
#ifdef USE_STD_MAP
# include <map>
# define MAP std::map
#else
#include "boost/unordered_map.hpp"
#define MAP boost::unordered_map
# ifdef USE_STD_UNORDERED_MAP
# include <unordered_map>
# define MAP std::unordered_map
# else
# include "boost/unordered_map.hpp"
# define MAP boost::unordered_map
# endif
#endif
#include <stdexcept>
@ -33,11 +39,17 @@ namespace mrmc {
namespace dtmc {
/*! This class manages the objects of class atomic_proposition. Access is possible with the
* string identifiers which are used in the input.
*/
class labeling {
public:
/*! Constructor creating an object of 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,
const uint_fast32_t propositionCount) {
node_count = nodeCount;
@ -60,6 +72,12 @@ class labeling {
propositions = NULL;
}
/*! Registers the name of a proposition.
* Will throw an error if more propositions are added than were initialized,
* or if a proposition is registered twice.
* @param proposition The name of the proposition to add.
* @return The index of the new proposition.
*/
uint_fast32_t addProposition(std::string proposition) {
if (proposition_map.count(proposition) != 0) {
throw std::out_of_range("Proposition does already exist.");
@ -74,11 +92,17 @@ class labeling {
return returnValue;
}
/*! Checks whether the name of a proposition is already registered with the labeling.
* @return True if the proposition was added to the labeling, false otherwise.
*/
bool containsProposition(std::string proposition) {
return (proposition_map.count(proposition) != 0);
}
/*! Labels a node with an atomic proposition.
* @param proposition The name of the proposition
* @param node The index of the node to label
*/
void addLabelToNode(std::string proposition, const uint_fast32_t node) {
//TODO (Thomas Heinemann): Differentiate exceptions?
if (proposition_map.count(proposition) == 0) {
@ -90,14 +114,28 @@ class labeling {
propositions[proposition_map[proposition]]->addLabelToNode(node);
}
/*! Checks whether a node is labeled with a proposition.
* @param proposition The name of the proposition
* @param node The index of the node
* @return True if the node is labeled with the proposition, false otherwise.
*/
bool nodeHasProposition(std::string proposition, const uint_fast32_t node) {
return propositions[proposition_map[proposition]]->hasNodeLabel(node);
}
/*! Returns the number of propositions managed by this object (which was set in the initialization)
* @return The number of propositions.
*/
uint_fast32_t getNumberOfPropositions() {
return proposition_count;
}
/*! This function provides direct access to an atomic_proposition class object
* by its string identifier. This object manages the nodes that are labeled with the
* respective atomic proposition.
* @param proposition The name of the proposition.
* @return A pointer to the atomic_proposition object of the proposition.
*/
AtomicProposition* getProposition(std::string proposition) {
return (propositions[proposition_map[proposition]]);
}

6
src/parser/read_lab_file.cpp

@ -32,10 +32,12 @@ namespace parser {
/*!
* Reads a .lab file and puts the result in a labelling structure.
* Reads a .lab file and puts the result in a labeling structure.
*
* Labelings created with this method have to be freed with the delete operator.
* @param node_count the number of states.
* @param filename input .lab file's name.
* @return returns a pointer to a labelling object.
* @return The pointer to the created labeling object.
*/
mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
{

6
src/parser/read_tra_file.cpp

@ -86,8 +86,10 @@ static uint_fast32_t make_first_pass(FILE* p) {
/*!Reads a .tra file and produces a sparse matrix representing the described Markov Chain.
* @param *filename input .tra file's name.
* @return a pointer to a sparse matrix.
*
* Matrices created with this method have to be freed with the delete operator.
* @param filename input .tra file's name.
* @return a pointer to the created sparse matrix.
*/
sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {

Loading…
Cancel
Save