From a742359791b8c32066f8a20a0273036c37b282b6 Mon Sep 17 00:00:00 2001
From: Shon Feder <shon@informal.systems>
Date: Wed, 13 Mar 2024 23:05:18 -0400
Subject: [PATCH] Update apalache integration test for compile

We now test that identifiers are sanitized, that imports and instances
are resolved as expected, and that the unit is represented correctly.
---
 quint/apalache-tests.md                   | 41 ++++++++++++++---------
 quint/testFixture/ApalacheCompilation.qnt | 35 +++++++++++++++++++
 2 files changed, 61 insertions(+), 15 deletions(-)
 create mode 100644 quint/testFixture/ApalacheCompilation.qnt

diff --git a/quint/apalache-tests.md b/quint/apalache-tests.md
index 8a716f60c..d570c831d 100644
--- a/quint/apalache-tests.md
+++ b/quint/apalache-tests.md
@@ -224,34 +224,45 @@ An example execution:
 
 ### Test that we can compile to TLA+ of the expected form
 
-<!-- !test in can convert booleans.qnt to TLA+ -->
+<!-- !test in can convert ApalacheCompliation.qnt to TLA+ -->
 ```
-quint compile --target tlaplus  ../examples/language-features/booleans.qnt
+quint compile --target tlaplus  ./testFixture/ApalacheCompilation.qnt
 ```
 
-<!-- !test out can convert booleans.qnt to TLA+ -->
+<!-- !test out can convert ApalacheCompliation.qnt to TLA+ -->
 ```
-------------------------------- MODULE booleans -------------------------------
+-------------------------- MODULE ApalacheCompilation --------------------------
 
 EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache
 
-VARIABLE b
+VARIABLE x
 
-step ==
-  (b \/ TRUE)
-    /\ ~(b /\ FALSE)
-    /\ (b => b)
-    /\ (b <=> b)
-    /\ b = b
-    /\ b /= (~b)
-    /\ b' := (~b)
+A == Variant("A", <<>>)
 
-init == b' := TRUE
+B(__BParam_27) == Variant("B", __BParam_27)
+
+foo_bar(id__123_31) == id__123_31
+
+importedValue == 0
+
+ApalacheCompilation_ModuleToInstantiate_C == 0
+
+step == x' := (x + 1)
+
+inv == x >= 0
+
+ApalacheCompilation_ModuleToInstantiate_instantiatedValue ==
+  ApalacheCompilation_ModuleToInstantiate_C
+
+init ==
+  x'
+    := (importedValue
+      + ApalacheCompilation_ModuleToInstantiate_instantiatedValue)
 
 ================================================================================
 ```
 
-### Test that we can compile a module with imports and instances to TLA+
+### Test that we can compile a module to TLA+ that instantiates but has not declarations
 
 
 <!-- !test in can convert clockSync3.qnt to TLA+ -->
diff --git a/quint/testFixture/ApalacheCompilation.qnt b/quint/testFixture/ApalacheCompilation.qnt
new file mode 100644
index 000000000..02a415496
--- /dev/null
+++ b/quint/testFixture/ApalacheCompilation.qnt
@@ -0,0 +1,35 @@
+module ModuleToInstantiate {
+  const C: int
+
+  val instantiatedValue = C
+}
+
+module ModuleToImport {
+  val importedValue = 0
+}
+
+module ApalacheCompilation {
+  // Tests whether we can compile imports
+  import ModuleToImport.*
+
+  // Tests whether we can compile instantiations
+  import ModuleToInstantiate(C = 0).*
+
+  var x: int
+
+  type T =
+    | A  // Test whether we represent the unit correctly
+    | B(int)
+
+  // Tests whether we will sanitize identifiers
+  def foo::bar(__123) = __123
+
+  // TODO: Tests that we remove primes from assignments in the init functino
+  action init = {
+    x' = importedValue + instantiatedValue
+  }
+
+  action step = x' = x + 1
+
+  def inv = x >= 0
+}