From 19ba1c38e76bbbe57f99f27c636e55872e35fa88 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);