I set up a model with UPPAAL and i used the verifier to check for a deadlock. The answer is: Property not satisfied. Thus there exists a deadlock.
Is there a way in UPPAAL to report more detailled information about the deadlock such as the state and the current values of all variables in the specific situation?
yes. we can trace deadlock in UPPAAL i-e we can find the states or path that is causing deadlock. Go to option--> diagnostic trace --> fastest. you can select any one of these option some/fastest/shortest in diagnostic trace. After selecting fastest. Go to verifier and check deadlock lock property. Store new trace in simulation by selecting "yes" after this go to simulator, it will show you the new store trace that is making property unsatisfiable. Hope it will be helpfull