Mercurial > hg > Papers > 2023 > soto-master
changeset 6:8c1e9a6d58e2
Add paper dpp
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 21 Jan 2023 20:47:38 +0900 |
| parents | eaef105dff41 |
| children | c821e707a5ee |
| files | DPP/ModelChecking.agda Paper/master_paper.pdf Paper/src/dpp-verif/ModelChecking.agda Paper/src/dpp-verif/judge-deadlock.agda Paper/tex/dpp_impl.tex |
| diffstat | 5 files changed, 29 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/DPP/ModelChecking.agda Sat Jan 21 17:57:20 2023 +0900 +++ b/DPP/ModelChecking.agda Sat Jan 21 20:47:38 2023 +0900 @@ -356,6 +356,19 @@ ... | 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 +judge-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t +judge-deadlock-metaenv meta2 exit = judge-deadlock-p [] (metal meta2) (λ e → exit record meta2{metal = e} ) 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
--- a/Paper/src/dpp-verif/ModelChecking.agda Sat Jan 21 17:57:20 2023 +0900 +++ b/Paper/src/dpp-verif/ModelChecking.agda Sat Jan 21 20:47:38 2023 +0900 @@ -356,6 +356,19 @@ ... | 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 +judge-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t +judge-deadlock-metaenv meta2 exit = judge-deadlock-p [] (metal meta2) (λ e → exit record meta2{metal = e} ) 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
--- a/Paper/src/dpp-verif/judge-deadlock.agda Sat Jan 21 17:57:20 2023 +0900 +++ b/Paper/src/dpp-verif/judge-deadlock.agda Sat Jan 21 20:47:38 2023 +0900 @@ -1,5 +1,5 @@ -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-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t +judge-deadlock-metaenv meta2 exit = judge-deadlock-p [] (metal meta2) (λ e → exit record meta2{metal = e} ) 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)
--- a/Paper/tex/dpp_impl.tex Sat Jan 21 17:57:20 2023 +0900 +++ b/Paper/tex/dpp_impl.tex Sat Jan 21 20:47:38 2023 +0900 @@ -161,6 +161,7 @@ その値が一致している場合には別の値を見て、一致していない場合はeq-envに遷移して State List にある次の State との一致を見るようにしている。 他の値である、lhandやrhandなども同じように記述している。 + これらにて、まだ分岐を見ていない1つのStateの分岐を確かめる。 発生した分岐を step 実行させる。 step実行して作成された state が State Listに存在していないかを確かめる。