--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tableau3.cbc	Wed Dec 16 15:16:11 2015 +0900
@@ -0,0 +1,301 @@
+/*
+** Dining Philosophers Problem's scheduler
+**    with state developper as a tableau method
+
+** 連絡先： 琉球大学情報工学科 河野 真治  
+** （E-Mail Address: kono@ie.u-ryukyu.ac.jp）
+**
+**    このソースのいかなる複写，改変，修正も許諾します。ただし、
+**    その際には、誰が貢献したを示すこの部分を残すこと。
+**    再配布や雑誌の付録などの問い合わせも必要ありません。
+**    営利利用も上記に反しない範囲で許可します。
+**    バイナリの配布の際にはversion messageを保存することを条件とします。
+**    このプログラムについては特に何の保証もしない、悪しからず。
+**
+**    Everyone is permitted to do anything on this program 
+**    including copying, modifying, improving,
+**    as long as you don't try to pretend that you wrote it.
+**    i.e., the above copyright notice has to appear in all copies.  
+**    Binary distribution requires original version messages.
+**    You don't have to ask before copying, redistribution or publishing.
+**    THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE.
+
+*/
+#include <stdlib.h>
+#include <time.h>
+#include "dpp2.h"
+#include "queue.h"
+#include "memory.h"
+#include "state_db.h"
+#include "ltl.h"
+
+int NUM_PHILOSOPHER = 5;    /* A number of philosophers must be more than 2. */
+
+static code (*ret)(int);
+static void *env;
+
+static PhilsPtr phils_list = NULL;
+
+static int max_step = 100;
+
+static StateDB state_db;
+static MemoryPtr mem;
+static StateNode st;
+static int always_flag;  // for LTL
+
+int
+list_length(TaskPtr list)
+{
+    int length;
+    TaskPtr t;
+
+    if (!list) return 0;
+    t = list->next;
+
+    for (length = 1; t && t != list; length++) {
+	t = t->next;
+    }
+    return length;
+}
+
+TaskPtr
+get_task(int num, TaskPtr list)
+{
+    while (num-- > 0) {
+	list = list->next;
+    }
+    return list;
+}
+
+
+static TaskIteratorPtr task_iter;
+static int depth,count;
+
+/*
+    Performe depth frist search
+    Possible task iterleave is generated by TaskIterator
+        (using task ring)
+    State are recorded in StateDB
+	all memory fragments are regsitered by add_memory_range()
+	including task queue
+ */
+
+
+code tableau(TaskPtr list)
+{
+    StateDB out;
+
+    st.hash = get_memory_hash(mem,0);
+    if (lookup_StateDB(&st, &state_db, &out)) {
+	// found in the state database
+	//printf("found %d\n",count);
+	while(!(list = next_task_iterator(task_iter))) {
+	    // no more branch, go back to the previous one
+	    TaskIteratorPtr prev_iter = task_iter->prev;
+	    if (!prev_iter) {
+		printf("All done count %d\n",count);
+		printf("Number of unique states %d\n", state_count());
+		memory_usage();
+		show_result(always_flag);
+		goto ret(0),env;
+	    }
+	    //printf("no more branch %d\n",count);
+	    depth--;
+	    free_task_iterator(task_iter);
+	    task_iter = prev_iter;
+	}
+	// return to previous state
+	//    here we assume task list is fixed, we don't have to
+	//    recover task list itself
+	restore_memory(task_iter->state->memory);
+	//printf("restore list %x next %x\n",(int)list,(int)(list->next));
+    } else {
+	// one step further
+	depth++;
+	task_iter = create_task_iterator(list,out,task_iter);
+    }
+    //printf("depth %d count %d\n", depth, count++);
+    count++;
+    goto list->phils->next(list->phils,list);
+}
+
+code get_next_task_fifo(TaskPtr list)
+{
+    TaskPtr t = list;
+    TaskPtr e;
+
+    if (max_step--<0) goto die("Simuration end.");
+
+    list = list->next;
+    goto list->phils->next(list->phils,list);
+}
+
+code scheduler(PhilsPtr phils, TaskPtr list)
+{
+    goto check(&always_flag, phils, list);
+    // goto next_next_task_fifo(list);
+}
+
+code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last);
+
+code task_entry2(int count,PhilsPtr self, TaskPtr list,TaskPtr last, TaskPtr q)
+{
+    if (!q) {
+	goto die("Can't allocate Task\n");
+    } else {
+	add_memory_range(q,sizeof(Task),&mem);
+	goto enqueue(count, self, list, last, q, task_entry1);
+    }
+}
+
+code task_entry1(int count, PhilsPtr self, TaskPtr list, TaskPtr last)
+{
+    StateDB out;
+    /*
+    printf("int count %d, PhilsPtr self %x, TaskPtr list %x, TaskPtr last %x\n",
+	count, self, list, last);
+    */
+
+    if (count++ < NUM_PHILOSOPHER) {
+	self = self->left;
+	goto create_queue(count,self,list,last,task_entry2);
+    } else {
+	// make circular task list
+	last->next = list;
+	st.memory = mem;
+	st.hash = get_memory_hash(mem,0);
+	lookup_StateDB(&st, &state_db, &out);
+	task_iter = create_task_iterator(list,out,0);
+	// start first task
+	goto list->phils->next(list->phils,list);
+    }
+}
+
+code task_entry0(int count, PhilsPtr self, TaskPtr list, TaskPtr last, TaskPtr q)
+{
+    add_memory_range(q,sizeof(Task),&mem);
+    goto task_entry1(count, self, q, q);
+}
+
+code init_final(PhilsPtr self)
+{
+    self->right = phils_list;
+    phils_list->left = self;
+    self->right_fork = phils_list->left_fork;
+    always_flag = 1;
+    //add_memory_range(&always_flag, sizeof(int), &mem);
+    //printf("init all\n");
+
+    goto create_queue(1, self, 0, 0, task_entry0);
+}
+
+code init_phils2(PhilsPtr self, int count, int id)
+{
+    PhilsPtr tmp_self;
+
+    tmp_self = (PhilsPtr)malloc(sizeof(Phils));
+    if (!tmp_self) {
+	goto die("Can't allocate Phils\n");
+    }
+    self->right = tmp_self;
+    tmp_self->id = id;
+    tmp_self->right_fork = NULL;
+    tmp_self->left_fork = self->right_fork;
+    tmp_self->right = NULL;
+    tmp_self->left = self;
+    tmp_self->next = pickup_lfork;
+    add_memory_range(tmp_self,sizeof(Phils),&mem);
+
+    count--;
+    id++;
+
+    if (count == 0) {
+	goto init_final(tmp_self);
+    } else {
+	goto init_fork2(tmp_self, count, id);
+    }
+}
+
+code init_fork2(PhilsPtr self, int count, int id)
+{
+    ForkPtr tmp_fork;
+
+    tmp_fork = (ForkPtr)malloc(sizeof(Fork));
+    if (!tmp_fork) {
+	goto die("Can't allocate Fork\n");
+    }
+    tmp_fork->id = id;
+    tmp_fork->owner = NULL;
+    self->right_fork = tmp_fork;
+    add_memory_range(tmp_fork,sizeof(Fork),&mem);
+
+    goto init_phils2(self, count, id);
+}
+
+code init_phils1(ForkPtr fork, int count, int id)
+{
+    PhilsPtr self;
+
+    self = (PhilsPtr)malloc(sizeof(Phils));
+    if (!self) {
+	goto die("Can't allocate Phils\n");
+    }
+    phils_list = self;
+    self->id = id;
+    self->right_fork = NULL;
+    self->left_fork = fork;
+    self->right = NULL;
+    self->left = NULL;
+    self->next = pickup_lfork;
+    add_memory_range(self,sizeof(Phils),&mem);
+
+    count--;
+    id++;
+
+    goto init_fork2(self, count, id);
+}
+
+code init_fork1(int count)
+{
+    ForkPtr fork;
+    int id = 1;
+
+    fork = (ForkPtr)malloc(sizeof(Fork));
+    if (!fork) {
+	goto die("Can't allocate Fork\n");
+    }
+    fork->id = id;
+    fork->owner = NULL;
+    add_memory_range(fork,sizeof(Fork),&mem);
+
+    goto init_phils1(fork, count, id);
+}
+
+code die(char *err)
+{
+    printf("%s\n", err);
+    goto ret(1), env;
+}
+
+int main(int ac, char *av[])
+{
+    ret = return;
+    env = environment;
+    // srand((unsigned)time(NULL));
+    // srandom((unsigned long)time(NULL));
+    reset_state_count();
+    srandom(555);
+
+    if (ac==2) {
+	NUM_PHILOSOPHER = atoi(av[1]);
+	if (NUM_PHILOSOPHER >10 ||NUM_PHILOSOPHER < 2) {
+	    printf("illegal number of philosopher = %d\n", NUM_PHILOSOPHER );
+	    return 1; 
+	}
+	//printf("number of philosopher = %d\n", NUM_PHILOSOPHER );
+    }
+
+    goto init_fork1(NUM_PHILOSOPHER);
+}
+
+/* end */