Merge branch 'main' into gabriela/nondet-checks

quint/apalache-tests.md

@@ -235,38 +235,84 @@ quint compile --target tlaplus ./testFixture/ApalacheCompilation.qnt
 
 EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants
 
-VARIABLE x
-
+VARIABLE
+  (*
+    @type: Int;
+  *)
+  x
+
+(*
+  @type: (() => A(UNIT) | B(Int));
+*)
 A == Variant("A", "U_OF_UNIT")
 
+(*
+  @type: ((Int) => A(UNIT) | B(Int));
+*)
 B(__BParam_31) == Variant("B", __BParam_31)
 
+(*
+  @type: ((a) => a);
+*)
 foo_bar(id__123_35) == id__123_35
 
+(*
+  @type: (() => Int);
+*)
 importedValue == 0
 
+(*
+  @type: (() => Int);
+*)
 ApalacheCompilation_ModuleToInstantiate_C == 0
 
+(*
+  @type: (() => Bool);
+*)
 altInit == x' := 0
 
+(*
+  @type: (() => Bool);
+*)
 step == x' := (x + 1)
 
+(*
+  @type: (() => Bool);
+*)
 altStep == x' := (x + 0)
 
+(*
+  @type: (() => Bool);
+*)
 inv == x >= 0
 
+(*
+  @type: (() => Bool);
+*)
 altInv == x >= 0
 
+(*
+  @type: (() => Int);
+*)
 ApalacheCompilation_ModuleToInstantiate_instantiatedValue ==
   ApalacheCompilation_ModuleToInstantiate_C
 
+(*
+  @type: (() => Bool);
+*)
 init ==
   x'
     := (importedValue
       + ApalacheCompilation_ModuleToInstantiate_instantiatedValue)
 
+(*
+  @type: (() => Bool);
+*)
 q_step == step
 
+(*
+  @type: (() => Bool);
+*)
 q_init == init
 
 ================================================================================
@@ -304,14 +350,29 @@ quint compile --target tlaplus --main ModuleToImport ./testFixture/ApalacheCompi
 
 EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants
 
+(*
+  @type: (() => Bool);
+*)
 step == TRUE
 
+(*
+  @type: (() => Int);
+*)
 importedValue == 0
 
+(*
+  @type: (() => Bool);
+*)
 init == TRUE
 
+(*
+  @type: (() => Bool);
+*)
 q_init == init
 
+(*
+  @type: (() => Bool);
+*)
 q_step == step
 
 ================================================================================
@@ -333,10 +394,10 @@ The compiled module is not empty:
 
 EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants
 
-VARIABLE clockSync3_clockSync3Spec_time
-
-clockSync3_clockSync3Spec_Proc(clockSync3_clockSync3Spec_id_37) ==
-  [id |-> clockSync3_clockSync3Spec_id_37]
+VARIABLE
+  (*
+    @type: Int;
+  *)
+  clockSync3_clockSync3Spec_time
 
-VARIABLE clockSync3_clockSync3Spec_hc
 ```

quint/io-cli-tests.md

@@ -24,11 +24,15 @@ We want to ensure we do not throw uncaught exceptions when the input file is
 doesn't exist.
 
 <!-- !test in non-existent file -->
-    quint parse ../examples/non-existent.file
+```
+quint parse ../examples/non-existent.file
+```
 
 <!-- !test exit 1 -->
 <!-- !test err non-existent file -->
-    error: file ../examples/non-existent.file does not exist
+```
+error: file ../examples/non-existent.file does not exist
+```
 
 ### User error on parse with junk after modules
 
@@ -37,14 +41,18 @@ We want to ensure that the parser shows an error, when it detects junk in
 the end of file.
 
 <!-- !test in junk -->
-    quint parse ./testFixture/modulesAndJunk.qnt 2>&1 | sed 's#.*quint/\(testFixture\)#Q/\1#g'
+```
+quint parse ./testFixture/modulesAndJunk.qnt 2>&1 | sed 's#.*quint/\(testFixture\)#Q/\1#g'
+```
 
 <!-- !test out junk -->
-    Q/testFixture/modulesAndJunk.qnt:9:1 - error: [QNT000] extraneous input 'the' expecting {<EOF>, 'module', DOCCOMMENT}
-    9: the parser
-       ^^^
+```
+Q/testFixture/modulesAndJunk.qnt:9:1 - error: [QNT000] extraneous input 'the' expecting {<EOF>, 'module', DOCCOMMENT}
+9: the parser
+   ^^^
 
-    error: parsing failed
+error: parsing failed
+```
 
 ### User error on parse with invalid input
 

quint/src/apalache.ts

@@ -39,7 +39,7 @@ import type { Buffer } from 'buffer'
 import type { PackageDefinition as ProtoPackageDefinition } from '@grpc/proto-loader'
 
 const APALACHE_SERVER_URI = 'localhost:8822'
-const APALACHE_VERSION_TAG = '0.44.10'
+const APALACHE_VERSION_TAG = '0.44.11'
 // TODO: used by GitHub api approach: https://github.com/informalsystems/quint/issues/1124
 // const APALACHE_TGZ = 'apalache.tgz'