don’t rewrite real division operation into definition

src/main/java/de/tla2b/analysis/SymbolRenamer.java

@@ -110,6 +110,7 @@ public class SymbolRenamer extends BuiltInOPs implements TranslationGlobals,
 		BBUILTIN_OPERATOR.put("\\geq", "geq");
 		BBUILTIN_OPERATOR.put("%", "modulo");
 		BBUILTIN_OPERATOR.put("\\div", "div");
+		BBUILTIN_OPERATOR.put("/", "realdiv");
 		BBUILTIN_OPERATOR.put("..", "dot2");
 	}
 

src/main/java/de/tla2b/analysis/TypeChecker.java

@@ -1229,6 +1229,19 @@ public class TypeChecker extends BuiltInOPs implements ASTConstants, BBuildIns,
 			return type;
 		}
 
+			case B_OPCODE_realdiv: { // /
+				try {
+					RealType.getInstance().unify(expected);
+				} catch (UnificationException e) {
+					throw new TypeErrorException(String.format("Expected %s, found REAL at '%s',%n%s", expected,
+						n.getOperator().getName(), n.getLocation()));
+				}
+				for (int i = 0; i < n.getArgs().length; i++) {
+					visitExprOrOpArgNode(n.getArgs()[i], RealType.getInstance());
+				}
+				return RealType.getInstance();
+			}
+
 		case B_OPCODE_dotdot: // ..
 		{
 			try {

src/main/java/de/tla2b/global/BBuildIns.java

@@ -12,6 +12,8 @@ public interface BBuildIns {
 			.uniqueStringOf("*");
 	UniqueString OP_div = UniqueString
 			.uniqueStringOf("\\div");
+	UniqueString OP_realdiv = UniqueString
+		.uniqueStringOf("/");
 	UniqueString OP_mod = UniqueString.uniqueStringOf("%");
 	UniqueString OP_exp = UniqueString.uniqueStringOf("^");
 
@@ -133,4 +135,5 @@ public interface BBuildIns {
 	int B_OPCODE_assert = B_OPCODE_rel_inverse + 1;
 
 	int B_OPCODE_real = B_OPCODE_assert + 1;
+	int B_OPCODE_realdiv = B_OPCODE_real + 1;
 }

src/main/java/de/tla2b/global/BBuiltInOPs.java

@@ -13,6 +13,7 @@ public class BBuiltInOPs implements BBuildIns{
 		B_Opcode_Table.put(OP_minus, B_OPCODE_minus);
 		B_Opcode_Table.put(OP_times, B_OPCODE_times);
 		B_Opcode_Table.put(OP_div, B_OPCODE_div);
+		B_Opcode_Table.put(OP_realdiv, B_OPCODE_realdiv);
 		B_Opcode_Table.put(OP_mod, B_OPCODE_mod);
 		B_Opcode_Table.put(OP_exp, B_OPCODE_exp);
 		B_Opcode_Table.put(OP_uminus, B_OPCODE_uminus);

src/main/java/de/tla2bAst/BAstCreator.java

@@ -1020,6 +1020,15 @@ public class BAstCreator extends BuiltInOPs
 				returnNode = aFlooredDivExpression;
 				break;
 
+			case B_OPCODE_realdiv: // /
+				ADivExpression aDivExpression = new ADivExpression(
+					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
+					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
+
+				setPosition(aDivExpression, opApplNode);
+				returnNode = aDivExpression;
+				break;
+
 			case B_OPCODE_dotdot: // ..
 				returnNode = new AIntervalExpression(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]),
 					visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));

src/test/java/de/tla2b/expression/SimpleExpressionTest.java

@@ -32,6 +32,11 @@ public class SimpleExpressionTest {
 		compareExpr("1.0 : REAL", "1.0 \\in Real");
 	}
 
+	@Test
+	public void testRealDivisionExpression() throws Exception {
+		compareExpr("1.0 / 2.0", "1.0 / 2.0");
+	}
+
 	@Test
 	public void testExist() throws Exception {
 		compareExpr("#a.(a : {1} & 2 > 1)", "\\E a \\in {1}: 2 > 1");

src/test/java/de/tla2b/typechecking/standardmodules/TestModuleReals.java

@@ -133,6 +133,17 @@ public class TestModuleReals {
 		TestUtil.typeCheckString(module);
 	}
 
+	@Test
+	public void testRealDivision() throws TLA2BException {
+		final String module = "-------------- MODULE Testing ----------------\n"
+			+ "EXTENDS Reals \n"
+			+ "CONSTANTS k \n"
+			+ "ASSUME k = 1.0 / 1.0 \n"
+			+ "=================================";
+		TestTypeChecker t = TestUtil.typeCheckString(module);
+		assertEquals("REAL", t.getConstantType("k"));
+	}
+
 	/*
 	 * Interval operator: x .. y
 	 */