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

Renamed classes for atomic proposition labeling storage. 

Added some methods to DTMC class stub.
tempestpy_adaptions
dehnert 12 years ago
parent
88101ef238
commit
c33dfac505
8 changed files with 271 additions and 238 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. 62
      src/models/atomic_proposition.h
  2. 169
      src/models/atomic_propositions_labeling.h
  3. 45
      src/models/dtmc.h
  4. 164
      src/models/labeling.h
  5. 56
      src/models/single_atomic_proposition_labeling.h
  6. 4
      src/parser/read_lab_file.cpp
  7. 5
      src/parser/read_lab_file.h
  8. 4
      test/parser/read_lab_file_test.cpp

62
src/models/atomic_proposition.h
View File

@ -1,62 +0,0 @@
#ifndef MRMC_DTMC_ATOMIC_PROPOSITION_H_
#define MRMC_DTMC_ATOMIC_PROPOSITION_H_
#include <exception>
#include <cmath>
#include "boost/integer/integer_mask.hpp"
#include <pantheios/pantheios.hpp>
#include <pantheios/inserters/integer.hpp>
#include "src/vector/bitvector.h"
namespace mrmc {
namespace models {
//! An atomic proposition for DTMCs with a constant number of nodes
/*!
A dense vector representing a single atomic proposition for all nodes of a DTMC.
*/
class AtomicProposition {
public:
//! Constructor
/*!
\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) {
return nodes.get(nodeId);
}
void addLabelToNode(uint_fast32_t nodeId) {
nodes.set(nodeId, true);
}
private:
/*! BitVector containing the boolean bits for each node */
mrmc::vector::BitVector nodes;
};
} // namespace models
} // namespace mrmc
#endif // MRMC_DTMC_ATOMIC_PROPOSITION_H_

169
src/models/atomic_propositions_labeling.h
View File

@ -0,0 +1,169 @@
/*
* labeling.h
*
* Created on: 10.09.2012
* Author: Thomas Heinemann
*/
#ifndef MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_
#define MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_
#include "single_atomic_proposition_labeling.h"
#define USE_STD_UNORDERED_MAP
/* Map types: By default, the boost hash map is used.
* If the macro USE_STD_MAP is defined, the default C++ class (std::map)
* is used instead.
*/
#ifdef USE_STD_MAP
# include <map>
# define MAP std::map
#else
# 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>
#include <pantheios/pantheios.hpp>
#include <pantheios/inserters/integer.hpp>
namespace mrmc {
namespace models {
/*!
* This class manages the labeling of the state space with a fixed number of
* atomic propositions.
*/
class AtomicPropositionsLabeling {
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.
*/
AtomicPropositionsLabeling(const uint_fast32_t nodeCount,
const uint_fast32_t propositionCount) {
node_count = nodeCount;
proposition_count = propositionCount;
propositions_current = 0;
propositions = new SingleAtomicPropositionLabeling*[proposition_count];
for (uint_fast32_t i = 0; i < proposition_count; ++i) {
propositions[i] = new SingleAtomicPropositionLabeling(node_count);
}
}
//! Copy Constructor
/*! Copy Constructor. Performs a deep copy of this Labeling object.
*
*/
AtomicPropositionsLabeling(const AtomicPropositionsLabeling& atomic_propositions_labeling) :
node_count(atomic_propositions_labeling.node_count), proposition_count(
atomic_propositions_labeling.proposition_count), propositions_current(
atomic_propositions_labeling.propositions_current), proposition_map(
atomic_propositions_labeling.proposition_map) {
propositions = new SingleAtomicPropositionLabeling*[proposition_count];
for (uint_fast32_t i = 0; i < proposition_count; ++i) {
propositions[i] = new SingleAtomicPropositionLabeling(
*atomic_propositions_labeling.propositions[i]);
}
}
virtual ~AtomicPropositionsLabeling() {
//deleting all the labeling vectors in the map.
MAP<std::string, SingleAtomicPropositionLabeling*>::iterator it;
for (uint_fast32_t i = 0; i < proposition_count; ++i) {
delete propositions[i];
propositions[i] = NULL;
}
delete[] propositions;
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.");
}
if (propositions_current >= proposition_count) {
throw std::out_of_range("Added more propositions than initialized for");
}
proposition_map[proposition] = propositions_current;
uint_fast32_t returnValue = propositions_current++;
//pantheios::log_INFO("returning ", pantheios::integer(returnValue), " for position ");
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) {
throw std::out_of_range("Proposition does not exist.");
}
if (node >= node_count) {
throw std::out_of_range("Node number out of range");
}
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.
*/
SingleAtomicPropositionLabeling* getProposition(std::string proposition) {
return (propositions[proposition_map[proposition]]);
}
private:
uint_fast32_t node_count, proposition_count, propositions_current;
MAP<std::string, uint_fast32_t> proposition_map;
SingleAtomicPropositionLabeling** propositions;
};
} //namespace models
} //namespace mrmc
#endif /* MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_ */

