# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1465803030 -32400
# Node ID 81717f43ea007f4165c69d59f51ea6aa996388dc
# Parent  593ab851ad7696ffb3944b44f3cd588d94119578
Convert C function to cs (getMaxHeight)

diff -r 593ab851ad76 -r 81717f43ea00 src/insert_verification/include/akashaLLRBContext.h
--- a/src/insert_verification/include/akashaLLRBContext.h	Mon Jun 13 11:47:37 2016 +0900
+++ b/src/insert_verification/include/akashaLLRBContext.h	Mon Jun 13 16:30:30 2016 +0900
@@ -2,7 +2,7 @@
 #include "stack.h"
 
 #define ALLOCATE_SIZE 20000000
-#define LIMIT_OF_VERIFICATION_SIZE 8
+#define LIMIT_OF_VERIFICATION_SIZE 10
 
 enum Code {
     ShowTree,
diff -r 593ab851ad76 -r 81717f43ea00 src/insert_verification/verifySpecification.c
--- a/src/insert_verification/verifySpecification.c	Mon Jun 13 11:47:37 2016 +0900
+++ b/src/insert_verification/verifySpecification.c	Mon Jun 13 16:30:30 2016 +0900
@@ -65,6 +65,13 @@
     const struct AkashaNode* akashaNode = akashaInfo->akashaNode;
 
     if (akashaNode == NULL) {
+        allocate->size = sizeof(struct AkashaNode);
+        allocator(context);
+        akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum];
+
+        akashaInfo->akashaNode->height = 1;
+        akashaInfo->akashaNode->node   = context->data[Tree]->tree.root;
+
         goto getMaxHeight_stub(context);
     }
 
@@ -103,20 +110,68 @@
 }
 
 __code getMaxHeight_stub(struct Context* context) {
-    goto getMaxHeight(context);
+    goto getMaxHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo);
+
 }
-__code getMaxHeight(struct Context* context) {
-    goto verifySpecificationFinish(context);
+__code getMaxHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) {
+    const struct AkashaNode* akashaNode = akashaInfo->akashaNode;
+
+    if (akashaNode == NULL) {
+        allocate->size = sizeof(struct AkashaNode);
+        allocator(context);
+        akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum];
+
+        akashaInfo->akashaNode->height = 1;
+        akashaInfo->akashaNode->node   = context->data[Tree]->tree.root;
+
+        goto verifySpecificationFinish(context);
+    }
+
+    /* FIXME: Reuse parts of getMinHeight */
+    const struct Node* node = akashaInfo->akashaNode->node;
+    if (node->left == NULL && node->right == NULL) {
+        if (akashaInfo->maxHeight < akashaNode->height) {
+            akashaInfo->maxHeight  = akashaNode->height;
+            akashaInfo->akashaNode = akashaNode->nextAkashaNode;
+            goto getMaxHeight_stub(context);
+        }
+    }
+
+    akashaInfo->akashaNode = akashaInfo->akashaNode->nextAkashaNode;
+
+    if (node->left != NULL) {
+        allocate->size = sizeof(struct AkashaNode);
+        allocator(context);
+        struct AkashaNode* left = (struct AkashaNode*)context->data[context->dataNum];
+        left->height           = akashaNode->height+1;
+        left->node             = node->left;
+        left->nextAkashaNode   = akashaInfo->akashaNode;
+        akashaInfo->akashaNode = left;
+    }
+
+    if (node->right != NULL) {
+        allocate->size = sizeof(struct AkashaNode);
+        allocator(context);
+        struct AkashaNode* right = (struct AkashaNode*)context->data[context->dataNum];
+        right->height            = akashaNode->height+1;
+        right->node              = node->right;
+        right->nextAkashaNode    = akashaInfo->akashaNode;
+        akashaInfo->akashaNode   = right;
+    }
+
+    goto getMaxHeight_stub(context);
 }
 
 __code verifySpecification(struct Context* context, struct Allocate* allocate, struct Tree* tree, struct AkashaInfo* akashaInfo) {
+    if (tree->root == NULL) {
+        akashaInfo->minHeight = 1;
+        akashaInfo->maxHeight = 1;
+        goto verifySpecificationFinish(context);
+    }
+
     akashaInfo->minHeight = -1;
     akashaInfo->maxHeight = 0;
 
-    if (tree->root == NULL) {
-        goto verifySpecificationFinish(context);
-    }
-
     allocate->size = sizeof(struct AkashaNode);
     allocator(context);
     akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum];
@@ -124,28 +179,13 @@
     akashaInfo->akashaNode->height = 1;
     akashaInfo->akashaNode->node   = tree->root;
 
-
-    //unsigned const int max_h = max_height(tree->root, 1);
-
     goto getMinHeight_stub(context);
 }
 
 __code verifySpecificationFinish(struct Context* context) {
-
-    printf(">>>>>>>>>>\n");
-    printTree(context->data[Tree]->tree.root, 0);
-    printf("%d\n", context->data[AkashaInfo]->akashaInfo.minHeight);
-    printf("<<<<<<<<<<\n");
-
-    /*
-    if (max_h > 2*min_h) {
-        printf("llrb-condition violated.\n");
-        printf("\tmin-height %u\n", min_h);
-        printf("\tmax-height %u\n", max_h);
-
+    if (context->data[AkashaInfo]->akashaInfo.minHeight > 2*context->data[AkashaInfo]->akashaInfo.maxHeight) {
         context->next = Exit;
         goto meta(context, ShowTrace);
     }
-    */
     goto meta(context, DuplicateIterator);
 }