--- a/DPP/ModelChecking.agda	Mon Jan 23 18:10:19 2023 +0900
+++ b/DPP/ModelChecking.agda	Thu Jan 26 21:49:18 2023 +0900
@@ -136,8 +136,22 @@
       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 -- 変更対象なので変更して奥に進む
       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 -- 変更対象なので変更して奥に進む
       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 -- 変更対象なので変更して奥に進む
-      set-state redu origin (s ∷ ss)     f b env envl exit | p ∷ ps | _ = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
+      set-state redu origin st@(s ∷ ss)     f b env envl exit | p ∷ ps | _ = set-state redu origin st (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
 
+-- eatingも探索範囲に含める
+brute-force-search-1 : {n : Level} {t : Set n} → Env → (exit : List Bool → t) → t
+brute-force-search-1 env exit = make-state-list 1 [] (ph env) env (env ∷ []) exit where
+  make-state-list : {n : Level} {t : Set n} → ℕ → List Bool → List Phi → Env → (List Env) → (exit : List Bool → t) → t
+  make-state-list redu state (x ∷ pl) env envl exit with next-code x
+  ... | C_thinking = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit
+  ... | C_eating = make-state-list (redu + redu) (state ++ (false ∷ [])) pl env envl exit
+  ... | _ = make-state-list redu state pl env envl exit
+  make-state-list redu state [] env envl exit = bit-force-search redu [] state env envl exit where
+    bit-force-search : {n : Level} {t : Set n} → ℕ → (f b : List Bool )→ Env → (List Env) → (exit : List Bool → t) → t
+    bit-force-search zero f l env envl exit = exit []
+    bit-force-search (suc redu) f [] env envl exit = exit []
+    bit-force-search (suc redu) f (true ∷ bs) env envl exit = bit-force-search (suc redu) (f ++ (false ∷ [])) bs env envl exit 
+    bit-force-search (suc redu) f (false ∷ bs) env envl exit = exit (f ++ (true ∷ bs)) 
 
 test-search : List Env
 test-search = init-table 3 (λ e0 → brute-force-search e0 (λ e1 → e1))
@@ -281,6 +295,7 @@
     metal :  List MetaEnv -- 結局探索して1ステップ実行(インターリーディング)するからMetaEnvのList Envがちょうどよい
 open MetaEnv2
 
+-- this one need
 branch-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t
 branch-deadlock-check metaenv exit = search-brute-force-envll-p [] metaenv exit where
   search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
@@ -290,7 +305,8 @@
   ... | (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
     make-brute-force-envl : {n : Level} {t : Set n} → ℕ → List MetaEnv → MetaEnv → (state : List Env) → (exit : List MetaEnv → t) → t
     make-brute-force-envl len res xs [] exit = exit res
-    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
+    make-brute-force-envl len res xs (x ∷ state) exit =  brute-force-search env (λ e0 → search-brute-force-envll-p (f ++ ( record metaenv{meta = record (meta metaenv){num-branch = (length e0)} } ∷ [])) bs exit )
+    -- make-brute-force-envl len (res ++ (record xs{DG = (x ∷ DG xs); meta = record (meta xs){num-branch = len}} ∷ [])) xs state exit
 
 data _===_ {n} {A : Set n} :  List A -> List A -> Set n where
           reflection  : {x : List A} -> x === x
@@ -305,6 +321,7 @@
 testhoge _ _ = {!!}
 -}
 
+-- this need
 step-deadlock-check : {n : Level} {t : Set n} → List MetaEnv → (exit : List MetaEnv → t) → t
 step-deadlock-check metaenvl exit = deadlock-check-p [] metaenvl exit where
   deadlock-check-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
@@ -356,6 +373,45 @@
   ... | tri> ¬a ¬b c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
   ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = true} ∷ []) ) bs exit
 
