|Summary:||Can not automatically get counter example if not satisfied|
|Component:||Engine||Assignee:||Alexandre David <adavid>|
Description 吴居宜 2013-02-17 14:54:12 CET
Even the train example or the bridge example. I don't know how to set to get a counter example automatically when it is not satisfied. Tutorial on uppaal does not mentioned anything about it. Please help me...Thank you very much. email@example.com
Comment 1 Francesco Spegni 2013-11-21 17:55:33 CET
Did you checked the option in menu: Options -> Diagnostic Trace -> Some ? (or anyone except "None") By default it is not checked, and it is tricky for a newbie to understand that without it the counterexample is not generated. Wouldn't be better if Uppaal, by default, did generate a counterexample?