Markus Alexander Kuppe
Markus Alexander Kuppe
A more promising approach would be to use @will62794 https://github.com/will62794/tla-web for the purely browser-based variant of the VSCode extension.
Will try to reproduce.
I haven't checked with *all* specifications. However, it is definitely reproducible (iff VSCode launches with a collapsed Outline).
Note that related to the last item, TLC has a simulator/generator mode.
@bestchai The simulator honors state and action constraints. https://github.com/lemmy/PageQueue/blob/master/Schedules.tla is an example of how to make TLC follow a specific schedule.
Have you tested this feature already? If yes, it seems as if it is broken because so far there have been no exec-stats for "tlaplus_jupyter" (https://github.com/kelvich/tlaplus_jupyter/commit/d64477f1171534a39b815a98b0b84f542a8c7bcb#diff-8f9c6fbaedaf902848b1e9f9e47d60f2R253).
No, only recent nightlies report the value of ```tlc2.TLC.ide```.
Great, but be aware of https://github.com/tlaplus/tlaplus/issues/393#issuecomment-560508473
Do you want to open a PR? Btw. the existing variant of Hanoi is not just about module overrides but also shows how towers can be modeled as natural numbers....
I suggest creating `HanoiSeq.tla` in the existing `towers_of_hanoi` folder to leave the door open to adding a refinement mapping later. Please add comments to your spec and state the Hanoi...