| Summary: | TIGA properties cannot be checked for systems with strict invariants for learning queries. | ||
|---|---|---|---|
| Product: | UPPAAL Stratego | Reporter: | Jakob Haahr Taankvist <jht> |
| Component: | Engine | Assignee: | Marius Mikučionis <marius> |
| Status: | ASSIGNED --- | ||
| Severity: | normal | ||
| Priority: | P5 | ||
| Version: | 4.1.20-pre4 | ||
| Hardware: | PC | ||
| OS: | Linux | ||
| Architecture: | |||
| Attachments: | Minimal example | ||
Created attachment 312 [details] Minimal example When having a strict invariant in a model and attempting to learn on it I get the error "TIGA properties cannot be checked for systems with strict invariants.". This does not make sense in (at least) two ways, first, it's not a Tiga query but a learning query. Secondly the strict invariant is between two integers, this should never be a problem as it can simply be considered a guard on all incoming transitions (at least in Uppaal Tiga) Another issue is that I get a warning in the model, again, this should not be an error as it's two integers. I have tested in Uppaal stratego: pre3, pre4 and "My development version" I attach a small example exhibiting the bug.