VDM-RT hangs on initalization with some operators

[nickbattle]

If you write a VDM-RT specification that makes operation calls (typically as object constructors) during the initialization phase, the VDMJ interpreter runtime will hang indefinitely if you use some time-based operators. The VSCode debug console just shows "Initialized in ...".

For example:

class A
operations
    public A: () ==> A
    A() == duration(0) skip;

end A

class Test
instance variables
    static obj : A := new A();

end Test

This produces the following:

*
* VDMJ VDM_RT Interpreter
*

Default class is Test
Initialized in ...

At this point you can only kill the session by pressing the red "stop" square, twice.

[nickbattle]

The problem here is that specification initialization is not performed in a full VDM-RT execution environment, with CPUs, buses, object threads and so on under control of a time-aware resource scheduler. Rather, it is expected that specification initialization can be achieved by simple direct evaluation within a single thread - since the intent is not "behaviour" but just to evaluate the data structures needed for the initial conditions.

So when (in the example above) a "duration" statement is reached, this puts the thread running the initialization into a waiting state, until the time indicated by the argument to duration has passed. But there is no resource scheduler running and so no concept of the movement of time at this point. So the suspended thread is never woken up and the system hangs.

[nickbattle]

Perhaps rather than looking for deep principles, the way forward here is to explicitly raise individual cases of things that you cannot do during an initialization. I've just created a assertNotInit method, which we can call from duration as well as other places, which will throw a context exception if they are attempted from initialization. That traps into the debugger, of course.

So now we "just" have to call this for things that we think you can't do during an initialization. This could be used for VDM-SL and VDM++ too, of course. I'll also need to check that it plays nice with various other tool features that execute things (QC, CT, etc), but I think that's okay.

It might also be a good idea to allow a magic override property to disable this feature, in case some legacy specifications are broken.

[nickbattle]

Here's what the test spec execution now looks like:

[nickbattle]

Currently, I've added this to duration, cycles, start and time. Note that start would affect VDM++ as well as VDM-RT.

[nickbattle]

I've added a VDMJ property to control the feature. The default is true, but setting it false will avoid these checks.

# Whether to do checks during initialization
vdmj.in.init_checks = true