From b84c29f40a41e480fe327ffc7001fbe8bc1df811 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Mon, 24 Nov 2014 11:30:07 +0100
Subject: [PATCH] Fixed bug in the detection of the used modules procedure
---
src/main/java/de/tlc4b/TLC4B.java | 23 +++++++++-
src/main/java/de/tlc4b/Translator.java | 3 +-
.../analysis/NotSupportedConstructs.java | 1 -
.../tlc4b/analysis/UsedStandardModules.java | 15 +++++--
src/test/java/de/tlc4b/util/TestUtil.java | 6 ++-
src/test/java/testing/Testing2.java | 45 -------------------
6 files changed, 39 insertions(+), 54 deletions(-)
delete mode 100644 src/test/java/testing/Testing2.java
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index cc283c1..9b8a967 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/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());
}
}
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 7f8aa1c..2f16221 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/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();
@@ -126,7 +125,7 @@ public class Translator {
DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(
machineContext);
-
+
Generator generator = new Generator(machineContext, typeRestrictor,
constantsEvaluator, deferredSetSizeCalculator, typechecker);
generator.generate();
diff --git a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
index 56372a5..2683892 100644
--- a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
+++ b/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) {
diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index 19497f2..68b521d 100644
--- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+++ b/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)) {
- BType type = typechecker.getType(node.getIdentifier());
- if (type instanceof SetType) {
- usedStandardModules.add(STANDARD_MODULES.FunctionsAsRelations);
+ // 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);
+ }
}
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 936163d..6f4343b 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/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 {
@@ -177,7 +180,8 @@ public class TestUtil {
System.out.println("No result found.");
return null;
}
-
+
+
private static Process startJVM(final String optionsAsString,
final String mainClass, final String[] arguments)
throws IOException {
diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java
deleted file mode 100644
index 925ef7e..0000000
--- a/src/test/java/testing/Testing2.java
+++ /dev/null
@@ -1,45 +0,0 @@
-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);
- }
-
-}
--
GitLab