Mercurial > hg > Papers > 2023 > soto-master
changeset 24:988528add93f
fix slide
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 07 Feb 2023 14:49:15 +0900 |
| parents | 016e82a71407 |
| children | 83e28d9da152 |
| files | DPP/sample.agda slide/slide.md slide/slide.pdf |
| diffstat | 3 files changed, 10 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/DPP/sample.agda Tue Feb 07 02:27:53 2023 +0900 +++ b/DPP/sample.agda Tue Feb 07 14:49:15 2023 +0900 @@ -19,6 +19,14 @@ ... | 0 = exit env ... | suc s = next (record env{varn = suc (varn env) ; vari = s }) +record _∧1_ (A B : Set) : Set where + field + p1 : A + p2 : B +open _∧1_ + +s1 : {A B C : Set} → (A → B) ∧1 (B → C) → (A → C) +s1 x = init-env-c : {l : Level} {t : Set l} → ℕ → (next : Env → t) → t init-env-c x next = next record { c10 = x ; varn = 0 ; vari = x }
--- a/slide/slide.md Tue Feb 07 02:27:53 2023 +0900 +++ b/slide/slide.md Tue Feb 07 14:49:15 2023 +0900 @@ -454,7 +454,7 @@ test-dead-lock-loop2 : MetaEnv2 → MetaEnv2 test-dead-lock-loop2 metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 - (λ me3 → testhoge me3 metaenv2 + (λ me3 → exclude-same-env me3 metaenv2 (λ me4 → test-dead-lock-loop2 me4) ) ) (λ e → check-and-judge-deadlock e (λ e1 → e1) ) ``` @@ -468,7 +468,7 @@ - モデル検査 - 有向グラフからなる有限オートマトンの遷移を全自動探索する - live lock の検出や LTTL も用いたアサーションなどの検証 - - State List のデータ構造を blanced tree にする + - State List のデータ構造を balanced tree にする - モデル検査に定理証明を組み込む - 定理証明 - Red Black Tree の検証を行う