Skip to content
Snippets Groups Projects
Commit 15ecfd4c authored by hansen's avatar hansen
Browse files

adapt to new parser version

parent 9ba46146
Branches
No related tags found
No related merge requests found
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 272 additions and 514 deletions
build.gradle
+ 3
− 4
View file @ 15ecfd4c
......@@ -28,7 +28,7 @@ configurations.all {
resolutionStrategy.cacheChangingModulesFor 0, 'seconds'
}
def parser_version = '2.5.1'
def parser_version = '2.7.1-SNAPSHOT'
def tlatools_version = '1.0.2'
dependencies {
......@@ -40,7 +40,6 @@ dependencies {
compile (group: 'de.hhu.stups', name: 'bparser', version: parser_version)
compile (group: 'de.hhu.stups', name: 'ltlparser', version: parser_version)
testCompile (group: 'junit', name: 'junit', version: '4.12')
}
......
src/main/java/de/tla2b/output/Renamer.java
+ 1
− 1
View file @ 15ecfd4c
......@@ -4,7 +4,7 @@ import java.util.HashSet;
import java.util.Hashtable;
import java.util.Set;
import de.be4.classicalb.core.parser.Utils;
import de.be4.classicalb.core.parser.util.Utils;
import de.be4.classicalb.core.parser.analysis.DepthFirstAdapter;
import de.be4.classicalb.core.parser.node.AIdentifierExpression;
import de.be4.classicalb.core.parser.node.Node;
......
src/main/java/de/tla2bAst/BAstCreator.java
+ 196
− 358
View file @ 15ecfd4c
This diff is collapsed.
src/main/java/de/tla2bAst/Translator.java
+ 46
− 84
View file @ 15ecfd4c
......@@ -16,7 +16,7 @@ import java.util.Hashtable;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.Definitions;
import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.exceptions.BCompoundException;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
import de.tla2b.analysis.InstanceTransformation;
......@@ -72,8 +72,7 @@ public class Translator implements TranslationGlobals {
}
private void findConfigFile() {
String configFileName = FileUtils.removeExtention(moduleFile
.getAbsolutePath());
String configFileName = FileUtils.removeExtention(moduleFile.getAbsolutePath());
configFileName = configFileName + ".cfg";
configFile = new File(configFileName);
if (!configFile.exists()) {
......@@ -84,14 +83,12 @@ public class Translator implements TranslationGlobals {
private void findModuleFile() {
moduleFile = new File(moduleFileName);
if (!moduleFile.exists()) {
throw new RuntimeException("Can not find module file: '"
+ moduleFileName + "'");
throw new RuntimeException("Can not find module file: '" + moduleFileName + "'");
}
try {
moduleFile = moduleFile.getCanonicalFile();
} catch (IOException e) {
throw new RuntimeException("Can not access module file: '"
+ moduleFileName + "'");
throw new RuntimeException("Can not access module file: '" + moduleFileName + "'");
}
}
......@@ -104,10 +101,9 @@ public class Translator implements TranslationGlobals {
* @return
* @throws TLA2BException
*/
public static String translateModuleString(String moduleName,
String moduleString, String configString) throws TLA2BException {
Translator translator = new Translator(moduleName, moduleString,
configString);
public static String translateModuleString(String moduleName, String moduleString, String configString)
throws TLA2BException {
Translator translator = new Translator(moduleName, moduleString, configString);
Start bAST = translator.getBAST();
Renamer renamer = new Renamer(bAST);
ASTPrettyPrinter aP = new ASTPrettyPrinter(bAST, renamer);
......@@ -115,8 +111,7 @@ public class Translator implements TranslationGlobals {
return aP.getResultString();
}
public Translator(String moduleName, String moduleString,
String configString) throws TLA2BException {
public Translator(String moduleName, String moduleString, String configString) throws TLA2BException {
createTLATempFile(moduleString, moduleName);
createCfgFile(configString, moduleName);
parse();
......@@ -124,8 +119,7 @@ public class Translator implements TranslationGlobals {
}
// Used for Testing in tla2bAST project
public Translator(String moduleString, String configString)
throws FrontEndException {
public Translator(String moduleString, String configString) throws FrontEndException {
String moduleName = "Testing";
createTLATempFile(moduleString, moduleName);
createCfgFile(configString, moduleName);
......@@ -138,8 +132,8 @@ public class Translator implements TranslationGlobals {
configFile = new File("temp/" + moduleName + ".cfg");
try {
configFile.createNewFile();
BufferedWriter out = new BufferedWriter(new OutputStreamWriter(
new FileOutputStream(configFile), "UTF-8"));
BufferedWriter out = new BufferedWriter(
new OutputStreamWriter(new FileOutputStream(configFile), "UTF-8"));
try {
out.write(configString);
} finally {
......@@ -159,8 +153,7 @@ public class Translator implements TranslationGlobals {
try {
moduleFile = new File("temp/" + moduleName + ".tla");
moduleFile.createNewFile();
BufferedWriter out = new BufferedWriter(new OutputStreamWriter(
new FileOutputStream(moduleFile), "UTF-8"));
BufferedWriter out = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(moduleFile), "UTF-8"));
try {
out.write(moduleString);
} finally {
......@@ -172,8 +165,7 @@ public class Translator implements TranslationGlobals {
}
}
public ModuleNode parseModule()
throws de.tla2b.exceptions.FrontEndException {
public ModuleNode parseModule() throws de.tla2b.exceptions.FrontEndException {
String fileName = moduleFile.getName();
ToolIO.setUserDir(moduleFile.getParent());
......@@ -187,8 +179,7 @@ public class Translator implements TranslationGlobals {
if (spec.parseErrors.isFailure()) {
throw new de.tla2b.exceptions.FrontEndException(
allMessagesToString(ToolIO.getAllMessages())
+ spec.parseErrors, spec);
allMessagesToString(ToolIO.getAllMessages()) + spec.parseErrors, spec);
}
if (spec.semanticErrors.isFailure()) {
......@@ -206,8 +197,7 @@ public class Translator implements TranslationGlobals {
if (n == null) { // Parse Error
// System.out.println("Rootmodule null");
throw new de.tla2b.exceptions.FrontEndException(
allMessagesToString(ToolIO.getAllMessages()), spec);
throw new de.tla2b.exceptions.FrontEndException(allMessagesToString(ToolIO.getAllMessages()), spec);
}
return n;
......@@ -226,8 +216,7 @@ public class Translator implements TranslationGlobals {
modelConfig = null;
if (configFile != null) {
modelConfig = new ModelConfig(configFile.getAbsolutePath(),
new SimpleResolver());
modelConfig = new ModelConfig(configFile.getAbsolutePath(), new SimpleResolver());
modelConfig.parse();
}
......@@ -239,8 +228,7 @@ public class Translator implements TranslationGlobals {
SymbolSorter symbolSorter = new SymbolSorter(moduleNode);
symbolSorter.sort();
PredicateVsExpression predicateVsExpression = new PredicateVsExpression(
moduleNode);
PredicateVsExpression predicateVsExpression = new PredicateVsExpression(moduleNode);
ConfigfileEvaluator conEval = null;
if (modelConfig != null) {
......@@ -259,14 +247,11 @@ public class Translator implements TranslationGlobals {
typechecker.start();
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
UsedExternalFunctions usedExternalFunctions = new UsedExternalFunctions(
moduleNode, specAnalyser);
RecursiveFunctionHandler recursiveFunctionHandler = new RecursiveFunctionHandler(
specAnalyser);
UsedExternalFunctions usedExternalFunctions = new UsedExternalFunctions(moduleNode, specAnalyser);
RecursiveFunctionHandler recursiveFunctionHandler = new RecursiveFunctionHandler(specAnalyser);
BMacroHandler bMacroHandler = new BMacroHandler(specAnalyser, conEval);
bAstCreator = new BAstCreator(moduleNode, conEval, specAnalyser,
usedExternalFunctions, predicateVsExpression, bMacroHandler,
recursiveFunctionHandler);
bAstCreator = new BAstCreator(moduleNode, conEval, specAnalyser, usedExternalFunctions, predicateVsExpression,
bMacroHandler, recursiveFunctionHandler);
this.BAst = bAstCreator.getStartNode();
this.typeTable = bAstCreator.getTypeTable();
......@@ -275,30 +260,25 @@ public class Translator implements TranslationGlobals {
}
public void createProbFile() {
String fileName = FileUtils.removeExtention(moduleFile
.getAbsolutePath());
String fileName = FileUtils.removeExtention(moduleFile.getAbsolutePath());
fileName = fileName + ".prob";
File probFile;
probFile = new File(fileName);
try {
probFile.createNewFile();
} catch (IOException e) {
System.err.println(String.format("Could not create File %s.",
probFile.getName()));
System.err.println(String.format("Could not create File %s.", probFile.getName()));
System.exit(-1);
}
BParser bParser = new BParser();
bParser.getDefinitions().addAll(getBDefinitions());
try {
final RecursiveMachineLoader rml = parseAllMachines(getBAST(),
getModuleFile(), bParser);
// rml.printAsProlog(new PrintWriter(System.out), false);
// rml.printAsProlog(new PrintWriter(probFile), false);
bParser.getDefinitions().addDefinitions(getBDefinitions());
final RecursiveMachineLoader rml = parseAllMachines(getBAST(), getModuleFile(), bParser);
String moduleName = FileUtils.removeExtention(moduleFile.getName());
PrologPrinter prologPrinter = new PrologPrinter(rml, bParser,
moduleFile, moduleName, typeTable);
PrologPrinter prologPrinter = new PrologPrinter(rml, bParser, moduleFile, moduleName, typeTable);
prologPrinter.setPositions(bAstCreator.getSourcePositions());
PrintWriter outWriter = new PrintWriter(probFile, "UTF-8");
......@@ -306,14 +286,9 @@ public class Translator implements TranslationGlobals {
outWriter.close();
System.out.println(probFile.getAbsolutePath() + " created.");
// prologPrinter.printAsProlog(new PrintWriter(System.out), false);
} catch (BException e) {
e.printStackTrace();
} catch (FileNotFoundException e) {
e.printStackTrace();
} catch (UnsupportedEncodingException e) {
e.printStackTrace();
} catch (BCompoundException | FileNotFoundException | UnsupportedEncodingException e) {
System.err.println(e.getMessage());
System.exit(-1);
}
}
......@@ -329,12 +304,9 @@ public class Translator implements TranslationGlobals {
in = new BufferedReader(new FileReader(machineFile));
String firstLine = in.readLine();
in.close();
if (firstLine != null
&& !firstLine.startsWith("/*@ generated by TLA2B ")) {
System.err.println("Error: File " + machineFile.getName()
+ " already exists"
+ " and was not generated by TLA2B.\n"
+ "Delete or move this file.");
if (firstLine != null && !firstLine.startsWith("/*@ generated by TLA2B ")) {
System.err.println("Error: File " + machineFile.getName() + " already exists"
+ " and was not generated by TLA2B.\n" + "Delete or move this file.");
System.exit(-1);
}
} catch (IOException e) {
......@@ -346,8 +318,7 @@ public class Translator implements TranslationGlobals {
try {
machineFile.createNewFile();
} catch (IOException e) {
System.err.println(String.format("Could not create File %s.",
machineFile.getName()));
System.err.println(String.format("Could not create File %s.", machineFile.getName()));
System.exit(-1);
}
......@@ -355,48 +326,39 @@ public class Translator implements TranslationGlobals {
ASTPrettyPrinter aP = new ASTPrettyPrinter(BAst, renamer);
BAst.apply(aP);
StringBuilder result = aP.getResultAsStringbuilder();
result.insert(0, "/*@ generated by TLA2B " + VERSION_NUMBER + " " + new Date()
+ " */\n");
result.insert(0, "/*@ generated by TLA2B " + VERSION_NUMBER + " " + new Date() + " */\n");
try {
BufferedWriter out = new BufferedWriter(new OutputStreamWriter(
new FileOutputStream(machineFile), "UTF-8"));
BufferedWriter out = new BufferedWriter(new OutputStreamWriter(new FileOutputStream(machineFile), "UTF-8"));
try {
out.write(result.toString());
} finally {
out.close();
}
System.out.println("B-Machine " + machineFile.getAbsolutePath()
+ " created.");
System.out.println("B-Machine " + machineFile.getAbsolutePath() + " created.");
} catch (IOException e) {
System.err.println("Error while creating file '"
+ machineFile.getAbsolutePath() + "'.");
System.err.println("Error while creating file '" + machineFile.getAbsolutePath() + "'.");
System.exit(-1);
}
}
public static RecursiveMachineLoader parseAllMachines(final Start ast,
final File f, final BParser bparser) throws BException {
final RecursiveMachineLoader rml = new RecursiveMachineLoader(
f.getParent(), bparser.getContentProvider());
rml.loadAllMachines(f, ast, bparser.getSourcePositions(),
bparser.getDefinitions());
public static RecursiveMachineLoader parseAllMachines(final Start ast, final File f, final BParser bparser)
throws BCompoundException {
final RecursiveMachineLoader rml = new RecursiveMachineLoader(f.getParent(), bparser.getContentProvider());
rml.loadAllMachines(f, ast, bparser.getSourcePositions(), bparser.getDefinitions());
return rml;
}
public Start translateExpression(String tlaExpression)
throws TLA2BException {
ExpressionTranslator expressionTranslator = new ExpressionTranslator(
tlaExpression, this);
public Start translateExpression(String tlaExpression) throws TLA2BException {
ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression, this);
expressionTranslator.parse();
Start start = expressionTranslator.translateIncludingModel();
return start;
}
public static Start translateTlaExpression(String tlaExpression) {
ExpressionTranslator expressionTranslator = new ExpressionTranslator(
tlaExpression);
ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression);
expressionTranslator.parse();
expressionTranslator.translate();
return expressionTranslator.getBExpressionParseUnit();
......
src/test/java/de/tla2b/examples/RegressionTests.java
+ 4
− 5
View file @ 15ecfd4c
package de.tla2b.examples;
import static de.tla2b.util.TestUtil.load_TLA_File;
import java.io.File;
import java.util.ArrayList;
......@@ -12,6 +10,7 @@ import de.tla2b.util.AbstractParseModuleTest;
import de.tla2b.util.PolySuite;
import de.tla2b.util.PolySuite.Config;
import de.tla2b.util.PolySuite.Configuration;
import de.tla2b.util.TestUtil;
@RunWith(PolySuite.class)
public class RegressionTests extends AbstractParseModuleTest {
......@@ -23,7 +22,7 @@ public class RegressionTests extends AbstractParseModuleTest{
@Test
public void testRunTLC() throws Exception {
load_TLA_File(moduleFile.getPath());
TestUtil.loadTlaFile(moduleFile.getPath());
}
@Config
......
src/test/java/de/tla2b/prettyprintb/ActionsTest.java
+ 0
− 1
View file @ 15ecfd4c
......@@ -2,7 +2,6 @@ package de.tla2b.prettyprintb;
import static de.tla2b.util.TestUtil.compare;
import org.junit.Ignore;
import org.junit.Test;
public class ActionsTest {
......
src/test/java/de/tla2b/util/TestUtil.java
+ 21
− 60
View file @ 15ecfd4c
......@@ -8,13 +8,9 @@ import static org.junit.Assert.*;
import util.FileUtil;
import de.be4.classicalb.core.parser.BParser;
import de.be4.classicalb.core.parser.exceptions.BException;
import de.be4.classicalb.core.parser.exceptions.BCompoundException;
import de.be4.classicalb.core.parser.node.Node;
import de.be4.classicalb.core.parser.node.Start;
//import de.prob.scripting.Api;
//import de.prob.statespace.StateSpace;
//import de.prob.statespace.Trace;
//import de.prob.statespace.Transition;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.output.ASTPrettyPrinter;
......@@ -24,14 +20,10 @@ import util.ToolIO;
public class TestUtil {
// public static StringBuilder translateString(String moduleString)
// throws FrontEndException, TLA2BException, AbortException {
// ToolIO.setMode(ToolIO.TOOL);
// ToolIO.reset();
// Tla2BTranslator translator = new Tla2BTranslator();
// translator.startTest(moduleString, null);
// return translator.translate();
// }
public static void loadTlaFile(String tlaFile) throws Exception {
Translator t = new Translator(tlaFile);
t.translate();
}
public static void runModule(String tlaFile) throws Exception {
Translator t = new Translator(tlaFile);
......@@ -56,8 +48,7 @@ public class TestUtil {
// System.out.println(t.getBDefinitions().getDefinitionNames());
}
public static void compareExpr(String bExpr, String tlaExpr)
throws BException {
public static void compareExpr(String bExpr, String tlaExpr) throws Exception {
ToolIO.setMode(ToolIO.TOOL);
ToolIO.reset();
Start resultNode = Translator.translateTlaExpression(tlaExpr);
......@@ -71,8 +62,7 @@ public class TestUtil {
assertEquals(bAstString, result);
}
public static void compareExprIncludingModel(String bExpr, String tlaExpr,
String moduleString) throws TLA2BException, BException {
public static void compareExprIncludingModel(String bExpr, String tlaExpr, String moduleString) throws Exception {
Translator trans = new Translator(moduleString, null);
trans.translate();
Start resultNode = trans.translateExpression(tlaExpr);
......@@ -84,20 +74,16 @@ public class TestUtil {
assertEquals(bAstString, result);
}
public static void compare(String bMachine, String tlaModule)
throws BException, TLA2BException {
public static void compare(final String bMachine, final String tlaModule) throws Exception {
ToolIO.setMode(ToolIO.TOOL);
String expected = getAstStringofBMachineString(bMachine);
Translator trans = new Translator(tlaModule, null);
Start resultNode = trans.translate();
String result = getTreeAsString(resultNode);
System.out.println(expected);
System.out.println(result);
ASTPrettyPrinter aP = new ASTPrettyPrinter(resultNode);
resultNode.apply(aP);
System.out.println("-------------------");
......@@ -116,8 +102,7 @@ public class TestUtil {
// assertEquals(expected, getTreeAsString(ast));
}
public static void compare(String bMachine, String tlaModule, String config)
throws BException, TLA2BException {
public static void compare(String bMachine, String tlaModule, String config) throws Exception {
ToolIO.setMode(ToolIO.TOOL);
String expected = getAstStringofBMachineString(bMachine);
System.out.println(expected);
......@@ -129,9 +114,6 @@ public class TestUtil {
resultNode.apply(aP);
System.out.println(aP.getResultString());
// BParser.printASTasProlog(System.out, new BParser(), new
// File("./test.mch"), resultNode, false, true, null);
String result = getTreeAsString(resultNode);
System.out.println(result);
assertEquals(expected, result);
......@@ -155,8 +137,7 @@ public class TestUtil {
parser.parse(aP.getResultString(), false);
}
public static TestTypeChecker typeCheckString(String moduleString)
throws FrontEndException, TLA2BException {
public static TestTypeChecker typeCheckString(String moduleString) throws FrontEndException, TLA2BException {
ToolIO.setMode(ToolIO.TOOL);
ToolIO.reset();
TestTypeChecker testTypeChecker = new TestTypeChecker();
......@@ -165,8 +146,8 @@ public class TestUtil {
}
public static TestTypeChecker typeCheckString(String moduleString,
String configString) throws FrontEndException, TLA2BException {
public static TestTypeChecker typeCheckString(String moduleString, String configString)
throws FrontEndException, TLA2BException {
ToolIO.setMode(ToolIO.TOOL);
ToolIO.reset();
TestTypeChecker testTypeChecker = new TestTypeChecker();
......@@ -174,8 +155,7 @@ public class TestUtil {
return testTypeChecker;
}
public static TestTypeChecker typeCheck(String moduleFileName)
throws FrontEndException, TLA2BException {
public static TestTypeChecker typeCheck(String moduleFileName) throws FrontEndException, TLA2BException {
ToolIO.setMode(ToolIO.TOOL);
ToolIO.reset();
moduleFileName = moduleFileName.replace('/', FileUtil.separatorChar);
......@@ -184,8 +164,7 @@ public class TestUtil {
return testTypeChecker;
}
public static String getAstStringofBMachineString(final String testMachine)
throws BException {
public static String getAstStringofBMachineString(final String testMachine) throws BCompoundException {
final BParser parser = new BParser("testcase");
final Start startNode = parser.parse(testMachine, false);
......@@ -195,8 +174,7 @@ public class TestUtil {
return string;
}
public static String getAstStringofBExpressionString(final String expr)
throws BException {
public static String getAstStringofBExpressionString(final String expr) throws BCompoundException {
final BParser parser = new BParser("testcase");
final Start startNode = parser.parse("#FORMULA " + expr, false);
......@@ -206,21 +184,4 @@ public class TestUtil {
return string;
}
public static void load_TLA_File(String tlaFile) throws Exception {
// Api api = de.prob.Main.getInjector().getInstance(Api.class);
// // TODO translate here and then pass the AST to api
// // Currently B definitions are not recognized by the api load command
// // Translator t = new Translator(tlaFile);
// // Start start = t.translate();
// // ASTPrettyPrinter aP = new ASTPrettyPrinter(start);
// // start.apply(aP);
// // System.out.println(aP.getResultString());
// // StateSpace stateSpace = api.b_load(start);
//
// StateSpace stateSpace = api.tla_load(tlaFile);
// Trace trace = new Trace(stateSpace);
// Set<Transition> nextTransitions = trace.getNextTransitions();
// assertTrue(nextTransitions.size() > 0);
}
}
src/test/java/de/tla2b/prettyprintb/ExampleFilesTest.java → src/test/java/testing/ExampleFilesTest.java
+ 1
− 1
View file @ 15ecfd4c
package de.tla2b.prettyprintb;
package testing;
import java.io.File;
import java.util.ArrayList;
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment