issues
search
tlaplus
/
tlaplus
TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
https://lamport.azurewebsites.net/tla/tla.html
MIT License
2.33k
stars
197
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
NullPointerException when last state of the trace is *not* in the model.
#1087
lemmy
closed
3 days ago
0
The exception was a java.lang.ArrayIndexOutOfBoundsException : Index 0 out of bounds for length 0
#1086
lemmy
closed
4 days ago
0
Add support for new tlapm command-line syntax
#1085
glondu
opened
4 days ago
1
Improving counterexamples for concurrent designs
#1084
craft095
opened
4 days ago
6
Use of TLCSet and TLCGet across multiple workers
#1083
craft095
closed
7 hours ago
2
SANY outputs `\u27e9` code in parse error message instead of unicode symbol
#1082
ahelwer
opened
5 days ago
0
[Provisional] Support for running the TLA+ debugger with multiple workers (part 2)
#1081
lemmy
opened
5 days ago
0
Correct the predecessors and level of *all* states after dropping *finite* stuttering steps.
#1080
lemmy
closed
4 days ago
2
Add unicode support to state / value serialization
#1079
fhackett
opened
6 days ago
21
When run with the `-dump dot,constrained ...` option, TLC does not verify invariants or action properties for states that are considered unreachable due to state or action constraints
#1078
lemmy
closed
4 days ago
0
Remove unused methods {has,get,set}Data()
#1077
Calvin-L
opened
6 days ago
1
Deserializing non-ASCII strings from disk causes error
#1076
fhackett
opened
1 week ago
9
Proposal: Add -nosymmetry Option for TLC
#1075
Atafid
opened
1 week ago
0
Feature: add `-I` flag to SANY to define include directories for specs
#1074
ahelwer
opened
1 week ago
4
Proposal: design robust export format for TLC state graph
#1073
ahelwer
opened
1 week ago
2
Proposal: TLC/SANY quiet mode
#1072
hwayne
opened
1 week ago
1
`java.lang.ArrayIndexOutOfBoundsException` with `TLCExt!lassoOrdinal`
#1071
lemmy
closed
2 weeks ago
0
Proposal: support set membership checks on recursive datatypes in TLC
#1070
ahelwer
opened
2 weeks ago
1
SANY: Removed init error logging since it's static now
#1069
ahelwer
opened
2 weeks ago
0
Level-checking: fix false acceptances in OpApplNode
#1068
ahelwer
opened
2 weeks ago
1
SANY commandline enhancements
#1067
MathieuBordere
closed
1 week ago
0
Checking liveness properties in simulation mode creates a scalability bottleneck due to unnecessary sharing of ILiveCheck instances.
#1066
lemmy
closed
2 weeks ago
0
Checking liveness properties with simulation mode creates a scalability bottleneck
#1065
lemmy
closed
2 weeks ago
0
SANY: Remove unused stats feature from commandline.
#1064
MathieuBordere
closed
2 weeks ago
1
Evaluate the ALIAS expression on counterexamples generated by liveness checking while running in simulation mode.
#1063
lemmy
closed
2 weeks ago
0
[Provisional] Support running the TLA+ debugger with multiple workers.
#1062
lemmy
closed
1 week ago
3
Cancel PR CI workflow runs when newer changes are pushed
#1061
ahelwer
closed
3 weeks ago
0
Cannot debug TLC VIEW with TLA+ Debugger.
#1060
lemmy
closed
3 weeks ago
0
ClassCastException when evaluating TLCGet("spec") with coverage enabled.
#1059
lemmy
closed
3 weeks ago
0
SANY XML: added CLI help text
#1058
ahelwer
closed
2 weeks ago
2
SANY XML: pretty-print by default and add terse CLI option
#1057
ahelwer
closed
3 weeks ago
4
SANY XML: silence stdout during parsing then restore
#1056
ahelwer
closed
2 weeks ago
3
SANY XML Exporter: added CLI help text and pretty-print option
#1055
ahelwer
closed
3 weeks ago
1
SANY XML exporter: use local schema file
#1054
ahelwer
closed
3 weeks ago
5
SANY XML Export fails to validate XML
#1053
ahelwer
closed
3 weeks ago
0
Cannot debug TLC VIEW with TLA+ Debugger
#1052
lemmy
closed
3 weeks ago
1
Pretty printing of expressions in the error trace
#1051
arssher
opened
4 weeks ago
0
Add more syntax tests from TLAPM work
#1050
ahelwer
closed
2 weeks ago
0
Trace minimization when using simulation
#1049
Vanlightly
closed
1 month ago
1
Proposal: remove SANY's dependencies on TLC and publish as minimal standalone maven package or jar
#1048
ahelwer
opened
1 month ago
2
Move JavaCC files to tla2sany.parser module
#1047
ahelwer
closed
1 month ago
3
Add syntax tests to improve parser code coverage
#1046
ahelwer
closed
1 month ago
1
Lasso-Shaped counterexample fails to reconstruct when VIEW present
#1045
lemmy
opened
1 month ago
3
Refactoring goal: improve stability of liveness checker
#1044
ahelwer
opened
1 month ago
3
Generate HTML railroad diagram from TLA+ JavaCC grammar
#1043
ahelwer
closed
1 month ago
0
POSTCONDITION is evaluated twice with different values for TLCExt!Counterexample when TLC detects a liveness violation.
#1042
lemmy
closed
1 month ago
1
Distinct exit codes/return values for action property violation and for liveness violation that end in stuttering
#1041
lemmy
opened
1 month ago
3
Flaky unit test: `tlc2.tool.InliningTest`
#1040
ahelwer
opened
1 month ago
0
Randomization approach to increase state-space coverage in simulation mode interferes with liveness checking, leading to spurious counterexamples
#1039
lemmy
opened
1 month ago
0
Convert TLC.traceNum to a non-static class variable
#1038
ahelwer
closed
1 month ago
1
Next