Skip to content

Problem evaluating large trace #771

@jonaskrask

Description

@jonaskrask

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions