From c0b5757e4df7faeb1f81ba82ba115817aba87e21 Mon Sep 17 00:00:00 2001 From: sjunges Date: Thu, 24 Apr 2014 15:57:36 +0200 Subject: [PATCH] Adding new atomic propositions and attach it to a set of states Former-commit-id: 2fee551b17a223ac8425212b507c7d8ed088a799 --- src/models/AtomicPropositionsLabeling.h | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index b7b067090..b5ebfba8b 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -139,20 +139,38 @@ public: * @return The index of the new proposition. */ 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) { LOG4CPLUS_ERROR(logger, "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) { apCountMax++; singleLabelings.reserve(apCountMax); } nameToLabelingMap.emplace(ap, apsCurrent); - singleLabelings.emplace_back(stateCount); + singleLabelings.push_back(states); uint_fast64_t returnValue = apsCurrent++; return returnValue; } + /*! * Checks whether the name of an atomic proposition is registered within this labeling.