tlaplus/tlapm issues and pull requests

#83 - Dune based build

Pull Request - State: closed - Opened by kape1395 over 1 year ago - 21 comments

#82 - Simplify the build process.

Issue - State: closed - Opened by kape1395 over 1 year ago

#81 - Basic support for build with dune.

Pull Request - State: closed - Opened by kape1395 over 1 year ago - 1 comment

#80 - Use Dune for build?

Issue - State: closed - Opened by kape1395 over 1 year ago

#79 - fix wrong expansion of @ in nested EXCEPT

Pull Request - State: closed - Opened by damiendoligez over 1 year ago

#78 - TLAPS in WSL2 - Prover Launch problem

Issue - State: closed - Opened by hejersbo over 1 year ago - 3 comments

#77 - wrong expansion of @ in record updates

Issue - State: closed - Opened by muenchnerkindl over 1 year ago - 2 comments
Labels: bug

#76 - Incorrect output of obligation that includes `\lnot` on an unbound variable

Issue - State: closed - Opened by ahelwer over 1 year ago - 1 comment

#75 - ENABLED is not coalesced

Issue - State: open - Opened by muenchnerkindl over 1 year ago
Labels: enhancement

#74 - Is there a way to designate the output directory for the fingerprint files?

Issue - State: closed - Opened by ahelwer almost 2 years ago - 1 comment

#73 - Install error messages on macOS: unable to locate a Java runtime

Issue - State: closed - Opened by ahelwer almost 2 years ago - 5 comments

#72 - Easy way to set up portable TLAPS?

Issue - State: closed - Opened by ahelwer almost 2 years ago - 1 comment

#71 - Primed variables in quantifier bounds are ignored

Issue - State: open - Opened by rozlynd almost 2 years ago - 1 comment
Labels: bug, semantic checker

#70 - Smt changes

Pull Request - State: closed - Opened by adef-inr almost 2 years ago - 12 comments

#69 - TLAPM identifies instantiated fairness condition with fairness of instantiated action

Issue - State: open - Opened by muenchnerkindl over 2 years ago
Labels: bug

#68 - BUG: quoting of environment variables for CI, and automatically run `release.yml`

Pull Request - State: open - Opened by johnyf over 2 years ago - 6 comments

#67 - CI: run `pr.yml` when changed

Pull Request - State: closed - Opened by johnyf over 2 years ago - 1 comment

#66 - CI: move release-making actions to file `release.yml`

Pull Request - State: closed - Opened by johnyf over 2 years ago - 3 comments

#65 - REF: configuration files for GitHub Actions

Pull Request - State: closed - Opened by johnyf over 2 years ago

#64 - Fix spurious warning from ps

Pull Request - State: closed - Opened by damiendoligez almost 3 years ago - 2 comments

#63 - HIDE X HIDE Y works but HIDE X, Y doesn't

Issue - State: open - Opened by cpacejo almost 3 years ago - 1 comment
Labels: bug, semantic checker

#62 - Examples involving use of WF.

Pull Request - State: closed - Opened by kape1395 almost 3 years ago - 4 comments

#61 - formatting of modules related to indexing and subexpression references

Pull Request - State: closed - Opened by johnyf almost 3 years ago - 2 comments

#60 - fixes related to bounding of declarees in quantification and function definitions

Pull Request - State: open - Opened by johnyf almost 3 years ago

#59 - API: represent tuply declarations in the syntax tree

Pull Request - State: open - Opened by johnyf almost 3 years ago - 1 comment

#58 - REF: add functions for creating syntax-tree nodes, revise internal interfaces

Pull Request - State: closed - Opened by johnyf almost 3 years ago - 1 comment

#57 - _API: mainly related to expressions

Pull Request - State: closed - Opened by johnyf almost 3 years ago - 2 comments

#56 - fixes mainly related to operator indexing

Pull Request - State: closed - Opened by johnyf almost 3 years ago - 1 comment

#55 - Smt fix

Pull Request - State: closed - Opened by adef-inr about 3 years ago - 3 comments

#54 - Problem instantiating a module with a RECURSIVE operator

Issue - State: open - Opened by josedusol about 3 years ago - 1 comment
Labels: bug, syntax parser, semantic checker

#53 - Solver timeout isn't respected properly

Issue - State: open - Opened by will62794 about 3 years ago - 1 comment
Labels: bug

#52 - TAKE directive leads to bogus obligations if confronted with chained universal quantifiers

