diff --git a/src/main/java/de/tla2b/global/BBuildIns.java b/src/main/java/de/tla2b/global/BBuildIns.java index 424a955054e5ce6ee35789b465adb49852430dd4..af2ca6c81706bf1d80adb0cd2cbe470cf56a6d4d 100644 --- a/src/main/java/de/tla2b/global/BBuildIns.java +++ b/src/main/java/de/tla2b/global/BBuildIns.java @@ -30,7 +30,7 @@ public interface BBuildIns { UniqueString OP_int = UniqueString .uniqueStringOf("Int"); UniqueString OP_real = UniqueString - .uniqueStringOf("Real"); + .uniqueStringOf("Real"); UniqueString OP_bool = UniqueString .uniqueStringOf("BOOLEAN"); UniqueString OP_true = UniqueString diff --git a/src/main/java/de/tla2bAst/ExpressionTranslator.java b/src/main/java/de/tla2bAst/ExpressionTranslator.java index 76121dfee6cfb553dfe400205b6c53faa28cae61..5e69ae449829e4be826df39c7c6e1648868e619a 100644 --- a/src/main/java/de/tla2bAst/ExpressionTranslator.java +++ b/src/main/java/de/tla2bAst/ExpressionTranslator.java @@ -27,8 +27,8 @@ import de.tla2b.exceptions.TLA2BException; public class ExpressionTranslator implements SyntaxTreeConstants { private final String tlaExpression; - private final ArrayList<String> variables = new ArrayList<String>(); - private final ArrayList<String> noVariables = new ArrayList<String>(); + private final ArrayList<String> variables = new ArrayList<>(); + private final ArrayList<String> noVariables = new ArrayList<>(); private Start expressionStart; private ModuleNode moduleNode; private String expr; @@ -51,9 +51,9 @@ public class ExpressionTranslator implements SyntaxTreeConstants { String dir = System.getProperty("java.io.tmpdir"); ToolIO.setUserDir(dir); - File tempFile = null; - String moduleName = null; - String module = null; + File tempFile; + String moduleName; + String module; try { tempFile = File.createTempFile("Testing", ".tla"); @@ -75,9 +75,9 @@ public class ExpressionTranslator implements SyntaxTreeConstants { evalVariables(spec, moduleName); StringBuilder sb = new StringBuilder(); - sb.append("----MODULE " + moduleName + " ----\n"); - sb.append("EXTENDS Naturals, Integers, Sequences, FiniteSets \n"); - if (variables.size() > 0) { + sb.append("----MODULE ").append(moduleName).append(" ----\n"); + sb.append("EXTENDS Naturals, Integers, Reals, Sequences, FiniteSets \n"); + if (!variables.isEmpty()) { sb.append("VARIABLES "); for (int i = 0; i < variables.size(); i++) { if (i != 0) { @@ -193,9 +193,7 @@ public class ExpressionTranslator implements SyntaxTreeConstants { SANY.frontEndInitialize(spec, ToolIO.out); SANY.frontEndParse(spec, ToolIO.out); - } catch (InitException e1) { - System.out.println(e1); - } catch (ParseException e1) { + } catch (InitException | ParseException e1) { System.out.println(e1); } @@ -217,19 +215,20 @@ public class ExpressionTranslator implements SyntaxTreeConstants { // this code seems to assume that there is no variable clash between outer and nested variables // I guess the parser will then generate "Multiply-defined symbol ..." errors - for (int i = 0; i < noVariables.size(); i++) { - variables.remove(noVariables.get(i)); + for (String noVariable : noVariables) { + variables.remove(noVariable); } } - private final static Set<String> KEYWORDS = new HashSet<String>(); + private final static Set<String> KEYWORDS = new HashSet<>(); static { KEYWORDS.add("BOOLEAN"); KEYWORDS.add("TRUE"); KEYWORDS.add("FALSE"); KEYWORDS.add("Nat"); KEYWORDS.add("Int"); + KEYWORDS.add("Real"); KEYWORDS.add("Cardinality"); KEYWORDS.add("IsFiniteSet"); KEYWORDS.add("Append"); @@ -327,10 +326,6 @@ public class ExpressionTranslator implements SyntaxTreeConstants { } public static String allMessagesToString(String[] allMessages) { - StringBuilder sb = new StringBuilder(); - for (int i = 0; i < allMessages.length - 1; i++) { - sb.append(allMessages[i] + "\n"); - } - return sb.toString(); + return Translator.allMessagesToString(allMessages); } } diff --git a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java index 91b392a433c89380439c603ed948a4fdd4ce534c..7f4553833e0fe7f8661d8a032a507fd4097ac30f 100644 --- a/src/test/java/de/tla2b/expression/SimpleExpressionTest.java +++ b/src/test/java/de/tla2b/expression/SimpleExpressionTest.java @@ -27,11 +27,9 @@ public class SimpleExpressionTest { compareExpr("-1 : INTEGER", "-1 \\in Int"); } - // FIXME: real_set(none) vs identifier(none,'Real') - @Ignore @Test public void testModulReals() throws Exception { - compareExpr("1 : REAL", "1 \\in Real"); + compareExpr("1.0 : REAL", "1.0 \\in Real"); } @Test