From 8c8f4ae75899a329a380062ad51fd06385526f07 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Mon, 30 Dec 2024 09:14:32 +0100
Subject: [PATCH] add pretty-print test for real division

---
 .../standardmodules/ModuleRealsTest.java      | 22 +++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleRealsTest.java

diff --git a/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleRealsTest.java b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleRealsTest.java
new file mode 100644
index 0000000..0e455af
--- /dev/null
+++ b/src/test/java/de/tla2b/prettyprintb/standardmodules/ModuleRealsTest.java
@@ -0,0 +1,22 @@
+package de.tla2b.prettyprintb.standardmodules;
+
+import org.junit.Test;
+
+import static de.tla2b.util.TestUtil.compare;
+
+public class ModuleRealsTest {
+
+	// Arithmetic operator: /
+	@Test
+	public void testArithmeticOperators() throws Exception {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Reals \n"
+			+ "ASSUME 1.0 / 2.0 = 0.5 \n"
+			+ "=================================";
+		final String expected = "MACHINE Testing\n"
+			+ "PROPERTIES 1.0 / 2.0 = 0.5 \n"
+			+ "END";
+		compare(expected, module);
+	}
+
+}
-- 
GitLab