Matthias Volk
					
					5 years ago
					
				 
				
			 
		 
		
			
				
				  
				  No known key found for this signature in database
				  
				  	
						GPG Key ID: 83A57678F739FCD3
				  	
				  
				
			
		
		
		
	
		
			
				 2 changed files with 
5 additions and 
5 deletions
			 
			
		 
		
			
				- 
					
					
					 
					doc/source/doc/reward_models.rst
				
 
			
				- 
					
					
					 
					examples/reward_models/01-reward-models.py
				
 
			
		
		
			
				
					
					
						
							
								
									
										
											
	
		
			
				
					| 
						
						
							
								
							
						
						
					 | 
				
				 | 
				
					@ -28,8 +28,8 @@ We can do model checking analogous to probabilities:: | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					
 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    >>> initial_state = model.initial_states[0] | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    >>> result = stormpy.model_checking(model, properties[0]) | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    >>> print("Result: {}".format(result.at(initial_state))) | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    Result: 3.666666666666667 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    >>> print("Result: {}".format(round(result.at(initial_state), 6))) | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    Result: 3.666667 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					
 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					
 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					The reward model has a name which we can obtain as follows:: | 
				
			
			
		
	
	
		
			
				
					| 
						
							
								
							
						
						
						
					 | 
				
				 | 
				
					
  | 
				
			
			
		
	
										
									
								
							
						 
					 
				 
			
		
			
				
					
					
						
							
								
									
										
											
	
		
			
				
					| 
						
						
							
								
							
						
						
					 | 
				
				 | 
				
					@ -10,11 +10,11 @@ def example_reward_models_01(): | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    prop = "R=? [F \"done\"]" | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    properties = stormpy.parse_properties_for_prism_program(prop, program, None) | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    model = stormpy.build_model(program, properties) | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    assert len(model.reward_models) == 1 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    initial_state = model.initial_states[0] | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    result = stormpy.model_checking(model, properties[0]) | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    print("Result: {}".format(result.at(initial_state))) | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    print("Result: {}".format(round(result.at(initial_state), 6))) | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					
 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    assert len(model.reward_models) == 1 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    reward_model_name = list(model.reward_models.keys())[0] | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    print(reward_model_name) | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    assert reward_model_name == "coin_flips" | 
				
			
			
		
	
	
		
			
				
					| 
						
						
						
							
								
							
						
					 | 
				
				 | 
				
					@ -29,4 +29,4 @@ def example_reward_models_01(): | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    assert reward_model_name == "coin_flips" | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					
 | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					if __name__ == '__main__': | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    example_reward_models_01() | 
				
			
			
		
	
		
			
				
					 | 
					 | 
				
				 | 
				
					    example_reward_models_01() |