Mercurial > hg > Members > nobuyasu > CbC

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

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add some files
author Nobuyasu Oshiro <dimolto@cr.ie.u-ryukyu.ac.jp>
date Sun, 03 Jun 2012 22:09:13 +0900
parents
children
comparison
equal deleted inserted replaced
9:18d2a590bc10 10:972515f10c1d
1 #include <stdlib.h>
2 #include "hoge.h"
3 #include "task.h"
4 #include "memory.h"
5 #include "state_db.h"
6
7 static code (*ret)(int);
8 static void *env;
9
10 static StateDB state_db;
11 static MemoryPtr mem;
12 static StateNode st;
13 static TaskIteratorPtr task_iter;
14 static int depth,count;
15
16 /*
17 Performe depth frist search
18 Possible task iterleave is generated by TaskIterator
19 (using task ring)
20 State are recorded in StateDB
21 all memory fragments are regsitered by add_memory_range()
22 including task queue
23 */
24
25
26 code tableau(TaskPtr list)
27 {
28 StateDB out;
29
30 st.hash = get_memory_hash(mem,0);
31 if (lookup_StateDB(&st, &state_db, &out)) {
32 // found in the state database
33 printf("found %d\n",count);
34 while(!(list = next_task_iterator(task_iter))) {
35 // no more branch, go back to the previous one
36 TaskIteratorPtr prev_iter = task_iter->prev;
37 if (!prev_iter) {
38 printf("All done count %d\n",count);
39 memory_usage();
40 goto ret(0),env;
41 }
42 printf("no more branch %d\n",count);
43 depth--;
44 free_task_iterator(task_iter);
45 task_iter = prev_iter;
46 }
47 // return to previous state
48 // here we assume task list is fixed, we don't have to
49 // recover task list itself
50 restore_memory(task_iter->state->memory);
51 printf("restore list %x next %x\n",(int)list,(int)(list->next));
52 } else {
53 // one step further
54 depth++;
55 task_iter = create_task_iterator(list,out,task_iter);
56 }
57 printf("depth %d count %d\n", depth, count++);
58 goto list->pkt->next(list->pkt, list);
59 }
60
61 code scheduler(PktPtr pkt, TaskPtr list)
62 {
63 goto tableau(list);
64 }
65
66 code task_entry2(TaskPtr list)
67 {
68 StateDB out;
69
70 st.memory = mem;
71 st.hash = get_memory_hash(mem, 0);
72 lookup_StateDB(&st, &state_db, &out);
73 task_iter = create_task_iterator(list, out, 0);
74 // start first task
75 goto list->pkt->next(list->pkt, list);
76 }
77
78 code task_entry1(PktPtr pkt)
79 {
80 TaskPtr list = new_task(pkt);
81 if (!list) goto die("Can't allocate Task");
82 add_memory_range(list, sizeof(Task), &mem);
83 // make circular task list
84 list->next = list;
85
86 goto task_entry2(list);
87 }
88
89 code init_pkt()
90 {
91 PktPtr pkt = (PktPtr)malloc(sizeof(Pkt));
92 if (!pkt) goto die("Can't allocate Pkt");
93 pkt->val = 1;
94 pkt->next = modulo;
95 add_memory_range(pkt, sizeof(Pkt), &mem);
96
97 goto task_entry1(pkt);
98 }
99
100 code die(char *err)
101 {
102 printf("%s\n", err);
103 goto ret(1), env;
104 }
105
106 int main(void)
107 {
108 ret = return;
109 env = environment;
110
111 goto init_pkt();
112 }
113
114 /* end */