|
2
|
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
|
