From a745931061d7423e0c00fe54fdca29ec18747f3e Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Wed, 15 Jan 2025 08:13:39 +0100
Subject: [PATCH] add function test for first tuple
---
.../java/de/tla2b/prettyprintb/FunctionTest.java | 16 ++++++++++++++++
.../java/de/tla2b/typechecking/FunctionTest.java | 1 -
2 files changed, 16 insertions(+), 1 deletion(-)
diff --git a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
index 69a65cb..b17a67c 100644
--- a/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/FunctionTest.java
@@ -94,6 +94,22 @@ public class FunctionTest {
compare(expected, module);
}
+ @Test
+ public void testFunctionConstructorFirstTuple() throws Exception {
+ // TODO: investigate why a first tuple is a special case
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "CONSTANTS k\n"
+ + "ASSUME k = [<<a,d>> \\in {4} \\X {5}, <<b,c>> \\in {2} \\X {3} |-> a + b + c + d] \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "CONSTANTS k\n"
+ + "PROPERTIES k : (INTEGER * INTEGER) * (INTEGER * INTEGER) +-> INTEGER & k = %(a, d, bc).((a,d) : {4} * {5} & bc : {2} * {3} | (a + prj1(INTEGER, INTEGER)(bc)) + prj2(INTEGER, INTEGER)(bc) + d) \n"
+ + "END";
+ compare(expected, module);
+ }
+
/*
* recursive Function
*/
diff --git a/src/test/java/de/tla2b/typechecking/FunctionTest.java b/src/test/java/de/tla2b/typechecking/FunctionTest.java
index 896633b..e20d01a 100644
--- a/src/test/java/de/tla2b/typechecking/FunctionTest.java
+++ b/src/test/java/de/tla2b/typechecking/FunctionTest.java
@@ -395,7 +395,6 @@ public class FunctionTest {
/*
* Except @
*/
-
@Test
public void testAt2() throws TLA2BException {
final String module = "-------------- MODULE Testing ----------------\n"
--
GitLab