William Schultz

ALIAS expression in config appears to be ignored when error trace is printed

5

It appears that the [ALIAS expression](https://github.com/tlaplus/tlaplus/issues/485) included in a config file is being ignored when an error trace is printed on an invariant violation. It's possible I am using this...

Ability to export TLC state graph in JSON format

6

In some cases it would be helpful to have the ability to export the state graph generated by TLC in an easily parseable format (e.g. JSON) for use by other...

TLC reports varying number of distinct states per run

9

I noticed a discrepancy in the number of distinct states reported by TLC over multiple runs of the same spec and model. I have attached a folder with a repro...

It appears that `nearley-unparse` will generate strings that violate a grammar when a postprocessor is used to explicitly reject certain strings. Here is a small example: ``` Main -> boolval...

Consider adding a more explicit section on "deadlocks" in TLA+

3

People often seem to get tripped up by the semantics of what a deadlock is in TLA+ and how TLC checks for it. For example, see [this thread](https://groups.google.com/g/tlaplus/c/-vy59p38qTk) and [this...

Inline interactive/executable TLA+

1

My understanding is that you are working on an overhaul of this site, so I am posting this note as a possible feature you might be interested in including in...

Unit tests in `FiniteSetsExtTests` rely on specific line numbers

1

[These unit tests](https://github.com/tlaplus/CommunityModules/blob/3621b586922fed2a9ea8e5002c22500f4c14e477/tests/FiniteSetsExtTests.tla#L98-L108) in `FiniteSetsExtTests` rely on specific line numbers of statements in the `FiniteSetsExt.tla` module. So, if one tries to modify `FiniteSetsExt.tla` in a way that shifts existing statements...

Solver timeout isn't respected properly

1

When using the `--stretch` parameter of `tlapm`, the resulting timeouts for the backend solvers don't seem to respected properly. See the following output from the attached repro ([tlapm-timeout-repro.zip](https://github.com/tlaplus/tlapm/files/7438793/tlapm-timeout-repro.zip)): ``` $...

SMT backend encounters 'Queue.nth: internal error'

4

I encountered a `Queue.nth: internal error` message when trying to prove a simple TLAPS theorem using an SMT backend. I first noticed this in the Toolbox, but also reproduced it...

Complete support for module semantics

7

For the use cases I envision, I was not planning to implement full blown semantics of modules and module imports e.g. `EXTENDS`, etc. For example, for now I'm just considering...