Repository navigation
Problem evaluating large trace #771
Description
Description
We have been looking for a large trace for performance measuring the VS Code extension for VDM. However, it seems that Overture has some problems if traces get very big.
We have been trying to execute a test in the LUHNSL project that you can import from Overture. Here we have changed the First1000 trace to:
First1000:
let a,b,c,d,e,f in set {0,...,9} in
(
luhn([a]);
luhn([a,b]);
luhn([a,b,c]);
luhn([a,b,c,d]);
luhn([a,b,c,d,e]);
luhn([a,b,c,d,e,f]);
);
This generates 1000k tests, the VS Code version takes about 10 min to complete execution, the VDMJ CLI is faster.
When I try to execute it in Overture is stalls for some time before sending the console response:
LUHNSL:DEFAULT Initialized
Error CT runtime
Message: Connection error: Connection reset
Steps to Reproduce
- Import LUHNSL
- Change trace First1000 as described
- Run Full Evaluation on trace First1000
Expected behavior: The trace evaluation finishes in about 10 min
Actual behavior: Trace is not evaluated and reports "Error CT runtime"
Reproduces how often: always
Versions
Overture version: 3.0.2
OS: Windows 10 Pro version 1909
Activity
nickbattle commentedon Dec 9, 2020
The Overture setup (ie. Window/Preferences/VDM/Combinatorial Testing) has a box called "Additional VM Arguments". This allows you to set things like maximum heap that is allocated to the CT runtime. Mine is set to "-Xmx2048m", but obviously you can give the process as much memory as your machine will allow.
Is this field set in this case? If not, does setting it to something other than the default help?
jonaskrask commentedon Dec 9, 2020
The field was not set, tried to allow it 14GB of memory, it didn't get to where the connection closed, but it ate all the memory without providing any responses (didn't get to 10% done in 5 min). Overture ate the last 10GB of my harddrive so I could not run any further. I have attached an image from VisualVM if it helps.
nickbattle commentedon Dec 9, 2020
How much memory does the VS Code/VDMJ combination use during the same test run? (I'm not sure what that proves, but if it's significantly less it might indicate some sort of issue with Overture rather than just "not enough memory").
jonaskrask commentedon Dec 11, 2020
The VS Code/VDMJ combination use around 2.5GB of memory and takes 15 min to complete the evaluation.
