Fixed bug in the detection of the used modules procedure

src/main/java/de/tlc4b/TLC4B.java

@@ -164,7 +164,7 @@ public class TLC4B {
 				index = index + 1;
 				if (index == args.length) {
 					throw new TLC4BIOException(
-							"Error: Number requiered after option '-maxnint'.");
+							"Error: Number requiered after option '-maxint'.");
 				}
 				int maxint = Integer.parseInt(args[index]);
 				TLC4BGlobals.setMAX_INT(maxint);
@@ -424,7 +424,28 @@ public class TLC4B {
 				file.deleteOnExit();
 			}
 		}
+	}
+
+	public static void testParse(String[] args, boolean deleteFiles)
+			throws Exception {
+		TLC4BGlobals.resetGlobals();
+		TLC4BGlobals.setDeleteOnExit(deleteFiles);
+		TLC4BGlobals.setCreateTraceFile(false);
+		TLC4BGlobals.setTestingMode(true);
+		// B2TLAGlobals.setCleanup(true);
+		TLC4B tlc4b = new TLC4B();
+		try {
+			tlc4b.progress(args);
+		} catch (Exception e) {
+			e.printStackTrace();
+			System.err.println(e.getMessage());
+			throw e;
+		}
+		File module = new File(tlc4b.buildDir,
+				tlc4b.machineFileNameWithoutFileExtension + ".tla");
 
+		// parse result
+		new de.tla2bAst.Translator(module.getCanonicalPath());
 	}
 
 }

src/main/java/de/tlc4b/Translator.java

@@ -110,7 +110,6 @@ public class Translator {
 		UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(
 				machineContext);
 
-		
 		ConstantsEliminator constantsEliminator = new ConstantsEliminator(
 				machineContext);
 		constantsEliminator.start();

src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java

@@ -19,7 +19,6 @@ public class NotSupportedConstructs extends DepthFirstAdapter {
 
 	public NotSupportedConstructs(Start start) {
 		start.apply(this);
-		System.out.println(start.getPParseUnit().getClass());
 	}
 
 	public void inARefinesModelClause(ARefinesModelClause node) {

src/main/java/de/tlc4b/analysis/UsedStandardModules.java

@@ -388,12 +388,19 @@ public class UsedStandardModules extends DepthFirstAdapter {
 
 	// Function call
 	public void inAFunctionExpression(AFunctionExpression node) {
-		if (!(node.parent() instanceof AAssignSubstitution)) {
+		// System.out.println(node.parent().getClass());
+		if (node.parent() instanceof AAssignSubstitution) {
+			AAssignSubstitution parent = (AAssignSubstitution) node.parent();
+			if (parent.getLhsExpression().contains(node)) {
+				// function assignment (function call on the left side), e.g.
+				// f(x) := 1
+				return;
+			}
+		}
 		BType type = typechecker.getType(node.getIdentifier());
 		if (type instanceof SetType) {
 			usedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
 		}
-		}
 
 	}
 

src/test/java/de/tlc4b/util/TestUtil.java

@@ -19,8 +19,11 @@ import de.tla2b.exceptions.FrontEndException;
 import de.tla2b.exceptions.TLA2BException;
 import de.tla2b.output.ASTPrettyPrinter;
 import de.tla2b.output.Renamer;
+import de.tlc4b.TLC4B;
 import de.tlc4b.TLC4BGlobals;
+import de.tlc4b.TLCRunner;
 import de.tlc4b.Translator;
+import de.tlc4b.tlc.TLCResults;
 import de.tlc4b.tlc.TLCResults.TLCResult;
 
 public class TestUtil {
@@ -178,6 +181,7 @@ public class TestUtil {
 		return null;
 	}
 	
+	
 	private static Process startJVM(final String optionsAsString,
 			final String mainClass, final String[] arguments)
 			throws IOException {

src/test/java/testing/Testing2.java

-package testing;
-
-import static de.tlc4b.tlc.TLCResults.TLCResult.NoError;
-import static de.tlc4b.util.TestUtil.test;
-
-import java.io.File;
-import java.util.ArrayList;
-
-import org.junit.Test;
-import org.junit.runner.RunWith;
-
-import de.tlc4b.TLC4B;
-import de.tlc4b.tlc.TLCResults.TLCResult;
-import de.tlc4b.util.AbstractParseMachineTest;
-import de.tlc4b.util.PolySuite;
-import de.tlc4b.util.TestPair;
-import de.tlc4b.util.PolySuite.Config;
-import de.tlc4b.util.PolySuite.Configuration;
-
-@RunWith(PolySuite.class)
-public class Testing2 extends AbstractParseMachineTest {
-
-	private final File machine;
-
-	public Testing2(File machine, TLCResult result) {
-		this.machine = machine;
-	}
-
-	@Test
-	public void testRunTLC() throws Exception {
-		String[] a = new String[] { machine.getPath(), "-nodead", "-noinv" };
-		//String[] a = new String[] { "./src/test/resources/testing/Counter.mch" };
-		TLC4B.main(a);
-		//TLC4B.test(a, false);
-		// test(a);
-	}
-
-	@Config
-	public static Configuration getConfig() {
-		final ArrayList<TestPair> list = new ArrayList<TestPair>();
-		list.add(new TestPair(NoError, "./src/test/resources/testing"));
-		return getConfiguration(list);
-	}
-
-}