Skip to content
Snippets Groups Projects
Commit 9b3e6f0d authored by Jan Gruteser's avatar Jan Gruteser
Browse files

cleanup and fix imported module in real tests

parent 1c64c81f
Branches
Tags
No related merge requests found
Pipeline #134729 passed
......@@ -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;
......
......@@ -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"
+ "=================================";
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment