Browse Source

Adding new atomic propositions and attach it to a set of states

Former-commit-id: 2fee551b17
main
sjunges 11 years ago
parent
commit
c0b5757e4d
  1. 20
      src/models/AtomicPropositionsLabeling.h

20
src/models/AtomicPropositionsLabeling.h

@ -139,21 +139,39 @@ public:
* @return The index of the new proposition. * @return The index of the new proposition.
*/ */
uint_fast64_t addAtomicProposition(std::string const& ap) { uint_fast64_t addAtomicProposition(std::string const& ap) {
return addAtomicProposition(ap, storage::BitVector(stateCount));
}
/**
* Creates a new atomic proposition and attaches the given states with the label.
* @param ap
* @param states
* @return
*/
uint_fast64_t addAtomicProposition(std::string const& ap, storage::BitVector const& states)
{
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.");
} }
if(states.size() != stateCount)
{
LOG4CPLUS_ERROR(logger, "State vector has invalid size.");
throw storm::exceptions::OutOfRangeException("State vector has invalid size.");
}
if (apsCurrent >= apCountMax) { if (apsCurrent >= apCountMax) {
apCountMax++; apCountMax++;
singleLabelings.reserve(apCountMax); singleLabelings.reserve(apCountMax);
} }
nameToLabelingMap.emplace(ap, apsCurrent); nameToLabelingMap.emplace(ap, apsCurrent);
singleLabelings.emplace_back(stateCount);
singleLabelings.push_back(states);
uint_fast64_t returnValue = apsCurrent++; uint_fast64_t returnValue = apsCurrent++;
return returnValue; return returnValue;
} }
/*! /*!
* Checks whether the name of an atomic proposition is registered within this labeling. * Checks whether the name of an atomic proposition is registered within this labeling.
* *

Loading…
Cancel
Save