-
Notifications
You must be signed in to change notification settings - Fork 25
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Problem evaluating large trace #771
Comments
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? |
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. |
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"). |
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
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
Additional Information
The text was updated successfully, but these errors were encountered: