diff --git a/src/models/atomic_propositions_labeling.h b/src/models/atomic_propositions_labeling.h index 78dfe9f5e..3d7bfadb6 100644 --- a/src/models/atomic_propositions_labeling.h +++ b/src/models/atomic_propositions_labeling.h @@ -11,7 +11,7 @@ #include #include -#include +#include #include "single_atomic_proposition_labeling.h" @@ -51,115 +51,131 @@ 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. + //! Constructor + /*! + * Constructs an empty atomic propositions labeling for the given number + * of states and amount of atomic propositions. + * @param state_count The number of states of the model. + * @param ap_count The number of atomic propositions. */ - AtomicPropositionsLabeling(const uint_fast32_t nodeCount, - const uint_fast32_t propositionCount) { + AtomicPropositionsLabeling(const uint_fast32_t state_count, + const uint_fast32_t ap_count) { // add one for 1-bound indices - node_count = nodeCount + 1; - 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); + this->state_count = state_count + 1; + this->ap_count = ap_count; + this->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); } } //! Copy Constructor - /*! Copy Constructor. Performs a deep copy of this Labeling object. - * + /*! + * Copy Constructor. Performs a deep copy of the given atomic proposition + * labeling. */ 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]); + 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( + *atomic_propositions_labeling.single_labelings[i]); } } + //! Destructor + /* + * Destructor. Needs to take care of deleting all single labelings. + */ virtual ~AtomicPropositionsLabeling() { - //deleting all the labeling vectors in the map. + // delete all the single atomic proposition labelings in the map MAP::iterator it; - for (uint_fast32_t i = 0; i < proposition_count; ++i) { - delete propositions[i]; - propositions[i] = NULL; + for (uint_fast32_t i = 0; i < ap_count; ++i) { + delete this->single_labelings[i]; + this->single_labelings[i] = NULL; } - delete[] propositions; - propositions = NULL; + delete[] this->single_labelings; + this->single_labelings = 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. + /*! + * Registers the name of a proposition. + * Will throw an error if more atomic propositions are added than were + * originally declared or if an atomic proposition is registered twice. + * @param ap The name of the atomic 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."); + uint_fast32_t addAtomicProposition(std::string ap) { + if (name_to_labeling_map.count(ap) != 0) { + throw std::out_of_range("Atomic Proposition already exists."); } - if (propositions_current >= proposition_count) { - throw std::out_of_range("Added more propositions than initialized for"); + if (aps_current >= ap_count) { + throw std::out_of_range("Added more atomic propositions than" + "previously declared."); } - proposition_map[proposition] = propositions_current; + name_to_labeling_map[ap] = aps_current; - uint_fast32_t returnValue = propositions_current++; - //pantheios::log_INFO("returning ", pantheios::integer(returnValue), " for position "); + uint_fast32_t returnValue = aps_current++; return returnValue; } - /*! Checks whether the name of a proposition is already registered with the labeling. + /*! + * Checks whether the name of an atomic proposition is already registered + * within this labeling. * @return True if the proposition was added to the labeling, false otherwise. */ - bool containsProposition(std::string proposition) { - return (proposition_map.count(proposition) != 0); + bool containsAtomicProposition(std::string proposition) { + return (name_to_labeling_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 + /*! + * Adds an atomic proposition to a given state. + * @param ap The name of the atomic proposition. + * @param node The index of the state 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."); + void addAtomicPropositionToState(std::string ap, const uint_fast32_t state_index) { + if (name_to_labeling_map.count(ap) == 0) { + throw std::out_of_range("Atomic Proposition '" + ap + "' unknown."); } - if (node >= node_count) { - throw std::out_of_range("Node number out of range"); + if (state_index >= state_count) { + throw std::out_of_range("State index out of range."); } - propositions[proposition_map[proposition]]->addLabelToNode(node); + this->single_labelings[name_to_labeling_map[ap]]->addLabelToState(state_index); } - /*! 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. + /*! + * Checks whether a given state is labeled with the given atomic proposition. + * @param ap The name of the atomic proposition. + * @param state_index The index of the state to check. + * @return True if the node is labeled with the atomic proposition, false + * otherwise. */ - bool nodeHasProposition(std::string proposition, const uint_fast32_t node) { - return propositions[proposition_map[proposition]]->hasNodeLabel(node); + bool stateHasAtomicProposition(std::string ap, + const uint_fast32_t state_index) { + return this->single_labelings[name_to_labeling_map[ap]]->hasLabel(state_index); } - /*! Returns the number of propositions managed by this object (which was set in the initialization) - * @return The number of propositions. + /*! + * Returns the number of atomic propositions managed by this object (set in + * the initialization). + * @return The number of atomic propositions. */ uint_fast32_t getNumberOfAtomicPropositions() { - return proposition_count; + return ap_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. + /*! + * Returns the labeling of states associated with the given atomic proposition. + * @param ap The name of the atomic proposition. + * @return A pointer to an instance of SingleAtomicPropositionLabeling that + * represents the labeling of the states with the given atomic proposition. */ - SingleAtomicPropositionLabeling* getAtomicProposition(std::string proposition) { - return (propositions[proposition_map[proposition]]); + SingleAtomicPropositionLabeling* getAtomicProposition(std::string ap) { + return (this->single_labelings[name_to_labeling_map[ap]]); } /*! @@ -168,28 +184,59 @@ public: */ uint_fast64_t getSizeInMemory() { uint_fast64_t size = sizeof(*this); - for (uint_fast32_t i = 0; i < proposition_count; i++) { - size += propositions[i]->getSizeInMemory(); // count sizes of bit vectors + // add sizes of all single labelings + for (uint_fast32_t i = 0; i < ap_count; i++) { + size += this->single_labelings[i]->getSizeInMemory(); } return size; } - void printAtomicPropositionsInformation() { - std::cout << "Atomic Propositions: \t" << this->getNumberOfAtomicPropositions() << std::endl; - for(auto ap : this->proposition_map) { - std::cout << "\t * " << ap.first << " -> " << propositions[ap.second]->getNumberOfLabeledStates(); - std::cout << " state(s)" << std::endl; + /*! + * Prints information about the labeling to the specified stream. + * @param out The stream the information is to be printed to. + */ + void printAtomicPropositionsInformationToStream(std::ostream& out) { + out << "Atomic Propositions: \t" << this->getNumberOfAtomicPropositions() + << std::endl; + for(auto ap : this->name_to_labeling_map) { + out << "\t * " << ap.first << " -> " + << this->single_labelings[ap.second]->getNumberOfLabeledStates(); + out << " state(s)" << std::endl; } } private: - uint_fast32_t node_count, proposition_count, propositions_current; - MAP proposition_map; - SingleAtomicPropositionLabeling** propositions; + + /*! The number of states whose labels are to be stored by this object. */ + uint_fast32_t state_count; + + /*! The number of different atomic propositions this object can store. */ + uint_fast32_t ap_count; + + /*! + * The number of different atomic propositions currently associated with + * this labeling. Used to prevent too many atomic propositions from being + * added to this object. + */ + uint_fast32_t aps_current; + + /*! + * Associates a name of an atomic proposition to its corresponding labeling + * by mapping the name to a specific index in the array of all + * individual labelings. + */ + MAP name_to_labeling_map; + + /*! + * Stores all individual labelings. To find the labeling associated with + * a particular atomic proposition, the map from names to indices in this + * array has to be used. + */ + SingleAtomicPropositionLabeling** single_labelings; }; -} //namespace models +} // namespace models -} //namespace mrmc +} // namespace mrmc #endif /* MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_ */ diff --git a/src/models/dtmc.h b/src/models/dtmc.h index 46a715cdc..9fd939a71 100644 --- a/src/models/dtmc.h +++ b/src/models/dtmc.h @@ -11,7 +11,7 @@ #include #include -#include +#include #include "atomic_propositions_labeling.h" #include "src/sparse/static_sparse_matrix.h" @@ -30,10 +30,13 @@ class Dtmc { public: //! 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 state_labeling The labeling that assigns a set of atomic propositions to each state. - */ + * 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 state_labeling The labeling that assigns a set of atomic + * propositions to each state. + */ Dtmc(mrmc::sparse::StaticSparseMatrix* probability_matrix, mrmc::models::AtomicPropositionsLabeling* state_labeling) { this->probability_matrix = probability_matrix; @@ -42,10 +45,11 @@ public: //! Copy Constructor /*! - Copy Constructor. Performs a deep copy of the given DTMC. - @param dtmc A reference to the DTMC that is to be copied. + * Copy Constructor. Performs a deep copy of the given DTMC. + * @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 &dtmc) : probability_matrix(dtmc.probability_matrix), + state_labeling(dtmc.state_labeling) { pantheios::log_DEBUG("Copy constructor of DTMC invoked."); } @@ -66,23 +70,33 @@ public: } /*! - * Returns a pointer to the matrix representing the transition probability function. - * @return A pointer to the matrix representing the transition probability function. + * 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* getTransitionProbabilityMatrix() { return this->probability_matrix; } - void printModelInformation() { - std::cout << "------------------------------------------------------- " << std::endl; - std::cout << "Model type: \t\tDTMC" << std::endl; - std::cout << "States: \t\t" << this->getStateSpaceSize() << std::endl; - std::cout << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; - this->state_labeling->printAtomicPropositionsInformation(); - std::cout << "Size in memory: \t" << (this->probability_matrix->getSizeInMemory() + - this->state_labeling->getSizeInMemory() + - sizeof(*this))/1024 << " kbytes" << std::endl; - std::cout << "------------------------------------------------------- " << std::endl; + /*! + * Prints information about the model to the specified stream. + * @param out The stream the information is to be printed to. + */ + void printModelInformationToStream(std::ostream& out) { + out << "-------------------------------------------------------------- " + << std::endl; + out << "Model type: \t\tDTMC" << std::endl; + out << "States: \t\t" << this->getStateSpaceSize() << std::endl; + out << "Transitions: \t\t" << this->getNumberOfTransitions() + << std::endl; + this->state_labeling->printAtomicPropositionsInformationToStream(out); + out << "Size in memory: \t" + << (this->probability_matrix->getSizeInMemory() + + this->state_labeling->getSizeInMemory() + + sizeof(*this))/1024 << " kbytes" << std::endl; + out << "-------------------------------------------------------------- " + << std::endl; } private: @@ -95,8 +109,8 @@ private: }; -} //namespace models +} // namespace models -} //namespace mrmc +} // namespace mrmc #endif /* DTMC_H_ */ diff --git a/src/models/single_atomic_proposition_labeling.h b/src/models/single_atomic_proposition_labeling.h index ebd384727..cef601856 100644 --- a/src/models/single_atomic_proposition_labeling.h +++ b/src/models/single_atomic_proposition_labeling.h @@ -8,57 +8,74 @@ 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 + * This class represents the labeling of a state space with a single atomic + * proposition. */ class SingleAtomicPropositionLabeling { public: //! Constructor /*! - \param nodeCount Amount of nodes that the DTMC has to label + * Constructs a labeling for the given number of states. + * @param state_count Amount of states for which this objects manages the + * labeling with one particular atomic proposition. */ - SingleAtomicPropositionLabeling(uint_fast32_t nodeCount) : nodes(nodeCount) { + SingleAtomicPropositionLabeling(uint_fast32_t state_count) : label_vector(state_count) { // intentionally left empty } //! Copy Constructor /*! - * Copy constructor. Performs a deep copy of this AtomicProposition object. + * Copy constructor. Performs a deep copy of the given + * SingleAtomicPropositionLabeling object. + * @param single_atomic_proposition_labeling The object to copy. */ - SingleAtomicPropositionLabeling(const SingleAtomicPropositionLabeling& single_atomic_proposition_labeling) : nodes(single_atomic_proposition_labeling.nodes) { + SingleAtomicPropositionLabeling(const SingleAtomicPropositionLabeling& single_atomic_proposition_labeling) + : label_vector(single_atomic_proposition_labeling.label_vector) { // intentionally left empty } - ~SingleAtomicPropositionLabeling() { - // intentionally left empty - } - - bool hasNodeLabel(uint_fast32_t nodeId) { - return nodes.get(nodeId); + /*! + * Checks whether the given state possesses the label. + * @param state_index The index of the state to check. + */ + bool hasLabel(uint_fast32_t state_index) { + return label_vector.get(state_index); } - void addLabelToNode(uint_fast32_t nodeId) { - nodes.set(nodeId, true); + /*! + * Adds the label to the given state. + * @param state_index The index of the state to label. + */ + void addLabelToState(uint_fast32_t state_index) { + label_vector.set(state_index, true); } + /*! + * Returns the number of states that are labeled. + * @return The number of states that are labeled. + */ uint_fast64_t getNumberOfLabeledStates() { - return nodes.getNumberOfSetBits(); + return label_vector.getNumberOfSetBits(); } /*! - * Returns the size of the single atomic proposition labeling in memory measured in bytes. - * @return The size of the single atomic proposition labeling in memory measured in bytes. + * Returns the size of the single atomic proposition labeling in memory + * measured in bytes. + * @return The size of the single atomic proposition labeling in memory + * measured in bytes. */ uint_fast64_t getSizeInMemory() { - return sizeof(*this) + nodes.getSizeInMemory(); + return sizeof(*this) + label_vector.getSizeInMemory(); } private: - /*! BitVector containing the boolean bits for each node */ - mrmc::vector::BitVector nodes; + + /*! + * A bit vector storing for every state whether or not that state is + * labeled. + */ + mrmc::vector::BitVector label_vector; }; } // namespace models diff --git a/src/parser/read_lab_file.cpp b/src/parser/read_lab_file.cpp index 45aa31929..2a3742afe 100644 --- a/src/parser/read_lab_file.cpp +++ b/src/parser/read_lab_file.cpp @@ -131,7 +131,7 @@ mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const c for (proposition = STRTOK_FUNC(decl_buffer, sep, &saveptr); proposition != NULL; proposition = STRTOK_FUNC(NULL, sep, &saveptr)) { - result -> addProposition(proposition); + result -> addAtomicProposition(proposition); } // Free decl_buffer @@ -167,7 +167,7 @@ mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const c if (token == NULL) { break; } - result->addLabelToNode(token, node); + result->addAtomicPropositionToState(token, node); } while (token != NULL); } diff --git a/test/parser/read_lab_file_test.cpp b/test/parser/read_lab_file_test.cpp index 789f853cf..7a273a35d 100644 --- a/test/parser/read_lab_file_test.cpp +++ b/test/parser/read_lab_file_test.cpp @@ -29,50 +29,50 @@ TEST(ReadLabFileTest, ParseTest) { char phi[] = "phi", psi[] = "psi", smth[] = "smth"; if (labeling != NULL) { - ASSERT_TRUE(labeling->containsProposition(phi)); - ASSERT_TRUE(labeling->containsProposition(psi)); - ASSERT_TRUE(labeling->containsProposition(smth)); + ASSERT_TRUE(labeling->containsAtomicProposition(phi)); + ASSERT_TRUE(labeling->containsAtomicProposition(psi)); + ASSERT_TRUE(labeling->containsAtomicProposition(smth)); //Testing whether all and only the correct nodes are labeled with "phi" - ASSERT_TRUE(labeling->nodeHasProposition(phi,1)); - ASSERT_TRUE(labeling->nodeHasProposition(phi,2)); - ASSERT_TRUE(labeling->nodeHasProposition(phi,3)); - ASSERT_TRUE(labeling->nodeHasProposition(phi,5)); - ASSERT_TRUE(labeling->nodeHasProposition(phi,7)); - ASSERT_TRUE(labeling->nodeHasProposition(phi,9)); - ASSERT_TRUE(labeling->nodeHasProposition(phi,10)); - ASSERT_TRUE(labeling->nodeHasProposition(phi,11)); - - ASSERT_FALSE(labeling->nodeHasProposition(phi,4)); - ASSERT_FALSE(labeling->nodeHasProposition(phi,6)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,1)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,2)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,3)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,5)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,7)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,9)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,10)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,11)); + + ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,4)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,6)); //Testing whether all and only the correct nodes are labeled with "psi" - ASSERT_TRUE(labeling->nodeHasProposition(psi,6)); - ASSERT_TRUE(labeling->nodeHasProposition(psi,7)); - ASSERT_TRUE(labeling->nodeHasProposition(psi,8)); - - ASSERT_FALSE(labeling->nodeHasProposition(psi,1)); - ASSERT_FALSE(labeling->nodeHasProposition(psi,2)); - ASSERT_FALSE(labeling->nodeHasProposition(psi,3)); - ASSERT_FALSE(labeling->nodeHasProposition(psi,4)); - ASSERT_FALSE(labeling->nodeHasProposition(psi,5)); - ASSERT_FALSE(labeling->nodeHasProposition(psi,9)); - ASSERT_FALSE(labeling->nodeHasProposition(psi,10)); - ASSERT_FALSE(labeling->nodeHasProposition(psi,11)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(psi,6)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(psi,7)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(psi,8)); + + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,1)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,2)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,3)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,4)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,5)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,9)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,10)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,11)); //Testing whether all and only the correct nodes are labeled with "smth" - ASSERT_TRUE(labeling->nodeHasProposition(smth,4)); - ASSERT_TRUE(labeling->nodeHasProposition(smth,5)); - - ASSERT_FALSE(labeling->nodeHasProposition(smth,1)); - ASSERT_FALSE(labeling->nodeHasProposition(smth,2)); - ASSERT_FALSE(labeling->nodeHasProposition(smth,3)); - ASSERT_FALSE(labeling->nodeHasProposition(smth,6)); - ASSERT_FALSE(labeling->nodeHasProposition(smth,7)); - ASSERT_FALSE(labeling->nodeHasProposition(smth,8)); - ASSERT_FALSE(labeling->nodeHasProposition(smth,9)); - ASSERT_FALSE(labeling->nodeHasProposition(smth,10)); - ASSERT_FALSE(labeling->nodeHasProposition(smth,11)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(smth,4)); + ASSERT_TRUE(labeling->stateHasAtomicProposition(smth,5)); + + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,1)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,2)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,3)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,6)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,7)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,8)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,9)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,10)); + ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,11)); //Deleting the labeling delete labeling;