Issue - State: open - Opened by zwergziege about 3 years ago - 3 comments
Labels: bug, translator

#51 - Existence of non-existing recursive functions

Issue - State: open - Opened by zwergziege about 3 years ago - 3 comments
Labels: bug, dependencies

#50 - SMT backend encounters 'Queue.nth: internal error'

Issue - State: open - Opened by will62794 about 3 years ago - 4 comments
Labels: bug, translator

#49 - ENH: convert syntax tree to JSON

Pull Request - State: open - Opened by johnyf about 3 years ago

#48 - Formatting, documentation, local refactoring

Pull Request - State: closed - Opened by johnyf about 3 years ago - 3 comments

#47 - API: read (env) variable `TLAPM_CACHE_DIR`, add command-line parameter `--cache-dir`

Pull Request - State: closed - Opened by johnyf about 3 years ago - 1 comment
Labels: enhancement, api, ui

#46 - Sign TLAPS release to be accepted by macOS gatekeeper

Issue - State: open - Opened by lemmy about 3 years ago - 6 comments
Labels: enhancement

#45 - Under specific circumstances SMT can't handle strings

Issue - State: open - Opened by zwergziege over 3 years ago
Labels: bug, translator

#44 - TLAPM Pb

Issue - State: closed - Opened by FilaliM over 3 years ago - 1 comment

#43 - convert website source to Markdown, print message from installer about Cygwin paths

Pull Request - State: closed - Opened by johnyf over 3 years ago - 3 comments

#42 - Fingerprint loaded with `--nofp`

Issue - State: closed - Opened by lemmy over 3 years ago - 2 comments
Labels: documentation, ui

#41 - Silent failure when input file doesn't exist -- output suggests file exists

Issue - State: closed - Opened by lemmy over 3 years ago - 2 comments
Labels: bug

#40 - Contradictory warning with ExpandENABLED

Issue - State: open - Opened by lemmy over 3 years ago - 1 comment
Labels: documentation

#39 - CHOOSE

Issue - State: closed - Opened by lemmy over 3 years ago - 3 comments

#38 - interfacing to `cvc5`

Issue - State: open - Opened by johnyf over 3 years ago
Labels: enhancement, documentation, api

#37 - CodeOfConduct

Issue - State: closed - Opened by lemmy over 3 years ago - 2 comments
Labels: enhancement, documentation

#36 - TLAPM fails to run with error code -1073741515

Issue - State: closed - Opened by ahelwer over 3 years ago - 5 comments
Labels: documentation

#35 - Spec => <>[]TRUE

Issue - State: open - Opened by lemmy over 3 years ago - 1 comment
Labels: enhancement

#34 - parse tuple syntax in function constructors and comma-separated arguments in `EXCEPT` assignments

Pull Request - State: closed - Opened by johnyf over 3 years ago - 3 comments
Labels: bug

#33 - correctly interpret multiple `EXCEPT` assignments

Pull Request - State: closed - Opened by johnyf over 3 years ago - 1 comment
Labels: bug

#32 - crash when naming subexpressions with free variables in LET/IN constructs

Issue - State: open - Opened by zwergziege almost 4 years ago
Labels: bug, semantic checker

#31 - incorrect naming of subexpressions of operators defining recursive functions

Issue - State: open - Opened by zwergziege almost 4 years ago
Labels: bug, semantic checker

#30 - Unsupported syntax causes TLAPM to crash

Issue - State: closed - Opened by cipher1024 almost 4 years ago - 4 comments

#29 - Dekker's algorithm for mutual exclusion

Pull Request - State: closed - Opened by johnyf almost 4 years ago - 1 comment

#28 - Running TLAPM in a specification which extends Randomization results in a crash

Issue - State: closed - Opened by uguryavuz almost 4 years ago - 5 comments

#27 - modifications to standard TLAPS library

Pull Request - State: closed - Opened by muenchnerkindl almost 4 years ago

#26 - tlapm problems

Issue - State: closed - Opened by FilaliM almost 4 years ago - 3 comments

#25 - update to OCaml v4.11.0

Pull Request - State: closed - Opened by johnyf almost 4 years ago - 5 comments

#24 - `INSTANCE` within `LET`, `ENABLED` in parametrized `INSTANCE`, `ENABLED` in instantiated operators with parameters, and related changes

Pull Request - State: closed - Opened by johnyf almost 4 years ago - 1 comment
Labels: bug

GitHub / tlaplus/tlapm issues and pull requests