(57)【要約】      （修正有）【課題】可変制約に分類を付与することで、全制約を満たせなかった場合は、ユーザが選別した特定分類の可変制約を満たす解を生成することのできる制約充足解生成装置を提供する。【解決手段】制約充足度を評価するための評価情報を入力する入力部１１と、入力部１１で入力した評価情報を記憶する記憶部１２と、制約充足度を評価するためのモデル検査用プログラムの生成で用いる関数を保持する関数ライブラリ１４と、評価情報を元に、関数ライブラリ１４に保持している関数を利用して、モデル検査用プログラムと、モデル検査のための検証式を生成するプログラム生成部１３と、モデル検査用プログラムを、検証式を用いてモデル検査により検証し、与えられた制約に対して最適となる組み合わせを表す最適解の組み合わせと、生成された最適解に対して、各制約を充足しているかどうかを表す制約充足結果とを求める探索部１５と、を備える。【選択図】図１
2014086022.tif 000002
【特許請求の範囲】
【請求項１】
対象となるシステムに要求される制約のうち、ユーザが変更可能であって分類を付与した制約を充足する割合を表す制約充足度を評価するための評価情報を入力する入力部と、
前記入力部で入力した評価情報を記憶する記憶部と、
前記制約充足度を評価するためのモデル検査用プログラムの生成で用いる関数を保持する関数ライブラリと、
前記評価情報を元に、前記関数ライブラリに保持している関数を利用して、前記モデル検査用プログラムと、モデル検査のための検証式を生成するプログラム生成部と、
前記モデル検査用プログラムを、前記検証式を用いてモデル検査により検証し、与えられた制約に対して最適となる組み合わせを表す最適解の組み合わせと、生成された前記最適解に対して、各制約を充足しているかどうかを表す制約充足結果とを求める探索部と、
を備える制約充足解生成装置。
【請求項２】
前記評価情報は、制約情報、属性情報、動作仕様である請求項１記載の制約充足解生成装置。
【請求項３】
前記制約情報は、特定の前記制約に対して条件・結果・分類の変数値の集合を記述した制約リストである請求項２記載の制約充足解生成装置。
【請求項４】
前記制約リストは、前記制約を、(条件１)＆・・・＆(条件Ｎ)の場合、(結果１) ＆・・・＆(結果Ｎ)になる、と定義したときの前記制約の要素が持つべき値と分類を列挙した前記制約毎のリストである請求項３記載の制約充足解生成装置。
【請求項５】
前記属性情報は、対象システムに設定する可変のもので、属性が取り得る候補値を列挙し各属性毎にリスト化した属性値リストと、設定可能な前記属性値の組み合わせの上限値である組み合わせ数である請求項４記載の制約充足解生成装置。
【請求項６】
前記動作仕様は、対象システムの持つ変数定義情報と、対象システムの挙動を変数間の関係で表した、ドメイン固有の動作仕様を記述した動作仕様表である請求項５記載の制約充足解生成装置。
【請求項７】
前記記憶部は、前記動作仕様表を取得し、記憶する動作仕様記憶部と、前記制約リストを取得し、記憶する制約情報記憶部と、前記属性値リスト及び前記組み合わせ数を取得し、記憶する属性情報記憶部から構成される請求項６記載の制約充足解生成装置。
【請求項８】
前記動作仕様表は、前記制約情報及び前記属性情報の変数仕様と、ある動作結果を出す上での前記属性や前記制約の要素の取る値を列挙した前記動作仕様毎のリストである請求項６記載の制約充足解生成装置。
【請求項９】
前記探索部は、モデル検査のツールとしてＳＰＩＮ（登録商標）を利用する請求項１記載の制約充足解生成装置。
【請求項１０】
前記関数は、前記制約の充足度を評価するため制約充足度評価関数、前記制約を設定するための制約設定関数、前記属性値を設定するための属性値設定関数、前記動作結果を取得するための動作結果取得関数である請求項９記載の制約充足解生成装置。
【請求項１１】
前記探索部では、解はないという命題を網羅的に検証して、反例を挙げることで解を生成する請求項１乃至請求項１０のいずれか１項に記載の制約充足解生成装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明の実施形態は、制約を充足する解の生成装置に関する。
【背景技術】
【０００２】
一般的に、対象となるシステムが成立するのに必要な条件として、いくつかの制約がある。システムが複雑化・高度化するにつれて制約も増えていくが、全ての制約が満たされる（充足される）のか否かが問題となる。
【０００３】
制約充足問題は、変数の組み合わせの中から与えられた全ての制約を満たす組み合わせを探索する問題である。制約充足問題の中には、制約が強すぎるために問題が解けない場合がある。
【０００４】
実問題における制約充足問題では、解を生成する対象となるシステム上変更できない、必ず充足すべき不変制約と、ユーザがシステムに要求する機能・性能など柔軟に変更できる可変制約に分けることができる。
【０００５】
上記のような場合に、事前に分類が決定している制約に対して、ユーザが自由に制約を選択した状況下で最適解を求めたい、との課題がある。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開平８−１２９５８２号公報
【特許文献２】特開平７−６４９６７号公報
【特許文献３】特開平５−１６５９００号公報
【特許文献４】特開平６−２４３１２０号公報
【発明の概要】
【発明が解決しようとする課題】
【０００７】
本発明が解決しようとする課題は、可変制約に分類を付与することで、全制約を満たせなかった場合は、ユーザが選別した特定分類の可変制約を満たす解を生成することのできる制約充足解生成装置を提供することである。
【課題を解決するための手段】
【０００８】
実施形態の制約充足解生成装置は、対象となるシステムに要求される制約のうち、ユーザが変更可能であって分類を付与した制約を充足する割合を表す制約充足度を評価するための評価情報を入力する入力部と、前記入力部で入力した評価情報を記憶する記憶部と、前記制約充足度を評価するためのモデル検査用プログラムの生成で用いる関数を保持する関数ライブラリと、前記評価情報を元に、前記関数ライブラリに保持している関数を利用して、前記モデル検査用プログラムと、モデル検査のための検証式を生成するプログラム生成部と、前記モデル検査用プログラムを、前記検証式を用いてモデル検査により検証し、与えられた制約に対して最適となる組み合わせを表す最適解の組み合わせと、生成された前記最適解に対して、各制約を充足しているかどうかを表す制約充足結果とを求める探索部と、を備える。
【図面の簡単な説明】
【０００９】
【図１】第１の実施形態に係る制約充足解生成装置の構成例を示す図である。
【図２】制約リストの一例を示す図である。
【図３】属性値リストの一例を示す図である。
【図４】動作仕様表の一例を示す図である。
【図５】動作仕様表、属性値リスト、制約リストの関係を示す図である。
【図６】最適解の組み合わせの一例を示す図である。
【図７】制約充足結果の一例を示す図である。
【図８】第１の実施形態に係る制約充足解生成装置による制約充足解の生成処理の流れを示すフローチャートである。
【図９】モデル検査用プログラムと検証式の生成処理の流れを示すフローチャートである。
【図１０】“OSメモリ保護”の実施例をイメージ化した図である。
【図１１】“OSメモリ保護”の実施例をイメージ化した図である。
【図１２】生成されたモデル検査用プログラムの構成を示す図である。
【図１３】生成されたモデル検査用プログラムの構成の一例を示す図である。
【図１４】制約設定関数の定義化の一例を示す図である。
【図１５】属性値設定関数の定義化の一例を示す図である。
【図１６】動作結果取得関数の定義化の一例を示す図である。
【図１７】制約充足度評価関数の一例を示す図である。
【図１８】検証式変更の一例を示す図である。
【発明を実施するための形態】
【００１０】
以下、本発明の一実施の形態について、図面を参照して説明する。尚、各図において同一箇所については同一の符号を付すとともに、重複した説明は省略する。
【００１１】
まず、本実施形態で用いる主要な用語について説明する。
【００１２】
「制約充足解」とは、制約を充足する解（それらの制約の組み合わせ）をいう。
【００１３】
「制約充足度」とは、全制約に対して、ユーザが変更可能であって分類を付与した制約の充足する割合をいう。
【００１４】
「制約充足結果」とは、生成された最適解に対して、各制約を充足しているかどうかの結果をいう。
【００１５】
「最適解の組み合わせ」とは、与えられた制約に対して最適解となる充足度を評価する評価情報の組み合わせをいう。
【００１６】
本実施形態に係る制約充足解生成装置は、演算処理装置（ＣＰＵ）、主メモリ（ＲＡＭ）、読出し専用メモリ（ＲＯＭ）、入力装置（例えば、キーボード、操作パネルなど）、ハードディスク装置や半導体メモリであるフラッシュメモリを使用したソリッドステートドライブ（ＳＳＤ）装置等の記憶装置を具備したパーソナル・コンピュータやワークステーション等の汎用計算機を用いることができ、制約充足解生成支援用の処理プログラムをインストールすることにより実現できる。
【００１７】
本実施形態では、非決定的（ランダム）に選択した変数の組み合わせの制約充足度を評価するモデルを生成し、「解はない」という命題を網羅的に検証して、反例を挙げることで最適解を生成する。可変制約に分類を付与することで、全制約を満たせなかった場合は、ユーザが選別した特定分類の可変制約を満たす解を生成する。解探索にモデル検査の機構を利用して最適解を生成する。
【００１８】
図１は、実施形態に係る制約充足解生成装置の構成例を示す図である。実施形態に係る制約充足解生成装置１００は、主として制約の充足度を評価する評価情報を入力する入力部１１と、入力した評価情報を記憶する記憶部１２と、プログラム生成部１３と、関数ライブラリ１４と、探索部１５から構成されている。
【００１９】
入力部１１は、制約の充足度を評価する評価情報を入力するものである。評価情報としては、制約情報、属性情報、動作仕様が好適である。
【００２０】
制約情報は、例えば、特定の制約に対して条件・結果・分類の変数値の集合である制約情報を記述した「制約リスト」である。「制約リスト」は、制約を「(条件１)＆・・・＆(条件Ｎ)の場合、(結果１) ＆・・・＆(結果Ｎ)になる」と定義したときの各制約要素が持つべき値と、その制約の分類を列挙した各制約毎のリストである。
【００２１】
解を生成する対象となるシステム上変更できない、必ず満たすべき不変制約と、ユーザがシステムに要求する機能・性能など柔軟に変更できる可変制約に制約を分け、可変制約に分類を付与することで、全制約を満たせなかった場合は、ユーザが選別した特定分類の可変制約を満たす解を生成する。
【００２２】
分類は、ユーザが自由に利用することができる。例えば、優先度、機能による分類などである。図２は、制約リストの一例を示す図である。図２に示す制約リストでは、制約毎に、制約要素として条件・結果、及び分類（優先度）がリスト化されている。
【００２３】
属性情報は、例えば、「属性値リスト」や「組み合わせ数」である。「属性値リスト」は、対象システムに設定する可変のもので、属性が取り得る値（候補値）を列挙し各属性毎にリスト化したものである。「組み合わせ数」は、属性値の組み合わせをいくつまで設定可能かを示す上限値である。図３は、属性値リストの一例を示す図である。
【００２４】
動作仕様は、例えば、対象システムの持つ変数定義情報と、対象システムの挙動を変数間の関係で表した、ドメイン固有の動作仕様を記述した「動作仕様表」である。すなわち、動作仕様表は、属性情報・制約情報の変数仕様と、ある動作結果を出す上での各属性・制約要素の取る値を列挙した各動作仕様毎のリストである。図４は、動作仕様表の一例を示す図である。図４に示す例では、属性・条件・結果の変数名及び属性・条件・結果のデータ型が各変数仕様の定義情報としてリスト化され、対応する各動作仕様の定義情報がリスト化されている。動作仕様の定義情報においては、動作結果を出す上で「true」となる条件式を記述する。条件式は、「等号ｏｒ不等号」＋「値ｏｒ変数」で表す。
【００２５】
動作仕様表では、全ての動作仕様を書きだす必要はなく、初期仕様と異なる結果を出す動作仕様だけを並べたコンパクトな表にする。ここで、動作仕様は、属性、制約要素などシステムの変数間関係からどういう動作結果になるか、システムの挙動を示すものである。初期仕様は、制約要素・結果の初期値である。システムが動作仕様に一致しない動作をする場合は、初期値が動作結果になる。
【００２６】
図５は、動作仕様表、属性値リスト、制約リストの関係を示す図である。図５に示すように、動作仕様表から各属性の候補値としてリスト化したものとして属性値リストが成立し、動作仕様表からある制約における制約要素毎の固定値としてリスト化したものとして制約リストが成立している。
【００２７】
入力部１１は、ユーザが操作することにより制約に関する情報を送信する装置で、例えば、キーボードやマウス等で構成することができる。
【００２８】
記憶部１２は、動作仕様記憶部１２１、制約情報記憶部１２２、属性情報記憶部１２３から構成される。動作仕様記憶部１２１は、「動作仕様表」を取得し、記憶するものである。制約情報記憶部１２２は、「制約リスト」を取得し、記憶するものである。属性情報記憶部１２３は、属性情報である「属性値リスト」や「組み合わせ数」を取得し、記憶するものである。
【００２９】
プログラム生成部１３は、制約情報・属性情報・動作仕様を元に、関数ライブラリ１４から後述する関数を利用して、制約充足度を評価するためのモデル検査用プログラムと、モデル検査のための検証式を生成するものである。
【００３０】
関数ライブラリ１４は、モデル検査用プログラムの生成で用いる、制約充足度評価関数(メイン関数)、制約設定関数、属性値設定関数、動作結果取得関数を保持するものである。制約充足度評価関数は、制約の充足度を評価するための関数である。
【００３１】
制約充足度評価関数は、例えば、属性値の組み合わせを非決定的に選択する部分、入力した動作仕様表によって、各制約ごとに現在の組み合わせで得られる動作結果を算出する部分、制約通りならば、制約の優先度毎にポイントを加算する部分から構成することができる。
【００３２】
制約設定関数は、制約を設定するための関数である。制約設定関数は、例えば、入力した制約リストによる各制約保持変数への固定値の設定を行う部分、分類1の制約の設定を行う部分、分類２の制約の設定を行う部分等から構成することができる。
【００３３】
属性値設定関数は、属性値を設定するための関数である。属性値設定関数は、例えば、組み合わせ数分だけ属性値を設定する部分、属性1を候補値から非決定的に設定する部分、属性２を候補値から非決定的に設定する部分等から構成することができる。
【００３４】
動作結果取得関数は、動作結果を取得するための関数である。動作結果取得関数は、入力した動作仕様表に基づいて生成されたIf文による分岐を持つ関数とするのが好適である。動作結果取得関数は、例えば、まず[=〜]関係の属性値によって分岐させる部分、その後、各属性値毎に分岐させる部分、動作仕様表に記述された仕様を満たす動作結果を得る部分等から構成することができる。
【００３５】
関数ライブラリ１４は、さらに検証式の生成で用いる検証式定義関数を保持する。検証式定義関数は、検証式を定義する関数である。
【００３６】
探索部１５は、プログラム生成部１３において生成したモデル検査用プログラムを、同様に生成した検証式を用いてモデル検査により検証し、反例として“最適解の組み合わせ”と“制約充足結果”を出力する。最適解の組み合わせは、与えられた制約に対して最適解となる属性値の組み合わせである。制約充足結果は、生成された最適解に対して、各制約を充足しているかどうかの結果である。制約充足結果は、優先度が高い制約に重点を置く際に、優先度が低い制約の内、満たしているものや満たしていないものがある場合に利用するのが好適である。モデル検査のためのツールとしては、オートマトンベースのモデルチェッカであるＳＰＩＮ（登録商標）を利用することができる。
【００３７】
図６は、最適解の組み合わせの一例を示す図である。図７は、制約充足結果の一例を示す図である。
【００３８】
次に、以上のように構成された制約充足解生成装置１００による制約充足解の生成について説明する。図８は、第１の実施形態に係る制約充足解生成装置による制約充足解の生成処理の流れを示すフローチャートである。
【００３９】
まず、入力部１１から、図２〜図４に示すような制約充足度評価情報を入力する（ステップＳ８０１）。入力した制約充足度評価情報は、記憶部１２で保持される（ステップＳ８０２）。
【００４０】
次いで、プログラム生成部１３においてモデル検査用プログラムと検証式を生成する（ステップＳ８０３）。これらの詳細については、後述する。
【００４１】
次に、探索部１５において、モデル検査用プログラムと検証式の検証を行う（ステップＳ８０４）。本実施形態では「全ての制約を満たす(評価が満点の)属性値の組み合わせはない」と検証する。網羅的に検証して、反例として出てきた組み合わせが最適解である。
【００４２】
次いで、反例として最適解を生成したか否かを判定する（ステップＳ８０５）。
【００４３】
最適解が生成できなければ（ステップＳ８０５でＮｏ）、分類の選別の仕方を全て網羅したかを判定する（ステップＳ８０６）。
【００４４】
分類の選別の仕方を全て網羅していれば（ステップＳ８０６でＹｅｓ）、特定分類を選択するよう検証式を変更し（ステップＳ８０７）、ステップＳ８０４に戻る。
【００４５】
分類の選別の仕方を全て網羅していなければ（ステップＳ８０６でＮｏ）、制約リストを変更（ステップＳ８０８）し、ステップＳ８０１に戻る。
【００４６】
一方、最適解を生成したならば（ステップＳ８０５でＹｅｓ）、他の最適解を生成するかを判定する（ステップＳ８０９）。他の最適解を生成するのであれば（ステップＳ８０９でＹｅｓ）、生成した解を除くよう検証式を変更し（ステップＳ８１０）、ステップＳ８０４に戻る。他の最適解を生成しないならば（ステップＳ８０９でＮｏ）、終了する。
【００４７】
次に、プログラム生成部１３におけるモデル検査用プログラムと検証式の生成処理の流れについて説明する。図９は、モデル検査用プログラムと検証式の生成処理の流れを示すフローチャートである。
【００４８】
まず、動作仕様表に基づいて、制約を保持する構造体変数と、属性値を保持する構造体変数を作成する（ステップＳ９０１）。
【００４９】
次いで、関数ライブラリ１４から得た制約設定関数に、図２に示すような制約リストの値を設定する（ステップＳ９０２）。
【００５０】
次に、関数ライブラリ１４から得た属性値設定関数に、図３に示すような属性値リストと組み合わせ数の値を設定する（ステップＳ９０３）。
【００５１】
次いで、関数ライブラリ１４から得た動作結果取得関数に、図４に示すような動作仕様表の値を設定する（ステップＳ９０４）。
【００５２】
次いで、関数ライブラリ１４から得た制約充足度評価関数に、図２に示すような制約リストの値を設定する（ステップＳ９０５）。
【００５３】
一方、関数ライブラリ１４から得た検証式定義関数に、図２に示すような制約リストの値を設定する（ステップＳ９０６）。
【００５４】
（実施例）
以上のように構成された制約充足解生成装置において、“OSメモリ保護”を事例にとって、制約充足解の生成の例を説明する。この例では、「OSの制約(仕様)を満たすように、 プロセッサ上で8つのリージョンに対してアクセス権の設定を行う」ことが不変制約として設定される。すなわち、「OSのスタックへの書き込みがあった場合、必ずアクセスを防ぐ」ことが制約となる。
【００５５】
制約を「(条件1:target)&(条件2:request)の場合、(結果:memory Access)になる」として考える。属性を「属性1:region」、「属性2:access Right」として、これらの組み合わせの最適解を求める。組み合わせの上限は8つであり、モデル検査ツールＳＰＩＮ（登録商標）を利用する。
【００５６】
図１０、図１１はいずれも“OSメモリ保護”の実施例をイメージ化した図である。
【００５７】
図１０に示すように、制約リストにおいては、制約毎に条件、結果、分類（優先度）をリスト化している。この実施例では、組み合わせの数は、上限数として“８”を設定している。また、属性値リストにおいては、属性毎に候補値をリスト化している。
【００５８】
図１１に示すように、動作仕様表においては、属性、制約要素として条件、結果毎に、変数名、データ型、動作仕様、初期仕様をリスト化している。動作仕様表は、必ずしも全ての組合わせの関係を表記する必要はなく、制約要素・結果の値がデフォルトから変化する組み合わせを表記することで足りる。動作仕様表は、換言すれば、動作仕様を方程式R(x,y,u,v)=wとしたとき、制約要素(u,v,w)を与えたときに、R(x,y,u,v)=wを満たす属性値(x,y)を生成するものとして捉えることができる。図１１の動作仕様表中、「[=〜]」は「〜」の変数同士が同値であればよく、「／」は結果に関係ないことを表している。
【００５９】
図１１に示すように、制約充足解生成装置１００は、上記の制約情報を入力し、関数ライブラリ１４から取得した関数を利用して、モデル検査用プログラム及び検証式を生成する。
【００６０】
図１２は、生成されたモデル検査用プログラムの構成を示す図である。図１２に沿ってモデル検査用プログラムの流れを説明する。まず、属性値と制約を保持する構造体変数の配列をグローバル変数として定義する（ステップＳ１２０１）。図１３は、生成されたモデル検査用プログラムの構成の一例を示している。
【００６１】
次いで、制約設定関数の定義を行い（ステップＳ１２０２）、属性値設定関数の定義を行い（ステップＳ１２０３）、動作結果取得関数の定義を行う（ステップＳ１２０４）。尚、ステップＳ１２０２からステップＳ１２０４は、順不同である。図１４は、制約設定関数の定義化の一例を示している。図１５は、属性値設定関数の定義化の一例を示している。図１６は、動作結果取得関数の定義化の一例を示している。
【００６２】
次いで、制約設定関数を呼び出し、各変数に入力値を設定する（ステップＳ１２０５）。次に、属性値設定関数を呼び出し、非決定的に属性値の組み合わせを設定する（ステップＳ１２０６）。次に、制約要素・条件を引数として、動作結果取得関数を呼び出し、設定した属性値からの結果を得る（ステップＳ１２０７）。その結果が制約Aを満たすかどうかを判定し加点する（ステップＳ１２０８）。尚、ステップＳ１２０７及びステップＳ１２０８は、制約数分、繰り返される。図１７は、制約充足度評価関数の一例を示している。
【００６３】
モデル検査用プログラム及び検証式はモデル検査ツールで検証する。検証結果として、制約充足結果及び最適解の組み合わせが出力される。
【００６４】
例えば、「！<>(ｐｏｉｎｔ１==優先度１制約数＆＆ｐｏｉｎｔ２==優先度２制約数)」という検証式で網羅的に検証して、反例として出てきた、全ポイントを獲得した属性値の組み合わせが最適解となる。
【００６５】
モデル検査ツールで検証した結果、“反例なし”あるいは“反例は出たが他の解も出したい”場合には、検証式の変更を行うことが好適である。図１８は、検証式変更の一例を示す図である。
【００６６】
“反例は出たが他の解も出したい”場合には、検証式と検証式定義部分を変更して再検証を実行する。他の最適解を生成するには、例えば上記検証式を「!<>(p && q && !r)」と変更し、定義部分に「#define r rule[0].region == … && … &&」と生成された最適解の変数値を記述する。
【００６７】
“反例なし”の場合には、検証式定義部分を変更して再検証を実行する。例えば、優先度1だけを満たす最適解を生成する場合には、「#define q point2 == 0」に変更する。優先度1を全て満たし、優先度2を3つ以上満たす最適解を生成する場合には、「#define q point2 >= 3」に変更する。
【００６８】
本実施形態によれば、可変制約に分類を付与することで、全制約を満たせなかった場合は、ユーザが選別した特定分類の可変制約を満たす解を生成することができる。また、過制約でない限り、充足しなくてもよい制約がなくても制約を充足する解を探索できる。
【００６９】
本発明のいくつかの実施形態を説明したが、これらの実施形態は、例として提示したものであり、発明の範囲を限定することは意図していない。これら新規な実施形態は、その他の様々な形態で実施されることが可能であり、発明の要旨を逸脱しない範囲で、種々の省略、置き換え、変更を行うことができる。これら実施形態やその変形は、発明の範囲や要旨に含まれるとともに、特許請求の範囲に記載された発明とその均等の範囲に含まれる。
【符号の説明】
【００７０】
１００・・・制約充足解生成装置
１１・・・入力部
１２・・・記憶部
１３・・・プログラム生成部
１４・・・関数ライブラリ
１５・・・探索部
【図１】
2014086022.tif 000003
【図２】
2014086022.tif 000004
【図３】
2014086022.tif 000005
【図４】
2014086022.tif 000006
【図５】
2014086022.tif 000007
【図６】
2014086022.tif 000008
【図７】
2014086022.tif 000009
【図８】
2014086022.tif 000010
【図９】
2014086022.tif 000011
【図１０】
2014086022.tif 000012
【図１１】
2014086022.tif 000013
【図１２】
2014086022.tif 000014
【図１３】
2014086022.tif 000015
【図１４】
2014086022.tif 000016
【図１５】
2014086022.tif 000017
【図１６】
2014086022.tif 000018
【図１７】
2014086022.tif 000019
【図１８】
2014086022.tif 000020