diff --git a/src/test/java/de/tla2b/prettyprintb/ActionsTest.java b/src/test/java/de/tla2b/prettyprintb/ActionsTest.java index adaad8aa28ca5df650ab507be55212385ba07d3c..1bdb1c7968ef2637c108894cda4d82b3715b5413 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 8899544f22bb9e2eb152e0a286eed8abe7042466..2291c75a9014d6b001580ac4b9ac3027f3c35599 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 */