diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp index 86a45235d..131c0389e 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.cpp +++ b/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::NONE; + heuristic = storm::builder::ApproximationHeuristic::PROBABILITY; } template @@ -267,8 +267,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)); diff --git a/src/builder/ExplicitDFTModelBuilderApprox.h b/src/builder/ExplicitDFTModelBuilderApprox.h index c3ffe4467..446bed6ad 100644 --- a/src/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/builder/ExplicitDFTModelBuilderApprox.h @@ -28,7 +28,7 @@ namespace storm { using DFTStatePointer = std::shared_ptr>; // TODO Matthias: make choosable - using ExplorationHeuristic = DFTExplorationHeuristicNone; + using ExplorationHeuristic = DFTExplorationHeuristicProbability; using ExplorationHeuristicPointer = std::shared_ptr; diff --git a/src/storage/BucketPriorityQueue.h b/src/storage/BucketPriorityQueue.h index 1aa18689d..253b34e19 100644 --- a/src/storage/BucketPriorityQueue.h +++ b/src/storage/BucketPriorityQueue.h @@ -13,7 +13,7 @@ namespace storm { template class BucketPriorityQueue { - using HeuristicPointer = std::shared_ptr>; + using HeuristicPointer = std::shared_ptr>; public: explicit BucketPriorityQueue(size_t nrBuckets, double lowerValue, double stepPerBucket);