--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/tableau.cbc	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,114 @@
+#include <stdlib.h>
+#include "hoge.h"
+#include "task.h"
+#include "memory.h"
+#include "state_db.h"
+
+static code (*ret)(int);
+static void *env;
+
+static StateDB state_db;
+static MemoryPtr mem;
+static StateNode st;
+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);
+		memory_usage();
+		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++);
+    goto list->pkt->next(list->pkt, list);
+}
+
+code scheduler(PktPtr pkt, TaskPtr list)
+{
+    goto tableau(list);
+}
+
+code task_entry2(TaskPtr list)
+{
+    StateDB out;
+
+    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->pkt->next(list->pkt, list);
+}
+
+code task_entry1(PktPtr pkt)
+{
+    TaskPtr list = new_task(pkt);
+    if (!list) goto die("Can't allocate Task");
+    add_memory_range(list, sizeof(Task), &mem);
+    // make circular task list
+    list->next = list;
+
+    goto task_entry2(list);
+}
+
+code init_pkt()
+{
+    PktPtr pkt = (PktPtr)malloc(sizeof(Pkt));
+    if (!pkt) goto die("Can't allocate Pkt");
+    pkt->val = 1;
+    pkt->next = modulo;
+    add_memory_range(pkt, sizeof(Pkt), &mem);
+
+    goto task_entry1(pkt);
+}
+
+code die(char *err)
+{
+    printf("%s\n", err);
+    goto ret(1), env;
+}
+
+int main(void)
+{
+    ret = return;
+    env = environment;
+
+    goto init_pkt();
+}
+
+/* end */