Markus Alexander Kuppe
Markus Alexander Kuppe
The Toolbox asks users to activate execution statistics to guide TLC development (see screenshot below). Please add similar functionality to your extension. Technically, a file called esc.txt is dropped into...
Installation into virtualenv with python3 complains about ```error: invalid command 'bdist_wheel'``` on Ubuntu 18.04. However, TLA+ notebook appears to work fine (unless unknown unknown). ``` (tlaplus) markus@avocado:~/dump/tlaplus_jupyter$ python3 -m venv...
* https://en.wikipedia.org/wiki/Huang's_algorithm (related https://github.com/tlaplus/CommunityModules/issues/4) * https://dl.acm.org/doi/10.5555/647172.716117
https://github.com/tlaplus/Examples/commit/4686a0be8af77260a27351cad2491873ac124d60 adds rudimentary support for Github Codespaces. TODOs: * Include the latest version of TLA+ vscode extension (https://github.com/lemmy/vscode-tlaplus/releases which comes with the debugger?) * Integrate Apalache (https://github.com/informalsystems/apalache/issues/716) ```shell ## Waiting...
Unfinished, random math exercises collected from Specifying Systems, LearnTLA, and elsewhere. ```tla ---- MODULE F ---- EXTENDS Naturals, FiniteSets, Sequences (* 1. Set of all permutations of {"T","L","A"} including repetitions....
* Modeling towers as Naturals in [Hanoi.tla](https://github.com/tlaplus/Examples/blob/master/specifications/tower_of_hanoi/Hanoi.tla) is rather low-level/close to an implementation. A high-level spec is likely simpler to grasp if it models towers as sequences... * Current Hanoi.tla...
The [current README](https://github.com/tlaplus/Examples/blob/master/README.md) does not order examples that make it easy to pick beginner-friendly examples. TLA+ concepts by which to cluster (tag?) specs: ---------------- * Constant-level expressions * Set of...
`FlattenSet({{1},{2}}) = UNION {{1},{2}}` https://github.com/tlaplus/CommunityModules/blob/e88b5536133eaf0ad68c698d618480c9a84f4192/modules/FiniteSetsExt.tla#L42-L51 @konnov @Kukovec @quicquid
https://github.com/tlaplus/tlaplus/commit/1eb815620dedc696a5a637944853129595c47216#diff-364040e3b4487febdb3378d1e3a325421763d819b32c40520360494933a8e263R12 does not work for absolute paths. We should consider adding URI-related operators such as `Dirname`, `Basename`, `Extname`, ...