From da615fa7a7c9edc0671c995e53fee74216f4919d Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Mon, 16 Mar 2015 15:26:43 +0100
Subject: [PATCH] updated parser version
---
build.gradle | 2 +-
.../de/tlc4b/analysis/typerestriction/TypeRestrictor.java | 5 +----
2 files changed, 2 insertions(+), 5 deletions(-)
diff --git a/build.gradle b/build.gradle
index 0aee239..955cd14 100644
--- a/build.gradle
+++ b/build.gradle
@@ -20,7 +20,7 @@ configurations { // configuration that holds jars to copy into lib
releaseJars
}
-def parser_version = '2.4.28-SNAPSHOT'
+def parser_version = '2.4.36-SNAPSHOT'
dependencies {
//compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
diff --git a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
index 89203c9..d695f4c 100644
--- a/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
+++ b/src/main/java/de/tlc4b/analysis/typerestriction/TypeRestrictor.java
@@ -7,8 +7,6 @@ import java.util.Hashtable;
import java.util.List;
import java.util.Set;
-import tla2sany.semantic.OpApplNode;
-import tla2sany.semantic.OpDefNode;
import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AAnySubstitution;
@@ -16,7 +14,6 @@ import de.be4.classicalb.core.parser.node.ABecomesSuchSubstitution;
import de.be4.classicalb.core.parser.node.AComprehensionSetExpression;
import de.be4.classicalb.core.parser.node.AConjunctPredicate;
import de.be4.classicalb.core.parser.node.AConstraintsMachineClause;
-import de.be4.classicalb.core.parser.node.ACoupleExpression;
import de.be4.classicalb.core.parser.node.ADisjunctPredicate;
import de.be4.classicalb.core.parser.node.AEqualPredicate;
import de.be4.classicalb.core.parser.node.AExistsPredicate;
@@ -566,7 +563,7 @@ public class TypeRestrictor extends DepthFirstAdapter {
String localVariableName = Utils.getIdentifierAsString(id
.getIdentifier());
throw new NotSupportedException(
- "Can not restrict the type of the variable '"
+ "Unable to restrict the type of the variable '"
+ localVariableName
+ "' to a finite set. TLC is not able to handle infinite sets.\n"
+ e.getStartPos());
--
GitLab