module ModelChecking where

open import Level renaming (zero to Z ; suc to succ)

open import Data.Nat hiding (compare)
open import Data.Nat.Properties as NatProp
open import Data.Maybe
-- open import Data.Maybe.Properties
open import Data.Empty
open import Data.List
open import Data.Product
open import Function as F hiding (const)
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
open import logic
open import Data.Unit hiding (_≟_ ; _≤?_ ; _≤_)
open import Relation.Binary.Definitions



record AtomicNat : Set where
   field
      value : ℕ

set : {n : Level } {t : Set n} → AtomicNat → (value : ℕ) → ( AtomicNat → t ) → t
set a v next = next record { value = v }

record Phils  : Set  where
   field
      pid : ℕ
      left right : AtomicNat

putdown_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
putdown_rfork p next = set (Phils.right p) 0 ( λ f → next record p { right = f } )

putdown_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
putdown_lfork p next = set (Phils.left p) 0 ( λ f → next record p { left = f } )

thinking : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
thinking p next = next p

pickup_rfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
pickup_rfork p next = set (Phils.right p) (Phils.pid p) ( λ f → next record p { right = f } )

pickup_lfork : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
pickup_lfork p next = set (Phils.left p) (Phils.pid p) ( λ f → next record p { left = f } )

--eating : {n : Level} {t : Set n} → Phils → ( Phils → t ) → t
--eating p next = next  p

data Code : Set  where
   C_putdown_rfork : Code
   C_putdown_lfork : Code
   C_thinking : Code
   C_pickup_rfork : Code
   C_pickup_lfork : Code
   C_eating : Code

record Process : Set  where
   field
      phil : Phils
      next_code : Code

putdown_rfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t
putdown_rfork_stub p next = putdown_rfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } )

putdown_lfork_stub : {n : Level} {t : Set n} → Process → ( Process → t) → t
putdown_lfork_stub p next = putdown_lfork ( Process.phil p ) ( λ ph → next record p { phil = ph ; next_code = C_putdown_lfork } )

code_table :  {n : Level} {t : Set n} → Code → Process → ( Process → t) → t
-- code_table C_set  = {!!}
code_table C_putdown_rfork = putdown_rfork_stub
code_table C_putdown_lfork = putdown_lfork_stub
code_table C_thinking = {!!}
code_table C_pickup_rfork = {!!}
code_table C_pickup_lfork = {!!}
code_table C_eating = {!!}

open Process

step : {n : Level} {t : Set n} → List Process → (List Process → t) → t
step {n} {t} [] next0 = next0 []
step {n} {t} (p ∷ ps) next0 = code_table (next_code p) p ( λ np → next0 (ps ++ ( np ∷ [] ) ))

test : List Process
test = step ( record { phil = record { pid = 1 ; left = record { value = 1 }  ; right = record { value = 1 }  } ; next_code = C_putdown_rfork } ∷ [] ) ( λ ps → ps )

test1 : List Process
test1 = step ( record { phil = record { pid = 1 ; left = record { value = 1 }  ; right = record { value = 1 }  } ; next_code = C_putdown_rfork } ∷ [] )
  $ λ ps → step ps $ λ ps → ps

record Phi : Set where
  field
    pid : ℕ
    right-hand : Bool
    left-hand : Bool
    next-code : Code
open Phi

record Env : Set where
  field
    table : List ℕ
    ph : List Phi
open Env

init-table : {n : Level} {t : Set n} → ℕ → (exit : Env → t) → t
init-table n exit = init-table-loop n 0 (record {table = [] ; ph = []}) exit where
  init-table-loop : {n : Level} {t : Set n} → (redu inc : ℕ) → Env → (exit : Env → t) → t
  init-table-loop zero ind env exit = exit env
  init-table-loop (suc redu) ind env exit = init-table-loop redu (suc ind) record env{
    table = 0 ∷ (table env)
    ; ph = record {pid = redu ; left-hand = false ; right-hand = false ; next-code = C_thinking } ∷ (ph env) } exit

-- eatingも探索範囲に含める
brute-force-search : {n : Level} {t : Set n} → Env → (exit : List Env → t) → t
brute-force-search 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 Env → 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 Env → t) → t
    bit-force-search zero f l env envl exit = exit envl
    bit-force-search (suc redu) f [] env envl exit = exit envl
    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を次の対象にする
    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させる
      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のやつのみ
      set-state redu origin [] f b env envl exit = bit-force-search redu [] origin env (record env{ph = (f ++ b)} ∷ envl) exit -- Stateが先に尽きる
      set-state redu origin state@(s ∷ ss) f b env envl exit with b
      ... | [] = bit-force-search redu [] origin env (record env{ph = f} ∷ envl) exit
      ... | p ∷ ps with next-code p
      ... | C_putdown_rfork = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
      ... | C_putdown_lfork = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
      ... | C_pickup_rfork = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
      ... | C_pickup_lfork = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
      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 -- 変更対象なので変更して奥に進む
      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 -- 変更対象なので変更して奥に進む



