@ -1034,14 +1034,14 @@ namespace storm { 
			
		
	
		
			
				
					                     
			
		
	
		
			
				
					                    phiStates  =  untilFormula . getLeft ( ) . check ( modelchecker ) ;  
			
		
	
		
			
				
					                    psiStates  =  untilFormula . getRight ( ) . check ( modelchecker ) ;  
			
		
	
		
			
				
					                }  catch  ( std : : bad_cast  const &  e  )  {  
			
		
	
		
			
				
					                }  catch  ( std : : bad_cast  const & )  {  
			
		
	
		
			
				
					                    / /  If  the  nested  formula  was  not  an  until  formula ,  it  remains  to  check  whether  it ' s  an  eventually  formula .  
			
		
	
		
			
				
					                    try  {  
			
		
	
		
			
				
					                        storm : : property : : prctl : : Eventually < double >  const &  eventuallyFormula  =  dynamic_cast < storm : : property : : prctl : : Eventually < double >  const & > ( pathFormula ) ;  
			
		
	
		
			
				
					                         
			
		
	
		
			
				
					                        phiStates  =  storm : : storage : : BitVector ( labeledMdp . getNumberOfStates ( ) ,  true ) ;  
			
		
	
		
			
				
					                        psiStates  =  eventuallyFormula . getChild ( ) . check ( modelchecker ) ;  
			
		
	
		
			
				
					                    }  catch  ( std : : bad_cast  const &  e  )  {  
			
		
	
		
			
				
					                    }  catch  ( std : : bad_cast  const & )  {  
			
		
	
		
			
				
					                        / /  If  the  nested  formula  is  neither  an  until  nor  a  finally  formula ,  we  throw  an  exception .  
			
		
	
		
			
				
					                        throw  storm : : exceptions : : InvalidPropertyException ( )  < <  " Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation. " ;  
			
		
	
		
			
				
					                    }