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

Bug 546 - Can not automatically get counter example if not satisfied
Summary: Can not automatically get counter example if not satisfied
Status: NEW
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.13
Hardware: PC Windows XP
: P5 minor
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2013-02-17 14:54 CET by 吴居宜
Modified: 2013-11-21 17:55 CET (History)
1 user (show)

See Also:
Architecture:

Attachments
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
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?