Skip to content
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

Jump to bottom

Handle quint quantified variables #2873

Merged
merged 6 commits into from
Mar 25, 2024
Merged

Handle quint quantified variables #2873

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
7d9500a
Ensure that Quint's quantified variables are freshly generated for ea…
bugarela Mar 25, 2024
1258715
Update Makefile and generated quint fixtures
bugarela Mar 25, 2024
1499237
Add CHANGELOG entry
bugarela Mar 25, 2024
710af96
Fix formatting
bugarela Mar 25, 2024
7f6806a
Revert "Use type given by quint to build lambda bodies"
bugarela Mar 25, 2024
8844f46
Update one more hidden fixture
bugarela Mar 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .unreleased/bug-fixes/quint-quantified-types.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Fix a problem where different quantified variables from Quint received the same TlaType1 var number (#2873).
8 changes: 4 additions & 4 deletions Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,20 +44,20 @@ quint-fixtures: tla-io/src/test/resources/tictactoe.json tla-io/src/test/resourc

TEMP_QNT_TTT_FILE := $(shell mktemp)
tla-io/src/test/resources/tictactoe.json:
curl https://raw.githubusercontent.com/informalsystems/quint/main/examples/puzzles/tictactoe/tictactoe.qnt > $(TEMP_QNT_TTT_FILE)
quint typecheck --out $@ $(TEMP_QNT_TTT_FILE)
curl https://raw.githubusercontent.com/informalsystems/quint/main/examples/games/tictactoe/tictactoe.qnt > $(TEMP_QNT_TTT_FILE)
quint compile $(TEMP_QNT_TTT_FILE) --main=tictactoe > $@
rm $(TEMP_QNT_TTT_FILE)

TEMP_QNT_CS_FILE := $(shell mktemp)
tla-io/src/test/resources/clockSync3.json:
curl https://raw.githubusercontent.com/informalsystems/quint/main/examples/classic/distributed/ClockSync/clockSync3.qnt > $(TEMP_QNT_CS_FILE)
quint typecheck --out $@ $(TEMP_QNT_CS_FILE)
quint compile $(TEMP_QNT_CS_FILE) --main=clockSync3 > $@
rm $(TEMP_QNT_CS_FILE)

TEMP_QNT_BOOL_FILE := $(shell mktemp)
test/tla/booleans.qnt.json:
curl https://raw.githubusercontent.com/informalsystems/quint/main/examples/language-features/booleans.qnt > $(TEMP_QNT_BOOL_FILE)
quint typecheck --out $@ $(TEMP_QNT_BOOL_FILE)
quint compile $(TEMP_QNT_BOOL_FILE) --main=booleans > $@
rm $(TEMP_QNT_BOOL_FILE)

# Build the docker image
Expand Down
2 changes: 1 addition & 1 deletion test/tla/bigint.qnt.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
{"stage":"typechecking","warnings":[],"modules":[{"id":17,"name":"t","declarations":[{"kind":"var","name":"balance","typeAnnotation":{"id":1,"kind":"int"},"id":2},{"id":12,"kind":"def","name":"step","qualifier":"action","expr":{"id":11,"kind":"app","opcode":"assign","args":[{"id":10,"kind":"name","name":"balance"},{"id":9,"kind":"app","opcode":"iadd","args":[{"id":7,"kind":"name","name":"balance"},{"id":8,"kind":"int","value":10000}]}]}},{"id":16,"kind":"def","name":"inv","qualifier":"action","expr":{"id":15,"kind":"app","opcode":"ilt","args":[{"id":13,"kind":"name","name":"balance"},{"id":14,"kind":"int","value":10000}]}},{"id":6,"kind":"def","name":"init","qualifier":"action","expr":{"id":5,"kind":"app","opcode":"assign","args":[{"id":4,"kind":"name","name":"balance"},{"id":3,"kind":"int","value":100000000000}]}}]}],"table":{"4":{"kind":"var","name":"balance","typeAnnotation":{"id":1,"kind":"int"},"id":2},"7":{"kind":"var","name":"balance","typeAnnotation":{"id":1,"kind":"int"},"id":2},"10":{"kind":"var","name":"balance","typeAnnotation":{"id":1,"kind":"int"},"id":2},"13":{"kind":"var","name":"balance","typeAnnotation":{"id":1,"kind":"int"},"id":2}},"types":{"2":{"typeVariables":{},"rowVariables":{},"type":{"id":1,"kind":"int"}},"3":{"typeVariables":{},"rowVariables":{},"type":{"kind":"int"}},"4":{"typeVariables":{},"rowVariables":{},"type":{"id":1,"kind":"int"}},"5":{"typeVariables":{},"rowVariables":{},"type":{"id":3,"kind":"bool"}},"6":{"typeVariables":{},"rowVariables":{},"type":{"id":3,"kind":"bool"}},"7":{"typeVariables":{},"rowVariables":{},"type":{"id":1,"kind":"int"}},"8":{"typeVariables":{},"rowVariables":{},"type":{"kind":"int"}},"9":{"typeVariables":{},"rowVariables":{},"type":{"id":3,"kind":"int"}},"10":{"typeVariables":{},"rowVariables":{},"type":{"id":1,"kind":"int"}},"11":{"typeVariables":{},"rowVariables":{},"type":{"id":3,"kind":"bool"}},"12":{"typeVariables":{},"rowVariables":{},"type":{"id":3,"kind":"bool"}},"13":{"typeVariables":{},"rowVariables":{},"type":{"id":1,"kind":"int"}},"14":{"typeVariables":{},"rowVariables":{},"type":{"kind":"int"}},"15":{"typeVariables":{},"rowVariables":{},"type":{"id":3,"kind":"bool"}},"16":{"typeVariables":{},"rowVariables":{},"type":{"id":3,"kind":"bool"}}},"effects":{"2":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}},"3":{"effect":{"kind":"concrete","components":[]},"effectVariables":{},"entityVariables":{}},"4":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}},"5":{"effect":{"kind":"concrete","components":[{"kind":"update","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}},"6":{"effect":{"kind":"concrete","components":[{"kind":"update","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}},"7":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}},"8":{"effect":{"kind":"concrete","components":[]},"effectVariables":{},"entityVariables":{}},"9":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}},"10":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}},"11":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}},{"kind":"update","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}},"12":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}},{"kind":"update","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}},"13":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}},"14":{"effect":{"kind":"concrete","components":[]},"effectVariables":{},"entityVariables":{}},"15":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}},"16":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":{},"entityVariables":{}}}}
{"stage":"compiling","warnings":[],"modules":[{"id":17,"name":"t","declarations":[{"kind":"var","name":"balance","typeAnnotation":{"id":1,"kind":"int"},"id":2,"depth":0},{"id":12,"kind":"def","name":"step","qualifier":"action","expr":{"id":11,"kind":"app","opcode":"assign","args":[{"id":10,"kind":"name","name":"balance"},{"id":9,"kind":"app","opcode":"iadd","args":[{"id":7,"kind":"name","name":"balance"},{"id":8,"kind":"int","value":10000}]}]}},{"id":16,"kind":"def","name":"inv","qualifier":"action","expr":{"id":15,"kind":"app","opcode":"ilt","args":[{"id":13,"kind":"name","name":"balance"},{"id":14,"kind":"int","value":10000}]}},{"id":6,"kind":"def","name":"init","qualifier":"action","expr":{"id":5,"kind":"app","opcode":"assign","args":[{"id":4,"kind":"name","name":"balance"},{"id":3,"kind":"int","value":100000000000}]}}]}],"table":{"4":{"kind":"var","name":"balance","typeAnnotation":{"id":1,"kind":"int"},"id":2,"depth":0},"7":{"kind":"var","name":"balance","typeAnnotation":{"id":1,"kind":"int"},"id":2,"depth":0},"10":{"kind":"var","name":"balance","typeAnnotation":{"id":1,"kind":"int"},"id":2,"depth":0},"13":{"kind":"var","name":"balance","typeAnnotation":{"id":1,"kind":"int"},"id":2,"depth":0}},"types":{"2":{"typeVariables":[],"rowVariables":[],"type":{"id":1,"kind":"int"}},"3":{"typeVariables":[],"rowVariables":[],"type":{"kind":"int"}},"4":{"typeVariables":[],"rowVariables":[],"type":{"id":1,"kind":"int"}},"5":{"typeVariables":[],"rowVariables":[],"type":{"id":3,"kind":"bool"}},"6":{"typeVariables":[],"rowVariables":[],"type":{"id":3,"kind":"bool"}},"7":{"typeVariables":[],"rowVariables":[],"type":{"id":1,"kind":"int"}},"8":{"typeVariables":[],"rowVariables":[],"type":{"kind":"int"}},"9":{"typeVariables":[],"rowVariables":[],"type":{"id":3,"kind":"int"}},"10":{"typeVariables":[],"rowVariables":[],"type":{"id":1,"kind":"int"}},"11":{"typeVariables":[],"rowVariables":[],"type":{"id":3,"kind":"bool"}},"12":{"typeVariables":[],"rowVariables":[],"type":{"id":3,"kind":"bool"}},"13":{"typeVariables":[],"rowVariables":[],"type":{"id":1,"kind":"int"}},"14":{"typeVariables":[],"rowVariables":[],"type":{"kind":"int"}},"15":{"typeVariables":[],"rowVariables":[],"type":{"id":3,"kind":"bool"}},"16":{"typeVariables":[],"rowVariables":[],"type":{"id":3,"kind":"bool"}}},"effects":{"2":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":[],"entityVariables":[]},"3":{"effect":{"kind":"concrete","components":[]},"effectVariables":[],"entityVariables":[]},"4":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":[],"entityVariables":[]},"5":{"effect":{"kind":"concrete","components":[{"kind":"update","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":[],"entityVariables":[]},"6":{"effectVariables":[],"entityVariables":[],"effect":{"kind":"concrete","components":[{"kind":"update","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]}},"7":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":[],"entityVariables":[]},"8":{"effect":{"kind":"concrete","components":[]},"effectVariables":[],"entityVariables":[]},"9":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":[],"entityVariables":[]},"10":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":[],"entityVariables":[]},"11":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}},{"kind":"update","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":[],"entityVariables":[]},"12":{"effectVariables":[],"entityVariables":[],"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}},{"kind":"update","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]}},"13":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":[],"entityVariables":[]},"14":{"effect":{"kind":"concrete","components":[]},"effectVariables":[],"entityVariables":[]},"15":{"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]},"effectVariables":[],"entityVariables":[]},"16":{"effectVariables":[],"entityVariables":[],"effect":{"kind":"concrete","components":[{"kind":"read","entity":{"kind":"concrete","stateVariables":[{"name":"balance","reference":2}]}}]}}},"errors":[]}
Loading
Loading