view DPP/ltl.cbc @ 33:3946f8d26710 draft default tip

add benchmarck/binary-trees
author Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
date Tue, 09 Apr 2013 16:41:30 +0900
parents a89b61162c29
children
line wrap: on
line source

#include <stdio.h>
#include "queue.h"
#include "dpp_common.h"

static int
p(PhilsPtr phils)
{
    PhilsPtr current = phils;
    PhilsPtr last = phils->left;

    if (last->left_fork->owner == NULL) return 0;
    while (current != last) {
		if (current->left_fork->owner == NULL) return 0;
		current = current->right;
    }
    return 1;
}

code check(int *always_flag, PhilsPtr phils, TaskPtr list)
{
    if (p(list->phils)) {
		*always_flag = 0;
    }
    goto tableau(list);
}

void
show_result(int always_flag)
{
    if (always_flag == 1) {
		printf("[]~p is valid.\n");
    } else {
		printf("[]~p is not valid.\n");
    }
}