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