Andrei Tonkikh

SYMMETRY causes TLC to find (presumably, false) temporal property violation

5

I have a simple Spec with a temporal property and it passes the model checker. When I add SYMMETRY to the TLC config file, I get a warning by TLC...

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

9

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...

[Bug] backslash is interpreted as a special character

2

The backslashes ("\\") are interpreted as special characters, resulting in unexpected behaviour. E.g., `hello, \text{world}` is interpreted as `hello, [tab symbol]ext{world}` and on something like `hello, \world` it simply doesn't...