45
src/models/dtmc.h
View File

@ -8,6 +8,9 @@
#ifndef DTMC_H_ #ifndef DTMC_H_
#define DTMC_H_ #define DTMC_H_
#include <pantheios/pantheios.hpp>
#include <pantheios/inserters/integer.hpp>
#include "labeling.h" #include "labeling.h"
#include "src/sparse/static_sparse_matrix.h" #include "src/sparse/static_sparse_matrix.h"
@ -18,33 +21,63 @@ namespace models {
/*! This class represents a discrete-time Markov chain (DTMC) whose states are /*! This class represents a discrete-time Markov chain (DTMC) whose states are
* labeled with atomic propositions. * labeled with atomic propositions.
*/ */
template <class T>
class Dtmc { class Dtmc {
public: public:
//! Constructor //! Constructor
/*! /*!
* Constructs a DTMC object from the given transition probability matrix and the given labeling of the states.
\param probability_matrix The transition probability function of the DTMC given by a matrix. \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. \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) {
Dtmc(mrmc::sparse::StaticSparseMatrix<T>* probability_matrix,
mrmc::models::AtomicPropositionsLabeling* state_labeling) {
pantheios::log_DEBUG("Creating a DTMC ");
this->probability_matrix = probability_matrix; this->probability_matrix = probability_matrix;
this->state_labeling = state_labeling; this->state_labeling = state_labeling;
} }
//! Copy Constructor //! Copy Constructor
/*! /*!
Copy Constructor. Creates an exact copy of the source DTMC. Modification of either DTMC does not affect the other.
Copy Constructor. Performs a deep copy of the given DTMC.
@param dtmc A reference to the DTMC that is to be copied. @param dtmc A reference to the DTMC that is to be copied.
*/ */
Dtmc(const Dtmc &dtmc) : probability_matrix(dtmc.probability_matrix), state_labeling(dtmc.state_labeling) {
Dtmc(const Dtmc<T> &dtmc) : probability_matrix(dtmc.probability_matrix), state_labeling(dtmc.state_labeling) {
// intentionally left empty // intentionally left empty
} }
/*!
* Returns the state space size of the DTMC.
* @return The size of the state space of the DTMC.
*/
uint_fast64_t getStateSpaceSize() {
return this->probability_matrix->getRowCount();
}
/*!
* Returns the number of (non-zero) transitions of the DTMC.
* @return The number of (non-zero) transitions of the DTMC.
*/
uint_fast64_t getNumberOfTransitions() {
return this->probability_matrix->getNonZeroEntryCount();
}
/*!
* Returns a pointer to the matrix representing the transition probability function.
* @return A pointer to the matrix representing the transition probability function.
*/
mrmc::sparse::StaticSparseMatrix<T>* getTransitionProbabilityMatrix() {
return this->probability_matrix;
}
private: private:
mrmc::sparse::StaticSparseMatrix* probability_matrix;
mrmc::models::Labeling* state_labeling;
/*! A matrix representing the transition probability function of the DTMC. */
mrmc::sparse::StaticSparseMatrix<T>* probability_matrix;
/*! The labeling of the states of the DTMC. */
mrmc::models::AtomicPropositionsLabeling* state_labeling;
}; };

164
src/models/labeling.h
View File

@ -1,164 +0,0 @@
/*
* labeling.h
*
* Created on: 10.09.2012
* Author: Thomas Heinemann
*/
#ifndef MRMC_DTMC_LABELING_H_
#define MRMC_DTMC_LABELING_H_
#include "atomic_proposition.h"
#define USE_STD_UNORDERED_MAP
/* Map types: By default, the boost hash map is used.
* If the macro USE_STD_MAP is defined, the default C++ class (std::map)
* is used instead.
*/
#ifdef USE_STD_MAP
# include <map>
# define MAP std::map
#else
# 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>
#include <pantheios/pantheios.hpp>
#include <pantheios/inserters/integer.hpp>
namespace mrmc {
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 {
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;
proposition_count = propositionCount;
propositions_current = 0;
propositions = new AtomicProposition*[proposition_count];
for (uint_fast32_t i = 0; i < proposition_count; ++i) {
propositions[i] = new AtomicProposition(node_count);
}
}
//! 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) {
delete propositions[i];
propositions[i] = NULL;
}
delete[] propositions;
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.");
}
if (propositions_current >= proposition_count) {
throw std::out_of_range("Added more propositions than initialized for");
}
proposition_map[proposition] = propositions_current;
uint_fast32_t returnValue = propositions_current++;
//pantheios::log_INFO("returning ", pantheios::integer(returnValue), " for position ");
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) {
throw std::out_of_range("Proposition does not exist.");
}
if (node >= node_count) {
throw std::out_of_range("Node number out of range");
}
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]]);
}
private:
uint_fast32_t node_count, proposition_count, propositions_current;
MAP<std::string, uint_fast32_t> proposition_map;
AtomicProposition** propositions;
};
} //namespace models
} //namespace mrmc
#endif /* MRMC_DTMC_LABELING_H_ */

