Mercurial > hg > Papers > 2023 > soto-master

comparison Paper/tex/dpp_impl.tex @ 5:eaef105dff41

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add paper dpp
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Sat, 21 Jan 2023 17:57:20 +0900
parents 4f5dde4cff0b
children 8c1e9a6d58e2
comparison
equal deleted inserted replaced
4:4f5dde4cff0b 5:eaef105dff41
105 これまでの実装は一般的なDPPの実装であったため、 105 これまでの実装は一般的なDPPの実装であったため、
106 Code / Data Gear の実装であった。 106 Code / Data Gear の実装であった。
107 ここからは、モデル検査を行うため、Meta Data Gear の定義をし、 107 ここからは、モデル検査を行うため、Meta Data Gear の定義をし、
108 それの操作を行う Meta Code Gear の実装を行っていく。 108 それの操作を行う Meta Code Gear の実装を行っていく。
109 109
110 以下がMeta Code Gear の定義になる 110 以下\coderef{dpp-mdg}がMeta Code Gear の定義になる
111 111
112 % ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける 112 % ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける
113 \lstinputlisting[caption=Gears Agdaでの DPP モデル検査を行うための Meta Data Gear の定義, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced}
113 114
114 この Meta Data Gear の説明をすると、 115 この Meta Data Gear の説明をすると、
115
116 metadataは状態の分岐数を持っておくnum-brunchがある。 116 metadataは状態の分岐数を持っておくnum-brunchがある。
117
118 MetaEnv はもとの DataGear を保持するDG(Data Gearの省略) 117 MetaEnv はもとの DataGear を保持するDG(Data Gearの省略)
119 meta に 前述したmetadataを持っており、 118 meta に 前述したmetadataを持っており、
120 他には、deadlockしているかのフラグである deadlock 、 119 他には、deadlockしているかのフラグである deadlock 、
121 最後の2つは後述する際に必要になる。 120 最後の2つは後述する際に必要になる。
122 そのstate が step 実行済みなのかのフラグであるis-step、 121 そのstate が step 実行済みなのかのフラグであるis-step、
127 126
128 deadlockの検出方法として、状態の分岐数を保存するnum-brunchをmetadataに持つようにした。 127 deadlockの検出方法として、状態の分岐数を保存するnum-brunchをmetadataに持つようにした。
129 128
130 そしてnum-brunchの値が1であるということは、それ以上の状態に移動することができないとして、この状態をdead lockであると定義した。 129 そしてnum-brunchの値が1であるということは、それ以上の状態に移動することができないとして、この状態をdead lockであると定義した。
131 130
132 以下のソースコードがdead-lockを検知する関数となる 131 以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる
133 132
134 複雑なことは何もしておらず、単純にstate毎のnum-brunchの値を見て 133 複雑なことは何もしておらず、単純にstate毎のnum-brunchの値を見て
135 deadlockのフラグを立ち上げている。 134 deadlockのフラグを立ち上げている。
136 135
137 % judge-dead-lock-pのソースコードを貼り付ける 136 % judge-dead-lock-pのソースコードを貼り付ける
137 \lstinputlisting[caption=DPP での dead lock を検知する Meta Code Gear, label=code:dpp-judge-mcg]{src/dpp-verif/judge-deadlock.agda.replaced}
138 % こいつはmetaEnv2を受け取れるように変えないと行けない
138 139
139 ここから前述した通り、State Listを作成する。 140 ここから前述した通り、State Listを作成する。
140 141
141 そのまま実行するだけでは無限に実行されるのみで停止しないと思われる。 142 そのまま実行するだけでは無限に実行されるのみで停止しないと思われる。
142 しかし、分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる。 143 しかし、分岐後に step 実行後の state を保存している State List に同じ State が存在しないかを確かめる。
143 存在していた場合はそれを追加せず、存在しなかった場合にのみ State を追加する。 144 存在していた場合はそれを追加せず、存在しなかった場合にのみ State を追加する。
144 145
145 Agdaには2つの record が等しい場合の分岐など存在しないため、 146 Agdaには2つの record が等しい場合の分岐など存在しないため、
146 以下のソースコードのようにrecordの中身を一つづつ一致しているか確認する。 147 \coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つづつ一致しているか確認する。
148 こちらはそのまま掲載すると長いので、実際のコードに手を加えて省略している。実際のコードは付録にて参照できる。
147 149
148 これで、 150 \lstinputlisting[caption=重複しているstateを除外する Meta Code Gear, label=code:dpp-exclude-state-mcg]{src/dpp-verif/exclude-same-env.agda.replaced}
149 まだ分岐を見ていない1つのStateの分岐を確かめる。 151 % 手を加えているので詳細は付録を参照するように促す
152
153 MetaEnv2 を受け取ってその中身の state を比較するが、そこまで展開する必要がある。
154 loop-metaenv と loop-target-metaenv, eq-env にてそれを行っている。
155
156 更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し、次のstateの一致を探索するように記述されている。
157
158 実際にstateの一致を見ているのは22行目のeq-env関数で、一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている
159
160 State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている。
161 その値が一致している場合には別の値を見て、一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている。
162 他の値である、lhandやrhandなども同じように記述している。
163
164 これらにて、まだ分岐を見ていない1つのStateの分岐を確かめる。
150 発生した分岐を step 実行させる。 165 発生した分岐を step 実行させる。
151 step実行して作成された state が State Listに存在していないかを確かめる。 166 step実行して作成された state が State Listに存在していないかを確かめる。
152 これを繰り返すことで State Listを作る。 167 これを繰り返すことで State Listを作る。
153 State List に存在している全ての state の分岐を見たということは、 168 State List に存在している全ての state の分岐を見たということは、
154 出現するStateを全て網羅することができたと言える。 169 出現するStateを全て網羅することができたと言える。