diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java index 7602508f2295ea4a7a62092ec2618145951d7190..f0de31afdc577bbfafa9e67785bc52cf8a90732a 100644 --- a/src/main/java/de/tla2b/analysis/SpecAnalyser.java +++ b/src/main/java/de/tla2b/analysis/SpecAnalyser.java @@ -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; } } } diff --git a/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java b/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java index b2f3c81ab0b9de5389256b8614745f4730e8e0ab..3341f3cecf25f5cebf32cd3a3daf2f06606b4021 100644 --- a/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java +++ b/src/test/java/de/tla2b/prettyprintb/RecursiveFunctionTest.java @@ -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); } + + + }