+waitlist-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
+waitlist-deadlock-metaenv meta2 exit = deadlock-check-p [] (metal meta2) (λ e → exit record meta2{metal = e}) where
+  deadlock-check-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
+  deadlock-check-p f [] exit = exit f
+  deadlock-check-p f b@(metaenv ∷ bs) exit with DG metaenv
+  ... | [] = deadlock-check-p f bs exit
+  ... | p0 ∷ envs = step-c p0 (λ e0 → check-wait-process [] (ph p0) e0 ( λ e → deadlock-check-p (f ++ (record metaenv{meta = record (meta metaenv){wait-list = e } } ∷ [])) bs exit) ) where
+    check-wait-process : {n : Level} {t : Set n} → List ℕ → List Phi → (p1 : Env) → (exit : List ℕ → t) → t
+    check-wait-process waitl [] p1 exit = exit waitl
+    check-wait-process waitl (p ∷ ps) p1 exit = hoge11 p (ph p1)  (λ e → check-wait-process (waitl ++ e) ps p1 exit) where
+      hoge11 : {n : Level} {t : Set n} → Phi → List Phi → (exit : List ℕ → t) → t
+      hoge11 p [] exit = exit []
+      hoge11 p (bp ∷ p1s) exit with <-cmp (pid p) (pid bp)
+      hoge11 p (bp ∷ p1s) exit | tri< a ¬b ¬c = hoge11 p p1s exit
+      hoge11 p (bp ∷ p1s) exit | tri> ¬a ¬b c = hoge11 p p1s exit
+      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c with (next-code p)
+      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | next-codea with (next-code bp)
+      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_rfork | C_putdown_rfork = exit (pid p ∷ [])
+      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_putdown_lfork | C_putdown_lfork = exit (pid p ∷ [])
+      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_thinking | C_thinking = exit (pid p ∷ [])
+      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_rfork | C_pickup_rfork = exit (pid p ∷ [])
+      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_pickup_lfork | C_pickup_lfork = exit (pid p ∷ [])
+      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | C_eating | C_eating = exit (pid p ∷ [])
+      hoge11 p (bp ∷ p1s) exit | tri≈ ¬a b ¬c | _ | _ = exit []
+
+check-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
+check-deadlock-metaenv meta2 exit = search-brute-force-envll-p [] (metal meta2) (λ e → exit record meta2{metal = e}) where
+  search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
+  search-brute-force-envll-p f [] exit = exit f
+  search-brute-force-envll-p f b@(metaenv ∷ bs) exit with DG metaenv
+  ... | [] = search-brute-force-envll-p f bs exit
+  ... | (env ∷ envs) =  brute-force-search env (λ e0 → search-brute-force-envll-p (f ++ ( record metaenv{meta = record (meta metaenv){num-branch = (length e0)} } ∷ [])) bs exit )
+  {-
+  -- brute-force-search env (λ e0 → make-brute-force-envl (length e0)  [] metaenv e0 (λ e1 → search-brute-force-envll-p (f ++ e1) bs exit))  where
+    make-brute-force-envl : {n : Level} {t : Set n} → ℕ → List MetaEnv → MetaEnv → (state : List Env) → (exit : List MetaEnv → t) → t
+    make-brute-force-envl len res xs [] exit = exit res
+    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
+-}
+
 judge-deadlock-metaenv : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
 judge-deadlock-metaenv meta2 exit = judge-deadlock-p [] (metal meta2) (λ e → exit record meta2{metal = e} ) where
   judge-deadlock-p : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
@@ -368,7 +424,7 @@
   ... | p ∷ ps with <-cmp (length (wait-list (meta metaenv))) (length (ph p))
   ... | tri< a ¬b ¬c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
   ... | tri> ¬a ¬b c = judge-deadlock-p (f ++ (metaenv ∷ []) ) bs exit
-  ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = true} ∷ []) ) bs exit
+  ... | tri≈ ¬a b ¬c = judge-deadlock-p (f ++ (record metaenv{deadlock = false} ∷ []) ) bs exit
 
 {-
 test-env-deadlock : {n : Level} {t : Set n} → (a b : Env)→ (exit : List MetaEnv → t) → t
@@ -412,14 +468,14 @@
   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
 
 
-step-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (next exit : MetaEnv2 → t) → t
-step-meta2 meta2 next1 exit = step-brute-force-p1 [] (metal meta2) (λ envll → next1 record meta2{metal = envll}) (λ e → exit meta2) where
+step-meta2 : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
+step-meta2 meta2 exit = step-brute-force-p1 [] (metal meta2) (λ envll → exit record meta2{metal = envll}) where
   step-brute-force-p-p : {n : Level} {t : Set n} → (envl : (List Env)) → (exit : (List Env) → t) → t
-  step-brute-force-p1 : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (next exit : List (MetaEnv) → t) → t
-  step-brute-force-p1 f [] next1 exit = next1 f
-  step-brute-force-p1 f (metaenv ∷ metaenvl) next1 exit with is-step metaenv
-  ... | true =  step-brute-force-p1 (f ++ (metaenv ∷ [])) metaenvl next1 exit
-  ... | false = step-brute-force-p-p (DG metaenv) (λ e0 → step-brute-force-p1 (f ++ (record metaenv{DG = e0; is-step = true} ∷ [])) metaenvl next1 exit)
+  step-brute-force-p1 : {n : Level} {t : Set n} → (f b : List (MetaEnv)) → (exit : List (MetaEnv) → t) → t
+  step-brute-force-p1 f [] exit = exit f
+  step-brute-force-p1 f (metaenv ∷ metaenvl) exit with is-step metaenv
+  ... | true =  step-brute-force-p1 (f ++ (metaenv ∷ [])) metaenvl exit
+  ... | false = step-brute-force-p-p (DG metaenv) (λ e0 → step-brute-force-p1 (f ++ (record metaenv{DG = e0; is-step = true} ∷ [])) metaenvl exit)
   step-brute-force-p-p [] exit = exit []
   step-brute-force-p-p (x ∷ bs) exit = step-c x (λ e0 → exit (e0 ∷ bs))
 
@@ -457,7 +513,7 @@
   ... | env ∷ envs = check-wait-process-p 0 (ph env) env (λ nn → check-wait-process nn pl sss me exit)
   check-same-env-p : {n : Level} {t : Set n} → (f b : List MetaEnv) → MetaEnv2 → (exit : MetaEnv2 → t) → t
   check-same-env-p [] [] metae2 exit = exit metae2
-  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 
+  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 )
   check-same-env-p [] bl@(b ∷ bs) metae2 exit with DG b
   ... | [] =  check-same-env-p [] bs metae2 exit
   ... | env ∷ envs = check-wait-process 0 (ph env) bl b (λ lme → check-same-env-p ([] ++ lme) bl metae2 exit)
