Use heuristic NONE to explore complete state space

Former-commit-id: 25990b5dda

src/builder/ExplicitDFTModelBuilderApprox.cpp

@@ -33,12 +33,12 @@ namespace storm {
                 matrixBuilder(!generator.isDeterministicModel()),
                 stateStorage(((dft.stateVectorSize() / 64) + 1) * 64),
                 // TODO Matthias: make choosable
-                //explorationQueue(dft.nrElements()+1, 0, 1)
-                explorationQueue(1001, 0, 0.001)
+                explorationQueue(dft.nrElements()+1, 0, 1)
+                //explorationQueue(1001, 0, 0.001)
         {
             // Intentionally left empty.
             // TODO Matthias: remove again
-            heuristic = storm::builder::ApproximationHeuristic::PROBABILITY;
+            heuristic = storm::builder::ApproximationHeuristic::NONE;
         }
 
         template<typename ValueType, typename StateType>
@@ -266,8 +266,8 @@ namespace storm {
                 // Try to explore the next state
                 generator.load(currentState);
 
-                if (nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
-                //if (currentExplorationHeuristic->isSkip(approximationThreshold)) {
+                //if (nrExpandedStates > approximationThreshold && !currentExplorationHeuristic->isExpand()) {
+                if (currentExplorationHeuristic->isSkip(approximationThreshold)) {
                     // Skip the current state
                     ++nrSkippedStates;
                     STORM_LOG_TRACE("Skip expansion of state: " << dft.getStateString(currentState));

src/builder/ExplicitDFTModelBuilderApprox.h

@@ -28,7 +28,7 @@ namespace storm {
 
             using DFTStatePointer = std::shared_ptr<storm::storage::DFTState<ValueType>>;
             // TODO Matthias: make choosable
-            using ExplorationHeuristic = DFTExplorationHeuristicProbability<ValueType>;
+            using ExplorationHeuristic = DFTExplorationHeuristicNone<ValueType>;
             using ExplorationHeuristicPointer = std::shared_ptr<ExplorationHeuristic>;
 
 

src/storage/BucketPriorityQueue.h

@@ -13,7 +13,7 @@ namespace storm {
         template<typename ValueType>
         class BucketPriorityQueue {
 
-            using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicProbability<ValueType>>;
+            using HeuristicPointer = std::shared_ptr<storm::builder::DFTExplorationHeuristicNone<ValueType>>;
 
         public:
             explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket);

src/storage/dft/DFTState.cpp

@@ -323,7 +323,7 @@ namespace storm {
                         mCurrentlyFailableBE.push_back(elem);
                         // Remove from not failable BEs
                         auto it = std::find(mCurrentlyNotFailableBE.begin(), mCurrentlyNotFailableBE.end(), elem);
-                        STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element not found.");
+                        STORM_LOG_ASSERT(it != mCurrentlyNotFailableBE.end(), "Element " << elem << " not found.");
                         mCurrentlyNotFailableBE.erase(it);
                     }
                 } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) {