examples - v1.1.0 release

Breaking changes: - Since tree-sitter-tlaplus now releases a python package alongside prebuilt wheels for a number of platforms, it is no longer necessary to download & compile the tree-sitter-tlaplus grammar, nor pass its path as a parameter to various scripts. - Added the capability to do symbolic model checking with Apalache, necessitating passing its path as a parameter to some scripts. - Unified the way --skip and --only parameters work, or rather moved their intended method of function in line with the actual way they were functioning; these parameters accept paths as keys into the manifest.json file, not paths as paths from whatever directory the script is being called from.

Non-breaking changes: - Added new scripts to test Unicode functionality, by converting all specs to Unicode and adding shims for the Naturals/Integers/Reals imports. - Added new script to run PlusCal translation on all PlusCal specs, and fixed any existing issues with PlusCal specs in the repo (source/generated code out of sync, etc.) - Unified all line endings in the repo as LF - TLAi Linter spec added by @lemmy to check conformance of plain-language comments to TLA+ code using a LLM - Trace Validation CI step added by @lemmy - CITATION.cff file added by @lemmy

New specs: - YoYo Leader Election spec added by @muenchnerkindl - EWD998 spec added by @lemmy - TCP spec added by @lemmy

- TLA
Published by ahelwer almost 2 years ago

examples - v1.0.0 release

Since various repos might start depending on the manifest format for their own testing & tooling, it is good practice to begin tracking it using standard semantic versioning. Patch releases will also be issued occasionally as specs are added.

- TLA
Published by ahelwer almost 2 years ago