Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • release/1.1.4
  • release/1.1.3
  • release/1.1.1
  • 1.4.1
  • 1.4.0
  • 1.3.0
  • 1.2.1
  • 1.2.0
  • 1.1.5
  • 1.1.4
  • 1.1.3
  • 1.1.1
  • 1.1.0
  • 1.0.9
  • 1.0.8
  • 1.0.7
  • v1.0.5
  • 1.0.5
19 results

TestUtil.java

Blame
  • Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    TestUtil.java 6.77 KiB
    /**
     * @author Dominik Hansen <Dominik.Hansen at hhu.de>
     **/
    
    package de.tla2b.util;
    
    import static org.junit.Assert.assertEquals;
    
    import util.FileUtil;
    import de.be4.classicalb.core.parser.BParser;
    import de.be4.classicalb.core.parser.exceptions.BException;
    import de.be4.classicalb.core.parser.node.Node;
    import de.be4.classicalb.core.parser.node.Start;
    import de.tla2b.exceptions.FrontEndException;
    import de.tla2b.exceptions.TLA2BException;
    import de.tla2b.output.ASTPrettyPrinter;
    import de.tla2b.output.Renamer;
    import de.tla2bAst.Translator;
    import util.ToolIO;
    
    public class TestUtil {
    
    	// public static StringBuilder translateString(String moduleString)
    	// throws FrontEndException, TLA2BException, AbortException {
    	// ToolIO.setMode(ToolIO.TOOL);
    	// ToolIO.reset();
    	// Tla2BTranslator translator = new Tla2BTranslator();
    	// translator.startTest(moduleString, null);
    	// return translator.translate();
    	// }
    
    	public static void runModule(String tlaFile) throws Exception {
    		Translator t = new Translator(tlaFile);
    		Start start = t.translate();
    
    		System.out.println("-------------------");
    		ASTPrettyPrinter aP = new ASTPrettyPrinter(start);
    		start.apply(aP);
    		System.out.println(aP.getResultString());
    
    		final BParser parser = new BParser("testcase");
    		final Start ppStart = parser.parse(aP.getResultString(), false);
    
    		String result = getTreeAsString(start);
    		System.out.println(result);
    		String ppResult = getTreeAsString(ppStart);
    		System.out.println(ppResult);
    
    		System.out.println("-------------------");
    		assertEquals(result, ppResult);
    		// System.out.println(t.getBDefinitions().getDefinitionNames());
    	}
    
    	public static void compareExpr(String bExpr, String tlaExpr)
    			throws BException {
    		ToolIO.setMode(ToolIO.TOOL);
    		ToolIO.reset();
    		Start resultNode = Translator.translateTlaExpression(tlaExpr);
    		Renamer renamer = new Renamer(resultNode);
    		ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
    		resultNode.apply(aP);
    		System.out.println(aP.getResultString());
    		String bAstString = getAstStringofBExpressionString(bExpr);
    		String result = getAstStringofBExpressionString(aP.getResultString());
    		// String tlaAstString = getTreeAsString(resultNode);
    		assertEquals(bAstString, result);
    	}
    
    	public static void compareExprIncludingModel(String bExpr, String tlaExpr,
    			String moduleString) throws TLA2BException, BException {
    		Translator trans = new Translator(moduleString, null);
    		trans.translate();
    		Start resultNode = trans.translateExpression(tlaExpr);
    		Renamer renamer = new Renamer(resultNode);
    		ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode, renamer);
    		resultNode.apply(aP);
    		String bAstString = getAstStringofBExpressionString(bExpr);
    		String result = getAstStringofBExpressionString(aP.getResultString());
    		assertEquals(bAstString, result);
    	}
    
    	public static void compare(String bMachine, String tlaModule)
    			throws BException, TLA2BException {
    		ToolIO.setMode(ToolIO.TOOL);
    		String expected = getAstStringofBMachineString(bMachine);
    		System.out.println(expected);
    
    		Translator trans = new Translator(tlaModule, null);
    		Start resultNode = trans.translate();
    		String result = getTreeAsString(resultNode);
    		System.out.println(result);
    		ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode);
    		resultNode.apply(aP);
    		System.out.println("-------------------");
    		System.out.println(aP.getResultString());
    		final BParser parser = new BParser("testcase");
    		Start ast = parser.parse(aP.getResultString(), false);
    		// BParser.printASTasProlog(System.out, new BParser(), new
    		// File("./test.mch"), resultNode, false, true, null);
    
    		// System.out.println(result);
    		assertEquals(expected, result);
    		assertEquals(expected, getTreeAsString(ast));
    	}
    
    	public static void compare(String bMachine, String tlaModule, String config)
    			throws BException, TLA2BException {
    		ToolIO.setMode(ToolIO.TOOL);
    		String expected = getAstStringofBMachineString(bMachine);
    		System.out.println(expected);
    
    		Translator trans = new Translator(tlaModule, config);
    		Start resultNode = trans.translate();
    
    		ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode);
    		resultNode.apply(aP);
    		System.out.println(aP.getResultString());
    
    		// BParser.printASTasProlog(System.out, new BParser(), new
    		// File("./test.mch"), resultNode, false, true, null);
    
    		String result = getTreeAsString(resultNode);
    		System.out.println(result);
    		assertEquals(expected, result);
    	}
    
    	public static String getTreeAsString(Node node) {
    		final Ast2String ast2String = new Ast2String();
    		node.apply(ast2String);
    		return ast2String.toString();
    	}
    
    	public static void renamerTest(String tlaFile) throws Exception {
    		Translator t = new Translator(tlaFile);
    		Start start = t.translate();
    		Renamer renamer = new Renamer(start);
    		ASTPrettyPrinter aP = new ASTPrettyPrinter(start, renamer);
    		start.apply(aP);
    		System.out.println(aP.getResultString());
    
    		final BParser parser = new BParser("testcase");
    		parser.parse(aP.getResultString(), false);
    	}
    
    	public static TestTypeChecker typeCheckString(String moduleString)
    			throws FrontEndException, TLA2BException {
    		ToolIO.setMode(ToolIO.TOOL);
    		ToolIO.reset();
    		TestTypeChecker testTypeChecker = new TestTypeChecker();
    		testTypeChecker.startTest(moduleString, null);
    		return testTypeChecker;
    
    	}
    
    	public static TestTypeChecker typeCheckString(String moduleString,
    			String configString) throws FrontEndException, TLA2BException {
    		ToolIO.setMode(ToolIO.TOOL);
    		ToolIO.reset();
    		TestTypeChecker testTypeChecker = new TestTypeChecker();
    		testTypeChecker.startTest(moduleString, configString);
    		return testTypeChecker;
    	}
    
    	public static TestTypeChecker typeCheck(String moduleFileName)
    			throws FrontEndException, TLA2BException {
    		ToolIO.setMode(ToolIO.TOOL);
    		ToolIO.reset();
    		moduleFileName = moduleFileName.replace('/', FileUtil.separatorChar);
    		TestTypeChecker testTypeChecker = new TestTypeChecker();
    		testTypeChecker.start(moduleFileName);
    		return testTypeChecker;
    	}
    
    	public static String getAstStringofBMachineString(final String testMachine)
    			throws BException {
    		final BParser parser = new BParser("testcase");
    		final Start startNode = parser.parse(testMachine, false);
    
    		final Ast2String ast2String = new Ast2String();
    		startNode.apply(ast2String);
    		final String string = ast2String.toString();
    		return string;
    	}
    
    	public static String getAstStringofBExpressionString(final String expr)
    			throws BException {
    		final BParser parser = new BParser("testcase");
    		final Start startNode = parser.parse("#FORMULA " + expr, false);
    
    		final Ast2String ast2String = new Ast2String();
    		startNode.apply(ast2String);
    		final String string = ast2String.toString();
    		return string;
    	}
    
    }