--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/DPP/ModelChecking.agda	Sun May 01 15:17:52 2022 +0900
@@ -0,0 +1,278 @@
+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_set : Code
+   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 : ℕ
+    eating : Bool
+    right-hand : Bool
+    left-hand : Bool
+    next-code : Code
+open Phi
+
+record Env : Set where
+  field
+    table : List Bool
+    ph : List Phi
+    len : ℕ
+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 = [] ; len = n}) 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 = true ∷ (table env)
+    ; ph = record {pid = redu ; eating = false ; 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 eating p
+      ... | true = set-state redu origin state (f ++ (p ∷ [])) ps env envl exit -- 変更対象ではないので奥を対象にする
+      ... | false with s
+      ... | true = set-state redu origin ss (f ++ (record p{eating = s ; next-code = C_pickup_rfork} ∷ [])) ps env envl exit -- 変更対象なので変更して奥に進む
+      ... | false = set-state redu origin ss (f ++ (record p{eating = s} ∷ [])) 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 Bool) → Phi → Env → (Env → t) → t
+  pickup-rfork-p zero f [] p env exit = exit env
+  pickup-rfork-p zero f (true ∷ ts) p env exit = exit record env{ph = ((ph env) ++ (record p{right-hand = true ; next-code = C_pickup_lfork} ∷ [])); table = (f ++ (false ∷ ts))} -- 取得可能なので変更する envの後ろにappendする感じ
+  pickup-rfork-p zero f (false ∷ 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 Bool) → Phi → Env → (Env → t) → t
+  pickup-lfork-p zero f [] p env exit with table env
+  ... | [] = exit env
+  ... | true ∷ ts = exit record env{ph = ((ph env) ++ (record p{left-hand = true ; next-code = C_eating} ∷ [])); table = (false ∷ ts)} -- 取得可能なので変更する envの後ろにappendする感じ
+  ... | false ∷ ts = exit record env{ph = ((ph env) ++ p ∷ [])} -- 取得不可能なので変更せず終了する
+  pickup-lfork-p zero f (true ∷ ts) p env exit = exit record env{ph = ((ph env) ++ (record p{left-hand = true ; next-code = C_eating} ∷ [])); table = (f ++ (false ∷ ts))} -- 取得可能なので変更する envの後ろにappendする感じ
+  pickup-lfork-p zero f (false ∷ 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 Bool) → 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 = (true ∷ 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 ++ (true ∷ 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 Bool) → 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 ++ (true ∷ 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
+-- code_table-test C_set  = ?
+
+step-c : {n : Level} {t : Set n} → Env → (exit : Env → t) → t
+step-c env exit = step-p (len 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 (len 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)
+
+{-# TERMINATING #-}
+exec-brute-force : {n : Level} {t : Set n} → List Env → (exit : List (List Env) → t) → t
+exec-brute-force envl exit = exec-brute-force-p [] (envl ∷ []) exit where
+  exec-brute-force-p : {n : Level} {t : Set n} → (f b : List (List Env)) → (exit : List (List Env) → t) → t
+  exec-brute-force-p f [] exit = exit f
+  exec-brute-force-p f l@([] ∷ bs) exit = exit l
+  exec-brute-force-p f ((x ∷ b) ∷ bs) exit = step-c x (λ e → exec-brute-force-p (f ++(e ∷ x ∷ b) ∷ [])) bs exit
+
+
+test-step-c : List (List Env)
+test-step-c = brute-force-search record {
+  table = true ∷ true ∷ true ∷ []
+  ; ph = record
+           { pid = 1
+           ; eating = false
+           ; left-hand = false
+           ; right-hand = false
+           ; next-code = C_thinking
+           } ∷ record
+                 { pid = 2
+                 ; eating = false
+                 ; left-hand = false
+                 ; right-hand = false
+                 ; next-code = C_thinking
+           } ∷ record
+                 { pid = 3
+                 ; eating = true
+                 ; left-hand = false
+                 ; right-hand = false
+                 ; next-code = C_pickup_rfork
+                 }  ∷ []
+  ; len = 3
+  } (λ e0 → exec-brute-force e0 (λ e1 → e1))
+
+{-
+with table env
+... | [] = exit env
+... | true ∷ tl = exit record env{ph = record ph{right-hand = true}} --forkが存在しているのでOK
+... | false ∷ tl = exit env --forkが存在しないので待機
+pickup-rfork-c (suc ind) ph env exit = {!!}
+-}
+
+
+-- loop execution
+
+-- concurrnt execution
+
+-- state db ( binary tree of processes )
+
+-- depth first ececution
+
+-- verify temporal logic poroerries
+
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/DPP/logic.agda	Sun May 01 15:17:52 2022 +0900
@@ -0,0 +1,91 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary.PropositionalEquality
+
+open import Data.Empty
+open import Data.Nat hiding (_⊔_)
+
+
+data Bool : Set where
+    true : Bool
+    false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   constructor ⟪_,_⟫
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
+
+_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
+_⇔_ A B =  ( A → B ) ∧ ( B → A )
+
+contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
+contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
+
+double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
+double-neg A notnot = notnot A
+
+double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
+dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
+dont-orb {A} {B} (case1 a) ¬B = a
+
+
+infixr  130 _∧_
+infixr  140 _∨_
+infixr  150 _⇔_
+
+_/\_ : Bool → Bool → Bool 
+true /\ true = true
+_ /\ _ = false
+
+_<B?_ : ℕ → ℕ → Bool
+ℕ.zero <B? x = true
+ℕ.suc x <B? ℕ.zero = false
+ℕ.suc x <B? ℕ.suc xx = x <B? xx
+
+-- _<BT_ : ℕ → ℕ → Set
+-- ℕ.zero <BT ℕ.zero = ⊤
+-- ℕ.zero <BT ℕ.suc b = ⊤
+-- ℕ.suc a <BT ℕ.zero = ⊥
+-- ℕ.suc a <BT ℕ.suc b = a <BT b
+
+
+_≟B_ : Decidable {A = Bool} _≡_
+true  ≟B true  = yes refl
+false ≟B false = yes refl
+true  ≟B false = no λ()
+false ≟B true  = no λ()
+
+_\/_ : Bool → Bool → Bool 
+false \/ false = false
+_ \/ _ = true
+
+not_ : Bool → Bool 
+not true = false
+not false = true 
+
+_<=>_ : Bool → Bool → Bool  
+true <=> true = true
+false <=> false = true
+_ <=> _ = false
+
+infixr  130 _\/_
+infixr  140 _/\_

Binary file Paper/soto-sigos.dvi has changed

Binary file Paper/soto-sigos.pdf has changed

Binary file Paper/soto-sigos.synctex.gz has changed

--- a/Paper/tex/cbc.tex	Sun Apr 24 23:13:44 2022 +0900
+++ b/Paper/tex/cbc.tex	Sun May 01 15:17:52 2022 +0900
@@ -10,19 +10,12 @@
 CodeGear の入力となる DataGear を Input DataGear と呼び、
 出力は Output DataGear と呼ぶ。
 
-CodeGear はプログラムの処理そのもので、図 \ref{fig:cgdg}で示しているように任意の数の
+CodeGear はプログラムの処理そのもので、図 で示しているように任意の数の
 Input DataGear を参照し、処理が完了すると任意の数の Output DataGear に書き込む。
 
 CodeGear 間の移動は継続を用いて行われる。継続は関数呼び出しとは異なり、呼び出し
 た後に元のコードに戻らず、次の CodeGear へ継続を行う。
 これは、関数型プログラミングでは末尾関数呼び出しを行うことに相当する。
-\begin{figure}[htpb]
- \begin{center}
-  \scalebox{0.3}{\includegraphics{fig/cgdg.pdf}}
- \end{center}
- \caption{CodeGear と DataGear}
- \label{fig:cgdg}
-\end{figure}
 
 また、プログラムの記述する際は、ノーマルレベルの計算の他に、メモリ管理、スレッド管理、資源管理等を記述しなければならない処理が存在する。
 これらの計算はノーマルレベルの計算と区別してメタ計算と呼ぶ。