Mercurial > hg > Members > kono > Proof > automaton

changeset 269:52ed73a116d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Nov 2021 09:58:19 +0900
parents 8006cbd87b20
children dd98e7e5d4a5
files automaton-in-agda/src/nfa.agda automaton-in-agda/src/regular-concat.agda
diffstat 2 files changed, 21 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/nfa.agda	Thu Nov 25 12:19:36 2021 +0900
+++ b/automaton-in-agda/src/nfa.agda	Fri Nov 26 09:58:19 2021 +0900
@@ -71,7 +71,24 @@
     to-list (λ q →  sb q ) ∷
     Ntrace M exists to-list (λ q →  exists ( λ qn → (sb qn /\ ( Nδ M qn i q )  ))) t
 
-
+{-# TERMINATING #-}
+NtraceDepth : { Q : Set } { Σ : Set  } 
+    → NAutomaton Q  Σ
+    → (Nstart : Q → Bool) → List Q  → List  Σ → List (List ( Σ ∧ Q ))
+NtraceDepth {Q} {Σ} M sb all is = ndepth all sb is [] where
+    ndepth : List Q → (q : Q → Bool ) → List Σ  →  List (List ( Σ ∧ Q )  ) →  List (List ( Σ ∧ Q )  )
+    ndepth1 : Q → List Q →  List Σ  → List ( Σ ∧ Q )  →  List ( List ( Σ ∧ Q )) →  List ( List ( Σ ∧ Q ))
+    ndepth1 q [] is t t1 = t ∷ t1
+    ndepth1 q _ [] t t1 = t1
+    ndepth1 q (x ∷ qns) (i ∷ []) t t1 with Nend M x
+    ... | true = ndepth1 q qns (i ∷ []) (⟪ i , x ⟫ ∷ t) t1
+    ... | false = t1
+    ndepth1 q (x ∷ qns) (i ∷ is) t t1 =  ndepth all (Nδ M x i) is (ndepth1 q qns (i ∷ is) (⟪ i , q ⟫ ∷ t) t1 )
+    ndepth [] sb is t = t
+    ndepth (q ∷ qs) sb is t with sb q 
+    ... | true  = ndepth qs sb is (ndepth1 q all is [] t )
+    ... | false = ndepth qs sb is t
+    
 transition3 : States1  → In2  → States1 → Bool
 transition3 sr i0 sr = true
 transition3 sr i1 ss = true
@@ -103,6 +120,8 @@
 t-1 : List ( List States1 )
 t-1 = Ntrace am2 existsS1 to-listS1 start1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
 t-2 = Ntrace am2 existsS1 to-listS1 start1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
+t-3 = NtraceDepth am2 start1 LStates1 ( i1  ∷ i1  ∷ i1  ∷ [] ) 
+t-4 = NtraceDepth am2 start1 LStates1 ( i0  ∷ i1  ∷ i0  ∷ [] ) 
 
 transition4 : States1  → In2  → States1 → Bool
 transition4 sr i0 sr = true
--- a/automaton-in-agda/src/regular-concat.agda	Thu Nov 25 12:19:36 2021 +0900
+++ b/automaton-in-agda/src/regular-concat.agda	Fri Nov 26 09:58:19 2021 +0900
@@ -23,6 +23,7 @@
 open Automaton
 open FiniteSet
 
+open RegularLanguage
 
 Concat-NFA :  {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ 
 Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend }