| 
					
					
					
				 | 
				@ -1,6 +1,7 @@ | 
			
		
		
	
		
			
				 | 
				 | 
				#include "ExplicitDFTModelBuilder.h"
 | 
				 | 
				 | 
				#include "ExplicitDFTModelBuilder.h"
 | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				#include <map>
 | 
				 | 
				 | 
				#include <map>
 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				#include <storm/exceptions/IllegalArgumentException.h>
 | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				#include "storm/models/sparse/MarkovAutomaton.h"
 | 
				 | 
				 | 
				#include "storm/models/sparse/MarkovAutomaton.h"
 | 
			
		
		
	
		
			
				 | 
				 | 
				#include "storm/models/sparse/Ctmc.h"
 | 
				 | 
				 | 
				#include "storm/models/sparse/Ctmc.h"
 | 
			
		
		
	
	
		
			
				| 
					
						
							
						
					
					
						
							
						
					
					
				 | 
				@ -169,6 +170,8 @@ namespace storm { | 
			
		
		
	
		
			
				 | 
				 | 
				                    case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: | 
				 | 
				 | 
				                    case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: | 
			
		
		
	
		
			
				 | 
				 | 
				                        heuristic = std::make_shared<DFTExplorationHeuristicBoundDifference<ValueType>>(initialStateIndex); | 
				 | 
				 | 
				                        heuristic = std::make_shared<DFTExplorationHeuristicBoundDifference<ValueType>>(initialStateIndex); | 
			
		
		
	
		
			
				 | 
				 | 
				                        break; | 
				 | 
				 | 
				                        break; | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				                    default: | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				                        STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Heuristic not known."); | 
			
		
		
	
		
			
				 | 
				 | 
				                } | 
				 | 
				 | 
				                } | 
			
		
		
	
		
			
				 | 
				 | 
				                heuristic->markExpand(); | 
				 | 
				 | 
				                heuristic->markExpand(); | 
			
		
		
	
		
			
				 | 
				 | 
				                statesNotExplored[initialStateIndex].second = heuristic; | 
				 | 
				 | 
				                statesNotExplored[initialStateIndex].second = heuristic; | 
			
		
		
	
	
		
			
				| 
					
					
					
						
							
						
					
				 | 
				@ -184,9 +187,10 @@ namespace storm { | 
			
		
		
	
		
			
				 | 
				 | 
				                        break; | 
				 | 
				 | 
				                        break; | 
			
		
		
	
		
			
				 | 
				 | 
				                    case storm::builder::ApproximationHeuristic::PROBABILITY: | 
				 | 
				 | 
				                    case storm::builder::ApproximationHeuristic::PROBABILITY: | 
			
		
		
	
		
			
				 | 
				 | 
				                    case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: | 
				 | 
				 | 
				                    case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: | 
			
		
		
	
		
			
				 | 
				 | 
				                        double exponent = iteration; // Need conversion to avoid overflow when negating
 | 
				 | 
				 | 
				 | 
			
		
		
	
		
			
				 | 
				 | 
				                        approximationThreshold = std::pow(2, -exponent); | 
				 | 
				 | 
				 | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				                        approximationThreshold = std::pow(2, -(double)iteration); // Need conversion to avoid overflow when negating
 | 
			
		
		
	
		
			
				 | 
				 | 
				                        break; | 
				 | 
				 | 
				                        break; | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				                    default: | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				                        STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Heuristic not known."); | 
			
		
		
	
		
			
				 | 
				 | 
				                } | 
				 | 
				 | 
				                } | 
			
		
		
	
		
			
				 | 
				 | 
				            } | 
				 | 
				 | 
				            } | 
			
		
		
	
		
			
				 | 
				 | 
				            exploreStateSpace(approximationThreshold); | 
				 | 
				 | 
				            exploreStateSpace(approximationThreshold); | 
			
		
		
	
	
		
			
				| 
					
						
							
						
					
					
						
							
						
					
					
				 | 
				@ -399,6 +403,8 @@ namespace storm { | 
			
		
		
	
		
			
				 | 
				 | 
				                                        case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: | 
				 | 
				 | 
				                                        case storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE: | 
			
		
		
	
		
			
				 | 
				 | 
				                                            heuristic = std::make_shared<DFTExplorationHeuristicBoundDifference<ValueType>>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); | 
				 | 
				 | 
				                                            heuristic = std::make_shared<DFTExplorationHeuristicBoundDifference<ValueType>>(stateProbabilityPair.first, *currentExplorationHeuristic, stateProbabilityPair.second, choice.getTotalMass()); | 
			
		
		
	
		
			
				 | 
				 | 
				                                            break; | 
				 | 
				 | 
				                                            break; | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				                                        default: | 
			
		
		
	
		
			
				 | 
				 | 
				 | 
				 | 
				 | 
				                                            STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Heuristic not known."); | 
			
		
		
	
		
			
				 | 
				 | 
				                                    } | 
				 | 
				 | 
				                                    } | 
			
		
		
	
		
			
				 | 
				 | 
				
 | 
				 | 
				 | 
				
 | 
			
		
		
	
		
			
				 | 
				 | 
				                                    iter->second.second = heuristic; | 
				 | 
				 | 
				                                    iter->second.second = heuristic; | 
			
		
		
	
	
		
			
				| 
					
						
							
						
					
					
					
				 | 
				
  |