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(), storm::utility::zero()); } 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 std::vector DftNextStateGenerator::getInitialStates(StateToIdCallback const& stateToIdCallback) { DFTStatePointer initialState = std::make_shared>(mDft, mStateGenerationInfo, 0); - initialState->setHeuristicValues(0, storm::utility::zero(), storm::utility::zero()); // Register initial state StateType id = stateToIdCallback(initialState); @@ -158,10 +157,8 @@ namespace storm { ValueType remainingProbability = storm::utility::one() - probability; choice.addProbability(unsuccessfulStateId, remainingProbability); STORM_LOG_TRACE("Added transition to " << unsuccessfulStateId << " with remaining probability " << remainingProbability); - unsuccessfulState->setHeuristicValues(state, remainingProbability, storm::utility::one()); } result.addChoice(std::move(choice)); - newState->setHeuristicValues(state, probability, storm::utility::one()); } 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 builder(dft, symmetries, enableDC); typename storm::builder::ExplicitDFTModelBuilderApprox::LabelOptions labeloptions; // TODO initialize this with the formula - builder.buildModel(labeloptions, true); + builder.buildModel(labeloptions, 0); model = builder.getModel(); } else { storm::builder::ExplicitDFTModelBuilder builder(dft, symmetries, enableDC);