Skip to content

GitLab

Explore

Sign in

Primary navigation

Project

T

tlatools
- Activity
- Members
- Labels
- Releases

Snippets Groups Projects

f10aa783

Commit f10aa783 authored Mar 15, 2023 by Markus Alexander Kuppe

Downloads
- Patches
- Plain Diff

LazyValue can cause TLC to generate too many or too few states.

Part of Github issue #798
https://github.com/tlaplus/tlaplus/issues/798



[Bug][TLC][Changelog]

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

parent 3c7caa56

Branches

Tags

No related merge requests found

Changes 7

Show whitespace changes

Inline Side-by-side

Showing

tlatools/org.lamport.tlatools/src/tlc2/tool/impl/SymbolNodeValueLookupProvider.java 12 additions, 0 deletions

...ols/src/tlc2/tool/impl/SymbolNodeValueLookupProvider.java
tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java 1 addition, 1 deletion

tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java
tlatools/org.lamport.tlatools/src/tlc2/value/impl/LazyValue.java 1 addition, 1 deletion

...s/org.lamport.tlatools/src/tlc2/value/impl/LazyValue.java
tlatools/org.lamport.tlatools/test-model/Github798I.tla 31 additions, 0 deletions

tlatools/org.lamport.tlatools/test-model/Github798I.tla
tlatools/org.lamport.tlatools/test-model/Github798N.tla 35 additions, 0 deletions

tlatools/org.lamport.tlatools/test-model/Github798N.tla
tlatools/org.lamport.tlatools/test/tlc2/tool/Github798ITest.java 62 additions, 0 deletions

...s/org.lamport.tlatools/test/tlc2/tool/Github798ITest.java
tlatools/org.lamport.tlatools/test/tlc2/tool/Github798NTest.java 62 additions, 0 deletions

...s/org.lamport.tlatools/test/tlc2/tool/Github798NTest.java

with 204 additions and 2 deletions

Loading

0% Loading or .

You are about to add 0 people to the discussion. Proceed with caution.

Finish editing this message first!

Please register or sign in to comment