From bd261f38256817e6d1fedd868e60243f88c67980 Mon Sep 17 00:00:00 2001
From: hansene <dominik_hansen@web.de>
Date: Thu, 30 Jul 2015 19:38:22 +0200
Subject: [PATCH] Adapted the translator to the new parser version

---
 build.gradle                                  | 31 +++++++------
 .../de/tla2b/analysis/RecursiveFunktion.java  | 45 +++++++++----------
 .../java/de/tla2b/output/PrologPrinter.java   | 10 -----
 src/main/java/de/tla2bAst/SimpleResolver.java |  8 +++-
 src/main/java/de/tla2bAst/Translator.java     | 12 +++--
 src/test/java/de/tla2b/util/TestUtil.java     |  5 ---
 6 files changed, 53 insertions(+), 58 deletions(-)

diff --git a/build.gradle b/build.gradle
index 2e6b66c..555420f 100644
--- a/build.gradle
+++ b/build.gradle
@@ -7,8 +7,6 @@ apply plugin: 'findbugs'
 project.version = '1.0.5-SNAPSHOT'
 project.group = 'de.prob'
 
-sourceCompatibility = 1.5
-
 repositories {
 	mavenCentral()
 	maven {
@@ -20,7 +18,7 @@ configurations { // configuration that holds jars to copy into lib
 	releaseJars 
 }
  
-def parser_version = '2.4.28-SNAPSHOT'
+def parser_version = '2.5.0-SNAPSHOT'
 
 dependencies {
 	//compile (group: 'com.microsoft', name: 'tla2tools', version: '1.4.6')
@@ -43,32 +41,34 @@ dependencies {
 }
 
 jacoco {
-    toolVersion = "0.6.2.201302030002"
+    toolVersion = "0.7.1.201405082137"
     reportsDir = file("$buildDir/customJacocoReportDir")
 }
 
-jacocoTestReport {
-    reports {
-        xml.enabled false
-        csv.enabled false
-        html.destination "${buildDir}/jacocoHtml"
-    }
-}
+// type 'gradle tla2b jacocoIntegrationTestReport' in order to run the jacoco code coverage analysis
+task jacocoIntegrationTestReport(type: JacocoReport) {
+	sourceSets sourceSets.main
+	//executionData files('build/jacoco/integrationTests.exec')
+	executionData fileTree(project.rootDir.absolutePath).include("**/build/jacoco/*.exec")
+ }
 
 tasks.withType(FindBugs) {
+	// disable findbugs by default
+	// in order to run findbugs type 'gradle tlc4b findbugsMain findbugsTest'
+	task -> enabled = gradle.startParameter.taskNames.contains(task.name)
+	
     reports {
         xml.enabled = false
         html.enabled = true
     }
-}
-
-findbugs { 
-	ignoreFailures = true 
+	
+	ignoreFailures = true
 }
 
 
 test { 
 	exclude('testing')
+	allJvmArgs = [ "-Xss515m" ]
 }
 
 jar { from sourceSets.main.allJava }
@@ -79,7 +79,6 @@ jar	{
 jar {
 	manifest {
 		attributes "Main-Class" : 'de.tla2b.TLA2B'
-		attributes "Class-Path": './tla/ tlatools.jar'
 	}
 }
 
diff --git a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
index 0f8f0c2..54ccc54 100644
--- a/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
+++ b/src/main/java/de/tla2b/analysis/RecursiveFunktion.java
@@ -5,7 +5,6 @@
 package de.tla2b.analysis;
 
 import de.tla2b.exceptions.NotImplementedException;
-import tla2sany.semantic.ExprOrOpArgNode;
 import tla2sany.semantic.OpApplNode;
 import tla2sany.semantic.OpDefNode;
 import tlc2.tool.BuiltInOPs;
@@ -24,28 +23,28 @@ public class RecursiveFunktion extends BuiltInOPs {
 	}
 
 
-	/**
-	 * @throws NotImplementedException
-	 * 
-	 */
-	private void evalDef() throws NotImplementedException {
-		ExprOrOpArgNode e = rfs.getArgs()[0];
-		//System.out.println(rfs.toString(5));
-		if (e instanceof OpApplNode) {
-			OpApplNode o = (OpApplNode) e;
-			switch (getOpCode(o.getOperator().getName())) {
-			case OPCODE_ite: { // IF THEN ELSE
-				ifThenElse = o;
-				return;
-			}
-			}
-			throw new NotImplementedException(
-					"Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
-		} else {
-			throw new NotImplementedException(
-					"Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
-		}
-	}
+//	/**
+//	 * @throws NotImplementedException
+//	 * 
+//	 */
+//	private void evalDef() throws NotImplementedException {
+//		ExprOrOpArgNode e = rfs.getArgs()[0];
+//		//System.out.println(rfs.toString(5));
+//		if (e instanceof OpApplNode) {
+//			OpApplNode o = (OpApplNode) e;
+//			switch (getOpCode(o.getOperator().getName())) {
+//			case OPCODE_ite: { // IF THEN ELSE
+//				ifThenElse = o;
+//				return;
+//			}
+//			}
+//			throw new NotImplementedException(
+//					"Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
+//		} else {
+//			throw new NotImplementedException(
+//					"Only IF/THEN/ELSE or CASE constructs are supported at the body of a recursive function.");
+//		}
+//	}
 
 	public OpDefNode getOpDefNode() {
 		return def;
diff --git a/src/main/java/de/tla2b/output/PrologPrinter.java b/src/main/java/de/tla2b/output/PrologPrinter.java
index 46ba2b8..22007dc 100644
--- a/src/main/java/de/tla2b/output/PrologPrinter.java
+++ b/src/main/java/de/tla2b/output/PrologPrinter.java
@@ -10,9 +10,7 @@ import java.util.List;
 import java.util.Map;
 
 import de.be4.classicalb.core.parser.BParser;
-import de.be4.classicalb.core.parser.analysis.pragma.Pragma;
 import de.be4.classicalb.core.parser.analysis.prolog.ASTProlog;
-import de.be4.classicalb.core.parser.analysis.prolog.NodeIdAssignment;
 import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
 import de.be4.classicalb.core.parser.node.Node;
 import de.be4.classicalb.core.parser.node.Start;
@@ -84,14 +82,6 @@ public class PrologPrinter {
 			pout.fullstop();
 		}
 
-		if (bParser.getPragmas().size() > 0) {
-			NodeIdAssignment ids = pprinter.nodeIds;
-			List<Pragma> pragmas = bParser.getPragmas();
-			for (Pragma pragma : pragmas) {
-				pragma.printProlog(pout, ids);
-				pout.fullstop();
-			}
-		}
 		pout.flush();
 	}
 }
diff --git a/src/main/java/de/tla2bAst/SimpleResolver.java b/src/main/java/de/tla2bAst/SimpleResolver.java
index 8ffd983..c91f186 100644
--- a/src/main/java/de/tla2bAst/SimpleResolver.java
+++ b/src/main/java/de/tla2bAst/SimpleResolver.java
@@ -5,6 +5,8 @@ import java.io.File;
 import util.FilenameToStream;
 
 public class SimpleResolver implements FilenameToStream {
+	
+	private File file;
 
 	public boolean isStandardModule(String arg0) {
 		return false;
@@ -12,8 +14,12 @@ public class SimpleResolver implements FilenameToStream {
 
 	public File resolve(String arg0, boolean arg1) {
 
-		File file = new File(arg0);
+		file = new File(arg0);
 		return file;
 	}
 
+	public String getFullPath() {
+		return file.getAbsolutePath();
+	}
+
 }
\ No newline at end of file
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 76f539e..4433413 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -93,7 +93,14 @@ public class Translator implements TranslationGlobals {
 		}
 	}
 
-	// used to for external use
+	/**
+	 * External interface
+	 * @param moduleName
+	 * @param moduleString
+	 * @param configString
+	 * @return
+	 * @throws TLA2BException
+	 */
 	public static String translateModuleString(String moduleName,
 			String moduleString, String configString) throws TLA2BException {
 		Translator translator = new Translator(moduleName, moduleString,
@@ -371,8 +378,7 @@ public class Translator implements TranslationGlobals {
 			final File f, final BParser bparser) throws BException {
 		final RecursiveMachineLoader rml = new RecursiveMachineLoader(
 				f.getParent(), bparser.getContentProvider());
-		rml.loadAllMachines(f, ast, null, bparser.getDefinitions(),
-				bparser.getPragmas());
+		rml.loadAllMachines(f, ast, null, bparser.getDefinitions());
 		return rml;
 	}
 
diff --git a/src/test/java/de/tla2b/util/TestUtil.java b/src/test/java/de/tla2b/util/TestUtil.java
index 7e2af8f..2dfadfa 100644
--- a/src/test/java/de/tla2b/util/TestUtil.java
+++ b/src/test/java/de/tla2b/util/TestUtil.java
@@ -6,10 +6,6 @@ package de.tla2b.util;
 
 import static org.junit.Assert.assertEquals;
 
-import java.io.BufferedReader;
-import java.io.FileReader;
-import java.io.IOException;
-
 import util.FileUtil;
 import de.be4.classicalb.core.parser.BParser;
 import de.be4.classicalb.core.parser.exceptions.BException;
@@ -20,7 +16,6 @@ import de.tla2b.exceptions.TLA2BException;
 import de.tla2b.output.ASTPrettyPrinter;
 import de.tla2b.output.Renamer;
 import de.tla2bAst.Translator;
-import tla2sany.semantic.AbortException;
 import util.ToolIO;
 
 public class TestUtil {
-- 
GitLab