search

overturetool / overture

The Overture Tool
http://overturetool.org
GNU General Public License v3.0
49 stars 25 forks source link

Problem evaluating large trace #771

Open jonaskrask opened 3 years ago

jonaskrask commented 3 years ago

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

  1. Import LUHNSL
  2. Change trace First1000 as described
  3. 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

Additional Information

nickbattle commented 3 years ago

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 commented 3 years ago

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.

image

nickbattle commented 3 years ago

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 commented 3 years ago

The VS Code/VDMJ combination use around 2.5GB of memory and takes 15 min to complete the evaluation. image