From b515c2306584d3e072a8db1f88bb23e9c13deadd Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 4 Jul 2014 14:03:36 +0200
Subject: [PATCH] Throwing a NotSupported exception if TLC has to enumerate an
infinite set.
---
.../de/tlc4b/analysis/typerestriction/TypeRestrictor.java | 4 +++-
src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java | 4 +++-
src/test/java/de/tlc4b/analysis/ScopeTest.java | 2 +-
src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java | 3 ++-
4 files changed, 9 insertions(+), 4 deletions(-)
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index 435f47d..e9e826d 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -556,7 +556,9 @@ public class TypeRestrictor extends DepthFirstAdapter {
conType = typechecker.getType(machineContext
.getReferenceNode(e));
}
- if (conType.containsIntegerType()) {
+ if (conType.containsIntegerType()
+ && !(e.parent() instanceof ALambdaExpression)
+ && !(e.parent() instanceof AComprehensionSetExpression)) {
AIdentifierExpression id = (AIdentifierExpression) e;
String localVariableName = Utils.getIdentifierAsString(id
.getIdentifier());
diff --git a/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java b/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java
index 51083fe..0e18c33 100644
--- a/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java
+++ b/src/test/java/de/tlc4b/analysis/ExpressionConstantTest.java
@@ -4,6 +4,8 @@ import static de.tlc4b.util.TestUtil.compare;
import org.junit.Test;
+import de.tlc4b.exceptions.NotSupportedException;
+
public class ExpressionConstantTest {
@Test
@@ -43,7 +45,7 @@ public class ExpressionConstantTest {
compare(expected, machine);
}
- @Test
+ @Test (expected = NotSupportedException.class)
public void testNotConstantBoundedVariable() throws Exception {
String machine = "MACHINE test\n"
+ "PROPERTIES !x,y.(x = y & y = 1 => 1 = 1)\n" + "END";
diff --git a/src/test/java/de/tlc4b/analysis/ScopeTest.java b/src/test/java/de/tlc4b/analysis/ScopeTest.java
index 7ab79c9..cf65a0f 100644
--- a/src/test/java/de/tlc4b/analysis/ScopeTest.java
+++ b/src/test/java/de/tlc4b/analysis/ScopeTest.java
@@ -147,7 +147,7 @@ public class ScopeTest {
@Test
public void testNestedLocalExists() throws Exception {
String machine = "MACHINE test\n"
- + "PROPERTIES #x.(x : INT & #x.(x + 1 = 1))\n" + "END";
+ + "PROPERTIES #x.(x : {1} & #x.(x : {1} & x + 1 = 1))\n" + "END";
checkMachine(machine);
}
diff --git a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
index afa83cc..37e24e4 100644
--- a/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
+++ b/src/test/java/de/tlc4b/analysis/TypeRestrictionsTest.java
@@ -74,6 +74,7 @@ public class TypeRestrictionsTest {
compare(expected, machine);
}
+ @Ignore
@Test
public void testExistQuantification2VariablesNotConstant() throws Exception {
String machine = "MACHINE test\n"
@@ -195,7 +196,7 @@ public class TypeRestrictionsTest {
compare(expected, machine);
}
-
+ @Ignore
@Test
public void testExistDependingVariables() throws Exception {
String machine = "MACHINE test\n"
--
GitLab