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

Renamed and refactored atomic propositions labeling.

tempestpy_adaptions
dehnert 12 years ago
parent
8911b0b71a
commit
378fe3f532
7 changed files with 48 additions and 133 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      src/modelChecker/DtmcPrctlModelChecker.h
  2. 86
      src/models/AtomicPropositionsLabeling.h
  3. 2
      src/models/dtmc.h
  4. 85
      src/models/single_atomic_proposition_labeling.h
  5. 2
      src/mrmc.cpp
  6. 2
      src/parser/read_lab_file.h
  7. 2
      test/parser/read_lab_file_test.cpp

2
src/modelChecker/DtmcPrctlModelChecker.h
View File

@ -40,7 +40,7 @@ class DtmcPrctlModelChecker {
~DtmcPrctlModelChecker();
virtual void makeAbsorbing(mrmc::storage::BitVector*) = 0;
virtual mrmc::storage::BitVector getStatesSatisying(mrmc::models::SingleAtomicPropositionLabeling*) = 0;
virtual mrmc::storage::BitVector& getStatesSatisying(std::string) = 0;
virtual std::vector<T> multiplyMatrixVector(std::vector<T>*) = 0;
virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula* formula) {

86
src/models/atomic_propositions_labeling.h → src/models/AtomicPropositionsLabeling.h
View File

@ -8,10 +8,9 @@
#ifndef MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_
#define MRMC_MODELS_ATOMIC_PROPOSITIONS_LABELING_H_
#include "src/storage/BitVector.h"
#include <ostream>
#include "src/models/single_atomic_proposition_labeling.h"
/* 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.
@ -47,14 +46,14 @@ public:
/*!
* 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.
* @param stateCount The number of states of the model.
* @param apCountMax The number of atomic propositions.
*/
AtomicPropositionsLabeling(const uint_fast32_t state_count, const uint_fast32_t ap_count)
: state_count(state_count), ap_count(ap_count), 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);
AtomicPropositionsLabeling(const uint_fast32_t stateCount, const uint_fast32_t apCountMax)
: stateCount(stateCount), apCountMax(apCountMax), apsCurrent(0) {
this->singleLabelings = new mrmc::storage::BitVector*[apCountMax];
for (uint_fast32_t i = 0; i < apCountMax; ++i) {
this->singleLabelings[i] = new mrmc::storage::BitVector(stateCount);
}
}
@ -62,15 +61,16 @@ public:
/*!
* Copy Constructor. Performs a deep copy of the given atomic proposition
* labeling.
* @param atomicPropositionsLabeling The atomic propositions labeling to copy.
*/
AtomicPropositionsLabeling(const AtomicPropositionsLabeling& atomic_propositions_labeling)
: 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]);
AtomicPropositionsLabeling(const AtomicPropositionsLabeling& atomicPropositionsLabeling)
: stateCount(atomicPropositionsLabeling.stateCount),
apCountMax(atomicPropositionsLabeling.apCountMax),
apsCurrent(atomicPropositionsLabeling.apsCurrent),
nameToLabelingMap(atomicPropositionsLabeling.nameToLabelingMap) {
this->singleLabelings = new mrmc::storage::BitVector*[apCountMax];
for (uint_fast32_t i = 0; i < apCountMax; ++i) {
this->singleLabelings[i] = new mrmc::storage::BitVector(*atomicPropositionsLabeling.singleLabelings[i]);
}
}
@ -80,12 +80,12 @@ public:
*/
virtual ~AtomicPropositionsLabeling() {
// delete all the single atomic proposition labelings in the map
for (uint_fast32_t i = 0; i < ap_count; ++i) {
delete this->single_labelings[i];
this->single_labelings[i] = NULL;
for (uint_fast32_t i = 0; i < apCountMax; ++i) {
delete this->singleLabelings[i];
this->singleLabelings[i] = NULL;
}
delete[] this->single_labelings;
this->single_labelings = NULL;
delete[] this->singleLabelings;
this->singleLabelings = NULL;
}
/*!
@ -96,16 +96,16 @@ public:
* @return The index of the new proposition.
*/
uint_fast32_t addAtomicProposition(std::string ap) {
if (name_to_labeling_map.count(ap) != 0) {
if (nameToLabelingMap.count(ap) != 0) {
throw std::out_of_range("Atomic Proposition already exists.");
}
if (aps_current >= ap_count) {
if (apsCurrent >= apCountMax) {
throw std::out_of_range("Added more atomic propositions than"
"previously declared.");
}
name_to_labeling_map[ap] = aps_current;
nameToLabelingMap[ap] = apsCurrent;
uint_fast32_t returnValue = aps_current++;
uint_fast32_t returnValue = apsCurrent++;
return returnValue;
}
@ -115,7 +115,7 @@ public:
* @return True if the proposition was added to the labeling, false otherwise.
*/
bool containsAtomicProposition(std::string proposition) {
return (name_to_labeling_map.count(proposition) != 0);
return (nameToLabelingMap.count(proposition) != 0);
}
/*!
@ -124,13 +124,13 @@ public:
* @param state The index of the state to label.
*/
void addAtomicPropositionToState(std::string ap, const uint_fast32_t state) {
if (name_to_labeling_map.count(ap) == 0) {
if (nameToLabelingMap.count(ap) == 0) {
throw std::out_of_range("Atomic Proposition '" + ap + "' unknown.");
}
if (state >= state_count) {
if (state >= stateCount) {
throw std::out_of_range("State index out of range.");
}
this->single_labelings[name_to_labeling_map[ap]]->addLabelToState(state);
this->singleLabelings[nameToLabelingMap[ap]]->set(state, true);
}
/*!
@ -141,7 +141,7 @@ public:
* otherwise.
*/
bool stateHasAtomicProposition(std::string ap, const uint_fast32_t state) {
return this->single_labelings[name_to_labeling_map[ap]]->hasLabel(state);
return this->singleLabelings[nameToLabelingMap[ap]]->get(state);
}
/*!
@ -150,7 +150,7 @@ public:
* @return The number of atomic propositions.
*/
uint_fast32_t getNumberOfAtomicPropositions() {
return ap_count;
return apCountMax;
}
/*!
@ -159,8 +159,8 @@ public:
* @return A pointer to an instance of SingleAtomicPropositionLabeling that
* represents the labeling of the states with the given atomic proposition.
*/
SingleAtomicPropositionLabeling* getAtomicProposition(std::string ap) {
return (this->single_labelings[name_to_labeling_map[ap]]);
mrmc::storage::BitVector* getAtomicProposition(std::string ap) {
return (this->singleLabelings[nameToLabelingMap[ap]]);
}
/*!
@ -170,8 +170,8 @@ public:
uint_fast64_t getSizeInMemory() {
uint_fast64_t size = sizeof(*this);
// add sizes of all single labelings
for (uint_fast32_t i = 0; i < ap_count; i++) {
size += this->single_labelings[i]->getSizeInMemory();
for (uint_fast32_t i = 0; i < apCountMax; i++) {
size += this->singleLabelings[i]->getSizeInMemory();
}
return size;
}
@ -183,9 +183,9 @@ public:
void printAtomicPropositionsInformationToStream(std::ostream& out) {
out << "Atomic Propositions: \t" << this->getNumberOfAtomicPropositions()
<< std::endl;
for(auto ap : this->name_to_labeling_map) {
for(auto ap : this->nameToLabelingMap) {
out << "\t * " << ap.first << " -> "
<< this->single_labelings[ap.second]->getNumberOfLabeledStates();
<< this->singleLabelings[ap.second]->getNumberOfSetBits();
out << " state(s)" << std::endl;
}
}
@ -193,31 +193,31 @@ public:
private:
/*! The number of states whose labels are to be stored by this object. */
uint_fast32_t state_count;
uint_fast32_t stateCount;
/*! The number of different atomic propositions this object can store. */
uint_fast32_t ap_count;
uint_fast32_t apCountMax;
/*!
* 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;
uint_fast32_t apsCurrent;
/*!
* 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;
MAP<std::string, uint_fast32_t> nameToLabelingMap;
/*!
* 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;
mrmc::storage::BitVector** singleLabelings;
};
} // namespace models

2
src/models/dtmc.h
View File

@ -10,7 +10,7 @@
#include <ostream>
#include "atomic_propositions_labeling.h"
#include "AtomicPropositionsLabeling.h"
#include "backward_transitions.h"
#include "src/storage/SquareSparseMatrix.h"

85
src/models/single_atomic_proposition_labeling.h
View File

@ -1,85 +0,0 @@
#ifndef MRMC_MODELS_SINGLE_ATOMIC_PROPOSITION_LABELING_H_
#define MRMC_MODELS_SINGLE_ATOMIC_PROPOSITION_LABELING_H_
#include "src/storage/BitVector.h"
namespace mrmc {
namespace models {
/*!
* This class represents the labeling of a state space with a single atomic
* proposition.
*/
class SingleAtomicPropositionLabeling {
public:
//! Constructor
/*!
* 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 state_count) : label_vector(state_count) {
// intentionally left empty
}
//! Copy Constructor
/*!
* 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)
: label_vector(single_atomic_proposition_labeling.label_vector) {
// intentionally left empty
}
/*!
* 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);
}
/*!
* 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 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.
*/
uint_fast64_t getSizeInMemory() {
return sizeof(*this) + label_vector.getSizeInMemory();
}
private:
/*!
* A bit vector storing for every state whether or not that state is
* labeled.
*/
mrmc::storage::BitVector label_vector;
};
} // namespace models
} // namespace mrmc
#endif // MRMC_MODELS_SINGLE_ATOMIC_PROPOSITION_LABELING_H_

2
src/mrmc.cpp
View File

@ -18,7 +18,7 @@
#include "mrmc-config.h"
#include "src/models/dtmc.h"
#include "src/storage/SquareSparseMatrix.h"
#include "src/models/atomic_propositions_labeling.h"
#include "src/models/AtomicPropositionsLabeling.h"
#include "src/parser/read_lab_file.h"
#include "src/parser/read_tra_file.h"
#include "src/utility/settings.h"

2
src/parser/read_lab_file.h
View File

@ -8,7 +8,7 @@
#ifndef READ_LAB_FILE_H_
#define READ_LAB_FILE_H_
#include "src/models/atomic_propositions_labeling.h"
#include "src/models/AtomicPropositionsLabeling.h"
namespace mrmc {

2
test/parser/read_lab_file_test.cpp
View File

@ -7,7 +7,7 @@
#include "gtest/gtest.h"
#include "mrmc-config.h"
#include "src/models/atomic_propositions_labeling.h"
#include "src/models/AtomicPropositionsLabeling.h"
#include "src/parser/read_lab_file.h"
#include "src/exceptions/file_IO_exception.h"
#include "src/exceptions/wrong_file_format.h"

Write Preview
Loading…
Cancel
Save