From 7b370cb3d52ee1af907d60647363852b1b87c5c6 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Mon, 15 Aug 2016 10:21:48 +0200
Subject: [PATCH] improved detection of unsupported constructs
---
src/main/java/de/tlc4b/Translator.java | 90 ++++++++---------
.../analysis/NotSupportedConstructs.java | 90 -----------------
.../analysis/UnsupportedConstructsFinder.java | 96 +++++++++++++++++++
.../analysis/UnsupportedConstructsTest.java | 22 +++++
src/test/java/de/tlc4b/util/TestUtil.java | 68 ++++++-------
5 files changed, 186 insertions(+), 180 deletions(-)
delete mode 100644 src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
create mode 100644 src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
create mode 100644 src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java
diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index 1a344ff..48626c9 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -15,7 +15,7 @@ import de.tlc4b.analysis.ConstantsEliminator;
import de.tlc4b.analysis.ConstantsEvaluator;
import de.tlc4b.analysis.DefinitionsAnalyser;
import de.tlc4b.analysis.MachineContext;
-import de.tlc4b.analysis.NotSupportedConstructs;
+import de.tlc4b.analysis.UnsupportedConstructsFinder;
import de.tlc4b.analysis.PrecedenceCollector;
import de.tlc4b.analysis.PrimedNodesMarker;
import de.tlc4b.analysis.Renamer;
@@ -57,8 +57,7 @@ public class Translator {
// System.out.println(ast2String2.toString());
}
- public Translator(String machineString, String ltlFormula)
- throws BException {
+ public Translator(String machineString, String ltlFormula) throws BException {
this.machineString = machineString;
this.ltlFormula = ltlFormula;
BParser parser = new BParser("Testing");
@@ -68,8 +67,8 @@ public class Translator {
// System.out.println(ast2String2.toString());
}
- public Translator(String machineName, File machineFile, String ltlFormula,
- String constantSetup) throws BException, IOException {
+ public Translator(String machineName, File machineFile, String ltlFormula, String constantSetup)
+ throws BException, IOException {
this.machineName = machineName;
this.ltlFormula = ltlFormula;
@@ -82,10 +81,10 @@ public class Translator {
// Definitions of definitions files are injected in the ast of the main
// machine
- final RecursiveMachineLoader rml = new RecursiveMachineLoader(
- machineFile.getParent(), parser.getContentProvider());
+ final RecursiveMachineLoader rml = new RecursiveMachineLoader(machineFile.getParent(),
+ parser.getContentProvider());
rml.loadAllMachines(machineFile, start, parser.getSourcePositions(), parser.getDefinitions());
-
+
parsedMachines = rml.getParsedMachines();
if (constantSetup != null) {
@@ -94,13 +93,11 @@ public class Translator {
try {
start2 = con.parse("#FORMULA " + constantSetup, false);
} catch (BException e) {
- System.err
- .println("An error occured while parsing the constants setup predicate.");
+ System.err.println("An error occured while parsing the constants setup predicate.");
throw e;
}
- APredicateParseUnit parseUnit = (APredicateParseUnit) start2
- .getPParseUnit();
+ APredicateParseUnit parseUnit = (APredicateParseUnit) start2.getPParseUnit();
this.constantsSetup = parseUnit.getPredicate();
final Ast2String ast2String2 = new Ast2String();
@@ -114,75 +111,66 @@ public class Translator {
}
public void translate() {
+
+ UnsupportedConstructsFinder unsupportedConstructsFinder = new UnsupportedConstructsFinder(start);
+ unsupportedConstructsFinder.find();
+
// ast transformation
SeesEliminator.eliminateSeesClauses(start, parsedMachines);
- new NotSupportedConstructs(start);
DefinitionsEliminator.eliminateDefinitions(start);
- //TODO move set comprehension optimizer behind the type checker
+ // TODO move set comprehension optimizer behind the type checker
SetComprehensionOptimizer.optimizeSetComprehensions(start);
-
- MachineContext machineContext = new MachineContext(machineName, start,
- ltlFormula, constantsSetup);
+
+ MachineContext machineContext = new MachineContext(machineName, start, ltlFormula, constantsSetup);
this.machineName = machineContext.getMachineName();
if (machineContext.machineContainsOperations()) {
TLC4BGlobals.setPrintCoverage(true);
}
Typechecker typechecker = new Typechecker(machineContext);
- UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(
- machineContext);
-
- ConstantsEliminator constantsEliminator = new ConstantsEliminator(
- machineContext);
+ UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(machineContext);
+
+ ConstantsEliminator constantsEliminator = new ConstantsEliminator(machineContext);
constantsEliminator.start();
- ConstantsEvaluator constantsEvaluator = new ConstantsEvaluator(
- machineContext);
+ ConstantsEvaluator constantsEvaluator = new ConstantsEvaluator(machineContext);
- InvariantPreservationAnalysis invariantPreservationAnalysis = new InvariantPreservationAnalysis(
- machineContext, constantsEvaluator.getInvariantList(),
- unchangedVariablesFinder);
+ InvariantPreservationAnalysis invariantPreservationAnalysis = new InvariantPreservationAnalysis(machineContext,
+ constantsEvaluator.getInvariantList(), unchangedVariablesFinder);
- TypeRestrictor typeRestrictor = new TypeRestrictor(start,
- machineContext, typechecker, constantsEvaluator);
-
- PrecedenceCollector precedenceCollector = new PrecedenceCollector(
- start, typechecker, machineContext, typeRestrictor);
+ TypeRestrictor typeRestrictor = new TypeRestrictor(start, machineContext, typechecker, constantsEvaluator);
- DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(
- machineContext);
-
-
+ PrecedenceCollector precedenceCollector = new PrecedenceCollector(start, typechecker, machineContext,
+ typeRestrictor);
- Generator generator = new Generator(machineContext, typeRestrictor,
- constantsEvaluator, deferredSetSizeCalculator, typechecker);
+ DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(machineContext);
+
+ Generator generator = new Generator(machineContext, typeRestrictor, constantsEvaluator,
+ deferredSetSizeCalculator, typechecker);
generator.generate();
- UsedStandardModules usedModules = new UsedStandardModules(start,
- typechecker, typeRestrictor, generator.getTlaModule());
+ UsedStandardModules usedModules = new UsedStandardModules(start, typechecker, typeRestrictor,
+ generator.getTlaModule());
- standardModulesToBeCreated = usedModules
- .getStandardModulesToBeCreated();
+ standardModulesToBeCreated = usedModules.getStandardModulesToBeCreated();
- PrimedNodesMarker primedNodesMarker = new PrimedNodesMarker(generator
- .getTlaModule().getOperations(), machineContext);
+ PrimedNodesMarker primedNodesMarker = new PrimedNodesMarker(generator.getTlaModule().getOperations(),
+ machineContext);
primedNodesMarker.start();
Renamer renamer = new Renamer(machineContext);
- TLAPrinter printer = new TLAPrinter(machineContext, typechecker,
- unchangedVariablesFinder, precedenceCollector, usedModules,
- typeRestrictor, generator.getTlaModule(),
- generator.getConfigFile(), primedNodesMarker, renamer,
- invariantPreservationAnalysis);
+ TLAPrinter printer = new TLAPrinter(machineContext, typechecker, unchangedVariablesFinder, precedenceCollector,
+ usedModules, typeRestrictor, generator.getTlaModule(), generator.getConfigFile(), primedNodesMarker,
+ renamer, invariantPreservationAnalysis);
printer.start();
moduleString = printer.getStringbuilder().toString();
configString = printer.getConfigString().toString();
translatedLTLFormula = printer.geTranslatedLTLFormula();
- tlcOutputInfo = new TLCOutputInfo(machineContext, renamer, typechecker,
- generator.getTlaModule(), generator.getConfigFile());
+ tlcOutputInfo = new TLCOutputInfo(machineContext, renamer, typechecker, generator.getTlaModule(),
+ generator.getConfigFile());
}
public String getMachineString() {
diff --git a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
deleted file mode 100644
index 90fc65e..0000000
--- a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java
+++ /dev/null
@@ -1,90 +0,0 @@
-package de.tlc4b.analysis;
-
-import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
-import de.be4.classicalb.core.parser.node.ACaseSubstitution;
-import de.be4.classicalb.core.parser.node.AExtendsMachineClause;
-import de.be4.classicalb.core.parser.node.AImportsMachineClause;
-import de.be4.classicalb.core.parser.node.AIncludesMachineClause;
-import de.be4.classicalb.core.parser.node.APromotesMachineClause;
-import de.be4.classicalb.core.parser.node.ARefinesModelClause;
-import de.be4.classicalb.core.parser.node.ASeesMachineClause;
-import de.be4.classicalb.core.parser.node.ASeesModelClause;
-import de.be4.classicalb.core.parser.node.ASequenceSubstitution;
-import de.be4.classicalb.core.parser.node.AUsesMachineClause;
-import de.be4.classicalb.core.parser.node.AVarSubstitution;
-import de.be4.classicalb.core.parser.node.AWhileSubstitution;
-import de.be4.classicalb.core.parser.node.Start;
-import de.tlc4b.exceptions.NotSupportedException;
-
-public class NotSupportedConstructs extends DepthFirstAdapter {
-
- public NotSupportedConstructs(Start start) {
- start.apply(this);
- }
-
- public void inARefinesModelClause(ARefinesModelClause node) {
- throw new NotSupportedException(
- "Refines clause is currently not supported.");
- }
-
- public void inASeesMachineClause(ASeesMachineClause node) {
- throw new NotSupportedException(
- "SEES clause is currently not supported.");
- }
-
- public void inAUsesMachineClause(AUsesMachineClause node) {
- throw new NotSupportedException(
- "USES clause is currently not supported.");
- }
-
- public void inAPromotesMachineClause(APromotesMachineClause node) {
- throw new NotSupportedException(
- "Promotes clause is currently not supported.");
- }
-
- public void inASeesModelClause(ASeesModelClause node) {
- throw new NotSupportedException(
- "Sees clause is currently not supported.");
- }
-
- public void inAIncludesMachineClause(AIncludesMachineClause node) {
- throw new NotSupportedException(
- "INCLUDES clause is currently not supported.");
- }
-
- public void inAExtendsMachineClause(AExtendsMachineClause node) {
- throw new NotSupportedException(
- "EXTENDS clause is currently not supported.");
- }
-
- public void inAImportsMachineClause(AImportsMachineClause node) {
- throw new NotSupportedException(
- "IMPORTS clause is currently not supported.");
- }
-
- /**
- * Substitutions
- */
-
- public void inAWhileSubstitution(AWhileSubstitution node) {
- throw new NotSupportedException(
- "While substitutions are currently not supported.");
- }
-
- public void inASequenceSubstitution(ASequenceSubstitution node) {
- throw new NotSupportedException(
- "Sequence substitutions ';' are currently not supported.");
- }
-
- public void inAVarSubstitution(AVarSubstitution node) {
- throw new NotSupportedException(
- "VAR substitutions are currently not supported.");
- }
-
- public void inACaseSubstitution(ACaseSubstitution node) {
- // TODO it is possible to support this substitution
- throw new NotSupportedException(
- "Case substitutions are currently not supported.");
- }
-
-}
diff --git a/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
new file mode 100644
index 0000000..ca12eb3
--- /dev/null
+++ b/src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java
@@ -0,0 +1,96 @@
+package de.tlc4b.analysis;
+
+import java.io.StringWriter;
+import java.util.Arrays;
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Set;
+
+import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
+import de.be4.classicalb.core.parser.node.ACaseSubstitution;
+import de.be4.classicalb.core.parser.node.AExtendsMachineClause;
+import de.be4.classicalb.core.parser.node.AImplementationMachineParseUnit;
+import de.be4.classicalb.core.parser.node.AImportsMachineClause;
+import de.be4.classicalb.core.parser.node.AIncludesMachineClause;
+import de.be4.classicalb.core.parser.node.APromotesMachineClause;
+import de.be4.classicalb.core.parser.node.ARefinesModelClause;
+import de.be4.classicalb.core.parser.node.ASequenceSubstitution;
+import de.be4.classicalb.core.parser.node.AVarSubstitution;
+import de.be4.classicalb.core.parser.node.AWhileSubstitution;
+import de.be4.classicalb.core.parser.node.Node;
+import de.be4.classicalb.core.parser.node.Start;
+import de.tlc4b.exceptions.NotSupportedException;
+
+public class UnsupportedConstructsFinder extends DepthFirstAdapter {
+ private final Start start;
+ private static final Set<Class<? extends Node>> unsupportedClasses = new HashSet<>();
+
+ static {
+ add(ARefinesModelClause.class);
+ add(AExtendsMachineClause.class);
+ add(APromotesMachineClause.class);
+ add(AIncludesMachineClause.class);
+ add(AImportsMachineClause.class);
+
+ add(AWhileSubstitution.class);
+ add(ASequenceSubstitution.class);
+ add(AVarSubstitution.class);
+ add(ACaseSubstitution.class);
+
+ add(AImplementationMachineParseUnit.class);
+ }
+
+ private static void add(Class<? extends Node> clazz) {
+ unsupportedClasses.add(clazz);
+ }
+
+ public UnsupportedConstructsFinder(Start start) {
+ this.start = start;
+ }
+
+ public void find() {
+ start.apply(this);
+ }
+
+ private static final List<String> SUM_TYPE = new LinkedList<String>(
+ Arrays.asList("model_clause", "machine_clause", "substitution", "machine_parse_unit"));
+
+ private String formatCamel(final String input) {
+ StringWriter out = new StringWriter();
+ char[] chars = input.toCharArray();
+ for (int i = 0; i < chars.length; i++) {
+ char current = chars[i];
+ if (Character.isUpperCase(current)) {
+ out.append('_');
+ out.append(Character.toLowerCase(current));
+ } else {
+ out.append(current);
+ }
+ }
+ return out.toString();
+ }
+
+ public void defaultIn(Node node) {
+ if (unsupportedClasses.contains(node.getClass())) {
+ final String formatedName = formatCamel(node.getClass().getSimpleName());
+ final String className = node.getClass().getSimpleName();
+ for (final String suffix : SUM_TYPE) {
+ if (formatedName.endsWith(suffix)) {
+ final String shortName = formatedName.substring(3, formatedName.length() - suffix.length() - 1)
+ .toUpperCase();
+ final String[] split = suffix.split("_");
+ final String type = split[split.length - 1];
+ if (type.equals("clause") || type.equals("substitution")) {
+ throw new NotSupportedException(shortName + " " + type + " is not supported.");
+ } else {
+ throw new NotSupportedException(shortName + " is not supported.");
+ }
+
+ }
+ }
+ throw new NotSupportedException(className + " is not supported.");
+ }
+ }
+
+}
diff --git a/src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java b/src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java
new file mode 100644
index 0000000..030e639
--- /dev/null
+++ b/src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java
@@ -0,0 +1,22 @@
+package de.tlc4b.analysis;
+
+import static de.tlc4b.util.TestUtil.*;
+
+import org.junit.Test;
+
+import de.tlc4b.exceptions.NotSupportedException;
+
+public class UnsupportedConstructsTest {
+
+ @Test(expected = NotSupportedException.class)
+ public void testExtends() throws Exception {
+ final String machine = "MACHINE test\n" + "EXTENDS foo\n PROMOTES bar\n" + "END";
+ tryTranslating(machine);
+ }
+
+ @Test(expected = NotSupportedException.class)
+ public void testImplementation() throws Exception {
+ final String machine = "IMPLEMENTATION test REFINES foo END";
+ tryTranslating(machine);
+ }
+}
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 5c868dc..bcfc579 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -23,8 +23,7 @@ import de.tlc4b.tlc.TLCResults.TLCResult;
public class TestUtil {
- public static void compare(String expectedModule, String machineString)
- throws Exception {
+ public static void compare(final String expectedModule, final String machineString) throws Exception {
TLC4BGlobals.setForceTLCToEvalConstants(false);
ToolIO.setMode(ToolIO.TOOL);
@@ -35,11 +34,9 @@ public class TestUtil {
// TODO create standard modules BBuildins
String moduleName = b2tlaTranslator.getMachineName();
- String str1 = de.tla2bAst.Translator.translateModuleString(moduleName,
- b2tlaTranslator.getModuleString(), null);
+ String str1 = de.tla2bAst.Translator.translateModuleString(moduleName, b2tlaTranslator.getModuleString(), null);
- String str2 = de.tla2bAst.Translator.translateModuleString(moduleName,
- expectedModule, null);
+ String str2 = de.tla2bAst.Translator.translateModuleString(moduleName, expectedModule, null);
// StringBuilder sb1 = de.tla2b.translation.Tla2BTranslator
// .translateString(name, b2tlaTranslator.getModuleString(), null);
// StringBuilder sb2 = de.tla2b.translation.Tla2BTranslator
@@ -47,26 +44,28 @@ public class TestUtil {
if (!str1.equals(str2)) {
// assertEquals(expected, actual);
- fail("expected:\n" + expectedModule + "\nbut was:\n"
- + b2tlaTranslator.getModuleString());
+ fail("expected:\n" + expectedModule + "\nbut was:\n" + b2tlaTranslator.getModuleString());
}
// assertEquals(sb2.toString(), sb1.toString());
}
- public static String translateTLA2B(String moduleName, String tlaString)
- throws TLA2BException {
- return de.tla2bAst.Translator.translateModuleString(moduleName,
- tlaString, null);
+ public static void tryTranslating(final String machineString) throws BException {
+ TLC4BGlobals.setForceTLCToEvalConstants(false);
+ ToolIO.setMode(ToolIO.TOOL);
+ Translator b2tlaTranslator = new Translator(machineString);
+ b2tlaTranslator.translate();
+ }
+
+ public static String translateTLA2B(String moduleName, String tlaString) throws TLA2BException {
+ return de.tla2bAst.Translator.translateModuleString(moduleName, tlaString, null);
}
- public static String translateTLA2B(String moduleName, String tlaString,
- String configString) throws TLA2BException {
- return de.tla2bAst.Translator.translateModuleString(moduleName,
- tlaString, configString);
+ public static String translateTLA2B(String moduleName, String tlaString, String configString)
+ throws TLA2BException {
+ return de.tla2bAst.Translator.translateModuleString(moduleName, tlaString, configString);
}
- public static void compareLTLFormula(String expected, String machine,
- String ltlFormula) throws Exception {
+ public static void compareLTLFormula(String expected, String machine, String ltlFormula) throws Exception {
Translator b2tlaTranslator = new Translator(machine, ltlFormula);
b2tlaTranslator.translate();
String translatedLTLFormula = b2tlaTranslator.getTranslatedLTLFormula();
@@ -94,8 +93,8 @@ public class TestUtil {
System.out.println(ast2String2.toString());
}
- public static void compareEqualsConfig(String expectedModule,
- String expectedConfig, String machine) throws Exception {
+ public static void compareEqualsConfig(String expectedModule, String expectedConfig, String machine)
+ throws Exception {
Translator b2tlaTranslator = new Translator(machine);
b2tlaTranslator.translate();
// print(b2tlaTranslator.getStart());
@@ -105,15 +104,14 @@ public class TestUtil {
String name = b2tlaTranslator.getMachineName();
// parse check
- translateTLA2B(name, b2tlaTranslator.getModuleString(),
- b2tlaTranslator.getConfigString());
+ translateTLA2B(name, b2tlaTranslator.getModuleString(), b2tlaTranslator.getConfigString());
assertEquals(expectedModule, b2tlaTranslator.getModuleString());
assertEquals(expectedConfig, b2tlaTranslator.getConfigString());
}
- public static void compareModuleAndConfig(String expectedModule,
- String expectedConfig, String machine) throws Exception {
+ public static void compareModuleAndConfig(String expectedModule, String expectedConfig, String machine)
+ throws Exception {
Translator b2tlaTranslator = new Translator(machine);
b2tlaTranslator.translate();
// print(b2tlaTranslator.getStart());
@@ -136,8 +134,7 @@ public class TestUtil {
// }
}
- public static void compareEquals(String expected, String machine)
- throws BException {
+ public static void compareEquals(String expected, String machine) throws BException {
Translator b2tlaTranslator = new Translator(machine);
b2tlaTranslator.translate();
System.out.println(b2tlaTranslator.getModuleString());
@@ -157,14 +154,13 @@ public class TestUtil {
return runTLC(runnerClassName, args);
}
-
+
public static TLCResult test(String[] args) throws IOException {
String runnerClassName = TLC4BTester.class.getCanonicalName();
return runTLC(runnerClassName, args);
}
- private static TLCResult runTLC(String runnerClassName, String[] args)
- throws IOException {
+ private static TLCResult runTLC(String runnerClassName, String[] args) throws IOException {
System.out.println("Starting JVM...");
final Process p = startJVM("", runnerClassName, args);
StreamGobbler stdOut = new StreamGobbler(p.getInputStream());
@@ -192,16 +188,12 @@ public class TestUtil {
}
-
-
- private static Process startJVM(final String optionsAsString,
- final String mainClass, final String[] arguments)
+ private static Process startJVM(final String optionsAsString, final String mainClass, final String[] arguments)
throws IOException {
String separator = System.getProperty("file.separator");
- String jvm = System.getProperty("java.home") + separator + "bin"
- + separator + "java";
+ String jvm = System.getProperty("java.home") + separator + "bin" + separator + "java";
String classpath = System.getProperty("java.class.path");
List<String> command = new ArrayList<String>();
@@ -216,8 +208,7 @@ public class TestUtil {
return process;
}
- public static void testParse(String[] args, boolean deleteFiles)
- throws Exception {
+ public static void testParse(String[] args, boolean deleteFiles) throws Exception {
TLC4BGlobals.resetGlobals();
TLC4BGlobals.setDeleteOnExit(deleteFiles);
TLC4BGlobals.setCreateTraceFile(false);
@@ -231,8 +222,7 @@ public class TestUtil {
System.err.println(e.getMessage());
throw e;
}
- File module = new File(tlc4b.getBuildDir(),
- tlc4b.getMachineFileNameWithoutFileExtension() + ".tla");
+ File module = new File(tlc4b.getBuildDir(), tlc4b.getMachineFileNameWithoutFileExtension() + ".tla");
// parse result
new de.tla2bAst.Translator(module.getCanonicalPath());
--
GitLab