Skip to content
Snippets Groups Projects
Commit 615a6961 authored by hansen's avatar hansen
Browse files

fixed precedence Bug

parent e140d6fa
No related branches found
No related tags found
No related merge requests found
......@@ -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")
......
......@@ -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,6 +19,7 @@ public class NotSupportedConstructs extends DepthFirstAdapter {
public NotSupportedConstructs(Start start) {
start.apply(this);
System.out.println(start.getPParseUnit().getClass());
}
public void inARefinesModelClause(ARefinesModelClause node) {
......@@ -25,6 +27,12 @@ public class NotSupportedConstructs extends DepthFirstAdapter {
"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.");
......
......@@ -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);
......
......@@ -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);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment