diff Paper/master_paper.tex @ 3:c28e8156a37b

Add paper init~agda
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Fri, 20 Jan 2023 13:40:03 +0900
parents a72446879486
children eaef105dff41
line wrap: on
line diff
--- a/Paper/master_paper.tex	Thu Jan 12 20:31:09 2023 +0900
+++ b/Paper/master_paper.tex	Fri Jan 20 13:40:03 2023 +0900
@@ -138,6 +138,9 @@
 加えて、CbCでは並列処理も実行できる\cite{parusu-master}が、
 並列処理を定理証明にて検証するには考慮する状態が多すぎる。
 そのため、並列処理はモデル検査にて検証する。
+\section{モデル検査とは}
+\section{SPINによるモデル検査}% 内容にそぐわない場合は使わない
+\section{Gears Agdaによるモデル検査の流れ}
 
 \input{tex/dpp_impl.tex}% Gears Agda の記法 loopのやつやる