From 646adb4fc6be45ad1596e3cb17bdf0c2710ea398 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Tue, 12 Mar 2024 16:19:49 -0400 Subject: [PATCH 1/2] Add Variants to STANDARD_MODULES --- .../at/forsyte/apalache/shai/v1/TestCmdExecutorService.scala | 2 +- .../src/main/scala/at/forsyte/apalache/io/lir/TlaWriter.scala | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/shai/src/test/scala/at/forsyte/apalache/shai/v1/TestCmdExecutorService.scala b/shai/src/test/scala/at/forsyte/apalache/shai/v1/TestCmdExecutorService.scala index 4574daa405..94aeb6bfca 100644 --- a/shai/src/test/scala/at/forsyte/apalache/shai/v1/TestCmdExecutorService.scala +++ b/shai/src/test/scala/at/forsyte/apalache/shai/v1/TestCmdExecutorService.scala @@ -126,7 +126,7 @@ object TestCmdExecutorService extends DefaultRunnableSpec { val expectedPayload = """|----------------------------------- MODULE M ----------------------------------- | - |EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache + |EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants | |Foo == TRUE | diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriter.scala index 67d302546b..b1f4a3f995 100644 --- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriter.scala +++ b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/TlaWriter.scala @@ -41,6 +41,6 @@ object TlaWriter { /** * The names of all standard modules that are supported by Apalache IR. */ - val STANDARD_MODULES = List("Integers", "Sequences", "FiniteSets", "TLC", "Apalache") + val STANDARD_MODULES = List("Integers", "Sequences", "FiniteSets", "TLC", "Apalache", "Variants") } From 618906f64f09b28af05e00b9024c8c987bfcf856 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Wed, 13 Mar 2024 15:48:54 -0400 Subject: [PATCH 2/2] Fix integration tests --- test/tla/cli-integration-tests.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md index 3237804fc2..6cec251917 100644 --- a/test/tla/cli-integration-tests.md +++ b/test/tla/cli-integration-tests.md @@ -339,7 +339,7 @@ EXITCODE: OK $ cat output.tla | head -------------------------------- MODULE output -------------------------------- -EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache +EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants CONSTANT (* @@ -414,7 +414,7 @@ EXITCODE: OK $ cat output.tla | head -------------------------------- MODULE output -------------------------------- -EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache +EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants CONSTANT (* @@ -3920,7 +3920,7 @@ EXITCODE: OK $ cat module-lookup/subdir-no-dummy/output.tla -------------------------------- MODULE output -------------------------------- -EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache +EXTENDS Integers, Sequences, FiniteSets, TLC, Apalache, Variants Init == TRUE