diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java index 6817f7107d220c52c9f6b2803a5ad86f4c496e1a..b762f563129aa5f9d69371bccb95fc6237156a9b 100644 --- a/src/main/java/de/tlc4b/TLC4B.java +++ b/src/main/java/de/tlc4b/TLC4B.java @@ -72,6 +72,11 @@ public class TLC4B { private void printResults(TLCResults results, boolean createTraceFile) { + String s = ""; + for (int i = 0; i < 10; i++) { + s += i; + } + System.out.println("Parsing time: " + StopWatch.getRunTime("Parsing") + " ms"); System.out.println("Translation time: " + StopWatch.getRunTime("Pure") diff --git a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java index 1798fb444d4f14b2c64c118c02e33d5024a586ce..56372a55d502a3d439ca0aec65cd62360a3b13c1 100644 --- a/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java +++ b/src/main/java/de/tlc4b/analysis/NotSupportedConstructs.java @@ -7,6 +7,7 @@ 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; @@ -18,12 +19,19 @@ public class NotSupportedConstructs extends DepthFirstAdapter { public NotSupportedConstructs(Start start) { start.apply(this); + System.out.println(start.getPParseUnit().getClass()); } 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( diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java index c1e861c23962689b6ff2d3bbde139d178fa15969..425a40569503c23db5e1080f0cfc533650d776f4 100644 --- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java +++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java @@ -813,7 +813,7 @@ public class TLAPrinter extends DepthFirstAdapter { public void caseASelectSubstitution(ASelectSubstitution node) { inASelectSubstitution(node); // TODO remove brackets - + tlaModuleString.append("("); List<PSubstitution> copy = new ArrayList<PSubstitution>( node.getWhenSubstitutions()); @@ -857,6 +857,7 @@ public class TLAPrinter extends DepthFirstAdapter { && (copy.size() > 0 || node.getElse() != null)) { tlaModuleString.append(")"); } + tlaModuleString.append(")"); printUnchangedVariables(node, true); outASelectSubstitution(node); diff --git a/src/test/java/testing/Testing2.java b/src/test/java/testing/Testing2.java index 4a936a7b82e06041d5f131e6470d3ff5215bea27..925ef7ec719a8beed62958d49f39341bed4edd41 100644 --- a/src/test/java/testing/Testing2.java +++ b/src/test/java/testing/Testing2.java @@ -29,6 +29,7 @@ public class Testing2 extends AbstractParseMachineTest { @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);