From 91084a5da4b1954c3dab0ddcc657f0894cdd2831 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 28 Nov 2014 11:14:55 +0100 Subject: [PATCH 1/2] 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 554287e0828dbe72cdf1ede39c8dce2dbe6fcada Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 16 Dec 2014 09:59:20 +0100 Subject: [PATCH 2/2] 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.