Markus Alexander Kuppe
Markus Alexander Kuppe
Closed in favor of https://github.com/tlaplus/Examples/pull/155
I'm reluctant to merge this PR because it breaks users still on the latest [1.7.2.](https://github.com/tlaplus/tlaplus/releases/tag/v1.7.2) TLC release, which does not bundle `Json.tla`.
https://github.com/tlaplus/Examples/blob/789a653495f2e41d449d28e3935b15ab4b21e147/.devcontainer/install.sh#L40-L45
> If we devolve this to individual directories, it becomes a much nicer experience for users to write their own JSON file. Users can use github's repository search function to...
JSON, YAML, XML—pick your poison. The real issue is that there's complex machinery (Python scripts coupled with JSON) that creates friction for the second biggest audience of this repo and...
I have no preference—I dislike all programming languages equally. 🙂 That said, the TLA+ project shouldn't turn into a programming language zoo. As much as possible, we stick to OCaml...
I suggest using "undefined" instead of "unassigned" because TLA+ does not have assignment.
Adding the following to `SequencesExt.java` causes TLC to treat `BoundedSeq`/`SeqOf` strictly symbolically. However, there is no infrastructure for a hybrid value. We would have to implement a BoundedSeqValue that extends...
### Automated trace validation tests to verify correctness of etcd-io/raft The CCF project has already figured out most of the bits and bobs to run trace validation and model checking...