Merge pull request #191 from tlaplus/fix-inst-use

Fix instantiation of a module containing USE.
tlaplus · Jan 4, 2025 · 9df048d · 9df048d
2 parents e0ce98e + 05a8e2e
commit 9df048d
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 0 deletions.
diff --git a/src/module/m_visit.ml b/src/module/m_visit.ml
@@ -165,6 +165,7 @@ class map =
     method mutate cx change usable =
         let mu = Mutate (
             change, usable) in
+        let cx = update_cx cx mu in
         (cx, mu)
 
     method submod cx tla_module =

diff --git a/test/bugs/instance_mutate.tla b/test/bugs/instance_mutate.tla
@@ -0,0 +1,5 @@
+---- MODULE instance_mutate ----
+Op(x) == TRUE
+USE TRUE
+OpAll == \A x : Op(x)
+====
diff --git a/test/bugs/instance_mutate_test.tla b/test/bugs/instance_mutate_test.tla
@@ -0,0 +1,7 @@
+---- MODULE instance_mutate_test ----
+(*
+Instantiation was failing on use of an operator if there was
+a Mutation (USE) involved in the instantiated module.
+*)
+INSTANCE instance_mutate
+====