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

multiple recursive functions

parent 37f493e8
No related branches found
No related tags found
No related merge requests found
......@@ -18,7 +18,6 @@ import de.tla2b.exceptions.SemanticErrorException;
import de.tla2b.global.BBuiltInOPs;
import de.tla2b.global.TranslationGlobals;
import de.tla2b.types.IType;
import de.tla2b.types.TLAType;
import tla2sany.semantic.ASTConstants;
import tla2sany.semantic.AssumeNode;
......@@ -108,6 +107,8 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
public void start() throws SemanticErrorException, FrontEndException,
ConfigFileErrorException, NotImplementedException {
if (spec != null) {
evalSpec();
} else {
......@@ -134,7 +135,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
con.getName()));
}
}
evalRecursiveFunctions();
}
......@@ -579,7 +579,6 @@ public class SpecAnalyser extends BuiltInOPs implements ASTConstants,
case OPCODE_rfs: { // recursive Function
bDefinitionsSet.remove(def);
recursiveFunctions.add(def);
return;
}
}
}
......
......@@ -52,6 +52,24 @@ public class RecursiveFunctionTest {
+ "fac = %(x).(x : NATURAL | 5 + (%(t_).(t_ = 0 & x = 1 | 1) \\/ %(t_).(t_ = 0 & not(x = 1) | x * fac((x - 1))))(0)) & fac(3) = 56 \n"
+ "END";
compare(expected, module);
}
@Test
public void testSum() throws Exception {
final String module = "-------------- MODULE Testing ----------------\n"
+ "EXTENDS Integers, FiniteSets \n"
+ " Sum[x \\in Nat] == IF x = 0 THEN 0 ELSE x + Sum[x-1] \n"
+ "ASSUME 6 = Sum[3] \n"
+ "=================================";
final String expected = "MACHINE Testing\n"
+ "ABSTRACT_CONSTANTS Sum\n"
+ "PROPERTIES "
+ "Sum = %(x).(x : NATURAL | (%(t_).(t_ = 0 & x = 0 | 0) \\/ %(t_).(t_ = 0 & not(x = 0) | x + Sum((x - 1))))(0)) & 6 = Sum(3) \n"
+ "END";
compare(expected, module);
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment