diff --git a/src/main/java/de/tla2b/pprint/BAstCreator.java b/src/main/java/de/tla2b/pprint/BAstCreator.java index 6d6b6fff89029db5a2101775907a20a9392ef8ef..1cf06cba92228dd5ae5c99e8b49a239d60c675a2 100644 --- a/src/main/java/de/tla2b/pprint/BAstCreator.java +++ b/src/main/java/de/tla2b/pprint/BAstCreator.java @@ -59,6 +59,7 @@ import de.be4.classicalb.core.parser.node.ALambdaExpression; import de.be4.classicalb.core.parser.node.ALessEqualPredicate; import de.be4.classicalb.core.parser.node.ALessPredicate; import de.be4.classicalb.core.parser.node.AMachineHeader; +import de.be4.classicalb.core.parser.node.AMachineMachineVariant; import de.be4.classicalb.core.parser.node.AMemberPredicate; import de.be4.classicalb.core.parser.node.AMinusOrSetSubtractExpression; import de.be4.classicalb.core.parser.node.AMultOrCartExpression; @@ -132,6 +133,7 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, machineClauseList = new ArrayList<PMachineClause>(); AAbstractMachineParseUnit aAbstractMachineParseUnit = new AAbstractMachineParseUnit(); + aAbstractMachineParseUnit.setVariant(new AMachineMachineVariant()); AMachineHeader machineHeader = new AMachineHeader(); List<TIdentifierLiteral> headerName = createTIdentifierLiteral(moduleNode .getName().toString()); diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java index b5744d7cd451f9c89a064f5f154341725fe8db5f..fbbe9a36479f4f90aebde9c1d118ac07dfe9c836 100644 --- a/src/main/java/de/tla2bAst/Translator.java +++ b/src/main/java/de/tla2bAst/Translator.java @@ -5,6 +5,7 @@ import java.io.FileWriter; import java.io.IOException; import de.be4.classicalb.core.parser.node.Node; +import de.be4.classicalb.core.parser.node.Start; import de.tla2b.analysis.InstanceTransformation; import de.tla2b.analysis.SpecAnalyser; import de.tla2b.analysis.SymbolRenamer; @@ -41,19 +42,8 @@ public class Translator { parse(); } - private void parse(){ - moduleName = evalFileName(moduleFileName); - - TLAParser tlaParser = new TLAParser(null); - moduleNode = tlaParser.parseModule(moduleName); - - modelConfig = null; - if (configFileName != null) { - modelConfig = new ModelConfig(configFileName, null); - modelConfig.parse(); - } - } - + + //Used for Testing public Translator(String moduleString, String configString, int i) { moduleName = "Testing"; File dir = new File("temp/"); @@ -90,8 +80,21 @@ public class Translator { parse(); } + + private void parse(){ + moduleName = evalFileName(moduleFileName); + + TLAParser tlaParser = new TLAParser(null); + moduleNode = tlaParser.parseModule(moduleName); + + modelConfig = null; + if (configFileName != null) { + modelConfig = new ModelConfig(configFileName, null); + modelConfig.parse(); + } + } - public Node translate() throws TLA2BException { + public Start translate() throws TLA2BException { InstanceTransformation trans = new InstanceTransformation(moduleNode); trans.start(); diff --git a/src/test/java/de/tla2b/prettyprintb/SimpleModulesTest.java b/src/test/java/de/tla2b/prettyprintb/SimpleModulesTest.java new file mode 100644 index 0000000000000000000000000000000000000000..2a895f7bc98ceadeca78666e7a9643ced8ff66cf --- /dev/null +++ b/src/test/java/de/tla2b/prettyprintb/SimpleModulesTest.java @@ -0,0 +1,20 @@ +package de.tla2b.prettyprintb; + +import static de.tla2b.util.TestUtil.compare; + +import org.junit.Test; + +public class SimpleModulesTest { + + + @Test + public void testSimpleModule() throws Exception { + final String module = "-------------- MODULE Testing ----------------\n" + + "================================="; + + final String expected = "MACHINE Testing\n" + + "END"; + compare(expected, module); + } + +} diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java index d8f7b1d17b5d5a653e5359d9467b9411f072d41a..a57adc55d2e70d10ab8cf5c27239c8cc9193ca8d 100644 --- a/src/test/java/de/tla2b/util/TestUtil.java +++ b/src/test/java/de/tla2b/util/TestUtil.java @@ -7,11 +7,13 @@ package de.tla2b.util; import static org.junit.Assert.assertEquals; import java.io.BufferedReader; +import java.io.File; import java.io.FileReader; import java.io.IOException; import de.be4.classicalb.core.parser.BParser; import de.be4.classicalb.core.parser.exceptions.BException; +import de.be4.classicalb.core.parser.node.AAbstractMachineParseUnit; import de.be4.classicalb.core.parser.node.Node; import de.be4.classicalb.core.parser.node.Start; import de.tla2b.exceptions.FrontEndException; @@ -39,7 +41,10 @@ public class TestUtil { System.out.println(expected); Translator trans = new Translator(tlaModule, null, 1); - Node resultNode = trans.translate(); + Start resultNode = trans.translate(); + + //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); @@ -138,7 +143,7 @@ public class TestUtil { 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();