From 1bfd9747957838406ddb033ac093ad99d0793902 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 18 Oct 2016 15:58:43 +0200
Subject: [PATCH] Minor fixes

Former-commit-id: 9344ebe5aac6a410ae5e84b4230037401c2946f3
---
 src/builder/ExplicitDFTModelBuilderApprox.cpp | 19 +++++++++++++++----
 src/generator/DftNextStateGenerator.cpp       |  4 ----
 src/modelchecker/dft/DFTModelChecker.cpp      |  2 +-
 3 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/builder/ExplicitDFTModelBuilderApprox.cpp b/src/builder/ExplicitDFTModelBuilderApprox.cpp
index 5acf60980..fda689be7 100644
--- a/src/builder/ExplicitDFTModelBuilderApprox.cpp
+++ b/src/builder/ExplicitDFTModelBuilderApprox.cpp
@@ -75,12 +75,16 @@ namespace storm {
                 STORM_LOG_ASSERT(stateStorage.initialStateIndices.size() == 1, "Only one initial state assumed.");
                 initialStateIndex = stateStorage.initialStateIndices[0];
                 STORM_LOG_TRACE("Initial state: " << initialStateIndex);
-
+                // Initialize heuristic values for inital state
+                statesNotExplored.at(initialStateIndex)->setHeuristicValues(0, storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
             } else {
                 initializeNextIteration();
             }
 
             switch (heuristic) {
+                case storm::builder::ApproximationHeuristic::NONE:
+                    // Do not change anything
+                    break;
                 case storm::builder::ApproximationHeuristic::DEPTH:
                     approximationThreshold = iteration;
                     break;
@@ -246,6 +250,7 @@ namespace storm {
                 matrixBuilder.newRowGroup();
 
                 // Try to explore the next state
+                bool fixQueue = false;
                 generator.load(currentState);
 
                 if (currentState->isSkip(approximationThreshold, heuristic)) {
@@ -270,15 +275,21 @@ namespace storm {
                         for (auto const& stateProbabilityPair : choice) {
                             // Set transition to state id + offset. This helps in only remapping all previously skipped states.
                             matrixBuilder.addTransition(matrixBuilder.mappingOffset + stateProbabilityPair.first, stateProbabilityPair.second);
-                            // TODO Matthias: set heuristic values here
+                            // Set heuristic values for reached states
+                            auto iter = statesNotExplored.find(stateProbabilityPair.first);
+                            if (iter != statesNotExplored.end()) {
+                                iter->second->setHeuristicValues(currentState, stateProbabilityPair.second, choice.getTotalMass());
+                                fixQueue = true;
+                            }
                         }
                         matrixBuilder.finishRow();
                     }
                 }
 
                 // Update priority queue
-                // TODO Matthias: only when necessary
-                explorationQueue.fix();
+                if (fixQueue) {
+                    explorationQueue.fix();
+                }
             } // end exploration
         }
 
diff --git a/src/generator/DftNextStateGenerator.cpp b/src/generator/DftNextStateGenerator.cpp
index e61e8e331..69fca22b4 100644
--- a/src/generator/DftNextStateGenerator.cpp
+++ b/src/generator/DftNextStateGenerator.cpp
@@ -20,7 +20,6 @@ namespace storm {
         template<typename ValueType, typename StateType>
         std::vector<StateType> DftNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
             DFTStatePointer initialState = std::make_shared<storm::storage::DFTState<ValueType>>(mDft, mStateGenerationInfo, 0);
-            initialState->setHeuristicValues(0, storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
 
             // Register initial state
             StateType id = stateToIdCallback(initialState);
@@ -158,10 +157,8 @@ namespace storm {
                         ValueType remainingProbability = storm::utility::one<ValueType>() - probability;
                         choice.addProbability(unsuccessfulStateId, remainingProbability);
                         STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability);
-                        unsuccessfulState->setHeuristicValues(state, remainingProbability, storm::utility::one<ValueType>());
                     }
                     result.addChoice(std::move(choice));
-                    newState->setHeuristicValues(state, probability, storm::utility::one<ValueType>());
                 } else {
                     // Failure is due to "normal" BE failure
                     // Set failure rate according to activation
@@ -174,7 +171,6 @@ namespace storm {
                     STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0.");
                     choice.addProbability(newStateId, rate);
                     STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " failure rate " << rate);
-                    newState->setHeuristicValues(state, rate, choice.getTotalMass());
                 }
 
                 ++currentFailable;
diff --git a/src/modelchecker/dft/DFTModelChecker.cpp b/src/modelchecker/dft/DFTModelChecker.cpp
index 1fa1ca245..cadc37ac7 100644
--- a/src/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/modelchecker/dft/DFTModelChecker.cpp
@@ -204,7 +204,7 @@ namespace storm {
                 if (approximationError >= 0.0) {
                     storm::builder::ExplicitDFTModelBuilderApprox<ValueType> builder(dft, symmetries, enableDC);
                     typename storm::builder::ExplicitDFTModelBuilderApprox<ValueType>::LabelOptions labeloptions; // TODO initialize this with the formula
-                    builder.buildModel(labeloptions, true);
+                    builder.buildModel(labeloptions, 0);
                     model = builder.getModel();
                 } else {
                     storm::builder::ExplicitDFTModelBuilder<ValueType> builder(dft, symmetries, enableDC);