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

Refactoring of labeling classes.

main
dehnert 13 years ago
parent
44fbef62bd
commit
b7618fd91a
5 changed files with 243 additions and 165 deletions
Unified View
  1. 209
      src/models/atomic_propositions_labeling.h
  2. 52
      src/models/dtmc.h
  3. 61
      src/models/single_atomic_proposition_labeling.h
  4. 4
      src/parser/read_lab_file.cpp
  5. 76
      test/parser/read_lab_file_test.cpp

209
src/models/atomic_propositions_labeling.h
View File

@ -11,7 +11,7 @@
#include <pantheios/pantheios.hpp> #include <pantheios/pantheios.hpp>
#include <pantheios/inserters/integer.hpp> #include <pantheios/inserters/integer.hpp>
#include <iostream> #include <ostream>
#include "single_atomic_proposition_labeling.h" #include "single_atomic_proposition_labeling.h"
@ -51,115 +51,131 @@ class AtomicPropositionsLabeling {
public: public:
/*! Constructor creating an object of class labeling. //! Constructor
* @param nodeCount The number of nodes; necessary for class AtomicProposition. /*!
* @param propositionCount The number of atomic propositions. * 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, AtomicPropositionsLabeling(const uint_fast32_t state_count,
const uint_fast32_t propositionCount) { const uint_fast32_t ap_count) {
// add one for 1-bound indices // add one for 1-bound indices
node_count = nodeCount + 1; this->state_count = state_count + 1;
proposition_count = propositionCount; this->ap_count = ap_count;
propositions_current = 0; this->aps_current = 0;
propositions = new SingleAtomicPropositionLabeling*[proposition_count]; this->single_labelings = new SingleAtomicPropositionLabeling*[ap_count];
for (uint_fast32_t i = 0; i < proposition_count; ++i) { for (uint_fast32_t i = 0; i < ap_count; ++i) {
propositions[i] = new SingleAtomicPropositionLabeling(node_count); this->single_labelings[i] = new SingleAtomicPropositionLabeling(state_count);
} }
} }
//! Copy Constructor //! 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) : AtomicPropositionsLabeling(const AtomicPropositionsLabeling& atomic_propositions_labeling) :
node_count(atomic_propositions_labeling.node_count), proposition_count( state_count(atomic_propositions_labeling.state_count),
atomic_propositions_labeling.proposition_count), propositions_current( ap_count(atomic_propositions_labeling.ap_count),
atomic_propositions_labeling.propositions_current), proposition_map( aps_current(atomic_propositions_labeling.aps_current),
atomic_propositions_labeling.proposition_map) { name_to_labeling_map(atomic_propositions_labeling.name_to_labeling_map) {
propositions = new SingleAtomicPropositionLabeling*[proposition_count]; this->single_labelings = new SingleAtomicPropositionLabeling*[ap_count];
for (uint_fast32_t i = 0; i < proposition_count; ++i) { for (uint_fast32_t i = 0; i < ap_count; ++i) {
propositions[i] = new SingleAtomicPropositionLabeling( this->single_labelings[i] = new SingleAtomicPropositionLabeling(
*atomic_propositions_labeling.propositions[i]); *atomic_propositions_labeling.single_labelings[i]);
} }
} }
//! Destructor
/*
* Destructor. Needs to take care of deleting all single labelings.
*/
virtual ~AtomicPropositionsLabeling() { virtual ~AtomicPropositionsLabeling() {
//deleting all the labeling vectors in the map. // delete all the single atomic proposition labelings in the map
MAP<std::string, SingleAtomicPropositionLabeling*>::iterator it; MAP<std::string, SingleAtomicPropositionLabeling*>::iterator it;
for (uint_fast32_t i = 0; i < proposition_count; ++i) { for (uint_fast32_t i = 0; i < ap_count; ++i) {
delete propositions[i]; delete this->single_labelings[i];
propositions[i] = NULL; this->single_labelings[i] = NULL;
} }
delete[] propositions; delete[] this->single_labelings;
propositions = NULL; this->single_labelings = NULL;
} }
/*! Registers the name of a proposition. /*!
* Will throw an error if more propositions are added than were initialized, * Registers the name of a proposition.
* or if a proposition is registered twice. * Will throw an error if more atomic propositions are added than were
* @param proposition The name of the proposition to add. * 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. * @return The index of the new proposition.
*/ */
uint_fast32_t addProposition(std::string proposition) { uint_fast32_t addAtomicProposition(std::string ap) {
if (proposition_map.count(proposition) != 0) { if (name_to_labeling_map.count(ap) != 0) {
throw std::out_of_range("Proposition does already exist."); throw std::out_of_range("Atomic Proposition already exists.");
} }
if (propositions_current >= proposition_count) { if (aps_current >= ap_count) {
throw std::out_of_range("Added more propositions than initialized for"); 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++; uint_fast32_t returnValue = aps_current++;
//pantheios::log_INFO("returning ", pantheios::integer(returnValue), " for position ");
return returnValue; 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. * @return True if the proposition was added to the labeling, false otherwise.
*/ */
bool containsProposition(std::string proposition) { bool containsAtomicProposition(std::string proposition) {
return (proposition_map.count(proposition) != 0); return (name_to_labeling_map.count(proposition) != 0);
} }
/*! Labels a node with an atomic proposition. /*!
* @param proposition The name of the proposition * Adds an atomic proposition to a given state.
* @param node The index of the node to label * @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) { void addAtomicPropositionToState(std::string ap, const uint_fast32_t state_index) {
//TODO (Thomas Heinemann): Differentiate exceptions? if (name_to_labeling_map.count(ap) == 0) {
if (proposition_map.count(proposition) == 0) { throw std::out_of_range("Atomic Proposition '" + ap + "' unknown.");
throw std::out_of_range("Proposition does not exist.");
} }
if (node >= node_count) { if (state_index >= state_count) {
throw std::out_of_range("Node number out of range"); 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 * Checks whether a given state is labeled with the given atomic proposition.
* @param node The index of the node * @param ap The name of the atomic proposition.
* @return True if the node is labeled with the proposition, false otherwise. * @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) { bool stateHasAtomicProposition(std::string ap,
return propositions[proposition_map[proposition]]->hasNodeLabel(node); 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() { 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 * Returns the labeling of states associated with the given atomic proposition.
* respective atomic proposition. * @param ap The name of the atomic proposition.
* @param proposition The name of the proposition. * @return A pointer to an instance of SingleAtomicPropositionLabeling that
* @return A pointer to the atomic_proposition object of the proposition. * represents the labeling of the states with the given atomic proposition.
*/ */
SingleAtomicPropositionLabeling* getAtomicProposition(std::string proposition) { SingleAtomicPropositionLabeling* getAtomicProposition(std::string ap) {
return (propositions[proposition_map[proposition]]); return (this->single_labelings[name_to_labeling_map[ap]]);
} }
/*! /*!
@ -168,28 +184,59 @@ public:
*/ */
uint_fast64_t getSizeInMemory() { uint_fast64_t getSizeInMemory() {
uint_fast64_t size = sizeof(*this); uint_fast64_t size = sizeof(*this);
for (uint_fast32_t i = 0; i < proposition_count; i++) { // add sizes of all single labelings
size += propositions[i]->getSizeInMemory(); // count sizes of bit vectors for (uint_fast32_t i = 0; i < ap_count; i++) {
size += this->single_labelings[i]->getSizeInMemory();
} }
return size; return size;
} }
void printAtomicPropositionsInformation() { /*!
std::cout << "Atomic Propositions: \t" << this->getNumberOfAtomicPropositions() << std::endl; * Prints information about the labeling to the specified stream.
for(auto ap : this->proposition_map) { * @param out The stream the information is to be printed to.
std::cout << "\t * " << ap.first << " -> " << propositions[ap.second]->getNumberOfLabeledStates(); */
std::cout << " state(s)" << std::endl; 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: private:
uint_fast32_t node_count, proposition_count, propositions_current; /*! The number of states whose labels are to be stored by this object. */
MAP<std::string, uint_fast32_t> proposition_map; uint_fast32_t state_count;
SingleAtomicPropositionLabeling** propositions; /*! 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<std::string, uint_fast32_t> 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_ */ #endif /* MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_ */

52
src/models/dtmc.h
View File

@ -11,7 +11,7 @@
#include <pantheios/pantheios.hpp> #include <pantheios/pantheios.hpp>
#include <pantheios/inserters/integer.hpp> #include <pantheios/inserters/integer.hpp>
#include <iostream> #include <ostream>
#include "atomic_propositions_labeling.h" #include "atomic_propositions_labeling.h"
#include "src/sparse/static_sparse_matrix.h" #include "src/sparse/static_sparse_matrix.h"
@ -30,9 +30,12 @@ class Dtmc {
public: public:
//! Constructor //! Constructor
/*! /*!
* Constructs a DTMC object from the given transition probability matrix and the given labeling of the states. * Constructs a DTMC object from the given transition probability matrix and
\param probability_matrix The transition probability function of the DTMC given by a matrix. * the given labeling of the states.
\param state_labeling The labeling that assigns a set of atomic propositions to each state. * \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<T>* probability_matrix, Dtmc(mrmc::sparse::StaticSparseMatrix<T>* probability_matrix,
mrmc::models::AtomicPropositionsLabeling* state_labeling) { mrmc::models::AtomicPropositionsLabeling* state_labeling) {
@ -42,10 +45,11 @@ public:
//! Copy Constructor //! Copy Constructor
/*! /*!
Copy Constructor. Performs a deep copy of the given DTMC. * 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<T> &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) {
pantheios::log_DEBUG("Copy constructor of DTMC invoked."); pantheios::log_DEBUG("Copy constructor of DTMC invoked.");
} }
@ -66,23 +70,33 @@ public:
} }
/*! /*!
* Returns a pointer to the matrix representing the transition probability function. * Returns a pointer to the matrix representing the transition probability
* @return A pointer to the matrix representing the transition probability function. * function.
* @return A pointer to the matrix representing the transition probability
* function.
*/ */
mrmc::sparse::StaticSparseMatrix<T>* getTransitionProbabilityMatrix() { mrmc::sparse::StaticSparseMatrix<T>* getTransitionProbabilityMatrix() {
return this->probability_matrix; return this->probability_matrix;
} }
void printModelInformation() { /*!
std::cout << "------------------------------------------------------- " << std::endl; * Prints information about the model to the specified stream.
std::cout << "Model type: \t\tDTMC" << std::endl; * @param out The stream the information is to be printed to.
std::cout << "States: \t\t" << this->getStateSpaceSize() << std::endl; */
std::cout << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl; void printModelInformationToStream(std::ostream& out) {
this->state_labeling->printAtomicPropositionsInformation(); out << "-------------------------------------------------------------- "
std::cout << "Size in memory: \t" << (this->probability_matrix->getSizeInMemory() + << 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() + this->state_labeling->getSizeInMemory() +
sizeof(*this))/1024 << " kbytes" << std::endl; sizeof(*this))/1024 << " kbytes" << std::endl;
std::cout << "------------------------------------------------------- " << std::endl; out << "-------------------------------------------------------------- "
<< std::endl;
} }
private: private:
@ -95,8 +109,8 @@ private:
}; };
} //namespace models } // namespace models
} //namespace mrmc } // namespace mrmc
#endif /* DTMC_H_ */ #endif /* DTMC_H_ */

61
src/models/single_atomic_proposition_labeling.h
View File

@ -8,57 +8,74 @@ namespace mrmc {
namespace models { namespace models {
/*! /*!
* This class represents the labeling of a state space with a single atomic proposition. * This class represents the labeling of a state space with a single atomic
* Internally, this is done by keeping a dense bit vector such that the i-th bit * proposition.
* in the vector is set to true if and only if the i-th state satisfies the
* atomic proposition
*/ */
class SingleAtomicPropositionLabeling { class SingleAtomicPropositionLabeling {
public: public:
//! Constructor //! 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 // intentionally left empty
} }
//! Copy Constructor //! 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 // intentionally left empty
} }
~SingleAtomicPropositionLabeling() { /*!
// intentionally left empty * Checks whether the given state possesses the label.
} * @param state_index The index of the state to check.
*/
bool hasNodeLabel(uint_fast32_t nodeId) { bool hasLabel(uint_fast32_t state_index) {
return nodes.get(nodeId); 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() { 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. * Returns the size of the single atomic proposition labeling in memory
* @return The size of the single atomic proposition labeling in memory measured in bytes. * measured in bytes.
* @return The size of the single atomic proposition labeling in memory
* measured in bytes.
*/ */
uint_fast64_t getSizeInMemory() { uint_fast64_t getSizeInMemory() {
return sizeof(*this) + nodes.getSizeInMemory(); return sizeof(*this) + label_vector.getSizeInMemory();
} }
private: 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 } // namespace models

4
src/parser/read_lab_file.cpp
View File

@ -131,7 +131,7 @@ mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const c
for (proposition = STRTOK_FUNC(decl_buffer, sep, &saveptr); for (proposition = STRTOK_FUNC(decl_buffer, sep, &saveptr);
proposition != NULL; proposition != NULL;
proposition = STRTOK_FUNC(NULL, sep, &saveptr)) { proposition = STRTOK_FUNC(NULL, sep, &saveptr)) {
result -> addProposition(proposition); result -> addAtomicProposition(proposition);
} }
// Free decl_buffer // Free decl_buffer
@ -167,7 +167,7 @@ mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const c
if (token == NULL) { if (token == NULL) {
break; break;
} }
result->addLabelToNode(token, node); result->addAtomicPropositionToState(token, node);
} while (token != NULL); } while (token != NULL);
} }

76
test/parser/read_lab_file_test.cpp
View File

@ -29,50 +29,50 @@ TEST(ReadLabFileTest, ParseTest) {
char phi[] = "phi", psi[] = "psi", smth[] = "smth"; char phi[] = "phi", psi[] = "psi", smth[] = "smth";
if (labeling != NULL) { if (labeling != NULL) {
ASSERT_TRUE(labeling->containsProposition(phi)); ASSERT_TRUE(labeling->containsAtomicProposition(phi));
ASSERT_TRUE(labeling->containsProposition(psi)); ASSERT_TRUE(labeling->containsAtomicProposition(psi));
ASSERT_TRUE(labeling->containsProposition(smth)); ASSERT_TRUE(labeling->containsAtomicProposition(smth));
//Testing whether all and only the correct nodes are labeled with "phi" //Testing whether all and only the correct nodes are labeled with "phi"
ASSERT_TRUE(labeling->nodeHasProposition(phi,1)); ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,1));
ASSERT_TRUE(labeling->nodeHasProposition(phi,2)); ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,2));
ASSERT_TRUE(labeling->nodeHasProposition(phi,3)); ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,3));
ASSERT_TRUE(labeling->nodeHasProposition(phi,5)); ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,5));
ASSERT_TRUE(labeling->nodeHasProposition(phi,7)); ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,7));
ASSERT_TRUE(labeling->nodeHasProposition(phi,9)); ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,9));
ASSERT_TRUE(labeling->nodeHasProposition(phi,10)); ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,10));
ASSERT_TRUE(labeling->nodeHasProposition(phi,11)); ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,11));
ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,4));
ASSERT_FALSE(labeling->nodeHasProposition(phi,4)); ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,6));
ASSERT_FALSE(labeling->nodeHasProposition(phi,6));
//Testing whether all and only the correct nodes are labeled with "psi" //Testing whether all and only the correct nodes are labeled with "psi"
ASSERT_TRUE(labeling->nodeHasProposition(psi,6)); ASSERT_TRUE(labeling->stateHasAtomicProposition(psi,6));
ASSERT_TRUE(labeling->nodeHasProposition(psi,7)); ASSERT_TRUE(labeling->stateHasAtomicProposition(psi,7));
ASSERT_TRUE(labeling->nodeHasProposition(psi,8)); ASSERT_TRUE(labeling->stateHasAtomicProposition(psi,8));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,1));
ASSERT_FALSE(labeling->nodeHasProposition(psi,1)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,2));
ASSERT_FALSE(labeling->nodeHasProposition(psi,2)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,3));
ASSERT_FALSE(labeling->nodeHasProposition(psi,3)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,4));
ASSERT_FALSE(labeling->nodeHasProposition(psi,4)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,5));
ASSERT_FALSE(labeling->nodeHasProposition(psi,5)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,9));
ASSERT_FALSE(labeling->nodeHasProposition(psi,9)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,10));
ASSERT_FALSE(labeling->nodeHasProposition(psi,10)); ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,11));
ASSERT_FALSE(labeling->nodeHasProposition(psi,11));
//Testing whether all and only the correct nodes are labeled with "smth" //Testing whether all and only the correct nodes are labeled with "smth"
ASSERT_TRUE(labeling->nodeHasProposition(smth,4)); ASSERT_TRUE(labeling->stateHasAtomicProposition(smth,4));
ASSERT_TRUE(labeling->nodeHasProposition(smth,5)); ASSERT_TRUE(labeling->stateHasAtomicProposition(smth,5));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,1));
ASSERT_FALSE(labeling->nodeHasProposition(smth,1)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,2));
ASSERT_FALSE(labeling->nodeHasProposition(smth,2)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,3));
ASSERT_FALSE(labeling->nodeHasProposition(smth,3)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,6));
ASSERT_FALSE(labeling->nodeHasProposition(smth,6)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,7));
ASSERT_FALSE(labeling->nodeHasProposition(smth,7)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,8));
ASSERT_FALSE(labeling->nodeHasProposition(smth,8)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,9));
ASSERT_FALSE(labeling->nodeHasProposition(smth,9)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,10));
ASSERT_FALSE(labeling->nodeHasProposition(smth,10)); ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,11));
ASSERT_FALSE(labeling->nodeHasProposition(smth,11));
//Deleting the labeling //Deleting the labeling
delete labeling; delete labeling;

Write Preview
|||||||
100:0
Loading…
Cancel
Save