# HG changeset patch
# User soto <soto@cr.ie.u-ryukyu.ac.jp>
# Date 1653572363 -32400
# Node ID 517b22769bf7bed45720d3865fc43579166452cd
# Parent  c3f937a26b260cad73cad62d1f718d77deb1b423
FIX

diff -r c3f937a26b26 -r 517b22769bf7 slide/slide.md
--- 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なモデル検査)
diff -r c3f937a26b26 -r 517b22769bf7 slide/slide.pdf
Binary file slide/slide.pdf has changed