Set correct order for priorities according to heuristic

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) {

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;

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;
 
         };
 

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);