view src/insert_verification/verifySpecification.c @ 43:23b9717a5c14

Fix include
author atton
date Thu, 16 Jun 2016 07:23:27 +0000
parents 56ea709e7af3
children 3e6cd523bf6d
line wrap: on
line source

#include <stdio.h>
#include "akashaLLRBContext.h"
#include "akashaCS.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) {
        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);
    }

    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, &context->data[Allocate]->allocate, &context->data[AkashaInfo]->akashaInfo);

}
__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_stub(struct Context* context) {
    goto verifySpecification(context, &context->data[Allocate]->allocate, &context->data[Tree]->tree, &context->data[AkashaInfo]->akashaInfo);
}

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

    allocate->size = sizeof(struct AkashaNode);
    allocator(context);
    akashaInfo->akashaNode = (struct AkashaNode*)context->data[context->dataNum];

    akashaInfo->akashaNode->height = 1;
    akashaInfo->akashaNode->node   = tree->root;

    goto getMinHeight_stub(context);
}

__code verifySpecificationFinish(struct Context* context) {
    if (context->data[AkashaInfo]->akashaInfo.minHeight > 2*context->data[AkashaInfo]->akashaInfo.maxHeight) {
        context->next = Exit;
        goto meta(context, ShowTrace);
    }
    goto meta(context, DuplicateIterator);
}