Mercurial > hg > CbC > old > DPP
view ltl.cbc @ 7:171cc032eb29
Fix tableau2
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 25 Dec 2015 18:31:20 +0900 |
parents | d4bc23cb728b |
children | cef74c1054c1 |
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"); } }