Skip to content

chore: reorganize Cslib/Computability/Automata/ #196

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
fmontesi merged 1 commit into from
Dec 4, 2025
Merged

chore: reorganize Cslib/Computability/Automata/ #196

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
30 changes: 15 additions & 15 deletions Cslib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
0 Cslib/Computability/Automata/Acceptor.lean → ...tability/Automata/Acceptors/Acceptor.lean
View file
Open in desktop
File renamed without changes.
0 ...Computability/Automata/OmegaAcceptor.lean → ...ity/Automata/Acceptors/OmegaAcceptor.lean
View file
Open in desktop
File renamed without changes.
4 changes: 2 additions & 2 deletions Cslib/Computability/Automata/DA.lean → Cslib/Computability/Automata/DA/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion Cslib/Computability/Automata/DABuchi.lean → Cslib/Computability/Automata/DA/Buchi.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
-/
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Computability/Automata/DAProd.lean → Cslib/Computability/Automata/DA/Prod.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/

Expand Down
4 changes: 2 additions & 2 deletions Cslib/Computability/Automata/DAToNA.lean → Cslib/Computability/Automata/DA/ToNA.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Computability/Automata/EpsilonNA.lean → ...mputability/Automata/EpsilonNA/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/

Expand Down
2 changes: 1 addition & 1 deletion ...Computability/Automata/EpsilonNAToNA.lean → ...omputability/Automata/EpsilonNA/ToNA.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 -/

Expand Down
4 changes: 2 additions & 2 deletions Cslib/Computability/Automata/NA.lean → Cslib/Computability/Automata/NA/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion .../Computability/Automata/NABuchiEquiv.lean → ...Computability/Automata/NA/BuchiEquiv.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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). -/

Expand Down
4 changes: 2 additions & 2 deletions .../Computability/Automata/NABuchiInter.lean → ...Computability/Automata/NA/BuchiInter.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Computability/Automata/NAHist.lean → Cslib/Computability/Automata/NA/Hist.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
2 changes: 1 addition & 1 deletion Cslib/Computability/Automata/NAProd.lean → Cslib/Computability/Automata/NA/Prod.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/

Expand Down
2 changes: 1 addition & 1 deletion Cslib/Computability/Automata/NASum.lean → Cslib/Computability/Automata/NA/Sum.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/

Expand Down
4 changes: 2 additions & 2 deletions Cslib/Computability/Automata/NAToDA.lean → Cslib/Computability/Automata/NA/ToDA.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Cslib/Computability/Languages/ExampleEventuallyZero.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions Cslib/Computability/Languages/OmegaRegularLanguage.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions Cslib/Computability/Languages/RegularLanguage.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion CslibTests/DFA.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down