| Summary: | Wrong answer from the model checker | ||
|---|---|---|---|
| Product: | UPPAAL | Reporter: | Jakob Haahr Taankvist <jht> |
| Component: | Engine | Assignee: | Marius Mikučionis <marius> |
| Status: | ASSIGNED --- | ||
| Severity: | normal | CC: | adavid |
| Priority: | P5 | ||
| Version: | 4.1.19 | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| Architecture: | |||
| Attachments: | Model with wrong results | ||
"E<> Process.GOAL" should refuse to verify such model in the first place. |
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