Removed hard limit on module initialization

[sifraser]

With a large number of VDM-SL modules (200+) with mutual dependencies we have been hitting an issue whereby the specification would parse and type check fine, but would then hit scope issues when initialising for animation.

With a bit of digging, we discovered a hard limit that we were hitting despite having a resolvable scenario. Rather than just increasing the limit, we added a problem count and allowed the initialisation to continue as long as that problem count decreased on each pass.

I have not been able to devise a mechanism to force a unit test that would have failed but now passes, but this certainly removes the blocker in our large project with failures occurring when expected. All existing tests continue to pass.

There may well be a better solution than the one proposed here, but this fix enabled us to proceed with our project using a patched tool.

[nickbattle]

This seems like an excellent suggestion! Obviously the current scheme is a rather lightweight attempt to avoid a complex dependency analysis by "doing as much as we can" and then trying again. But continuing while the problem count decreases is an improvement. I'll need to check that we can't create a situation where the first pass (say) fails on A, and then the second passes A but then fails B, and so the error count does not decrease - so it may be better to say "while it decreases, but at least N times" to cover such cases.

Thanks for submitting the change. I'll clone the same logic into VDMJ.

[nickbattle]

Incidentally, Leo Freitas had some dependency problems with a large specification a while back. We added detail to the -verbose option in VDMJ (not Overture) that prints out the detail of this loop resolution process and allowed us to add the modules in the most efficient order to avoid too much retrying during the typecheck. With extremely large projects that can save a lot of time. For example:

values  -- module A
    X = B`Y;
    Z = 123;

values -- module B
    Y = A`Z;

Parsed 2 modules in 0.072 secs. No syntax errors
Loaded ast-tc.mappings in 0.221 secs
Mapped 36 nodes with ast-tc.mappings in 0.004 secs
A`X => (B`Y)
WARNING: B`Y declared after X
B`Y => (A`Z)
Type checked 2 modules in 0.013 secs. No type errors
Loaded tc-in.mappings in 0.106 secs
Mapped 26 nodes with tc-in.mappings in 0.002 secs
Pass 1:
Error 4034: Name 'B`Y' not in scope in 'A' (x.vdm) at line 6:9
Initialized 2 modules in 0.046 secs.

Notice the two "=>" dependency indications and the WARNING. And at the end it says "Pass 1" and lists the error. That results in pass 2 to fix it, but you can see how these forward reference and dependency problems can help you to decide the order to put your modules to reduce the number of passes required.

[sifraser]

That is very interesting .. we have a lot of dependency information to hand (statically) given the way we structure our modules. I hadn't really given much thought to the order in which we passed them in, but now you say it we could certainly be much more efficient just with the information we already have and knowing the above could improve things still further, thanks!

[nickbattle]

OK, thanks again Simon. I've merged this change via a private local branch into ncb/development, which is more in line with our bugfix process. It's covered by issue #773, and should be merged in the next Overture release. I will close this PR as complete, even though it isn't merged as such.