ModuleAndExpressionTest.java

package de.tla2b.expression;

import de.tla2b.exceptions.ExpressionTranslationException;
import org.junit.Test;

import static de.tla2b.util.TestUtil.compareExprIncludingModel;

public class ModuleAndExpressionTest {

	@Test
	public void testCon() throws Exception {
		String module = "---- MODULE Testing ----\n"
			+ "CONSTANTS k \n"
			+ "ASSUME k = 4"
			+ "===============";
		compareExprIncludingModel("k = 1", "k = 1", module);
	}

	@Test
	public void testVar() throws Exception {
		String module = "---- MODULE Testing ----\n"
				+ "VARIABLES v \n"
				+ "Init == v = 4.0 \n"
				+ "Next == v' = 5.0"
				+ "===============";
		compareExprIncludingModel("v = 4.0", "v = 4.0", module);
	}

	@Test(expected = ExpressionTranslationException.class)
	public void testConTypeError() throws Exception {
		String module = "---- MODULE Testing ----\n"
			+ "CONSTANTS k \n"
			+ "ASSUME k = 4"
			+ "===============";
		compareExprIncludingModel(null, "k = TRUE", module);
	}

	@Test(expected = ExpressionTranslationException.class)
	public void testVarTypeError() throws Exception {
		String module = "---- MODULE Testing ----\n"
				+ "VARIABLES v \n"
				+ "Init == v = 4.0 \n"
				+ "Next == v' = 5.0"
				+ "===============";
		compareExprIncludingModel(null, "v = TRUE", module);
	}

	@Test
	public void testConAdditionalFreeVariable() throws Exception {
		String module = "---- MODULE Testing ----\n"
				+ "CONSTANTS k \n"
				+ "ASSUME k = 4"
				+ "===============";
		compareExprIncludingModel("k = s", "k = s", module);
	}

	@Test
	public void testVarAdditionalFreeVariable() throws Exception {
		String module = "---- MODULE Testing ----\n"
				+ "VARIABLES v \n"
				+ "Init == v = 4.0 \n"
				+ "Next == v' = 5.0"
				+ "===============";
		compareExprIncludingModel("v = s", "v = s", module);
	}

	@Test(expected = ExpressionTranslationException.class)
	public void testAdditionalFreeVariableError() throws Exception {
		String module = "---- MODULE Testing ----\n"
				+ "CONSTANTS k \n"