test-search : List Env
test-search = init-table 3 (λ e0 → brute-force-search e0 (λ e1 → e1))

-- テーブルをたどるために若干loopが必要
pickup-rfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
pickup-rfork-c ind p env exit = pickup-rfork-p ind [] (table env) p env exit where
  pickup-rfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
  pickup-rfork-p zero f [] p env exit = exit env
  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する感じ
  pickup-rfork-p zero f ((suc x) ∷ ts) p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する
  pickup-rfork-p (suc ind) f [] p env exit = exit env
  pickup-rfork-p (suc ind) f (x ∷ ts) p env exit = pickup-rfork-p ind (f ++ (x ∷ [])) ts p env exit

pickup-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
pickup-lfork-c ind p env exit = pickup-lfork-p (suc ind) [] (table env) p env exit where
  pickup-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
  pickup-lfork-p zero f [] p env exit with table env
  ... | [] = exit env
  ... | 0 ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = true ; next-code = C_eating} ∷ [])); table = ((pid p) ∷ ts)} -- 取得可能なので変更する envの後ろにappendする感じ
  ... | (suc x) ∷ ts = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する
  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する感じ
  pickup-lfork-p zero f ((suc x) ∷ ts) p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する
  pickup-lfork-p (suc ind) f [] p env exit = exit env
  pickup-lfork-p (suc ind) f (x ∷ ts) p env exit = pickup-lfork-p ind (f ++ (x ∷ [])) ts p env exit


putdown-lfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
putdown-lfork-c ind p env exit = putdown-lfork-p (suc ind) [] (table env) p env exit where
  putdown-lfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
  putdown-lfork-p zero f [] p env exit with table env
  ... | [] = exit env
  ... | x ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = false ; next-code = C_putdown_rfork} ∷ [])); table = (0 ∷ ts)} -- 取得可能なので変更する envの後ろにappendする感じ
  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する感じ
  putdown-lfork-p (suc ind) f [] p env exit = exit env
  putdown-lfork-p (suc ind) f (x ∷ ts) p env exit = putdown-lfork-p ind (f ++ (x ∷ [])) ts p env exit



putdown-rfork-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
putdown-rfork-c ind p env exit = putdown-rfork-p ind [] (table env) p env exit where
  putdown-rfork-p : {n : Level} {t : Set n} → ℕ → (f b : List ℕ) → Phi → Env → (Env → t) → t
  putdown-rfork-p zero f [] p env exit = exit env
  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する感じ
  putdown-rfork-p (suc ind) f [] p env exit = exit env
  putdown-rfork-p (suc ind) f (x ∷ ts) p env exit = putdown-rfork-p ind (f ++ (x ∷ [])) ts p env exit


thinking-c : {n : Level} {t : Set n} → ℕ → Phi → Env → (Env → t) → t
thinking-c ind p env exit = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不要なので変更せず終了する

code_table-test : {n : Level} {t : Set n} → Code → ℕ → Phi → Env → (Env → t) → t
code_table-test C_putdown_rfork = putdown-rfork-c
code_table-test C_putdown_lfork = putdown-lfork-c
code_table-test C_thinking = thinking-c
code_table-test C_pickup_rfork = pickup-rfork-c
code_table-test C_pickup_lfork = pickup-lfork-c
code_table-test C_eating = thinking-c

step-c : {n : Level} {t : Set n} → Env → (exit : Env → t) → t
step-c env exit = step-p (length (table env)) 0 record env{ph = []} (ph env) exit where
  step-p : {n : Level} {t : Set n} → (redu index : ℕ) → Env → (List Phi) → (exit : Env → t) → t
  step-p zero ind env pl exit = exit env
  step-p (suc redu) ind env [] exit = exit env
  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 )

step-c-debug : {n : Level} {t : Set n} → Env → (exit : List Env → t) → t
step-c-debug env exit = step-p (length (table env)) 0 (record env{ph = [] } ∷ env ∷ []) (ph env) exit where
  step-p : {n : Level} {t : Set n} → (redu index : ℕ) → List Env → (List Phi) → (exit : List Env → t) → t
  step-p zero ind envl pl exit = exit envl
  step-p (suc redu) ind [] pl exit = exit []
  step-p (suc redu) ind (e ∷ envl) [] exit = exit []
  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 )

exec-n : {n : Level} {t : Set n} → ℕ → Env → (exit : List Env → t) → t
exec-n n env exit = exec-n-p n (env ∷ []) exit where
  exec-n-p : {n : Level} {t : Set n} → ℕ → List Env → (exit : List Env → t) → t
  exec-n-p zero envl exit = exit envl
  exec-n-p (suc n) [] exit = exit []
  exec-n-p (suc n) envl@(x ∷ es) exit = step-c x (λ e → exec-n-p n (e ∷ envl) exit)

