|
0
|
1 \chapter{線形時相論理によるCbCプログラムの検証手法}
|
|
1
|
2 \label{chapter3}
|
|
0
|
3
|
|
|
4 \section{CbCによる並列プログラミング}
|
|
|
5 ここでは、例題に用いるサンプルプログラムの概要と、
|
|
|
6 そのプログラムの状態の分割およびCbCプログラムとの対応について説明する。
|
|
|
7 また、並列プログラムのシミュレーション方法についても述べる。
|
|
|
8
|
|
|
9 \subsection{Dining Philosophers Problemの概要}
|
|
|
10 検証用のサンプルプログラムとしてDining Philosophers Problemを用いる。
|
|
|
11 これは資源共有問題の一つで、次のような内容である。
|
|
|
12
|
|
|
13 5人の哲学者が円卓についている。各々の哲学者にはスパゲッティーを持った皿が出されている。
|
|
|
14 スパゲッティーはとても絡まっているので、2本のフォークを使わないと食べられない。
|
|
|
15 お皿の間には1本のフォークが置いてあるので、
|
|
|
16 5人の哲学者に対して5本のフォークが用意されていることになる(図\ref{fig:dpp_image})。
|
|
|
17 哲学者は思索と食事を交互に繰り返している。
|
|
|
18 空腹を覚えると、左右のフォークを手に取ろうと試み、
|
|
|
19 2本のフォークを取ることに成功するとしばし食事をし、
|
|
|
20 しばらくするとフォークを置いて思索に戻る。
|
|
|
21 隣の哲学者が食事中でフォークが手に取れない場合は、
|
|
|
22 そのままフォークが空くのを待つ。
|
|
|
23
|
|
|
24 \begin{figure}[htpb]
|
|
|
25 \begin{center}
|
|
|
26 \includegraphics[scale=.5]{figure/dpp_image.pdf}
|
|
|
27 \end{center}
|
|
|
28 \caption{Dining Philosophers Problemのイメージ}
|
|
|
29 \label{fig:dpp_image}
|
|
|
30 \end{figure}
|
|
|
31
|
|
|
32 各哲学者を一つのプロセスとすると、この問題では5個のプロセスが並列に動くことになる。
|
|
|
33 プロセスの並列実行はスケジューラによって制御することで実現する。
|
|
|
34
|
|
|
35 \subsection{状態の定義とコードセグメントとの対応}
|
|
|
36 Dining Philosophers ProblemをCbCで実装するにあたり、
|
|
|
37 プロセスを次のような8個の状態に分割した。
|
|
|
38 \begin{itemize}
|
|
|
39 \item 思索
|
|
|
40 \item フォークを持っていない場合の飢餓
|
|
|
41 \item 左手にフォークを持つ
|
|
|
42 \item 左手にフォークを持っている場合の飢餓
|
|
|
43 \item 右手にフォークを持つ
|
|
|
44 \item 食事
|
|
|
45 \item 右手のフォークを置く
|
|
|
46 \item 左手のフォークを置く
|
|
|
47 \end{itemize}
|
|
|
48
|
|
|
49 CbCではconcurrencyがコードセグメント単位であるため、
|
|
|
50 実装の方法により任意に細分化することができる。
|
|
|
51 今回は、状態数を8個とし、各状態に対応したコードセグメントを実装した。
|
|
|
52 以下にコードセグメントの例を示す。
|
|
|
53
|
|
|
54 \lstinputlisting[caption=「左手でフォークを持つ」コードセグメント,label=src:pickupL]
|
|
|
55 {src/pickupL.cbc}
|
|
|
56
|
|
|
57 ソースコード\ref{src:pickupL}はDining Philosophers Problemの
|
|
|
58 プログラムの一部である。
|
|
|
59 このコードセグメントは、「左手にフォークを持つ」状態に対応したものである。
|
|
|
60
|
|
|
61 処理の具体的な内容は、左手側のフォークがあればそのフォークを取り、
|
|
|
62 フォークを取ったプロセス(哲学者)のIDとフォークのIDを表示する。
|
|
|
63 その後、次の遷移先として「右手にフォークを持つ」状態である
|
|
|
64 pickup\_rforkコードセグメントをセットする。
|
|
|
65 もし、フォークがなければ次の遷移先として「フォークを持っていない場合の飢餓」状態である
|
|
|
66 hungry1コードセグメントをセットする。
|
|
|
67
|
|
|
68 各コードセグメントは、スケジューラに遷移するようにしている。
|
|
|
69 これは、複数のプロセスをスケジューラを用いて制御するためである。
|
|
|
70 状態遷移に必ずスケジューラを介すことで、
|
|
|
71 任意のプロセスのコードセグメントを実行することができる(図\ref{fig:scheduler})。
|
|
|
72
|
|
|
73 \begin{figure}[htpb]
|
|
|
74 \begin{center}
|
|
|
75 \includegraphics[scale=.7]{figure/scheduler.pdf}
|
|
|
76 \end{center}
|
|
|
77 \caption{スケジューラによる複数プロセスの制御}
|
|
|
78 \label{fig:scheduler}
|
|
|
79 \end{figure}
|
|
|
80
|
|
|
81 CbCプログラムはオートマトンと似た構造になっており、
|
|
|
82 コードセグメントと状態、引数付きgotoと状態遷移、
|
|
|
83 if制御文と遷移条件がそれぞれ対応している(表\ref{tab:automaton-cbc})。
|
|
|
84
|
|
|
85 \begin{table}
|
|
|
86 \centering
|
|
|
87 \begin{tabular}{|c|c|} \hline
|
|
|
88 オートマトン & CbC \\ \hline
|
|
|
89 状態 & コードセグメント \\
|
|
|
90 状態遷移 & 引数付きgoto \\
|
|
|
91 遷移条件 & if制御文 \\ \hline
|
|
|
92 \end{tabular}
|
|
|
93 \caption{オートマトンとCbCの対応}
|
|
|
94 \label{tab:automaton-cbc}
|
|
|
95 \end{table}
|
|
|
96
|
|
|
97 コードセグメントと状態の対応に関しては、実際にはコードセグメントを抜けるときに状態が
|
|
|
98 確定する。
|
|
|
99
|
|
|
100 並列実行をシミュレーションするために必要なスケジューラについて説明する。
|
|
|
101 スケジューラは、最初にプロセスの生成と初期化を行い、それをタスクリストに登録する。
|
|
|
102 その後、各プロセスに対してラウンドロビンやランダムといった任意の方式で実行する。
|
|
|
103 ラウンドロビンとは、各プロセスを一定時間ずつ順番に実行することである。
|
|
|
104
|
|
|
105 並列実行のシミュレーションに関しては、SPINを参考に各プロセスをランダムに
|
|
|
106 実行することで実現する。
|
|
|
107
|
|
|
108 \section{CbCプログラムのタブロー展開}
|
|
|
109 CbCプログラムのタブロー展開の特徴を以下に示す。
|
|
|
110 \begin{itemize}
|
|
|
111 \item プログラムの可能な実行の組み合わせすべてを調べる。
|
|
|
112 \item 状態の探索はDepth First Searchで行う。
|
|
|
113 \item プログラムの実行によって生成される状態は木構造で記録する。
|
|
|
114 \item 同じ状態はすべて共有される。
|
|
|
115 \end{itemize}
|
|
|
116
|
|
|
117 \subsection{状態の展開}
|
|
|
118 提案する手法では、プログラムの可能な実行の組み合わせをすべて調べることができる。
|
|
|
119 CbCプログラムにおける可能な実行の組み合わせとは、
|
|
|
120 CbCプログラムをオートマトンとみなすと、オートマトンの遷移経路にあたる。
|
|
|
121
|
|
|
122 例としてDining Philosophers Problemのプロセス(哲学者)を
|
|
|
123 状態遷移図で示す(図\ref{fig:dpp_automaton})。
|
|
|
124 本研究では、CbCで実装するにあたり状態を8個に分割している。
|
|
|
125 ここで、それぞれの状態をABCDEFGHと定義する。
|
|
|
126
|
|
|
127 \begin{description}
|
|
|
128 \item[A] 思索
|
|
|
129 \item[B] 飢餓
|
|
|
130 \item[C] 左手にフォークを持っている
|
|
|
131 \item[D] 左手にフォークを持つ場合の飢餓
|
|
|
132 \item[E] 両手にフォークを持っている
|
|
|
133 \item[F] 食事
|
|
|
134 \item[G] 右手のフォークを置いた
|
|
|
135 \item[H] 左手のフォークを置いた
|
|
|
136 \end{description}
|
|
|
137
|
|
|
138 このオートマトンは「プロセスを終了する」という入力がないと、
|
|
|
139 例えば、$A\to B\to B\to B\to\cdots$というように探索が無限に続いてしまう場合がある。
|
|
|
140 そうなると、一つの遷移経路が無限に続くことになり、
|
|
|
141 このオートマトンが取り得るすべての遷移経路を調べることができない。
|
|
|
142 そこで、「ひとつの遷移経路で同じ状態が表れた場合はその経路の探索を終了する」
|
|
|
143 という条件を付加する。
|
|
|
144 これにより、先ほどの経路の探索は$A\to B$で終了することができる。
|
|
|
145
|
|
|
146 このようにして、遷移経路を図\ref{fig:dpp_automaton}から求めると、
|
|
|
147 \begin{itemize}
|
|
|
148 \item $A\to B$
|
|
|
149 \item $A\to B\to C\to D$
|
|
|
150 \item $A\to B\to C\to D\to E\to F\to G\to H$
|
|
|
151 \item $A\to B\to C\to E\to F\to G\to H$
|
|
|
152 \end{itemize}
|
|
|
153 という結果が得られる。
|
|
|
154 これが、Dining Philosophers Problemのプロセスの可能な実行の組み合わせとなる。
|
|
|
155
|
|
|
156
|
|
|
157 \begin{figure}[htpb]
|
|
|
158 \begin{center}
|
|
3
|
159 \includegraphics[scale=.75]{figure/dpp_automaton.pdf}
|
|
0
|
160 \end{center}
|
|
|
161 \caption{Dining Philosophers Problemの状態遷移図}
|
|
|
162 \label{fig:dpp_automaton}
|
|
|
163 \end{figure}
|
|
|
164
|
|
|
165 例では単一のプロセスの場合を述べたが、実際には5個のプロセスを並列に実行することになる。
|
|
|
166 その場合、状態数は指数オーダーで増加する。
|
|
|
167 状態数が多い場合、特に並列プログラムに対する状態の展開を手作業で行うのは不可能に近い。
|
|
|
168
|
|
|
169 \newpage
|
|
|
170 \subsection{タブロー展開器の実装}
|
|
|
171 CbCプログラムの状態を自動的に展開するためのツールを作成した。
|
|
|
172 これをタブロー展開器と呼ぶ。
|
|
|
173
|
|
|
174
|
|
|
175 タブロー展開器は、スケジューラと同様にCbCプログラムに組み込み、
|
|
|
176 複数プロセスを制御することで並列実行をシミュレーションすることができる。
|
|
|
177 また、タブロー展開器は、コードセグメントを一つずつ実行しながら状態を探索していく。
|
|
|
178 状態の探索はDFS(Depth First Search)で行う。
|
|
|
179 例えば、Dining Philosophers Problemの単一プロセスの状態探索木は
|
|
|
180 図\ref{fig:dpp_dfs}のようになる。
|
|
|
181
|
|
|
182 \begin{figure}[htpb]
|
|
|
183 \begin{center}
|
|
|
184 \includegraphics[scale=.8]{figure/dpp_dfs.pdf}
|
|
|
185 \end{center}
|
|
|
186 \caption{Dining Philosophers Problemの状態遷移図}
|
|
|
187 \label{fig:dpp_dfs}
|
|
|
188 \end{figure}
|
|
|
189
|
|
|
190 探索が終了すると、すべての状態が展開されたことになる。
|
|
|
191
|
|
|
192
|
|
|
193 タブロー展開器の具体的な実装について説明する。
|
|
|
194
|
|
|
195 まず、始めに状態として扱う変数をすべて登録する。
|
|
|
196 変数はBinary Tree構造で記録する(図\ref{fig:memory_pattern})。
|
|
|
197 このBinary Treeをメモリパターンと呼ぶ。
|
|
|
198
|
|
|
199 \begin{figure}[htpb]
|
|
|
200 \begin{center}
|
|
|
201 \includegraphics[scale=.8]{figure/memory_pattern.pdf}
|
|
|
202 \end{center}
|
|
|
203 \caption{メモリパターンの例}
|
|
|
204 \label{fig:memory_pattern}
|
|
|
205 \end{figure}
|
|
|
206
|
|
|
207 新たに追加される変数がメモリパターンに既に登録されている場合、
|
|
|
208 その変数は登録されない。
|
|
|
209
|
|
|
210
|
|
|
211 メモリパターンは変数の集合である。
|
|
|
212 コードセグメントを実行することでいくつかの変数が変化した場合、
|
|
|
213 メモリパターンも変化したことになる(図\ref{fig:change_mem_pat})。
|
|
|
214
|
|
|
215 \begin{figure}[htpb]
|
|
|
216 \begin{center}
|
|
|
217 \includegraphics[scale=.9]{figure/change_mem_pat.pdf}
|
|
|
218 \end{center}
|
|
|
219 \caption{コードセグメントの実行にともなうメモリパターンの変化}
|
|
|
220 \label{fig:change_mem_pat}
|
|
|
221 \end{figure}
|
|
|
222
|
|
|
223 変化したメモリパターンを新しいメモリパターンとしてBinary Tree構造で記録していく。
|
|
|
224 このBinary Treeを状態データベースと呼ぶ。
|
|
|
225 状態データベースのノード(状態ノード)は、メモリパターンのアドレスと
|
|
|
226 そのメモリパターンのハッシュ値を保持する(図\ref{fig:state_db})。
|
|
|
227
|
|
|
228 \begin{figure}[htpb]
|
|
|
229 \begin{center}
|
|
|
230 \includegraphics[scale=.9]{figure/state_db.pdf}
|
|
|
231 \end{center}
|
|
|
232 \caption{状態データベースの構成}
|
|
|
233 \label{fig:state_db}
|
|
|
234 \end{figure}
|
|
|
235
|
|
|
236 新たにメモリパターンを追加する場合、メモリパターンのハッシュ値をもとに
|
|
|
237 状態データベースを検索する。もし、同じハッシュ値のメモリパターンが見つかった場合は
|
|
|
238 そのメモリパターンは状態データベースに追加されない。
|
|
|
239 見つからなかった場合、新たな状態ノードとして状態データベースに追加される。
|
|
|
240
|
|
|
241 メモリパターンの追加方法は、変化したメモリパターンのコピーを生成して
|
|
|
242 コピーの方を状態データベースに登録する。
|
|
|
243 これは、もとのメモリパターンは次のコードセグメントを実行すると変化してしまうからである
|
|
|
244 (図\ref{fig:mem_pat_entry})。
|
|
|
245
|
|
|
246 \begin{figure}[htpb]
|
|
|
247 \begin{center}
|
|
|
248 \includegraphics[scale=.9]{figure/mem_pat_entry.pdf}
|
|
|
249 \end{center}
|
|
|
250 \caption{メモリパターンの状態データベースへの追加方法}
|
|
|
251 \label{fig:mem_pat_entry}
|
|
|
252 \end{figure}
|
|
|
253
|
|
|
254
|
|
|
255 しかし、コードセグメントを実行してもメモリパターンに登録されているすべての変数が
|
|
|
256 変化するわけではない。変化するのは一部の変数のみである。
|
|
|
257 したがって、メモリパターン全体をコピーし、
|
|
|
258 状態データベースに登録するのはメモリ使用に関して無駄がある。
|
|
|
259
|
|
|
260 そこで、変化があった変数のみをコピーし、残りの変化のなかった部分は前回の状態を
|
|
|
261 そのまま使用するようにする。つまり、同じ状態を共有するようにする(図\ref{fig:mem_share})。
|
|
|
262 これにより、メモリ使用量を減らすことができる。
|
|
|
263
|
|
|
264 \begin{figure}[htpb]
|
|
|
265 \begin{center}
|
|
|
266 \includegraphics[scale=.9]{figure/mem_share.pdf}
|
|
|
267 \end{center}
|
|
|
268 \caption{同じ状態の共有}
|
|
|
269 \label{fig:mem_share}
|
|
|
270 \end{figure}
|
|
|
271
|
|
|
272
|
|
|
273
|
|
|
274 次にDepth First Search(DFS)による状態の探索の実装について述べる。
|
|
|
275
|
|
|
276 本研究では、イテレータを用いてDFSを実装した。
|
|
|
277 イテレータとは、配列やリストなどのデータ構造の各要素に対する
|
|
|
278 繰り返し処理を抽象化する手法のことである。
|
|
|
279
|
|
|
280 タブロー展開器はスケジューラとしての機能を備えている。
|
|
|
281 そのため、プロセスを実行する順番をリストとして持ち、制御する。
|
|
|
282 これをタスクリストと呼ぶ(図\ref{fig:task_list})。
|
|
|
283
|
|
|
284 \begin{figure}[htpb]
|
|
|
285 \begin{center}
|
|
|
286 \includegraphics[scale=.9]{figure/task_list.pdf}
|
|
|
287 \end{center}
|
|
|
288 \caption{タスクリストの例}
|
|
|
289 \label{fig:task_list}
|
|
|
290 \end{figure}
|
|
|
291
|
|
|
292 状態を展開する際に、このタスクリストに登録された順番にプロセスを実行していく。
|
|
|
293 したがって、プログラムの状態を一つ進めるためにタスクリストからタスクを取りだし、
|
|
|
294 実行するという処理が繰り返し必要になる。
|
|
|
295 その繰り返し処理を抽象化することで、データ構造の要素に対して行いたい処理を
|
|
|
296 簡潔に記述することができる。
|
|
|
297
|
|
|
298
|
|
|
299 DFSの実装の具体的な内容について述べる。
|
|
|
300
|
|
|
301 タスクリストからタスクを取り出す機構としてタスクイテレータを実装した。
|
|
|
302 タスクイテレータはその時点のタスクリストと状態データベースおよび
|
|
|
303 ひとつ前の時点のタスクイテレータを保持している(図\ref{fig:task_iterator})。
|
|
|
304
|
|
|
305 \begin{figure}[htpb]
|
|
|
306 \begin{center}
|
|
|
307 \includegraphics[scale=.9]{figure/task_iterator.pdf}
|
|
|
308 \end{center}
|
|
|
309 \caption{タスクイテレータ}
|
|
|
310 \label{fig:task_iterator}
|
|
|
311 \end{figure}
|
|
|
312
|
|
|
313 まず、最初のメモリパターンを状態データベースに登録後、
|
|
|
314 タスクイテレータの処理によりタスクを取りだしコードセグメントを実行する。
|
|
|
315 その実行によって、変化したメモリパターンを状態データベースからハッシュ値をもとに検索する。
|
|
|
316 同じメモリパターンがなかった場合、状態データベースに追加する。
|
|
|
317 その後、１段深く探索するために新たにタスクイテレータを生成し、
|
|
|
318 その時点の状態データベースを登録する(図\ref{fig:dfs1})。
|
|
|
319
|
|
|
320 \begin{figure}[htpb]
|
|
|
321 \begin{center}
|
|
|
322 \includegraphics[scale=.9]{figure/dfs1.pdf}
|
|
|
323 \end{center}
|
|
|
324 \caption{タスクイテレータを用いたDFS 1}
|
|
|
325 \label{fig:dfs1}
|
|
|
326 \end{figure}
|
|
|
327
|
|
|
328 同じメモリパターンがあった場合は、その経路の探索を終了し、
|
|
|
329 タスクイテレータにより次のタスクを取りだしコードセグメントを実行する。
|
|
|
330
|
|
|
331 タスクイテレータのタスクリストをすべて実行した場合、
|
|
|
332 そのタスクイテレータを破棄し、ひとつ前のタスクイテレータに戻る(図\ref{fig:dfs2})。
|
|
|
333 そこで探索可能な経路があればメモリパターンをレストアし探索を行う。
|
|
|
334
|
|
|
335 \begin{figure}[htpb]
|
|
|
336 \begin{center}
|
|
|
337 \includegraphics[scale=.8]{figure/dfs2.pdf}
|
|
|
338 \end{center}
|
|
|
339 \caption{タスクイテレータを用いたDFS 2}
|
|
|
340 \label{fig:dfs2}
|
|
|
341 \end{figure}
|
|
|
342
|
|
|
343 これを繰り返していき、タスクイテレータが根に到達した場合、
|
|
|
344 全状態の探索が完了したことになる(図\ref{fig:dfs3})。
|
|
|
345
|
|
|
346 \begin{figure}[htpb]
|
|
|
347 \begin{center}
|
|
|
348 \includegraphics[scale=.8]{figure/dfs3.pdf}
|
|
|
349 \end{center}
|
|
|
350 \caption{状態探索の完了}
|
|
|
351 \label{fig:dfs3}
|
|
|
352 \end{figure}
|
|
|
353
|
|
|
354
|
|
|
355 \newpage
|
|
|
356 ソースコード\ref{src:tableau}に実際にタブロー展開を行っているコードセグメントを示す。
|
|
|
357
|
|
|
358 \lstinputlisting[caption=タブローコードセグメント,label=src:tableau]
|
|
|
359 {src/tableau.cbc}
|
|
|
360
|
|
|
361 タブローコードセグメントは、関数呼び出しを使用するためCwCで記述している。
|
|
|
362
|
|
|
363 \verb|get_memory_hash()|関数によってメモリパターンのハッシュ値を取得する。
|
|
|
364 そのハッシュ値をもとに\verb|lookup_StateDB()|関数で状態データベースの検索を行っている。
|
|
|
365 \verb|next_task_iterator()|関数は次に実行するタスクを取り出すものである。
|
|
|
366
|
|
|
367 \verb|restore_memory()|関数は任意の時点の状態に戻すための関数である。
|
|
|
368
|
|
|
369 実際にコードセグメントを実行するのは\verb|goto list->phils->next()|である。
|
|
|
370 引数付きgotoで検証対象のプログラムのコードセグメントに遷移する。
|
|
|
371
|
|
|
372 タスクイテレータが根に達した場合、探索を終了するために
|
|
|
373 \verb|goto ret(0),env|を実行している。
|
|
|
374
|
|
|
375 %\section{LZW法を用いた状態の圧縮}
|
|
|
376
|
|
|
377 \section{線形時相論理による仕様の検証手法}
|
|
|
378 タブロー展開を行う際に、線形時相論理(Linear-time Temporal Logic、LTL)式より
|
|
|
379 生成されたコードセグメントを実行することで検証を行う。
|
|
|
380
|
|
|
381 \subsection{検証の実装}
|
|
|
382 検証対象のプログラムからスケジューラに遷移した後、タブローコードセグメントに遷移する前に
|
|
|
383 LTL式より生成された検証用コードセグメントを実行する。
|
|
|
384 これにより、すべての状態において特定の性質を満たすことを調べることが可能である。
|
|
|
385
|
|
|
386 実装したDining Philosophers Problemプログラムに対してデッドロックの検出を行う。
|
|
|
387 デッドロックとは、複数のプロセスが互いに相手の占有している資源の開放を待ってしまい、
|
|
|
388 結果としてプログラムが停止してしまうことである。排他制御の欠陥で起こる。
|
|
|
389
|
|
|
390 Dining Philosophers Problemにおいて、資源とはフォークのことである。
|
|
|
391 つまり、この場合のデッドロックはすべての哲学者(プロセス)が左手でフォークを持ち、
|
|
|
392 右手のフォークが空くのを待っている状態である(図\ref{fig:dpp_deadlock})。
|
|
|
393
|
|
|
394 \begin{figure}[htpb]
|
|
|
395 \begin{center}
|
|
|
396 \includegraphics[scale=.5]{figure/dpp_deadlock.pdf}
|
|
|
397 \end{center}
|
|
|
398 \caption{Dining Philosophers Problemのデッドロック状態}
|
|
|
399 \label{fig:dpp_deadlock}
|
|
|
400 \end{figure}
|
|
|
401
|
|
|
402
|
|
|
403 デッドロックを検知するために、 命題pを「すべての哲学者が左手にフォークを持っている」
|
|
|
404 として、 命題pが決して起こらないことを検査する。
|
|
|
405 これをLTL式で表すと□~pである。
|
|
|
406 これは、LTLで表現できる重要な特性の一つの安全性特性である。
|
|
|
407
|
|
|
408 これを検査するための検証用コードセグメントをソースコード\ref{src:check}に示す。
|
|
|
409
|
|
|
410 \lstinputlisting[caption=検証用コードセグメント,label=src:check]
|
|
|
411 {src/ltl.cbc}
|
|
|
412
|
|
|
413 \verb|p()|関数は命題pに相当するものですべての哲学者(プロセス)が
|
|
|
414 左手にフォークを持っているかを判定するものである。
|
|
|
415 checkコードセグメントがタブロー展開の際に実行されることで、
|
|
|
416 すべての状態において命題pが決して起こらないかどうかを検査することができる。
|
|
|
417
|
|
|
418 %%% end %%%
|
