From 869f8c50c954eea9c7544d816051e879e315d9d6 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 10 Apr 2015 11:49:20 +0200 Subject: [PATCH] Fixed some minor CTMC-related bugs. Former-commit-id: 3abb948542b4c5af86302e941626c7344f7b2c4a --- src/modelchecker/csl/HybridCtmcCslModelChecker.cpp | 4 ---- src/modelchecker/csl/SparseCtmcCslModelChecker.cpp | 6 +++--- src/storage/dd/CuddOdd.cpp | 4 +++- .../modelchecker/GmmxxCtmcCslModelCheckerTest.cpp | 4 ++-- .../modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp | 8 ++++---- .../modelchecker/SparseCtmcCslModelCheckerTest.cpp | 4 ++-- 6 files changed, 14 insertions(+), 16 deletions(-) diff --git a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp index c8a397b39..e371ad8ce 100644 --- a/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -228,9 +228,6 @@ namespace storm { HybridQuantitativeCheckResult hybridResult(this->getModel().getReachableStates(), psiStates || (!statesWithProbabilityGreater0 && this->getModel().getReachableStates()), psiStates.toAdd(), statesWithProbabilityGreater0NonPsi, odd, subResult); - // Determine the set of states that achieved a strictly positive probability. - std::unique_ptr statesWithValuesGreaterZero = hybridResult.compareAgainstBound(storm::logic::ComparisonType::Greater, storm::utility::zero()); - // Compute the set of relevant states. storm::dd::Bdd relevantStates = statesWithProbabilityGreater0 && phiStates; @@ -240,7 +237,6 @@ namespace storm { // Build an ODD for the relevant states. odd = storm::dd::Odd(relevantStates); - std::vector result; std::unique_ptr explicitResult = hybridResult.toExplicitQuantitativeCheckResult(); std::vector newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult().getValueVector()); diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 6fa6703ca..ecd550f4c 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -187,9 +187,9 @@ namespace storm { storm::storage::BitVector relevantStates = statesWithProbabilityGreater0 & phiStates; std::vector newSubresult = std::vector(relevantStates.getNumberOfSetBits()); - storm::utility::vector::selectVectorValues(newSubresult, statesWithProbabilityGreater0NonPsi % relevantStates, subresult); + storm::utility::vector::setVectorValues(newSubresult, statesWithProbabilityGreater0NonPsi % relevantStates, subresult); storm::utility::vector::setVectorValues(newSubresult, psiStates % relevantStates, storm::utility::one()); - + // Then compute the transient probabilities of being in such a state after t time units. For this, // we must re-uniformize the CTMC, so we need to compute the second uniformized matrix. uniformizationRate = storm::utility::zero(); @@ -312,7 +312,7 @@ namespace storm { if (computeCumulativeReward) { result = std::vector(values.size()); std::function scaleWithUniformizationRate = [&uniformizationRate] (ValueType const& a) -> ValueType { return a / uniformizationRate; }; - storm::utility::vector::applyPointwise(result, result, scaleWithUniformizationRate); + storm::utility::vector::applyPointwise(values, result, scaleWithUniformizationRate); } else { result = std::vector(values.size()); } diff --git a/src/storage/dd/CuddOdd.cpp b/src/storage/dd/CuddOdd.cpp index d78882b2f..29301957e 100644 --- a/src/storage/dd/CuddOdd.cpp +++ b/src/storage/dd/CuddOdd.cpp @@ -113,7 +113,9 @@ namespace storm { void Odd::expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd const& oldOdd, std::vector const& oldValues, uint_fast64_t newOffset, storm::dd::Odd const& newOdd, std::vector& newValues) { if (oldOdd.isTerminalNode()) { STORM_LOG_THROW(newOdd.isTerminalNode(), storm::exceptions::InvalidArgumentException, "The ODDs for the translation must have the same height."); - newValues[newOffset] += oldValues[oldOffset]; + if (oldOdd.getThenOffset() != 0) { + newValues[newOffset] += oldValues[oldOffset]; + } } else { expandValuesToVectorRec(oldOffset, oldOdd.getElseSuccessor(), oldValues, newOffset, newOdd.getElseSuccessor(), newValues); expandValuesToVectorRec(oldOffset + oldOdd.getElseOffset(), oldOdd.getThenSuccessor(), oldValues, newOffset + newOdd.getElseOffset(), newOdd.getThenSuccessor(), newValues); diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index f874bafef..e2a97ca5f 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -53,7 +53,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.001105335651650576, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); checkResult = modelchecker.check(*formula); @@ -139,7 +139,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(2.7720429852369946, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); } TEST(GmmxxCtmcCslModelCheckerTest, Polling) { diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index e7e224603..522e61691 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -60,8 +60,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(0.001112543139248814, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(0.001112543139248814, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision()); formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); checkResult = modelchecker.check(*formula); @@ -163,8 +163,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult()); checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult(ctmc->getReachableStates(), ctmc->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult(); - EXPECT_NEAR(2.7720429852369946, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); - EXPECT_NEAR(2.7720429852369946, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision()); } TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling) { diff --git a/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp index a5fc3d8f9..89ae9b08b 100644 --- a/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp @@ -53,7 +53,7 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) { ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(0.001105335651650576, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]"); checkResult = modelchecker.check(*formula); @@ -139,7 +139,7 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) { ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); storm::modelchecker::ExplicitQuantitativeCheckResult quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult(); - EXPECT_NEAR(2.7720429852369946, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); + EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision()); } TEST(SparseCtmcCslModelCheckerTest, Polling) {