56
src/models/single_atomic_proposition_labeling.h
View File

@ -0,0 +1,56 @@
#ifndef MRMC_MODELS_SINGLE_ATOMIC_PROPOSITION_LABELING_H_
#define MRMC_MODELS_SINGLE_ATOMIC_PROPOSITION_LABELING_H_
#include "src/vector/bitvector.h"
namespace mrmc {
namespace models {
/*!
* This class represents the labeling of a state space with a single atomic proposition.
* Internally, this is done by keeping a dense bit vector such that the i-th bit
* in the vector is set to true if and only if the i-th state satisfies the
* atomic proposition
*/
class SingleAtomicPropositionLabeling {
public:
//! Constructor
/*!
\param nodeCount Amount of nodes that the DTMC has to label
*/
SingleAtomicPropositionLabeling(uint_fast32_t nodeCount) : nodes(nodeCount) {
// intentionally left empty
}
//! Copy Constructor
/*!
* Copy constructor. Performs a deep copy of this AtomicProposition object.
*/
SingleAtomicPropositionLabeling(const SingleAtomicPropositionLabeling& single_atomic_proposition_labeling) : nodes(single_atomic_proposition_labeling.nodes) {
// intentionally left empty
}
~SingleAtomicPropositionLabeling() {
// intentionally left empty
}
bool hasNodeLabel(uint_fast32_t nodeId) {
return nodes.get(nodeId);
}
void addLabelToNode(uint_fast32_t nodeId) {
nodes.set(nodeId, true);
}
private:
/*! BitVector containing the boolean bits for each node */
mrmc::vector::BitVector nodes;
};
} // namespace models
} // namespace mrmc
#endif // MRMC_MODELS_SINGLE_ATOMIC_PROPOSITION_LABELING_H_

4
src/parser/read_lab_file.cpp
View File

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

5
src/parser/read_lab_file.h
View File

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

4
test/parser/read_lab_file_test.cpp
View File

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

Write Preview
Loading…
Cancel
Save