From 91084a5da4b1954c3dab0ddcc657f0894cdd2831 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Nov 2014 11:14:55 +0100 Subject: [PATCH 1/3] APs true/false can now be queried for a state. Former-commit-id: 3c16df45091fb606c97b2abdd987497101f78b5a --- src/models/AtomicPropositionsLabeling.h | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h index 6281c5d6b..c7c3912a6 100644 --- a/src/models/AtomicPropositionsLabeling.h +++ b/src/models/AtomicPropositionsLabeling.h @@ -209,9 +209,14 @@ public: * @return True if the node is labeled with the atomic proposition, false otherwise. */ bool getStateHasAtomicProposition(std::string const& ap, const uint_fast64_t state) const { + if (ap == "true") { + return true; + } else if (ap == "false") { + return false; + } if (!this->containsAtomicProposition(ap)) { - LOG4CPLUS_ERROR(logger, "The atomic proposition " << ap << " is invalid for the labeling of the model."); - throw storm::exceptions::InvalidArgumentException() << "The atomic proposition " << ap << " is invalid for the labeling of the model."; + LOG4CPLUS_ERROR(logger, "The atomic proposition '" << ap << "' is invalid for the labeling of the model."); + throw storm::exceptions::InvalidArgumentException() << "The atomic proposition '" << ap << "' is invalid for the labeling of the model."; } auto apIndexPair = nameToLabelingMap.find(ap); return this->singleLabelings[apIndexPair->second].get(state); From 7d0ae06f9fc49f5a1bb72fabeb3186ddb3f8b357 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 13 Dec 2014 17:19:13 +0100 Subject: [PATCH 2/3] Fixed creation of empty blocks under certain circumstances in bisimulation. Former-commit-id: f1240e234b0cc3cf9fc9cb87f3ee6ba95772fb55 --- ...ministicModelBisimulationDecomposition.cpp | 67 +++++++++++-------- 1 file changed, 38 insertions(+), 29 deletions(-) diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 63c939474..3d5b966dd 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -262,41 +262,50 @@ namespace storm { template DeterministicModelBisimulationDecomposition::Partition::Partition(std::size_t numberOfStates, storm::storage::BitVector const& prob0States, storm::storage::BitVector const& prob1States, std::string const& otherLabel, std::string const& prob1Label, bool keepSilentProbabilities) : numberOfBlocks(0), stateToBlockMapping(numberOfStates), statesAndValues(numberOfStates), positions(numberOfStates), keepSilentProbabilities(keepSilentProbabilities), silentProbabilities() { - typename std::list::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr, numberOfBlocks++); - Block& firstBlock = *firstIt; - firstBlock.setIterator(firstIt); - storm::storage::sparse::state_type position = 0; - for (auto state : prob0States) { - statesAndValues[position] = std::make_pair(state, storm::utility::zero()); - positions[state] = position; - stateToBlockMapping[state] = &firstBlock; - ++position; + Block* firstBlock = nullptr; + Block* secondBlock = nullptr; + Block* thirdBlock = nullptr; + if (!prob0States.empty()) { + typename std::list::iterator firstIt = blocks.emplace(this->blocks.end(), 0, prob0States.getNumberOfSetBits(), nullptr, nullptr, numberOfBlocks++); + firstBlock = &(*firstIt); + firstBlock->setIterator(firstIt); + + for (auto state : prob0States) { + statesAndValues[position] = std::make_pair(state, storm::utility::zero()); + positions[state] = position; + stateToBlockMapping[state] = firstBlock; + ++position; + } + firstBlock->setAbsorbing(true); } - firstBlock.setAbsorbing(true); - typename std::list::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), &firstBlock, nullptr, numberOfBlocks++, std::shared_ptr(new std::string(prob1Label))); - Block& secondBlock = *secondIt; - secondBlock.setIterator(secondIt); - - for (auto state : prob1States) { - statesAndValues[position] = std::make_pair(state, storm::utility::zero()); - positions[state] = position; - stateToBlockMapping[state] = &secondBlock; - ++position; + if (!prob1States.empty()) { + typename std::list::iterator secondIt = blocks.emplace(this->blocks.end(), position, position + prob1States.getNumberOfSetBits(), firstBlock, nullptr, numberOfBlocks++, std::shared_ptr(new std::string(prob1Label))); + secondBlock = &(*secondIt); + secondBlock->setIterator(secondIt); + + for (auto state : prob1States) { + statesAndValues[position] = std::make_pair(state, storm::utility::zero()); + positions[state] = position; + stateToBlockMapping[state] = secondBlock; + ++position; + } + secondBlock->setAbsorbing(true); } - secondBlock.setAbsorbing(true); - - typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, &secondBlock, nullptr, numberOfBlocks++, otherLabel == "true" ? std::shared_ptr(nullptr) : std::shared_ptr(new std::string(otherLabel))); - Block& thirdBlock = *thirdIt; - thirdBlock.setIterator(thirdIt); storm::storage::BitVector otherStates = ~(prob0States | prob1States); - for (auto state : otherStates) { - statesAndValues[position] = std::make_pair(state, storm::utility::zero()); - positions[state] = position; - stateToBlockMapping[state] = &thirdBlock; - ++position; + if (!otherStates.empty()) { + typename std::list::iterator thirdIt = blocks.emplace(this->blocks.end(), position, numberOfStates, secondBlock, nullptr, numberOfBlocks++, otherLabel == "true" ? std::shared_ptr(nullptr) : std::shared_ptr(new std::string(otherLabel))); + thirdBlock = &(*thirdIt); + thirdBlock->setIterator(thirdIt); + + for (auto state : otherStates) { + statesAndValues[position] = std::make_pair(state, storm::utility::zero()); + positions[state] = position; + stateToBlockMapping[state] = thirdBlock; + ++position; + } } // If we are requested to store silent probabilities, we need to prepare the vector. From 554287e0828dbe72cdf1ede39c8dce2dbe6fcada Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 16 Dec 2014 09:59:20 +0100 Subject: [PATCH 3/3] Fixed minor issue that caused problems with the measure-driven initial partition and rewards. Former-commit-id: 7379da548d829c2415bf6f28d24e11475589badc --- src/storage/DeterministicModelBisimulationDecomposition.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp index 3d5b966dd..8455825f2 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp @@ -1207,7 +1207,7 @@ namespace storm { template typename DeterministicModelBisimulationDecomposition::Partition DeterministicModelBisimulationDecomposition::getMeasureDrivenInitialPartition(ModelType const& model, storm::storage::SparseMatrix const& backwardTransitions, std::string const& phiLabel, std::string const& psiLabel, BisimulationType bisimulationType, bool keepRewards, bool bounded) { std::pair statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, phiLabel == "true" ? storm::storage::BitVector(model.getNumberOfStates(), true) : model.getLabeledStates(phiLabel), model.getLabeledStates(psiLabel)); - Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel, bisimulationType == BisimulationType::WeakDtmc); + Partition partition(model.getNumberOfStates(), statesWithProbability01.first, bounded || keepRewards ? model.getLabeledStates(psiLabel) : statesWithProbability01.second, phiLabel, psiLabel, bisimulationType == BisimulationType::WeakDtmc); // If the model has state rewards, we need to consider them, because otherwise reward properties are not // preserved.