view src/insert_verification/verifySpecification.c @ 38:593ab851ad76

Convert C function to cs (getMinHeight)
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 13 Jun 2016 11:47:37 +0900
parents be67b0312bea
children 81717f43ea00
line wrap: on
line source

#include <stdio.h>
#include "akashaLLRBContext.h"

extern void allocator(struct Context*);

/* C functions (TODO: convert to code segment) */

unsigned int min_height(struct Node* node, unsigned int height) {
    if ((node->left == NULL) && (node->right == NULL)) return height;
    if (node->left  == NULL) return min_height(node->right, height+1);
    if (node->right == NULL) return min_height(node->left, height+1);

    unsigned int left_min  = min_height(node->left, height+1);
    unsigned int right_min = min_height(node->right, height+1);

    if (left_min < right_min) {
        return left_min;
    } else {
        return right_min;
    }
}

unsigned int max_height(struct Node* node, unsigned int height) {
    if ((node->left == NULL) && (node->right == NULL)) return height;
    if (node->left  == NULL) return max_height(node->right, height+1);
    if (node->right == NULL) return max_height(node->left, height+1);

    unsigned int left_max  = max_height(node->left, height+1);
    unsigned int right_max = max_height(node->right, height+1);

    if (left_max > right_max) {
        return left_max;
    } else {
        return right_max;
    }
}
void printTree(struct Node* node, int n) {
    if (node != 0) {
        printTree(node->left, n+1);
        for (int i=0;i<n;i++)
            printf("  ");
        printf("key=%d value=%d color=%s\t%p\n", node->key, node->value,/* n, */node->color==0? "R":"B", node);
        printTree(node->right, n+1);
    }
}

/* Code Segments */

__code showTrace(struct Context* context, struct Iterator* iter) {
    printf("show trace(reversed):");

    for (; iter != NULL; iter = iter->previousDepth) {
        printf("%u ", iter->iteratedValue);
    }
    printf("\n");

    goto meta(context, context->next);
}

__code getMinHeight_stub(struct Context* context) {
    goto getMinHeight(context, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo);
}

__code getMinHeight(struct Context* context, struct Allocate* allocate, struct AkashaInfo* akashaInfo) {
    const struct AkashaNode* akashaNode = akashaInfo->akashaNode;

    if (akashaNode == NULL) {
        goto getMaxHeight_stub(context);
    }

    const struct Node* node = akashaInfo->akashaNode->node;
    if (node->left == NULL && node->right == NULL) {
        if (akashaInfo->minHeight > akashaNode->height) {
            akashaInfo->minHeight  = akashaNode->height;
            akashaInfo->akashaNode = akashaNode->nextAkashaNode;
            goto getMinHeight_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 getMinHeight_stub(context);
}

__code getMaxHeight_stub(struct Context* context) {
    goto getMaxHeight(context);
}
__code getMaxHeight(struct Context* context) {
    goto verifySpecificationFinish(context);
}

__code verifySpecification(struct Context* context, struct Allocate* allocate, struct Tree* tree, struct AkashaInfo* akashaInfo) {
    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];

    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);

        context->next = Exit;
        goto meta(context, ShowTrace);
    }
    */
    goto meta(context, DuplicateIterator);
}