From bf40b4487a915ad246b4f5c5dd5704a2a9db2233 Mon Sep 17 00:00:00 2001 From: Ching-Tsun Chou Date: Tue, 2 Dec 2025 13:27:49 -0800 Subject: [PATCH] chore: reorganize Cslib/Computability/Automata/ --- Cslib.lean | 30 +++++++++---------- .../Automata/{ => Acceptors}/Acceptor.lean | 0 .../{ => Acceptors}/OmegaAcceptor.lean | 0 .../Automata/{DA.lean => DA/Basic.lean} | 4 +-- .../Automata/{DABuchi.lean => DA/Buchi.lean} | 2 +- .../Automata/{DAProd.lean => DA/Prod.lean} | 2 +- .../Automata/{DAToNA.lean => DA/ToNA.lean} | 4 +-- .../{EpsilonNA.lean => EpsilonNA/Basic.lean} | 2 +- .../ToNA.lean} | 2 +- .../Automata/{NA.lean => NA/Basic.lean} | 4 +-- .../{NABuchiEquiv.lean => NA/BuchiEquiv.lean} | 2 +- .../{NABuchiInter.lean => NA/BuchiInter.lean} | 4 +-- .../Automata/{NAHist.lean => NA/Hist.lean} | 2 +- .../Automata/{NAProd.lean => NA/Prod.lean} | 2 +- .../Automata/{NASum.lean => NA/Sum.lean} | 2 +- .../Automata/{NAToDA.lean => NA/ToDA.lean} | 4 +-- .../Languages/ExampleEventuallyZero.lean | 2 +- .../Languages/OmegaRegularLanguage.lean | 8 ++--- .../Languages/RegularLanguage.lean | 6 ++-- CslibTests/DFA.lean | 2 +- 20 files changed, 42 insertions(+), 42 deletions(-) rename Cslib/Computability/Automata/{ => Acceptors}/Acceptor.lean (100%) rename Cslib/Computability/Automata/{ => Acceptors}/OmegaAcceptor.lean (100%) rename Cslib/Computability/Automata/{DA.lean => DA/Basic.lean} (96%) rename Cslib/Computability/Automata/{DABuchi.lean => DA/Buchi.lean} (93%) rename Cslib/Computability/Automata/{DAProd.lean => DA/Prod.lean} (95%) rename Cslib/Computability/Automata/{DAToNA.lean => DA/ToNA.lean} (95%) rename Cslib/Computability/Automata/{EpsilonNA.lean => EpsilonNA/Basic.lean} (97%) rename Cslib/Computability/Automata/{EpsilonNAToNA.lean => EpsilonNA/ToNA.lean} (96%) rename Cslib/Computability/Automata/{NA.lean => NA/Basic.lean} (97%) rename Cslib/Computability/Automata/{NABuchiEquiv.lean => NA/BuchiEquiv.lean} (97%) rename Cslib/Computability/Automata/{NABuchiInter.lean => NA/BuchiInter.lean} (98%) rename Cslib/Computability/Automata/{NAHist.lean => NA/Hist.lean} (98%) rename Cslib/Computability/Automata/{NAProd.lean => NA/Prod.lean} (96%) rename Cslib/Computability/Automata/{NASum.lean => NA/Sum.lean} (98%) rename Cslib/Computability/Automata/{NAToDA.lean => NA/ToDA.lean} (93%) diff --git a/Cslib.lean b/Cslib.lean index 2a327dfd..17891097 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -1,18 +1,18 @@ -import Cslib.Computability.Automata.Acceptor -import Cslib.Computability.Automata.DA -import Cslib.Computability.Automata.DABuchi -import Cslib.Computability.Automata.DAProd -import Cslib.Computability.Automata.DAToNA -import Cslib.Computability.Automata.EpsilonNA -import Cslib.Computability.Automata.EpsilonNAToNA -import Cslib.Computability.Automata.NA -import Cslib.Computability.Automata.NABuchiEquiv -import Cslib.Computability.Automata.NABuchiInter -import Cslib.Computability.Automata.NAHist -import Cslib.Computability.Automata.NAProd -import Cslib.Computability.Automata.NASum -import Cslib.Computability.Automata.NAToDA -import Cslib.Computability.Automata.OmegaAcceptor +import Cslib.Computability.Automata.Acceptors.Acceptor +import Cslib.Computability.Automata.Acceptors.OmegaAcceptor +import Cslib.Computability.Automata.DA.Basic +import Cslib.Computability.Automata.DA.Buchi +import Cslib.Computability.Automata.DA.Prod +import Cslib.Computability.Automata.DA.ToNA +import Cslib.Computability.Automata.EpsilonNA.Basic +import Cslib.Computability.Automata.EpsilonNA.ToNA +import Cslib.Computability.Automata.NA.Basic +import Cslib.Computability.Automata.NA.BuchiEquiv +import Cslib.Computability.Automata.NA.BuchiInter +import Cslib.Computability.Automata.NA.Hist +import Cslib.Computability.Automata.NA.Prod +import Cslib.Computability.Automata.NA.Sum +import Cslib.Computability.Automata.NA.ToDA import Cslib.Computability.Languages.ExampleEventuallyZero import Cslib.Computability.Languages.Language import Cslib.Computability.Languages.OmegaLanguage diff --git a/Cslib/Computability/Automata/Acceptor.lean b/Cslib/Computability/Automata/Acceptors/Acceptor.lean similarity index 100% rename from Cslib/Computability/Automata/Acceptor.lean rename to Cslib/Computability/Automata/Acceptors/Acceptor.lean diff --git a/Cslib/Computability/Automata/OmegaAcceptor.lean b/Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean similarity index 100% rename from Cslib/Computability/Automata/OmegaAcceptor.lean rename to Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA/Basic.lean similarity index 96% rename from Cslib/Computability/Automata/DA.lean rename to Cslib/Computability/Automata/DA/Basic.lean index 12fb3a58..e14cfc0c 100644 --- a/Cslib/Computability/Automata/DA.lean +++ b/Cslib/Computability/Automata/DA/Basic.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi, Ching-Tsun Chou -/ -import Cslib.Computability.Automata.Acceptor -import Cslib.Computability.Automata.OmegaAcceptor +import Cslib.Computability.Automata.Acceptors.Acceptor +import Cslib.Computability.Automata.Acceptors.OmegaAcceptor import Cslib.Foundations.Data.OmegaSequence.InfOcc import Cslib.Foundations.Semantics.LTS.FLTS diff --git a/Cslib/Computability/Automata/DABuchi.lean b/Cslib/Computability/Automata/DA/Buchi.lean similarity index 93% rename from Cslib/Computability/Automata/DABuchi.lean rename to Cslib/Computability/Automata/DA/Buchi.lean index 6fecf462..ea545274 100644 --- a/Cslib/Computability/Automata/DABuchi.lean +++ b/Cslib/Computability/Automata/DA/Buchi.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.DA +import Cslib.Computability.Automata.DA.Basic /-! # Deterministic Buchi automata. -/ diff --git a/Cslib/Computability/Automata/DAProd.lean b/Cslib/Computability/Automata/DA/Prod.lean similarity index 95% rename from Cslib/Computability/Automata/DAProd.lean rename to Cslib/Computability/Automata/DA/Prod.lean index bcb547a2..4e9b9c88 100644 --- a/Cslib/Computability/Automata/DAProd.lean +++ b/Cslib/Computability/Automata/DA/Prod.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.DA +import Cslib.Computability.Automata.DA.Basic /-! # Product of deterministic automata. -/ diff --git a/Cslib/Computability/Automata/DAToNA.lean b/Cslib/Computability/Automata/DA/ToNA.lean similarity index 95% rename from Cslib/Computability/Automata/DAToNA.lean rename to Cslib/Computability/Automata/DA/ToNA.lean index 9aa96766..ce7dd563 100644 --- a/Cslib/Computability/Automata/DAToNA.lean +++ b/Cslib/Computability/Automata/DA/ToNA.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Computability.Automata.DA -import Cslib.Computability.Automata.NA +import Cslib.Computability.Automata.DA.Basic +import Cslib.Computability.Automata.NA.Basic import Cslib.Foundations.Semantics.LTS.FLTSToLTS /-! # Translation of Deterministic Automata into Nonodeterministic Automata. diff --git a/Cslib/Computability/Automata/EpsilonNA.lean b/Cslib/Computability/Automata/EpsilonNA/Basic.lean similarity index 97% rename from Cslib/Computability/Automata/EpsilonNA.lean rename to Cslib/Computability/Automata/EpsilonNA/Basic.lean index a13508ae..6083e1f3 100644 --- a/Cslib/Computability/Automata/EpsilonNA.lean +++ b/Cslib/Computability/Automata/EpsilonNA/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi, Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA +import Cslib.Computability.Automata.NA.Basic /-! # Nondeterministic automata with ε-transitions. -/ diff --git a/Cslib/Computability/Automata/EpsilonNAToNA.lean b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean similarity index 96% rename from Cslib/Computability/Automata/EpsilonNAToNA.lean rename to Cslib/Computability/Automata/EpsilonNA/ToNA.lean index 3941453a..5ed7ee05 100644 --- a/Cslib/Computability/Automata/EpsilonNAToNA.lean +++ b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Computability.Automata.EpsilonNA +import Cslib.Computability.Automata.EpsilonNA.Basic /-! # Translation of εNA into NA -/ diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA/Basic.lean similarity index 97% rename from Cslib/Computability/Automata/NA.lean rename to Cslib/Computability/Automata/NA/Basic.lean index 24159e24..bbdee77b 100644 --- a/Cslib/Computability/Automata/NA.lean +++ b/Cslib/Computability/Automata/NA/Basic.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi, Ching-Tsun Chou, Chris Henson. -/ -import Cslib.Computability.Automata.Acceptor -import Cslib.Computability.Automata.OmegaAcceptor +import Cslib.Computability.Automata.Acceptors.Acceptor +import Cslib.Computability.Automata.Acceptors.OmegaAcceptor import Cslib.Foundations.Data.OmegaSequence.InfOcc import Cslib.Foundations.Semantics.LTS.Basic diff --git a/Cslib/Computability/Automata/NABuchiEquiv.lean b/Cslib/Computability/Automata/NA/BuchiEquiv.lean similarity index 97% rename from Cslib/Computability/Automata/NABuchiEquiv.lean rename to Cslib/Computability/Automata/NA/BuchiEquiv.lean index 5cd29f7e..470b9d00 100644 --- a/Cslib/Computability/Automata/NABuchiEquiv.lean +++ b/Cslib/Computability/Automata/NA/BuchiEquiv.lean @@ -4,7 +4,7 @@ Relexsed under Apache 2.0 license xs described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA +import Cslib.Computability.Automata.NA.Basic /-! # Equivalence of nondeterministic Buchi automata (NBAs). -/ diff --git a/Cslib/Computability/Automata/NABuchiInter.lean b/Cslib/Computability/Automata/NA/BuchiInter.lean similarity index 98% rename from Cslib/Computability/Automata/NABuchiInter.lean rename to Cslib/Computability/Automata/NA/BuchiInter.lean index 8b8a9fc3..5e37f5f3 100644 --- a/Cslib/Computability/Automata/NABuchiInter.lean +++ b/Cslib/Computability/Automata/NA/BuchiInter.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NAHist -import Cslib.Computability.Automata.NAProd +import Cslib.Computability.Automata.NA.Hist +import Cslib.Computability.Automata.NA.Prod import Cslib.Foundations.Data.OmegaSequence.Temporal /-! # Intersection of nondeterministic Buchi automata. diff --git a/Cslib/Computability/Automata/NAHist.lean b/Cslib/Computability/Automata/NA/Hist.lean similarity index 98% rename from Cslib/Computability/Automata/NAHist.lean rename to Cslib/Computability/Automata/NA/Hist.lean index 48784923..8b9acc99 100644 --- a/Cslib/Computability/Automata/NAHist.lean +++ b/Cslib/Computability/Automata/NA/Hist.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA +import Cslib.Computability.Automata.NA.Basic /-! # Adding a history states to a nondeterministic automaton. diff --git a/Cslib/Computability/Automata/NAProd.lean b/Cslib/Computability/Automata/NA/Prod.lean similarity index 96% rename from Cslib/Computability/Automata/NAProd.lean rename to Cslib/Computability/Automata/NA/Prod.lean index 338a6925..37ace662 100644 --- a/Cslib/Computability/Automata/NAProd.lean +++ b/Cslib/Computability/Automata/NA/Prod.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA +import Cslib.Computability.Automata.NA.Basic /-! # Product of nondeterministic automata. -/ diff --git a/Cslib/Computability/Automata/NASum.lean b/Cslib/Computability/Automata/NA/Sum.lean similarity index 98% rename from Cslib/Computability/Automata/NASum.lean rename to Cslib/Computability/Automata/NA/Sum.lean index 05bbb68f..8a248976 100644 --- a/Cslib/Computability/Automata/NASum.lean +++ b/Cslib/Computability/Automata/NA/Sum.lean @@ -4,7 +4,7 @@ Relexsed under Apache 2.0 license xs described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA +import Cslib.Computability.Automata.NA.Basic /-! # Sum of nondeterministic automata. -/ diff --git a/Cslib/Computability/Automata/NAToDA.lean b/Cslib/Computability/Automata/NA/ToDA.lean similarity index 93% rename from Cslib/Computability/Automata/NAToDA.lean rename to Cslib/Computability/Automata/NA/ToDA.lean index c9ad4e0f..9b76130a 100644 --- a/Cslib/Computability/Automata/NAToDA.lean +++ b/Cslib/Computability/Automata/NA/ToDA.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Computability.Automata.DA -import Cslib.Computability.Automata.NA +import Cslib.Computability.Automata.DA.Basic +import Cslib.Computability.Automata.NA.Basic import Cslib.Foundations.Semantics.LTS.LTSToFLTS /-! # Translation of Nondeterministic Automata for finite strings into Deterministic Automata diff --git a/Cslib/Computability/Languages/ExampleEventuallyZero.lean b/Cslib/Computability/Languages/ExampleEventuallyZero.lean index bc928015..fef96835 100644 --- a/Cslib/Computability/Languages/ExampleEventuallyZero.lean +++ b/Cslib/Computability/Languages/ExampleEventuallyZero.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.NA +import Cslib.Computability.Automata.NA.Basic /-! # An ω-regular language that is not accepted by any deterministic Buchi automaton diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean index 8e0776ff..a5e9723e 100644 --- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean +++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.DABuchi -import Cslib.Computability.Automata.NABuchiEquiv -import Cslib.Computability.Automata.NABuchiInter -import Cslib.Computability.Automata.NASum +import Cslib.Computability.Automata.DA.Buchi +import Cslib.Computability.Automata.NA.BuchiEquiv +import Cslib.Computability.Automata.NA.BuchiInter +import Cslib.Computability.Automata.NA.Sum import Cslib.Computability.Languages.ExampleEventuallyZero import Cslib.Computability.Languages.RegularLanguage import Mathlib.Data.Finite.Sigma diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean index 29668b5c..5f7617dc 100644 --- a/Cslib/Computability/Languages/RegularLanguage.lean +++ b/Cslib/Computability/Languages/RegularLanguage.lean @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Ching-Tsun Chou -/ -import Cslib.Computability.Automata.DAProd -import Cslib.Computability.Automata.DAToNA -import Cslib.Computability.Automata.NAToDA +import Cslib.Computability.Automata.DA.Prod +import Cslib.Computability.Automata.DA.ToNA +import Cslib.Computability.Automata.NA.ToDA import Mathlib.Computability.DFA import Mathlib.Data.Set.Card import Mathlib.Tactic.Common diff --git a/CslibTests/DFA.lean b/CslibTests/DFA.lean index e0159fcd..f78e47c0 100644 --- a/CslibTests/DFA.lean +++ b/CslibTests/DFA.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Computability.Automata.DA +import Cslib.Computability.Automata.DA.Basic namespace CslibTests