From 346b1111013ee93ffd707cc6ebd9763f13e47697 Mon Sep 17 00:00:00 2001
From: Jan Gruteser <jan.gruteser@hhu.de>
Date: Mon, 30 Dec 2024 11:17:03 +0100
Subject: [PATCH] add two tests
negation ~ and missing Init
---
.../java/de/tla2b/prettyprintb/ActionsTest.java | 12 ++++++++++++
.../de/tla2b/prettyprintb/LogicOperatorsTest.java | 13 +++++++++++++
2 files changed, 25 insertions(+)
diff --git a/src/test/java/de/tla2b/prettyprintb/ActionsTest.java b/src/test/java/de/tla2b/prettyprintb/ActionsTest.java
index adaad8a..1bdb1c7 100644
--- a/src/test/java/de/tla2b/prettyprintb/ActionsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/ActionsTest.java
@@ -1,5 +1,6 @@
package de.tla2b.prettyprintb;
+import de.tla2b.exceptions.SemanticErrorException;
import org.junit.Ignore;
import org.junit.Test;
@@ -63,4 +64,15 @@ public class ActionsTest {
+ "END";
compare(expected, module);
}
+
+ @Test(expected = SemanticErrorException.class)
+ public void testMissingInit() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "EXTENDS Naturals \n"
+ + "VARIABLES x \n"
+ + "Next == x'=x+1 \n"
+ + "=================================";
+
+ compare("MACHINE Testing END", module);
+ }
}
diff --git a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
index 8899544..2291c75 100644
--- a/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
+++ b/src/test/java/de/tla2b/prettyprintb/LogicOperatorsTest.java
@@ -80,6 +80,19 @@ public class LogicOperatorsTest {
compare(expected, module);
}
+ @Test
+ public void testNegation2() throws Exception {
+ final String module = "-------------- MODULE Testing ----------------\n"
+ + "CONSTANTS a,b \n"
+ + "ASSUME a \\in BOOLEAN /\\ b = ~a \n"
+ + "=================================";
+
+ final String expected = "MACHINE Testing\n"
+ + "CONSTANTS a, b \n"
+ + "PROPERTIES a : BOOL & b : BOOL & (a : BOOL & b = bool(not(a = TRUE))) \n" + "END";
+ compare(expected, module);
+ }
+
/*
* Implication and Equivalence: =>, \equiv
*/
--
GitLab