tlaplus/Examples

📋 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.
• 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
• + 4 more