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

Bug 599 - Wrong answer from the model checker
Summary: Wrong answer from the model checker
Status: ASSIGNED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.19
Hardware: PC Linux
: P5 normal
Assignee: Marius Mikučionis
URL:
Depends on:
Blocks:
 
Reported: 2015-09-30 11:44 CEST by Jakob Haahr Taankvist
Modified: 2015-09-30 11:51 CEST (History)
1 user (show)

See Also:
Architecture:


Attachments
Model with wrong results (1.10 KB, text/xml)
2015-09-30 11:44 CEST, Jakob Haahr Taankvist
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Jakob Haahr Taankvist 2015-09-30 11:44:54 CEST
Created attachment 281 [details]
Model with wrong results

Open the attached model 

Verify the probability of reaching Process.GOAL - this is >= 0.9.. 

Use the model checker to check if Process.GOAL is reachable - FALSE

As SMC has made runs that hit Process.GOAL, Process.GOAL must be reachable.

I think in this model the model checker is not capable of verifying the model, and it should give an error message.

Tested in UPPAAL stratego and Uppaal 4.1.19 - none of them works
Comment 1 Marius Mikučionis 2015-09-30 11:51:08 CEST
"E<> Process.GOAL" should refuse to verify such model in the first place.