regex issue in parsing TLC output

[giacomociti]

Hello, the output of my model checking has lines like the following

<Write1 line 20, col 1 to line 20, col 6 of module spec (21 5 22 20)>: 6:27

which are not parsed by the regex https://github.com/alygin/vscode-tlaplus/blob/031ad983023cea0bc5fba2a1a54f835fed2cfd04/src/parsers/tlc.ts#L467

and they don't show up in the coverage section of the output panel.

I think the values unexpected in the regex are (21 5 22 20)

[lemmy]

FWIW: The Toolbox parses this output in org.lamport.tla.toolbox.tool.tlc.output.data.ActionInformationItem. However, I don't think that vscode-tlaplus has the UX for users to make sense of this info. In other words, the regex can probably just ignore this piece of info.

[giacomociti]

Ok, I'm not a regex expert but maybe we can add a pattern (?: \(\d+ \d+ \d+ \d+\))? and the whole regex would be:

const regex = /^<(\w+) line (\d+), col (\d+) to line (\d+), col (\d+) of module (\w+)(?: \(\d+ \d+ \d+ \d+\))?>: (\d+):(\d+)/g;

[giacomociti]

a very simple repro of the issue:

VARIABLE s
Init == s = ""
Next == \E x \in {"a", "b"}: s' = x

the .out file contains the unexpected numbers and the coverage for Next is not shown

[alygin]

@giacomociti, thanks for the report!

[alygin]

The fix is available in the v1.6.0-alpha.2 pre-release.

[FedericoPonzi]

Closing as this seems resolved.