@@ -544,19 +600,20 @@
                  ; next-code = C_thinking
                  }  ∷ []
   })
+
 test-env1 : Env
 test-env1 = (record {
-  table = 1 ∷ 2 ∷ 0 ∷ []
+  table = 1 ∷ 0 ∷ 0 ∷ []
   ; ph = record
            { pid = 1
            ; left-hand = false
-           ; right-hand = false
-           ; next-code = C_pickup_rfork
+           ; right-hand = true
+           ; next-code = C_pickup_lfork
            } ∷ record
                  { pid = 2
                  ; left-hand = false
                  ; right-hand = false
-                 ; next-code = C_pickup_rfork
+                 ; next-code = C_thinking
            } ∷ record
                  { pid = 3
                  ; left-hand = false
@@ -614,7 +671,7 @@
   ... | [] = exit origin
   ... | env1 ∷ envl with DG x
   ... | [] = loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit
-  ... | 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 = true } ∷ metaenvl)}) (λ e → loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit )
+  ... | 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) } ∷ metaenvl)}) (λ e → loop-metaenv me origin (f ++ (x ∷ [])) metaenvl exit )
 
   eq-env origin [] [] exit loop = exit origin -- true
   eq-env origin [] (x ∷ pl2) exit loop = loop false
@@ -714,7 +771,7 @@
                  ; left-hand = false
                  ; right-hand = false
                  ; next-code = C_pickup_rfork
-                 }  ∷ [] } ∷ []) ∷ [] ; 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)
+                 }  ∷ [] } ∷ []) ∷ [] ; 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)
 
 
 test-dead-lock-meta21 : MetaEnv2
@@ -733,18 +790,22 @@
                  ; left-hand = false
                  ; right-hand = false
                  ; next-code = C_pickup_rfork
-                 }  ∷ [] } ∷ []) ∷ [] ; 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)
+                 }  ∷ [] } ∷ []) ∷ [] ; 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)
 
 
+check-and-judge-deadlock : {n : Level} {t : Set n} → MetaEnv2 → (exit : MetaEnv2 → t) → t
+check-and-judge-deadlock meta2 exit = check-deadlock-metaenv meta2 (λ e0 → waitlist-deadlock-metaenv e0 (λ e → judge-deadlock-metaenv e exit ) )
+
 test-dead-lock-meta22 : ℕ → MetaEnv2 → MetaEnv2
-test-dead-lock-meta22 zero metaenv2 = metaenv2
-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)
+test-dead-lock-meta22 zero metaenv2 = check-and-judge-deadlock metaenv2 (λ e → e)
+test-dead-lock-meta22 (suc n) metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 metaenv2 (λ me4 → test-dead-lock-meta22 n me4) ) )  (λ e5 → e5)
 
 {-# TERMINATING #-}
 test-dead-lock-loop : MetaEnv2 → MetaEnv2
-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)
+test-dead-lock-loop metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 metaenv2 (λ me4 → test-dead-lock-loop me4) ) ) (λ e → e)
 
--- test-dead-lock-loop test-metaenv3
+test-dead-lock-loop2 : MetaEnv2 → MetaEnv2
+test-dead-lock-loop2 metaenv2 = branch-search-meta2 metaenv2 (λ me2 → step-meta2 me2 (λ me3 → testhoge me3 metaenv2 (λ me4 → test-dead-lock-loop me4) ) ) (λ e → check-and-judge-deadlock e (λ e1 → e1) )
 
 test-step-c2 : List (List Env)
 test-step-c2 = init-brute-force (record {