diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 8e9e23503..ccc5f06cf 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -1312,7 +1312,7 @@ namespace storm { // (4.5) Read off result from variables. storm::storage::VectorSet usedLabelSet = getUsedLabelsInSolution(environmentModelPair.first, environmentModelPair.second, variableInformation); - usedLabelSet.insert(choiceInformation.knownLabels.begin(), choiceInformation.knownLabels.end()); + usedLabelSet.insert(choiceInformation.knownLabels); // Display achieved probability. std::pair initialStateProbabilityPair = getReachabilityProbability(environmentModelPair.first, environmentModelPair.second, labeledMdp, variableInformation); diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index e3fa9e394..2391b772b 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -228,7 +228,7 @@ namespace storm { // If the state is initial, we need to add all the choice labels to the initial label set. if (initialStates.get(currentState)) { - initialLabels.insert(choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end()); + initialLabels.insert(choiceLabeling[currentChoice]); initialCombinations.insert(choiceLabeling[currentChoice]); } @@ -246,7 +246,7 @@ namespace storm { // If the choice can reach a target state directly, we add all the labels to the target label set. if (canReachTargetState) { - targetLabels.insert(choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end()); + targetLabels.insert(choiceLabeling[currentChoice]); targetCombinations.insert(choiceLabeling[currentChoice]); } } @@ -1513,7 +1513,7 @@ namespace storm { // Restrict the given MDP to the current set of labels and compute the reachability probability. modelCheckingClock = std::chrono::high_resolution_clock::now(); - commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); + commandSet.insert(relevancyInformation.knownLabels); storm::models::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(subMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver()); LOG4CPLUS_DEBUG(logger, "Invoking model checker."); diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp index ac909d69f..52af4c6f2 100644 --- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -43,29 +43,14 @@ namespace storm { // Record that the current source was the last source. lastsource = source; - char actionNameBuffer[20]; -#ifdef WINDOWS - int length = sscanf_s(buf, "%20s\n", actionNameBuffer, 20); -#else - int length = sscanf(buf, "%20s\n", actionNameBuffer); -#endif - - // If the number of arguments filled is not one, there was an error. - if (length != 1) { - LOG4CPLUS_ERROR(logger, "Parsing error."); - throw storm::exceptions::WrongFormatException() << "Parsing error."; - } else { - // If the action name was parsed successfully, we need to move by the corresponding number of characters. - buf += strlen(actionNameBuffer); - } - // Depending on the action name, the choice is either a probabilitic one or a markovian one. bool isMarkovianChoice = false; - if (strcmp(actionNameBuffer, "!") == 0) { + if (buf[0] == '!') { isMarkovianChoice = true; } else { isMarkovianChoice = false; } + ++buf; if (isMarkovianChoice) { if (stateHasMarkovianChoice) { @@ -89,33 +74,21 @@ namespace storm { // At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state. do { - // Now parse the next symbol to see whether there is another target state for the current choice - // or not. - char star[1]; -#ifdef WINDOWS - length = sscanf_s(buf, "%1s\n", star, 1); -#else - length = sscanf(buf, "%1s\n", star); -#endif - - // If the number of arguments filled is not one, there was an error. - if (length == EOF) { + // If the end of the file was reached, we need to abort and check whether we are in a legal state. + if (buf[0] == '\0') { if (!hasSuccessorState) { - LOG4CPLUS_ERROR(logger, "Premature end-of-file. Expected at least one successor state for state " << source << " under action " << actionNameBuffer << "."); - throw storm::exceptions::WrongFormatException() << "Premature end-of-file. Expected at least one successor state for state " << source << " under action " << actionNameBuffer << "."; + LOG4CPLUS_ERROR(logger, "Premature end-of-file. Expected at least one successor state for state " << source << "."); + throw storm::exceptions::WrongFormatException() << "Premature end-of-file. Expected at least one successor state for state " << source << "."; } else { // If there was at least one successor for the current choice, this is legal and we need to move on. encounteredEOF = true; } - } else if (length != 1) { - LOG4CPLUS_ERROR(logger, "Parsing error."); - throw storm::exceptions::WrongFormatException() << "Parsing error."; - } else if (strcmp(star, "*") == 0) { + } else if (buf[0] == '*') { // We need to record that we found at least one successor state for the current choice. hasSuccessorState = true; // As we have encountered a "*", we know that there is an additional successor state for the current choice. - buf += strlen(star); + ++buf; // Now we need to read the successor state and check if we already saw a higher state index. target = checked_strtol(buf, &buf); @@ -161,11 +134,11 @@ namespace storm { while (buf[0] != '\0' && !encounteredEOF) { // At the current point, the next thing to read is the source state of the next choice to come. source = checked_strtol(buf, &buf); - + // If we have skipped some states, we need to insert self-loops if requested. if (source > lastsource + 1) { if (fixDeadlocks) { - for (uint_fast64_t index = lastsource + 1; index < source; ++source) { + for (uint_fast64_t index = lastsource + 1; index < source; ++index) { result.nondeterministicChoiceIndices[index] = currentChoice; result.transitionMatrix.addNextValue(currentChoice, index, 1); ++currentChoice; @@ -184,25 +157,9 @@ namespace storm { // Record that the current source was the last source. lastsource = source; - char actionNameBuffer[20]; -#ifdef WINDOWS - int length = sscanf_s(buf, "%20s\n", actionNameBuffer, 20); -#else - int length = sscanf(buf, "%20s\n", actionNameBuffer); -#endif - - // If the number of arguments filled is not one, there was an error. - if (length != 1) { - LOG4CPLUS_ERROR(logger, "Parsing error."); - throw storm::exceptions::WrongFormatException() << "Parsing error."; - } else { - // If the action name was parsed successfully, we need to move by the corresponding number of characters. - buf += strlen(actionNameBuffer); - } - // Depending on the action name, the choice is either a probabilitic one or a markovian one. bool isMarkovianChoice = false; - if (strcmp(actionNameBuffer, "!") == 0) { + if (buf[0] == '!') { isMarkovianChoice = true; // Mark the current state as a Markovian one. @@ -219,40 +176,24 @@ namespace storm { // At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state. do { - // Now parse the next symbol to see whether there is another target state for the current choice - // or not. - char star[1]; -#ifdef WINDOWS - length = sscanf_s(buf, "%1s\n", star, 1); -#else - length = sscanf(buf, "%1s\n", star); -#endif - - // If the number of arguments filled is not one, there was an error. - if (length == EOF) { - if (!hasSuccessorState) { - LOG4CPLUS_ERROR(logger, "Premature end-of-file. Expected at least one successor state for state " << source << " under action " << actionNameBuffer << "."); - throw storm::exceptions::WrongFormatException() << "Premature end-of-file. Expected at least one successor state for state " << source << " under action " << actionNameBuffer << "."; - } else { - // If there was at least one successor for the current choice, this is legal and we need to move on. - encounteredEOF = true; - } - } else if (length != 1) { - LOG4CPLUS_ERROR(logger, "Parsing error."); - throw storm::exceptions::WrongFormatException() << "Parsing error."; - } else if (strcmp(star, "*") == 0) { + // If the end of the file was reached, we need to abort and check whether we are in a legal state. + if (buf[0] == '\0') { + // Under the assumption that the currently open choice has at least one successor (which is given after the first run) + // we may legally stop reading here. + encounteredEOF = true; + } else if (buf[0] == '*') { // We need to record that we found at least one successor state for the current choice. hasSuccessorState = true; // As we have encountered a "*", we know that there is an additional successor state for the current choice. - buf += strlen(star); + ++buf; // Now we need to read the successor state and check if we already saw a higher state index. target = checked_strtol(buf, &buf); // And the corresponding probability/rate. double val = checked_strtod(buf, &buf); - + // Record the value as well as the exit rate in case of a Markovian choice. result.transitionMatrix.addNextValue(currentChoice, target, val); if (isMarkovianChoice) { diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp index 0a4fe4441..26035baf7 100644 --- a/src/storage/MaximalEndComponentDecomposition.cpp +++ b/src/storage/MaximalEndComponentDecomposition.cpp @@ -94,7 +94,7 @@ namespace storm { // Now erase the states that have no option to stay inside the MEC with all successors. mecChanged |= !statesToRemove.empty(); std::vector statesToRemoveList = statesToRemove.getSetIndicesList(); - scc.erase(storm::storage::VectorSet(statesToRemoveList.begin(), statesToRemoveList.end())); + scc.erase(storm::storage::VectorSet(statesToRemoveList)); // Now check which states should be reconsidered, because successors of them were removed. statesToCheck.clear(); diff --git a/src/storage/VectorSet.cpp b/src/storage/VectorSet.cpp new file mode 100644 index 000000000..5fcffae4a --- /dev/null +++ b/src/storage/VectorSet.cpp @@ -0,0 +1,282 @@ +#include "src/storage/VectorSet.h" + +namespace storm { + namespace storage { + template + VectorSet::VectorSet() : data(), dirty(false) { + // Intentionally left empty. + } + + template + VectorSet::VectorSet(uint_fast64_t size) : data(), dirty(false) { + data.reserve(size); + } + + template + VectorSet::VectorSet(std::vector const& data) : data(data), dirty(true) { + ensureSet(); + } + + template + VectorSet::VectorSet(std::set const& data) : dirty(false) { + this->data.reserve(data.size()); + for (auto const& element : data) { + this->data.push_back(element); + } + } + + template + VectorSet::VectorSet(uint_fast64_t from, uint_fast64_t to) : dirty(false) { + data.reserve(to - from); + + for (uint_fast64_t element = from; element < to; ++element) { + data.push_back(element); + } + } + + template + VectorSet::VectorSet(VectorSet const& other) : dirty(false) { + other.ensureSet(); + data = other.data; + } + + template + VectorSet& VectorSet::operator=(VectorSet const& other) { + data = other.data; + dirty = other.dirty; + return *this; + } + + template + VectorSet::VectorSet(VectorSet&& other) : data(std::move(other.data)), dirty(std::move(other.dirty)) { + // Intentionally left empty. + } + + template + VectorSet& VectorSet::operator=(VectorSet&& other) { + data = std::move(other.data); + dirty = std::move(other.dirty); + return *this; + } + + template + bool VectorSet::operator==(VectorSet const& other) const { + ensureSet(); + if (this->size() != other.size()) return false; + return std::equal(data.begin(), data.end(), other.begin()); + } + + template + bool VectorSet::operator<(VectorSet const& other) const { + ensureSet(); + if (this->size() < other.size()) return true; + if (this->size() > other.size()) return false; + for (auto it1 = this->begin(), it2 = other.begin(); it1 != this->end(); ++it1, ++it2) { + if (*it1 < *it2) return true; + if (*it1 > *it2) return false; + } + return false; + } + + template + bool VectorSet::operator>(VectorSet const& other) const { + ensureSet(); + if (this->size() > other.size()) return true; + if (this->size() < other.size()) return false; + for (auto it1 = this->begin(), it2 = other.begin(); it1 != this->end(); ++it1, ++it2) { + if (*it1 > *it2) return true; + if (*it1 < *it2) return false; + } + return false; + } + + template + void VectorSet::ensureSet() const { + if (dirty) { + std::sort(data.begin(), data.end()); + data.erase(std::unique(data.begin(), data.end()), data.end()); + dirty = false; + } + } + + template + bool VectorSet::contains(ValueType const& element) const { + ensureSet(); + return std::binary_search(data.begin(), data.end(), element); + } + + template + bool VectorSet::subsetOf(VectorSet const& other) const { + ensureSet(); + other.ensureSet(); + return std::includes(other.begin(), other.end(), data.begin(), data.end()); + } + + template + bool VectorSet::supersetOf(VectorSet const& other) const { + ensureSet(); + return other.subsetOf(*this); + } + + template + VectorSet VectorSet::intersect(VectorSet const& other) { + ensureSet(); + other.ensureSet(); + VectorSet result; + std::set_intersection(data.begin(), data.end(), other.begin(), other.end(), std::inserter(result.data, result.data.end())); + return result; + } + + template + VectorSet VectorSet::join(VectorSet const& other) { + ensureSet(); + other.ensureSet(); + VectorSet result; + std::set_union(data.begin(), data.end(), other.begin(), other.end(), std::inserter(result.data, result.data.end())); + return result; + } + + template + typename VectorSet::iterator VectorSet::begin() { + ensureSet(); + return data.begin(); + } + + template + typename VectorSet::iterator VectorSet::end() { + ensureSet(); + return data.end(); + } + + template + typename VectorSet::const_iterator VectorSet::begin() const { + ensureSet(); + return data.begin(); + } + + template + typename VectorSet::const_iterator VectorSet::end() const { + ensureSet(); + return data.end(); + } + + template + ValueType const& VectorSet::min() const { + if (this->size() == 0) { + throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; + } + + ensureSet(); + return data.front(); + } + + template + ValueType const& VectorSet::max() const { + if (this->size() == 0) { + throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; + } + + ensureSet(); + return data.back(); + } + + template + void VectorSet::insert(ValueType const& element) { + data.push_back(element); + dirty = true; + } + + template + typename VectorSet::iterator VectorSet::insert(typename VectorSet::const_iterator pos, ValueType const& element) { + dirty = true; + return data.insert(pos, element); + } + + template + void VectorSet::insert(VectorSet const& other) { + data.insert(data.end(), other.data.begin(), other.data.end()); + } + + template + bool VectorSet::empty() const { + ensureSet(); + return data.empty(); + } + + template + size_t VectorSet::size() const { + ensureSet(); + return data.size(); + } + + template + void VectorSet::clear() { + data.clear(); + dirty = false; + } + + template + bool VectorSet::erase(ValueType const& element) { + ensureSet(); + uint_fast64_t lowerBound = 0; + uint_fast64_t upperBound = data.size(); + while (lowerBound != upperBound) { + uint_fast64_t currentPosition = lowerBound + (upperBound - lowerBound) / 2; + bool searchInLowerHalf = element < data[currentPosition]; + if (searchInLowerHalf) { + upperBound = currentPosition; + } else { + bool searchInRightHalf = element > data[currentPosition]; + if (searchInRightHalf) { + lowerBound = currentPosition + 1; + } else { + // At this point we have found the element. + data.erase(data.begin() + currentPosition); + return true; + } + } + } + return false; + } + + template + void VectorSet::erase(VectorSet const& eraseSet) { + if (eraseSet.size() > 0) { + ensureSet(); + eraseSet.ensureSet(); + + for (typename std::vector::reverse_iterator delIt = eraseSet.data.rbegin(), setIt = data.rbegin(); delIt != eraseSet.data.rend() && setIt != eraseSet.data.rend(); ++delIt) { + while (setIt != eraseSet.data.rend() && *setIt > *delIt) { + ++setIt; + } + if (setIt != data.rend()) break; + + if (*setIt == *delIt) { + data.erase((setIt + 1).base()); + ++setIt; + } + } + } + } + + template + std::ostream& operator<<(std::ostream& stream, VectorSet const& set) { + set.ensureSet(); + stream << "VectorSet(" << set.size() << ") { "; + if (set.size() > 0) { + for (uint_fast64_t index = 0; index < set.size() - 1; ++index) { + stream << set.data[index] << ", "; + } + stream << set.data[set.size() - 1] << " }"; + } else { + stream << "}"; + } + return stream; + } + + template class VectorSet; + template class VectorSet>; + template std::ostream& operator<<(std::ostream& stream, VectorSet const& set); + template std::ostream& operator<<(std::ostream& stream, VectorSet> const& set); + } +} \ No newline at end of file diff --git a/src/storage/VectorSet.h b/src/storage/VectorSet.h index 78057d684..e366611bd 100644 --- a/src/storage/VectorSet.h +++ b/src/storage/VectorSet.h @@ -19,254 +19,85 @@ namespace storm { namespace storage { - template + template class VectorSet { public: - typedef T* difference_type; - typedef T value_type; - typedef T* pointer; - typedef T& reference; - typedef typename std::vector::iterator iterator; - typedef typename std::vector::const_iterator const_iterator; - - VectorSet() : data(), dirty(false) { - // Intentionally left empty. - } - - VectorSet(uint_fast64_t size) : data(), dirty(false) { - data.reserve(size); - } - - VectorSet(std::vector const& data) : data(data), dirty(true) { - ensureSet(); - } - - VectorSet(std::set const& data) : dirty(false) { - this->data.reserve(data.size()); - for (auto const& element : data) { - this->data.push_back(element); - } - } - - VectorSet(uint_fast64_t from, uint_fast64_t to) : dirty(false) { - data.reserve(to - from); - - for (uint_fast64_t element = from; element < to; ++element) { - data.push_back(element); - } - } - - template - VectorSet(InputIterator first, InputIterator last) : data(first, last), dirty(true) { - ensureSet(); - } - - VectorSet(VectorSet const& other) : dirty(false) { - other.ensureSet(); - data = other.data; - } - - VectorSet& operator=(VectorSet const& other) { - data = other.data; - dirty = other.dirty; - return *this; - } - - VectorSet(VectorSet&& other) : data(std::move(other.data)), dirty(std::move(other.dirty)) { - // Intentionally left empty. - } - - VectorSet& operator=(VectorSet&& other) { - data = std::move(other.data); - dirty = std::move(other.dirty); - return *this; - } - - bool operator==(VectorSet const& other) const { - ensureSet(); - if (this->size() != other.size()) return false; - return std::equal(data.begin(), data.end(), other.begin()); - } - - bool operator<(VectorSet const& other) const { - ensureSet(); - if (this->size() < other.size()) return true; - if (this->size() > other.size()) return false; - for (auto it1 = this->begin(), it2 = other.begin(); it1 != this->end(); ++it1, ++it2) { - if (*it1 < *it2) return true; - if (*it1 > *it2) return false; - } - return false; - } - - void ensureSet() const { - if (dirty) { - std::sort(data.begin(), data.end()); - data.erase(std::unique(data.begin(), data.end()), data.end()); - dirty = false; - } - } - - bool contains(T const& element) const { - ensureSet(); - return std::binary_search(data.begin(), data.end(), element); - } - - bool subsetOf(VectorSet const& other) const { - ensureSet(); - other.ensureSet(); - return std::includes(other.begin(), other.end(), data.begin(), data.end()); - } - - bool supersetOf(VectorSet const& other) const { - ensureSet(); - return other.subsetOf(*this); - } - - VectorSet intersect(VectorSet const& other) { - ensureSet(); - other.ensureSet(); - VectorSet result; - std::set_intersection(data.begin(), data.end(), other.begin(), other.end(), std::inserter(result.data, result.data.end())); - return result; - } - - VectorSet join(VectorSet const& other) { - ensureSet(); - other.ensureSet(); - VectorSet result; - std::set_union(data.begin(), data.end(), other.begin(), other.end(), std::inserter(result.data, result.data.end())); - return result; - } - - iterator begin() { - ensureSet(); - return data.begin(); - } - - iterator end() { - ensureSet(); - return data.end(); - } - - const_iterator begin() const { - ensureSet(); - return data.begin(); - } - - const_iterator end() const { - ensureSet(); - return data.end(); - } - - T const& min() const { - if (this->size() == 0) { - throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; - } - - ensureSet(); - return data.first; - } - - T const& max() const { - if (this->size() == 0) { - throw storm::exceptions::InvalidStateException() << "Cannot retrieve minimum of empty set."; - } - - ensureSet(); - return data.back; - } - - void insert(T const& element) { - data.push_back(element); - dirty = true; - } - - template - iterator insert(InputIterator first, InputIterator last) { - dirty = true; - return data.insert(data.end(), first, last); - } - - template - iterator insert(InputIterator pos, T element) { - dirty = true; - return data.insert(pos, element); - } - - bool empty() const { - ensureSet(); - return data.empty(); - } - - size_t size() const { - ensureSet(); - return data.size(); - } - - void clear() { - data.clear(); - dirty = false; - } - - bool erase(T const& element) { - ensureSet(); - uint_fast64_t lowerBound = 0; - uint_fast64_t upperBound = data.size(); - while (lowerBound != upperBound) { - uint_fast64_t currentPosition = lowerBound + (upperBound - lowerBound) / 2; - bool searchInLowerHalf = element < data[currentPosition]; - if (searchInLowerHalf) { - upperBound = currentPosition; - } else { - bool searchInRightHalf = element > data[currentPosition]; - if (searchInRightHalf) { - lowerBound = currentPosition + 1; - } else { - // At this point we have found the element. - data.erase(data.begin() + currentPosition); - return true; - } - } - } - return false; - } - - void erase(VectorSet const& eraseSet) { - if (eraseSet.size() > 0) { - ensureSet(); - eraseSet.ensureSet(); - - for (typename std::vector::reverse_iterator delIt = eraseSet.data.rbegin(), setIt = data.rbegin(); delIt != eraseSet.data.rend() && setIt != eraseSet.data.rend(); ++delIt) { - while (setIt != eraseSet.data.rend() && *setIt > *delIt) { - ++setIt; - } - if (setIt != data.rend()) break; + typedef ValueType* difference_type; + typedef ValueType value_type; + typedef ValueType* pointer; + typedef ValueType& reference; + typedef typename std::vector::iterator iterator; + typedef typename std::vector::const_iterator const_iterator; + + VectorSet(); + + VectorSet(uint_fast64_t size); + + VectorSet(std::vector const& data); + + VectorSet(std::set const& data); + + VectorSet(uint_fast64_t from, uint_fast64_t to); - if (*setIt == *delIt) { - data.erase((setIt + 1).base()); - ++setIt; - } - } - } - } - - friend std::ostream& operator<< (std::ostream& stream, VectorSet const& set) { - set.ensureSet(); - stream << "VectorSet(" << set.size() << ") { "; - if (set.size() > 0) { - for (uint_fast64_t index = 0; index < set.size() - 1; ++index) { - stream << set.data[index] << ", "; - } - stream << set.data[set.size() - 1] << " }"; - } else { - stream << "}"; - } - return stream; - } + VectorSet(VectorSet const& other); + + VectorSet& operator=(VectorSet const& other); + + VectorSet(VectorSet&& other); + + VectorSet& operator=(VectorSet&& other); + + bool operator==(VectorSet const& other) const; + + bool operator<(VectorSet const& other) const; + + bool operator>(VectorSet const& other) const; + + void ensureSet() const; + + bool contains(ValueType const& element) const; + + bool subsetOf(VectorSet const& other) const; + + bool supersetOf(VectorSet const& other) const; + + VectorSet intersect(VectorSet const& other); + + VectorSet join(VectorSet const& other); + + iterator begin(); + + iterator end(); + + const_iterator begin() const; + + const_iterator end() const; + + ValueType const& min() const; + + ValueType const& max() const; + + void insert(ValueType const& element); + + iterator insert(const_iterator pos, ValueType const& element); + + void insert(VectorSet const& other); + + bool empty() const; + + size_t size() const; + + void clear(); + + bool erase(ValueType const& element); + + void erase(VectorSet const& eraseSet); + + template + friend std::ostream& operator<< (std::ostream& stream, VectorSet const& set); private: - mutable std::vector data; + mutable std::vector data; mutable bool dirty; }; }