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

Bug 392

Summary: Wrongful interpretation of query over automatically instantiated templates with select expressions
Product: UPPAAL Reporter: Jacob Illum <illum>
Component: EngineAssignee: Gerd Behrmann <behrmann>
Status: ASSIGNED ---    
Severity: critical    
Priority: P2    
Version: 4.0.5   
Hardware: PC   
OS: All   
Architecture:
Attachments: The model
The query

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.