Mercurial > hg > Papers > 2023 > soto-master
changeset 5:eaef105dff41
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 |
| files | Paper/Makefile Paper/master_paper.pdf Paper/master_paper.sty Paper/master_paper.tex Paper/src/dpp-verif/ModelChecking.agda Paper/src/dpp-verif/dpp-metadata.agda Paper/src/dpp-verif/exclude-same-env.agda Paper/src/dpp-verif/judge-deadlock.agda Paper/tex/dpp_impl.tex Paper/tex/while_loop.tex |
| diffstat | 10 files changed, 885 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/Paper/Makefile Fri Jan 20 15:20:31 2023 +0900 +++ b/Paper/Makefile Sat Jan 21 17:57:20 2023 +0900 @@ -36,7 +36,7 @@ open $(TARGET).pdf clean: - rm -f *.dvi *.aux *.log *.ilg *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx src/*.replaced *.fdb_latexmk *.fls + rm -f *.dvi *.aux *.log *.ilg *.ps *.gz *.bbl *.blg *.toc *~ *.core *.cpt *.lof *.lot *.lol *.bbl *.blg *.idx src/*/*.replaced *.fdb_latexmk *.fls remake: make clean
--- a/Paper/master_paper.sty Fri Jan 20 15:20:31 2023 +0900 +++ b/Paper/master_paper.sty Sat Jan 21 17:57:20 2023 +0900 @@ -111,8 +111,8 @@ \def\edepartment{Graduate School of Engineering and Science} % 専攻 -\def\course{情報工学専攻} -\def\ecourse{Information Engineering Course} +\def\course{知能情報プログラム} +\def\ecourse{Computer Science and Intelligent Systems} % 署名 \def\commission{論 文 審 査 会} @@ -194,7 +194,7 @@ \newcommand{\makecommission} { \noindent 論文題目: Gears Agda による形式手法 \newline\newline - 氏\hspace{4ex}名: 上地 悠斗 + 氏\hspace{4ex}名: 上地 悠斗 \vspace*{4.5cm} \begin{center} 本論文は、修士(工学)の学位論文として適切であると認める。 @@ -209,16 +209,16 @@ \bf\commission \vskip 3 em \underline{ 印}\\ - (主 査) 和田 知久 + (主 査) 和田 知久 \vskip 2 em \underline{ 印}\\ - (副 査) 名嘉村 盛和 + (副 査) 赤嶺 有平 \vskip 2 em \underline{ 印}\\ - (副 査) 當間 愛晃 + (副 査) 山田 孝治 \vskip 2 em \underline{ 印}\\ - (副 査) 河野 真治 + (副 査) 河野 真治 \end{center} \end{minipage} } @@ -251,7 +251,7 @@ \else\@restonecolfalse\fi \chapter*{\contentsname \@mkboth{\contentsname}{\contentsname}% - } \pagenumbering{arabic}\@starttoc{toc}% + } \pagenumbering{roman}\@starttoc{toc}% \if@restonecol\twocolumn\fi }
--- a/Paper/master_paper.tex Fri Jan 20 15:20:31 2023 +0900 +++ b/Paper/master_paper.tex Sat Jan 21 17:57:20 2023 +0900 @@ -18,21 +18,19 @@ %\input{dummy.tex} %% font \jtitle{Gears Agda での形式手法} -\etitle{} % +\etitle{Formal Methods in Gears Agda} % \year{2023年 3月} -\eyear{March 2022} +\eyear{March 2023} \author{上地 悠斗} \eauthor{Yuto Uechi} \chife{指導教員：教授 和田 知久} \echife{Supervisor: Prof. Tomohisa Wada} - \marklefthead{% 左上に挿入 \begin{minipage}[b]{.4\textwidth} 琉球大学大学院学位論文(修士) \end{minipage}} - % \markleftfoot{% 左下に挿入 % \begin{minipage}{.8\textwidth} % Gears OS の Paging @@ -85,11 +83,11 @@ \begin{document} %rome \maketitle - +\pagenumbering{roman} +\setcounter{page}{0} \newpage -\pagenumbering{roman} -\setcounter{page}{0} + \makecommission %\input{chapter/signature.tex} @@ -142,6 +140,8 @@ \section{SPINによるモデル検査}% 内容にそぐわない場合は使わない \section{Gears Agdaによるモデル検査の流れ} +% Gears Agdaの場合はListの方が停止することがわかりやすいので、今回はState Listを作成した。本来はburanceされたtree structureが最も良い + \input{tex/dpp_impl.tex}% Gears Agda の記法 loopのやつやる \chapter{今後の展望}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/dpp-verif/ModelChecking.agda Sat Jan 21 17:57:20 2023 +0900 @@ -0,0 +1,780 @@ +module ModelChecking where + +open import Level renaming (zero to Z ; suc to succ) + +open import Data.Nat hiding (compare) +open import Data.Nat.Properties as NatProp +open import Data.Maybe +-- open import Data.Maybe.Properties +open import Data.Empty +open import Data.List +open import Data.Product +open import Function as F hiding (const) +open import Relation.Binary +open import Relation.Binary.PropositionalEquality +open import Relation.Nullary +open import logic +open import Data.Unit hiding (_≟_ ; _≤?_ ; _≤_) +open import Relation.Binary.Definitions + +record AtomicNat : Set where + field + value : ℕ + +set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t +set a v next = next record { value = v } + +record Phils : Set where + field + pid : ℕ + left right : AtomicNat + +putdown_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t +putdown_rfork p next = set (Phils.right p) 0 ( λ f → next record p { right = f } ) + +putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t +putdown_lfork p next = set (Phils.left p) 0 ( λ f → next record p { left = f } ) + +thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t +thinking p next = next p + +pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t +pickup_rfork p next = set (Phils.right p) (Phils.pid p) ( λ f → next record p { right = f } ) + +pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t +pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → next record p { left = f } ) + +--eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t +--eating p next = next p + +data Code : Set where +-- C_set : Code + C_putdown_rfork : Code + C_putdown_lfork : Code + C_thinking : Code + C_pickup_rfork : Code + C_pickup_lfork : Code + C_eating : Code + +record Process : Set where + field + phil : Phils + next_code : Code + +putdown_rfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t +putdown_rfork_stub p next = putdown_rfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } ) + +putdown_lfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t +putdown_lfork_stub p next = putdown_lfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } ) + +{- +code_table : {n : Level} {t : Set n} → Code → Process → ( Process → t) → t +-- code_table C_set = {!!} +code_table C_putdown_rfork = putdown_rfork_stub +code_table C_putdown_lfork = putdown_lfork_stub +code_table C_thinking = {!!} +code_table C_pickup_rfork = {!!} +code_table C_pickup_lfork = {!!} +code_table C_eating = {!!} +-} + +open Process + +--step : {n : Level} {t : Set n} → List Process → (List Process → t) → t +--step {n} {t} [] next0 = next0 [] +--step {n} {t} (p ∷ ps) next0 = code_table (next_code p) p ( λ np → next0 (ps ++ ( np ∷ [] ) )) + +--test : List Process +--test = step ( record { phil = record { pid = 1 ; left = record { value = 1 } ; right = record { value = 1 } } ; next_code = C_putdown_rfork } ∷ [] ) ( λ ps → ps ) + +--test1 : List Process +--test1 = step ( record { phil = record { pid = 1 ; left = record { value = 1 } ; right = record { value = 1 } } ; next_code = C_putdown_rfork } ∷ [] ) +-- $ λ ps → step ps $ λ ps → ps + +record Phi : Set where + field + pid : ℕ + right-hand : Bool + left-hand : Bool + next-code : Code +open Phi + +record Env : Set where + field + table : List ℕ + ph : List Phi +open Env + +init-table : {n : Level} {t : Set n} → ℕ → (exit : Env → t) → t +init-table n exit = init-table-loop n 0 (record {table = [] ; ph = []}) exit where + init-table-loop : {n : Level} {t : Set n} → (redu inc : ℕ) → Env → (exit : Env → t) → t + init-table-loop zero ind env exit = exit env + init-table-loop (suc redu) ind env exit = init-table-loop redu (suc ind) record env{ + table = 0 ∷ (table env) + ; ph = record {pid = redu ; left-hand = false ; right-hand = false ; next-code = C_thinking } ∷ (ph env) } exit + +-- eatingも探索範囲に含める +brute-force-search : {n : Level} {t : Set n} → Env → (exit : List Env → t) → t +brute-force-search env exit = make-state-list 1 [] (ph env) env (env ∷ []) exit where + make-state-list : {n : Level} {t : Set n} → ℕ → List Bool → List Phi → Env → (List Env) → (exit : List Env → t) → t + make-state-list redu state (x ∷ pl) env envl exit with next-code x + ... | C_thinking = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit + ... | C_eating = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit + ... | _ = make-state-list redu state pl env envl exit + make-state-list redu state [] env envl exit = bit-force-search redu [] state env envl exit where + bit-force-search : {n : Level} {t : Set n} → ℕ → (f b : List Bool )→ Env → (List Env) → (exit : List Env → t) → t + bit-force-search zero f l env envl exit = exit envl + bit-force-search (suc redu) f [] env envl exit = exit envl + bit-force-search (suc redu) f (true ∷ bs) env envl exit = bit-force-search (suc redu) (f ++ (false ∷ [])) bs env envl exit -- 今回の対象をfalseにしてfに追加,bを次の対象にする + bit-force-search (suc redu) f (false ∷ bs) env envl exit = set-state redu (f ++ (true ∷ bs)) (f ++ (true ∷ bs)) [] (ph env) env envl exit where -- 今回の対象をtrueにし、fとbを結合してそのListを代入する。かつそれをbに入れfをinitしてloopさせる + set-state : {n : Level} {t : Set n} → ℕ → (origin state : List Bool ) → (f b : List Phi) → Env → (List Env) → (exit : List Env → t) → t -- 入れ替える必要のあるやつはphaseがThinkingのやつのみ + set-state redu origin [] f b env envl exit = bit-force-search redu [] origin env (record env{ph = (f ++ b)} ∷ envl) exit -- Stateが先に尽きる + set-state redu origin state@(s ∷ ss) f b env envl exit with b + ... | [] = bit-force-search redu [] origin env (record env{ph = f} ∷ envl) exit + ... | p ∷ ps with next-code p + set-state redu origin (true ∷ ss) f b env envl exit | p ∷ ps | C_eating = set-state redu origin ss (f ++ (record p{next-code = C_putdown_lfork} ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む + set-state redu origin (false ∷ ss) f b env envl exit | p ∷ ps | C_eating = set-state redu origin ss (f ++ (p ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む + set-state redu origin (true ∷ ss) f b env envl exit | p ∷ ps | C_thinking = set-state redu origin ss (f ++ (record p{next-code = C_pickup_rfork} ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む + set-state redu origin (false ∷ ss) f b env envl exit | p ∷ ps | C_thinking = set-state redu origin ss (f ++ (p ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む + set-state redu origin (s ∷ ss) f b env envl exit | p ∷ ps | _ = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする + + +test-search : List Env +test-search = init-table 3 (λ e0 → brute-force-search e0 (λ e1 → e1)) + +-- テーブルをたどるために若干loopが必要 +pickup-rfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t +pickup-rfork-c ind p env exit = pickup-rfork-p ind [] (table env) p env exit where + pickup-rfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t + pickup-rfork-p zero f [] p env exit = exit env + pickup-rfork-p zero f (zero ∷ ts) p env exit = exit record env{ph = ((ph env) ++ (record p{right-hand = true ; next-code = C_pickup_lfork} ∷ [])); table = (f ++ ((pid p) ∷ ts))} -- 取得可能なので変更する envの後ろにappendする感じ + pickup-rfork-p zero f ((suc x) ∷ ts) p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する + pickup-rfork-p (suc ind) f [] p env exit = exit env + pickup-rfork-p (suc ind) f (x ∷ ts) p env exit = pickup-rfork-p ind (f ++ (x ∷ [])) ts p env exit + +pickup-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t +pickup-lfork-c ind p env exit = pickup-lfork-p (suc ind) [] (table env) p env exit where + pickup-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t + pickup-lfork-p zero f [] p env exit with table env + ... | [] = exit env + ... | 0 ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = true ; next-code = C_eating} ∷ [])); table = ((pid p) ∷ ts)} -- 取得可能なので変更する envの後ろにappendする感じ + ... | (suc x) ∷ ts = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する + pickup-lfork-p zero f (0 ∷ ts) p env exit = exit record env{ph = ((ph env) ++ (record p{left-hand = true ; next-code = C_eating} ∷ [])); table = (f ++ ((pid p) ∷ ts))} -- 取得可能なので変更する envの後ろにappendする感じ + pickup-lfork-p zero f ((suc x) ∷ ts) p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する + pickup-lfork-p (suc ind) f [] p env exit = exit env + pickup-lfork-p (suc ind) f (x ∷ ts) p env exit = pickup-lfork-p ind (f ++ (x ∷ [])) ts p env exit + + +putdown-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t +putdown-lfork-c ind p env exit = putdown-lfork-p (suc ind) [] (table env) p env exit where + putdown-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t + putdown-lfork-p zero f [] p env exit with table env + ... | [] = exit env + ... | x ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = false ; next-code = C_putdown_rfork} ∷ [])); table = (0 ∷ ts)} -- 取得可能なので変更する envの後ろにappendする感じ + putdown-lfork-p zero f (x ∷ ts) p env exit = exit record env{ph = ((ph env) ++ (record p{left-hand = false ; next-code = C_putdown_rfork} ∷ [])); table = (f ++ (0 ∷ ts))} -- 取得可能なので変更する envの後ろにappendする感じ + putdown-lfork-p (suc ind) f [] p env exit = exit env + putdown-lfork-p (suc ind) f (x ∷ ts) p env exit = putdown-lfork-p ind (f ++ (x ∷ [])) ts p env exit + + + +putdown-rfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t +putdown-rfork-c ind p env exit = putdown-rfork-p ind [] (table env) p env exit where + putdown-rfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t + putdown-rfork-p zero f [] p env exit = exit env + putdown-rfork-p zero f (x ∷ ts) p env exit = exit record env{ph = ((ph env) ++ (record p{right-hand = false ; next-code = C_thinking} ∷ [])); table = (f ++ (0 ∷ ts))} -- 取得可能なので変更する envの後ろにappendする感じ + putdown-rfork-p (suc ind) f [] p env exit = exit env + putdown-rfork-p (suc ind) f (x ∷ ts) p env exit = putdown-rfork-p ind (f ++ (x ∷ [])) ts p env exit + + +thinking-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t +thinking-c ind p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不要なので変更せず終了する + +code_table-test : {n : Level} {t : Set n} → Code → ℕ → Phi → Env → (Env → t) → t +code_table-test C_putdown_rfork = putdown-rfork-c +code_table-test C_putdown_lfork = putdown-lfork-c +code_table-test C_thinking = thinking-c +code_table-test C_pickup_rfork = pickup-rfork-c +code_table-test C_pickup_lfork = pickup-lfork-c +code_table-test C_eating = thinking-c +-- code_table-test C_set = ? + +step-c : {n : Level} {t : Set n} → Env → (exit : Env → t) → t +step-c env exit = step-p (length (table env)) 0 record env{ph = []} (ph env) exit where + step-p : {n : Level} {t : Set n} → (redu index : ℕ) → Env → (List Phi) → (exit : Env → t) → t + step-p zero ind env pl exit = exit env + step-p (suc redu) ind env [] exit = exit env + step-p (suc redu) ind env (p ∷ ps) exit = code_table-test (next-code p) ind p env (λ e → step-p redu (suc ind) e ps exit ) + +step-c-debug : {n : Level} {t : Set n} → Env → (exit : List Env → t) → t +step-c-debug env exit = step-p (length (table env)) 0 (record env{ph = [] } ∷ env ∷ []) (ph env) exit where + step-p : {n : Level} {t : Set n} → (redu index : ℕ) → List Env → (List Phi) → (exit : List Env → t) → t + step-p zero ind envl pl exit = exit envl + step-p (suc redu) ind [] pl exit = exit [] + step-p (suc redu) ind (e ∷ envl) [] exit = exit [] + step-p (suc redu) ind (e ∷ envl) (p ∷ ps) exit = code_table-test (next-code p) ind p e (λ e0 → step-p redu (suc ind) (e0 ∷ envl) ps exit ) + +exec-n : {n : Level} {t : Set n} → ℕ → Env → (exit : List Env → t) → t +exec-n n env exit = exec-n-p n (env ∷ []) exit where + exec-n-p : {n : Level} {t : Set n} → ℕ → List Env → (exit : List Env → t) → t + exec-n-p zero envl exit = exit envl + exec-n-p (suc n) [] exit = exit [] + exec-n-p (suc n) envl@(x ∷ es) exit = step-c x (λ e → exec-n-p n (e ∷ envl) exit) + +init-brute-force : {n : Level} {t : Set n} → List Env → (exit : List (List Env) → t) → t +init-brute-force envl exit = init-brute-force-p envl [] exit where + init-brute-force-p : {n : Level} {t : Set n} → List Env → List (List Env) → (exit : List (List Env) → t) → t + init-brute-force-p [] envll exit = exit envll + init-brute-force-p (x ∷ envl) envll exit = init-brute-force-p envl ((x ∷ []) ∷ envll) exit + +search-brute-force-envll : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t +search-brute-force-envll envll exit = search-brute-force-envll-p [] envll exit where + search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t + search-brute-force-envll-p f [] exit = exit f + search-brute-force-envll-p f ([] ∷ bs) exit = search-brute-force-envll-p f bs exit + search-brute-force-envll-p f (b@(x ∷ xs) ∷ bs) exit = brute-force-search x (λ e0 → make-brute-force-envl [] e0 b (λ e1 → search-brute-force-envll-p (f ++ e1) bs exit) ) where + make-brute-force-envl : {n : Level} {t : Set n} → List (List Env) → (state p_step : List Env) → (exit : List (List Env) → t) → t + make-brute-force-envl res [] xs exit = exit res + make-brute-force-envl res (x ∷ state) xs exit = make-brute-force-envl (res ++ (x ∷ xs) ∷ []) state xs exit + +step-brute-force : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t +step-brute-force envll exit = step-brute-force-p [] envll exit where + step-brute-force-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t + step-brute-force-p f [] exit = exit f + step-brute-force-p f ([] ∷ bs) exit = step-brute-force-p f bs exit + step-brute-force-p f ((x ∷ xs) ∷ bs) exit = step-c x (λ e0 → step-brute-force-p (f ++ ((e0 ∷ x ∷ xs) ∷ [])) bs exit) + +exec-brute-force : {n : Level} {t : Set n} → ℕ → List (List Env) → (exit : List (List Env) → t) → t +exec-brute-force n envll exit = exec-brute-force-p n envll exit where + exec-brute-force-p : {n : Level} {t : Set n} → ℕ → List (List Env) → (exit : List (List Env) → t) → t + exec-brute-force-p zero envll exit = exit envll + exec-brute-force-p (suc n) envll exit = search-brute-force-envll envll (λ e1 → step-brute-force e1 (λ e2 → exec-brute-force-p n e2 exit)) + +{- +model-check-deadlock : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t +model-check-deadlock envll exit = test11 [] envll exit where + test11 : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t + test11 f [] exit = exit f + test11 f ([] ∷ bs) exit = test11 f bs exit + test11 f (s@(x ∷ []) ∷ bs) exit = test11 (f ++ (s ∷ [])) bs exit + test11 f (s@(x ∷ x1 ∷ []) ∷ bs) exit = test11 (f ++ (s ∷ [])) bs exit + test11 f ((x ∷ x1 ∷ x2 ∷ xs) ∷ bs) exit = {!!} +-} + +record metadata : Set where + field + num-branch : ℕ + wait-list : List ℕ +open metadata + +record MetaEnv : Set where + field + DG : List Env + meta : metadata + deadlock : Bool + is-done : Bool + is-step : Bool +open MetaEnv + +record MetaEnv2 : Set where + field + DG : List (List Env) + metal : List MetaEnv -- 結局探索して1ステップ実行(インターリーディング)するからMetaEnvのList Envがちょうどよい +open MetaEnv2 + +branch-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t +branch-deadlock-check metaenv exit = search-brute-force-envll-p [] metaenv exit where + search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t + search-brute-force-envll-p f [] exit = exit f + search-brute-force-envll-p f b@(metaenv ∷ bs) exit with DG metaenv + ... | [] = search-brute-force-envll-p f bs exit + ... | (env ∷ envs) = brute-force-search env (λ e0 → make-brute-force-envl (length e0) [] metaenv e0 (λ e1 → search-brute-force-envll-p (f ++ e1) bs exit)) where + make-brute-force-envl : {n : Level} {t : Set n} → ℕ → List MetaEnv → MetaEnv → (state : List Env) → (exit : List MetaEnv → t) → t + make-brute-force-envl len res xs [] exit = exit res + make-brute-force-envl len res xs (x ∷ state) exit = make-brute-force-envl len (res ++ (record xs{DG = (x ∷ DG xs); meta = record (meta xs){num-branch = len}} ∷ [])) xs state exit + +data _===_ {n} {A : Set n} : List A -> List A -> Set n where + reflection : {x : List A} -> x === x + reflection1 : {x : List A} -> (x === x) + +{- +testhoge : Code → Code → ℕ +testhoge C_putdown_rfork C_putdown_rfork = {!!} +testhoge C_putdown_lfork C_putdown_lfork = {!!} +testhoge C_pickup_rfork C_pickup_rfork = {!!} +testhoge C_pickup_lfork C_pickup_lfork = {!!} +testhoge _ _ = {!!} +-} + +step-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t +step-deadlock-check metaenvl exit = deadlock-check-p [] metaenvl exit where + deadlock-check-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t + deadlock-check-p f [] exit = exit f + deadlock-check-p f b@(metaenv ∷ bs) exit with DG metaenv + ... | [] = deadlock-check-p f bs exit + ... | p0 ∷ [] = deadlock-check-p f bs exit + ... | p0 ∷ bp ∷ envs = check-wait-process [] (ph p0) bp ( λ e → deadlock-check-p (f ++ (record metaenv{meta = record (meta metaenv){wait-list = e } } ∷ [])) bs exit) where + check-wait-process : {n : Level} {t : Set n} → List ℕ → List Phi → (p1 : Env) → (exit : List ℕ → t) → t + check-wait-process waitl [] p1 exit = exit waitl + check-wait-process waitl (p ∷ ps) p1 exit = hoge11 p (ph p1) (λ e → check-wait-process (waitl ++ e) ps p1 exit) where + hoge11 : {n : Level} {t : Set n} → Phi → List Phi → (exit : List ℕ → t) → t + hoge11 p [] exit = exit [] + hoge11 p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp) + hoge11 p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 p p1s exit + hoge11 p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 p p1s exit + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (pid p ∷ []) + hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit [] + +step-brute-force-meta : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t +step-brute-force-meta metaenvl exit = step-brute-force-p [] metaenvl exit where + step-brute-force-p : {n : Level} {t : Set n} → (f b : List MetaEnv) → (exit : List MetaEnv → t) → t + step-brute-force-p f [] exit = exit f + step-brute-force-p f (metaenv ∷ bs) exit with DG metaenv + ... | [] = step-brute-force-p f bs exit + ... | envl@(x ∷ xs) with is-done metaenv + ... | true = step-brute-force-p (f ++ (metaenv ∷ []) ) bs exit + ... | false = step-c x (λ e0 → step-brute-force-p (f ++ (record metaenv{DG = e0 ∷ envl} ∷ [])) bs exit) + + +judge-deadlock : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t +judge-deadlock metaenvl exit = judge-deadlock-p [] metaenvl exit where + judge-deadlock-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t + judge-deadlock-p f [] exit = exit f + judge-deadlock-p f (metaenv ∷ bs) exit with num-branch (meta metaenv) + ... | suc (suc branchnum) = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | zero = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | suc zero with (DG metaenv ) + ... | [] = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | p ∷ ps with <-cmp (length (wait-list (meta metaenv))) (length (ph p)) + ... | tri< a ¬b ¬c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | tri> ¬a ¬b c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = true} ∷ []) ) bs exit + + +{- +test-env-deadlock : {n : Level} {t : Set n} → (a b : Env)→ (exit : List MetaEnv → t) → t +test-env-deadlock a b exit = test12 (ph a) (ph b) exit where + test12 : {n : Level} {t : Set n} → (a b : List Phi)→ (exit : List MetaEnv → t) → t + test12 [] b = {!!} + test12 (x ∷ a) b = {!!} +-} + +{- + test12 : List ℕ → (a b0 b : List Phi) → List ℕ + test12 stack [] b0 b = stack + test12 stack (a ∷ as) b0 [] = test12 stack as b0 b0 + test12 stack (a ∷ as) b0 (b ∷ bs) with <-cmp (pid a) (pid b) + test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri< a₁ ¬b ¬c = test12 stack al b0 bs + test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri> ¬a ¬b c = test12 stack al b0 bs + test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri≈ ¬a b₁ ¬c with (next-code a) + test12 stack al@(a ∷ as) b0 (b ∷ bs) | _ | aaaa with (next-code b) + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_putdown_rfork | C_putdown_rfork = pid a ∷ [] + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_putdown_lfork | C_putdown_lfork = pid a ∷ [] + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_thinking | C_thinking = pid a ∷ [] + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_pickup_rfork | C_pickup_rfork = pid a ∷ [] + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_pickup_lfork | C_pickup_lfork = pid a ∷ [] + test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_eating | C_eating = pid a ∷ [] + test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | _ | _ = test12 stack al b0 bs +-} + +branch-search-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (next exit : MetaEnv2 → t) → t +branch-search-meta2 meta2 next1 exit = search-brute-force-envll-p [] (metal meta2) (λ e0 → next1 record meta2{metal = e0} ) (λ e → exit meta2) where + make-brute-force-envl : {n : Level} {t : Set n} → (statel : List MetaEnv) → ( f : List Env) → (state : MetaEnv) → (exit : List MetaEnv → t) → t + search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (next exit : List MetaEnv → t) → t + search-brute-force-envll-p f [] next1 exit = exit f + search-brute-force-envll-p f b@(x ∷ bs) next1 exit with is-done x + ... | true = search-brute-force-envll-p (f ++ (x ∷ [])) bs next1 exit + ... | false with is-step x + ... | false = search-brute-force-envll-p (f ++ (x ∷ [])) bs next1 exit + ... | true with DG x + ... | [] = search-brute-force-envll-p f bs next1 exit + ... | env1 ∷ sss = brute-force-search env1 (λ e2 → make-brute-force-envl [] e2 x (λ e1 → next1 (f ++ bs ++ (record x{is-done = true} ∷ e1)) ) ) + make-brute-force-envl res [] meta exit = exit res + make-brute-force-envl res (addenv ∷ statel) meta exit = make-brute-force-envl (res ++ ( record meta{DG = addenv ∷ (DG meta); is-done = false; is-step = false} ∷ [])) statel meta exit + + +step-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (next exit : MetaEnv2 → t) → t +step-meta2 meta2 next1 exit = step-brute-force-p1 [] (metal meta2) (λ envll → next1 record meta2{metal = envll}) (λ e → exit meta2) where + step-brute-force-p-p : {n : Level} {t : Set n} → (envl : (List Env)) → (exit : (List Env) → t) → t + step-brute-force-p1 : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (next exit : List (MetaEnv) → t) → t + step-brute-force-p1 f [] next1 exit = next1 f + step-brute-force-p1 f (metaenv ∷ metaenvl) next1 exit with is-step metaenv + ... | true = step-brute-force-p1 (f ++ (metaenv ∷ [])) metaenvl next1 exit + ... | false = step-brute-force-p-p (DG metaenv) (λ e0 → step-brute-force-p1 (f ++ (record metaenv{DG = e0; is-step = true} ∷ [])) metaenvl next1 exit) + step-brute-force-p-p [] exit = exit [] + step-brute-force-p-p (x ∷ bs) exit = step-c x (λ e0 → exit (e0 ∷ bs)) + +{-# TERMINATING #-} +check-same-env : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t +check-same-env meta2 exit = check-same-env-p [] (metal meta2) meta2 exit where + check-wait-process-p : {n : Level} {t : Set n} → ℕ → List Phi → (p1 : Env) → (exit : ℕ → t) → t + check-wait-process-p waitl [] p1 exit = exit waitl + check-wait-process-p waitl (p ∷ ps) p1 exit = hoge11 waitl p (ph p1) (λ e → check-wait-process-p e ps p1 exit) where + hoge11 : {n : Level} {t : Set n} → ℕ → Phi → List Phi → (exit : ℕ → t) → t + hoge11 n p [] exit = exit n + hoge11 n p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp) + hoge11 n p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 n p p1s exit + hoge11 n p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 n p p1s exit + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit n + check-wait-process : {n : Level} {t : Set n} → ℕ → List Phi → List MetaEnv → MetaEnv → (exit : List MetaEnv → t) → t + check-wait-process n pl metal me exit with metal + ... | sss with <-cmp (length pl) n + ... | tri≈ ¬a b ¬c = exit (me ∷ []) + check-wait-process n pl metal me exit | [] | tri< a ¬b ¬c = exit [] + check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c with DG x + check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c | [] = exit [] + check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit) + check-wait-process n pl metal me exit | [] | tri> ¬a ¬b c = exit [] + check-wait-process n pl metal me exit | x ∷ sss | tri> ¬a ¬b c with DG x + ... | [] = exit [] + ... | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit) + check-same-env-p : {n : Level} {t : Set n} → (f b : List MetaEnv) → MetaEnv2 → (exit : MetaEnv2 → t) → t + check-same-env-p [] [] metae2 exit = exit metae2 + check-same-env-p f@(x ∷ fs) [] metae2 exit = step-meta2 record metae2{metal = f} (λ me2 → branch-search-meta2 me2 (λ me3 → check-same-env me3 exit) exit ) exit + check-same-env-p [] bl@(b ∷ bs) metae2 exit with DG b + ... | [] = check-same-env-p [] bs metae2 exit + ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p ([] ++ lme) bl metae2 exit) + check-same-env-p f@(x ∷ fs) bl@(b ∷ bs) metae2 exit with DG b + ... | [] = check-same-env-p f bs metae2 exit + ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p (f ++ lme) bl metae2 exit) + +check-same-env-test : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t +check-same-env-test meta2 exit = check-same-env-p [] (metal meta2) meta2 exit where + check-wait-process-p : {n : Level} {t : Set n} → ℕ → List Phi → (p1 : Env) → (exit : ℕ → t) → t + check-wait-process-p waitl [] p1 exit = exit waitl + check-wait-process-p waitl (p ∷ ps) p1 exit = hoge11 waitl p (ph p1) (λ e → check-wait-process-p e ps p1 exit) where + hoge11 : {n : Level} {t : Set n} → ℕ → Phi → List Phi → (exit : ℕ → t) → t + hoge11 n p [] exit = exit n + hoge11 n p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp) + hoge11 n p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 n p p1s exit + hoge11 n p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 n p p1s exit + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (suc n) + hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit n + check-wait-process : {n : Level} {t : Set n} → ℕ → List Phi → List MetaEnv → MetaEnv → (exit : List MetaEnv → t) → t + check-wait-process n pl metal me exit with metal + ... | sss with <-cmp (length pl) n + ... | tri≈ ¬a b ¬c = exit (me ∷ []) + check-wait-process n pl metal me exit | [] | tri< a ¬b ¬c = exit (me ∷ []) + check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c with DG x + check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c | [] = exit [] + check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit) + check-wait-process n pl metal me exit | [] | tri> ¬a ¬b c = exit (me ∷ []) + check-wait-process n pl metal me exit | x ∷ sss | tri> ¬a ¬b c with DG x + ... | [] = exit [] + ... | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit) + make-metaenvl : {n : Level} {t : Set n} → (f : (List MetaEnv)) → List (List Env) → (exit : List MetaEnv → t) → t + make-metaenvl f [] exit = exit f + make-metaenvl f ([] ∷ bs) exit = make-metaenvl f bs exit + make-metaenvl f ((e ∷ es) ∷ bs) exit = make-metaenvl (f ++ (record{ DG = (e ∷ []); meta = record { num-branch = zero ; wait-list = [] }; deadlock = true; is-done = false; is-step = false} ∷ [])) bs exit + check-same-env-p : {n : Level} {t : Set n} → (f b : List MetaEnv) → MetaEnv2 → (exit : MetaEnv2 → t) → t + check-same-env-p [] [] metae2 exit = make-metaenvl [] (DG metae2) (λ lme → exit record metae2{metal = lme}) + check-same-env-p f@(x ∷ fs) [] metae2 exit = exit record metae2{metal = f} + check-same-env-p [] bl@(b ∷ bs) metae2 exit with DG b + ... | [] = check-same-env-p [] bs metae2 exit + ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p ([] ++ lme) bs metae2 exit) + check-same-env-p f@(x ∷ fs) bl@(b ∷ bs) metae2 exit with DG b + ... | [] = check-same-env-p f bs metae2 exit + ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p (f ++ lme) bs metae2 exit) + + + +{- +search-brute-force-envll : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t +search-brute-force-envll envll exit = search-brute-force-envll-p [] envll exit where + search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t + search-brute-force-envll-p f [] exit = exit f + search-brute-force-envll-p f ([] ∷ bs) exit = search-brute-force-envll-p f bs exit + search-brute-force-envll-p f (b@(x ∷ xs) ∷ bs) exit = brute-force-search x (λ e0 → make-brute-force-envl [] e0 b (λ e1 → search-brute-force-envll-p (f ++ e1) bs exit) ) where + make-brute-force-envl : {n : Level} {t : Set n} → List (List Env) → (state p_step : List Env) → (exit : List (List Env) → t) → t + make-brute-force-envl res [] xs exit = exit res + make-brute-force-envl res (x ∷ state) xs exit = make-brute-force-envl (res ++ (x ∷ xs) ∷ []) state xs exit +-} + +test-env : Env +test-env = (record { + table = 0 ∷ 0 ∷ 0 ∷ [] + ; ph = record + { pid = 1 + ; left-hand = false + ; right-hand = false + ; next-code = C_thinking + } ∷ record + { pid = 2 + ; left-hand = false + ; right-hand = false + ; next-code = C_thinking + } ∷ record + { pid = 3 + ; left-hand = false + ; right-hand = false + ; next-code = C_thinking + } ∷ [] + }) +test-env1 : Env +test-env1 = (record { + table = 1 ∷ 2 ∷ 0 ∷ [] + ; ph = record + { pid = 1 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ record + { pid = 2 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ record + { pid = 3 + ; left-hand = false + ; right-hand = false + ; next-code = C_thinking + } ∷ [] + }) + +test-metaenv : MetaEnv +test-metaenv = record + { DG = test-env1 ∷ test-env ∷ [] + ; meta = record { num-branch = zero ; wait-list = [] } + ; deadlock = true ; is-done = false ; is-step = false + } + +test-metaenv1 : MetaEnv +test-metaenv1 = record + { DG = test-env ∷ [] + ; meta = record { num-branch = zero ; wait-list = [] } + ; deadlock = true; is-done = false ; is-step = true + } +test-metaenv2 : MetaEnv2 +test-metaenv2 = record { DG = [] ; metal = test-metaenv ∷ [] } + +test-metaenv3 : MetaEnv2 +test-metaenv3 = record { DG = [] ; metal = test-metaenv1 ∷ [] } + + + +test-envl : List Env +test-envl = test-env1 ∷ test-env1 ∷ [] + +testhoge : {n : Level} {t : Set n} → (env1 env2 : MetaEnv2) → (exit : MetaEnv2 → t) → t +testhoge env1 env2 exit = loop-target-metaenv (metal env1) env2 exit where + eq-pid : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t) → (loop : Bool → t) → t + eq-lhand : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t ) → ( loop : Bool → t) → t + eq-rhand : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t ) → ( loop : Bool → t) → t + eq-next-code : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t ) → ( loop : Bool → t) → t + eq-env : {n : Level} {t : Set n} → MetaEnv2 → ( e1 e2 : List Phi) → (exit : MetaEnv2 → t) → (loop : Bool → t) → t + + loop-metaenv : {n : Level} {t : Set n} → MetaEnv → (origin : MetaEnv2) → (f b : List MetaEnv) → (exit : MetaEnv2 → t) → t + + loop-target-metaenv : {n : Level} {t : Set n} → (env1 : List MetaEnv) → ( env2 : MetaEnv2) → (exit : MetaEnv2 → t) → t + loop-target-metaenv [] metaenv2 exit = exit metaenv2 + loop-target-metaenv (metaenv ∷ metaenvl) metaenv2 exit = loop-metaenv metaenv metaenv2 [] (metal metaenv2) (λ e → loop-target-metaenv metaenvl e exit) + + boolor : Bool → Bool → Bool + boolor true true = true + boolor true false = true + boolor false true = true + boolor false false = false + + loop-metaenv me origin f [] exit = exit (record origin{metal = me ∷ (metal origin) }) -- not found & add state to origin + loop-metaenv me origin f (x ∷ metaenvl) exit with DG me + ... | [] = exit origin + ... | env1 ∷ envl with DG x + ... | [] = loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit + ... | env2 ∷ history = eq-env origin (ph env1) (ph env2) (λ exit-e → exit record origin{metal = f ++ (record x{is-done = boolor (is-done me) (is-done x); is-step = boolor (is-step me) (is-step x) } ∷ metaenvl)}) (λ e → loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit ) + + eq-env origin [] [] exit loop = exit origin -- true + eq-env origin [] (x ∷ pl2) exit loop = loop false + eq-env origin (p1 ∷ pl1) [] exit loop = loop false + eq-env origin (p1 ∷ pl1) (p2 ∷ pl2) exit loop = eq-pid origin pl1 pl2 p1 p2 exit (λ e → loop e) -- prototype + + eq-pid origin pl1 pl2 p1 p2 next1 exit1 with <-cmp (pid p1) (pid p2) + ... | tri< a ¬b ¬c = exit1 false + ... | tri> ¬a ¬b c = exit1 false + ... | tri≈ ¬a b ¬c = eq-lhand origin pl1 pl2 p1 p2 next1 exit1 + + eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 with (left-hand phi1) + ... | sss with (left-hand phi2) + eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | true = eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 + eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | false = exit1 false + eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | true = exit1 false + eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | false = eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 + + eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 with (right-hand phi1) + ... | sss with (right-hand phi2) + eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | true = eq-next-code origin pl1 pl2 phi1 phi2 next1 exit1 + eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | false = exit1 false + eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | true = exit1 false + eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | false = eq-next-code origin pl1 pl2 phi1 phi2 next1 exit1 + + eq-next-code origin pl1 pl2 p1 p2 next1 loop with (next-code p1) + ... | sss with (next-code p2) + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_putdown_rfork | C_putdown_rfork = eq-env origin pl1 pl2 next1 loop + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_putdown_rfork | _ = loop false + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_putdown_lfork | C_putdown_lfork = eq-env origin pl1 pl2 next1 loop + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_putdown_lfork | _ = loop false + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_thinking | C_thinking = eq-env origin pl1 pl2 next1 loop + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_thinking | _ = loop false + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_pickup_rfork | C_pickup_rfork = eq-env origin pl1 pl2 next1 loop + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_pickup_rfork | _ = loop false + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_pickup_lfork | C_pickup_lfork = eq-env origin pl1 pl2 next1 loop + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_pickup_lfork | _ = loop false + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_eating | C_eating = eq-env origin pl1 pl2 next1 loop + eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_eating | _ = loop false + +-- testhoge test-env test-env1 + +{- +testhoge record { table = table₁ ; ph = [] } record { table = table ; ph = [] } = true -- same table? is that realy true ? +testhoge record { table = table₁ ; ph = [] } record { table = table ; ph = (x ∷ ph₁) } = false +testhoge record { table = table₁ ; ph = (x ∷ ph₁) } record { table = table ; ph = [] } = false +testhoge record { table = table₁ ; ph = pl1@(x ∷ ph₁) } record { table = table ; ph = pl2@(x₁ ∷ ph₂) } = {!!} +-} + + + +exec-brute-force-meta : {n : Level} {t : Set n} → ℕ → List MetaEnv → (exit : List MetaEnv → t) → t +exec-brute-force-meta n metaenvl exit = exec-brute-force-p n metaenvl exit where + exec-brute-force-p : {n : Level} {t : Set n} → ℕ → List MetaEnv → (exit : List MetaEnv → t) → t + exec-brute-force-p zero envll exit = exit envll + exec-brute-force-p (suc n) envll exit = branch-deadlock-check envll (λ e1 → step-brute-force-meta e1 (λ e2 → step-deadlock-check e2 (λ e3 → judge-deadlock e3 (λ e4 → exec-brute-force-p n e4 exit)))) + + +test-dead-lock : List MetaEnv +test-dead-lock = exec-brute-force-meta 3 (record + { DG = (record { + table = 0 ∷ 0 ∷ 0 ∷ [] + ; ph = record + { pid = 1 + ; left-hand = false + ; right-hand = false + ; next-code = C_thinking + } ∷ record + { pid = 2 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ record + { pid = 3 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ [] + }∷ []) + ; meta = record { num-branch = zero ; wait-list = [] } + ; deadlock = false; is-done = false ; is-step = false + } ∷ []) (λ e3 → e3) + +test-dead-lock-meta2 : MetaEnv2 +test-dead-lock-meta2 = branch-search-meta2 (record { DG = (record { table = 0 ∷ 0 ∷ 0 ∷ [] ; ph = record + { pid = 1 + ; left-hand = false + ; right-hand = false + ; next-code = C_thinking + } ∷ record + { pid = 2 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ record + { pid = 3 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ [] } ∷ []) ∷ [] ; metal = [] }) (λ me0 → check-same-env-test me0 (λ me1 → step-meta2 me1 (λ me2 → branch-search-meta2 me2 ( λ me3 → testhoge me3 me2 (λ me4 → check-same-env-test me4 (λ me5 → me5))) (λ e → e) ) (λ e → e) )) (λ e → e) + + +test-dead-lock-meta21 : MetaEnv2 +test-dead-lock-meta21 = branch-search-meta2 (record { DG = (record { table = 0 ∷ 0 ∷ 0 ∷ [] ; ph = record + { pid = 1 + ; left-hand = false + ; right-hand = false + ; next-code = C_thinking + } ∷ record + { pid = 2 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ record + { pid = 3 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ [] } ∷ []) ∷ [] ; metal = [] }) (λ me0 → check-same-env-test me0 (λ me1 → step-meta2 me1 (λ me2 → branch-search-meta2 me2 ( λ me3 → testhoge me3 me2 (λ me4 → check-same-env-test me4 (λ me5 → me5))) (λ e → e) ) (λ e → e) )) (λ e → e) + + +test-dead-lock-meta22 : ℕ → MetaEnv2 → MetaEnv2 +test-dead-lock-meta22 zero metaenv2 = metaenv2 +test-dead-lock-meta22 (suc n) metaenv2 = branch-search-meta2 metaenv2 (λ me1 → testhoge me1 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 me2 (λ me4 → test-dead-lock-meta22 n me4) ) (λ e → e)) ) (λ e → e) + +{-# TERMINATING #-} +test-dead-lock-loop : MetaEnv2 → MetaEnv2 +test-dead-lock-loop metaenv2 = branch-search-meta2 metaenv2 (λ me1 → testhoge me1 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 me2 (λ me4 → test-dead-lock-loop me4) ) (λ e → e)) ) (λ e → e) + +-- test-dead-lock-loop test-metaenv2 + +test-step-c2 : List (List Env) +test-step-c2 = init-brute-force (record { + table = 0 ∷ 0 ∷ 0 ∷ [] + ; ph = record + { pid = 1 + ; left-hand = false + ; right-hand = false + ; next-code = C_thinking + } ∷ record + { pid = 2 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ record + { pid = 3 + ; left-hand = false + ; right-hand = false + ; next-code = C_pickup_rfork + } ∷ [] + } ∷ []) (λ e0 → exec-brute-force 2 e0 (λ e2 → e2)) + +-- 以下メモ + +-- eathingの状態はいらない Done +-- tableはℕのList Done +-- いきなりsearchしないで実行結果を持つ感じに +-- stubを使うとCodeの引数がスマートになるのでやる + +-- 実行結果をListでもっているので、stepをじっこうしても変化がなかった場合をdeadlockとして検出したい +-- 東恩納先輩とおなじように、waitに入れて評価する + +-- 余裕があったらassertにLTLの話をいれる + +-- loop execution + +-- concurrnt execution + +-- state db ( binary tree of processes ) + +-- depth first ececution + +-- verify temporal logic poroerries + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/dpp-verif/dpp-metadata.agda Sat Jan 21 17:57:20 2023 +0900 @@ -0,0 +1,20 @@ +record metadata : Set where + field + num-branch : ℕ + wait-list : List ℕ +open metadata + +record MetaEnv : Set where + field + DG : List Env + meta : metadata + deadlock : Bool + is-done : Bool + is-step : Bool +open MetaEnv + +record MetaEnv2 : Set where + field + DG : List (List Env) + metal : List MetaEnv +open MetaEnv2
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/dpp-verif/exclude-same-env.agda Sat Jan 21 17:57:20 2023 +0900 @@ -0,0 +1,33 @@ +exclude-same-env : {n : Level} {t : Set n} → (env1 env2 : MetaEnv2) → (exit : MetaEnv2 → t) → t +exclude-same-env env1 env2 exit = loop-target-metaenv (metal env1) env2 exit where + eq-pid : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t) → (loop : Bool → t) → t + eq-lhand : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t ) → ( loop : Bool → t) → t + eq-rhand : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t ) → ( loop : Bool → t) → t + eq-next-code : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t ) → ( loop : Bool → t) → t + eq-env : {n : Level} {t : Set n} → MetaEnv2 → ( e1 e2 : List Phi) → (exit : MetaEnv2 → t) → (loop : Bool → t) → t + + loop-metaenv : {n : Level} {t : Set n} → MetaEnv → (origin : MetaEnv2) → (f b : List MetaEnv) → (exit : MetaEnv2 → t) → t + + loop-target-metaenv : {n : Level} {t : Set n} → (env1 : List MetaEnv) → ( env2 : MetaEnv2) → (exit : MetaEnv2 → t) → t + loop-target-metaenv [] metaenv2 exit = exit metaenv2 + loop-target-metaenv (metaenv ∷ metaenvl) metaenv2 exit = loop-metaenv metaenv metaenv2 [] (metal metaenv2) (λ e → loop-target-metaenv metaenvl e exit) + + loop-metaenv me origin f [] exit = exit (record origin{metal = me ∷ (metal origin) }) -- not found & add state to origin + loop-metaenv me origin f (x ∷ metaenvl) exit with DG me + ... | [] = exit origin + ... | env1 ∷ envl with DG x + ... | [] = loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit + ... | env2 ∷ history = eq-env origin (ph env1) (ph env2) (λ exit-e → exit record origin{metal = f ++ (record x{is-done = boolor (is-done me) (is-done x); is-step = boolor (is-step me) (is-step x) } ∷ metaenvl)}) (λ e → loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit ) + + eq-env origin [] [] exit loop = exit origin -- true + eq-env origin [] (x ∷ pl2) exit loop = loop false + eq-env origin (p1 ∷ pl1) [] exit loop = loop false + eq-env origin (p1 ∷ pl1) (p2 ∷ pl2) exit loop = eq-pid origin pl1 pl2 p1 p2 exit (λ e → loop e) -- prototype + + eq-pid origin pl1 pl2 p1 p2 next1 exit1 with <-cmp (pid p1) (pid p2) + ... | tri< a ¬b ¬c = exit1 false + ... | tri> ¬a ¬b c = exit1 false + ... | tri≈ ¬a b ¬c = eq-lhand origin pl1 pl2 p1 p2 next1 exit1 + . + . + . \ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Paper/src/dpp-verif/judge-deadlock.agda Sat Jan 21 17:57:20 2023 +0900 @@ -0,0 +1,13 @@ +judge-deadlock : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t +judge-deadlock metaenvl exit = judge-deadlock-p [] metaenvl exit where + judge-deadlock-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t + judge-deadlock-p f [] exit = exit f + judge-deadlock-p f (metaenv ∷ bs) exit with num-branch (meta metaenv) + ... | suc (suc branchnum) = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | zero = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | suc zero with (DG metaenv ) + ... | [] = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | p ∷ ps with <-cmp (length (wait-list (meta metaenv))) (length (ph p)) + ... | tri< a ¬b ¬c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | tri> ¬a ¬b c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit + ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = true} ∷ []) ) bs exit \ No newline at end of file
--- a/Paper/tex/dpp_impl.tex Fri Jan 20 15:20:31 2023 +0900 +++ b/Paper/tex/dpp_impl.tex Sat Jan 21 17:57:20 2023 +0900 @@ -107,14 +107,13 @@ ここからは、モデル検査を行うため、Meta Data Gear の定義をし、 それの操作を行う Meta Code Gear の実装を行っていく。 -以下がMeta Code Gear の定義になる +以下\coderef{dpp-mdg}がMeta Code Gear の定義になる % ここにmetadata MetaEnv MetaEnv2のソースコードを貼り付ける +\lstinputlisting[caption=Gears Agdaでの DPP モデル検査を行うための Meta Data Gear の定義, label=code:dpp-mdg]{src/dpp-verif/dpp-metadata.agda.replaced} この Meta Data Gear の説明をすると、 - metadataは状態の分岐数を持っておくnum-brunchがある。 - MetaEnv はもとの DataGear を保持するDG(Data Gearの省略) meta に 前述したmetadataを持っており、 他には、deadlockしているかのフラグである deadlock 、 @@ -129,12 +128,14 @@ そしてnum-brunchの値が1であるということは、それ以上の状態に移動することができないとして、この状態をdead lockであると定義した。 -以下のソースコードがdead-lockを検知する関数となる +以下の\coderef{dpp-judge-mcg}がdead-lockを検知する関数となる 複雑なことは何もしておらず、単純にstate毎のnum-brunchの値を見て deadlockのフラグを立ち上げている。 % judge-dead-lock-pのソースコードを貼り付ける +\lstinputlisting[caption=DPP での dead lock を検知する Meta Code Gear, label=code:dpp-judge-mcg]{src/dpp-verif/judge-deadlock.agda.replaced} +% こいつはmetaEnv2を受け取れるように変えないと行けない ここから前述した通り、State Listを作成する。 @@ -143,10 +144,24 @@ 存在していた場合はそれを追加せず、存在しなかった場合にのみ State を追加する。 Agdaには2つの record が等しい場合の分岐など存在しないため、 -以下のソースコードのようにrecordの中身を一つづつ一致しているか確認する。 +\coderef{dpp-exclude-state-mcg} のようにrecordの中身を一つづつ一致しているか確認する。 +こちらはそのまま掲載すると長いので、実際のコードに手を加えて省略している。実際のコードは付録にて参照できる。 + +\lstinputlisting[caption=重複しているstateを除外する Meta Code Gear, label=code:dpp-exclude-state-mcg]{src/dpp-verif/exclude-same-env.agda.replaced} +% 手を加えているので詳細は付録を参照するように促す + +MetaEnv2 を受け取ってその中身の state を比較するが、そこまで展開する必要がある。 + loop-metaenv と loop-target-metaenv, eq-env にてそれを行っている。 -これで、 -まだ分岐を見ていない1つのStateの分岐を確かめる。 +更に15行目の loop-metaenv では State List 内に見つからなかった場合に State List に Stateを追加し、次のstateの一致を探索するように記述されている。 + +実際にstateの一致を見ているのは22行目のeq-env関数で、一致している State が見つかった場合には追加せずにこちらも次の State を探索するように記述されている + +State が保持している値がそれぞれ正しいのかは eq-pid のように一致を見て分岐させている。 +その値が一致している場合には別の値を見て、一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている。 +他の値である、lhandやrhandなども同じように記述している。 + +これらにて、まだ分岐を見ていない1つのStateの分岐を確かめる。 発生した分岐を step 実行させる。 step実行して作成された state が State Listに存在していないかを確かめる。 これを繰り返すことで State Listを作る。
--- a/Paper/tex/while_loop.tex Fri Jan 20 15:20:31 2023 +0900 +++ b/Paper/tex/while_loop.tex Sat Jan 21 17:57:20 2023 +0900 @@ -52,7 +52,7 @@ \lstinputlisting[label=conversion, caption=init時の Pre Condition を Post Condition に変換する Code Gear] {src/while_loop_verif/conversion.agda.replaced} ここで変換されて作成された Post Condition はプログラム実行中の不変条件となるため， -この後の Pre / Post Condition は停止するまでこれを用いる． +停止するまでこの Pre / Post Condition を用いる． 以下の Code \ref{loop_verif_cg} は停止性の検証を行っていないが， Wile Loop の Loop 部分の検証を行う Code Gear となる．