Model checking status page has only one entry in the States column

[xosmig]

Hi!

I tried to model-check a simple specification using the TLA+ extension.
On the model checking status page, the "Coverage" column is periodically updated as expected.
However, the "States" column always contains just one entry, although the model checker has been running for several minutes.
Please see the screenshot below.

Here is the corresponding .out file:

MC_n4_t1_f1_InitByz1.out.txt

For comparison, here is a screenshot of the statistics page from the TLA+ toolbox:

I would expect the extension output to also contain multiple entries in the "States" column.
Could you please help me to identify whether I am doing something wrong or if it is a bug in the plugin?

Thanks in advance.

[xosmig]

This may be related to these weird question marks in the TLC output. I guess it is some encoding-related problem.
I probably should file a bug to TLC.

[lemmy]

@xosmig What is your locale?

[xosmig]

I have Russian locale. The question marks are non-breakable spaces (ascii 160).

It seems that, when the system language is set to Russian, windows uses the non-breakable space as the default separator for groups of digits.

However, changing the separator or even disabling digit grouping altogether in windows settings doesn't seem to affect the output of TLC. I guess TLC doesn't use the system's settings and just uses non-breakable spaces for all locales.

[xosmig]

It seems that the reason why VS-code doesn't display these spaces correctly is that TLC outputs the text encoded in Windows-1252, but VS-code tries to interpret it in UTF-8. This may also explain why the tla+ extension is unable to parse the output.

[xosmig]

Changing the output encoding of TLC to UTF-8 (adding "-Dfile.encoding=UTF-8" to the jvm parameters) fixes the way output is displayed in VS-code, but doesn't fix the problem with the TLC Status page.

[alygin]

@lemmy, I think the best way to fix it is to change how TLC formats numbers in its output (to not format them at all). Since the only way to analyze model checking results is to parse TLC output, it would be nice to have this output independent of the user locale to make parsers more reliable. Is it possible?

[lemmy]

I suppose we could remove the formatting when TLC runs with the -tool flag. However, it would be inconsistent to still format dates according to the locale. At any rate, somebody would have to provide a pull request for TLC.

[alygin]

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

[xosmig]

Thanks!
This fixes the problem for me.