1/*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 */
10
11#ifndef COMPILE
12#define NULL ((void*)0)
13#endif
14
15struct node {
16  struct node *l, *r;
17  unsigned m, c;
18};
19
20/* This is Mehta & Nipkow's version of the algorithm (HOL/Hoare/SchorrWaite.thy). */
21void schorr_waite(struct node *root) {
22  struct node *t = root, *p = NULL, *q;
23  while (p != NULL || (t != NULL && !t->m)) {
24    if (t == NULL || t->m) {
25      if (p->c) {
26        q = t; t = p; p = p->r; t->r = q;
27      } else {
28        q = t; t = p->r; p->r = p->l; p->l = q; p->c = 1;
29      }
30    } else {
31      q = p; p = t; t = t->l; p->l = q; p->m = 1; p->c = 0;
32    }
33  }
34}
35
36
37/*
38 * An executable specification for graph traversal.
39 */
40void simple_traverse(struct node *n) {
41  if (n == NULL || n->m) {
42    return;
43  }
44
45  n->m = 1;
46  simple_traverse(n->l);
47  simple_traverse(n->r);
48}
49
50#ifdef COMPILE
51#include <stdlib.h>
52#include <assert.h>
53#include <sys/time.h>
54#include <time.h>
55
56void make_graph(unsigned size, unsigned graph[size][2], struct node n[size]) {
57  for (unsigned i = 0; i < size; ++i) {
58    if (graph[i][0] == size) {
59      n[i].l = NULL;
60    } else {
61      n[i].l = &n[0] + graph[i][0];
62    }
63    if (graph[i][1] == size) {
64      n[i].r = NULL;
65    } else {
66      n[i].r = &n[0] + graph[i][1];
67    }
68    n[i].c = n[i].m = 0;
69  }
70}
71
72int main(void) {
73  const unsigned max_size = 1000;
74  unsigned graph[max_size][2];
75
76  struct timeval tv;
77  if (gettimeofday(&tv, NULL)) {
78    return 1;
79  }
80  unsigned long long t = (unsigned long long)tv.tv_sec * 1000000 + tv.tv_usec;
81  const int seed = (t >> 32) ^ t;
82
83  srand(seed);
84  unsigned size = rand() % max_size + 1;
85  for (unsigned i = 0; i < size; ++i) {
86    graph[i][0] = rand() % (size+1);
87    graph[i][1] = rand() % (size+1);
88  }
89
90  struct node n1[max_size], n2[max_size];
91  make_graph(size, graph, n1);
92  make_graph(size, graph, n2);
93
94  schorr_waite(n1);
95  simple_traverse(n2);
96
97  for (unsigned i = 0; i < size; ++i) {
98    if (graph[i][0] == size) {
99      assert(n1[i].l == NULL);
100      assert(n2[i].l == NULL);
101    } else {
102      assert(n1[i].l == n1 + graph[i][0]);
103      assert(n2[i].l == n2 + graph[i][0]);
104    }
105    if (graph[i][1] == size) {
106      assert(n1[i].r == NULL);
107      assert(n2[i].r == NULL);
108    } else {
109      assert(n1[i].r == n1 + graph[i][1]);
110      assert(n2[i].r == n2 + graph[i][1]);
111    }
112    assert(n1[i].m == n2[i].m);
113  }
114
115  return 0;
116}
117#endif
118