diff --git a/src/main/java/de/tla2b/TLA2B.java b/src/main/java/de/tla2b/TLA2B.java
index 4436f6243d1559c369cb7b8cb2702db1788fc50a..b717d538724e05242dc6e6bc61f866f339dd45bc 100644
--- a/src/main/java/de/tla2b/TLA2B.java
+++ b/src/main/java/de/tla2b/TLA2B.java
@@ -4,11 +4,19 @@
package de.tla2b;
+import java.io.File;
+import java.io.PrintStream;
+import java.io.PrintWriter;
+
+import de.be4.classicalb.core.parser.BParser;
import de.tla2b.exceptions.FrontEndException;
import de.tla2b.exceptions.NotImplementedException;
import de.tla2b.exceptions.TLA2BException;
import de.tla2b.global.TranslationGlobals;
import de.tla2bAst.Translator;
+import de.be4.classicalb.core.parser.analysis.prolog.RecursiveMachineLoader;
+import de.be4.classicalb.core.parser.exceptions.BException;
+import de.be4.classicalb.core.parser.node.Start;
public class TLA2B implements TranslationGlobals {
private String mainFile;
@@ -62,6 +70,8 @@ public class TLA2B implements TranslationGlobals {
System.exit(-1);
}
translator.createMachineFile();
+ translator.createProbFile();
}
+
}
diff --git a/src/main/java/de/tla2bAst/Translator.java b/src/main/java/de/tla2bAst/Translator.java
index 94a1908996f6c64eb8ef41a66fd7c2a60627b502..60950178c119c6be72e91296c6a264b35781277d 100644
--- a/src/main/java/de/tla2bAst/Translator.java
+++ b/src/main/java/de/tla2bAst/Translator.java
@@ -2,13 +2,18 @@ package de.tla2bAst;
import java.io.BufferedReader;
import java.io.File;
+import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
+import java.io.PrintWriter;
import java.io.Writer;
import java.util.Date;
+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.node.Start;
import de.tla2b.analysis.InstanceTransformation;
import de.tla2b.analysis.PredicateVsExpression;
@@ -48,10 +53,7 @@ public class Translator implements TranslationGlobals {
private SpecAnalyser specAnalyser;
private TypeChecker typechecker;
-
-
-
-
+
public Translator(String moduleFileName) throws FrontEndException {
this.moduleFileName = moduleFileName;
@@ -62,7 +64,8 @@ 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()) {
@@ -199,10 +202,9 @@ public class Translator implements TranslationGlobals {
specAnalyser = SpecAnalyser.createSpecAnalyser(moduleNode);
}
specAnalyser.start();
- typechecker = new TypeChecker(moduleNode, conEval,
- specAnalyser);
+ typechecker = new TypeChecker(moduleNode, conEval, specAnalyser);
typechecker.start();
-
+
SymbolRenamer symRenamer = new SymbolRenamer(moduleNode, specAnalyser);
symRenamer.start();
UsedExternalFunctions usedExternalFunctions = new UsedExternalFunctions(
@@ -218,6 +220,35 @@ public class Translator implements TranslationGlobals {
return BAst;
}
+ public void createProbFile() {
+ 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.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);
+ System.out.println(probFile.getAbsolutePath() + " created.");
+ } catch (BException e) {
+ e.printStackTrace();
+ } catch (FileNotFoundException e) {
+ e.printStackTrace();
+ }
+ }
+
public void createMachineFile() {
String bFile = FileUtils.removeExtention(moduleFile.getAbsolutePath());
bFile = bFile + "_tla.mch";
@@ -274,21 +305,32 @@ public class Translator implements TranslationGlobals {
}
- public Start translateExpression(String tlaExpression) throws TLA2BException{
- ExpressionTranslator expressionTranslator = new ExpressionTranslator(tlaExpression, this);
+ 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, null, bparser.getDefinitions(),
+ bparser.getPragmas());
+ return rml;
+ }
+
+ 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);
+ public static Start translateTlaExpression(String tlaExpression) {
+ ExpressionTranslator expressionTranslator = new ExpressionTranslator(
+ tlaExpression);
expressionTranslator.parse();
expressionTranslator.translate();
return expressionTranslator.getBExpressionParseUnit();
}
-
public Definitions getBDefinitions() {
return bDefinitions;
@@ -301,13 +343,21 @@ public class Translator implements TranslationGlobals {
public ModuleNode getModuleNode() {
return moduleNode;
}
-
- protected TypeChecker getTypeChecker(){
+
+ protected TypeChecker getTypeChecker() {
return this.typechecker;
}
- protected SpecAnalyser getSpecAnalyser(){
+ protected SpecAnalyser getSpecAnalyser() {
return this.specAnalyser;
}
-
+
+ public Start getBAST() {
+ return BAst;
+ }
+
+ public File getModuleFile() {
+ return moduleFile;
+ }
+
}
diff --git a/src/test/resources/regression/Club/Club.prob b/src/test/resources/regression/Club/Club.prob
new file mode 100644
index 0000000000000000000000000000000000000000..8233cd655d1b118e9429e03a39c92318ab25fa41
--- /dev/null
+++ b/src/test/resources/regression/Club/Club.prob
@@ -0,0 +1,3 @@
+parser_version('2014-03-12 22:57:52.564').
+classical_b('Club',['/Users/hansen/git/tla2bAST/src/test/resources/regression/Club/Club.tla']).
+machine(abstract_machine(1,machine(2),machine_header(3,'Club',[]),[sets(4,[enumerated_set(5,'ENUM1',[identifier(6,n1),identifier(7,n2),identifier(8,n3)])]),abstract_constants(9,[identifier(10,capacity),identifier(11,'NAME'),identifier(12,total)]),properties(13,conjunct(14,conjunct(15,conjunct(16,conjunct(17,conjunct(18,member(19,identifier(20,capacity),integer_set(21)),equal(22,identifier(23,'NAME'),identifier(24,'ENUM1'))),member(25,identifier(26,total),integer_set(27))),conjunct(28,member(29,identifier(30,capacity),natural_set(31)),equal(32,identifier(33,capacity),integer(34,2)))),greater(35,card(36,identifier(37,'NAME')),identifier(38,capacity))),conjunct(39,member(40,identifier(41,total),natural_set(42)),greater(43,identifier(44,total),integer(45,2))))),variables(46,[identifier(47,member),identifier(48,waiting)]),invariant(49,conjunct(50,member(51,identifier(52,member),pow_subset(53,identifier(54,'ENUM1'))),member(55,identifier(56,waiting),pow_subset(57,identifier(58,'ENUM1'))))),initialisation(59,becomes_such(60,[identifier(61,member),identifier(62,waiting)],conjunct(63,equal(64,identifier(65,member),empty_set(66)),equal(67,identifier(68,waiting),empty_set(69))))),operations(70,[operation(71,identifier(71,join_queue),[],[identifier(72,nn)],any(73,[identifier(74,member_n)],conjunct(75,conjunct(76,conjunct(77,conjunct(78,conjunct(79,member(80,identifier(81,nn),identifier(82,'NAME')),not_member(83,identifier(84,nn),identifier(85,member))),not_member(86,identifier(87,nn),identifier(88,waiting))),member(89,identifier(90,member_n),pow_subset(91,identifier(92,'ENUM1')))),less(93,card(94,identifier(95,waiting)),identifier(96,total))),equal(97,identifier(98,member_n),identifier(99,member))),assign(100,[identifier(101,waiting),identifier(102,member)],[union(103,identifier(104,waiting),set_extension(105,[identifier(106,nn)])),identifier(107,member_n)]))),operation(108,identifier(108,join),[],[identifier(109,nn)],select(110,conjunct(111,conjunct(112,conjunct(113,member(114,identifier(115,nn),identifier(116,'NAME')),member(117,identifier(118,nn),identifier(119,waiting))),less(120,card(121,identifier(122,member)),identifier(123,capacity))),less(124,card(125,identifier(126,member)),identifier(127,capacity))),assign(128,[identifier(129,member),identifier(130,waiting)],[union(131,identifier(132,member),set_extension(133,[identifier(134,nn)])),minus_or_set_subtract(135,identifier(136,waiting),set_extension(137,[identifier(138,nn)]))]),[])),operation(139,identifier(139,remove),[],[identifier(140,nn)],any(141,[identifier(142,waiting_n)],conjunct(143,conjunct(144,conjunct(145,member(146,identifier(147,nn),identifier(148,'NAME')),member(149,identifier(150,nn),identifier(151,member))),member(152,identifier(153,waiting_n),pow_subset(154,identifier(155,'ENUM1')))),equal(156,identifier(157,waiting_n),identifier(158,waiting))),assign(159,[identifier(160,member),identifier(161,waiting)],[minus_or_set_subtract(162,identifier(163,member),set_extension(164,[identifier(165,nn)])),identifier(166,waiting_n)])))])])).