Markus Alexander Kuppe

Related: ["Model-checking embedded systems with probabilistic nondeterminism"](https://stevetarzia.com/papers/Tarzia_495_paper.pdf)

https://github.com/tlaplus/CommunityModules/issues/63

As outlined in https://github.com/tlaplus/tlaplus/issues/543, error-reporting for `ALIAS` still hasn't been figured out. What I assume is that your `Shiviz.tla` still has `LOCAL INSTANCE Toolbox`?!

I see what is going on here. Your spec is not a "trace spec", i.e., one that re-defines the `_TETrace` operator. The `Toolbox!_TETrace` works iff there is a definition override...

Why don't you evaluate your ShiViz trace expressions in the Toolbox? On the command line, things are in flux and still have rough edges.

Unfortunately, this issue will only be fixed with the next Toolbox release. :-( In the meantime, can you copy&paste the operators, assuming you don't care about Java module overrides? If...

@Isaac-DeFrain Please comment given that you are the original author of the example.

This is not limited to FiniteSetsExtTests but how most tests are written. The second paragraph in https://github.com/tlaplus/CommunityModules#contributing also warns about this. A workaround is to only append tests to an...

To continue the discussion about moving modules out of TLAPS: * Agreement that the CommunityModules repo is a good home for most TLA+ modules (some modules might later graduate to...

We could move *_theorems(_proofs) into a subdirectory to reduce clutter. Also, to catch regressions, the CM Github action can check the proofs with the latest TLAPS release (https://github.com/lemmy/BlockingQueue/blob/4fa409b020725631d8fa0fa99ea9c813c3cd40dc/.github/workflows/main.yml#L18-L29 for inspiration).