Mercurial > hg > Members > nobuyasu > CbC

changeset 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 18d2a590bc10
children bdf156058529
files ABP/Makefile.mc make_headers.py2 temporal_logic/Makefile temporal_logic/Makefile.mc temporal_logic/crc32.c temporal_logic/crc32.h temporal_logic/fomula.cbc temporal_logic/fomula.h temporal_logic/hoge.cbc temporal_logic/hoge.h temporal_logic/ltl.cbc temporal_logic/memory.c temporal_logic/memory.h temporal_logic/state_db.c temporal_logic/state_db.h temporal_logic/tableau.cbc temporal_logic/task.c temporal_logic/task.h
diffstat 18 files changed, 1406 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ABP/Makefile.mc	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,34 @@
+#CC=gcc
+#MCC=mcc
+CC=cbc-gcc-4.6.0
+MCC=cbc-gcc-4.6.0
+TARGET=abp abp2 sender2 sender3 receiver2
+MCCFLAGS=-s
+CFLAGS=-g -Wall
+
+.SUFFIXES:	.c .o
+
+.c.o:
+	$(MCC) $(MCCFLAGS) $<
+	$(CC) $(CFLAGS) -o $@ -c $(<:.c=.s)
+
+all: $(TARGET)
+
+abp: sender.o receiver.o scheduler.o
+	$(CC) -o $@ $^
+
+abp2: queue.o sender3.o receiver3.o scheduler2.o
+	$(CC) -o $@ $^
+
+sender2: sender2.o
+	$(CC) -o $@ $^
+
+sender3: sender3.o
+	$(CC) -o $@ $^
+
+receiver2: receiver2.o
+	$(CC) -o $@ $^
+
+clean:
+	$(RM) $(TARGET)
+	$(RM) *.s *.o
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/make_headers.py2	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,126 @@
+#!/usr/bin/env python
+# -*- coding: utf-8 -*-
+
+import sys
+import re
+import getopt
+
+reserved_words = [ "if", "for", "switch", "return", "while", "else", ]
+
+PATTERN = r"([a-zA-Z_][\w\s]*\**)\s([a-zA-Z_]\w*)\s*\(([^\{/;]*)\)\s*\{"
+#PATTERN = r"([a-zA-Z_]\w*)\s+([a-zA-Z_]\w*)\s*\(([^;]*)\)\s*\{"
+#PATTERN = r"((?:[a-zA-Z_]\w*)\s+)+?([a-zA-Z_]\w*)\s*\(([^;]*)\)\s*\{"
+# TODO: 関数パラメータ内にコメントがあると正しく動かない!
+PROG = re.compile(PATTERN, re.S)
+
+omit_static=False
+add_extern=""
+
+def truncate_comments(data):
+	pass
+
+def check_reserved_word(decl):
+	""" return true if decl's type and name is not reserved word. """
+
+	if decl["name"] in reserved_words or decl["type"] in reserved_words:
+		return False
+	return True
+
+def read_decls(file):
+	declarators = []
+
+	# open the file and read all lines into a string.
+	try:
+		fo = open(file, 'r')
+		lines = fo.readlines()
+		data = "".join(lines)
+		truncate_comments(data)
+	except IOError:
+		print "cannot read file %s" % file
+		return None
+
+	# find all matched strings.
+	# moiter is iterator of MatchObject.
+	moiter = PROG.finditer(data)
+	for mo in moiter:
+		tmp = { "type": mo.group(1),
+				"name": mo.group(2),
+				"parms": mo.group(3),
+				"offset": mo.start() }
+		if check_reserved_word(tmp):
+			declarators.append(tmp)
+
+	return declarators
+
+def debug_print(decl):
+	for (key,value) in decl.items():
+		if isinstance(value, str):
+			decl[key] = value.replace("\n"," ").replace("\t"," ")
+
+	print "Type:\t%s" % decl["type"]
+	print "Name:\t%s" % decl["name"]
+	print "Params:\t%s" % decl["parms"]
+	print "offset:\t%d" % decl["offset"]
+	print ""
+	#s = "%s %s ( %s );" % (decl["type"], decl["name"], decl["parms"])
+	#print s, "/* offset: %d */" % decl["offset"]
+
+def format_print(decl, file):
+	for (key,value) in decl.items():
+		if isinstance(value, str):
+			decl[key] = value.replace("\n"," ").replace("\t"," ")
+
+	print "/* defined in file %s at offset %d  */" % (file,decl["offset"])
+	print "%s%s %s (%s);" % (add_extern, decl["type"],decl["name"],decl["parms"])
+	print ""
+
+def getoptions():
+	global omit_static, add_extern
+
+	try:
+		opts, args = getopt.getopt(sys.argv[1:], 'se', [ 'omit-static', 'add-extern' ])
+	except getopt.GetoptError:
+		print(err)
+		usage()
+		sys.exit(2)
+
+	for opt,a in opts:
+		if opt in ("-s", "--omit-static"):
+			omit_static=True
+		elif opt in ("-e", "--add-extern"):
+			add_extern="extern "
+		else:
+			print("unhandled option {0}".format(opt))
+			usage()
+	
+	return args
+
+def usage():
+	print( """\
+Usage: {0:s} OPION... [FILE]...
+OPTIONS:
+	-s, --omit-static	omit static functions
+	-e, --add-extern	add extern to all function declarations
+	""".format(sys.argv[0]))
+
+def main():
+	# option handling.
+	args = getoptions()
+
+	for file in args:
+		# read function declaration from each file.
+		decls = read_decls(file)
+		if decls==None or len(decls)==0:
+			# no function found.
+			print "%s have no function definition!" % file
+			continue
+
+		for decl in decls:
+			if omit_static and 0 <= decl["type"].find("static"):
+				# static function is ignored.
+				continue
+			#debug_print(decl)
+			format_print(decl, file)
+
+main()
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/Makefile	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,99 @@
+CC=cbc-gcc-4.6.0
+#MCC=mcc
+MCC=~/hg/CbC/device/mc-ia32
+TARGET=tableau ltl
+#MCCFLAGS=-s
+CFLAGS=-I. -g -O0 -Wall
+
+
+.SUFFIXES:	.cbc .c .o
+
+.cbc.o:
+	$(CC) $(CFLAGS) -S $<
+	$(CC) $(CFLAGS) -o $@ -c $(<:.cbc=.s)
+
+all: $(TARGET)
+
+# tableau expansion 
+tableau: hoge.o task.o tableau.o memory.o state_db.o crc32.o
+	$(CC) $(CFLAGS) -o $@ $^
+
+# tableau expansion with linear temporal logic
+ltl: hoge.o task.o fomula.o ltl.o memory.o state_db.o crc32.o
+	$(CC) $(CFLAGS) -o $@ $^
+
+clean:
+	$(RM) -f $(TARGET)
+	$(RM) -f *.s *.o
+
+depend:
+	makedepend *.cbc *.[hc]
+# DO NOT DELETE
+
+#fomula.o: /usr/include/stdio.h /usr/include/_types.h
+#fomula.o: /usr/include/sys/_types.h /usr/include/sys/cdefs.h
+#fomula.o: /usr/include/machine/_types.h /usr/include/ppc/_types.h fomula.h
+#fomula.o: task.h state_db.h hoge.h
+#hoge.o: /usr/include/stdio.h /usr/include/_types.h /usr/include/sys/_types.h
+#hoge.o: /usr/include/sys/cdefs.h /usr/include/machine/_types.h
+#hoge.o: /usr/include/ppc/_types.h hoge.h task.h state_db.h
+#ltl.o: /usr/include/stdlib.h /usr/include/sys/cdefs.h /usr/include/_types.h
+#ltl.o: /usr/include/sys/_types.h /usr/include/machine/_types.h
+#ltl.o: /usr/include/ppc/_types.h /usr/include/sys/wait.h
+#ltl.o: /usr/include/sys/signal.h /usr/include/sys/appleapiopts.h
+#ltl.o: /usr/include/machine/signal.h /usr/include/ppc/signal.h
+#ltl.o: /usr/include/sys/resource.h /usr/include/machine/endian.h
+#ltl.o: /usr/include/ppc/endian.h /usr/include/sys/_endian.h
+#ltl.o: /usr/include/stdint.h /usr/include/libkern/OSByteOrder.h
+#ltl.o: /usr/include/libkern/ppc/OSByteOrder.h /usr/include/alloca.h
+#ltl.o: /usr/include/machine/types.h /usr/include/ppc/types.h hoge.h task.h
+#ltl.o: state_db.h memory.h fomula.h
+#tableau.o: /usr/include/stdlib.h /usr/include/sys/cdefs.h
+#tableau.o: /usr/include/_types.h /usr/include/sys/_types.h
+#tableau.o: /usr/include/machine/_types.h /usr/include/ppc/_types.h
+#tableau.o: /usr/include/sys/wait.h /usr/include/sys/signal.h
+#tableau.o: /usr/include/sys/appleapiopts.h /usr/include/machine/signal.h
+#tableau.o: /usr/include/ppc/signal.h /usr/include/sys/resource.h
+#tableau.o: /usr/include/machine/endian.h /usr/include/ppc/endian.h
+#tableau.o: /usr/include/sys/_endian.h /usr/include/stdint.h
+#tableau.o: /usr/include/libkern/OSByteOrder.h
+#tableau.o: /usr/include/libkern/ppc/OSByteOrder.h /usr/include/alloca.h
+#tableau.o: /usr/include/machine/types.h /usr/include/ppc/types.h hoge.h
+#tableau.o: task.h state_db.h memory.h
+#memory.o: /usr/include/stdio.h /usr/include/_types.h
+#memory.o: /usr/include/sys/_types.h /usr/include/sys/cdefs.h
+#memory.o: /usr/include/machine/_types.h /usr/include/ppc/_types.h
+#memory.o: /usr/include/stdlib.h /usr/include/sys/wait.h
+#memory.o: /usr/include/sys/signal.h /usr/include/sys/appleapiopts.h
+#memory.o: /usr/include/machine/signal.h /usr/include/ppc/signal.h
+#memory.o: /usr/include/sys/resource.h /usr/include/machine/endian.h
+#memory.o: /usr/include/ppc/endian.h /usr/include/sys/_endian.h
+#memory.o: /usr/include/stdint.h /usr/include/libkern/OSByteOrder.h
+#memory.o: /usr/include/libkern/ppc/OSByteOrder.h /usr/include/alloca.h
+#memory.o: /usr/include/machine/types.h /usr/include/ppc/types.h memory.h
+#memory.o: crc32.h /usr/include/string.h
+#state_db.o: /usr/include/stdlib.h /usr/include/sys/cdefs.h
+#state_db.o: /usr/include/_types.h /usr/include/sys/_types.h
+#state_db.o: /usr/include/machine/_types.h /usr/include/ppc/_types.h
+#state_db.o: /usr/include/sys/wait.h /usr/include/sys/signal.h
+#state_db.o: /usr/include/sys/appleapiopts.h /usr/include/machine/signal.h
+#state_db.o: /usr/include/ppc/signal.h /usr/include/sys/resource.h
+#state_db.o: /usr/include/machine/endian.h /usr/include/ppc/endian.h
+#state_db.o: /usr/include/sys/_endian.h /usr/include/stdint.h
+#state_db.o: /usr/include/libkern/OSByteOrder.h
+#state_db.o: /usr/include/libkern/ppc/OSByteOrder.h /usr/include/alloca.h
+#state_db.o: /usr/include/machine/types.h /usr/include/ppc/types.h state_db.h
+#state_db.o: memory.h
+#task.o: /usr/include/stdio.h /usr/include/_types.h /usr/include/sys/_types.h
+#task.o: /usr/include/sys/cdefs.h /usr/include/machine/_types.h
+#task.o: /usr/include/ppc/_types.h /usr/include/stdlib.h
+#task.o: /usr/include/sys/wait.h /usr/include/sys/signal.h
+#task.o: /usr/include/sys/appleapiopts.h /usr/include/machine/signal.h
+#task.o: /usr/include/ppc/signal.h /usr/include/sys/resource.h
+#task.o: /usr/include/machine/endian.h /usr/include/ppc/endian.h
+#task.o: /usr/include/sys/_endian.h /usr/include/stdint.h
+#task.o: /usr/include/libkern/OSByteOrder.h
+#task.o: /usr/include/libkern/ppc/OSByteOrder.h /usr/include/alloca.h
+#task.o: /usr/include/machine/types.h /usr/include/ppc/types.h task.h
+#task.o: state_db.h
+#task.o: state_db.h
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/Makefile.mc	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,98 @@
+CC=cbc-gcc-4.6.0
+#MCC=mcc
+MCC=/Users/aotokage/hg/CbC/device/mc-ia32
+TARGET=tableau ltl
+MCCFLAGS=-s
+CFLAGS=-I. -g -Wall
+
+.SUFFIXES:	.cbc .c .o
+
+.cbc.o:
+	$(MCC) $(MCCFLAGS) $<
+	$(CC) $(CFLAGS) -o $@ -c $(<:.cbc=.s)
+
+all: $(TARGET)
+
+# tableau expansion 
+tableau: hoge.o task.o tableau.o memory.o state_db.o crc32.o
+	$(CC) $(CFLAGS) -o $@ $^
+
+# tableau expansion with linear temporal logic
+ltl: hoge.o task.o fomula.o ltl.o memory.o state_db.o crc32.o
+	$(CC) $(CFLAGS) -o $@ $^
+
+clean:
+	$(RM) -f $(TARGET)
+	$(RM) -f *.s *.o
+
+depend:
+	makedepend *.cbc *.[hc]
+# DO NOT DELETE
+
+fomula.o: /usr/include/stdio.h /usr/include/_types.h
+fomula.o: /usr/include/sys/_types.h /usr/include/sys/cdefs.h
+fomula.o: /usr/include/machine/_types.h /usr/include/ppc/_types.h fomula.h
+fomula.o: task.h state_db.h hoge.h
+hoge.o: /usr/include/stdio.h /usr/include/_types.h /usr/include/sys/_types.h
+hoge.o: /usr/include/sys/cdefs.h /usr/include/machine/_types.h
+hoge.o: /usr/include/ppc/_types.h hoge.h task.h state_db.h
+ltl.o: /usr/include/stdlib.h /usr/include/sys/cdefs.h /usr/include/_types.h
+ltl.o: /usr/include/sys/_types.h /usr/include/machine/_types.h
+ltl.o: /usr/include/ppc/_types.h /usr/include/sys/wait.h
+ltl.o: /usr/include/sys/signal.h /usr/include/sys/appleapiopts.h
+ltl.o: /usr/include/machine/signal.h /usr/include/ppc/signal.h
+ltl.o: /usr/include/sys/resource.h /usr/include/machine/endian.h
+ltl.o: /usr/include/ppc/endian.h /usr/include/sys/_endian.h
+ltl.o: /usr/include/stdint.h /usr/include/libkern/OSByteOrder.h
+ltl.o: /usr/include/libkern/ppc/OSByteOrder.h /usr/include/alloca.h
+ltl.o: /usr/include/machine/types.h /usr/include/ppc/types.h hoge.h task.h
+ltl.o: state_db.h memory.h fomula.h
+tableau.o: /usr/include/stdlib.h /usr/include/sys/cdefs.h
+tableau.o: /usr/include/_types.h /usr/include/sys/_types.h
+tableau.o: /usr/include/machine/_types.h /usr/include/ppc/_types.h
+tableau.o: /usr/include/sys/wait.h /usr/include/sys/signal.h
+tableau.o: /usr/include/sys/appleapiopts.h /usr/include/machine/signal.h
+tableau.o: /usr/include/ppc/signal.h /usr/include/sys/resource.h
+tableau.o: /usr/include/machine/endian.h /usr/include/ppc/endian.h
+tableau.o: /usr/include/sys/_endian.h /usr/include/stdint.h
+tableau.o: /usr/include/libkern/OSByteOrder.h
+tableau.o: /usr/include/libkern/ppc/OSByteOrder.h /usr/include/alloca.h
+tableau.o: /usr/include/machine/types.h /usr/include/ppc/types.h hoge.h
+tableau.o: task.h state_db.h memory.h
+memory.o: /usr/include/stdio.h /usr/include/_types.h
+memory.o: /usr/include/sys/_types.h /usr/include/sys/cdefs.h
+memory.o: /usr/include/machine/_types.h /usr/include/ppc/_types.h
+memory.o: /usr/include/stdlib.h /usr/include/sys/wait.h
+memory.o: /usr/include/sys/signal.h /usr/include/sys/appleapiopts.h
+memory.o: /usr/include/machine/signal.h /usr/include/ppc/signal.h
+memory.o: /usr/include/sys/resource.h /usr/include/machine/endian.h
+memory.o: /usr/include/ppc/endian.h /usr/include/sys/_endian.h
+memory.o: /usr/include/stdint.h /usr/include/libkern/OSByteOrder.h
+memory.o: /usr/include/libkern/ppc/OSByteOrder.h /usr/include/alloca.h
+memory.o: /usr/include/machine/types.h /usr/include/ppc/types.h memory.h
+memory.o: crc32.h /usr/include/string.h
+state_db.o: /usr/include/stdlib.h /usr/include/sys/cdefs.h
+state_db.o: /usr/include/_types.h /usr/include/sys/_types.h
+state_db.o: /usr/include/machine/_types.h /usr/include/ppc/_types.h
+state_db.o: /usr/include/sys/wait.h /usr/include/sys/signal.h
+state_db.o: /usr/include/sys/appleapiopts.h /usr/include/machine/signal.h
+state_db.o: /usr/include/ppc/signal.h /usr/include/sys/resource.h
+state_db.o: /usr/include/machine/endian.h /usr/include/ppc/endian.h
+state_db.o: /usr/include/sys/_endian.h /usr/include/stdint.h
+state_db.o: /usr/include/libkern/OSByteOrder.h
+state_db.o: /usr/include/libkern/ppc/OSByteOrder.h /usr/include/alloca.h
+state_db.o: /usr/include/machine/types.h /usr/include/ppc/types.h state_db.h
+state_db.o: memory.h
+task.o: /usr/include/stdio.h /usr/include/_types.h /usr/include/sys/_types.h
+task.o: /usr/include/sys/cdefs.h /usr/include/machine/_types.h
+task.o: /usr/include/ppc/_types.h /usr/include/stdlib.h
+task.o: /usr/include/sys/wait.h /usr/include/sys/signal.h
+task.o: /usr/include/sys/appleapiopts.h /usr/include/machine/signal.h
+task.o: /usr/include/ppc/signal.h /usr/include/sys/resource.h
+task.o: /usr/include/machine/endian.h /usr/include/ppc/endian.h
+task.o: /usr/include/sys/_endian.h /usr/include/stdint.h
+task.o: /usr/include/libkern/OSByteOrder.h
+task.o: /usr/include/libkern/ppc/OSByteOrder.h /usr/include/alloca.h
+task.o: /usr/include/machine/types.h /usr/include/ppc/types.h task.h
+task.o: state_db.h
+task.o: state_db.h
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/crc32.c	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,80 @@
+/*
+    $Id: crc32.c,v 1.1.1.1 2007-01-23 10:38:45 atsuki Exp $
+    Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+       based on open source CRCtextDlg.cpp Richard A. Ellingson
+
+    This is generated by Perl, do not edit this. Edit Perl script.
+ */
+
+static unsigned crc32_table[256] = {
+	0x00000000,0x04c11db7,0x09823b6e,0x0d4326d9,0x130476dc,0x17c56b6b,
+	0x1a864db2,0x1e475005,0x2608edb8,0x22c9f00f,0x2f8ad6d6,0x2b4bcb61,
+	0x350c9b64,0x31cd86d3,0x3c8ea00a,0x384fbdbd,0x4c11db70,0x48d0c6c7,
+	0x4593e01e,0x4152fda9,0x5f15adac,0x5bd4b01b,0x569796c2,0x52568b75,
+	0x6a1936c8,0x6ed82b7f,0x639b0da6,0x675a1011,0x791d4014,0x7ddc5da3,
+	0x709f7b7a,0x745e66cd,0x9823b6e0,0x9ce2ab57,0x91a18d8e,0x95609039,
+	0x8b27c03c,0x8fe6dd8b,0x82a5fb52,0x8664e6e5,0xbe2b5b58,0xbaea46ef,
+	0xb7a96036,0xb3687d81,0xad2f2d84,0xa9ee3033,0xa4ad16ea,0xa06c0b5d,
+	0xd4326d90,0xd0f37027,0xddb056fe,0xd9714b49,0xc7361b4c,0xc3f706fb,
+	0xceb42022,0xca753d95,0xf23a8028,0xf6fb9d9f,0xfbb8bb46,0xff79a6f1,
+	0xe13ef6f4,0xe5ffeb43,0xe8bccd9a,0xec7dd02d,0x34867077,0x30476dc0,
+	0x3d044b19,0x39c556ae,0x278206ab,0x23431b1c,0x2e003dc5,0x2ac12072,
+	0x128e9dcf,0x164f8078,0x1b0ca6a1,0x1fcdbb16,0x018aeb13,0x054bf6a4,
+	0x0808d07d,0x0cc9cdca,0x7897ab07,0x7c56b6b0,0x71159069,0x75d48dde,
+	0x6b93dddb,0x6f52c06c,0x6211e6b5,0x66d0fb02,0x5e9f46bf,0x5a5e5b08,
+	0x571d7dd1,0x53dc6066,0x4d9b3063,0x495a2dd4,0x44190b0d,0x40d816ba,
+	0xaca5c697,0xa864db20,0xa527fdf9,0xa1e6e04e,0xbfa1b04b,0xbb60adfc,
+	0xb6238b25,0xb2e29692,0x8aad2b2f,0x8e6c3698,0x832f1041,0x87ee0df6,
+	0x99a95df3,0x9d684044,0x902b669d,0x94ea7b2a,0xe0b41de7,0xe4750050,
+	0xe9362689,0xedf73b3e,0xf3b06b3b,0xf771768c,0xfa325055,0xfef34de2,
+	0xc6bcf05f,0xc27dede8,0xcf3ecb31,0xcbffd686,0xd5b88683,0xd1799b34,
+	0xdc3abded,0xd8fba05a,0x690ce0ee,0x6dcdfd59,0x608edb80,0x644fc637,
+	0x7a089632,0x7ec98b85,0x738aad5c,0x774bb0eb,0x4f040d56,0x4bc510e1,
+	0x46863638,0x42472b8f,0x5c007b8a,0x58c1663d,0x558240e4,0x51435d53,
+	0x251d3b9e,0x21dc2629,0x2c9f00f0,0x285e1d47,0x36194d42,0x32d850f5,
+	0x3f9b762c,0x3b5a6b9b,0x0315d626,0x07d4cb91,0x0a97ed48,0x0e56f0ff,
+	0x1011a0fa,0x14d0bd4d,0x19939b94,0x1d528623,0xf12f560e,0xf5ee4bb9,
+	0xf8ad6d60,0xfc6c70d7,0xe22b20d2,0xe6ea3d65,0xeba91bbc,0xef68060b,
+	0xd727bbb6,0xd3e6a601,0xdea580d8,0xda649d6f,0xc423cd6a,0xc0e2d0dd,
+	0xcda1f604,0xc960ebb3,0xbd3e8d7e,0xb9ff90c9,0xb4bcb610,0xb07daba7,
+	0xae3afba2,0xaafbe615,0xa7b8c0cc,0xa379dd7b,0x9b3660c6,0x9ff77d71,
+	0x92b45ba8,0x9675461f,0x8832161a,0x8cf30bad,0x81b02d74,0x857130c3,
+	0x5d8a9099,0x594b8d2e,0x5408abf7,0x50c9b640,0x4e8ee645,0x4a4ffbf2,
+	0x470cdd2b,0x43cdc09c,0x7b827d21,0x7f436096,0x7200464f,0x76c15bf8,
+	0x68860bfd,0x6c47164a,0x61043093,0x65c52d24,0x119b4be9,0x155a565e,
+	0x18197087,0x1cd86d30,0x029f3d35,0x065e2082,0x0b1d065b,0x0fdc1bec,
+	0x3793a651,0x3352bbe6,0x3e119d3f,0x3ad08088,0x2497d08d,0x2056cd3a,
+	0x2d15ebe3,0x29d4f654,0xc5a92679,0xc1683bce,0xcc2b1d17,0xc8ea00a0,
+	0xd6ad50a5,0xd26c4d12,0xdf2f6bcb,0xdbee767c,0xe3a1cbc1,0xe760d676,
+	0xea23f0af,0xeee2ed18,0xf0a5bd1d,0xf464a0aa,0xf9278673,0xfde69bc4,
+	0x89b8fd09,0x8d79e0be,0x803ac667,0x84fbdbd0,0x9abc8bd5,0x9e7d9662,
+	0x933eb0bb,0x97ffad0c,0xafb010b1,0xab710d06,0xa6322bdf,0xa2f33668,
+	0xbcb4666d,0xb8757bda,0xb5365d03,0xb1f740b4
+};
+
+
+
+// Once the lookup table has been filled in by the two functions above,
+// this function creates all CRCs using only the lookup table.
+
+int Get_CRC(unsigned char *buffer,int len)
+{
+    // Be sure to use unsigned variables,
+    // because negative values introduce high bits
+    // where zero bits are required.
+    // Start out with all bits set high.
+
+    unsigned  ulCRC = 0xffffffff;
+
+    // Perform the algorithm on each character
+    // in the string, using the lookup table values.
+
+    while(len-->0) {
+	ulCRC = (ulCRC >> 8) ^ crc32_table[(ulCRC & 0xFF) ^ *buffer++];
+    }
+    // Exclusive OR the result with the beginning value.
+    return ulCRC ^ 0xffffffff;
+}
+
+// ******* End custom code *******
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/crc32.h	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,8 @@
+/*
+    $Id: crc32.h,v 1.1.1.1 2007-01-23 10:38:45 atsuki Exp $
+    Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+       based on open source
+ */
+
+extern int Get_CRC(unsigned char *buffer,int len);
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/fomula.cbc	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,27 @@
+#include <stdio.h>
+#include "fomula.h"
+#include "task.h"
+#include "hoge.h"
+
+code check(int *flag, int *always_flag, PktPtr pkt, TaskPtr list)
+{
+    if (pkt->val <= 10) {
+	*flag = 1;
+    } else {
+	*flag = 0;
+	*always_flag = 0;
+    }
+
+    goto tableau(list);
+}
+
+void show_result(int always_flag)
+{
+    if (always_flag == 1) {
+	printf("[]p: valid.\n");
+    } else {
+	printf("[]p: not valid.\n");
+    }
+}
+
+/* EOF */
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/fomula.h	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,10 @@
+#ifndef _FOMULA_H_
+#define _FOMULA_H_
+
+extern code
+check(int *flag, int *always_flag, struct packet *pkt, struct task *list);
+
+extern void
+show_result(int always_flag);
+
+#endif
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/hoge.cbc	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,20 @@
+#include <stdio.h>
+#include "hoge.h"
+#include "task.h"
+
+code increment(PktPtr pkt, TaskPtr current_task)
+{
+    pkt->val++;
+    printf("inc: %d\n", pkt->val);
+    pkt->next = modulo;
+    goto scheduler(pkt, current_task);
+}
+
+code modulo(PktPtr pkt, TaskPtr current_task)
+{
+    // pkt->val %= 10;
+    pkt->val = pkt->val % 10;
+    printf("mod: %d\n", pkt->val);
+    pkt->next = increment;
+    goto scheduler(pkt, current_task);
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/hoge.h	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,12 @@
+#ifndef _HOGE_H_
+#define _HOGE_H_
+
+typedef struct packet {
+    int val;
+    code (*next)(struct packet *, struct task *);
+} Pkt, *PktPtr;
+
+extern code modulo(PktPtr pkt, struct task *current_task);
+extern code increment(PktPtr pkt, struct task *current_task);
+
+#endif
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/ltl.cbc	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,122 @@
+#include <stdlib.h>
+#include "hoge.h"
+#include "task.h"
+#include "memory.h"
+#include "state_db.h"
+#include "fomula.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;
+static int flag;  // for ltl
+static int always_flag;  // for ltl
+
+/*
+    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();
+		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++);
+    goto list->pkt->next(list->pkt, list);
+}
+
+code scheduler(PktPtr pkt, TaskPtr list)
+{
+    goto check(&flag, &always_flag, pkt, 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()
+{
+    PktPtr pkt = (PktPtr)malloc(sizeof(Pkt));
+    if (!pkt) goto die("Can't allocate Pkt");
+    flag = 1;
+    always_flag = 1;
+    pkt->val = 1;
+    pkt->next = modulo;
+    add_memory_range(&flag, sizeof(int), &mem);
+    add_memory_range(&always_flag, sizeof(int), &mem);
+    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();
+}
+
+/* end */
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/memory.c	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,363 @@
+/*
+
+    memory fragment management library
+
+    Shinji Kono (2006)
+
+    usage:
+
+    MemoryPtr db = 0;
+    add_memory(address,length,&db);
+
+	memory pattern is copyied and stored in a binary tree in db.
+	All patterns are shared.
+
+    memory pattern database (binary tree by pattern)
+
+
+ */
+
+#include <stdio.h>
+#include <stdlib.h>
+#include "memory.h"
+#include "crc32.h"
+#include <string.h>
+
+#define MEMORY_REPORT 1
+
+#if MEMORY_REPORT
+int    memory_header;
+int    memcmp_count;
+int    memory_body;
+int    restore_count;
+int    restore_size;
+int    range_count;
+int    range_size;
+#endif
+
+extern void die_exit(char *);
+
+void 
+die_exit(char *msg)
+{
+    fprintf(stderr,"%s\n",msg);
+    exit(1);
+}
+
+// static MemoryPtr memory_root;
+
+
+/*
+
+    make memory fragment as a part of the program state
+
+ */
+
+MemoryPtr
+create_memory(void *adr, int length)
+{
+    MemoryPtr m = (MemoryPtr)malloc(sizeof(Memory));
+    if (!m) die_exit("Cann't alloc memory list.");
+    m->left = m->right = 0;
+    m->length = length;
+    m->adr = m->body = adr;
+#if MEMORY_REPORT
+    memory_header++;
+    while (length-- > 0) {
+	printf("memory_dump 0x%x:0x%x\n", adr, *(unsigned char *)adr++);
+    }
+    printf("memory_dump ----------------\n");
+#endif
+    return m;
+}
+
+/*
+
+    Compute hash value of a memory fragment
+
+ */
+
+void
+compute_memory_hash1(MemoryPtr m)
+{
+    m->hash = Get_CRC((unsigned char *)m->adr,m->length);
+}
+
+void
+free_memory(MemoryPtr m)
+{
+    m->left = m->right = 0;
+    m->adr = m->body = 0;
+    free(m);
+}
+
+/*
+
+   Compare memory contents ( doesn't care about its address )
+
+ */
+
+int
+cmp_content(MemoryPtr a,MemoryPtr b)
+{
+    if (a->length != b->length) {
+	if (a->length > b->length) {
+	    return 1;
+	} else {
+	    return -1;
+	}
+    }
+    if (a->hash == b->hash) {
+#if MEMORY_REPORT
+    memcmp_count ++;
+#endif
+	return memcmp(a->body,b->body,a->length);
+    } else if (a->hash > b->hash) {
+        return 1;
+    } else {
+        return -1;
+    }
+}
+
+/*
+
+   Compare entire memory contents ( doesn't care about its address )
+
+ */
+
+static int
+cmp_memory1(MemoryPtr a,MemoryPtr b)
+{
+    int r;
+    if ((r=cmp_content(a,b))) return r;
+
+    if (a->adr==b->adr) {
+	return 0;
+    } 
+    return (a->adr > b->adr) ? 1 : -1;
+}
+
+int
+cmp_memory(MemoryPtr a,MemoryPtr b)
+{
+    int r;
+    while(1) {
+	if ((r=cmp_memory1(a,b))) return r;
+	if (a->left && b->left) {
+	    if ((r=cmp_memory(a->left,b->left))) return r;
+	} else if (a->left || b->left) {
+	    return (a->left > b->left)? 1 : -1;
+	}
+	if (a->right && b->right) {
+	    a = a->right; b = b->right;
+	    // recursive loop
+	} else if (a->right || b->right) {
+	    return (a->right > b->right)? 1 : -1;
+	} else {
+	    return 0;  // singleton
+	}
+    }
+}
+
+/*
+    Make a copy of real memory fragments
+ */
+
+MemoryPtr 
+copy_memory1(MemoryPtr m)
+{
+    MemoryPtr new = create_memory(m->adr,m->length);
+    void *p = (void *)malloc(m->length);
+    if (!p) {
+	die_exit("can't alloc memory body");
+	return 0;
+    }
+#if MEMORY_REPORT
+    memory_body += m->length;
+#endif
+    memcpy(p,m->adr,m->length);
+    m->body = new->body = p;     // abondon original memory pattern
+    new->hash = m->hash;
+    return new;
+}
+
+MemoryPtr
+copy_memory(MemoryPtr m, MemoryPtr *db)
+{
+    MemoryPtr new, out;
+    if (!m) return m;
+    new = create_memory(m->adr,m->length);
+    new->hash = m->hash;
+    // look up is necessary to share its memory pattern
+    memory_lookup(new, db, copy_memory1, &out);
+    if (m->left)  new->left = copy_memory(m->left, db);
+    if (m->right) new->right = copy_memory(m->right, db);
+    return new;
+}
+
+/*
+    restore copied memory save to the original addresses
+ */
+
+void
+restore_memory(MemoryPtr m)
+{
+    while (m) {
+	memcpy(m->adr,m->body,m->length);
+#if MEMORY_REPORT
+    restore_count ++;
+    restore_size += m->length;
+#endif
+	if (m->left)  restore_memory(m->left);
+	m = m->right;
+    }
+}
+
+
+/*
+    get hash for all memeory fragments
+	initial value of hash should be zero
+ */
+
+int
+get_memory_hash(MemoryPtr m, int hash)
+{
+    if (!m) return hash;
+    compute_memory_hash1(m);
+    if (m->left)  hash = get_memory_hash(m->left, hash);
+    if (m->right) return get_memory_hash(m->right, hash);
+    return m->hash | hash;
+}
+
+/*
+    add modified memory fragments to the pattern database
+ */
+
+MemoryPtr
+add_memory(void *ptr,int length, MemoryPtr *parent)
+{
+    Memory m, *out;
+    m.adr = m.body = ptr;
+    m.length = length;
+    m.left = m.right = 0;
+    compute_memory_hash1(&m);
+    
+    memory_lookup(&m, parent, copy_memory1, &out);
+    return out;
+}
+
+int
+memory_lookup(MemoryPtr m, MemoryPtr *parent, 
+		    MemoryPtr (*new_memory)(MemoryPtr), MemoryPtr *out)
+{
+    MemoryPtr db;
+    int r;
+
+    while(1) {
+        db = *parent;
+        if (!db) {
+	    /* not found */
+	    if (new_memory && out) {
+		db = new_memory(m);
+		db->left = db->right = 0;
+		*out = *parent = db;
+	    }
+            return 0;
+        }
+        if(!(r = cmp_memory1(m,db))) {
+            /* bingo */
+	    if (out) {
+		*out = db;
+	    }
+            return 1;
+        } else if (r>0) {
+            parent = &db->left;
+        } else if (r<0) {
+            parent = &db->right;
+        }
+    }
+    /* !NOT REACHED */
+}
+
+/*
+    memory range list management for state registration
+	this list points the real memory
+ */
+
+MemoryPtr
+add_memory_range(void *ptr,int length, MemoryPtr *parent)
+{
+    Memory m, *out;
+    m.adr = ptr;
+    m.length = length;
+    m.left = m.right = 0;
+    
+    memory_range_lookup(&m, parent, &out);
+    return out;
+}
+
+static int
+cmp_range(MemoryPtr a,MemoryPtr b)
+{
+    if (a->adr==b->adr) {
+	if (a->length != b->length) 
+	    die_exit("memory range inconsitency");
+	return 0;
+    }
+    return (a->adr > b->adr) ? 1 : -1;
+}
+
+int
+memory_range_lookup(MemoryPtr m, MemoryPtr *parent, MemoryPtr *out)
+{
+    MemoryPtr db;
+    int r;
+
+    while(1) {
+        db = *parent;
+        if (!db) {
+	    /* not found */
+	    if (out) {
+		db = create_memory(m->adr, m->length);
+		*out = *parent = db;
+	    }
+#if MEMORY_REPORT
+	    range_count++;
+	    range_size+=m->length;
+#endif
+            return 0;
+        }
+        if(!(r = cmp_range(m,db))) {
+            /* bingo (actually an error) */
+	    if (out) {
+		*out = db;
+	    }
+            return 1;
+        } else if (r>0) {
+            parent = &db->left;
+        } else if (r<0) {
+            parent = &db->right;
+        }
+    }
+    /* !NOT REACHED */
+}
+
+/*
+ */
+
+void
+memory_usage()
+{
+#if MEMORY_REPORT
+    printf("	memory_header %d\n",memory_header);
+    printf("	memcmp_count %d\n",memcmp_count);
+    printf("	memory_body %d\n",memory_body);
+    printf("	restore_count %d\n",restore_count);
+    printf("	restore_size %d\n",restore_size);
+    printf("	range_count %d\n",range_count);
+    printf("	range_size %d\n",range_size);
+#endif
+}
+
+
+/* end */
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/memory.h	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,57 @@
+#ifndef _MEMORY_H_
+#define _MEMORY_H_
+
+
+typedef struct memory {
+	void *adr;
+	int  length;
+	void *body;
+	int  hash;
+	struct memory *left,*right;
+} Memory, *MemoryPtr;
+
+extern void die_exit(char *);
+
+extern MemoryPtr
+create_memory(void *adr, int length);
+
+extern void
+compute_memory_hash1(MemoryPtr m);
+
+extern void
+free_memory(MemoryPtr m);
+
+extern int
+cmp_content(MemoryPtr a,MemoryPtr b);
+
+extern int
+cmp_memory(MemoryPtr a,MemoryPtr b);
+
+extern MemoryPtr 
+copy_memory(MemoryPtr m, MemoryPtr *db);
+
+extern void
+restore_memory(MemoryPtr m) ;
+
+extern int
+get_memory_hash(MemoryPtr m, int hash);
+
+MemoryPtr
+add_memory(void *ptr,int length, MemoryPtr *parent);
+
+extern int
+memory_lookup(MemoryPtr m, MemoryPtr *parent,
+                    MemoryPtr (*new_memory)(MemoryPtr), MemoryPtr *out);
+
+extern MemoryPtr
+add_memory_range(void *ptr,int length, MemoryPtr *parent);
+
+extern int
+memory_range_lookup(MemoryPtr m, MemoryPtr *parent, MemoryPtr *out);
+
+extern void
+memory_usage();
+
+
+#endif
+/* end */
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/state_db.c	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,82 @@
+#include <stdlib.h>
+#include "state_db.h"
+#include "memory.h"
+
+StateDB
+create_stateDB()
+{
+    StateDB s = (StateDB)malloc(sizeof(StateNode));
+    if (!s) die_exit("Cann't alloc state db node.");
+    return s;
+}
+
+static MemoryPtr mem_db;
+
+static int state_count0;
+
+void
+reset_state_count()
+{
+    state_count0 = 0;
+}
+
+int
+state_count()
+{
+    return state_count0;
+}
+
+
+/*
+
+    lookup_StateDB(struct state *s, StateDB *parent, StatePtr *out)
+
+    s->memory points the real memory
+    if s is new, it is copied in the database (parent).
+    if s is in the database, existing state is returned.
+
+    if return value is 0, it returns new state.
+    if out is null, no copy_state is created. (lookup mode)
+
+    Founded state or newly created state is returned in out.
+    
+ */
+
+int
+lookup_StateDB(StateDB s, StateDB *parent, StateDB *out)
+{
+    StateDB db;
+    int r;
+
+    while(1) {
+	db = *parent;
+	if (!db) {
+	    /* not found */
+	    if (out) {
+		db = create_stateDB();
+		db->left = db->right = 0;
+		db->memory = copy_memory(s->memory,&mem_db);
+		db->hash = s->hash;
+		state_count0 ++;
+		*parent = db;
+		*out = db;
+	    }
+	    return 0;
+	}
+	if (s->hash == db->hash) {
+	    r =  cmp_memory(s->memory,db->memory);
+	} else
+	    r =  (s->hash > db->hash)? 1 : -1;
+	if(!r) {
+	    /* bingo */
+	    if (out) *out = db;
+	    return 1;
+	} else if (r>0) {
+	    parent = &db->left;
+	} else if (r<0) {
+	    parent = &db->right;
+	}
+    }
+}
+
+/* end */
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/state_db.h	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,20 @@
+#ifndef _STATE_DB_H_
+#define _STATE_DB_H_
+
+
+typedef struct state_db {
+    struct memory *memory;
+    int hash;
+    struct state_db *left;
+    struct state_db *right;
+} StateNode, *StateDB;
+
+extern int
+lookup_StateDB(StateDB s, StateDB *db, StateDB *out);
+
+extern int state_count();
+extern void reset_state_count();
+
+
+
+#endif
--- /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 */
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/task.c	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,106 @@
+/*
+    OS Scheduler Simulator
+
+** 連絡先： 琉球大学情報工学科 河野 真治  
+** （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.
+
+  Task Queue Manager
+
+** modify: Atsuki Shimoji(atsuki@cr.ie.u-ryukyu.ac.jp)
+
+ */
+#include <stdio.h>
+#include <stdlib.h>
+#include "task.h"
+
+static void
+die_exit(char *msg)
+{
+    fprintf(stderr, "%s\n", msg);
+    exit(1);
+}
+
+TaskPtr
+new_task(struct packet *pkt)
+{
+    TaskPtr t;
+    t = (TaskPtr)malloc(sizeof(Task));
+    if (t) {
+	t->next = NULL;
+	t->pkt = pkt;
+    }
+    return t;
+}
+
+void
+free_task(TaskPtr t)
+{
+	free(t);
+}
+
+TaskPtr
+append_task(TaskPtr list, TaskPtr t)
+{
+    TaskPtr s = list;
+    if (!s) {
+	return t;
+    } else {
+	while (s->next) s = s->next;
+	s->next = t;
+	return list;
+    }
+}
+
+TaskIteratorPtr
+create_task_iterator(TaskPtr list,StateDB s,TaskIteratorPtr prev)
+{
+    TaskIteratorPtr new = (TaskIteratorPtr)malloc(sizeof(TaskIterator));
+    if (!new) die_exit("can't allocate task iterlator");
+
+    new->prev = prev;
+    new->state = s;
+    new->list = list;
+    new->last = list;
+    return new;
+}
+
+TaskPtr
+next_task_iterator(TaskIteratorPtr self)
+{
+    TaskPtr next;
+    if (!self->list) {
+	die_exit("task iterator inconsistency");
+    }
+    next = self->list->next;
+    if (!next) {
+	die_exit("task iterator next inconsistency");
+    }
+    if (next == self->last) {
+	return 0;
+    }
+    self->list = next;
+    return next;
+}
+
+void
+free_task_iterator(TaskIteratorPtr iter)
+{
+    free(iter);
+}
+
+/* end */
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/temporal_logic/task.h	Sun Jun 03 22:09:13 2012 +0900
@@ -0,0 +1,28 @@
+#ifndef _TASK_H_
+#define _TASK_H_
+#include "state_db.h"
+
+typedef struct task {
+    struct task *next;
+    struct packet *pkt;
+} Task, *TaskPtr;
+
+typedef struct task_iterator {
+    struct task_iterator *prev;
+    StateDB state;
+    TaskPtr list;
+    TaskPtr last;
+} TaskIterator, *TaskIteratorPtr;
+
+extern TaskPtr new_task(struct packet *pkt);
+extern void free_task(TaskPtr t);
+extern TaskPtr append_task(TaskPtr list, TaskPtr t);
+extern TaskIteratorPtr
+create_task_iterator(TaskPtr list, struct state_db *s, TaskIteratorPtr prev);
+
+extern TaskPtr
+next_task_iterator(TaskIteratorPtr self);
+extern void
+free_task_iterator(TaskIteratorPtr iter);
+
+#endif