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

Adapted the labeling class such that no raw arrays are included any more, but a vector instead.

main
dehnert 12 years ago
parent
cec71c9632
commit
f899914799
4 changed files with 95 additions and 109 deletions
Unified View
  1. 6
      src/modelchecker/AbstractModelChecker.h
  2. 2
      src/models/AbstractModel.h
  3. 120
      src/models/AtomicPropositionsLabeling.h
  4. 76
      test/parser/ReadLabFileTest.cpp

6
src/modelchecker/AbstractModelChecker.h
View File

@ -131,7 +131,7 @@ public:
result = stateFormula.check(*this); result = stateFormula.check(*this);
LOG4CPLUS_INFO(logger, "Result for initial states:"); LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl; std::cout << "Result for initial states:" << std::endl;
for (auto initialState : *model.getLabeledStates("init")) { for (auto initialState : model.getLabeledStates("init")) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied")); LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl; std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl;
} }
@ -162,7 +162,7 @@ public:
result = this->checkNoBoundOperator(noBoundFormula); result = this->checkNoBoundOperator(noBoundFormula);
LOG4CPLUS_INFO(logger, "Result for initial states:"); LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl; std::cout << "Result for initial states:" << std::endl;
for (auto initialState : *model.getLabeledStates("init")) { for (auto initialState : model.getLabeledStates("init")) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]); LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl; std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
} }
@ -195,7 +195,7 @@ public:
throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid."; throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
} }
return new storm::storage::BitVector(*model.getLabeledStates(formula.getAp())); return new storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
} }
/*! /*!

2
src/models/AbstractModel.h
View File

@ -108,7 +108,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
* @return A bit vector in which exactly those bits are set to true that * @return A bit vector in which exactly those bits are set to true that
* correspond to a state labeled with the given atomic proposition. * correspond to a state labeled with the given atomic proposition.
*/ */
storm::storage::BitVector* getLabeledStates(std::string ap) const { storm::storage::BitVector const& getLabeledStates(std::string const& ap) const {
return stateLabeling->getAtomicProposition(ap); return stateLabeling->getAtomicProposition(ap);
} }

120
src/models/AtomicPropositionsLabeling.h
View File

