Browse Source
			
			
			Set result correctly for reachability rewards in MdpInstantiationChecker
			
			
				main
			
			
		 
		
			
				
					
						
						Matthias Volk
					
					5 years ago
					
				 
				
			 
		 
		
			
				
				  
				  No known key found for this signature in database
				  
				  	
						GPG Key ID: 83A57678F739FCD3
				  	
				  
				
			
		
		
		
	
		
			
				 1 changed files with 
1 additions and 
1 deletions
			 
			
		 
		
			
				- 
					
					
					 
					src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
				
 
			
		
		
			
				
					
					
						
							
								
									
										
											
	
		
			
				
					| 
						
						
							
								
							
						
						
					 | 
				
				 | 
				
					@ -140,7 +140,7 @@ namespace storm { | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					            // Check the formula and store the result as a hint for the next call.
 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					            // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					            if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) { | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					                std::unique_ptr<storm::modelchecker::CheckResult> result = modelChecker.check(env, *this->currentCheckTask); | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					                result = modelChecker.check(env, *this->currentCheckTask); | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					                storm::storage::Scheduler<ConstantType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler(); | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					                hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()); | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					                hint.setSchedulerHint(dynamic_cast<storm::storage::Scheduler<ConstantType> const&>(scheduler)); | 
				
			
			
		
	
	
		
			
				
					| 
						
							
								
							
						
						
						
					 | 
				
				 | 
				
					
  |