|
1
|
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
|
|
|
21
|
|
|
22 record AtomicNat : Set where
|
|
|
23 field
|
|
|
24 value : ℕ
|
|
|
25
|
|
|
26 set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t
|
|
|
27 set a v next = next record { value = v }
|
|
|
28
|
|
|
29 record Phils : Set where
|
|
|
30 field
|
|
|
31 pid : ℕ
|
|
|
32 left right : AtomicNat
|
|
|
33
|
|
|
34 putdown_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
|
35 putdown_rfork p next = set (Phils.right p) 0 ( λ f → next record p { right = f } )
|
|
|
36
|
|
|
37 putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
|
38 putdown_lfork p next = set (Phils.left p) 0 ( λ f → next record p { left = f } )
|
|
|
39
|
|
|
40 thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
|
41 thinking p next = next p
|
|
|
42
|
|
|
43 pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
|
44 pickup_rfork p next = set (Phils.right p) (Phils.pid p) ( λ f → next record p { right = f } )
|
|
|
45
|
|
|
46 pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
|
47 pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → next record p { left = f } )
|
|
|
48
|
|
|
49 --eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
|
|
|
50 --eating p next = next p
|
|
|
51
|
|
|
52 data Code : Set where
|
|
|
53 C_putdown_rfork : Code
|
|
|
54 C_putdown_lfork : Code
|
|
|
55 C_thinking : Code
|
|
|
56 C_pickup_rfork : Code
|
|
|
57 C_pickup_lfork : Code
|
|
|
58 C_eating : Code
|
|
|
59
|
|
|
60 record Process : Set where
|
|
|
61 field
|
|
|
62 phil : Phils
|
|
|
63 next_code : Code
|
|
|
64
|
|
|
65 putdown_rfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t
|
|
|
66 putdown_rfork_stub p next = putdown_rfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } )
|
|
|
67
|
|
|
68 putdown_lfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t
|
|
|
69 putdown_lfork_stub p next = putdown_lfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } )
|
|
|
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 open Process
|
|
|
81
|
|
|
82 step : {n : Level} {t : Set n} → List Process → (List Process → t) → t
|
|
|
83 step {n} {t} [] next0 = next0 []
|
|
|
84 step {n} {t} (p ∷ ps) next0 = code_table (next_code p) p ( λ np → next0 (ps ++ ( np ∷ [] ) ))
|
|
|
85
|
|
|
86 test : List Process
|
|
|
87 test = step ( record { phil = record { pid = 1 ; left = record { value = 1 } ; right = record { value = 1 } } ; next_code = C_putdown_rfork } ∷ [] ) ( λ ps → ps )
|
|
|
88
|
|
|
89 test1 : List Process
|
|
|
90 test1 = step ( record { phil = record { pid = 1 ; left = record { value = 1 } ; right = record { value = 1 } } ; next_code = C_putdown_rfork } ∷ [] )
|
|
|
91 $ λ ps → step ps $ λ ps → ps
|
|
|
92
|
|
|
93 record Phi : Set where
|
|
|
94 field
|
|
|
95 pid : ℕ
|
|
|
96 right-hand : Bool
|
|
|
97 left-hand : Bool
|
|
|
98 next-code : Code
|
|
|
99 open Phi
|
|
|
100
|
|
|
101 record Env : Set where
|
|
|
102 field
|
|
|
103 table : List ℕ
|
|
|
104 ph : List Phi
|
|
|
105 open Env
|
|
|
106
|
|
|
107 init-table : {n : Level} {t : Set n} → ℕ → (exit : Env → t) → t
|
|
|
108 init-table n exit = init-table-loop n 0 (record {table = [] ; ph = []}) exit where
|
|
|
109 init-table-loop : {n : Level} {t : Set n} → (redu inc : ℕ) → Env → (exit : Env → t) → t
|
|
|
110 init-table-loop zero ind env exit = exit env
|
|
|
111 init-table-loop (suc redu) ind env exit = init-table-loop redu (suc ind) record env{
|
|
|
112 table = 0 ∷ (table env)
|
|
|
113 ; ph = record {pid = redu ; left-hand = false ; right-hand = false ; next-code = C_thinking } ∷ (ph env) } exit
|
|
|
114
|
|
|
115 -- eatingも探索範囲に含める
|
|
|
116 brute-force-search : {n : Level} {t : Set n} → Env → (exit : List Env → t) → t
|
|
|
117 brute-force-search env exit = make-state-list 1 [] (ph env) env (env ∷ []) exit where
|
|
|
118 make-state-list : {n : Level} {t : Set n} → ℕ → List Bool → List Phi → Env → (List Env) → (exit : List Env → t) → t
|
|
|
119 make-state-list redu state (x ∷ pl) env envl exit with next-code x
|
|
|
120 ... | C_thinking = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit
|
|
|
121 ... | C_eating = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit
|
|
|
122 ... | _ = make-state-list redu state pl env envl exit
|
|
|
123 make-state-list redu state [] env envl exit = bit-force-search redu [] state env envl exit where
|
|
|
124 bit-force-search : {n : Level} {t : Set n} → ℕ → (f b : List Bool )→ Env → (List Env) → (exit : List Env → t) → t
|
|
|
125 bit-force-search zero f l env envl exit = exit envl
|
|
|
126 bit-force-search (suc redu) f [] env envl exit = exit envl
|
|
|
127 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を次の対象にする
|
|
|
128 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させる
|
|
|
129 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のやつのみ
|
|
|
130 set-state redu origin [] f b env envl exit = bit-force-search redu [] origin env (record env{ph = (f ++ b)} ∷ envl) exit -- Stateが先に尽きる
|
|
|
131 set-state redu origin state@(s ∷ ss) f b env envl exit with b
|
|
|
132 ... | [] = bit-force-search redu [] origin env (record env{ph = f} ∷ envl) exit
|
|
|
133 ... | p ∷ ps with next-code p
|
|
|
134 ... | C_putdown_rfork = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
|
|
|
135 ... | C_putdown_lfork = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
|
|
|
136 ... | C_pickup_rfork = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
|
|
|
137 ... | C_pickup_lfork = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
|
|
|
138 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 -- 変更対象なので変更して奥に進む
|
|
|
139 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 -- 変更対象なので変更して奥に進む
|
|
|
140 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 -- 変更対象なので変更して奥に進む
|
|
|
141 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 -- 変更対象なので変更して奥に進む
|
|
|
142
|
|
|
143
|
|
|
144
|
|
|
145 test-search : List Env
|
|
|
146 test-search = init-table 3 (λ e0 → brute-force-search e0 (λ e1 → e1))
|
|
|
147
|
|
|
148 -- テーブルをたどるために若干loopが必要
|
|
|
149 pickup-rfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
|
|
|
150 pickup-rfork-c ind p env exit = pickup-rfork-p ind [] (table env) p env exit where
|
|
|
151 pickup-rfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
|
|
|
152 pickup-rfork-p zero f [] p env exit = exit env
|
|
|
153 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する感じ
|
|
|
154 pickup-rfork-p zero f ((suc x) ∷ ts) p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する
|
|
|
155 pickup-rfork-p (suc ind) f [] p env exit = exit env
|
|
|
156 pickup-rfork-p (suc ind) f (x ∷ ts) p env exit = pickup-rfork-p ind (f ++ (x ∷ [])) ts p env exit
|
|
|
157
|
|
|
158 pickup-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
|
|
|
159 pickup-lfork-c ind p env exit = pickup-lfork-p (suc ind) [] (table env) p env exit where
|
|
|
160 pickup-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
|
|
|
161 pickup-lfork-p zero f [] p env exit with table env
|
|
|
162 ... | [] = exit env
|
|
|
163 ... | 0 ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = true ; next-code = C_eating} ∷ [])); table = ((pid p) ∷ ts)} -- 取得可能なので変更する envの後ろにappendする感じ
|
|
|
164 ... | (suc x) ∷ ts = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する
|
|
|
165 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する感じ
|
|
|
166 pickup-lfork-p zero f ((suc x) ∷ ts) p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する
|
|
|
167 pickup-lfork-p (suc ind) f [] p env exit = exit env
|
|
|
168 pickup-lfork-p (suc ind) f (x ∷ ts) p env exit = pickup-lfork-p ind (f ++ (x ∷ [])) ts p env exit
|
|
|
169
|
|
|
170
|
|
|
171 putdown-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
|
|
|
172 putdown-lfork-c ind p env exit = putdown-lfork-p (suc ind) [] (table env) p env exit where
|
|
|
173 putdown-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
|
|
|
174 putdown-lfork-p zero f [] p env exit with table env
|
|
|
175 ... | [] = exit env
|
|
|
176 ... | x ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = false ; next-code = C_putdown_rfork} ∷ [])); table = (0 ∷ ts)} -- 取得可能なので変更する envの後ろにappendする感じ
|
|
|
177 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する感じ
|
|
|
178 putdown-lfork-p (suc ind) f [] p env exit = exit env
|
|
|
179 putdown-lfork-p (suc ind) f (x ∷ ts) p env exit = putdown-lfork-p ind (f ++ (x ∷ [])) ts p env exit
|
|
|
180
|
|
|
181
|
|
|
182
|
|
|
183 putdown-rfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
|
|
|
184 putdown-rfork-c ind p env exit = putdown-rfork-p ind [] (table env) p env exit where
|
|
|
185 putdown-rfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
|
|
|
186 putdown-rfork-p zero f [] p env exit = exit env
|
|
|
187 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する感じ
|
|
|
188 putdown-rfork-p (suc ind) f [] p env exit = exit env
|
|
|
189 putdown-rfork-p (suc ind) f (x ∷ ts) p env exit = putdown-rfork-p ind (f ++ (x ∷ [])) ts p env exit
|
|
|
190
|
|
|
191
|
|
|
192 thinking-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
|
|
|
193 thinking-c ind p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不要なので変更せず終了する
|
|
|
194
|
|
|
195 code_table-test : {n : Level} {t : Set n} → Code → ℕ → Phi → Env → (Env → t) → t
|
|
|
196 code_table-test C_putdown_rfork = putdown-rfork-c
|
|
|
197 code_table-test C_putdown_lfork = putdown-lfork-c
|
|
|
198 code_table-test C_thinking = thinking-c
|
|
|
199 code_table-test C_pickup_rfork = pickup-rfork-c
|
|
|
200 code_table-test C_pickup_lfork = pickup-lfork-c
|
|
|
201 code_table-test C_eating = thinking-c
|
|
|
202
|
|
|
203 step-c : {n : Level} {t : Set n} → Env → (exit : Env → t) → t
|
|
|
204 step-c env exit = step-p (length (table env)) 0 record env{ph = []} (ph env) exit where
|
|
|
205 step-p : {n : Level} {t : Set n} → (redu index : ℕ) → Env → (List Phi) → (exit : Env → t) → t
|
|
|
206 step-p zero ind env pl exit = exit env
|
|
|
207 step-p (suc redu) ind env [] exit = exit env
|
|
|
208 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 )
|
|
|
209
|
|
|
210 step-c-debug : {n : Level} {t : Set n} → Env → (exit : List Env → t) → t
|
|
|
211 step-c-debug env exit = step-p (length (table env)) 0 (record env{ph = [] } ∷ env ∷ []) (ph env) exit where
|
|
|
212 step-p : {n : Level} {t : Set n} → (redu index : ℕ) → List Env → (List Phi) → (exit : List Env → t) → t
|
|
|
213 step-p zero ind envl pl exit = exit envl
|
|
|
214 step-p (suc redu) ind [] pl exit = exit []
|
|
|
215 step-p (suc redu) ind (e ∷ envl) [] exit = exit []
|
|
|
216 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 )
|
|
|
217
|
|
|
218 exec-n : {n : Level} {t : Set n} → ℕ → Env → (exit : List Env → t) → t
|
|
|
219 exec-n n env exit = exec-n-p n (env ∷ []) exit where
|
|
|
220 exec-n-p : {n : Level} {t : Set n} → ℕ → List Env → (exit : List Env → t) → t
|
|
|
221 exec-n-p zero envl exit = exit envl
|
|
|
222 exec-n-p (suc n) [] exit = exit []
|
|
|
223 exec-n-p (suc n) envl@(x ∷ es) exit = step-c x (λ e → exec-n-p n (e ∷ envl) exit)
|
|
|
224
|
|
|
225 init-brute-force : {n : Level} {t : Set n} → List Env → (exit : List (List Env) → t) → t
|
|
|
226 init-brute-force envl exit = init-brute-force-p envl [] exit where
|
|
|
227 init-brute-force-p : {n : Level} {t : Set n} → List Env → List (List Env) → (exit : List (List Env) → t) → t
|
|
|
228 init-brute-force-p [] envll exit = exit envll
|
|
|
229 init-brute-force-p (x ∷ envl) envll exit = init-brute-force-p envl ((x ∷ []) ∷ envll) exit
|
|
|
230
|
|
|
231 search-brute-force-envll : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t
|
|
|
232 search-brute-force-envll envll exit = search-brute-force-envll-p [] envll exit where
|
|
|
233 search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t
|
|
|
234 search-brute-force-envll-p f [] exit = exit f
|
|
|
235 search-brute-force-envll-p f ([] ∷ bs) exit = search-brute-force-envll-p f bs exit
|
|
|
236 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
|
|
|
237 make-brute-force-envl : {n : Level} {t : Set n} → List (List Env) → (state p_step : List Env) → (exit : List (List Env) → t) → t
|
|
|
238 make-brute-force-envl res [] xs exit = exit res
|
|
|
239 make-brute-force-envl res (x ∷ state) xs exit = make-brute-force-envl (res ++ (x ∷ xs) ∷ []) state xs exit
|
|
|
240
|
|
|
241 step-brute-force : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t
|
|
|
242 step-brute-force envll exit = step-brute-force-p [] envll exit where
|
|
|
243 step-brute-force-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t
|
|
|
244 step-brute-force-p f [] exit = exit f
|
|
|
245 step-brute-force-p f ([] ∷ bs) exit = step-brute-force-p f bs exit
|
|
|
246 step-brute-force-p f ((x ∷ xs) ∷ bs) exit = step-c x (λ e0 → step-brute-force-p (f ++ ((e0 ∷ x ∷ xs) ∷ [])) bs exit)
|
|
|
247
|
|
|
248 exec-brute-force : {n : Level} {t : Set n} → ℕ → List (List Env) → (exit : List (List Env) → t) → t
|
|
|
249 exec-brute-force n envll exit = exec-brute-force-p n envll exit where
|
|
|
250 exec-brute-force-p : {n : Level} {t : Set n} → ℕ → List (List Env) → (exit : List (List Env) → t) → t
|
|
|
251 exec-brute-force-p zero envll exit = exit envll
|
|
|
252 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))
|
|
|
253
|
|
|
254 model-check-deadlock : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t
|
|
|
255 model-check-deadlock envll exit = test11 [] envll exit where
|
|
|
256 test11 : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t
|
|
|
257 test11 f [] exit = exit f
|
|
|
258 test11 f ([] ∷ bs) exit = test11 f bs exit
|
|
|
259 test11 f (s@(x ∷ []) ∷ bs) exit = test11 (f ++ (s ∷ [])) bs exit
|
|
|
260 test11 f (s@(x ∷ x1 ∷ []) ∷ bs) exit = test11 (f ++ (s ∷ [])) bs exit
|
|
|
261 test11 f ((x ∷ x1 ∷ x2 ∷ xs) ∷ bs) exit = {!!}
|
|
|
262
|
|
|
263
|
|
|
264
|
|
|
265 data _===_ {n} {A : Set n} : List A -> List A -> Set n where
|
|
|
266 reflection : {x : List A} -> x === x
|
|
|
267 reflection1 : {x : List A} -> (x === x)
|
|
|
268
|
|
|
269 testhoge : Code → Code → ℕ
|
|
|
270 testhoge C_putdown_rfork C_putdown_rfork = {!!}
|
|
|
271 testhoge C_putdown_lfork C_putdown_lfork = {!!}
|
|
|
272 testhoge C_pickup_rfork C_pickup_rfork = {!!}
|
|
|
273 testhoge C_pickup_lfork C_pickup_lfork = {!!}
|
|
|
274 testhoge _ _ = {!!}
|
|
|
275
|
|
|
276
|
|
|
277 test-step-c : (List Env)
|
|
|
278 test-step-c = brute-force-search record {
|
|
|
279 table = 0 ∷ 0 ∷ 0 ∷ []
|
|
|
280 ; ph = record
|
|
|
281 { pid = 1
|
|
|
282 ; left-hand = false
|
|
|
283 ; right-hand = false
|
|
|
284 ; next-code = C_pickup_rfork
|
|
|
285 } ∷ record
|
|
|
286 { pid = 2
|
|
|
287 ; left-hand = false
|
|
|
288 ; right-hand = false
|
|
|
289 ; next-code = C_pickup_rfork
|
|
|
290 } ∷ record
|
|
|
291 { pid = 3
|
|
|
292 ; left-hand = false
|
|
|
293 ; right-hand = false
|
|
|
294 ; next-code = C_pickup_rfork
|
|
|
295 } ∷ []
|
|
|
296 } (λ e2 → e2)
|
|
|
297
|
|
|
298 test-step-c2 : List (List Env)
|
|
|
299 test-step-c2 = init-brute-force (record {
|
|
|
300 table = 0 ∷ 0 ∷ 0 ∷ []
|
|
|
301 ; ph = record
|
|
|
302 { pid = 1
|
|
|
303 ; left-hand = false
|
|
|
304 ; right-hand = false
|
|
|
305 ; next-code = C_thinking
|
|
|
306 } ∷ record
|
|
|
307 { pid = 2
|
|
|
308 ; left-hand = false
|
|
|
309 ; right-hand = false
|
|
|
310 ; next-code = C_pickup_rfork
|
|
|
311 } ∷ record
|
|
|
312 { pid = 3
|
|
|
313 ; left-hand = false
|
|
|
314 ; right-hand = false
|
|
|
315 ; next-code = C_pickup_rfork
|
|
|
316 } ∷ []
|
|
|
317 } ∷ []) (λ e0 → exec-brute-force 2 e0 (λ e2 → e2))
|
|
|
318
|
|
|
319 -- 以下メモ
|
|
|
320
|
|
|
321 -- eathingの状態はいらない Done
|
|
|
322 -- tableはℕのList Done
|
|
|
323 -- いきなりsearchしないで実行結果を持つ感じに
|
|
|
324 -- stubを使うとCodeの引数がスマートになるのでやる
|
|
|
325
|
|
|
326 -- 実行結果をListでもっているので，stepをじっこうしても変化がなかった場合をdeadlockとして検出したい
|
|
|
327 -- 東恩納先輩とおなじように，waitに入れて評価する
|
|
|
328
|
|
|
329 -- 余裕があったらassertにLTLの話をいれる
|
|
|
330
|
|
|
331 -- loop execution
|
|
|
332
|
|
|
333 -- concurrnt execution
|
|
|
334
|
|
|
335 -- state db ( binary tree of processes )
|
|
|
336
|
|
|
337 -- depth first ececution
|
|
|
338
|
|
|
339 -- verify temporal logic poroerries
|
|
|
340
|
|
|
341
|
|
|
342
|
