Nothing Special   »   [go: up one dir, main page]
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

250 Open 568 Closed
250 Open 568 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

Improving counterexamples for concurrent designs enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#1084 opened Nov 22, 2024 by craft095
6
SANY outputs \u27e9 code in parse error message instead of unicode symbol
#1082 opened Nov 21, 2024 by ahelwer
Deserializing non-ASCII strings from disk causes error bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ...
#1076 opened Nov 19, 2024 by fhackett
1
9
Proposal: Add -nosymmetry Option for TLC enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#1075 opened Nov 19, 2024 by Atafid
2
Feature: add -I flag to SANY to define include directories for specs
#1074 opened Nov 15, 2024 by ahelwer
4
Proposal: design robust export format for TLC state graph enhancement Lets change things for the better help wanted We need your help TLA+ Foundation Funding Tools The command line tools - TLC, SANY, ...
#1073 opened Nov 13, 2024 by ahelwer
2
Proposal: TLC/SANY quiet mode enhancement Lets change things for the better good first issue Your entry point to contributing to TLA+ help wanted We need your help Tools The command line tools - TLC, SANY, ...
#1072 opened Nov 13, 2024 by hwayne
1
Proposal: support set membership checks on recursive datatypes in TLC enhancement Lets change things for the better Tools The command line tools - TLC, SANY, ...
#1070 opened Nov 11, 2024 by ahelwer
1
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
More permissive evaluation of functions updated in transition relation
#998 opened Aug 15, 2024 by will62794
10
ProTip! Exclude everything labeled bug with -label:bug.