If one declares an array of channels and uses these as arguments for instantiating process templates the engine crashes if this is out of range. The link above has a very simple model that demonstrates the problem. The model can be sytax checked without errors but when one tries to enter the simulator or verifier or when opening the model (perhaps when building the location vector?) the server crashes. Global declarations: const N 1; chan c[N]; Process assignments: P1 := P(c[0]); P2 := P(c[1]); System definition: system P1, P2;
Problem confirmed. I could not reproduce the crash on Linux, but the parser should create an error message in this case (which it doesn't at the moment).
Turns out that the problem is not caused by the use of the array arguments on template channel parameters. The problem is that Transition::getSync() is used without catching the CannotEvaluateExpression exception which might be thrown as a consequence of evaluating the synchronisation expression. This will happen in the situation described in the bug report, but can be trigered in a number of different ways (e.g. doing something like c[i >> j] for j==-1 directly on the edge would also crash the engine). I will work on a fix for this problem. Unfortunately, we cannot give an error message in the editor for this problem. This requires static range checking in the parser, which we cannot do at the moment. The command line tool will print warnings for these problems during verification.
A fix has been checked into CVS. As mentioned above, we cannot at the moment produce a range check error during syntax checking. For the example linked to in the URL field, the 'failing' edge (the one which causes the out-of-bounds error) is simply disabled. This is consistent with how similar problems with guards and assignments are handled. The command line tools will issue a warning.