diff --git a/src/main/java/de/tla2b/analysis/SymbolRenamer.java b/src/main/java/de/tla2b/analysis/SymbolRenamer.java index 56ed582af98f39e9d4707c83e5d8bfee1e0de17c..bc89947fa4573e7dce11432a95784c41b55b7679 100644 --- a/src/main/java/de/tla2b/analysis/SymbolRenamer.java +++ b/src/main/java/de/tla2b/analysis/SymbolRenamer.java @@ -21,7 +21,7 @@ import tlc2.tool.BuiltInOPs; public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, ASTConstants { - private final static Set<String> KEYWORDS = new HashSet<String>(); + private final static Set<String> KEYWORDS = new HashSet<>(); static { KEYWORDS.add("seq"); KEYWORDS.add("left"); @@ -71,12 +71,11 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, KEYWORDS.add("CONSTRAINTS"); KEYWORDS.add("MODEL"); KEYWORDS.add("SYSTEM"); - KEYWORDS.add("MACHINE"); KEYWORDS.add("EVENTS"); KEYWORDS.add("OPERATIONS"); } - private final static Hashtable<String, String> INFIX_OPERATOR = new Hashtable<String, String>(); + private final static Hashtable<String, String> INFIX_OPERATOR = new Hashtable<>(); static { INFIX_OPERATOR.put("!!", "exclamationmark2"); INFIX_OPERATOR.put("??", "questionmark2"); @@ -98,7 +97,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, INFIX_OPERATOR.put("...", "dot3"); } - private final static Hashtable<String, String> BBUILTIN_OPERATOR = new Hashtable<String, String>(); + private final static Hashtable<String, String> BBUILTIN_OPERATOR = new Hashtable<>(); static { BBUILTIN_OPERATOR.put("+", "plus"); BBUILTIN_OPERATOR.put("-", "minus"); @@ -117,8 +116,8 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals, private final ModuleNode moduleNode; private final Set<OpDefNode> usedDefinitions; - private final Set<String> globalNames = new HashSet<String>(); - private final Hashtable<OpDefNode, Set<String>> usedNamesTable = new Hashtable<OpDefNode, Set<String>>(); + private final Set<String> globalNames = new HashSet<>(); + private final Hashtable<OpDefNode, Set<String>> usedNamesTable = new Hashtable<>(); public SymbolRenamer(ModuleNode moduleNode, SpecAnalyser specAnalyser) { this.moduleNode = moduleNode; diff --git a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java index 7926e6a218199162455fe8b1b5695e32b0a10051..6e56bcbbcd1ba75984168d49feb47835edb02258 100644 --- a/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java +++ b/src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java @@ -55,7 +55,7 @@ public class TestModuleReals { + "EXTENDS Reals \n" + "ASSUME -1 = -1.0 \n" + "================================="; - TestTypeChecker t = TestUtil.typeCheckString(module); + TestUtil.typeCheckString(module); } @Test(expected = TypeErrorException.class) @@ -100,7 +100,7 @@ public class TestModuleReals { @Test public void testArithmeticOperators() throws TLA2BException { final String module = "-------------- MODULE Testing ----------------\n" - + "EXTENDS Naturals \n" + + "EXTENDS Reals \n" + "ASSUME 2.0 = 1.0 + 1.0 \n" + "================================="; TestUtil.typeCheckString(module); @@ -109,7 +109,7 @@ public class TestModuleReals { @Test(expected = TypeErrorException.class) public void testArithmeticOperatorsException1() throws TLA2BException { final String module = "-------------- MODULE Testing ----------------\n" - + "EXTENDS Naturals \n" + + "EXTENDS Reals \n" + "ASSUME TRUE = 1.0 + 1.0 \n" + "================================="; TestUtil.typeCheckString(module); @@ -118,7 +118,7 @@ public class TestModuleReals { @Test(expected = TypeErrorException.class) public void testArithmeticOperatorsException2() throws TLA2BException { final String module = "-------------- MODULE Testing ----------------\n" - + "EXTENDS Naturals \n" + + "EXTENDS Reals \n" + "ASSUME 2.0 = 1.0 + 1 \n" + "================================="; TestUtil.typeCheckString(module); @@ -127,7 +127,7 @@ public class TestModuleReals { @Test(expected = TypeErrorException.class) public void testArithmeticOperatorsException3() throws TLA2BException { final String module = "-------------- MODULE Testing ----------------\n" - + "EXTENDS Naturals \n" + + "EXTENDS Reals \n" + "ASSUME 2 = 1.0 + 1.0 \n" + "================================="; TestUtil.typeCheckString(module); @@ -147,11 +147,10 @@ public class TestModuleReals { /* * Interval operator: x .. y */ - @Test(expected = TypeErrorException.class) public void testDotDotReal() throws TLA2BException { final String module = "-------------- MODULE Testing ----------------\n" - + "EXTENDS Naturals \n" + + "EXTENDS Reals \n" + "CONSTANTS k \n" + "ASSUME k = 1.0 .. 3.0 \n" + "=================================";