Skip to content

Commit

Permalink
Merge pull request #2873 from informalsystems/gabriela/handle-quint-q…
Browse files Browse the repository at this point in the history 
…uantified-variables

Handle quint quantified variables
  • Loading branch information
@bugarela
bugarela authored Mar 25, 2024
2 parents 27f1885 + 8844f46 commit 735f95d
Show file tree
Hide file tree
Showing 11 changed files with 46 additions and 47 deletions.
1 change: 1 addition & 0 deletions .unreleased/bug-fixes/quint-quantified-types.md
View file
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
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
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

0 comments on commit 735f95d

Please sign in to comment.