overture icon indicating copy to clipboard operation
overture copied to clipboard

Interpreter crash during model initialization does not get reported

Open peterwvj opened this issue 10 years ago • 1 comments

If you execute the VDM-SL spec below (using DEFAULT`f() as the entry) then the interpreter dies silently and no result is output to the console.

The problems happens during the initialization of the model where the interpreter tries to compute all members for the expression "set of A" which is the power-set of the type A. Since type A has (3_3) * (3_3) = 81 members the number of members for "set of A" are 2^81, which becomes too much for the interpreter to handle.

types

T = <C> | <B> | <A>;

A = (T * T) * (T * T);

values

xs = let s: set of A in s;

functions

f: () -> nat
f() == 1;

peterwvj avatar Jun 18 '14 17:06 peterwvj

This is a side effect of #136

lausdahl avatar Aug 14 '14 12:08 lausdahl