Skip to content

Commit a2d2682

Browse files
ctchouctchou
committed
chore: reorganize Cslib/Computability/Automata/
1 parent 2c4d800 commit a2d2682

File tree

19 files changed

+41
-41
lines changed

19 files changed

+41
-41
lines changed

‎Cslib.lean‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,18 @@
1-
import Cslib.Computability.Automata.Acceptor
2-
import Cslib.Computability.Automata.DA
3-
import Cslib.Computability.Automata.DABuchi
4-
import Cslib.Computability.Automata.DAProd
5-
import Cslib.Computability.Automata.DAToNA
6-
import Cslib.Computability.Automata.EpsilonNA
7-
import Cslib.Computability.Automata.EpsilonNAToNA
8-
import Cslib.Computability.Automata.NA
9-
import Cslib.Computability.Automata.NABuchiEquiv
10-
import Cslib.Computability.Automata.NABuchiInter
11-
import Cslib.Computability.Automata.NAHist
12-
import Cslib.Computability.Automata.NAProd
13-
import Cslib.Computability.Automata.NASum
14-
import Cslib.Computability.Automata.NAToDA
15-
import Cslib.Computability.Automata.OmegaAcceptor
1+
import Cslib.Computability.Automata.Acceptors.Acceptor
2+
import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
3+
import Cslib.Computability.Automata.DA.Basic
4+
import Cslib.Computability.Automata.DA.Buchi
5+
import Cslib.Computability.Automata.DA.Prod
6+
import Cslib.Computability.Automata.DA.ToNA
7+
import Cslib.Computability.Automata.EpsilonNA.Basic
8+
import Cslib.Computability.Automata.EpsilonNA.ToNA
9+
import Cslib.Computability.Automata.NA.Basic
10+
import Cslib.Computability.Automata.NA.BuchiEquiv
11+
import Cslib.Computability.Automata.NA.BuchiInter
12+
import Cslib.Computability.Automata.NA.Hist
13+
import Cslib.Computability.Automata.NA.Prod
14+
import Cslib.Computability.Automata.NA.Sum
15+
import Cslib.Computability.Automata.NA.ToDA
1616
import Cslib.Computability.Languages.ExampleEventuallyZero
1717
import Cslib.Computability.Languages.Language
1818
import Cslib.Computability.Languages.OmegaLanguage

Cslib/Computability/Automata/Acceptor.lean renamed to Cslib/Computability/Automata/Acceptors/Acceptor.lean

File renamed without changes.

Cslib/Computability/Automata/OmegaAcceptor.lean renamed to Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean

File renamed without changes.

Cslib/Computability/Automata/DA.lean renamed to Cslib/Computability/Automata/DA/Basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Fabrizio Montesi, Ching-Tsun Chou
55
-/
66

7-
import Cslib.Computability.Automata.Acceptor
8-
import Cslib.Computability.Automata.OmegaAcceptor
7+
import Cslib.Computability.Automata.Acceptors.Acceptor
8+
import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
99
import Cslib.Foundations.Data.OmegaSequence.InfOcc
1010
import Cslib.Foundations.Semantics.LTS.FLTS
1111

Cslib/Computability/Automata/DABuchi.lean renamed to Cslib/Computability/Automata/DA/Buchi.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Ching-Tsun Chou
55
-/
66

7-
import Cslib.Computability.Automata.DA
7+
import Cslib.Computability.Automata.DA.Basic
88

99
/-! # Deterministic Buchi automata.
1010
-/

Cslib/Computability/Automata/DAProd.lean renamed to Cslib/Computability/Automata/DA/Prod.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Ching-Tsun Chou
55
-/
66

7-
import Cslib.Computability.Automata.DA
7+
import Cslib.Computability.Automata.DA.Basic
88

99
/-! # Product of deterministic automata. -/
1010

Cslib/Computability/Automata/DAToNA.lean renamed to Cslib/Computability/Automata/DA/ToNA.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Fabrizio Montesi
55
-/
66

7-
import Cslib.Computability.Automata.DA
8-
import Cslib.Computability.Automata.NA
7+
import Cslib.Computability.Automata.DA.Basic
8+
import Cslib.Computability.Automata.NA.Basic
99
import Cslib.Foundations.Semantics.LTS.FLTSToLTS
1010

1111
/-! # Translation of Deterministic Automata into Nonodeterministic Automata.

Cslib/Computability/Automata/EpsilonNA.lean renamed to Cslib/Computability/Automata/EpsilonNA/Basic.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Fabrizio Montesi, Ching-Tsun Chou
55
-/
66

7-
import Cslib.Computability.Automata.NA
7+
import Cslib.Computability.Automata.NA.Basic
88

99
/-! # Nondeterministic automata with ε-transitions. -/
1010

Cslib/Computability/Automata/EpsilonNAToNA.lean renamed to Cslib/Computability/Automata/EpsilonNA/ToNA.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Fabrizio Montesi
55
-/
66

7-
import Cslib.Computability.Automata.EpsilonNA
7+
import Cslib.Computability.Automata.EpsilonNA.Basic
88

99
/-! # Translation of εNA into NA -/
1010

Cslib/Computability/Automata/NA.lean renamed to Cslib/Computability/Automata/NA/Basic.lean

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Fabrizio Montesi, Ching-Tsun Chou, Chris Henson.
55
-/
66

7-
import Cslib.Computability.Automata.Acceptor
8-
import Cslib.Computability.Automata.OmegaAcceptor
7+
import Cslib.Computability.Automata.Acceptors.Acceptor
8+
import Cslib.Computability.Automata.Acceptors.OmegaAcceptor
99
import Cslib.Foundations.Data.OmegaSequence.InfOcc
1010
import Cslib.Foundations.Semantics.LTS.Basic
1111

0 commit comments

Comments
 (0)