-
Notifications
You must be signed in to change notification settings - Fork 24
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