From 12287e509098263f944841dfeecbeff9ff774ab3 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 30 Jun 2016 12:43:02 +0200 Subject: [PATCH] small fix for building MAs Also fixed a test for explicit MA parsing, where the transitions of a probabilistic choice did not sum up to one Former-commit-id: c2f920a4d6d441ed80e8a64e1b1a25c28d736e74 --- src/builder/ExplicitModelBuilder.cpp | 6 +++--- src/models/sparse/MarkovAutomaton.cpp | 11 ++++++++++- src/models/sparse/MarkovAutomaton.h | 6 ++++-- src/storage/BitVector.cpp | 3 ++- 4 files changed, 19 insertions(+), 7 deletions(-) diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp index aaa000000..bb62757a4 100644 --- a/src/builder/ExplicitModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -178,7 +178,7 @@ namespace storm { // Create markovian states bit vector, if required if (generator->getModelType() == storm::generator::ModelType::MA) { // The BitVector will be resized when the correct size is known - markovianChoices = storm::storage::BitVector(64, false); + markovianChoices = storm::storage::BitVector(); } // Create a callback for the next-state generator to enable it to request the index of states. @@ -230,7 +230,7 @@ namespace storm { } if (generator->getModelType() == storm::generator::ModelType::MA) { - markovianChoices->enlargeLiberally(currentRow, false); + markovianChoices->enlargeLiberally(currentRow+1, false); markovianChoices->set(currentRow); } @@ -279,7 +279,7 @@ namespace storm { // If we keep track of the Markovian choices, store whether the current one is Markovian. if( markovianChoices && choice.isMarkovian() ) { - markovianChoices->enlargeLiberally(currentRow, false); + markovianChoices->enlargeLiberally(currentRow+1, false); markovianChoices->set(currentRow); } diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp index f822de3c1..b09da840e 100644 --- a/src/models/sparse/MarkovAutomaton.cpp +++ b/src/models/sparse/MarkovAutomaton.cpp @@ -267,7 +267,7 @@ namespace storm { ++row; } for(; row < this->getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { - STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Transitions of rateMatrix do not sum up to one for some non-Markovian choice."); + STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Transitions of rateMatrix do not sum up to one for some non-Markovian choice. Sum is " << this->getTransitionMatrix().getRowSum(row) << ". State is " << state << ". Choice is " << row << "."); } } } @@ -355,6 +355,15 @@ namespace storm { } + template + void MarkovAutomaton::printModelInformationToStream(std::ostream& out) const { + this->printModelInformationHeaderToStream(out); + out << "Choices: \t" << this->getNumberOfChoices() << std::endl; + out << "Markovian St.: \t" << this->getMarkovianStates().getNumberOfSetBits() << std::endl; + this->printModelInformationFooterToStream(out); + } + + template class MarkovAutomaton; // template class MarkovAutomaton; template class MarkovAutomaton; diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h index f78dc073c..71d35b894 100644 --- a/src/models/sparse/MarkovAutomaton.h +++ b/src/models/sparse/MarkovAutomaton.h @@ -188,9 +188,11 @@ namespace storm { std::shared_ptr> convertToCTMC(); - virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const; + virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; - std::size_t getSizeInBytes() const; + std::size_t getSizeInBytes() const override; + + virtual void printModelInformationToStream(std::ostream& out) const override; private: /*! diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index ccbcce134..81705d431 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -255,7 +255,8 @@ namespace storm { void BitVector::enlargeLiberally(uint_fast64_t minimumLength, bool init) { if(minimumLength > this->size()) { - uint_fast64_t newLength = this->bucketCount() << 6; + uint_fast64_t newLength = this->bucketCount(); + newLength = std::max(newLength, 1ull) << 6; while(newLength < minimumLength) { newLength = newLength << 1; }