-
Notifications
You must be signed in to change notification settings - Fork 43
- #78 · hejersbo opened
on Apr 30, 2023 3
Issues
is:issue state:open
is:issue state:open
Issue creation is restricted in this repository
Search results
Add a deterministic Z3
rlimitbudget for reproducible verification across machines and rerunenhancementA new feature, an improvement, or other addition.A new feature, an improvement, or other addition.Status: Open.#281 In tlaplus/tlapm;- Status: Open.#280 In tlaplus/tlapm;
--lineshould fail when no proof obligation is selectedenhancementA new feature, an improvement, or other addition.A new feature, an improvement, or other addition.Status: Open.#276 In tlaplus/tlapm;Learnings AI+TLAPS (TLAiPS)
documentationAdding or editing any form of documentation (documentation files, code comments, website pages, etc)Adding or editing any form of documentation (documentation files, code comments, website pages, etc)Status: Open.#272 In tlaplus/tlapm;tlapm ending abnormally with File "src/expr/e_levels.ml", line 933, characters 12-18: Assertion failed
bugAn error, usually in the code.An error, usually in the code.Status: Open.#270 In tlaplus/tlapm;- Status: Open.#269 In tlaplus/tlapm;
LSP: Proof decomposition should push
'downenhancementA new feature, an improvement, or other addition.A new feature, an improvement, or other addition.Status: Open.#261 In tlaplus/tlapm;- Status: Open.#259 In tlaplus/tlapm;
- Status: Open.#252 In tlaplus/tlapm;
- Status: Open.#250 In tlaplus/tlapm;
- Status: Open.#247 In tlaplus/tlapm;
When run from a different directory, TLAPM cannot handle leading text on modules imported using EXTENDS
syntax parserIssues relating to TLAPM's syntax parserIssues relating to TLAPM's syntax parserStatus: Open.#245 In tlaplus/tlapm;