@ -32,60 +32,47 @@ class AtomicPropositionsLabeling {
public: public:
//! Constructor
/*! /*!
* Constructs an empty atomic propositions labeling for the given number * Constructs an empty atomic propositions labeling for the given number of states and amount of atomic propositions.
* of states and amount of atomic propositions. *
* @param stateCount The number of states of the model. * @param stateCount The number of states of the model.
* @param apCountMax The number of atomic propositions. * @param apCountMax The number of atomic propositions.
*/ */
AtomicPropositionsLabeling(const uint_fast64_t stateCount, const uint_fast64_t apCountMax) AtomicPropositionsLabeling(const uint_fast64_t stateCount, uint_fast64_t const apCountMax)
: stateCount(stateCount), apCountMax(apCountMax), apsCurrent(0) { : stateCount(stateCount), apCountMax(apCountMax), apsCurrent(0), singleLabelings() {
this->singleLabelings = new storm::storage::BitVector*[apCountMax]; singleLabelings.reserve(apCountMax);
for (uint_fast64_t i = 0; i < apCountMax; ++i) {
this->singleLabelings[i] = new storm::storage::BitVector(stateCount);
}
} }
//! Copy Constructor
/*! /*!
* Copy Constructor. Performs a deep copy of the given atomic proposition * Copy Constructor that performs a deep copy of the given atomic proposition labeling.
* labeling. *
* @param atomicPropositionsLabeling The atomic propositions labeling to copy. * @param atomicPropositionsLabeling The atomic propositions labeling to copy.
*/ */
AtomicPropositionsLabeling(const AtomicPropositionsLabeling& atomicPropositionsLabeling) AtomicPropositionsLabeling(AtomicPropositionsLabeling const& atomicPropositionsLabeling)
: stateCount(atomicPropositionsLabeling.stateCount), : stateCount(atomicPropositionsLabeling.stateCount),
apCountMax(atomicPropositionsLabeling.apCountMax), apCountMax(atomicPropositionsLabeling.apCountMax),
apsCurrent(atomicPropositionsLabeling.apsCurrent), apsCurrent(atomicPropositionsLabeling.apsCurrent),
nameToLabelingMap(atomicPropositionsLabeling.nameToLabelingMap) { nameToLabelingMap(atomicPropositionsLabeling.nameToLabelingMap),
this->singleLabelings = new storm::storage::BitVector*[apCountMax]; singleLabelings(atomicPropositionsLabeling.singleLabelings) {
for (uint_fast64_t i = 0; i < apCountMax; ++i) { // Intentionally left empty.
this->singleLabelings[i] = new storm::storage::BitVector(*atomicPropositionsLabeling.singleLabelings[i]); }
}
}
//! Destructor /*!
/* * (Empty) destructor.
* Destructor. Needs to take care of deleting all single labelings.
*/ */
virtual ~AtomicPropositionsLabeling() { ~AtomicPropositionsLabeling() {
// delete all the single atomic proposition labelings in the map // Intentionally left empty.
for (uint_fast64_t i = 0; i < apCountMax; ++i) {
delete this->singleLabelings[i];
this->singleLabelings[i] = NULL;
}
delete[] this->singleLabelings;
this->singleLabelings = NULL;
} }
/*! /*!
* Registers the name of a proposition. * Registers the name of a proposition.
* Will throw an error if more atomic propositions are added than were * Will throw an error if more atomic propositions are added than were originally declared or if an atomic
* originally declared or if an atomic proposition is registered twice. * proposition is registered twice.
* @param ap The name of the atomic proposition to add. *
* @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_fast64_t addAtomicProposition(std::string ap) { uint_fast64_t addAtomicProposition(std::string const& ap) {
if (nameToLabelingMap.count(ap) != 0) { if (nameToLabelingMap.count(ap) != 0) {
LOG4CPLUS_ERROR(logger, "Atomic Proposition already exists."); LOG4CPLUS_ERROR(logger, "Atomic Proposition already exists.");
throw storm::exceptions::OutOfRangeException("Atomic Proposition already exists."); throw storm::exceptions::OutOfRangeException("Atomic Proposition already exists.");
@ -96,26 +83,28 @@ public:
"previously declared."); "previously declared.");
} }
nameToLabelingMap[ap] = apsCurrent; nameToLabelingMap[ap] = apsCurrent;
singleLabelings.push_back(storm::storage::BitVector(stateCount));
uint_fast64_t returnValue = apsCurrent++; uint_fast64_t returnValue = apsCurrent++;
return returnValue; return returnValue;
} }
/*! /*!
* Checks whether the name of an atomic proposition is already registered * Checks whether the name of an atomic proposition is registered within this labeling.
* within this labeling. *
* @return True if the proposition was added to the labeling, false otherwise. * @return True if the proposition is registered within the labeling, false otherwise.
*/ */
bool containsAtomicProposition(std::string proposition) { bool containsAtomicProposition(std::string const& proposition) {
return (nameToLabelingMap.count(proposition) != 0); return (nameToLabelingMap.count(proposition) != 0);
} }
/*! /*!
* Adds an atomic proposition to a given state. * Adds an atomic proposition to a given state.
*
* @param ap The name of the atomic proposition. * @param ap The name of the atomic proposition.
* @param state The index of the state to label. * @param state The index of the state to label.
*/ */
void addAtomicPropositionToState(std::string ap, const uint_fast64_t state) { void addAtomicPropositionToState(std::string const& ap, uint_fast64_t const state) {
if (nameToLabelingMap.count(ap) == 0) { if (nameToLabelingMap.count(ap) == 0) {
LOG4CPLUS_ERROR(logger, "Atomic Proposition '" << ap << "' unknown."); LOG4CPLUS_ERROR(logger, "Atomic Proposition '" << ap << "' unknown.");
throw storm::exceptions::OutOfRangeException() << "Atomic Proposition '" << ap << "' unknown."; throw storm::exceptions::OutOfRangeException() << "Atomic Proposition '" << ap << "' unknown.";
@ -124,13 +113,14 @@ public:
LOG4CPLUS_ERROR(logger, "State index out of range."); LOG4CPLUS_ERROR(logger, "State index out of range.");
throw storm::exceptions::OutOfRangeException("State index out of range."); throw storm::exceptions::OutOfRangeException("State index out of range.");
} }
this->singleLabelings[nameToLabelingMap[ap]]->set(state, true); this->singleLabelings[nameToLabelingMap[ap]].set(state, true);
} }
/*! /*!
* Creates a list of atomic propositions for a given state * Returns a list of atomic propositions of a given state.
* @param state The index of a state *
* @returns The list of propositions for the given state * @param state The index of a state.
* @returns The list of propositions for the given state.
*/ */
std::set<std::string> getPropositionsForState(uint_fast64_t state) { std::set<std::string> getPropositionsForState(uint_fast64_t state) {
if (state >= stateCount) { if (state >= stateCount) {
@ -138,11 +128,9 @@ public:
throw storm::exceptions::OutOfRangeException("State index out of range."); throw storm::exceptions::OutOfRangeException("State index out of range.");
} }
std::set<std::string> result; std::set<std::string> result;
for (auto it = nameToLabelingMap.begin(); for (auto apIndexPair : nameToLabelingMap) {
it != nameToLabelingMap.end(); if (this->getStateHasAtomicProposition(apIndexPair.first, state)) {
it++) { result.insert(apIndexPair.first);
if (stateHasAtomicProposition(it->first, state)) {
result.insert(it->first);
} }
} }
return result; return result;
@ -150,18 +138,18 @@ public:
/*! /*!
* Checks whether a given state is labeled with the given atomic proposition. * Checks whether a given state is labeled with the given atomic proposition.
*
* @param ap The name of the atomic proposition. * @param ap The name of the atomic proposition.
* @param state The index of the state to check. * @param state The index of the state to check.
* @return True if the node is labeled with the atomic proposition, false * @return True if the node is labeled with the atomic proposition, false otherwise.
* otherwise.
*/ */
bool stateHasAtomicProposition(std::string ap, const uint_fast64_t state) { bool getStateHasAtomicProposition(std::string const& ap, const uint_fast64_t state) {
return this->singleLabelings[nameToLabelingMap[ap]]->get(state); return this->singleLabelings[nameToLabelingMap[ap]].get(state);
} }
/*! /*!
* Returns the number of atomic propositions managed by this object (set in * Returns the number of atomic propositions managed by this object (set in the initialization).
* the initialization). *
* @return The number of atomic propositions. * @return The number of atomic propositions.
*/ */
uint_fast64_t getNumberOfAtomicPropositions() { uint_fast64_t getNumberOfAtomicPropositions() {
@ -170,11 +158,11 @@ public:
/*! /*!
* Returns the labeling of states associated with the given atomic proposition. * Returns the labeling of states associated with the given atomic proposition.
*
* @param ap The name of the atomic proposition. * @param ap The name of the atomic proposition.
* @return A pointer to an instance of SingleAtomicPropositionLabeling that * @return A bit vector that represents the labeling of the states with the given atomic proposition.
* represents the labeling of the states with the given atomic proposition.
*/ */
storm::storage::BitVector* getAtomicProposition(std::string ap) { storm::storage::BitVector const& getAtomicProposition(std::string const& ap) {
if (!this->containsAtomicProposition(ap)) { if (!this->containsAtomicProposition(ap)) {
LOG4CPLUS_ERROR(logger, "The atomic proposition " << ap << " is invalid for the labeling of the model."); LOG4CPLUS_ERROR(logger, "The atomic proposition " << ap << " is invalid for the labeling of the model.");
throw storm::exceptions::InvalidArgumentException() << "The atomic proposition " << ap throw storm::exceptions::InvalidArgumentException() << "The atomic proposition " << ap
@ -185,27 +173,25 @@ public:
/*! /*!
* Returns the size of the labeling in memory measured in bytes. * Returns the size of the labeling in memory measured in bytes.
*
* @return The size of the labeling in memory measured in bytes. * @return The size of the labeling in memory measured in bytes.
*/ */
uint_fast64_t getSizeInMemory() { uint_fast64_t getSizeInMemory() {
uint_fast64_t size = sizeof(*this); // Add size of this very object to the sizes of the single labelings.
// Add sizes of all single labelings. return sizeof(*this) + apCountMax * sizeof(storm::storage::BitVector);
for (uint_fast64_t i = 0; i < apCountMax; i++) {
size += this->singleLabelings[i]->getSizeInMemory();
}
return size;
} }
/*! /*!
* Prints information about the labeling to the specified stream. * Prints information about the labeling to the specified stream.
*
* @param out The stream the information is to be printed to. * @param out The stream the information is to be printed to.
*/ */
void printAtomicPropositionsInformationToStream(std::ostream& out) { void printAtomicPropositionsInformationToStream(std::ostream& out) {
out << "Atomic Propositions: \t" << this->getNumberOfAtomicPropositions() out << "Atomic Propositions: \t" << this->getNumberOfAtomicPropositions()
<< std::endl; << std::endl;
for (auto ap : this->nameToLabelingMap) { for (auto apIndexPair : this->nameToLabelingMap) {
out << "\t * " << ap.first << " -> " out << "\t * " << apIndexPair.first << " -> "
<< this->singleLabelings[ap.second]->getNumberOfSetBits(); << this->singleLabelings[apIndexPair.second].getNumberOfSetBits();
out << " state(s)" << std::endl; out << " state(s)" << std::endl;
} }
} }
@ -237,7 +223,7 @@ private:
* a particular atomic proposition, the map from names to indices in this * a particular atomic proposition, the map from names to indices in this
* array has to be used. * array has to be used.
*/ */
storm::storage::BitVector** singleLabelings; std::vector<storm::storage::BitVector> singleLabelings;
}; };
} // namespace models } // namespace models

76
test/parser/ReadLabFileTest.cpp
View File

@ -38,48 +38,48 @@ TEST(ReadLabFileTest, ParseTest) {
ASSERT_TRUE(labeling->containsAtomicProposition(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->stateHasAtomicProposition(phi,0)); ASSERT_TRUE(labeling->getStateHasAtomicProposition(phi,0));
ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,1)); ASSERT_TRUE(labeling->getStateHasAtomicProposition(phi,1));
ASSERT_TRUE(labeling->stateHasAtomicProposition(phi,2)); ASSERT_TRUE(labeling->getStateHasAtomicProposition(phi,2));
ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,3));
ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,3)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,4));
ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,4)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,5));
ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,5)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,6));
ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,6)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,7));
ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,7)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,8));
ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,8)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,9));
ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,9)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,10));
ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,10)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(phi,11));
ASSERT_FALSE(labeling->stateHasAtomicProposition(phi,11));
//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_FALSE(labeling->stateHasAtomicProposition(psi,0)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,0));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,1)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,1));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,2)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,2));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,3)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,3));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,4)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,4));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,5)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,5));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,6)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,6));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,7)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,7));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,8)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,8));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,9)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,9));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,10)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(psi,10));
ASSERT_FALSE(labeling->stateHasAtomicProposition(psi,11)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(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->stateHasAtomicProposition(smth,2)); ASSERT_TRUE(labeling->getStateHasAtomicProposition(smth,2));
ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,0));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,0)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,1));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,1)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,3));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,3)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,4));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,4)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,5));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,5)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,6));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,6)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,7));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,7)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,8));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,8)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,9));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,9)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,10));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,10)); ASSERT_FALSE(labeling->getStateHasAtomicProposition(smth,11));
ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,11));
//Deleting the labeling //Deleting the labeling
delete parser; delete parser;

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