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.

Created an attachment (id=143) [details]
The model

Created an attachment (id=144) [details]
The query

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.

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.

"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.