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

Bug 633 - TIGA properties cannot be checked for systems with strict invariants for learning queries.
Summary: TIGA properties cannot be checked for systems with strict invariants for lear...
Status: ASSIGNED
Alias: None
Product: UPPAAL Stratego
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.1.20-pre4
Hardware: PC Linux
: P5 normal
Assignee: Marius Mikučionis
URL:
Depends on:
Blocks:
 
Reported: 2017-04-10 09:55 CEST by Jakob Haahr Taankvist
Modified: 2019-01-25 12:06 CET (History)
0 users

See Also:
Architecture:


Attachments
Minimal example (1.10 KB, text/xml)
2017-04-10 09:55 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 2017-04-10 09:55:55 CEST
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.