Alexander Niederbühl

Thanks for looking into this! Yes, the error is on server side. If the websocket is not closed then `ktor-websockets` seems correct in throwing this exception, so I'm not sure...

That would be great, are you still planning to look into it @olme04?

Another example of the same problem: ``` apalache check crdt.tla ``` gives me ``` PASS #1: ConfigurationPass I@16:59:52.550 > crdt.cfg: Loading TLC configuration I@16:59:52.554 Operator Spec of 0 arguments is...

I tried to model this as an exercise, maybe this is along the lines of what you had in mind and can be used as example? ```TLA ------------------------------- MODULE hanoi...

> Do you want to open a PR? Sure, I can do that. Would it be ok to just add it as separate example and leave the current variant untouched?

> What I assume is that your `Shiviz.tla` still has `LOCAL INSTANCE Toolbox` It's the new version which has `INSTANCE Toolbox`.

Thank you, but I must admit I'm a bit lost on what the problem is and how it is solved. Is there anything I could read to learn about this?...

Another option would be to put small exercises like this into Jupyter notebooks, [here](https://github.com/Alexander-N/tlaplus-exercises) is an example for the ones from [Learn TLA+](https://learntla.com/tla).

Not having to install anything is one point, but I also like the experience of being able to easily check the output of the expression and then seeing the solution....

> For example decoding an "illegal" component code like 'decode("1HUg6wnerR9jP")' should raise an error. Since there are languages without exceptions I would put it more liberal, maybe something like "must...