updated the intersection definition

src/main/resources/standardModules/BBuiltIns.tla

@@ -73,7 +73,7 @@ NotStrictSubset(S, T) == ~ (S \subset T)
 
 RECURSIVE Inter(_)
 Inter(S) ==
-  IF Assert(S = {}, "Error: Applied the inter operator to an empty set.")
+  IF Assert(S /= {}, "Error: Applied the inter operator to an empty set.")
 	THEN
     LET e == (CHOOSE e \in S: TRUE)
     IN  IF  Cardinality(S) = 1

src/test/java/de/tlc4b/tlc/integration/BBuiltInsTest.java

+package de.tlc4b.tlc.integration;
+
+import static de.tlc4b.tlc.TLCResults.TLCResult.*;
+import static de.tlc4b.util.TestUtil.testString;
+import static org.junit.Assert.assertEquals;
+
+import org.junit.Test;
+
+public class BBuiltInsTest {
+
+	@Test
+	public void testIntersectionWDError() throws Exception {
+		String machine = "MACHINE Test\n" + "PROPERTIES \n"
+				+ "inter({}) = {} \n" + "END";
+		assertEquals(WellDefinednessError, testString(machine));
+	}
+}