From bc4cf703c3b9a427ceafc58f8f64e78718479f8d Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Wed, 30 Apr 2014 16:20:15 +0200
Subject: [PATCH] multiple recursive functions
---
.../java/de/tla2b/analysis/SpecAnalyser.java | 5 ++---
.../prettyprintb/RecursiveFunctionTest.java | 18 ++++++++++++++++++
2 files changed, 20 insertions(+), 3 deletions(-)
diff --git a/src/main/java/de/tla2b/analysis/SpecAnalyser.java b/src/main/java/de/tla2b/analysis/SpecAnalyser.java
index 7602508..f0de31a 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 b2f3c81..3341f3c 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);
}
+
+
+
}
--
GitLab