view temporal_logic/tableau.cbc @ 10:972515f10c1d draft

add some files
author Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
date Sun, 03 Jun 2012 22:09:13 +0900
parents
children
line wrap: on
line source

#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 */