From f2e9d20a8de8b921c8d45ca39b563ad2f48dc4c7 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Fri, 22 Mar 2019 19:04:01 +0100
Subject: [PATCH] Set correct order for priorities according to heuristic
---
.../builder/ExplicitDFTModelBuilder.cpp | 16 ++++++++++++++--
src/storm-dft/storage/BucketPriorityQueue.cpp | 2 +-
src/storm-dft/storage/BucketPriorityQueue.h | 16 +++++++++-------
src/test/storm-dft/api/DftApproximationTest.cpp | 2 +-
4 files changed, 25 insertions(+), 11 deletions(-)
diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
index 2ecabe6e4..eb7d50e06 100644
--- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp
@@ -60,8 +60,7 @@ namespace storm {
generator(dft, *stateGenerationInfo, enableDC, mergeFailedStates),
matrixBuilder(!generator.isDeterministicModel()),
stateStorage(dft.stateBitVectorSize()),
- //explorationQueue(dft.nrElements()+1, 0, 1)
- explorationQueue(200, 0, 0.9, false)
+ explorationQueue(1, 0, 0.9, false)
{
// Compute independent subtrees
if (dft.topLevelType() == storm::storage::DFTElementType::OR) {
@@ -126,6 +125,19 @@ namespace storm {
if (iteration < 1) {
// Initialize
+ switch (usedHeuristic) {
+ case storm::builder::ApproximationHeuristic::DEPTH:
+ explorationQueue = storm::storage::BucketPriorityQueue<ExplorationHeuristic>(dft.nrElements()+1, 0, 0.9, false);
+ break;
+ case storm::builder::ApproximationHeuristic::PROBABILITY:
+ explorationQueue = storm::storage::BucketPriorityQueue<ExplorationHeuristic>(200, 0, 0.9, true);
+ break;
+ case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE:
+ explorationQueue = storm::storage::BucketPriorityQueue<ExplorationHeuristic>(200, 0, 0.9, true);
+ break;
+ default:
+ STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Heuristic not known.");
+ }
modelComponents.markovianStates = storm::storage::BitVector(INITIAL_BITVECTOR_SIZE);
if(mergeFailedStates) {
diff --git a/src/storm-dft/storage/BucketPriorityQueue.cpp b/src/storm-dft/storage/BucketPriorityQueue.cpp
index 3ce3659b5..ceafc00fb 100644
--- a/src/storm-dft/storage/BucketPriorityQueue.cpp
+++ b/src/storm-dft/storage/BucketPriorityQueue.cpp
@@ -87,7 +87,7 @@ namespace storm {
}
} else {
// Move to new bucket
- STORM_LOG_ASSERT(newBucket < oldBucket, "Will update to higher bucket");
+ STORM_LOG_ASSERT(newBucket < oldBucket, "Will update item "<< item->getId() << " from " << oldBucket << " to higher bucket " << newBucket);
if (newBucket < currentBucket) {
currentBucket = newBucket;
nrUnsortedItems = 0;
diff --git a/src/storm-dft/storage/BucketPriorityQueue.h b/src/storm-dft/storage/BucketPriorityQueue.h
index 2c0c3cb37..51a2ec94c 100644
--- a/src/storm-dft/storage/BucketPriorityQueue.h
+++ b/src/storm-dft/storage/BucketPriorityQueue.h
@@ -30,6 +30,10 @@ namespace storm {
*/
explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double ratio, bool higher);
+ BucketPriorityQueue(BucketPriorityQueue const& queue) = default;
+
+ virtual ~BucketPriorityQueue() = default;
+
void fix();
/*!
@@ -106,18 +110,16 @@ namespace storm {
std::function<bool(PriorityTypePointer, PriorityTypePointer)> compare;
// Minimal value
- const double lowerValue;
+ double lowerValue;
- const bool higher;
+ bool higher;
- const bool AUTOSORT = false;
+ bool AUTOSORT = false;
- const double logBase;
+ double logBase;
// Number of available buckets
- const size_t nrBuckets;
-
-
+ size_t nrBuckets;
};
diff --git a/src/test/storm-dft/api/DftApproximationTest.cpp b/src/test/storm-dft/api/DftApproximationTest.cpp
index f552fa608..d00973da1 100644
--- a/src/test/storm-dft/api/DftApproximationTest.cpp
+++ b/src/test/storm-dft/api/DftApproximationTest.cpp
@@ -90,7 +90,7 @@ namespace {
TYPED_TEST(DftApproximationTest, HecsTimebound) {
//double errorBound = 0.01;
- double errorBound = 0.5;
+ double errorBound = 0.1;
double timeBound = 100;
std::pair<double, double> approxResult = this->analyzeTimebound(STORM_TEST_RESOURCES_DIR "/dft/hecs_3_2_2_np.dft", timeBound, errorBound);
EXPECT_LE(approxResult.first, 0.0410018417);