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
#672
lemmypr.yml
on: pull_request
Matrix: Examples Integration Tests
Matrix: TLA+ Tools Build & Test
Matrix: Eclipse Toolbox Build & Test
Annotations
5 errors
|
CCoverageTest.testSpec:
tlatools/org.lamport.tlatools/test/tlc2/tool/coverage/CCoverageTest.java#L53
expected:<Coverage [line=line 42, col 15 to line 42, col 20 of module C, count=254, cost=-1]> but was:<Coverage [line=line 42, col 15 to line 42, col 20 of module C, count=253, cost=-1]>
|
|
CoverageStatisticsTest.testSpec:
tlatools/org.lamport.tlatools/test/tlc2/tool/coverage/CoverageStatisticsTest.java#L52
expected:<Coverage [line=line 48, col 15 to line 48, col 20 of module CoverageStatistics, count=99, cost=-1]> but was:<Coverage [line=line 48, col 15 to line 48, col 20 of module CoverageStatistics, count=98, cost=-1]>
|
|
TLA+ Tools Build & Test (ubuntu-latest)
Process completed with exit code 1.
|
|
TLA+ Tools Build & Test (macos-latest)
The job was canceled because "ubuntu-latest" failed.
|
|
TLA+ Tools Build & Test (macos-latest)
The operation was canceled.
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
testresults-macos-latest
|
296 KB |
|
|
testresults-ubuntu-latest
|
1.71 MB |
|