init-brute-force : {n : Level} {t : Set n} → List Env → (exit : List (List Env) → t) → t
init-brute-force envl exit = init-brute-force-p envl [] exit where
  init-brute-force-p : {n : Level} {t : Set n} → List Env → List (List Env) → (exit : List (List Env) → t) → t
  init-brute-force-p [] envll exit = exit envll
  init-brute-force-p (x ∷ envl) envll exit = init-brute-force-p envl ((x ∷ [])  ∷ envll) exit

search-brute-force-envll : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t
search-brute-force-envll envll exit = search-brute-force-envll-p [] envll exit where
  search-brute-force-envll-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t
  search-brute-force-envll-p f [] exit = exit f
  search-brute-force-envll-p f ([] ∷ bs) exit = search-brute-force-envll-p f bs exit
  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
    make-brute-force-envl : {n : Level} {t : Set n} → List (List Env) → (state p_step : List Env) → (exit : List (List Env) → t) → t
    make-brute-force-envl res [] xs exit = exit res
    make-brute-force-envl res (x ∷ state) xs exit = make-brute-force-envl (res ++ (x ∷ xs) ∷ []) state xs exit

step-brute-force : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t
step-brute-force envll exit = step-brute-force-p [] envll exit where
  step-brute-force-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t
  step-brute-force-p f [] exit = exit f
  step-brute-force-p f ([] ∷ bs) exit = step-brute-force-p f bs exit
  step-brute-force-p f ((x ∷ xs) ∷ bs) exit = step-c x (λ e0 → step-brute-force-p (f ++ ((e0 ∷ x ∷ xs) ∷ [])) bs exit)

exec-brute-force : {n : Level} {t : Set n} → ℕ → List (List Env) → (exit : List (List Env) → t) → t
exec-brute-force n envll exit = exec-brute-force-p n  envll exit where
  exec-brute-force-p : {n : Level} {t : Set n} → ℕ → List (List Env) → (exit : List (List Env) → t) → t
  exec-brute-force-p zero envll exit = exit envll
  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))

model-check-deadlock : {n : Level} {t : Set n} → List (List Env) → (exit : List (List Env) → t) → t
model-check-deadlock envll exit = test11 [] envll exit where
  test11 : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t
  test11 f [] exit = exit f
  test11 f ([] ∷ bs) exit = test11 f bs exit
  test11 f (s@(x ∷ []) ∷ bs) exit = test11 (f ++ (s ∷ [])) bs exit
  test11 f (s@(x ∷ x1 ∷ []) ∷ bs) exit = test11 (f ++ (s ∷ [])) bs exit
  test11 f ((x ∷ x1 ∷ x2 ∷ xs) ∷ bs) exit = {!!}



data _===_ {n} {A : Set n} :  List A -> List A -> Set n where
          reflection  : {x : List A} -> x === x
          reflection1  : {x : List A} ->  (x === x)

testhoge : Code → Code → ℕ
testhoge C_putdown_rfork C_putdown_rfork = {!!}
testhoge C_putdown_lfork C_putdown_lfork = {!!}
testhoge C_pickup_rfork C_pickup_rfork = {!!}
testhoge C_pickup_lfork C_pickup_lfork = {!!}
testhoge _ _ = {!!}


test-step-c : (List Env)
test-step-c = brute-force-search record {
  table = 0 ∷ 0 ∷ 0 ∷ []
  ; ph = record
           { pid = 1
           ; left-hand = false
           ; right-hand = false
           ; next-code = C_pickup_rfork
           } ∷ record
                 { pid = 2
                 ; left-hand = false
                 ; right-hand = false
                 ; next-code = C_pickup_rfork
           } ∷ record
                 { pid = 3
                 ; left-hand = false
                 ; right-hand = false
                 ; next-code = C_pickup_rfork
                 }  ∷ []
  } (λ e2 →  e2)

test-step-c2 : List (List Env)
test-step-c2 = init-brute-force (record {
  table = 0 ∷ 0 ∷ 0 ∷ []
  ; ph = record
           { pid = 1
           ; left-hand = false
           ; right-hand = false
           ; next-code = C_thinking
           } ∷ record
                 { pid = 2
                 ; left-hand = false
                 ; right-hand = false
                 ; next-code = C_pickup_rfork
           } ∷ record
                 { pid = 3
                 ; left-hand = false
                 ; right-hand = false
                 ; next-code = C_pickup_rfork
                 }  ∷ []
  } ∷ []) (λ e0 → exec-brute-force 2 e0 (λ e2 → e2))

-- 以下メモ

-- eathingの状態はいらない Done
-- tableはℕのList Done
-- いきなりsearchしないで実行結果を持つ感じに
-- stubを使うとCodeの引数がスマートになるのでやる

-- 実行結果をListでもっているので，stepをじっこうしても変化がなかった場合をdeadlockとして検出したい
-- 東恩納先輩とおなじように，waitに入れて評価する

-- 余裕があったらassertにLTLの話をいれる

-- loop execution

-- concurrnt execution

-- state db ( binary tree of processes )

-- depth first ececution

-- verify temporal logic poroerries