Markus Alexander Kuppe

Simply dropping `CommunityModules.jar` (timestamp suffix stripped) into the `toolbox` directory makes sure that TLC loads the modules and overrides. Questions: * What is the lookup order if multiple copies of...

https://github.com/tlaplus/tlaplus/issues/490 (https://github.com/tlaplus/tlaplus/pull/493) would make it easy for users to load CommunityModules.jar system-wide (although `TLA_PATH` would have to be added to the classpath too for module overrides to work).

We will just move `TLCExt` and `Json` to TLC. The other modules will remain in the CommunityModules.

@ShonFeder Do you guys want to add support for Apalache (as per above), and provide `MC.tla` for those examples that work with Apalache?

The scripting would go to https://github.com/tlaplus/Examples/blob/616c4c2e00dd7084c623d1dcc83b140279652fb4/.devcontainer/devcontainer.json#L16 However, it occurred to me that -due to type annotations being mandatory in Apalache now- none of the examples will work. Thus, not terribly...

@will62794 Can you shed light on this?

Huang's algorithm has been added (https://github.com/tlaplus/Examples/tree/master/specifications/Huang). Additionally, we could try and find a refinement mapping s.t. Huang refines [AsyncTerminationDetection.tla](https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/AsyncTerminationDetection.tla).

Thanks: https://github.com/tlaplus/Examples/commit/5ef47ac84064da2bdda9c8c81eb72febaec4120d

A first attempt showing refinement of AsyncTerminationDetecting by Huang. It is not a refinement because ATD doesn't allow pending decrement when an inactive Leader in Huang receives the last weight...

Related rescale operator and its TLC module override in https://gist.github.com/lemmy/1eaf4bec8910b25e206d070b0bc80754