Skip to content
Snippets Groups Projects
Commit 7b370cb3 authored by hansen's avatar hansen
Browse files

improved detection of unsupported constructs

parent 8b7822e8
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
src/main/java/de/tlc4b/Translator.java
+ 39
− 51
View file @ 7b370cb3
......@@ -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,8 +81,8 @@ 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();
......@@ -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
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);
UnchangedVariablesFinder unchangedVariablesFinder = new UnchangedVariablesFinder(machineContext);
ConstantsEliminator constantsEliminator = new ConstantsEliminator(
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);
TypeRestrictor typeRestrictor = new TypeRestrictor(start, machineContext, typechecker, constantsEvaluator);
PrecedenceCollector precedenceCollector = new PrecedenceCollector(
start, typechecker, machineContext, typeRestrictor);
DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(
machineContext);
PrecedenceCollector precedenceCollector = new PrecedenceCollector(start, typechecker, machineContext,
typeRestrictor);
DefinitionsAnalyser deferredSetSizeCalculator = new DefinitionsAnalyser(machineContext);
Generator generator = new Generator(machineContext, typeRestrictor,
constantsEvaluator, deferredSetSizeCalculator, typechecker);
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() {
......
src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java deleted 100644 → 0
+ 0
− 90
View file @ 8b7822e8
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.");
}
}
src/main/java/de/tlc4b/analysis/UnsupportedConstructsFinder.java 0 → 100644
+ 96
− 0
View file @ 7b370cb3
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.");
}
}
}
src/test/java/de/tlc4b/analysis/UnsupportedConstructsTest.java 0 → 100644
+ 22
− 0
View file @ 7b370cb3
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);
}
}
src/test/java/de/tlc4b/util/TestUtil.java
+ 29
− 39
View file @ 7b370cb3
......@@ -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,
String configString) throws TLA2BException {
return de.tla2bAst.Translator.translateModuleString(moduleName,
tlaString, configString);
public static String translateTLA2B(String moduleName, String tlaString) throws TLA2BException {
return de.tla2bAst.Translator.translateModuleString(moduleName, tlaString, null);
}
public static void compareLTLFormula(String expected, String machine,
String ltlFormula) throws Exception {
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 {
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());
......@@ -163,8 +160,7 @@ public class TestUtil {
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());
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment