Mercurial > hg > Papers > 2023 > soto-master
comparison DPP/ModelChecking.agda @ 2:0425278b683b
Add dpp
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 12 Jan 2023 20:31:09 +0900 |
| parents | |
| children | 8c1e9a6d58e2 |
comparison
equal
deleted
inserted
replaced
| 1:a72446879486 | 2:0425278b683b |
|---|---|
| 1 module ModelChecking where | |
| 2 | |
| 3 open import Level renaming (zero to Z ; suc to succ) | |
| 4 | |
| 5 open import Data.Nat hiding (compare) | |
| 6 open import Data.Nat.Properties as NatProp | |
| 7 open import Data.Maybe | |
| 8 -- open import Data.Maybe.Properties | |
| 9 open import Data.Empty | |
| 10 open import Data.List | |
| 11 open import Data.Product | |
| 12 open import Function as F hiding (const) | |
| 13 open import Relation.Binary | |
| 14 open import Relation.Binary.PropositionalEquality | |
| 15 open import Relation.Nullary | |
| 16 open import logic | |
| 17 open import Data.Unit hiding (_≟_ ; _≤?_ ; _≤_) | |
| 18 open import Relation.Binary.Definitions | |
| 19 | |
| 20 record AtomicNat : Set where | |
| 21 field | |
| 22 value : ℕ | |
| 23 | |
| 24 set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t | |
| 25 set a v next = next record { value = v } | |
| 26 | |
| 27 record Phils : Set where | |
| 28 field | |
| 29 pid : ℕ | |
| 30 left right : AtomicNat | |
| 31 | |
| 32 putdown_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 33 putdown_rfork p next = set (Phils.right p) 0 ( λ f → next record p { right = f } ) | |
| 34 | |
| 35 putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 36 putdown_lfork p next = set (Phils.left p) 0 ( λ f → next record p { left = f } ) | |
| 37 | |
| 38 thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 39 thinking p next = next p | |
| 40 | |
| 41 pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 42 pickup_rfork p next = set (Phils.right p) (Phils.pid p) ( λ f → next record p { right = f } ) | |
| 43 | |
| 44 pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 45 pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → next record p { left = f } ) | |
| 46 | |
| 47 --eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t | |
| 48 --eating p next = next p | |
| 49 | |
| 50 data Code : Set where | |
| 51 -- C_set : Code | |
| 52 C_putdown_rfork : Code | |
| 53 C_putdown_lfork : Code | |
| 54 C_thinking : Code | |
| 55 C_pickup_rfork : Code | |
| 56 C_pickup_lfork : Code | |
| 57 C_eating : Code | |
| 58 | |
| 59 record Process : Set where | |
| 60 field | |
| 61 phil : Phils | |
| 62 next_code : Code | |
| 63 | |
| 64 putdown_rfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t | |
| 65 putdown_rfork_stub p next = putdown_rfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } ) | |
| 66 | |
| 67 putdown_lfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t | |
| 68 putdown_lfork_stub p next = putdown_lfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } ) | |
| 69 | |
| 70 {- | |
| 71 code_table : {n : Level} {t : Set n} → Code → Process → ( Process → t) → t | |
| 72 -- code_table C_set = {!!} | |
| 73 code_table C_putdown_rfork = putdown_rfork_stub | |
| 74 code_table C_putdown_lfork = putdown_lfork_stub | |
| 75 code_table C_thinking = {!!} | |
| 76 code_table C_pickup_rfork = {!!} | |
| 77 code_table C_pickup_lfork = {!!} | |
| 78 code_table C_eating = {!!} | |
| 79 -} | |
| 80 | |
| 81 open Process | |
| 82 | |
| 83 --step : {n : Level} {t : Set n} → List Process → (List Process → t) → t | |
| 84 --step {n} {t} [] next0 = next0 [] | |
| 85 --step {n} {t} (p ∷ ps) next0 = code_table (next_code p) p ( λ np → next0 (ps ++ ( np ∷ [] ) )) | |
| 86 | |
| 87 --test : List Process | |
| 88 --test = step ( record { phil = record { pid = 1 ; left = record { value = 1 } ; right = record { value = 1 } } ; next_code = C_putdown_rfork } ∷ [] ) ( λ ps → ps ) | |
| 89 | |
| 90 --test1 : List Process | |
| 91 --test1 = step ( record { phil = record { pid = 1 ; left = record { value = 1 } ; right = record { value = 1 } } ; next_code = C_putdown_rfork } ∷ [] ) | |
| 92 -- $ λ ps → step ps $ λ ps → ps | |
| 93 | |
| 94 record Phi : Set where | |
| 95 field | |
| 96 pid : ℕ | |
| 97 right-hand : Bool | |
| 98 left-hand : Bool | |
| 99 next-code : Code | |
| 100 open Phi | |
| 101 | |
| 102 record Env : Set where | |
| 103 field | |
| 104 table : List ℕ | |
| 105 ph : List Phi | |
| 106 open Env | |
| 107 | |
| 108 init-table : {n : Level} {t : Set n} → ℕ → (exit : Env → t) → t | |
| 109 init-table n exit = init-table-loop n 0 (record {table = [] ; ph = []}) exit where | |
| 110 init-table-loop : {n : Level} {t : Set n} → (redu inc : ℕ) → Env → (exit : Env → t) → t | |
| 111 init-table-loop zero ind env exit = exit env | |
| 112 init-table-loop (suc redu) ind env exit = init-table-loop redu (suc ind) record env{ | |
| 113 table = 0 ∷ (table env) | |
| 114 ; ph = record {pid = redu ; left-hand = false ; right-hand = false ; next-code = C_thinking } ∷ (ph env) } exit | |
| 115 | |
| 116 -- eatingも探索範囲に含める | |
| 117 brute-force-search : {n : Level} {t : Set n} → Env → (exit : List Env → t) → t | |
| 118 brute-force-search env exit = make-state-list 1 [] (ph env) env (env ∷ []) exit where | |
| 119 make-state-list : {n : Level} {t : Set n} → ℕ → List Bool → List Phi → Env → (List Env) → (exit : List Env → t) → t | |
| 120 make-state-list redu state (x ∷ pl) env envl exit with next-code x | |
| 121 ... | C_thinking = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit | |
| 122 ... | C_eating = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit | |
| 123 ... | _ = make-state-list redu state pl env envl exit | |
| 124 make-state-list redu state [] env envl exit = bit-force-search redu [] state env envl exit where | |
| 125 bit-force-search : {n : Level} {t : Set n} → ℕ → (f b : List Bool )→ Env → (List Env) → (exit : List Env → t) → t | |
| 126 bit-force-search zero f l env envl exit = exit envl | |
| 127 bit-force-search (suc redu) f [] env envl exit = exit envl | |
| 128 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を次の対象にする | |
| 129 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させる | |
| 130 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のやつのみ | |
| 131 set-state redu origin [] f b env envl exit = bit-force-search redu [] origin env (record env{ph = (f ++ b)} ∷ envl) exit -- Stateが先に尽きる | |
| 132 set-state redu origin state@(s ∷ ss) f b env envl exit with b | |
| 133 ... | [] = bit-force-search redu [] origin env (record env{ph = f} ∷ envl) exit | |
| 134 ... | p ∷ ps with next-code p | |
| 135 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 -- 変更対象なので変更して奥に進む | |
| 136 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 -- 変更対象なので変更して奥に進む | |
| 137 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 -- 変更対象なので変更して奥に進む | |
| 138 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 -- 変更対象なので変更して奥に進む | |
| 139 set-state redu origin (s ∷ ss) f b env envl exit | p ∷ ps | _ = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする | |
| 140 | |
| 141 | |
| 142 test-search : List Env | |
| 143 test-search = init-table 3 (λ e0 → brute-force-search e0 (λ e1 → e1)) | |
| 144 | |
| 145 -- テーブルをたどるために若干loopが必要 | |
| 146 pickup-rfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t | |
| 147 pickup-rfork-c ind p env exit = pickup-rfork-p ind [] (table env) p env exit where | |
| 148 pickup-rfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t | |
| 149 pickup-rfork-p zero f [] p env exit = exit env | |
| 150 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する感じ | |
| 151 pickup-rfork-p zero f ((suc x) ∷ ts) p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する | |
| 152 pickup-rfork-p (suc ind) f [] p env exit = exit env | |
| 153 pickup-rfork-p (suc ind) f (x ∷ ts) p env exit = pickup-rfork-p ind (f ++ (x ∷ [])) ts p env exit | |
| 154 | |
| 155 pickup-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t | |
| 156 pickup-lfork-c ind p env exit = pickup-lfork-p (suc ind) [] (table env) p env exit where | |
| 157 pickup-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t | |
| 158 pickup-lfork-p zero f [] p env exit with table env | |
| 159 ... | [] = exit env | |
| 160 ... | 0 ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = true ; next-code = C_eating} ∷ [])); table = ((pid p) ∷ ts)} -- 取得可能なので変更する envの後ろにappendする感じ | |
| 161 ... | (suc x) ∷ ts = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する | |
| 162 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する感じ | |
| 163 pickup-lfork-p zero f ((suc x) ∷ ts) p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する | |
| 164 pickup-lfork-p (suc ind) f [] p env exit = exit env | |
| 165 pickup-lfork-p (suc ind) f (x ∷ ts) p env exit = pickup-lfork-p ind (f ++ (x ∷ [])) ts p env exit | |
| 166 | |
| 167 | |
| 168 putdown-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t | |
| 169 putdown-lfork-c ind p env exit = putdown-lfork-p (suc ind) [] (table env) p env exit where | |
| 170 putdown-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t | |
| 171 putdown-lfork-p zero f [] p env exit with table env | |
| 172 ... | [] = exit env | |
| 173 ... | x ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = false ; next-code = C_putdown_rfork} ∷ [])); table = (0 ∷ ts)} -- 取得可能なので変更する envの後ろにappendする感じ | |
| 174 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する感じ | |
| 175 putdown-lfork-p (suc ind) f [] p env exit = exit env | |
| 176 putdown-lfork-p (suc ind) f (x ∷ ts) p env exit = putdown-lfork-p ind (f ++ (x ∷ [])) ts p env exit | |
| 177 | |
| 178 | |
| 179 | |
| 180 putdown-rfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t | |
| 181 putdown-rfork-c ind p env exit = putdown-rfork-p ind [] (table env) p env exit where | |
| 182 putdown-rfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t | |
| 183 putdown-rfork-p zero f [] p env exit = exit env | |
| 184 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する感じ | |
| 185 putdown-rfork-p (suc ind) f [] p env exit = exit env | |
| 186 putdown-rfork-p (suc ind) f (x ∷ ts) p env exit = putdown-rfork-p ind (f ++ (x ∷ [])) ts p env exit | |
| 187 | |
| 188 | |
| 189 thinking-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t | |
| 190 thinking-c ind p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不要なので変更せず終了する | |
| 191 | |
| 192 code_table-test : {n : Level} {t : Set n} → Code → ℕ → Phi → Env → (Env → t) → t | |
| 193 code_table-test C_putdown_rfork = putdown-rfork-c | |
| 194 code_table-test C_putdown_lfork = putdown-lfork-c | |
| 195 code_table-test C_thinking = thinking-c | |
| 196 code_table-test C_pickup_rfork = pickup-rfork-c | |
| 197 code_table-test C_pickup_lfork = pickup-lfork-c | |
| 198 code_table-test C_eating = thinking-c | |
| 199 -- code_table-test C_set = ? | |
| 200 | |
| 201 step-c : {n : Level} {t : Set n} → Env → (exit : Env → t) → t | |
| 202 step-c env exit = step-p (length (table env)) 0 record env{ph = []} (ph env) exit where | |
| 203 step-p : {n : Level} {t : Set n} → (redu index : ℕ) → Env → (List Phi) → (exit : Env → t) → t | |
| 204 step-p zero ind env pl exit = exit env | |
| 205 step-p (suc redu) ind env [] exit = exit env | |
| 206 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 ) | |
| 207 | |
| 208 step-c-debug : {n : Level} {t : Set n} → Env → (exit : List Env → t) → t | |
| 209 step-c-debug env exit = step-p (length (table env)) 0 (record env{ph = [] } ∷ env ∷ []) (ph env) exit where | |
| 210 step-p : {n : Level} {t : Set n} → (redu index : ℕ) → List Env → (List Phi) → (exit : List Env → t) → t | |
| 211 step-p zero ind envl pl exit = exit envl | |
| 212 step-p (suc redu) ind [] pl exit = exit [] | |
| 213 step-p (suc redu) ind (e ∷ envl) [] exit = exit [] | |
| 214 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 ) | |
| 215 | |
| 216 exec-n : {n : Level} {t : Set n} → ℕ → Env → (exit : List Env → t) → t | |
| 217 exec-n n env exit = exec-n-p n (env ∷ []) exit where | |
| 218 exec-n-p : {n : Level} {t : Set n} → ℕ → List Env → (exit : List Env → t) → t | |
| 219 exec-n-p zero envl exit = exit envl | |
| 220 exec-n-p (suc n) [] exit = exit [] | |
| 221 exec-n-p (suc n) envl@(x ∷ es) exit = step-c x (λ e → exec-n-p n (e ∷ envl) exit) | |
| 222 | |
| 223 init-brute-force : {n : Level} {t : Set n} → List Env → (exit : List (List Env) → t) → t | |
| 224 init-brute-force envl exit = init-brute-force-p envl [] exit where | |
| 225 init-brute-force-p : {n : Level} {t : Set n} → List Env → List (List Env) → (exit : List (List Env) → t) → t | |
| 226 init-brute-force-p [] envll exit = exit envll | |
| 227 init-brute-force-p (x ∷ envl) envll exit = init-brute-force-p envl ((x ∷ []) ∷ envll) exit | |
| 228 | |
| 229 search-brute-force-envll : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t | |
| 230 search-brute-force-envll envll exit = search-brute-force-envll-p [] envll exit where | |
| 231 search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t | |
| 232 search-brute-force-envll-p f [] exit = exit f | |
| 233 search-brute-force-envll-p f ([] ∷ bs) exit = search-brute-force-envll-p f bs exit | |
| 234 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 | |
| 235 make-brute-force-envl : {n : Level} {t : Set n} → List (List Env) → (state p_step : List Env) → (exit : List (List Env) → t) → t | |
| 236 make-brute-force-envl res [] xs exit = exit res | |
| 237 make-brute-force-envl res (x ∷ state) xs exit = make-brute-force-envl (res ++ (x ∷ xs) ∷ []) state xs exit | |
| 238 | |
| 239 step-brute-force : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t | |
| 240 step-brute-force envll exit = step-brute-force-p [] envll exit where | |
| 241 step-brute-force-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t | |
| 242 step-brute-force-p f [] exit = exit f | |
| 243 step-brute-force-p f ([] ∷ bs) exit = step-brute-force-p f bs exit | |
| 244 step-brute-force-p f ((x ∷ xs) ∷ bs) exit = step-c x (λ e0 → step-brute-force-p (f ++ ((e0 ∷ x ∷ xs) ∷ [])) bs exit) | |
| 245 | |
| 246 exec-brute-force : {n : Level} {t : Set n} → ℕ → List (List Env) → (exit : List (List Env) → t) → t | |
| 247 exec-brute-force n envll exit = exec-brute-force-p n envll exit where | |
| 248 exec-brute-force-p : {n : Level} {t : Set n} → ℕ → List (List Env) → (exit : List (List Env) → t) → t | |
| 249 exec-brute-force-p zero envll exit = exit envll | |
| 250 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)) | |
| 251 | |
| 252 {- | |
| 253 model-check-deadlock : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t | |
| 254 model-check-deadlock envll exit = test11 [] envll exit where | |
| 255 test11 : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t | |
| 256 test11 f [] exit = exit f | |
| 257 test11 f ([] ∷ bs) exit = test11 f bs exit | |
| 258 test11 f (s@(x ∷ []) ∷ bs) exit = test11 (f ++ (s ∷ [])) bs exit | |
| 259 test11 f (s@(x ∷ x1 ∷ []) ∷ bs) exit = test11 (f ++ (s ∷ [])) bs exit | |
| 260 test11 f ((x ∷ x1 ∷ x2 ∷ xs) ∷ bs) exit = {!!} | |
| 261 -} | |
| 262 | |
| 263 record metadata : Set where | |
| 264 field | |
| 265 num-branch : ℕ | |
| 266 wait-list : List ℕ | |
| 267 open metadata | |
| 268 | |
| 269 record MetaEnv : Set where | |
| 270 field | |
| 271 DG : List Env | |
| 272 meta : metadata | |
| 273 deadlock : Bool | |
| 274 is-done : Bool | |
| 275 is-step : Bool | |
| 276 open MetaEnv | |
| 277 | |
| 278 record MetaEnv2 : Set where | |
| 279 field | |
| 280 DG : List (List Env) | |
| 281 metal : List MetaEnv -- 結局探索して1ステップ実行(インターリーディング)するからMetaEnvのList Envがちょうどよい | |
| 282 open MetaEnv2 | |
| 283 | |
| 284 branch-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t | |
| 285 branch-deadlock-check metaenv exit = search-brute-force-envll-p [] metaenv exit where | |
| 286 search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t | |
| 287 search-brute-force-envll-p f [] exit = exit f | |
| 288 search-brute-force-envll-p f b@(metaenv ∷ bs) exit with DG metaenv | |
| 289 ... | [] = search-brute-force-envll-p f bs exit | |
| 290 ... | (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 | |
| 291 make-brute-force-envl : {n : Level} {t : Set n} → ℕ → List MetaEnv → MetaEnv → (state : List Env) → (exit : List MetaEnv → t) → t | |
| 292 make-brute-force-envl len res xs [] exit = exit res | |
| 293 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 | |
| 294 | |
| 295 data _===_ {n} {A : Set n} : List A -> List A -> Set n where | |
| 296 reflection : {x : List A} -> x === x | |
| 297 reflection1 : {x : List A} -> (x === x) | |
| 298 | |
| 299 {- | |
| 300 testhoge : Code → Code → ℕ | |
| 301 testhoge C_putdown_rfork C_putdown_rfork = {!!} | |
| 302 testhoge C_putdown_lfork C_putdown_lfork = {!!} | |
| 303 testhoge C_pickup_rfork C_pickup_rfork = {!!} | |
| 304 testhoge C_pickup_lfork C_pickup_lfork = {!!} | |
| 305 testhoge _ _ = {!!} | |
| 306 -} | |
| 307 | |
| 308 step-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t | |
| 309 step-deadlock-check metaenvl exit = deadlock-check-p [] metaenvl exit where | |
| 310 deadlock-check-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t | |
| 311 deadlock-check-p f [] exit = exit f | |
| 312 deadlock-check-p f b@(metaenv ∷ bs) exit with DG metaenv | |
| 313 ... | [] = deadlock-check-p f bs exit | |
| 314 ... | p0 ∷ [] = deadlock-check-p f bs exit | |
| 315 ... | 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 | |
| 316 check-wait-process : {n : Level} {t : Set n} → List ℕ → List Phi → (p1 : Env) → (exit : List ℕ → t) → t | |
| 317 check-wait-process waitl [] p1 exit = exit waitl | |
| 318 check-wait-process waitl (p ∷ ps) p1 exit = hoge11 p (ph p1) (λ e → check-wait-process (waitl ++ e) ps p1 exit) where | |
| 319 hoge11 : {n : Level} {t : Set n} → Phi → List Phi → (exit : List ℕ → t) → t | |
| 320 hoge11 p [] exit = exit [] | |
| 321 hoge11 p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp) | |
| 322 hoge11 p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 p p1s exit | |
| 323 hoge11 p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 p p1s exit | |
| 324 hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p) | |
| 325 hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp) | |
| 326 hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (pid p ∷ []) | |
| 327 hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (pid p ∷ []) | |
| 328 hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (pid p ∷ []) | |
| 329 hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (pid p ∷ []) | |
| 330 hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (pid p ∷ []) | |
| 331 hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (pid p ∷ []) | |
| 332 hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit [] | |
| 333 | |
| 334 step-brute-force-meta : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t | |
| 335 step-brute-force-meta metaenvl exit = step-brute-force-p [] metaenvl exit where | |
| 336 step-brute-force-p : {n : Level} {t : Set n} → (f b : List MetaEnv) → (exit : List MetaEnv → t) → t | |
| 337 step-brute-force-p f [] exit = exit f | |
| 338 step-brute-force-p f (metaenv ∷ bs) exit with DG metaenv | |
| 339 ... | [] = step-brute-force-p f bs exit | |
| 340 ... | envl@(x ∷ xs) with is-done metaenv | |
| 341 ... | true = step-brute-force-p (f ++ (metaenv ∷ []) ) bs exit | |
| 342 ... | false = step-c x (λ e0 → step-brute-force-p (f ++ (record metaenv{DG = e0 ∷ envl} ∷ [])) bs exit) | |
| 343 | |
| 344 | |
| 345 judge-deadlock : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t | |
| 346 judge-deadlock metaenvl exit = judge-deadlock-p [] metaenvl exit where | |
| 347 judge-deadlock-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t | |
| 348 judge-deadlock-p f [] exit = exit f | |
| 349 judge-deadlock-p f (metaenv ∷ bs) exit with num-branch (meta metaenv) | |
| 350 ... | suc (suc branchnum) = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit | |
| 351 ... | zero = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit | |
| 352 ... | suc zero with (DG metaenv ) | |
| 353 ... | [] = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit | |
| 354 ... | p ∷ ps with <-cmp (length (wait-list (meta metaenv))) (length (ph p)) | |
| 355 ... | tri< a ¬b ¬c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit | |
| 356 ... | tri> ¬a ¬b c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit | |
| 357 ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = true} ∷ []) ) bs exit | |
| 358 | |
| 359 | |
| 360 {- | |
| 361 test-env-deadlock : {n : Level} {t : Set n} → (a b : Env)→ (exit : List MetaEnv → t) → t | |
| 362 test-env-deadlock a b exit = test12 (ph a) (ph b) exit where | |
| 363 test12 : {n : Level} {t : Set n} → (a b : List Phi)→ (exit : List MetaEnv → t) → t | |
| 364 test12 [] b = {!!} | |
| 365 test12 (x ∷ a) b = {!!} | |
| 366 -} | |
| 367 | |
| 368 {- | |
| 369 test12 : List ℕ → (a b0 b : List Phi) → List ℕ | |
| 370 test12 stack [] b0 b = stack | |
| 371 test12 stack (a ∷ as) b0 [] = test12 stack as b0 b0 | |
| 372 test12 stack (a ∷ as) b0 (b ∷ bs) with <-cmp (pid a) (pid b) | |
| 373 test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri< a₁ ¬b ¬c = test12 stack al b0 bs | |
| 374 test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri> ¬a ¬b c = test12 stack al b0 bs | |
| 375 test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri≈ ¬a b₁ ¬c with (next-code a) | |
| 376 test12 stack al@(a ∷ as) b0 (b ∷ bs) | _ | aaaa with (next-code b) | |
| 377 test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_putdown_rfork | C_putdown_rfork = pid a ∷ [] | |
| 378 test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_putdown_lfork | C_putdown_lfork = pid a ∷ [] | |
| 379 test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_thinking | C_thinking = pid a ∷ [] | |
| 380 test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_pickup_rfork | C_pickup_rfork = pid a ∷ [] | |
| 381 test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_pickup_lfork | C_pickup_lfork = pid a ∷ [] | |
| 382 test12 stack (a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | C_eating | C_eating = pid a ∷ [] | |
| 383 test12 stack al@(a ∷ as) b0 (b ∷ bs) | tri≈ _ _ _ | _ | _ = test12 stack al b0 bs | |
| 384 -} | |
| 385 | |
| 386 branch-search-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (next exit : MetaEnv2 → t) → t | |
| 387 branch-search-meta2 meta2 next1 exit = search-brute-force-envll-p [] (metal meta2) (λ e0 → next1 record meta2{metal = e0} ) (λ e → exit meta2) where | |
| 388 make-brute-force-envl : {n : Level} {t : Set n} → (statel : List MetaEnv) → ( f : List Env) → (state : MetaEnv) → (exit : List MetaEnv → t) → t | |
| 389 search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (next exit : List MetaEnv → t) → t | |
| 390 search-brute-force-envll-p f [] next1 exit = exit f | |
| 391 search-brute-force-envll-p f b@(x ∷ bs) next1 exit with is-done x | |
| 392 ... | true = search-brute-force-envll-p (f ++ (x ∷ [])) bs next1 exit | |
| 393 ... | false with is-step x | |
| 394 ... | false = search-brute-force-envll-p (f ++ (x ∷ [])) bs next1 exit | |
| 395 ... | true with DG x | |
| 396 ... | [] = search-brute-force-envll-p f bs next1 exit | |
| 397 ... | env1 ∷ sss = brute-force-search env1 (λ e2 → make-brute-force-envl [] e2 x (λ e1 → next1 (f ++ bs ++ (record x{is-done = true} ∷ e1)) ) ) | |
| 398 make-brute-force-envl res [] meta exit = exit res | |
| 399 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 | |
| 400 | |
| 401 | |
| 402 step-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (next exit : MetaEnv2 → t) → t | |
| 403 step-meta2 meta2 next1 exit = step-brute-force-p1 [] (metal meta2) (λ envll → next1 record meta2{metal = envll}) (λ e → exit meta2) where | |
| 404 step-brute-force-p-p : {n : Level} {t : Set n} → (envl : (List Env)) → (exit : (List Env) → t) → t | |
| 405 step-brute-force-p1 : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (next exit : List (MetaEnv) → t) → t | |
| 406 step-brute-force-p1 f [] next1 exit = next1 f | |
| 407 step-brute-force-p1 f (metaenv ∷ metaenvl) next1 exit with is-step metaenv | |
| 408 ... | true = step-brute-force-p1 (f ++ (metaenv ∷ [])) metaenvl next1 exit | |
| 409 ... | false = step-brute-force-p-p (DG metaenv) (λ e0 → step-brute-force-p1 (f ++ (record metaenv{DG = e0; is-step = true} ∷ [])) metaenvl next1 exit) | |
| 410 step-brute-force-p-p [] exit = exit [] | |
| 411 step-brute-force-p-p (x ∷ bs) exit = step-c x (λ e0 → exit (e0 ∷ bs)) | |
| 412 | |
| 413 {-# TERMINATING #-} | |
| 414 check-same-env : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t | |
| 415 check-same-env meta2 exit = check-same-env-p [] (metal meta2) meta2 exit where | |
| 416 check-wait-process-p : {n : Level} {t : Set n} → ℕ → List Phi → (p1 : Env) → (exit : ℕ → t) → t | |
| 417 check-wait-process-p waitl [] p1 exit = exit waitl | |
| 418 check-wait-process-p waitl (p ∷ ps) p1 exit = hoge11 waitl p (ph p1) (λ e → check-wait-process-p e ps p1 exit) where | |
| 419 hoge11 : {n : Level} {t : Set n} → ℕ → Phi → List Phi → (exit : ℕ → t) → t | |
| 420 hoge11 n p [] exit = exit n | |
| 421 hoge11 n p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp) | |
| 422 hoge11 n p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 n p p1s exit | |
| 423 hoge11 n p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 n p p1s exit | |
| 424 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p) | |
| 425 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp) | |
| 426 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (suc n) | |
| 427 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (suc n) | |
| 428 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (suc n) | |
| 429 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (suc n) | |
| 430 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (suc n) | |
| 431 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (suc n) | |
| 432 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit n | |
| 433 check-wait-process : {n : Level} {t : Set n} → ℕ → List Phi → List MetaEnv → MetaEnv → (exit : List MetaEnv → t) → t | |
| 434 check-wait-process n pl metal me exit with metal | |
| 435 ... | sss with <-cmp (length pl) n | |
| 436 ... | tri≈ ¬a b ¬c = exit (me ∷ []) | |
| 437 check-wait-process n pl metal me exit | [] | tri< a ¬b ¬c = exit [] | |
| 438 check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c with DG x | |
| 439 check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c | [] = exit [] | |
| 440 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) | |
| 441 check-wait-process n pl metal me exit | [] | tri> ¬a ¬b c = exit [] | |
| 442 check-wait-process n pl metal me exit | x ∷ sss | tri> ¬a ¬b c with DG x | |
| 443 ... | [] = exit [] | |
| 444 ... | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit) | |
| 445 check-same-env-p : {n : Level} {t : Set n} → (f b : List MetaEnv) → MetaEnv2 → (exit : MetaEnv2 → t) → t | |
| 446 check-same-env-p [] [] metae2 exit = exit metae2 | |
| 447 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 | |
| 448 check-same-env-p [] bl@(b ∷ bs) metae2 exit with DG b | |
| 449 ... | [] = check-same-env-p [] bs metae2 exit | |
| 450 ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p ([] ++ lme) bl metae2 exit) | |
| 451 check-same-env-p f@(x ∷ fs) bl@(b ∷ bs) metae2 exit with DG b | |
| 452 ... | [] = check-same-env-p f bs metae2 exit | |
| 453 ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p (f ++ lme) bl metae2 exit) | |
| 454 | |
| 455 check-same-env-test : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t | |
| 456 check-same-env-test meta2 exit = check-same-env-p [] (metal meta2) meta2 exit where | |
| 457 check-wait-process-p : {n : Level} {t : Set n} → ℕ → List Phi → (p1 : Env) → (exit : ℕ → t) → t | |
| 458 check-wait-process-p waitl [] p1 exit = exit waitl | |
| 459 check-wait-process-p waitl (p ∷ ps) p1 exit = hoge11 waitl p (ph p1) (λ e → check-wait-process-p e ps p1 exit) where | |
| 460 hoge11 : {n : Level} {t : Set n} → ℕ → Phi → List Phi → (exit : ℕ → t) → t | |
| 461 hoge11 n p [] exit = exit n | |
| 462 hoge11 n p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp) | |
| 463 hoge11 n p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 n p p1s exit | |
| 464 hoge11 n p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 n p p1s exit | |
| 465 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p) | |
| 466 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp) | |
| 467 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (suc n) | |
| 468 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (suc n) | |
| 469 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (suc n) | |
| 470 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (suc n) | |
| 471 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (suc n) | |
| 472 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (suc n) | |
| 473 hoge11 n p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit n | |
| 474 check-wait-process : {n : Level} {t : Set n} → ℕ → List Phi → List MetaEnv → MetaEnv → (exit : List MetaEnv → t) → t | |
| 475 check-wait-process n pl metal me exit with metal | |
| 476 ... | sss with <-cmp (length pl) n | |
| 477 ... | tri≈ ¬a b ¬c = exit (me ∷ []) | |
| 478 check-wait-process n pl metal me exit | [] | tri< a ¬b ¬c = exit (me ∷ []) | |
| 479 check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c with DG x | |
| 480 check-wait-process n pl metal me exit | x ∷ sss | tri< a ¬b ¬c | [] = exit [] | |
| 481 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) | |
| 482 check-wait-process n pl metal me exit | [] | tri> ¬a ¬b c = exit (me ∷ []) | |
| 483 check-wait-process n pl metal me exit | x ∷ sss | tri> ¬a ¬b c with DG x | |
| 484 ... | [] = exit [] | |
| 485 ... | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit) | |
| 486 make-metaenvl : {n : Level} {t : Set n} → (f : (List MetaEnv)) → List (List Env) → (exit : List MetaEnv → t) → t | |
| 487 make-metaenvl f [] exit = exit f | |
| 488 make-metaenvl f ([] ∷ bs) exit = make-metaenvl f bs exit | |
| 489 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 | |
| 490 check-same-env-p : {n : Level} {t : Set n} → (f b : List MetaEnv) → MetaEnv2 → (exit : MetaEnv2 → t) → t | |
| 491 check-same-env-p [] [] metae2 exit = make-metaenvl [] (DG metae2) (λ lme → exit record metae2{metal = lme}) | |
| 492 check-same-env-p f@(x ∷ fs) [] metae2 exit = exit record metae2{metal = f} | |
| 493 check-same-env-p [] bl@(b ∷ bs) metae2 exit with DG b | |
| 494 ... | [] = check-same-env-p [] bs metae2 exit | |
| 495 ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p ([] ++ lme) bs metae2 exit) | |
| 496 check-same-env-p f@(x ∷ fs) bl@(b ∷ bs) metae2 exit with DG b | |
| 497 ... | [] = check-same-env-p f bs metae2 exit | |
| 498 ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p (f ++ lme) bs metae2 exit) | |
| 499 | |
| 500 | |
| 501 | |
| 502 {- | |
| 503 search-brute-force-envll : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t | |
| 504 search-brute-force-envll envll exit = search-brute-force-envll-p [] envll exit where | |
| 505 search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t | |
| 506 search-brute-force-envll-p f [] exit = exit f | |
| 507 search-brute-force-envll-p f ([] ∷ bs) exit = search-brute-force-envll-p f bs exit | |
| 508 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 | |
| 509 make-brute-force-envl : {n : Level} {t : Set n} → List (List Env) → (state p_step : List Env) → (exit : List (List Env) → t) → t | |
| 510 make-brute-force-envl res [] xs exit = exit res | |
| 511 make-brute-force-envl res (x ∷ state) xs exit = make-brute-force-envl (res ++ (x ∷ xs) ∷ []) state xs exit | |
| 512 -} | |
| 513 | |
| 514 test-env : Env | |
| 515 test-env = (record { | |
| 516 table = 0 ∷ 0 ∷ 0 ∷ [] | |
| 517 ; ph = record | |
| 518 { pid = 1 | |
| 519 ; left-hand = false | |
| 520 ; right-hand = false | |
| 521 ; next-code = C_thinking | |
| 522 } ∷ record | |
| 523 { pid = 2 | |
| 524 ; left-hand = false | |
| 525 ; right-hand = false | |
| 526 ; next-code = C_thinking | |
| 527 } ∷ record | |
| 528 { pid = 3 | |
| 529 ; left-hand = false | |
| 530 ; right-hand = false | |
| 531 ; next-code = C_thinking | |
| 532 } ∷ [] | |
| 533 }) | |
| 534 test-env1 : Env | |
| 535 test-env1 = (record { | |
| 536 table = 1 ∷ 2 ∷ 0 ∷ [] | |
| 537 ; ph = record | |
| 538 { pid = 1 | |
| 539 ; left-hand = false | |
| 540 ; right-hand = false | |
| 541 ; next-code = C_pickup_rfork | |
| 542 } ∷ record | |
| 543 { pid = 2 | |
| 544 ; left-hand = false | |
| 545 ; right-hand = false | |
| 546 ; next-code = C_pickup_rfork | |
| 547 } ∷ record | |
| 548 { pid = 3 | |
| 549 ; left-hand = false | |
| 550 ; right-hand = false | |
| 551 ; next-code = C_thinking | |
| 552 } ∷ [] | |
| 553 }) | |
| 554 | |
| 555 test-metaenv : MetaEnv | |
| 556 test-metaenv = record | |
| 557 { DG = test-env1 ∷ test-env ∷ [] | |
| 558 ; meta = record { num-branch = zero ; wait-list = [] } | |
| 559 ; deadlock = true ; is-done = false ; is-step = false | |
| 560 } | |
| 561 | |
| 562 test-metaenv1 : MetaEnv | |
| 563 test-metaenv1 = record | |
| 564 { DG = test-env ∷ [] | |
| 565 ; meta = record { num-branch = zero ; wait-list = [] } | |
| 566 ; deadlock = true; is-done = false ; is-step = true | |
| 567 } | |
| 568 test-metaenv2 : MetaEnv2 | |
| 569 test-metaenv2 = record { DG = [] ; metal = test-metaenv ∷ [] } | |
| 570 | |
| 571 test-metaenv3 : MetaEnv2 | |
| 572 test-metaenv3 = record { DG = [] ; metal = test-metaenv1 ∷ [] } | |
| 573 | |
| 574 | |
| 575 | |
| 576 test-envl : List Env | |
| 577 test-envl = test-env1 ∷ test-env1 ∷ [] | |
| 578 | |
| 579 testhoge : {n : Level} {t : Set n} → (env1 env2 : MetaEnv2) → (exit : MetaEnv2 → t) → t | |
| 580 testhoge env1 env2 exit = loop-target-metaenv (metal env1) env2 exit where | |
| 581 eq-pid : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t) → (loop : Bool → t) → t | |
| 582 eq-lhand : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t ) → ( loop : Bool → t) → t | |
| 583 eq-rhand : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t ) → ( loop : Bool → t) → t | |
| 584 eq-next-code : {n : Level} {t : Set n} → MetaEnv2 → (phl1 phl2 : List Phi) → (p1 p2 : Phi) → (exit : MetaEnv2 → t ) → ( loop : Bool → t) → t | |
| 585 eq-env : {n : Level} {t : Set n} → MetaEnv2 → ( e1 e2 : List Phi) → (exit : MetaEnv2 → t) → (loop : Bool → t) → t | |
| 586 | |
| 587 loop-metaenv : {n : Level} {t : Set n} → MetaEnv → (origin : MetaEnv2) → (f b : List MetaEnv) → (exit : MetaEnv2 → t) → t | |
| 588 | |
| 589 loop-target-metaenv : {n : Level} {t : Set n} → (env1 : List MetaEnv) → ( env2 : MetaEnv2) → (exit : MetaEnv2 → t) → t | |
| 590 loop-target-metaenv [] metaenv2 exit = exit metaenv2 | |
| 591 loop-target-metaenv (metaenv ∷ metaenvl) metaenv2 exit = loop-metaenv metaenv metaenv2 [] (metal metaenv2) (λ e → loop-target-metaenv metaenvl e exit) | |
| 592 | |
| 593 boolor : Bool → Bool → Bool | |
| 594 boolor true true = true | |
| 595 boolor true false = true | |
| 596 boolor false true = true | |
| 597 boolor false false = false | |
| 598 | |
| 599 loop-metaenv me origin f [] exit = exit (record origin{metal = me ∷ (metal origin) }) -- not found & add state to origin | |
| 600 loop-metaenv me origin f (x ∷ metaenvl) exit with DG me | |
| 601 ... | [] = exit origin | |
| 602 ... | env1 ∷ envl with DG x | |
| 603 ... | [] = loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit | |
| 604 ... | 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 ) | |
| 605 | |
| 606 eq-env origin [] [] exit loop = exit origin -- true | |
| 607 eq-env origin [] (x ∷ pl2) exit loop = loop false | |
| 608 eq-env origin (p1 ∷ pl1) [] exit loop = loop false | |
| 609 eq-env origin (p1 ∷ pl1) (p2 ∷ pl2) exit loop = eq-pid origin pl1 pl2 p1 p2 exit (λ e → loop e) -- prototype | |
| 610 | |
| 611 eq-pid origin pl1 pl2 p1 p2 next1 exit1 with <-cmp (pid p1) (pid p2) | |
| 612 ... | tri< a ¬b ¬c = exit1 false | |
| 613 ... | tri> ¬a ¬b c = exit1 false | |
| 614 ... | tri≈ ¬a b ¬c = eq-lhand origin pl1 pl2 p1 p2 next1 exit1 | |
| 615 | |
| 616 eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 with (left-hand phi1) | |
| 617 ... | sss with (left-hand phi2) | |
| 618 eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | true = eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | |
| 619 eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | false = exit1 false | |
| 620 eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | true = exit1 false | |
| 621 eq-lhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | false = eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | |
| 622 | |
| 623 eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 with (right-hand phi1) | |
| 624 ... | sss with (right-hand phi2) | |
| 625 eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | true = eq-next-code origin pl1 pl2 phi1 phi2 next1 exit1 | |
| 626 eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | true | false = exit1 false | |
| 627 eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | true = exit1 false | |
| 628 eq-rhand origin pl1 pl2 phi1 phi2 next1 exit1 | false | false = eq-next-code origin pl1 pl2 phi1 phi2 next1 exit1 | |
| 629 | |
| 630 eq-next-code origin pl1 pl2 p1 p2 next1 loop with (next-code p1) | |
| 631 ... | sss with (next-code p2) | |
| 632 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_putdown_rfork | C_putdown_rfork = eq-env origin pl1 pl2 next1 loop | |
| 633 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_putdown_rfork | _ = loop false | |
| 634 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_putdown_lfork | C_putdown_lfork = eq-env origin pl1 pl2 next1 loop | |
| 635 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_putdown_lfork | _ = loop false | |
| 636 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_thinking | C_thinking = eq-env origin pl1 pl2 next1 loop | |
| 637 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_thinking | _ = loop false | |
| 638 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_pickup_rfork | C_pickup_rfork = eq-env origin pl1 pl2 next1 loop | |
| 639 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_pickup_rfork | _ = loop false | |
| 640 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_pickup_lfork | C_pickup_lfork = eq-env origin pl1 pl2 next1 loop | |
| 641 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_pickup_lfork | _ = loop false | |
| 642 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_eating | C_eating = eq-env origin pl1 pl2 next1 loop | |
| 643 eq-next-code origin pl1 pl2 p1 p2 next1 loop | C_eating | _ = loop false | |
| 644 | |
| 645 -- testhoge test-env test-env1 | |
| 646 | |
| 647 {- | |
| 648 testhoge record { table = table₁ ; ph = [] } record { table = table ; ph = [] } = true -- same table? is that realy true ? | |
| 649 testhoge record { table = table₁ ; ph = [] } record { table = table ; ph = (x ∷ ph₁) } = false | |
| 650 testhoge record { table = table₁ ; ph = (x ∷ ph₁) } record { table = table ; ph = [] } = false | |
| 651 testhoge record { table = table₁ ; ph = pl1@(x ∷ ph₁) } record { table = table ; ph = pl2@(x₁ ∷ ph₂) } = {!!} | |
| 652 -} | |
| 653 | |
| 654 | |
| 655 | |
| 656 exec-brute-force-meta : {n : Level} {t : Set n} → ℕ → List MetaEnv → (exit : List MetaEnv → t) → t | |
| 657 exec-brute-force-meta n metaenvl exit = exec-brute-force-p n metaenvl exit where | |
| 658 exec-brute-force-p : {n : Level} {t : Set n} → ℕ → List MetaEnv → (exit : List MetaEnv → t) → t | |
| 659 exec-brute-force-p zero envll exit = exit envll | |
| 660 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)))) | |
| 661 | |
| 662 | |
| 663 test-dead-lock : List MetaEnv | |
| 664 test-dead-lock = exec-brute-force-meta 3 (record | |
| 665 { DG = (record { | |
| 666 table = 0 ∷ 0 ∷ 0 ∷ [] | |
| 667 ; ph = record | |
| 668 { pid = 1 | |
| 669 ; left-hand = false | |
| 670 ; right-hand = false | |
| 671 ; next-code = C_thinking | |
| 672 } ∷ record | |
| 673 { pid = 2 | |
| 674 ; left-hand = false | |
| 675 ; right-hand = false | |
| 676 ; next-code = C_pickup_rfork | |
| 677 } ∷ record | |
| 678 { pid = 3 | |
| 679 ; left-hand = false | |
| 680 ; right-hand = false | |
| 681 ; next-code = C_pickup_rfork | |
| 682 } ∷ [] | |
| 683 }∷ []) | |
| 684 ; meta = record { num-branch = zero ; wait-list = [] } | |
| 685 ; deadlock = false; is-done = false ; is-step = false | |
| 686 } ∷ []) (λ e3 → e3) | |
| 687 | |
| 688 test-dead-lock-meta2 : MetaEnv2 | |
| 689 test-dead-lock-meta2 = branch-search-meta2 (record { DG = (record { table = 0 ∷ 0 ∷ 0 ∷ [] ; ph = record | |
| 690 { pid = 1 | |
| 691 ; left-hand = false | |
| 692 ; right-hand = false | |
| 693 ; next-code = C_thinking | |
| 694 } ∷ record | |
| 695 { pid = 2 | |
| 696 ; left-hand = false | |
| 697 ; right-hand = false | |
| 698 ; next-code = C_pickup_rfork | |
| 699 } ∷ record | |
| 700 { pid = 3 | |
| 701 ; left-hand = false | |
| 702 ; right-hand = false | |
| 703 ; next-code = C_pickup_rfork | |
| 704 } ∷ [] } ∷ []) ∷ [] ; 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) | |
| 705 | |
| 706 | |
| 707 test-dead-lock-meta21 : MetaEnv2 | |
| 708 test-dead-lock-meta21 = branch-search-meta2 (record { DG = (record { table = 0 ∷ 0 ∷ 0 ∷ [] ; ph = record | |
| 709 { pid = 1 | |
| 710 ; left-hand = false | |
| 711 ; right-hand = false | |
| 712 ; next-code = C_thinking | |
| 713 } ∷ record | |
| 714 { pid = 2 | |
| 715 ; left-hand = false | |
| 716 ; right-hand = false | |
| 717 ; next-code = C_pickup_rfork | |
| 718 } ∷ record | |
| 719 { pid = 3 | |
| 720 ; left-hand = false | |
| 721 ; right-hand = false | |
| 722 ; next-code = C_pickup_rfork | |
| 723 } ∷ [] } ∷ []) ∷ [] ; 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) | |
| 724 | |
| 725 | |
| 726 test-dead-lock-meta22 : ℕ → MetaEnv2 → MetaEnv2 | |
| 727 test-dead-lock-meta22 zero metaenv2 = metaenv2 | |
| 728 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) | |
| 729 | |
| 730 {-# TERMINATING #-} | |
| 731 test-dead-lock-loop : MetaEnv2 → MetaEnv2 | |
| 732 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) | |
| 733 | |
| 734 -- test-dead-lock-loop test-metaenv2 | |
| 735 | |
| 736 test-step-c2 : List (List Env) | |
| 737 test-step-c2 = init-brute-force (record { | |
| 738 table = 0 ∷ 0 ∷ 0 ∷ [] | |
| 739 ; ph = record | |
| 740 { pid = 1 | |
| 741 ; left-hand = false | |
| 742 ; right-hand = false | |
| 743 ; next-code = C_thinking | |
| 744 } ∷ record | |
| 745 { pid = 2 | |
| 746 ; left-hand = false | |
| 747 ; right-hand = false | |
| 748 ; next-code = C_pickup_rfork | |
| 749 } ∷ record | |
| 750 { pid = 3 | |
| 751 ; left-hand = false | |
| 752 ; right-hand = false | |
| 753 ; next-code = C_pickup_rfork | |
| 754 } ∷ [] | |
| 755 } ∷ []) (λ e0 → exec-brute-force 2 e0 (λ e2 → e2)) | |
| 756 | |
| 757 -- 以下メモ | |
| 758 | |
| 759 -- eathingの状態はいらない Done | |
| 760 -- tableはℕのList Done | |
| 761 -- いきなりsearchしないで実行結果を持つ感じに | |
| 762 -- stubを使うとCodeの引数がスマートになるのでやる | |
| 763 | |
| 764 -- 実行結果をListでもっているので、stepをじっこうしても変化がなかった場合をdeadlockとして検出したい | |
| 765 -- 東恩納先輩とおなじように、waitに入れて評価する | |
| 766 | |
| 767 -- 余裕があったらassertにLTLの話をいれる | |
| 768 | |
| 769 -- loop execution | |
| 770 | |
| 771 -- concurrnt execution | |
| 772 | |
| 773 -- state db ( binary tree of processes ) | |
| 774 | |
| 775 -- depth first ececution | |
| 776 | |
| 777 -- verify temporal logic poroerries | |
| 778 | |
| 779 | |
| 780 |