From 88596385f72a9b76fabfcb98d204df64830184a4 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Wed, 23 Sep 2015 12:12:13 +0200
Subject: [PATCH] updated the intersection definition
---
.../resources/standardModules/BBuiltIns.tla | 2 +-
.../de/tlc4b/tlc/integration/BBuiltInsTest.java | 17 +++++++++++++++++
2 files changed, 18 insertions(+), 1 deletion(-)
create mode 100644 src/test/java/de/tlc4b/tlc/integration/BBuiltInsTest.java
diff --git a/src/main/resources/standardModules/BBuiltIns.tla b/src/main/resources/standardModules/BBuiltIns.tla
index 3f2ad56..afbfa2e 100644
--- a/src/main/resources/standardModules/BBuiltIns.tla
+++ b/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
diff --git a/src/test/java/de/tlc4b/tlc/integration/BBuiltInsTest.java b/src/test/java/de/tlc4b/tlc/integration/BBuiltInsTest.java
new file mode 100644
index 0000000..69df14b
--- /dev/null
+++ b/src/test/java/de/tlc4b/tlc/integration/BBuiltInsTest.java
@@ -0,0 +1,17 @@
+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));
+ }
+}
--
GitLab