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

Bug 392 - Wrongful interpretation of query over automatically instantiated templates with select expressions
Summary: Wrongful interpretation of query over automatically instantiated templates wi...
Status: ASSIGNED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.5
Hardware: PC All
: P2 critical
Assignee: Gerd Behrmann
URL:
Depends on:
Blocks:
 
Reported: 2007-02-19 12:11 CET by Jacob Illum
Modified: 2007-05-13 18:11 CEST (History)
0 users

See Also:
Architecture:


Attachments
The model (2.44 KB, text/xml)
2007-02-19 12:12 CET, Jacob Illum
Details
The query (153 bytes, application/octet-stream)
2007-02-19 12:13 CET, Jacob Illum
Details

Note You need to log in before you can comment on or make changes to this bug.
Description Jacob Illum 2007-02-19 12:11:48 CET
The two queries evaluate differently, but given the way the model is constructed, the evaluation should be identical. 

- One query test on all instantiations will reach the 'complete' location.
- The other tests the boolean array done, which is only altered upon entering the 'complete' location.

Thus, the two expressions should evaluate identically, but the former returns false, whereas the latter returns true. Random simulation will even lead to satisfaction of the former query.
Comment 1 Jacob Illum 2007-02-19 12:12:49 CET
Created attachment 143 [details]
The model
Comment 2 Jacob Illum 2007-02-19 12:13:13 CET
Created attachment 144 [details]
The query
Comment 3 Gerd Behrmann 2007-02-19 15:09:43 CET
The problem is in the automatic instantiation of templates. 

If P(i) is a template, then P is internally treated as an array of processes with i being an index. This assumes that all instances of P have the same footprint. In the test case, this is not the case: The process argument is used in the select expression. Since the select expression is being unfolded into a number of edges, this means that the number of syntactic function calls varies between instances of P. Since we generate an internal variable for the return value for each syntactic function call, this has the consequence of differences in footprint.
Comment 4 Gerd Behrmann 2007-02-19 16:38:10 CET
There does not seem to be a small/simple fix for the problem. I am currently considering to disallow models that trigger the bug and postpone the real fix for 4.2.
Comment 5 Gerd Behrmann 2007-02-19 18:42:04 CET
"Fixed" on the 4.0 branch from rev. 2971. I choose to disallow models triggering the problem.

I will leave this bug open, since it needs to be fixed on the trunk.