view src/llrb/verifier/verify_put_cs.c @ 99:ca55f4be5f0f

Create verifier directory
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 02 Feb 2016 16:02:55 +0900
parents
children 3d7ecced7e14
line wrap: on
line source

/* Verification of LLRB-Tree height in put operations.
 * LLRB-Tree allows (max-height) <= 2*(min-height).
 */

#include <stdlib.h>
#include <stdio.h>
#include <time.h>
#include "../llrbContext.h"

void verify_tree_height(struct Node*);

__code meta(struct Context* context, enum Code next) {
    if (next == Put) {
        verify_tree_height(context->data[Tree]->tree.root);
    }
    goto (context->code[next])(context);
}

__code start_code(struct Context* context, enum Code next) {
    unsigned int seed = (unsigned int)time(NULL);

    printf("--- srand(%u)\n", seed);
    goto meta(context, next);
}

__code exit_code(struct Context* context) {
    free(context->code);
    free(context->data);
    free(context->heapStart);
    goto exit(0);
}

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 verify_tree_height(struct Node* root) {
    if (root == NULL) return;

    unsigned int min_h = min_height(root, 1);
    unsigned int max_h = max_height(root, 1);

    if (max_h >= 2*min_h) {
        printf("llrb-condition violated.\n");
        printf("\tmin-height %u", min_h);
        printf("\tmax-height %u", max_h);
        exit(EXIT_FAILURE);
    }
}