Mercurial > hg > Papers > 2008 > atsuki-master
changeset 9:c2a35ce4546e
*** empty log message ***
author | atsuki |
---|---|
date | Fri, 15 Feb 2008 17:17:15 +0900 (2008-02-15) |
parents | 17d019b274a5 |
children | a4babe6179a7 |
files | paper/chapter3.tex paper/figure/change_mem_pat.bb paper/figure/change_mem_pat.pdf paper/figure/dfs1.bb paper/figure/dfs1.pdf paper/figure/mem_pat_entry.bb paper/figure/mem_pat_entry.pdf paper/figure/mem_pat_tree.bb paper/figure/mem_pat_tree.pdf paper/figure/mem_share.bb paper/figure/mem_share.pdf paper/figure/memoryBtree.bb paper/figure/memoryBtree.pdf paper/figure/memory_pattern.bb paper/figure/memory_pattern.pdf paper/figure/stateDB.bb paper/figure/stateDB.pdf paper/figure/state_db.bb paper/figure/state_db.pdf paper/figure/task_iterator.bb paper/figure/task_iterator.pdf |
diffstat | 21 files changed, 99 insertions(+), 95 deletions(-) [+] |
line wrap: on
line diff
--- a/paper/chapter3.tex Fri Feb 15 17:17:15 2008 +0900 +++ b/paper/chapter3.tex Fri Feb 15 17:17:15 2008 +0900 @@ -192,38 +192,76 @@ ���֥���Ÿ����ζ���Ū�ʼ����ˤĤ����������롣 -�ޤ����Ϥ�˾��֤Ȥ��ư����ѿ��٤���Ͽ���롣 -�ѿ���Binary Tree��¤�ǵ�Ͽ����(��\ref{fig:memory_pattern})�� -����Binary Tree�����ѥ�����ȸƤ֡� +�ޤ����Ϥ�˾��֤Ȥ��ư������٤Ƥ��ѿ��Υ��ɥ쥹�Ȥ��Υ�� +Binary Tree��¤�ǵ�Ͽ����(��\ref{fig:memoryBtree})�� +����Binary Tree�����ĥ�ȸƤ֡� +�ѿ��ϥ����ΰ�˳�Ǽ����Ƥ��ꡢ�����ΰ�Υ��ɥ쥹�Ȥ��Υ�ǻ��ꤵ��롣 +�������ɲä�����ѿ�������ĥ�˴�����Ͽ����Ƥ����硢�����ѿ�����Ͽ����ʤ��� + +\begin{figure}[htpb] + \begin{center} + \includegraphics[scale=.8]{figure/memoryBtree.pdf} + \end{center} + \caption{�ѿ��Υ��ɥ쥹�Ȥ��Υ��Binary Tree} + \label{fig:memoryBtree} +\end{figure} + + +���٤Ƥ��ѿ�����Ͽ���줿�顢���ˤ��Υ���ĥ�Υ��ԡ����������� +���ԡ�����֥ǡ����١�������Ͽ���롣 +����ĥ�ԡ�����Ȥ������Τޤޥ��ԡ�����ΤǤϤʤ��� +����Υѥ���������ܤ���Ʊ���ѥ�����϶�ͭ�����褦�˥��ԡ����������롣 +���Υ���ĥ�Υ��ԡ��ˤ�ä����������Binary Tree�����ѥ�����ĥ�ȸƤ֡� + +����Υѥ�����Ȥϡ��㤨���ѿ�A���ѿ�B������ĥ����Ͽ����Ƥ���Ȥ����������롣 +�ѿ�A���ѿ�B�ϥ��ɥ쥹���㤦�Τǥ���ĥ�ˤ��̡�����Ͽ����Ƥ��롣 +�����Ǥ⤷���ѿ�A���ѿ�B�����Ƥ�ξ���Ȥ�0���ä���硢 +���ɥ쥹�ϰ�äƤ��Ƥ�����ΰ�����Ƥ�Ʊ���ˤʤ�(��\ref{fig:memory_pattern})�� +���Υ����ΰ�����ƤΤ��Ȥ����ѥ�����ȸƤ֡� \begin{figure}[htpb] \begin{center} \includegraphics[scale=.8]{figure/memory_pattern.pdf} \end{center} - \caption{����ѥ��������} + \caption{����ѥ�����} \label{fig:memory_pattern} \end{figure} -����ѥ�����ΥΡ��ɤϡ������ΰ�Υ��ɥ쥹�Ȥ��Υ������� -�����ΰ�ԡ�������ΤΥ��ɥ쥹�������ΰ�Υϥå����͡� -�����λҥΡ��ɤΥݥ��ǹ�������Ƥ���(��\ref{fig:mem_pat_structure})�� -�����ΰ�Υ��ɥ쥹����Ͽ���줿�ѿ��Υ��ɥ쥹�Ǥ��롣 + +����ѥ�����ĥ�������ˤĤ����������롣 + +����ѥ�����ĥ�ϥ���ѥ�����Ȥ��Υ�����ǤȤ���Binary Tree�Ǥ��롣 +����ĥ�����Ǥԡ�������������ѥ�����ĥ����Ͽ���Ƥ����� +��Ͽ����ݤˡ�����ѥ�����ĥ��Ʊ������ѥ����ʤ����������롣 +�⤷��Ʊ������ѥ������ä���硢����ĥ�����Ǥԡ������� +����ѥ�����ĥ��Ʊ���ѥ���������Ǥ�ؤ��褦�ˤ���(��\ref{fig:mem_pat_tree})�� +�ĤޤꡢƱ�����֤�ͭ����褦�ˤ��롣 + +����ˤ����Ѥ�������̤餹���Ȥ��Ǥ��롣 \begin{figure}[htpb] \begin{center} - \includegraphics[scale=.8]{figure/mem_pat_structure.pdf} + \includegraphics[scale=.8]{figure/mem_pat_tree.pdf} \end{center} - \caption{����ѥ�����ΥΡ��ɤι�¤�ȥ����ΰ�} - \label{fig:mem_pat_structure} + \caption{����ѥ�����ĥ} + \label{fig:mem_pat_tree} \end{figure} -�������ɲä�����ѿ�������ѥ�����˴�����Ͽ����Ƥ����硢 -�����ѿ�����Ͽ����ʤ��� -\\ + +���֥ǡ����١����Ȥϡ�����ѥ�����ĥ�Ȥ��Υϥå����ͤ� +���ǤȤ��ƻ���Binary Tree�Ǥ���(��\ref{fig:stateDB})�� -����ѥ�������ѿ��ν���Ǥ��롣 -�����ɥ������Ȥ�¹Ԥ��뤳�ȤǤ����Ĥ����ѿ����Ѳ�������硢 -����ѥ�������Ѳ��������Ȥˤʤ�(��\ref{fig:change_mem_pat})�� +\begin{figure}[htpb] + \begin{center} + \includegraphics[scale=.8]{figure/stateDB.pdf} + \end{center} + \caption{���֥ǡ����١���} + \label{fig:stateDB} +\end{figure} + + +�����ɥ������Ȥ�¹Ԥ���ȡ�����ĥ����Ͽ����Ƥ��� +�ѿ�������(����ѥ�����)���Ѳ������礬����(��\ref{fig:change_mem_pat})�� \begin{figure}[htpb] \begin{center} @@ -233,55 +271,13 @@ \label{fig:change_mem_pat} \end{figure} -�Ѳ���������ѥ������������ѥ�����Ȥ���Binary Tree��¤�ǵ�Ͽ���Ƥ����� -����Binary Tree����֥ǡ����١����ȸƤ֡� -���֥ǡ����١����ΥΡ���(���֥Ρ���)�ϡ�����ѥ�����Υ��ɥ쥹�� -���Υ���ѥ�����Υϥå����ͤ��ݻ�����(��\ref{fig:state_db})�� - -\begin{figure}[htpb] - \begin{center} - \includegraphics[scale=.9]{figure/state_db.pdf} - \end{center} - \caption{���֥ǡ����١����ι���} - \label{fig:state_db} -\end{figure} - -�����˥���ѥ�������ɲä����硢����ѥ�����Υϥå����ͤ��Ȥ� -���֥ǡ����١��������롣�⤷��Ʊ���ϥå����ͤΥ���ѥ������Ĥ��ä����� -���Υ���ѥ�����Ͼ��֥ǡ����١������ɲä���ʤ��� -���Ĥ���ʤ��ä���硢�����ʾ��֥Ρ��ɤȤ��ƾ��֥ǡ����١������ɲä���롣 - -����ѥ�������ɲ���ˡ�ϡ��Ѳ���������ѥ�����Υ��ԡ����������� -���ԡ���������֥ǡ����١�������Ͽ���롣 -����ϡ���ȤΥ���ѥ�����ϼ��Υ����ɥ������Ȥ�¹Ԥ�����Ѳ����Ƥ��ޤ�����Ǥ��� -(��\ref{fig:mem_pat_entry})�� - -\begin{figure}[htpb] - \begin{center} - \includegraphics[scale=.9]{figure/mem_pat_entry.pdf} - \end{center} - \caption{����ѥ�����ξ��֥ǡ����١����ؤ��ɲ���ˡ} - \label{fig:mem_pat_entry} -\end{figure} - - -�������������ɥ������Ȥ�¹Ԥ��Ƥ����ѥ��������Ͽ����Ƥ��뤹�٤Ƥ��ѿ��� -�Ѳ�����櫓�ǤϤʤ����Ѳ�����Τϰ������ѿ��ΤߤǤ��롣 -�������äơ�����ѥ��������Τԡ����� -���֥ǡ����١�������Ͽ����Τϥ�����Ѥ˴ؤ���̵�̤����롣 - -�����ǡ��Ѳ������ä��ѿ��Τߤԡ������Ĥ���Ѳ��Τʤ��ä���ʬ������ξ��֤� -���Τޤ��Ѥ���褦�ˤ��롣�ĤޤꡢƱ�����֤�ͭ����褦�ˤ���(��\ref{fig:mem_share})�� -����ˤ�ꡢ��������̤餹���Ȥ��Ǥ��롣 - -\begin{figure}[htpb] - \begin{center} - \includegraphics[scale=.9]{figure/mem_share.pdf} - \end{center} - \caption{Ʊ�����֤ζ�ͭ} - \label{fig:mem_share} -\end{figure} - +����ѥ������Ѳ���������ĥ���鿷���˥���ѥ�����ĥ���������롣 +�������줿����ѥ�����ĥ����֥ǡ����١������ɲä����硢 +����ѥ�����ĥ�Υϥå����ͤ��Ȥ˾��֥ǡ����١��������롣 +�⤷��Ʊ���ϥå����ͤΥ���ѥ�����ĥ�����Ĥ��ä����� +���Υ���ѥ�����ĥ�Ͼ��֥ǡ����١������ɲä���ʤ��� +���Ĥ���ʤ��ä���硢���֥ǡ����١������ɲä���롣 +\\ ����Depth First Search(DFS)�ˤ����֤�õ���μ����ˤĤ��ƽҤ٤롣 @@ -313,7 +309,8 @@ �������ꥹ�Ȥ��饿��������Ф������Ȥ��ƥ��������ƥ졼������������� ���������ƥ졼���Ϥ��λ����Υ������ꥹ�ȤȾ��֥ǡ����١�������� -�ҤȤ����λ����Υ��������ƥ졼�����ݻ����Ƥ���(��\ref{fig:task_iterator})�� +�ҤȤ����λ����Υ��������ƥ졼�����ݻ����Ƥ��롣 +�ޤ����������ꥹ�Ȥ��鼡�Υ���������Ф���ǽ����äƤ���(��\ref{fig:task_iterator})�� \begin{figure}[htpb] \begin{center} @@ -323,10 +320,11 @@ \label{fig:task_iterator} \end{figure} -�ޤ����ǽ�Υ���ѥ��������֥ǡ����١�������Ͽ�塢 +�ޤ����ǽ�Υ���ѥ�����ĥ�����ĥ��������������֥ǡ����١�������Ͽ���롣 ���������ƥ졼���ν����ˤ�����������������ɥ������Ȥ�¹Ԥ��롣 -���μ¹Ԥˤ�äơ��Ѳ���������ѥ��������֥ǡ����١�������ϥå����ͤ��Ȥ˸������롣 -Ʊ������ѥ����ʤ��ä���硢���֥ǡ����١������ɲä��롣 +���μ¹Ԥˤ�ä��Ѳ���������ĥ������ѥ�����ĥ���������� +�������֥ǡ����١������鸡�����롣 +Ʊ������ѥ�����ĥ���ʤ��ä���硢���֥ǡ����١������ɲä��롣 ���θ塢���ʿ���õ�����뤿��˿����˥��������ƥ졼������������ ���λ����ξ��֥ǡ����١�������Ͽ����(��\ref{fig:dfs1})�� @@ -338,7 +336,7 @@ \label{fig:dfs1} \end{figure} -Ʊ������ѥ������ä����ϡ����η�ϩ��õ����λ���� +Ʊ������ѥ�����ĥ�����ä����ϡ����η�ϩ��õ����λ���� ���������ƥ졼���ˤ�꼡�Υ�����������������ɥ������Ȥ�¹Ԥ��롣 ���������ƥ졼���Υ������ꥹ�Ȥ٤Ƽ¹Ԥ�����硢 @@ -392,7 +390,8 @@ �������줿�����ɥ������Ȥ�¹Ԥ��뤳�ȤǸ��ڤ�Ԥ��� \subsection{���ڤμ���} -�����оݤΥץ�����फ�饹�����塼������ܤ����塢���֥��������ɥ������Ȥ����ܤ������� +�����оݤΥץ�����फ�饹�����塼������ܤ����塢 +���֥��������ɥ������Ȥ����ܤ������� LTL������������줿�����ѥ����ɥ������Ȥ�¹Ԥ��롣 ����ˤ�ꡢ���٤Ƥξ��֤ˤ�������������������������Ȥ�Ĵ�٤뤳�Ȥ���ǽ�Ǥ��롣 @@ -423,8 +422,8 @@ \lstinputlisting[caption=�����ѥ����ɥ�������,label=src:check] {src/ltl.cbc} -\verb|p()|�ؿ���̿��p�����������ΤǤ��٤Ƥ�ů�ؼ�(�ץ�����)�� -����˥ե���������äƤ��뤫��Ƚ�ꤹ���ΤǤ��롣 +\verb|p()|�ؿ���̿��p�����������Τǡ����٤Ƥ�ů�ؼ�(�ץ�����)�� +����˥ե���������äƤ��뤫�ɤ�����Ƚ�ꤹ���ΤǤ��롣 check�����ɥ������Ȥ����֥���Ÿ���κݤ˼¹Ԥ���뤳�Ȥǡ� ���٤Ƥξ��֤ˤ�����̿��p���褷�Ƶ�����ʤ����ɤ��������뤳�Ȥ��Ǥ��롣
--- a/paper/figure/change_mem_pat.bb Fri Feb 15 17:17:15 2008 +0900 +++ b/paper/figure/change_mem_pat.bb Fri Feb 15 17:17:15 2008 +0900 @@ -1,5 +1,5 @@ %%Title: ./change_mem_pat.pdf %%Creator: ebb Version 0.5.2 -%%BoundingBox: 0 0 490 703 -%%CreationDate: Fri Feb 8 01:17:47 2008 +%%BoundingBox: 0 0 479 382 +%%CreationDate: Fri Feb 15 15:43:22 2008
--- a/paper/figure/dfs1.bb Fri Feb 15 17:17:15 2008 +0900 +++ b/paper/figure/dfs1.bb Fri Feb 15 17:17:15 2008 +0900 @@ -1,5 +1,5 @@ %%Title: ./dfs1.pdf %%Creator: ebb Version 0.5.2 -%%BoundingBox: 0 0 495 376 -%%CreationDate: Tue Feb 12 01:17:32 2008 +%%BoundingBox: 0 0 526 332 +%%CreationDate: Fri Feb 15 17:35:26 2008
--- a/paper/figure/mem_pat_entry.bb Fri Feb 15 17:17:15 2008 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -%%Title: ./mem_pat_entry.pdf -%%Creator: ebb Version 0.5.2 -%%BoundingBox: 0 0 537 320 -%%CreationDate: Fri Feb 8 04:17:33 2008 -
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/figure/mem_pat_tree.bb Fri Feb 15 17:17:15 2008 +0900 @@ -0,0 +1,5 @@ +%%Title: ./mem_pat_tree.pdf +%%Creator: ebb Version 0.5.2 +%%BoundingBox: 0 0 466 429 +%%CreationDate: Fri Feb 15 14:05:10 2008 +
--- a/paper/figure/mem_share.bb Fri Feb 15 17:17:15 2008 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -%%Title: ./mem_share.pdf -%%Creator: ebb Version 0.5.2 -%%BoundingBox: 0 0 484 507 -%%CreationDate: Fri Feb 8 04:17:33 2008 -
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/figure/memoryBtree.bb Fri Feb 15 17:17:15 2008 +0900 @@ -0,0 +1,5 @@ +%%Title: ./memoryBtree.pdf +%%Creator: ebb Version 0.5.2 +%%BoundingBox: 0 0 522 283 +%%CreationDate: Fri Feb 15 10:04:40 2008 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/figure/memory_pattern.bb Fri Feb 15 17:17:15 2008 +0900 @@ -0,0 +1,5 @@ +%%Title: ./memory_pattern.pdf +%%Creator: ebb Version 0.5.2 +%%BoundingBox: 0 0 494 233 +%%CreationDate: Fri Feb 15 17:48:32 2008 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/paper/figure/stateDB.bb Fri Feb 15 17:17:15 2008 +0900 @@ -0,0 +1,5 @@ +%%Title: ./stateDB.pdf +%%Creator: ebb Version 0.5.2 +%%BoundingBox: 0 0 526 343 +%%CreationDate: Fri Feb 15 15:01:46 2008 +
--- a/paper/figure/state_db.bb Fri Feb 15 17:17:15 2008 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,5 +0,0 @@ -%%Title: ./state_db.pdf -%%Creator: ebb Version 0.5.2 -%%BoundingBox: 0 0 436 304 -%%CreationDate: Fri Feb 8 01:59:03 2008 -
--- a/paper/figure/task_iterator.bb Fri Feb 15 17:17:15 2008 +0900 +++ b/paper/figure/task_iterator.bb Fri Feb 15 17:17:15 2008 +0900 @@ -1,5 +1,5 @@ %%Title: ./task_iterator.pdf %%Creator: ebb Version 0.5.2 -%%BoundingBox: 0 0 502 187 -%%CreationDate: Fri Feb 8 09:28:29 2008 +%%BoundingBox: 0 0 508 369 +%%CreationDate: Fri Feb 15 16:41:12 2008