Merge pull request #2696 from informalsystems/gabriela/quint-fields-u…

…pdate

Update quint deserialization

.unreleased/breaking-changes/2696-quint-deserialization.md

@@ -0,0 +1 @@
+Update Quint deserialization for compatibility with version > 0.13.0, see #2696

Makefile

@@ -50,7 +50,7 @@ tla-io/src/test/resources/tictactoe.json:
 
 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_TTT_FILE)
+	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)
 	rm $(TEMP_QNT_CS_FILE)
 

test/tla/bigint.qnt.json

@@ -1 +1 @@
-{"stage":"typechecking","warnings":[],"modules":[{"id":"17","name":"bigint","defs":[{"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","reference":"2","typeAnnotation":{"id":"1","kind":"int"}},"7":{"kind":"var","reference":"2","typeAnnotation":{"id":"1","kind":"int"}},"10":{"kind":"var","reference":"2","typeAnnotation":{"id":"1","kind":"int"}},"13":{"kind":"var","reference":"2","typeAnnotation":{"id":"1","kind":"int"}}},"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":"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":{}}}}