Validate that VDM examples work with the extension

[jonaskrask]

The VDM examples where downloaded from the overture list. However, it has never been validated that they all work with the extension.

Projects that are unable to run should be found and changed to allow execution from the extension.

[jonaskrask]

Perhaps we should also include one or more run configurations and settings for each example, to show how that works.

Especially for remote control projects.

[nickbattle]

Yes, ideally they should just install and be runnable.

Incidentally, whenever I install from examples, I'm always very confused about where the project will be installed. I usually end up adding it inside another one or outside the workspace completely. Can that be clarified somehow?

[jonaskrask]

SL/ACSSL cannot initialise the interpreter, fails with error: java.lang.Exception: Internal error: Java heap space

I have tried increasing the heap size to 8 GB, but that was not enough.

(Overture has the same issue)

[nickbattle]

I think I looked at this in the past and decided it was just the way the spec was written. But I'll take another look...

[nickbattle]

Yeah, it's the spec. In the "old days" this would not have been executable, but it is trying to evaluate this:

exceptions_hd1_1:set of (Table_Co_ordinate) = let s:set of (Table_Co_ordinate) in s

If you look at the definition of Table_Co_ordinate, you'll see that it is a complex mix of product types and unions, but all of the components are finite types. So in theory this set can be evaluated, but ... it's enormous(!).

RelOrientation = <PERP> | <FACING> | <AWAY>;

OrientedExs = Exs_types * (RelOrientation | <NONE>)
inv mk_(exs,ro) ==
  not is_Storage_building(exs) <=> (ro = <NONE>);

OrientedPes = Pes_types * (RelOrientation | <NONE>)
inv mk_(pes,ro) ==
  pes <> <EARTHCOVEREDBUILDING> <=> (ro = <NONE>);

Table_Co_ordinate = OrientedExs * OrientedPes

So we know why... but perhaps we should do something, like add a deliberate error in the spec so that it fails early and leaves the user looking at a line that says, "This spec cannot be evaluated" or something?

Perhaps more generally, we could think about a flag that allows specs to be labelled as "do not interpret"?

[jonaskrask]

Ahh okay, I guess we can just delete the "Entry" and launch configuration for the spec and write in the README that you cannot interpret the spec?

[nickbattle]

Yes, that would be a reasonable compromise, for now.