Mercurial > hg > Papers > 2022 > soto-sigos
changeset 13:517b22769bf7
FIX
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 26 May 2022 22:39:23 +0900 |
| parents | c3f937a26b26 |
| children | ba98083f9853 |
| files | slide/slide.md slide/slide.pdf |
| diffstat | 2 files changed, 2 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/slide/slide.md Thu May 26 21:43:41 2022 +0900 +++ b/slide/slide.md Thu May 26 22:39:23 2022 +0900 @@ -102,7 +102,7 @@ - 型の定義部分で、入力と出力の型を定義できる - input → output のようになる - 関数の定義は = を用いて行う - - 関数名の後ろの行で、 = の前で受け取る引数を記述、=の後ろで実装を記述します + - 関数名の後ろの行で、 = の前で受け取る引数を記述、=の後ろで実装を記述する <!-- curry-Houerd対応 @@ -160,9 +160,8 @@ # Dining Philosophers Program の記述 - DPPはマルチプロセスの同期問題である - しかし、Agdaでは並列実行をサポートしていないため、step実行毎に一つづつ処理することで並列実行を表現している - - 加えて、哲学者が思考中に食事をし始めるのか、食事中に思考に戻ろうとするのかで分岐が発生する - - これを網羅するために今回はその状態に対して網羅することでモデル検査をboundedに行っている + - 今回はその状態に対して網羅することでモデル検査をboundedに行っている # モデル検査でのデッドロック検知 - 現在は探索する深さを指定している(boundedなモデル検査)