Uppaal is a new tool suit for automatic verification of networks oftimed automata. In this paper we describe the diagnostic model-checking featureof Uppaal and illustrates its usefulness through the debugging of (a versionof) the Philips Audio-Control Protocol. Together with a graphical interface ofUppaal this diagnostic feature allows for a number of errors to be more easilydetected and corrected.