diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,7 +1,13 @@
 # Turing Machine Model
-An implementation of Turing Machine and Automaton for language theory
+An implementation of Turing Machine and Automaton for Language Theory
 
-## Models
+  [![turingMachine](https://img.shields.io/badge/turingMachine-v1.0.0.0-blue.svg?style=plastic)](https://hackage.haskell.org/package/turingMachine)
+  [![Build Status](https://travis-ci.org/sanjorgek/turingMachine.svg?branch=master)](https://travis-ci.org/sanjorgek/turingMachine)
+  [![Code Climate](https://codeclimate.com/github/sanjorgek/turingMachine/badges/gpa.svg)](https://codeclimate.com/github/sanjorgek/turingMachine)
+  [![Issue Count](https://codeclimate.com/github/sanjorgek/turingMachine/badges/issue_count.svg)](https://codeclimate.com/github/sanjorgek/turingMachine)
+  [![CircleCI](https://circleci.com/gh/sanjorgek/turingMachine.svg?style=svg)](https://circleci.com/gh/sanjorgek/turingMachine)
+
+## Math Models
 ### Finite Automaton
 
 Finite State machine, with no memory.
@@ -15,3 +21,48 @@
 Stack memory machine with states
 
 ### Turing Machine
+
+## To Do
+
+- [ ] Finite Automaton
+  - [x] Delta
+    - [x] Deterministic
+    - [x] Non-deterministic
+    - [x] Lift deltas
+  - [x] Lambda
+    - [x] Lambda1
+    - [x] Lambda2
+    - [x] Lift lambda
+  - [ ] Recognizer
+    - [x] Deterministic def
+    - [x] Non-deterministic def
+    - [x] Check Word
+    - [ ] k-distinguishable states
+    - [ ] Distinguishable states
+    - [ ] Equivalent states
+    - [x] Equivalent recognizer
+    - [x] Non-deterministic to deterministic, and viceversa
+    - [x] Recheable recognizer
+    - [x] Distinguishable recognizer
+    - [x] Minimize recognizer
+    - [ ] Remove Ambiguity
+    - [x] Language cadinality
+  - [ ] Transductor
+    - [x] Moore
+    - [x] Mealy
+    - [x] translate
+    - [ ] Moore to Mealy, and viceversa   
+  - [ ] Recognizer with epsilon transitions
+    - [ ] def
+    - [ ] Recognizer with epsilon transitions to Recognizer without epsilon transitions
+- [ ] Stack Automaton
+  - [x] Lift delta
+  - [x] Deterministic stack automaton def
+  - [ ] Non-deterministic stack automaton def
+  - [ ] Non-deterministic to deterministic stack automaton
+  - [ ] Recognizer with epsilon transitions
+- [ ] Turing Machine
+  - [ ] Class def
+  - [ ] Tape def
+  - [ ] Delta def
+  - [ ] Accept word
diff --git a/src/Data/Delta.hs b/src/Data/Delta.hs
--- a/src/Data/Delta.hs
+++ b/src/Data/Delta.hs
@@ -1,9 +1,9 @@
-{-# OPTIONS_GHC -fno-warn-tabs #-}
+{-# OPTIONS_GHC -fno-warn-tabs      #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeOperators          #-}
 {-|
-Module      : Delta
-Description : Implementacion de un mapeo
+Module      : Data.Delta
+Description : Partial functions
 Copyright   : (c) Jorge Santiago Alvarez Cuadros, 2016
 License     : GPL-3
 Maintainer  : sanjorgek@ciencias.unam.mx
@@ -14,30 +14,185 @@
 -}
 module Data.Delta
 (
-	-- * Delta
+  -- * Delta
+  -- ** Generic
+	(:*>:)(..)
 	-- ** Deterministic
 	-- *** Constructor
-	(:->:)(..)
+	,(:->:)(..)
 	-- *** Functions
+  ,liftD
 	,nextD
 	-- ** Not deterministic
 	-- *** Constructor
-	,(:>-:)(..)
-	-- * Transductor
-	-- ** Constructor
-	,(:*>:)(..)
+	,(:-<:)(..)
+  -- *** Functions
+  ,liftND
+  ,nextND
+  -- ** Functions
+  ,liftL
+  ,nextTMaybe
+  ,nextSymbol
+  -- * Auxiliar functions
+  ,getFirstParam
+  ,getFirstParamSet
+	,getSecondParamD
+  ,getSecondParamND
+	,getSecondParamSetD
+  ,getSecondParamSetND
+  ,getStateDomain
+  ,getStateDomainSet
+  ,getStateRangeD
+  ,getStateRangeND
+  ,getStateRangeSetD
+  ,getStateRangeSetND
 ) where
-import Data.State
-import Control.Applicative
-import Data.Monoid
-import Data.Foldable
-import qualified Data.Map.Lazy as Map
+import qualified Data.Foldable   as Fold
+import           Data.Label
+import           Data.List
+import qualified Data.Map.Strict as Map
+import           Data.Maybe
+import qualified Data.Set        as Set
+import           Data.Sigma
 
-type (:->:) a p1 p2 = Map.Map (State a, p1) (State a, p2)
+{-|
+Map a tuple, a state and a param, to some output
+-}
+type (:*>:) a p o = Map.Map (Label a, p) o
 
-nextD :: (Ord p1, Ord a) => (:->:) a p1 p2 -> (State a, p1) -> State a
-nextD dt k = if Map.member k dt then fst (dt Map.! k) else QE 
+{-|
+Lift a generic delta/map from a 3-tuple list
+-}
+liftL :: (Ord a, Ord p) => [(a, p, o)] -> (:*>:) a p o
+liftL ds = let
+    (xs, ys, zs) = unzip3 ds
+  in Map.fromList $ zip (zip (fmap return xs) ys) zs
 
-type (:>-:) a p1 p2 = Map.Map (State a, p1) ([State a], p2)
+{-|
+Take a state and a param and maybe resolve some output
+-}
+nextTMaybe :: (Ord p1, Ord a) => (:*>:) a p1 o -> (Label a, p1) -> Maybe o
+nextTMaybe dt k = if Map.member k dt
+  then Just $ dt Map.! k
+  else Nothing
 
-type (:*>:) a p o = Map.Map (State a, p) o
+{-|
+For simple map with Chars range
+-}
+nextSymbol::(Ord p1, Ord a) => (:*>:) a p1 Symbol -> (Label a, p1) -> Symbol
+nextSymbol dt k = fromMaybe '\NUL' $ nextTMaybe dt k
+
+{-|
+Deterministic Delta
+
+Maps a tuple, a state and a param, to another tuple, a state and a param.
+-}
+type (:->:) a p1 p2 = (:*>:) a p1 (Label a, p2)
+
+{-|
+Lifts a deterministic delta from a 4-tuple list
+-}
+liftD::(Ord a, Ord p1) => [(a, p1, a, p2)] -> (:->:) a p1 p2
+liftD ds = let
+    (xs, ys, ws, zs) = unzip4 ds
+  in liftL $ zip3 xs ys $ zip (fmap return ws) zs
+
+{-|
+Next state function for deterministic delta
+-}
+nextD :: (Ord p1, Ord a) => (:->:) a p1 p2 -> (Label a, p1) -> Label a
+nextD dt k = maybe QE fst $ nextTMaybe dt k
+
+{-|
+Non-Deterministic Delta
+
+Maps a tuple, a state and a param, to a tuple, a state list and a param.
+-}
+type (:-<:) a p1 p2 = (:*>:) a p1 (Set.Set (Label a, p2))
+
+{-|
+Lifts a non-deterministic delta from a 4-tuple list
+-}
+liftND::(Ord a, Ord p1, Ord p2) => [(a, p1, [(a,p2)])] -> (:-<:) a p1 p2
+liftND ds = let
+		(xs, ys, wss) = unzip3 ds
+		f (x,y) = (return x, y)
+	in liftL $ zip3 xs ys $ fmap (Set.fromList . fmap f) wss
+
+{-|
+Next state function for non-deterministic delta
+-}
+nextND :: (Ord p1, Ord a) => (:-<:) a p1 p2 -> p2 -> (Label a, p1) -> Set.Set (Label a)
+nextND dt p k =  maybe (Set.singleton QE) (Set.map fst) $ nextTMaybe dt k
+
+{-|
+Gets all params at domain, for (:->:) and (:-<:)
+-}
+getFirstParam::(Eq b) => Map.Map (a, b) a1 -> [b]
+getFirstParam = nub . fmap snd . Map.keys
+
+{-|
+Gets all params at domain, for (:-<:) and (:-<:)
+-}
+getFirstParamSet::(Ord b) => Map.Map (a, b) a1 -> Set.Set b
+getFirstParamSet = Set.fromList . fmap snd . Map.keys
+
+{-|
+Gets all states at domain, for (:->:) and (:-<:)
+-}
+getStateDomain::(Eq a) => Map.Map (a, b) a1 -> [a]
+getStateDomain = nub . fmap fst . Map.keys
+
+{-|
+Gets all states at domain, for (:->:) and (:-<:)
+-}
+getStateDomainSet::(Ord a) => Map.Map (a, b) a1 -> Set.Set a
+getStateDomainSet = Set.fromList . fmap fst . Map.keys
+
+{-|
+Gets all params at range, for (:->:)
+-}
+getSecondParamD::(Eq p2) => (:->:) a p1 p2 -> [p2]
+getSecondParamD = nub . fmap snd . Map.elems
+
+{-|
+Gets all params at range, for (:->:)
+-}
+getSecondParamSetD::(Ord b) => Map.Map k (a, b) -> Set.Set b
+getSecondParamSetD = Set.fromList . fmap snd . Map.elems
+
+{-|
+Gets all params at range, for (:-<:)
+-}
+getSecondParamND::(Ord p2) => (:-<:) a p1 p2 -> [p2]
+getSecondParamND = foldr union [] . fmap (Set.toList . Set.map snd) . Map.elems
+
+{-|
+Gets all params at range, for (:-<:)
+-}
+getSecondParamSetND::(Ord p2) => (:-<:) a p1 p2 -> Set.Set p2
+getSecondParamSetND = Set.unions . fmap (Set.map snd) . Map.elems
+
+{-|
+Gets first param at range, for (:->:)
+-}
+getStateRangeD::(Eq a) => (:->:) a p1 p2 -> [Label a]
+getStateRangeD = nub . fmap fst . Map.elems
+
+{-|
+Gets first param at range, for (:->:)
+-}
+getStateRangeSetD::(Ord a) => (:->:) a p1 p2 -> Set.Set (Label a)
+getStateRangeSetD = Set.fromList . fmap fst . Map.elems
+
+{-|
+Gets state at range in a list, for (:-<:)
+-}
+getStateRangeND::(Ord a) => (:-<:) a p1 p2 -> [Label a]
+getStateRangeND = Set.toList . Set.unions . fmap (Set.map fst) . Map.elems
+
+{-|
+Gets state at range in a set, for (:-<:)
+-}
+getStateRangeSetND::(Ord a) => (:-<:) a p1 p2 -> Set.Set (Label a)
+getStateRangeSetND = Set.unions . fmap (Set.map fst)  . Map.elems
diff --git a/src/Data/Helper.hs b/src/Data/Helper.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Helper.hs
@@ -0,0 +1,39 @@
+{-# OPTIONS_HADDOCK show-extensions #-}
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-|
+Module      : Helper
+Description : Aux Functions
+Copyright   : (c) Jorge Santiago Alvarez Cuadros, 2016
+License     : GPL-3
+Maintainer  : sanjorgek@ciencias.unam.mx
+Stability   : experimental
+Portability : portable
+
+Auxiliar Functions
+-}
+module Data.Helper
+(
+  -- * Set
+  unionsFold
+  ,setGenericSize
+) where
+import qualified Data.Foldable as Fold
+import           Data.List
+import qualified Data.Map.Lazy as Map
+import qualified Data.Set      as Set
+
+{-|
+Union of set monad
+-}
+unionsFold:: (Ord a, Fold.Foldable t) => t (Set.Set a) -> Set.Set a
+unionsFold = Fold.foldr Set.union Set.empty
+
+{-|
+Size of a set, with large integers
+-}
+setGenericSize:: (Ord a) => Set.Set a -> Integer
+setGenericSize s = if Set.null s
+  then 0
+  else 1 + setGenericSize (Set.delete (Set.findMin s) s)
diff --git a/src/Data/Label.hs b/src/Data/Label.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Label.hs
@@ -0,0 +1,117 @@
+{-# OPTIONS_GHC -fno-warn-tabs      #-}
+{-# OPTIONS_HADDOCK show-extensions #-}
+{-|
+Module      : Data.State
+Description : Simple label state data
+Copyright   : (c) Jorge Santiago Alvarez Cuadros, 2016
+License     : GPL-3
+Maintainer  : sanjorgek@ciencias.unam.mx
+Stability   : experimental
+Portability : portable
+
+Simple Label-State function, have an isomorphism with Maybe but order are diferent
+-}
+module Data.Label
+(
+	-- * Data and type
+	Label(..)
+	,Final(..)
+	-- * Functions
+	,isError
+	,terminal
+  -- * Alias
+  ,SetLabel(..)
+  ,LabelSS(..)
+) where
+import           Control.Applicative
+import           Control.Monad
+import qualified Data.Foldable       as F
+import           Data.Monoid
+import qualified Data.Set            as Set
+
+{-|
+Machine states are only a label, maybe a letter
+-}
+data Label a =
+	-- |State constructor
+	Q a
+	-- |Error state
+	| QE deriving(Show, Eq)
+
+-- |Same as Maybe
+instance Functor Label where
+	fmap _ QE = QE
+	fmap f (Q q) = Q $ f q
+
+-- |Same as Maybe
+instance Applicative Label where
+	pure = Q
+	QE <*> _ = QE
+	(Q f) <*> q = fmap f q
+
+-- |Same as Maybe
+instance Monad Label where
+	return = pure
+	QE >>= _ = QE
+	(Q q) >>= f = f q
+
+{-|
+Holds
+
+>>> QE /= (toEnum:: State Int) . fromEnum QE
+True
+-}
+instance (Enum a) => Enum (Label a) where
+  toEnum = return . toEnum
+  fromEnum (Q x) = fromEnum x
+  fromEnum QE    = maxBound
+
+-- |In this differ with Maybe because this show a upper bounded order
+instance (Bounded a) => Bounded (Label a) where
+	minBound = Q minBound
+	maxBound = QE
+
+instance (Ord a) => Ord (Label a) where
+  compare QE QE       = EQ
+  compare _ QE        = LT
+  compare QE _        = GT
+  compare (Q a) (Q b) = compare a b
+
+instance Monoid a => Monoid (Label a) where
+	mempty = QE
+	QE `mappend` m = m
+	m `mappend` QE = m
+	(Q a) `mappend` (Q b) = Q (a `mappend` b)
+
+instance F.Foldable Label where
+    foldr _ z QE    = z
+    foldr f z (Q x) = f x z
+    foldl _ z QE    = z
+    foldl f z (Q x) = f z x
+
+{-|
+Final label state represent a set of states which elements put end to computation
+-}
+type Final a = Set.Set (Label a)
+
+{-|
+Tells if a label state is final
+-}
+terminal :: (Ord a) => Final a -> Label a -> Bool
+terminal qs q = Set.member q qs
+
+{-|
+Tells if a label state is a error state
+-}
+isError::(Eq a) => Label a -> Bool
+isError = (QE==)
+
+{-|
+Alias for a set of lalbel states
+-}
+type SetLabel a = Set.Set (Label a)
+
+{-|
+Alias for a label state of a set of label states
+-}
+type LabelSS a = Label (SetLabel a)
diff --git a/src/Data/Numerable.hs b/src/Data/Numerable.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Numerable.hs
@@ -0,0 +1,50 @@
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+{-# OPTIONS_HADDOCK show-extensions #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-|
+Module      : Cardinal
+Description : Cardinal Def
+Copyright   : (c) Jorge Santiago Alvarez Cuadros, 2016
+License     : GPL-3
+Maintainer  : sanjorgek@ciencias.unam.mx
+Stability   : experimental
+Portability : portable
+
+Cardinal definitions
+-}
+module Data.Numerable where
+
+{-|
+All sets can be one and only one:
+
+- a empty set
+- a set with, at least, one element
+-}
+data Essence = Empty | Occupied deriving(Show, Eq, Ord, Bounded)
+
+{-|
+Simple cardinality definition, we work here with numerable sets.
+
+All numerable set have one and only one:
+
+1. A finite size
+
+2. A infinite size
+-}
+data Discrete = Fin Integer | Numerable deriving(Show, Eq)
+
+{-|
+Order for numerable cardinality
+-}
+instance Ord Discrete where
+  compare (Fin n) (Fin m)     = compare n m
+  compare Numerable Numerable = EQ
+  compare Numerable _         = GT
+  compare _ _                 = LT
+
+{-|
+Bound limits for numerable cardinality
+-}
+instance Bounded Discrete where
+  minBound = Fin 0
+  maxBound = Numerable
diff --git a/src/Data/Sigma.hs b/src/Data/Sigma.hs
--- a/src/Data/Sigma.hs
+++ b/src/Data/Sigma.hs
@@ -1,6 +1,7 @@
 {-# OPTIONS_HADDOCK show-extensions #-}
-{-# OPTIONS_GHC -fno-warn-tabs #-}
-{-# LANGUAGE TypeSynonymInstances #-}
+{-# OPTIONS_GHC -fno-warn-tabs      #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE TypeSynonymInstances   #-}
 {-|
 Module      : Sigma
 Description : Alphabet and symbols
@@ -12,15 +13,24 @@
 
 Alphabet and symbols of languaje
 -}
-module Data.Sigma 
+module Data.Sigma
 (
+  -- * Symbols
 	Symbol(..)
 	,blank
-	,z0
 	,Wd(..)
+  -- * Alphabets
+  ,Alphabet(..)
+  ,enumWord
+  ,closureAlph
+  ,lessKWords
+  ,kWords
 ) where
-import Data.Monoid
-import Data.Char
+import           Data.Char
+import           Data.List
+import qualified Data.Map.Lazy as Map
+import           Data.Monoid
+import qualified Data.Set      as Set
 
 {-|
 Symbols are character, and with Unicode CharSet we have a big amount of them.
@@ -32,17 +42,60 @@
 -}
 instance Monoid Symbol where
 	mempty = blank
-	mappend x y = chr (mod ((ord x)+(ord y)) (ord maxBound))
 
 -- |Blank symbol
 blank::Symbol
 blank = '\164'
 
--- |Initial symbol for stack
-z0::Symbol
-z0 = '\248'
-
 {-|
 List symbol alias, Word are defined in Prelude
 -}
 type Wd = [Symbol]
+
+-- |An alphabet is a set of symbols
+type Alphabet = Set.Set Symbol
+
+{-|
+For every alphabet there is a function __h__ that maps one symbol to one
+natural. For every __h__ function there is a function that enumerete every
+words in that alphabet
+-}
+enumWord::Alphabet -> Wd -> Integer
+enumWord sig w = let
+    sigL = Set.toList sig
+    n = genericLength sigL
+    map' = Map.fromList (zip (Set.toList sig) [1..])
+    f [] = 0
+    f xs = (n * f (init xs))+(map' Map.! last xs)
+  in f w
+
+closureAlph' sigL = fmap (:"") sigL ++ [x:ys | ys<-closureAlph' sigL, x<-sigL]
+
+{-|
+Gives the Kleene Closure for all alphabets. closureAlph is a infinite list of
+words.
+-}
+closureAlph::Alphabet -> [Wd]
+closureAlph sig = if Set.null sig
+  then [""]
+  else "":closureAlph' (Set.toList sig)
+
+{-|
+For some alphabet __S__ and a natural number __n__ take all words of length
+__n__ or less
+-}
+lessKWords::Alphabet -> Integer -> [Wd]
+lessKWords sig k = let
+    f x y = genericLength y <= x
+  in
+    takeWhile (f k) (closureAlph sig)
+
+{-|
+For some alphabet __S__ and a natural number __n__ take all words of length __n__
+-}
+kWords::Alphabet -> Integer -> [Wd]
+kWords sig k = let
+    f x y = genericLength y == x
+    g x y = genericLength y < x
+  in
+    takeWhile (f k) (dropWhile (g k) (closureAlph sig))
diff --git a/src/Data/State.hs b/src/Data/State.hs
deleted file mode 100644
--- a/src/Data/State.hs
+++ /dev/null
@@ -1,92 +0,0 @@
-{-# OPTIONS_GHC -fno-warn-tabs #-}
-{-# OPTIONS_HADDOCK show-extensions #-}
-{-|
-Module      : State
-Description : Simple state data
-Copyright   : (c) Jorge Santiago Alvarez Cuadros, 2016
-License     : GPL-3
-Maintainer  : sanjorgek@ciencias.unam.mx
-Stability   : experimental
-Portability : portable
-
-Simple State function, have an isomorphism with Maybe but order are diferent
--}
-module Data.State 
-(
-	-- * Data and type
-	State(..)
-	,Final(..)
-	,terminal
-	-- * Functions
-	,isError
-) where
-import Control.Applicative
-import Control.Monad
-
-{-|
-Macine states are only a label, maybe a letter
--}
-data State a = 
-	-- |State constructor
-	Q a 
-	-- |Error state
-	| QE deriving(Show, Eq, Ord)
-
--- |Same as Maybe
-instance Functor State where
-	fmap _ QE = QE
-	fmap f (Q q) = Q $ f q 
-
--- |Same as Maybe
-instance Applicative State where
-	pure = Q
-	QE <*> _ = QE
-	(Q f) <*> q = fmap f q
-
--- |Same as Maybe
-instance Monad State where
-	return = pure
-	QE >>= _ = QE
-	(Q q) >>= f = f q
-
--- |Same as Maybe
-instance (Enum a) => Enum (State a) where
-	toEnum n = if n<0 then QE else Q (toEnum n)
-	fromEnum QE = -1
-	fromEnum (Q a) = fromEnum a
-
--- |In this differ with Maybe because this show a upper bounded order
-instance (Bounded a)=> Bounded (State a) where
-	minBound = Q minBound
-	maxBound = QE 
-
-instance Monoid a => Monoid (State a) where
-	mempty = QE
-	QE `mappend` m = m
-	m `mappend` QE = m
-	(Q a) `mappend` (Q b) = Q (a `mappend` b)
-
-instance Foldable State where
-    foldr _ z QE = z
-    foldr f z (Q x) = f x z
-    foldl _ z QE = z
-    foldl f z (Q x) = f z x
-
-{-|
-Final state represent a set of states which elements put end to computation
--}
-type Final a = [State a]
-
-{-|
-Tells if a state is final
--}
-terminal :: (Eq a) => Final a -> State a -> Bool
-terminal qs q = elem q qs
-
--- |Verifica si el estado es de error, comparandolo con la definicion de 
--- estado de error
-{-|
-Tells if a state is a error state
--}
-isError::(Eq a) => State a -> Bool
-isError q = q==QE
diff --git a/src/Math/Model/Automaton/Finite.hs b/src/Math/Model/Automaton/Finite.hs
--- a/src/Math/Model/Automaton/Finite.hs
+++ b/src/Math/Model/Automaton/Finite.hs
@@ -1,6 +1,6 @@
-{-# OPTIONS_GHC -fno-warn-tabs #-}
+{-# OPTIONS_GHC -fno-warn-tabs      #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeOperators          #-}
 {-|
 Module      : Finite Automaton
 Description : Finite Automaton
@@ -10,89 +10,173 @@
 Stability   : experimental
 Portability : portable
 
-Finite Automaton is a stateful machine where all transition means that machine 
+Finite Automaton is a stateful machine where all transition means that machine
 reads a symbol
 -}
 module Math.Model.Automaton.Finite
 (
-	-- * Deterministic
-	-- ** Function 
-	-- *** Recognizer
+  -- * Recognizer
+  -- ** Functions
 	Delta(..)
-	,liftD
-	-- ** Transducer
+	,NDelta(..)
+  -- ** Constructor
+	,FiniteA(..)
+	,checkString
+	-- * Transducer
+  -- ** Functions
 	,Lambda1(..)
-	,liftL1
 	,Lambda2(..)
-	,liftL2
-	-- ** Constructor
-	,FiniteA(..)
+  -- ** Constructor
 	,Transductor(..)
-	-- ** Function
-	,checkString
 	,translate
-	-- * Not deterministic
-	-- ** Function
-	,DeltaN(..)
-	,liftDN
-	-- ** Constructor
-	,FiniteAN(..)
-	,checkStringN
+  -- * Auxiliar functions
+  ,getAlphabet
+  ,endState
+  ,endStates
+  -- ** Create deltas and lambdas
+	,liftDelta
+	,liftNDelta
+	,liftL1
+	,liftL2
+  -- ** Mininmize delta
+  ,reachableDelta
+  ,distinguishableDelta
+  ,minimizeFinite
+  -- ** Equivalence
+  ,convertFA
+	,transducerToFinite
+	,finiteToMoore
+	,finiteToMealy
+  -- * Language
+  ,automatonEssence
+  ,automatonCardinality
 ) where
-import Data.State
-import Data.Sigma
-import Data.Delta
-import Data.List
-import Data.Monoid
-import Control.Monad
-import qualified Data.Map.Lazy as Map
-import qualified Data.Foldable as Fold
+import           Data.Numerable
+import           Data.Delta
+import qualified Data.Foldable   as Fold
+import           Data.Label
+import           Data.List
+import qualified Data.Map.Strict as Map
+import qualified Data.Set        as Set
+import           Data.Sigma
+import           Control.Monad.State.Lazy
 
+tupleVoid:: (a,b,c) -> (a,b,c,())
+tupleVoid (a,b,c) = (a,b,c,())
+
 {-|
-Transition function hava a State and a Symbol by domain to decide next state in 
-machine
+Union of set monad
 -}
+unionsFold:: (Ord a, Fold.Foldable t) => t (Set.Set a) -> Set.Set a
+unionsFold = Fold.foldr Set.union Set.empty
+
+{-|
+Size of a set, with large integers
+-}
+setGenericSize:: (Ord a) => Set.Set a -> Integer
+setGenericSize s = if Set.null s
+  then 0
+  else 1 + setGenericSize (Set.delete (Set.findMin s) s)
+
+{-|
+Transition function that for every pair, a State and a Symbol by domain, decide
+next state in machine
+-}
 type Delta a = (:->:) a Symbol ()
 
 {-|
-Lift a list of 3-tuples in a Delta
+Lift a list of 3-tuples to a Delta
 
->>>let delta = liftD [(0,'0',0),(0,'1',1),(1,'0',1),(1,'1',0)]
+>>>let delta = liftDelta [(0,'0',0),(0,'1',1),(1,'0',1),(1,'1',0)]
 -}
-liftD::(Ord a) => [(a,Symbol,a)] -> Delta a
-liftD ds = let
-		(xs,ys,zs) = unzip3 ds
-		f = map return 
-		xys = zip (f xs) ys
-		qzs = zip (f zs) (repeat ())
-	in Map.fromList (zip xys qzs)
+liftDelta::(Ord a) => [(a,Symbol,a)] -> Delta a
+liftDelta ds = liftD $ fmap tupleVoid ds
 
+{-|
+Transition function that for every pair, a State and a Symbol by domain, decide
+next list of states in machine
+-}
+type NDelta a = (:-<:) a Symbol ()
+
+tupleLast:: (a,b,[c]) -> (a,b,[(c,())])
+tupleLast (a,b,xs) = let
+		f x = (x,())
+	in (a,b,fmap f xs)
+
+{-|
+Lift a list of 3-tuples to a non deterministic delta
+
+>>>let deltaN = liftNDelta [(0,'0',[0]),(0,'1',[1]),(1,'0',[1]),(1,'1',[0])]
+-}
+liftNDelta::(Ord a) => [(a,Symbol,[a])] -> NDelta a
+liftNDelta ds = liftND $ fmap tupleLast ds
+
+{-|
+Transducer function
+-}
 type Lambda1 a = (:*>:) a () Symbol
 
+tupleMidVoid :: (a, b) -> (a, (), b)
+tupleMidVoid (a, b) = (a, (), b)
+
+{-|
+Lift simple transducer function
+-}
 liftL1::(Ord a) => [(a, Symbol)] -> Lambda1 a
-liftL1 ds = let
-		(xs, ys) = unzip ds
-		f = map return
-		nds = zip (zip (f xs) (repeat ())) ys
-	in Map.fromList nds
+liftL1 = liftL . fmap tupleMidVoid
 
+{-|
+Transducer function with output at transition
+-}
 type Lambda2 a = (:*>:) a Symbol Symbol
 
+{-|
+Lift second transducer function
+-}
 liftL2::(Ord a) => [(a, Symbol, Symbol)] -> Lambda2 a
-liftL2 ds = let
-		(xs, ys, zs) = unzip3 ds
-		f = map return
-		nds = zip (zip (f xs) ys) zs
-	in Map.fromList nds
- 
+liftL2 = liftL
+
 {-|
 Finite deterministic Automaton
 -}
-data FiniteA a = 
-	-- |>>>let autFin = F delta [Q 0] (Q 0)
-	F (Delta a) (Final a) (State a) deriving(Show, Eq)
+data FiniteA a =
+	-- |>>>let autFin = F delta (Set.fromList [Q 0]) (Q 0)
+	F (Delta a) (Final a) (Label a)
+	-- |>>>let autFinN = FN deltaN (Set.fromList [Q 0]) (Q 0)
+	| FN (NDelta a) (Final a) (Label a) deriving(Show,Eq)
 
 {-|
+Gets alphabet for some finite automaton
+-}
+getAlphabet:: FiniteA a -> Alphabet
+getAlphabet (F d _ _)   = getFirstParamSet d
+getAlphabet (FN dn _ _) = getFirstParamSet dn
+
+getAlphabetList::FiniteA a -> [Symbol]
+getAlphabetList (F d _ _)   = getFirstParam d
+getAlphabetList (FN dn _ _) = getFirstParam dn
+
+{-|
+For some delta, an initial state anf a word returns final state for that word
+-}
+endState:: (Ord a) => Delta a -> Wd -> State (Label a) (Label a)
+endState _ [] = get
+endState d (x:xs) = do
+	q <- get
+	put (nextD d (q,x))
+	endState d xs
+
+{-|
+Same as endState but work with no deterministic delta
+-}
+endStates::(Ord a) => NDelta a -> Wd -> State (SetLabel a) (SetLabel a)
+endStates _ [] = get
+endStates dn (x:xs) = do
+	sq <- get
+	put ((Set.unions . Set.toList) (Set.map (\q -> nextND dn () (q,x)) sq))
+	endStates dn xs
+
+{-|
 Executes a automaton over a word
 
 >>>checkString autFin "1010010101101010"
@@ -102,67 +186,343 @@
 -}
 checkString::(Ord a) => FiniteA a -> Wd -> Bool
 checkString (F d qF s) ws = let
-		q = checkString' d s ws
-		f y = ((not.isError) y)&&(terminal qF y)
+		q = evalState (endState d ws) s
+		f y = (not.isError) y && terminal qF y
 	in f q
-	where
-		checkString' _ q [] = q
-		checkString' dt q (x:xs) = checkString' dt (nextD dt (q,x)) xs
+checkString (FN dn qF s) ws = let
+		sq = evalState (endStates dn ws) (Set.fromList [s])
+		qs = Set.toList sq
+		f y = (not.isError) y && terminal qF y
+		g = any f
+	in g qs
 
-data Transductor a = 
-	Moore (Delta a) (Lambda1 a) (Final a) (State a) 
-	|Mealy (Delta a) (Lambda2 a) (Final a) (State a) deriving(Show, Eq)
+{-|
+Transducer Autmaton, both types:
 
-translate::(Ord a) => Transductor a -> Wd -> Wd
+1. Moore
+
+2. Mealy
+-}
+data Transductor a =
+	Moore (Delta a) (Lambda1 a) (Final a) (Label a)
+	|Mealy (Delta a) (Lambda2 a) (Final a) (Label a) deriving(Show, Eq)
+
+
+transMoore:: (Ord a) => Delta a -> Lambda1 a -> Wd -> State (Wd, Label a) (Label a)
+transMoore _ _ [] = do
+	(_, q) <- get
+	return q
+transMoore d l (x:xs) = do
+	(ys, q) <- get
+	put (ys++[nextSymbol l (q, ())], nextD d (q,x))
+	transMoore d l xs
+
+transMealy:: (Ord a) => Delta a -> Lambda2 a -> Wd -> State (Wd, Label a) (Label a)
+transMealy _ _ [] = do
+	(_, q) <- get
+	return q
+transMealy d l (x:xs) = do
+	(ys, q) <- get
+	put (ys++[nextSymbol l (q,x)], nextD d (q,x))
+	transMealy d l xs
+
+{-|
+For every transducer, given a word the automaton change all symbols in lambda
+-}
+translate::(Ord a) => Transductor a -> Wd -> (Wd, Bool)
 translate (Moore d l qF s) ws = let
-		(q, w) = translate d l s ws []
-	in w
-	where
-		translate _ _ QE xs ys = (QE, "Error: \nCadena:"++xs++"\nResp parcial: "++ys)
-		translate _ _ q [] xs = (q, xs)
-		translate dt lm q (y:ys) xs = translate dt lm (nextD dt (q,y)) ys (xs++[lm Map.! (q, ())])
+		(q, (nws, _)) = runState (transMoore d l ws) ([], s)
+		f y = (not.isError) y && terminal qF y
+	in (nws, f q)
 translate (Mealy d l qF s) ws = let
-		(q, w) = translate d l s ws []
-	in ws
-	where 
-		translate _ _ QE xs ys = (QE, "Error: \nCadena:"++xs++"\nResp parcial: "++ys)
-		translate _ _ q [] xs = (q, xs)
-		translate dt lm q (x:xs) ys = translate dt lm (nextD dt (q, x)) xs (ys++[lm Map.! (q,x)])
+		(q, (nws, _)) = runState (transMealy d l ws) ([], s)
+		f y = (not.isError) y && terminal qF y
+	in (nws, f q)
 
+{-|
+Transforms a Transducer to a Finite Autmaton
+-}
+transducerToFinite:: Transductor a -> FiniteA a
+transducerToFinite (Moore d _ qf s) = F d qf s
+transducerToFinite (Mealy d _ qf s) = F d qf s
 
-type DeltaN a = (:>-:) a Symbol ()
+{-|
+Transforms a Finite Autmaton with some lambda to a Moore Transducer
+-}
+finiteToMoore:: (Enum a, Ord a) => FiniteA a -> Lambda1 a -> Transductor a
+finiteToMoore (F d qf s) l = Moore d l qf s
+finiteToMoore fn l = finiteToMoore (convertFA fn) l
 
 {-|
-Lift a list of 3-tuples in a non deterministic delta
+Transforms a Finite Autmaton with some lambda to a Mealy Transducer
+-}
+finiteToMealy:: (Enum a, Ord a) => FiniteA a -> Lambda2 a -> Transductor a
+finiteToMealy (F d qf s) l = Mealy d l qf s
+finiteToMealy fn l = finiteToMealy (convertFA fn) l
 
->>>let deltaN = liftDN [(0,'0',[0]),(0,'1',[1]),(1,'0',[1]),(1,'1',[0])]
+reachableStates1 alp d xs = let
+    qs = xs ++ [nextD d (y,x) | x<-alp, y<-xs]
+    nqs = (\\) (nub qs) [QE]
+  in
+    if nqs==xs then nqs else reachableStates1 alp d nqs
+
+reachableStates2 alp d xs = let
+    qs = (xs ++ concat [Set.toList (nextND d () (y,x)) | x<-alp, y<-xs])\\[QE]
+    nqs = nub qs
+  in
+    if nqs==xs then nqs else reachableStates2 alp d nqs
+
+{-|
+Minimaize a delta for some finite automaton.
+Gets a delta with all reachable states from initial state.
 -}
-liftDN::(Ord a) => [(a,Symbol,[a])] -> DeltaN a
-liftDN ds = let
-		(xs,ys,zs) = unzip3 ds
-		f = map return
-		xys = zip (f xs) ys
-		qzs = zip (map f zs) (repeat ())
-	in Map.fromList (zip xys qzs)
+reachableDelta::(Ord a) => FiniteA a -> FiniteA a
+reachableDelta af@(F d sqf qi) = let
+    alp = getAlphabetList af
+    qs = reachableStates1 alp d [qi]
+    allUnused = (\\) (getStateDomain d) qs
+    ks = [(x,y) | x<-allUnused, y<-alp]
+    nDelta = foldl (flip Map.delete) d ks
+  in
+    F nDelta (Set.intersection sqf (Set.fromList qs)) qi
+reachableDelta afn@(FN dn sqf qi) = let
+    alp = getAlphabetList afn
+    qs = reachableStates2 alp dn [qi]
+    allUnused = (\\) (getStateDomain dn) qs
+    ks = [(x,y) | x<-allUnused, y<-alp]
+    nDelta = foldl (flip Map.delete) dn ks
+  in
+    FN nDelta (Set.intersection sqf (Set.fromList qs)) qi
 
+fstPartitionSet sf qs = let
+    (xs,ys) = Set.partition (terminal sf) qs
+  in
+    Set.delete Set.empty $ Set.fromList [xs, ys]
+
+partitionSet q = Set.filter (Set.member q)
+partitionSet2 q = Set.filter (Set.isSubsetOf q)
+
+distinguishableSet alp d partSet pi = let
+    qM = Set.findMin pi
+    eqD p q = (==) (partitionSet p partSet) (partitionSet q partSet)
+    g p q a = eqD (nextD d (p, a)) (nextD d (q, a))
+    f p q = Fold.all (g p q) alp
+    (sx, sy) = Set.partition (f qM) pi
+  in Set.delete Set.empty $ Set.fromList [sx, sy]
+
+distinguishableSet2 alp nd partSet pi = let
+    qM = Set.findMin pi
+    eqD p q = (==) (partitionSet2 p partSet) (partitionSet2 q partSet)
+    g p q a = eqD (nextND nd () (p, a)) (nextND nd () (q, a))
+    f p q = Fold.all (g p q) alp
+    (sx, sy) = Set.partition (f qM) pi
+  in Set.delete Set.empty $ Set.fromList [sx, sy]
+
+lDistinguishableSet alp d partSet = let
+    g = distinguishableSet alp d partSet
+    f = unionsFold . Set.map g
+    nPartSet = f partSet
+  in if nPartSet == partSet
+    then nPartSet
+    else lDistinguishableSet alp d nPartSet
+
+lDistinguishableSet2 alp nd partSet = let
+    g = distinguishableSet2 alp nd partSet
+    f = unionsFold . Set.map g
+    nPartSet = f partSet
+  in if nPartSet == partSet
+    then nPartSet
+    else lDistinguishableSet2 alp nd nPartSet
+
+allStateSet (F d sqf q0) = Set.unions [getStateRangeSetD d, getStateDomainSet d, sqf, Set.singleton q0]
+allStateSet (FN nd sqf q0) = Set.unions [getStateRangeSetND nd, getStateDomainSet nd, sqf, Set.singleton q0]
+
 {-|
-Finite non deterministic Automaton
+Delete redundant states and their transitions, if a state is equivalent to
+another then is redundant, two state are equivalent if they are
+undistinguisahbles.
 -}
-data FiniteAN a = 
-	-- |>>>let autFinN = FN deltaN (terminal [Q 0]) (Q 0)
-	FN (DeltaN a) (Final a) (State a) deriving(Show,Eq)
+distinguishableDelta::(Ord a) => FiniteA a -> FiniteA a
+distinguishableDelta af@(F d sf si) = let
+    allState = allStateSet af
+    pInitSet = fstPartitionSet sf allState
+    alp = getAlphabet af
+    partSet = lDistinguishableSet alp d pInitSet
+    f q = (Set.findMin . Set.findMin) $ partitionSet q partSet
+    allNewStateSet = Set.map f allState
+    g q delta a = let
+        k = (q, a)
+        nQ = nextD d k
+      in if nQ==QE
+        then delta
+        else Map.insert k (f nQ, ()) delta
+    h delta q = Fold.foldl (g q) delta alp
+    newDelta = Fold.foldl h Map.empty allNewStateSet
+  in
+    F newDelta (Set.map f sf) (f si)
+distinguishableDelta afn@(FN nd sf si) = let
+    allState = allStateSet afn
+    pInitSet = fstPartitionSet sf allState
+    alp = getAlphabet afn
+    partSet = lDistinguishableSet2 alp nd pInitSet
+    f q = (Set.findMin . Set.findMin) $ partitionSet q partSet
+    allNewStateSet = Set.map f allState
+    g q ndelta a = let
+        k = (q, a)
+        nQ = nextND nd () k
+      in if Set.null nQ
+        then ndelta
+        else Map.insert k (Set.map f nQ, ()) ndelta
+    h ndelta q = Fold.foldl (g q) ndelta alp
+    newDelta = Fold.foldl h Map.empty allNewStateSet
+  in
+    afn
 
 {-|
-Executes a non-deterministic automaton over a word, maybe overload your pc 
+Minimize a finite automaton,
+
+1. Delete redundant states
+
+2. Delete unreachable states and their transitions
 -}
-checkStringN::(Ord a) => FiniteAN a -> Wd -> Bool
-checkStringN (FN dn qF s) ws = let
-		qs = checkStringN' dn [s] ws
-		f y = ((not.isError) y)&&(terminal qF y)
-		g y = or (map f y)
-	in g qs
-	where
-		check dt k = if Map.member k dt then dt Map.! k else ([QE], ())
-		mDelta dt lq a = (nub.concat.(map fst)) (map (\q -> check dt (q,a)) lq)
-		checkStringN' _ qs [] = qs
-		checkStringN' dn qs (x:xs) = checkStringN' dn (mDelta dn qs x) xs
+minimizeFinite::(Ord a) => FiniteA a -> FiniteA a
+minimizeFinite = reachableDelta . distinguishableDelta
+
+state2Set::(Ord a) => Label a -> Set.Set a
+state2Set QE    = Set.empty
+state2Set (Q x) = Set.fromList [x]
+
+setState2Set'::(Ord a) => Set.Set a -> SetLabel a -> Set.Set a
+setState2Set' sa sP = if sP==Set.empty
+  then sa
+  else let
+      p = Set.elemAt 0 sP
+    in setState2Set' (Set.union (state2Set p) sa) (Set.delete p sP)
+
+setState2Set::(Ord a) => SetLabel a -> Set.Set a
+setState2Set = setState2Set' Set.empty
+
+nextStateSet::(Ord a) => NDelta a -> LabelSS a -> Symbol -> SetLabel a
+nextStateSet nd qsq a = let
+    f q = nextND nd () (q, a)
+    g = Set.map f
+    Q sq = fmap g qsq
+  in unionsFold sq
+
+updateDeltaBySym::(Ord a) => NDelta a -> LabelSS a -> Symbol -> Delta (SetLabel a) -> Delta (SetLabel a)
+updateDeltaBySym nd qsq a d = let
+    k = (qsq, a)
+    psp = Q $ nextStateSet nd qsq a
+  in Map.insert k (psp, ()) d
+
+updateDeltaByState::(Ord a) => NDelta a -> LabelSS a -> Delta (SetLabel a) -> Delta (SetLabel a)
+updateDeltaByState nd qsq delta = let
+    f d a = updateDeltaBySym nd qsq a d
+  in Fold.foldl f delta (getFirstParamSet nd)
+
+updateDelta::(Ord a) => NDelta a -> LabelSS a -> Delta (SetLabel a) -> Delta (SetLabel a)
+updateDelta nd qsq d = let
+    dDom = getStateDomainSet d
+    newD = updateDeltaByState nd qsq d
+    newDDom = getStateRangeSetD newD
+    difS = Set.difference (Set.difference newDDom dDom) (Set.fromList [qsq])
+    f delta psp = updateDelta nd psp delta
+  in if Set.null difS
+    then newD
+    else Fold.foldl f newD difS
+
+isNewFinal::(Ord a) => Set.Set a -> LabelSS a -> Bool
+isNewFinal _ QE = False
+isNewFinal sa (Q sq) = let
+    sInter = Set.intersection sa (setState2Set sq)
+  in not $ Set.null sInter
+
+convertFA'::(Ord a) => FiniteA a -> FiniteA (SetLabel a)
+convertFA' (FN nd sqf q0) = let
+    alp = getFirstParamSet nd
+    newQ0 = Q $ Set.singleton q0
+    newD = updateDelta nd newQ0 Map.empty
+    sf = setState2Set sqf
+    dDom = Set.unions [getStateDomainSet newD, getStateRangeSetD newD, Set.singleton newQ0]
+    newSQF = Set.filter (isNewFinal sf) dDom
+  in minimizeFinite $ F newD newSQF newQ0
+
+enumDom::(Ord a) => Set.Set (LabelSS a) -> LabelSS a -> Int
+enumDom sqsq qsq = Set.findIndex qsq sqsq
+
+succN:: (Enum a) => a -> Int -> a
+succN a 0 = a
+succN a n = succN (succ a) (n-1)
+
+newLabel::(Enum a, Ord a) => a -> Set.Set (LabelSS a) -> LabelSS a -> Label a
+newLabel o sqsq qsq = Q . succN o $ enumDom sqsq qsq
+
+mapSetLabel::(Enum a, Ord a) => a -> Set.Set (LabelSS a) -> Set.Set (LabelSS a) -> Set.Set (Label a)
+mapSetLabel o sqsq = Set.map $ newLabel o sqsq
+
+mapDeltaLabel::(Enum a, Ord a) => a -> Set.Set (LabelSS a) -> Delta (SetLabel a) -> Delta a
+mapDeltaLabel o sqsq rareD = let
+    f (qsq, x) = (newLabel o sqsq qsq, x)
+  in Map.mapKeys f (Map.map f rareD)
+
+state2Enum::(Enum a) => Label a -> a
+state2Enum QE    = toEnum 0
+state2Enum (Q a) = a
+
+mapAFLabel::(Enum a, Ord a) => Label a -> FiniteA (SetLabel a) -> FiniteA a
+mapAFLabel q af@(F d sqf q0) = let
+    o = state2Enum q
+    sqsq = allStateSet af
+  in F (mapDeltaLabel o sqsq d) (mapSetLabel o sqsq sqf) (newLabel o sqsq q0)
+
+{-|
+Finite Autmaton Equivalence
+-}
+convertFA::(Enum a, Ord a) => FiniteA a -> FiniteA a
+convertFA (F d sqf q0) = let
+    f (x, y) = Set.singleton (x, y)
+  in
+    FN (fmap f d) sqf q0
+convertFA afn@(FN nd sqf q0) = let
+    afRare = convertFA' afn
+  in
+    mapAFLabel q0 afRare
+
+{-|
+Tells if a finite automaton had empty language or not.
+-}
+automatonEssence:: (Ord a) => FiniteA a -> Essence
+automatonEssence af@F{} = let
+    (F d sqf q0) = reachableDelta af
+    rangeD = getStateRangeSetD d
+  in if Set.null (Set.intersection rangeD sqf) && Set.notMember q0 sqf
+    then Empty
+    else Occupied
+automatonEssence af@FN{} = let
+    (FN nd sqf q0) = reachableDelta af
+    rangeD = getStateRangeSetND nd
+  in if Set.null (Set.intersection rangeD sqf) && Set.notMember q0 sqf
+    then Empty
+    else Occupied
+
+acceptWord _ []      = False
+acceptWord af (w:ws) = checkString af w || acceptWord af ws
+
+allStateSize s = setGenericSize $ allStateSet s
+
+filterWords af = filter (checkString af)
+
+{-|
+Tells if a finite automaton had infinite language or the number or words in his
+language
+-}
+automatonCardinality::(Ord a) => FiniteA a -> Discrete
+automatonCardinality af = let
+    afm = minimizeFinite af
+    alp = getAlphabet afm
+    n = allStateSize afm
+    g = kWords alp
+    acceptedWord = acceptWord afm $ g =<< [n..(2*(n-1))]
+  in if acceptedWord
+    then Numerable
+    else Fin . genericLength . filterWords afm $ lessKWords alp (n-1)
diff --git a/src/Math/Model/Automaton/Stack.hs b/src/Math/Model/Automaton/Stack.hs
--- a/src/Math/Model/Automaton/Stack.hs
+++ b/src/Math/Model/Automaton/Stack.hs
@@ -1,6 +1,6 @@
-{-# OPTIONS_GHC -fno-warn-tabs #-}
+{-# OPTIONS_GHC -fno-warn-tabs      #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
-{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeOperators          #-}
 {-|
 Module      : StackA
 Description : Stack Automaton
@@ -12,61 +12,55 @@
 
 Stack Automaton
 -}
-module Math.Model.Automaton.Stack
-(
-	Delta(..)
-	,liftD
-	,StackA(..)
-	,checkString
-) where
-import Data.List
-import Data.Monoid
-import qualified Data.Map.Lazy as Map
-import qualified Data.Foldable as Fold
-import Data.Delta
-import Data.State
-import Data.Sigma
+module Math.Model.Automaton.Stack where
+import           Data.Delta
+import qualified Data.Foldable   as Fold
+import           Data.List
+import qualified Data.Map.Strict as Map
+import           Data.Sigma
+import           Data.Label
+import           Control.Monad.State.Lazy
 
 {-|
-Delta for stack machine, takes a state, a symbol in string input and a symbol in
-stack head and returns next state and update stack
+Delta for stack machine, takes a state, a symbol in string input or not and a
+symbol in stack head and returns next state and update stack
 -}
-type Delta a = (:->:) a (Symbol, Symbol) [Symbol]
+type Delta a = (:->:) a (Maybe Symbol, Symbol) Wd
 
 {-|
+A key for a delta.
+-}
+type Key a = (Label a, (Maybe Symbol, Symbol))
+
+{-|
 Takes a list of tuples and lift a Delta
 
->>>let delta = liftD [(0,'1','A',1,[AA]),(0,'0',blank,0,[A])]
+>>>let delta = liftD [(0,"(",'Z',0,"IZ"),(0,"",'Z',0,""),(0,"(",'I',0,"II"),(0,")",'I',0,"")]
 -}
-liftD::(Ord a) => [(a, Symbol, Symbol, a, [Symbol])]-> Delta a
-liftD xs = let
-		(as,bs,cs,ds,es) = unzip5 xs
-		f = map (Q)
-		p = zip bs cs
-		k = zip (f as) p
-		r = zip (f ds) es
-	in Map.fromList (zip k r)
+liftDelta:: Ord a => [(a, Wd, Symbol, a, Wd)]-> Delta a
+liftDelta xs = let
+    (as,bs,cs,ds,es) = unzip5 xs
+    f = fmap Q
+    g [] = Nothing
+    g (x:_) = Just x
+    ps = zip (fmap g bs) cs
+    ks = zip (f as) ps
+    rs = zip (f ds) es
+  in Map.fromList (zip ks rs)
 
--- |Stack machine only needs a delta and a init state
-data StackA a = S (Delta a) (State a)
+nextDTuple :: Ord a => Delta a -> Key a -> (Label a, Wd)
+nextDTuple dt k = if Map.member k dt then dt Map.! k else (QE,[])
 
-{-|
-Executes a stack machine over a word
+-- |Stack machine only needs a delta, an init state and an initial symbol.
+--
+-- This works for empty stack and final state acceptor
+data StackA a = Stack {
+  getDelta::Delta a
+  ,getInitState::Label a
+  ,getFinal::Final a
+  ,getInitSymbol::Symbol} deriving(Show, Eq)
 
->>>checkString autStack 'aaabbbcccccc'
-True
--}
-checkString::(Ord a) => StackA a -> Wd -> Bool
-checkString (S d s) ws = let
-		q = checkString' d s [z0] ws
-		f = not.isError
-	in f q
-	where
-		check dt s = if Map.member s dt then dt Map.! s else (QE,[])
-		checkString' _ QE _ _ = QE
-		checkString' _ q [] [] = q
-		checkString' _ _ (_:_) [] = QE
-		checkString' _ q [] (_:_) = QE
-		checkString' dt q (x:xs) (y:ys) = let 
-				(qn, st) = check dt (q, (y, x))
-			in checkString' dt qn (st++xs) ys
+nextState::(Ord a) => Delta a -> Wd -> State (Wd, Label a) (Label a)
+nextState _ [] = do
+	(_, q) <- get
+	return q
diff --git a/src/Math/Model/Turing.hs b/src/Math/Model/Turing.hs
--- a/src/Math/Model/Turing.hs
+++ b/src/Math/Model/Turing.hs
@@ -1,8 +1,10 @@
 {-# OPTIONS_GHC -fno-warn-tabs #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
-{-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE GADTSyntax #-}
 {-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTSyntax                #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE MultiParamTypeClasses     #-}
+{-# LANGUAGE TypeOperators             #-}
 {-|
 Module      : Turing
 Description : Turing machine abstaction
@@ -15,19 +17,19 @@
 Turing machine abstaction
 -}
 module Math.Model.Turing where
-import Data.Delta
-import Data.State
-import Data.Sigma
-import Data.List
-import Data.Monoid
-import Control.Applicative
-import qualified Data.Map.Lazy as Map
-import qualified Data.Foldable as Fold
+import           Control.Applicative
+import           Data.Delta
+import qualified Data.Foldable       as Fold
+import           Data.Label
+import           Data.List
+import qualified Data.Map.Strict     as Map
+import           Data.Monoid
+import           Data.Sigma
 
 class Ways a where
 	oposite::a -> a
 
-data LRS = 
+data LRS =
 	-- |Left move
 	L
 	-- |No move
@@ -40,7 +42,7 @@
 	oposite R = L
 	oposite S = S
 
-data FW = 
+data FW =
 	Dw
 	|Lf
 	|Rt
@@ -57,17 +59,15 @@
 type MDelta a b c = (:->:) a [b] ([b],[c])
 
 liftD::(Ord a, Ord b) => [(a,b,a,b,c)]->Delta a b c
-liftD ls = let
-		(as,bs,cs,ds,es) = unzip5 ls
-		f = map return
-		xs = zip (f as) bs
-		ys = zip (f cs) (zip ds es)
-	in Map.fromList (zip xs ys)
+liftD = liftDAux
 
 liftMD::(Ord a, Ord b) => [(a,[b],a,[b],[c])]->MDelta a b c
-liftMD ls = let
+liftMD = liftDAux
+
+liftDAux:: (Ord a, Ord b) => [(a,b,a,b,c)]-> (:->:) a b (b,c)
+liftDAux ls = let
 		(as,bs,cs,ds,es) = unzip5 ls
-		f = map return
+		f = fmap return
 		xs = zip (f as) bs
 		ys = zip (f cs) (zip ds es)
 	in Map.fromList (zip xs ys)
@@ -76,7 +76,7 @@
 	getHead::t a -> a
 	liftTape::(Monoid (t a)) => [a] -> t a
 
-data MultiTape t a = MT [t a] deriving(Show, Eq)
+newtype MultiTape t a = MT [t a]
 
 getMHead::(Tapeable t a) => MultiTape t a -> [a]
 getMHead (MT ts) = [getHead t | t<-ts]
@@ -88,7 +88,7 @@
 	moveHead::(Monoid b) => w -> t b -> t b
 
 data Model a b c where
-	TS::(Ways c) => Delta a b c->State a->Final a->Model a b c
+	TS::(Ways c) => Delta a b c->Label a->Final a->Model a b c
 
 data MultiModel a b c where
-	MTS::(Ways c) => MDelta a b c->State a->[Final a]->MultiModel a b c
+	MTS::(Ways c) => MDelta a b c->Label a->[Final a]->MultiModel a b c
diff --git a/src/Math/Model/Turing/FourWays.hs b/src/Math/Model/Turing/FourWays.hs
--- a/src/Math/Model/Turing/FourWays.hs
+++ b/src/Math/Model/Turing/FourWays.hs
@@ -1,9 +1,9 @@
 {-# OPTIONS_GHC -fno-warn-tabs #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
 {-|
 Module      : Turing1T4W
 Description : Four ways turing machine
@@ -16,27 +16,27 @@
 Four ways turing machine
 -}
 module Math.Model.Turing.FourWays where
-import Data.Delta
-import Data.State
-import Data.Sigma
-import Math.Model.Turing
-import Math.Model.Turing.TwoWays
-import Data.List
-import Data.Monoid
-import qualified Data.Foldable as Fold
+import           Control.Applicative
+import           Data.Delta
+import qualified Data.Foldable             as Fold
+import           Data.List
+import           Data.Monoid
+import           Data.Sigma
+import           Data.Label
+import           Math.Model.Turing
+import           Math.Model.Turing.TwoWays
 
 data Tracks a = Track [Tape a] (Tape a) [Tape a] deriving(Eq)
 
 instance (Show a) => Show (Tracks a) where
-	show (Track xts ts yts) = let 
-			f x = "--"++(show x)++"\n"
-			g x = "->"++(show x)++"\n"
-			h x y = (concat.(map x)) y
-		in (h f xts)++(g ts)++(h f yts)
+	show (Track xts ts yts) = let
+			f x = "--" ++ show x ++ "\n"
+			g x = "->" ++ show x ++ "\n"
+		in (f =<< xts) ++ g ts ++ (f =<< yts)
 
 instance Functor Tracks where
-	fmap f (Track xts ts yts) = let 
-			g = map (fmap f)
+	fmap f (Track xts ts yts) = let
+			g = fmap (fmap f)
 		in Track (g xts) (fmap f ts) (g yts)
 
 instance Applicative Tracks where
@@ -45,7 +45,7 @@
 
 instance (Eq s, Monoid s) => Monoid (Tracks s) where
 	mempty = Track [] mempty []
-	mappend (Track xts ts yts) (Track zts ss wts) = let 
+	mappend (Track xts ts yts) (Track zts ss wts) = let
 			f = zipWith mappend
 		in Track (f xts zts) (mappend ts ss) (f yts wts)
 
@@ -53,7 +53,7 @@
 	getHead (Track _ ts _) = getHead ts
 	liftTape ws = Track [] (liftTape ws) []
 
-instance TuringM Tape Symbol FW where 
+instance TuringM Tape Symbol FW where
 	moveHead Rt (T xs a []) = T (xs++[a]) mempty []
 	moveHead Rt (T xs a (y:ys)) = T (xs++[a]) y ys
 	moveHead Lf (T [] a ys) = T [] mempty (a:ys)
diff --git a/src/Math/Model/Turing/TwoWays.hs b/src/Math/Model/Turing/TwoWays.hs
--- a/src/Math/Model/Turing/TwoWays.hs
+++ b/src/Math/Model/Turing/TwoWays.hs
@@ -1,10 +1,10 @@
 {-# OPTIONS_GHC -fno-warn-tabs #-}
 {-# OPTIONS_HADDOCK show-extensions #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeSynonymInstances #-}
-{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleInstances     #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE TypeSynonymInstances  #-}
 {-|
 Module      : Turing1T4W
 Description : Two ways turing machine
@@ -17,34 +17,31 @@
 Two ways turing machine
 -}
 module Math.Model.Turing.TwoWays where
-import Data.Delta
-import Data.State
-import Data.Sigma
-import Math.Model.Turing
-import Data.List
-import Data.Monoid
-import Control.Applicative
-import qualified Data.Foldable as Fold
+import           Control.Applicative
+import           Data.Delta
+import qualified Data.Foldable       as Fold
+import           Data.List
+import           Data.Monoid
+import           Data.Sigma
+import           Data.Label
+import           Math.Model.Turing
 
 data Tape a = T [a] a [a] deriving(Show, Eq)
 
 instance Functor Tape where
-	fmap f (T xs a ys) = T (map f xs) (f a) (map f ys)
+	fmap f (T xs a ys) = T (fmap f xs) (f a) (fmap f ys)
 
 instance Applicative Tape where
-	pure x = T [] x [] 
+	pure x = T [] x []
 	--
 	(<*>) (T fs f gs) (T xs a ys) = T [] (f a) []
 
 instance (Eq s, Monoid s) => Monoid (Tape s) where
 	mempty = T [] mempty []
-	mappend (T xs a ys) (T [] b zs) = if 
-			b==mempty 
-		then T xs a (ys++zs) 
-		else T xs a (ys++(b:zs))
-	mappend t (T (x:xs) a ys) = if 
-			x==mempty 
-		then mappend t (T [] mempty (xs++(a:ys))) 
+	mappend (T xs a ys) (T [] b zs) = T xs a ((++) ys (if b == mempty then zs else b : zs))
+	mappend t (T (x:xs) a ys) = if
+			x==mempty
+		then mappend t (T [] mempty (xs++(a:ys)))
 		else mappend t (T [] x (xs++(a:ys)))
 
 {-|
@@ -54,14 +51,14 @@
 -}
 instance Tapeable Tape Symbol where
 	getHead (T _ a _) = a
-	liftTape ws = Fold.foldMap pure ws
+	liftTape = Fold.foldMap pure
 
 instance Tapeable Tape [Symbol] where
 	getHead (T _ as _) = as
 	liftTape [] = T [[]] [blank] [[]]
 	liftTape wss = let
-			f = map head
-			g = map tail
+			f = fmap head
+			g = fmap tail
 		in T (genericReplicate (genericLength wss) []) (f wss) (g wss)
 
 instance TuringM Tape Symbol LRS where
@@ -74,28 +71,28 @@
 instance TuringM Tape [Symbol] LRS where
 	moveHead S t = t
 	moveHead R (T xss as []) = let
-			f z = zipWith (\x y -> x++[y]) z
+			f = zipWith (\x y -> x++[y])
 			g x = genericReplicate (genericLength x) mempty
 		in T (f xss as) (g as) []
 	moveHead R (T xss as l@([]:yss)) = let
-			f z = zipWith (\x y -> x++[y]) z
+			f = zipWith (\x y -> x++[y])
 			g x = genericReplicate (genericLength x) mempty
 		in T (f xss as) (g as) l
 	moveHead R (T xss as yss) = let
-			f = map head
-			g = map tail
-			h z = zipWith (\x y -> x++[y]) z
+			f = fmap head
+			g = fmap tail
+			h = zipWith (\x y -> x++[y])
 		in T (h xss as) (f yss) (g yss)
 	moveHead L (T [] as yss) = let
 			g x = genericReplicate (genericLength x) mempty
-			f x y = zipWith (:) x y
+			f = zipWith (:)
 		in T [] (g as) (f as yss)
 	moveHead L (T l@([]:xss) as yss) = let
-			f x y = zipWith (:) x y
+			f = zipWith (:)
 			g x = genericReplicate (genericLength x) mempty
 		in T l (g as) (f as yss)
 	moveHead L (T xss as yss) = let
-			f = map last
-			g = map init
-			h z = zipWith (:) z
+			f = fmap last
+			g = fmap init
+			h = zipWith (:)
 		in T (g yss) (f yss) (h as xss)
diff --git a/test/FiniteTest.hs b/test/FiniteTest.hs
new file mode 100644
--- /dev/null
+++ b/test/FiniteTest.hs
@@ -0,0 +1,156 @@
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+module Main where
+
+import           Data.Numerable
+import qualified Data.Map                    as Map
+import qualified Data.Set                    as Set
+import           Data.Label
+import           Math.Model.Automaton.Finite
+import           Test.Hspec
+import           Test.Hspec.QuickCheck
+import           Test.Hspec.Variant
+import           Test.QuickCheck
+import           Test.QuickCheck.Variant
+
+returnEnum = return . toEnum
+
+oneOfEnum = oneof . fmap returnEnum
+
+instance Variant () where
+  invalid = return ()
+  valid = return ()
+
+instance Variant Char where
+  invalid = oneOfEnum $ [0..31]++[127..1114111]
+  valid = oneOfEnum [32..126]
+
+instance (Arbitrary a) => Variant (Label a) where
+  invalid = return QE
+  valid = do
+    x <- arbitrary
+    return $ Q x
+
+instance (Variant a) => Variant [a] where
+  valid = do
+    x <- valid
+    xs <- valid
+    (oneof . fmap return) [x:xs, []]
+  invalid = do
+    x <- invalid
+    xs <- invalid
+    y <- valid
+    ys <- valid
+    (oneof . fmap return) [[x], x:xs, x:ys, y:xs]
+
+instance (Arbitrary a) => Arbitrary (Label a) where
+  arbitrary = oneof [invalid, valid]
+
+instance (Variant a, Variant b) => Variant ((,) a b) where
+  invalid = do
+    x <- invalid
+    y <- invalid
+    z <- valid
+    w <- valid
+    (oneof . fmap return) [(x,y), (x,z), (w,y)]
+  valid = do
+    x <- valid
+    y <- valid
+    return (x, y)
+
+instance (Ord a, Variant a) => Variant (Set.Set a) where
+  invalid = do
+    xs <- invalid
+    return $ Set.fromList xs
+  valid = do
+    xs <- valid
+    (oneof . fmap return) [Set.empty, Set.fromList xs]
+
+instance (Ord k, Variant k, Variant a) => Variant (Map.Map k a) where
+  invalid = do
+    xs <- invalid
+    return $ Map.fromList xs
+  valid = do
+    xs <- valid
+    (oneof . fmap return) [Map.empty, Map.fromList xs]
+
+instance (Ord a,Arbitrary a) => Variant (FiniteA a) where
+  invalid = do
+    nd <- valid
+    sqf <- valid
+    q0 <- valid
+    return $ FN nd sqf q0
+  valid = do
+    d <- valid
+    sqf <- valid
+    q0 <- valid
+    return $ F d sqf q0
+
+instance (Ord a, Arbitrary a) => Arbitrary (FiniteA a) where
+  arbitrary = do
+    afn <- invalid
+    af <- valid
+    (oneof . fmap return) [afn, af]
+
+pairWord = F (liftDelta [(1,'0',1),(1,'1',2),(2,'0',2),(2,'1',1)]) (Set.fromList [Q 2]) (Q 2)
+
+emptyLang1 = F (liftDelta [(1,'0',1),(1,'1',2),(2,'0',2),(2,'1',1)]) (Set.fromList [Q 3]) (Q 2)
+
+finiteLang = F (liftDelta []) (Set.fromList [Q 2]) (Q 2)
+
+finiteAut = describe "Finite automaton check" . it "pair of one's" $ do
+    checkString pairWord "" `shouldBe` True
+    checkString pairWord "00000" `shouldBe` True
+    checkString pairWord "00101" `shouldBe` True
+    checkString pairWord "00001" `shouldBe` False
+    checkString pairWord "11111" `shouldBe` False
+    checkString pairWord "11011" `shouldBe` True
+
+transDetTest = describe "Transform" $ do
+  prop "reachable check same" $
+    \ af w -> checkString (reachableDelta (af::FiniteA Int)) w == checkString af w
+  prop "distinguishable check same" $
+    \ af w -> checkString (distinguishableDelta (af::FiniteA Int)) w == checkString af w
+  prop "minimize check same" $
+    \ af w -> checkString (minimizeFinite (af::FiniteA Int)) w == checkString af w
+  prop "minimize" $
+    \ af -> let naf = minimizeFinite (af::FiniteA Int) in minimizeFinite naf == naf
+  prop "equivalence" $
+    \fa w -> checkString (fa:: FiniteA Int) w == checkString (convertFA fa) w
+
+cardinalityTest = describe "Cardinal" $ do
+  it "essence" $ do
+    automatonEssence pairWord `shouldBe` Occupied
+    automatonEssence emptyLang1 `shouldBe` Empty
+    automatonEssence finiteLang `shouldBe` Occupied
+  it "cardinality" $ do
+    automatonCardinality pairWord `shouldBe` Numerable
+    automatonCardinality emptyLang1 `shouldBe` Fin 0
+    automatonCardinality finiteLang `shouldBe` Fin 1
+  prop "if empty then Fin 0" $
+    \ af -> let
+        e = automatonEssence (af:: FiniteA Int)
+        c = automatonCardinality af
+      in (e /= Empty) || (c == Fin 0)
+  prop "if (Fin n) where n>0 then Occupied" $
+    \ af -> let
+        e = automatonEssence (af:: FiniteA Int)
+        c@(Fin n) = automatonCardinality af
+      in (c /= Numerable) || (n == 0) || (e == Occupied)
+  prop "if Numerable then Occupied" $
+    \ af -> let
+        e = automatonEssence (af:: FiniteA Int)
+        c = automatonCardinality af
+      in (c /= Numerable) || (e == Occupied)
+  prop "if Numerable then not Empty" $
+    \ af -> let
+        e = automatonEssence (af:: FiniteA Int)
+        c = automatonCardinality af
+      in (c /= Numerable) || (e /= Empty)
+
+
+main::IO ()
+main = hspec . describe "Math.Model.Automaton.Finite" $ do
+    finiteAut
+    transDetTest
+    cardinalityTest
diff --git a/test/LabelTest.hs b/test/LabelTest.hs
new file mode 100644
--- /dev/null
+++ b/test/LabelTest.hs
@@ -0,0 +1,23 @@
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+module Main where
+
+import qualified Data.Set              as Set
+import           Data.Label
+import           Test.Hspec
+import           Test.Hspec.QuickCheck
+import           Test.QuickCheck
+
+instance (Arbitrary a) => Arbitrary (Label a) where
+  arbitrary = do
+    x <- arbitrary
+    (oneof . fmap return) [QE, Q x]
+
+terminalTest = describe "terminal" $ do
+  prop "Not in" $
+    \x y -> (x == y) || not (terminal (Set.fromList [x]) (y:: Label Int))
+  prop "In" $
+    \x -> terminal (Set.fromList [x]) (x:: Label Int)
+
+main::IO ()
+main = hspec $
+	describe "Data.State" terminalTest
diff --git a/test/SigmaTest.hs b/test/SigmaTest.hs
new file mode 100644
--- /dev/null
+++ b/test/SigmaTest.hs
@@ -0,0 +1,33 @@
+{-# OPTIONS_GHC -fno-warn-tabs #-}
+module Main where
+
+import qualified Data.Set              as Set
+import           Data.Sigma
+import           Test.Hspec
+import           Test.Hspec.QuickCheck
+import           Test.QuickCheck
+
+enumWordTest = describe "enumWordTest" $ do
+  let alpF = enumWord (Set.fromList ['a','b','c'])
+  it "Empty word and empty alphabet" $
+    enumWord Set.empty [] `shouldBe` 0
+  it "Empty word and non-empty alphabet" $
+    alpF [] `shouldBe` 0
+  it "Symbol word1" $
+    alpF "a" `shouldBe` 1
+  it "Symbol word2" $
+    alpF "b" `shouldBe` 2
+  it "Symbol word3" $
+    alpF "c" `shouldBe` 3
+  it "Two Symbol word" $
+    alpF "aa" `shouldBe` 4
+  it "Two Symbol word1" $
+    alpF "ab" `shouldBe` 5
+  it "Two Symbol word2" $
+    alpF "bc" `shouldBe` 9
+  it "Two Symbol word3" $
+    alpF "ca" `shouldBe` 10
+
+main::IO ()
+main = hspec $
+  describe "Data.Sigma" enumWordTest
diff --git a/turingMachine.cabal b/turingMachine.cabal
--- a/turingMachine.cabal
+++ b/turingMachine.cabal
@@ -1,13 +1,10 @@
--- Initial turingMachine.cabal generated by cabal init.  For further 
--- documentation, see http://haskell.org/cabal/users-guide/
-
 name:                turingMachine
 -- PVP summary:      +-+------- breaking API changes
 --                   | | +----- non-breaking API additions
 --                   | | | +--- code changes with no API change
-version:             0.1.3.0
+version:             1.0.0.0
 synopsis:            An implementation of Turing Machine and Automaton
-description:         An implementation of Turing Machine and Automaton for 
+description:         An implementation of Turing Machine and Automaton for
                      language theory
 homepage:            https://github.com/sanjorgek/turingMachine
 license:             GPL-3
@@ -27,22 +24,70 @@
 
 library
   exposed-modules:     Data.Delta
+                       , Data.Helper
+                       , Data.Numerable
                        , Data.Sigma
-                       , Data.State
+                       , Data.Label
                        , Math.Model.Automaton.Finite
                        , Math.Model.Automaton.Stack
                        , Math.Model.Turing
                        , Math.Model.Turing.TwoWays
                        , Math.Model.Turing.FourWays
-  -- other-modules:       
+  -- other-modules:
   other-extensions:    TypeSynonymInstances
                        , TypeOperators
                        , MultiParamTypeClasses
                        , GADTSyntax
+                       , GADTs
                        , ExistentialQuantification
                        , TypeFamilies
                        , FlexibleInstances
-  build-depends:       base >=4.8 && <4.9
+  build-depends:       base >=4.6 && <5
                        , containers >= 0.5.6.2
+                       , mtl >= 2 && < 2.3
   hs-source-dirs:      src
+  default-language:    Haskell2010
+
+
+test-suite state
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             LabelTest.hs
+  --other-modules:
+  build-depends:       base
+                       , containers
+                       , hspec
+                       , hspecVariant >=1 && <2
+                       , QuickCheck
+                       , QuickCheckVariant >=1 && <2
+                       , turingMachine
+  default-language:    Haskell2010
+
+test-suite sigma
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             SigmaTest.hs
+  --other-modules:
+  build-depends:       base
+                       , hspec
+                       , hspecVariant >=1 && <2
+                       , QuickCheck
+                       , QuickCheckVariant >=1 && <2
+                       , QuickCheck
+                       , containers
+                       , turingMachine
+  default-language:    Haskell2010
+
+test-suite finite
+  type:                exitcode-stdio-1.0
+  hs-source-dirs:      test
+  main-is:             FiniteTest.hs
+  --other-modules:
+  build-depends:       base
+                       , hspec
+                       , hspecVariant >=1 && <2
+                       , QuickCheck
+                       , QuickCheckVariant >=1 && <2
+                       , containers
+                       , turingMachine
   default-language:    Haskell2010