view ltl.cbc @ 1:2874954d97b2

Fix dpp for cbc using LLVM 3.7
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 16 Dec 2015 16:52:16 +0900
parents d4bc23cb728b
children 171cc032eb29
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");
    }
}