Skip to content

Issues: tlaplus/tlaplus

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

245 Open 564 Closed
245 Open 564 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Checking liveness properties with simulation mode creates a scalability bottleneck enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#1065 opened Nov 7, 2024 by lemmy
Pretty printing of expressions in the error trace enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#1051 opened Oct 29, 2024 by arssher
Proposal: remove SANY's dependencies on TLC and publish as minimal standalone maven package or jar
#1048 opened Oct 21, 2024 by ahelwer
2
Lasso-Shaped counterexample fails to reconstruct when VIEW present bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ...
#1045 opened Oct 18, 2024 by lemmy
3
Refactoring goal: improve stability of liveness checker
#1044 opened Oct 18, 2024 by ahelwer
3
Distinct exit codes/return values for action property violation and for liveness violation that end in stuttering enhancement Lets change things for the better good first issue Your entry point to contributing to TLA+ help wanted We need your help
#1041 opened Oct 17, 2024 by lemmy
3
Flaky unit test: tlc2.tool.InliningTest
#1040 opened Oct 11, 2024 by ahelwer
Randomization approach to increase state-space coverage in simulation mode interferes with liveness checking, leading to spurious counterexamples enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#1039 opened Oct 9, 2024 by lemmy
Liveness checker regression: TLC reports spurious error in initial state for formulas of form P => <>[]Q bug error, glitch, fault, flaw, ... regression we've regressed Tools The command line tools - TLC, SANY, ...
#1037 opened Oct 7, 2024 by ahelwer
4
Support projecting an error trace based on the logical processes in a system enhancement Lets change things for the better help wanted We need your help Tools The command line tools - TLC, SANY, ...
#1035 opened Oct 7, 2024 by lemmy
Clone foreign model does not work a second time bug error, glitch, fault, flaw, ... Toolbox The TLA Toolbox/IDE
#1032 opened Oct 6, 2024 by lemmy
BEGIN/EDN TRANSLATION markers preceding the algorithm confuse the PlusCal translator bug error, glitch, fault, flaw, ... PlusCal PlusCal Algorithm Language
#1031 opened Oct 6, 2024 by lemmy
TLC should be able to handle temporal formulas containing <=> enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#1029 opened Oct 3, 2024 by ahelwer
Graduate _PERIODIC hook enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#1023 opened Oct 1, 2024 by lemmy
5 tasks
3
SANY mistakenly parses set literal as set filter
#1021 opened Oct 1, 2024 by ahelwer
1
Add ℕ, ℤ, and ℝ to the standard modules enhancement Lets change things for the better Unicode Unicode support for TLA
#1020 opened Oct 1, 2024 by ahelwer
3
Level parameters are not set for built-in dot infix operator (record access operator) SANY Issues involving SANY's analysis
#1008 opened Sep 8, 2024 by ahelwer
5
Grammar railroad diagram DevEnvironment Everything related to the Toolbox development environment SANY Issues involving SANY's analysis
#1001 opened Aug 29, 2024 by mingodad
More permissive evaluation of functions updated in transition relation
#998 opened Aug 15, 2024 by will62794
10
TLCRuntime returns x86 on non-x86 architecture such as arm bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ...
#997 opened Aug 14, 2024 by lemmy
4
Value API improvements DevEnvironment Everything related to the Toolbox development environment enhancement Lets change things for the better refactoring Steadily improving code base Tools The command line tools - TLC, SANY, ...
#996 opened Aug 13, 2024 by Calvin-L
2
StackOverflowError when evaluating bounded recursion in the scope of ENABLED bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ...
#991 opened Jul 21, 2024 by lemmy
2
Upload code-coverage-report in PR and CI DevEnvironment Everything related to the Toolbox development environment enhancement Lets change things for the better
#981 opened Jul 2, 2024 by FedericoPonzi
1
@FedericoPonzi
7
TLA+ Debugger returns bogus source path on Windows bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ...
#970 opened Jun 21, 2024 by lemmy
ant compile target should not depend on clean and generate target. DevEnvironment Everything related to the Toolbox development environment
#969 opened Jun 21, 2024 by lemmy
8
ProTip! Find all open issues with in progress development work with linked:pr.