This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 546

Summary: Can not automatically get counter example if not satisfied
Product: UPPAAL Reporter: 吴居宜 <fireuc>
Component: EngineAssignee: Alexandre David <adavid>
Status: NEW ---    
Severity: minor CC: francesco.spegni
Priority: P5    
Version: 4.1.13   
Hardware: PC   
OS: Windows XP   
Architecture:

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.

fireuc@gmail.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?