Stuff...

6 files changed, 367 insertions, 199 deletions

diff --git a/edit-lens/package.yaml b/edit-lens/package.yaml
index 88a35ca..7455dcc 100644
--- a/edit-lens/package.yaml
+++ b/edit-lens/package.yaml
@@ -36,6 +36,8 @@ dependencies:
   - mtl
   - wl-pprint
   - intervals
+  - universe
+  - dotgen
 
 # ghc-options: [ -O2 ]
 
diff --git a/edit-lens/src/Control/DFST.lhs b/edit-lens/src/Control/DFST.lhs
index 6e16c74..271a13e 100644
--- a/edit-lens/src/Control/DFST.lhs
+++ b/edit-lens/src/Control/DFST.lhs
@@ -10,9 +10,10 @@ module Control.DFST
   ( DFST(..)
   , runDFST, runDFST'
   , toFST
+  , dotDFST
   ) where
 
-import Data.Map.Lazy (Map, (!?))
+import Data.Map.Lazy (Map, (!?), (!))
 import qualified Data.Map.Lazy as Map
 
 import Data.Set (Set)
@@ -21,6 +22,8 @@ import qualified Data.Set as Set
 import Data.Sequence (Seq(..))
 import qualified Data.Sequence as Seq
 
+import Data.Bool (bool)
+
 import Data.Monoid
 
 import Numeric.Natural
@@ -30,6 +33,8 @@ import Control.Monad.State
 
 import Control.FST (FST(FST))
 import qualified Control.FST as FST
+
+import Text.Dot
 \end{code}
 \end{comment}
 
@@ -39,6 +44,10 @@ import qualified Control.FST as FST
   Zusätzlich ändern wir die Darstellung indem wir $\epsilon$-Transitionen kontrahieren.
   Wir erweitern hierfür die Ausgabe pro Transition von einem einzelnen Zeichen zu einem Wort beliebiger Länge und fügen, bei jeder Kontraktion einer $\epsilon$-Transition $A \rightarrow B$, die Ausgabe der Transition vorne an die Ausgabe aller Transitionen $B \rightarrow \ast$ von $B$ an.
 \end{defn}
+
+\begin{rem}
+  Die FSTs aus den bisherigen Beispielen \ref{eg:linebreak}, \ref{eg:w100}, \ref{eg:l80timesw100} sind deterministisch.
+\end{rem}
   
 \begin{code}
 data DFST state input output = DFST
@@ -105,5 +114,21 @@ runDFST' _             st  Empty     acc = (acc, Just st)
 runDFST' dfst@DFST{..} st (c :<| cs) acc = case stTransition !? (st, c) of
   Just (st', mc') -> runDFST' dfst st' cs $ acc <> mc'
   Nothing -> (acc, Nothing)
+  
+dotDFST :: forall state input output. (Ord state, Ord input, Ord output, Show state, Show input, Show output) => DFST state input output -> Dot ()
+dotDFST DFST{..} = do
+  let
+    stTransition' = Map.toList stTransition
+    states = Set.singleton stInitial <> stAccept <> foldMap (Set.singleton . fst . fst) stTransition' <> foldMap (Set.singleton . fst . snd) stTransition'
+  stateIds <- sequence . (flip Map.fromSet) states $ \st -> node
+    [ ("label", show st)
+    , ("peripheries", bool "1" "2" $ st `Set.member` stAccept)
+    ]
+  init <- node [ ("label", ""), ("shape", "none") ]
+  init .->. (stateIds ! stInitial)
+  forM_ stTransition' $ \((f, inS), (t, outS)) -> do
+    edge (stateIds ! f) (stateIds ! t)
+      [ ("label", show (inS, outS))
+      ]
 \end{code}
 \end{comment}
diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
index fe33bd6..1e5bbb1 100644
--- a/edit-lens/src/Control/DFST/Lens.lhs
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -37,6 +37,9 @@ import qualified Data.Set as Set
 import Data.Map.Lazy (Map)
 import qualified Data.Map.Lazy as Map
 
+import qualified Data.Map as Strict (Map)
+import qualified Data.Map.Strict as Strict.Map
+
 import Data.Compositions (Compositions)
 import qualified Data.Compositions as Comp
 
@@ -45,23 +48,26 @@ import qualified Data.Algorithm.Diff as Diff
 
 import Data.Monoid
 import Data.Bool (bool)
-import Data.Maybe (fromMaybe, maybeToList, listToMaybe, catMaybes, isNothing, isJust)
+import Data.Maybe (fromMaybe, maybeToList, listToMaybe, catMaybes, isNothing, isJust, mapMaybe)
 import Data.Function (on)
 import Data.Foldable (toList)
-import Data.List (partition)
+import Data.List (partition, isPrefixOf)
 
 import Control.Exception (assert)
 
+import System.IO (Handle, hPutStrLn, IOMode(AppendMode), withFile)
 import System.IO.Unsafe
 import Text.PrettyPrint.Leijen (Pretty(..))
 
+import Data.Universe (Finite(..))
+
 \end{code}
 \end{comment}
 
 
-Wir betrachten, zur Einfachheit, ein minimiales Set von Edits auf Strings\footnote{Wie in der Konstruktion zum Longest Common Subsequence Problem}:
-
 \begin{defn}[Atomare edits of strings]
+Wir betrachten, zur Einfachheit, ein minimiales Set von Edits auf Strings\footnote{Wie in der Konstruktion zum Longest Common Subsequence Problem}, bestehend nur aus Einfügung eines einzelnen Zeichens und löschen des Zeichens an einer einzelnen Position:
+
 \begin{code}
 data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
                          | Delete { _sePos :: pos }
@@ -73,7 +79,6 @@ data StringEdit pos char = Insert { _sePos :: pos, _seInsertion :: char }
 -- @seInsertion :: Traversal' (StringEdits pos char) char@
 makeLenses ''StringEdit
 \end{code}
-\end{defn}
 
 Atomare edits werden, als Liste, zu edits komponiert.
 Wir führen einen speziellen edit ein, der nicht-Anwendbarkeit der edits repräsentiert:
@@ -86,32 +91,19 @@ makePrisms ''StringEdits
 
 stringEdits :: Traversal (StringEdits pos char) (StringEdits pos' char') (StringEdit pos char) (StringEdit pos' char')
 \end{code}
+\end{defn}
+
 \begin{comment}
 \begin{code}
 stringEdits = _StringEdits . traverse
-\end{code}
-\end{comment}
-\begin{code}
+
 insert :: pos -> char -> StringEdits pos char
-\end{code}
-\begin{comment}
-\begin{code}
 insert n c = StringEdits .  Seq.singleton $ Insert n c
-\end{code}
-\end{comment}
-\begin{code}
+
 delete :: pos -> StringEdits pos char
-\end{code}
-\begin{comment}
-\begin{code}
 delete n = StringEdits .  Seq.singleton $ Delete n
-\end{code}
-\end{comment}
-\begin{code}
+
 replace :: Eq pos => pos -> char -> StringEdits pos char
-\end{code}
-\begin{comment}
-\begin{code}
 replace n c = insert n c <> delete n
 
 -- | Rudimentarily optimize edit composition
@@ -130,7 +122,7 @@ instance Eq pos => Monoid (StringEdits pos char) where
 \end{code}
 \end{comment}
 
-Da wir ein minimales set an atomaren edits gewählt haben, ist die Definiton der Modulnstruktur über Strings des passenden Alphabets recht einfach:
+Da wir ein minimales Set an atomaren edits gewählt haben, ist die Definiton der Modulnstruktur über Strings des passenden Alphabets recht einfach:
 \begin{code}
 instance Module (StringEdits Natural char) where
   type Domain (StringEdits Natural char) = Seq char
@@ -159,12 +151,6 @@ instance Module (StringEdits Natural char) where
 
 \end{code}
 
-% TODO Make notation mathy
-
-Um zunächst eine asymmetrische edit-lens \texttt{StringEdits -> StringEdits} mit akzeptabler Komplexität für einen bestimmten DFST (entlang der \emph{Richtung} des DFSTs) zu konstruieren möchten wir folgendes Verfahren anwenden:
-
-Gegeben eine Sequenz von zu übersetzenden Änderungen genügt es die Übersetzung eines einzelnen \texttt{StringEdit}s in eine womöglich längere Sequenz von \texttt{StringEdits} anzugeben, alle \texttt{StringEdits} aus der Sequenz derart zu übersetzen (hierbei muss auf die korrekte Handhabung des Komplements geachtet werden) und jene Übersetzungen dann zu concatenieren.
-
 Wir definieren zunächst die \emph{Wirkung} eines DFST auf einen festen String als eine Abbildung \texttt{state -> (Seq output, Maybe state)}, die den aktuellen Zustand vor dem Parsen des Strings auf den Zustand danach und die (womöglich leere) Ausgabe schickt.
 Wir annotieren Wirkungen zudem mit dem konsumierten String.
 Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden.
@@ -189,10 +175,30 @@ instance Monoid (DFSTAction state input output) where
     }
 \end{code}
 \end{comment}
+
 \begin{code}
+dfstAction :: forall state input output. (Finite state, Ord state, Ord input) => DFST state input output -> input -> DFSTAction state input output
+-- | Smart constructor of `DFSTAction` ensuring that `Seq.length . dfstaConsumes == const 1` and that `runDFSTAction` has constant complexity
+\end{code}
+\begin{comment}
+\begin{code}
+dfstAction dfst (Seq.singleton -> dfstaConsumes) = DFSTAction{..}
+  where
+    runDFSTAction :: state -> (Seq output, Maybe state)
+    runDFSTAction = (actionMap Strict.Map.!)
+
+    actionMap :: Strict.Map state (Seq output, Maybe state)
+    actionMap = Strict.Map.fromSet (\st -> runDFST' dfst st dfstaConsumes Seq.empty) $ Set.fromList universeF
+\end{code}
+\end{comment}
 
+Wir halten im Komplement der edit-lens einen Cache der monoidalen Summen aller kontinuirlichen Teillisten.
+\texttt{Compositions} ist ein balancierter Binärbaum, dessen innere Knoten mit der monoidalen Summe der Annotationen aller Blätter annotiert sind.
+\begin{code}
 type DFSTComplement state input output = Compositions (DFSTAction state input output)
+\end{code}
 
+\begin{code}
 runDFSTAction' :: DFSTComplement state input output -> state -> (Seq output, Maybe state)
 runDFSTAction' = runDFSTAction . Comp.composed
 
@@ -203,28 +209,22 @@ dfstaProduces :: DFSTComplement state input output -> state -> Seq output
 dfstaProduces = fmap fst . runDFSTAction'
 \end{code}
 
-Die Unterliegende Idee von $\Rrightarrow$ ist nun im Komplement der edit-lens eine Liste von Wirkungen (eine für jedes Zeichen der Eingabe des DFSTs) und einen Cache der monoidalen Summen aller kontinuirlichen Teillisten zu halten.
-
-Wir können die alte DFST-Wirkung zunächst anhand des Intervalls indem der input-String von allen gegebenen edits betroffen ist in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen.
+Für $\Rrightarrow$ können wir die alte DFST-Wirkung zunächst anhand des Intervalls indem der input-String von allen gegebenen edits betroffen ist (\texttt{affected}) in einen unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen.
 
 Da wir wissen welche Stelle im input-String vom ersten gegebenen edit betroffen ist können wir, anhand der Wirkung des Teilstücks bis zu jener Stelle, den betroffenen Suffix wiederum teilen.
 Die Wirkung ab der betroffenen Stelle im input-String können wir als Komposition der Wirkung der durch den edit betroffenen Stelle und derer aller Zeichen danach bestimmen.
 Nun gilt es nur noch die Differenz (als `StringEdits`) des vorherigen Suffixes im output-String und des aus der gerade berechneten Wirkung zu bestimmen, wir bedienen uns hierzu dem Unix Standard-Diff-Algorithmus zwischen der ursprünglichen Ausgabe und dem Ergebnis der Iteration des Verfahrens auf alle gegebenen edits.
 
-Für die asymmetrische edit-lens entgegen der DFST-Richtung $\Lleftarrow$ verwenden wir Breitensuche über die Zustände des DFST innerhalb eines iterative vergrößerten Intervalls:
-
-Wir bestimmen zunächst (`affected`) eine obere Schranke an das Intervall in dem der Ausgabe-String vom edit betroffen ist und generieren eine von dort quadratisch wachsende Serie von Intervallen.
+Für die asymmetrische edit-lens entgegen der DFST-Richtung $\Lleftarrow$ verwenden wir Breitensuche über die Zustände des DFST innerhalb des von allen gegeben edits betroffenen Intervalls:
 
-Für jedes Intervall ("lokalere" Änderungen werden präferiert) schränken wir zunächst den DFST (zur einfachereren Implementierung in seiner Darstellung als FST) vermöge \texttt{restrictOutput} derart ein, dass nur die gewünschte Ausgabe produziert werden kann.
+Wir unterteilen zunächst das Komplement an den Grenzen des betroffenen Intervalls im output-String in drei Teile (durch Akkumulation der Elemente des Komplements bis die gewünschte Länge erreicht ist).
 
-Wir betrachten dann in jedem Schritt (beginnend mit dem initialen Zustand des DFST) alle ausgehenden Transitionen und ziehen hierbei jene vor, die im vorherigen Lauf (gespeichert im Komplement der edit-lens), ebenfalls genommen wurden.
-Abweichungen vom im Komplement gespeicherten Lauf lassen wir nur innerhalb des betrachteten Intervalls zu und wählen in diesem Fall einen Edit auf der Eingabe, der die gewählte Abweichung produziert.
-Es wird zudem, wie für Breitensuche üblich, jeder besuchte Zustand markiert und ausgehende Transitionen nicht ein zweites mal betrachtet.
+Wir transformieren dann den DFST in einen FST, dessen Ausgabe wir mit \texttt{restrictOutput} auf das gewünschte Fragment einschränken, setzen als initialen Zustand des FST den Zustand am linken Rand des von den edits betroffenen Intervalls und akzeptieren jene Zustände, von denen aus das Komplement-Fragment ab dem rechten Rand des betroffenen Intervalls zu einem im ursprünglichen DFST akzeptierten Zustand führt.
 
-Erreichen wir einen finalen Zustand (wegen der Einschränkung des DFSTs wurde dann auch genau die gewünschte Ausgabe produziert), so fügen wir an die gesammelten Eingabe-edits eine Serie von deletions an, die den noch nicht konsumierten suffix der Eingabe verwerfen und brechen die Suche unter Rückgabe der Eingabe-edits und des neuen Laufs ab.
+Wir verwenden dann gewöhnliche Breitensuche über die Zustände und Transitionen des soeben konstruierten FSTs um einen Lauf-Fragment zu bestimmen, dass wir in das betroffene Intervall einsetzen können.
+Hierbei sind sämtliche Randbedingungen (korrekte Ausgabe, Übereinstimmung an den Intervallgrenzen) bereits in den FST kodiert sodass wir nur noch prüfen müssen, dass der gefunde Lauf in einem akzeptierten Zustand endet.
 
-In Haskell formulieren wir das vorzeitige Abbrechen der Suche indem wir eine vollständige Liste von Rückgabe-Kandidaten konstruieren und dann immer ihr erstes Element zurück geben.
-Wegen der verzögerten Auswertungsstrategie von Haskell wird auch tatsächlich nur der erste Rückgabe-Kandidat konstruiert.
+Die input-edits können nun wiederum, unter Beachtung der Verschiebung der indices um die Länge der Eingabe vor der linken Intervallgrenze, mit dem Unix Standard-Diff-Algorithmus berechnet werden.
 
 \begin{comment}
 \begin{code}
@@ -232,7 +232,7 @@ type LState state input output = (Natural, (state, Maybe (input, Natural)))
 \end{code}
 \end{comment}
 \begin{code}
-dfstLens :: forall state input output. (Ord state, Ord input, Ord output, Show state, Show input, Show output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits Natural input) (StringEdits Natural output)
+dfstLens :: forall state input output. (Ord state, Ord input, Ord output, Show state, Show input, Show output, Finite state) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits Natural input) (StringEdits Natural output)
 \end{code}
 \begin{comment}
 \begin{code}
@@ -244,166 +244,108 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL
     propR :: (DFSTComplement state input output, StringEdits Natural input) -> (DFSTComplement state input output, StringEdits Natural output)
     propR (c, SEFail) = (c, SEFail)
     propR (c, StringEdits Seq.Empty) = (c, mempty)
-    propR (c, es'@(StringEdits (es :> e)))
+    propR (c, lEs@(StringEdits (es :> e)))
       | (_, Just final) <- runDFSTAction' c' stInitial
       , final `Set.member` stAccept
       = (c', rEs)
       | otherwise
       = (c, SEFail)
       where
-        Just int = affected es'
+        Just int = affected lEs
         (cAffSuffix, cAffPrefix) = Comp.splitAt (Comp.length c - fromIntegral (Int.inf int)) c
         (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
         cSuffix'
           | Delete _       <- e
           , Comp.length cSuffix > 0 = Comp.take (pred $ Comp.length cSuffix) cSuffix
-          | Insert _ nChar <- e = cSuffix <> Comp.singleton (DFSTAction (\x -> runDFST' dfst x (pure nChar) Seq.empty) (Seq.singleton nChar))
+          | Insert _ nChar <- e = cSuffix <> Comp.singleton (dfstAction dfst nChar)
           | otherwise = Comp.singleton $ DFSTAction (\_ -> (Seq.empty, Nothing)) Seq.empty
         (c', _) = propR (cSuffix' <> cPrefix, StringEdits es)
         (cAffSuffix', _) = Comp.splitAt (Comp.length c' - Comp.length cAffPrefix) c'
-        (_, Just pFinal) = runDFSTAction' cPrefix stInitial
-        rEs = strDiff (fst $ runDFSTAction' cAffSuffix pFinal) (fst $ runDFSTAction' cAffSuffix' pFinal) & stringEdits . sePos . from enum +~ length (dfstaProduces cAffPrefix stInitial)
-        
+        (_, Just pFinal) = runDFSTAction' cAffPrefix stInitial
+        rEs = strDiff (dfstaProduces cAffSuffix pFinal) (dfstaProduces cAffSuffix' pFinal) & stringEdits . sePos . from enum +~ length (dfstaProduces cAffPrefix stInitial)
+
 
     propL :: (DFSTComplement state input output, StringEdits Natural output) -> (DFSTComplement state input output, StringEdits Natural input)
     propL (c, StringEdits Seq.Empty) = (c, mempty)
     propL (c, es) = fromMaybe (c, SEFail) $ do
-      let prevOut = dfstaProduces c stInitial
-      newOut <- prevOut `apply` es
-      affected' <- affected es
+      -- Determine states @(iState, fState)@ at the boundary of the region affected by @es@
+      ((,) <$> Int.inf <*> Int.sup -> (minAff, maxAff)) <- affected es
+      trace (show (minAff, maxAff)) $ Just ()
+      let
+        prevTrans :: Natural -> Maybe ( DFSTComplement state input output -- ^ Run after chosen transition to accepting state
+                                      , (state, input, Seq output, state)
+                                      , DFSTComplement state input output -- ^ Run from `stInitial` up to chosen transition
+                                      )
+        -- ^ Given an index in the output, find the associated transition in @c@
+        prevTrans needle = do
+          let (after, before) = prevTrans' (c, mempty)
+          transSt <- view _2 $ runDFSTAction (Comp.composed before) stInitial
+          trace ("transSt = " ++ show transSt) $ Just ()
+          let (after', trans) = Comp.splitAt (pred $ Comp.length after) after
+              DFSTAction{..} = Comp.composed trans
+          [inS] <- return $ toList dfstaConsumes
+          (outSs , Just postTransSt) <- return $ runDFSTAction transSt
+          return (after', (transSt, inS, outSs, postTransSt), before)
+          where
+            -- | Move monoid summands from @after@ to @before@ until first transition of @after@ produces @needle@ or @after@ is a singleton
+            prevTrans' (after, before)
+              | producedNext > needle = (after, before)
+              | Comp.length after == 1 = (after, before)
+              | otherwise = prevTrans' (after', before')
+              where
+                producedNext = fromIntegral . Seq.length . traceShowId $ dfstaProduces before' stInitial
+                (after', nextTrans) = Comp.splitAt (pred $ Comp.length after) after
+                before' = nextTrans `mappend` before
+      (_, (iState, _, _, _), prefix) <- prevTrans minAff 
+      trace (show (iState, Comp.length prefix)) $ Just ()
+      (suffix, (pfState, _, _, fState), _) <- prevTrans maxAff
+      trace (show (pfState, fState, Comp.length suffix)) $ Just ()
+
+      newOut <- dfstaProduces c stInitial `apply` es
+      let affNewOut = (\s -> Seq.take (Seq.length s - Seq.length (dfstaProduces suffix fState)) s) $ Seq.drop (Seq.length $ dfstaProduces prefix stInitial) newOut
+      trace (show (iState, fState, affNewOut)) $ Just ()
+
       let outFST :: FST (LState state input output) input output
-          -- outFST = wordFST newOut `productFST` toFST dfst
-          outFST = restrictOutput newOut $ toFST dfst
-      
-          trace x y = flip seq y . unsafePerformIO $ appendFile "lens.log" (x <> "\n\n")
-
-          inflate by int
-            | Int.null int = Int.empty
-            | inf >= by = inf - by Int.... sup + by
-            | otherwise = 0 Int.... sup + by
-            where
-              (inf, sup) = (,) <$> Int.inf <*> Int.sup $ int
-          fragmentIntervals = (++ [all]) . takeWhile (not . Int.isSubsetOf (0 Int.... max)) $ inflate <$> 0 : [ 2^n | n <- [0..ceiling (logBase 2.0 max)] ] <*> pure affected'
-            where
-              max :: Num a => a
-              max = fromIntegral $ Seq.length newOut
-              all = 0 Int.... max
-          runCandidates :: Interval Natural -- ^ Departure from complement-run only permitted within interval (to guarantee locality)
-                        -> [ ( Seq (LState state input output, Maybe output) -- ^ Computed run
-                             , StringEdits Natural input
-                             , DFSTComplement state input output
-                             )
-                           ]
-          runCandidates focus = map ((,,) <$> view _1 <*> view _2 <*> view (_3 . _2)) $ go Set.empty [(Seq.empty, mempty, (c, mempty), 0)]
-            where
-              go _ [] = []
-              go visited (args@(run, edits, compZipper, inP) : alts) = 
-                  [ (run', finalizeEdits remC inP' edits', compZipper', inP') | (run', edits', compZipper'@(remC, _), inP') <- args : conts, isFinal run' ]
-                  ++ go visited' (alts ++ conts)
-                where
-                  conts
-                    | lastSt <- view _1 <$> Seq.lookup (pred $ Seq.length run) run
-                    , lastSt `Set.member` visited = []
-                    | otherwise = continueRun edits compZipper inP run
-                  visited' = Set.insert (view _1 <$> Seq.lookup (pred $ Seq.length run) run) visited
-
-              isFinal :: Seq (LState state input output, Maybe output) -> Bool
-              -- ^ Is the final state of the run a final state of the DFST?
-              isFinal Seq.Empty = (0, (stInitial, Nothing)) `Set.member` FST.stAccept outFST
-                               && (0 Int.... fromIntegral (Seq.length newOut)) `Int.isSubsetOf` focus
-              isFinal (_ :> (lastSt, _)) = lastSt `Set.member` FST.stAccept outFST
-
-              finalizeEdits :: DFSTComplement state input output -- ^ Remaining complement
-                            -> Natural -- ^ Input position
-                            -> StringEdits Natural input -> StringEdits Natural input
-              finalizeEdits remC inP = mappend . mconcat . replicate (Seq.length $ dfstaConsumes' remC) $ delete inP
-              
-              continueRun :: StringEdits Natural input
-                          -> (DFSTComplement state input output, DFSTComplement state input output) -- ^ Zipper into complement
-                          -> Natural -- ^ Input position
-                          -> Seq (LState state input output, Maybe output)
-                          -> [ ( Seq (LState state input output, Maybe output)
-                               , StringEdits Natural input
-                               , (DFSTComplement state input output, DFSTComplement state input output)
-                               , Natural
-                               )
-                             ]
-              -- ^ Nondeterministically make a single further step, continueing a given run
-              continueRun inEdits (c', remC) inP run = do
-                let
-                  pos :: Natural
-                  -- pos = fromIntegral $ Comp.length c - Comp.length c' -- FIXME: should use length of dfstaProduces
-                  pos = fromIntegral . Seq.length $ dfstaProduces remC stInitial
-                  (c'', step) = Comp.splitAt (pred $ Comp.length c') c' -- TODO: unsafe?
-                  current :: LState state input output
-                  current
-                    | Seq.Empty <- run      = (0, (stInitial, Nothing))
-                    | (_ :> (st, _)) <- run = st
-                  current' :: state
-                  oldIn :: Maybe input
-                  (current', oldIn)
-                    | (_ :> ((_, (st, _)), _)) <- rest
-                    , (_ :> ((_, (_, Just (partialIn, _))), _)) <- partial = (st, Just partialIn)
-                    | (_ :> ((_, (_, Just (partialIn, _))), _)) <- partial = (stInitial, Just partialIn)
-                    | Seq.Empty <- rest = (stInitial, Seq.lookup 0 $ dfstaConsumes' step)
-                    | (_ :> ((_, (st, _)), _)) <- rest = (st, Seq.lookup 0 $ dfstaConsumes' step)
-                    where
-                      (partial, rest) = Seq.spanr (\((_, (_, inp)), _) -> isJust inp) run
-                next' <- trace (show ("next'", pos, focus, run, (current', oldIn), current, dfstaConsumes' step, runDFST' dfst current' (maybe Seq.empty Seq.singleton oldIn) Seq.empty)) . maybeToList . snd $ runDFST' dfst current' (maybe Seq.empty Seq.singleton oldIn) Seq.empty
-                let
-                  outgoing :: LState state input output -> [(LState state input output, Maybe input, Maybe output)]
-                  outgoing current = let go (st, minS) outs acc
-                                           | st == current = Set.foldr (\(st', moutS) -> ((st', minS, moutS) :)) acc outs
-                                           | otherwise     = acc
-                                      in Map.foldrWithKey go [] $ FST.stTransition outFST 
-                  isPreferred :: (LState state input output, Maybe input, Maybe output) -> Bool
-                  isPreferred ((_, (st, Nothing)), _, _) = st == next'
-                  isPreferred (st@(_, (_, Just (inS , _))), _, _) = maybe True (== inS) oldIn && any isPreferred (outgoing st) -- By construction of `outFST`, `outgoing st` is a singleton in this case
-                  (preferred, alternate) = partition isPreferred $ outgoing current
-                  assocEdit :: (LState state input output, Maybe input, Maybe output) -- ^ Transition
-                            -> [ ( (DFSTComplement state input output, DFSTComplement state input output) -- ^ new `(c', remC)`, i.e. complement-zipper `(c', remC)` but with edit applied
-                                 , StringEdits Natural input
-                                 , Natural
-                                 )
-                               ]
-                  assocEdit (_, Just inS, _)
-                    | oldIn == Just inS = [ ((c'', step <> remC), mempty, succ inP) ]
-                    | isJust oldIn      = [ ((c', altStep inS <> remC), insert inP inS, succ inP)
-                                          , ((c'', altStep inS <> remC), replace inP inS, succ inP)
-                                          ]
-                    | otherwise         = [ ((c', altStep inS <> remC), insert inP inS, succ inP) ]
-                  assocEdit (_, Nothing, _) = [((c', remC), mempty, inP)]
-                  altStep :: input -> DFSTComplement state input output
-                  altStep inS = Comp.singleton DFSTAction{..}
-                    where
-                      dfstaConsumes = Seq.singleton inS
-                      runDFSTAction x = runDFST' dfst x (pure inS) Seq.empty
-                  options
-                    | pos `Int.member` focus = preferred ++ alternate
-                    | otherwise              = preferred
-                choice@(next, inS, outS) <- trace (unlines $ show (pretty outFST) : map show options) options
-                ((c3, remC'), inEdits', inP') <- assocEdit choice
-                -- let
-                --   -- | Replace prefix of old complement to reflect current candidate
-                --   -- TODO: smarter?
-                --   (_, ((c3 <>) -> newComplement')) = Comp.splitAt (Comp.length c') c -- TODO: unsafe?
-                --   acc = (run :> (next, outS), inEdits' <> inEdits, newComplement')
-                --   dropSuffix = mconcat (replicate (Seq.length $ dfstaConsumes' c3) $ delete inP')
-                --   fin
-                --     | (trans, inEs, newComplement) <- acc = (trans, dropSuffix <> inEs, newComplement)
-                let
-                  trans = run :> (next, outS)
-                  inEs = inEdits' <> inEdits
-                --   dropSuffix = mconcat (replicate (Seq.length $ dfstaConsumes' c3) $ delete inP')
-                --   fin
-                --     | (trans, inEs) <- acc = (trans, dropSuffix <> inEs, remC')
-                -- bool id (over _BFS $ cons fin) (next `Set.member` FST.stAccept outFST) $ continueRun acc (c3, remC') inP'
-                return (trans, inEs, (c3, remC'), inP')
-              
-      -- Properties of the edits computed are determined mostly by the order candidates are generated below
-      -- (_, inEs, c') <- (\xs -> foldr (\x f -> x `seq` f) listToMaybe xs $ xs) $ traceShowId fragmentIntervals >>= (\x -> (\y@(y1, y2, _) -> traceShow (y1, y2) y) <$> runCandidates x)
-
-      fmap ((,) <$> view _3 <*> view _2) .  listToMaybe $ runCandidates =<< fragmentIntervals
+          outFST = restrictOutput affNewOut $ toFST DFST
+            { stInitial = iState
+            , stTransition
+            , stAccept = Set.fromList $ do
+                fin <- Set.toList $ stAccept `Set.union` Set.map fst (Map.keysSet stTransition)
+                (suffOut, Just fin') <- return $ runDFSTAction' suffix fin
+                guard $ Set.member fin' stAccept
+                guard $ suffOut == dfstaProduces suffix fState
+                return fin
+            }
+      trace (show $ pretty outFST) $ Just ()
+
+      newPath <-
+        let
+          FST{ .. } = outFST
+          detOutgoing :: Maybe (LState state input output) -> [(LState state input output, (Maybe input, Maybe output))]
+          detOutgoing Nothing = concatMap detOutgoing . map Just $ toList stInitial
+          detOutgoing (Just st) = concatMap (\((_, inS), outs) -> map (\(st', outS) -> (st', (inS, outS))) $ toList outs) . Map.toList $ Map.filterWithKey (\(st', _) _ -> st == st') stTransition
+          predicate :: [(LState state input output, (Maybe input, Maybe output))] -> Maybe Bool
+          predicate []
+            | not . Set.null $ Set.intersection stInitial stAccept = Just True
+            | otherwise = Nothing
+          predicate ((lastSt, _) : _)
+            | Set.member lastSt stAccept = Just True
+            | otherwise = Nothing
+        in bfs detOutgoing predicate
+
+      trace (show newPath) $ Just ()
+
+      let oldIn = dfstaConsumes' . Comp.drop (Comp.length suffix) $ Comp.take (Comp.length c - Comp.length prefix) c
+          newIn = Seq.fromList . mapMaybe (\(_st, (inS, _outS)) -> inS) $ reverse newPath
+          inDiff = oldIn `strDiff` newIn
+          diffOffset = fromIntegral . Seq.length $ dfstaConsumes' prefix
+          inDiff' = inDiff & stringEdits . sePos +~ diffOffset
+
+      trace (show (oldIn, newIn, inDiff')) $ Just ()
+
+      let affComp = Comp.fromList [ dfstAction dfst inS | (_st, (Just inS, _outS)) <- newPath ]
+  
+      return (suffix <> affComp <> prefix, inDiff')
 
 strDiff :: forall sym pos. (Eq sym, Integral pos) => Seq sym -> Seq sym -> StringEdits pos sym
 -- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@
@@ -413,6 +355,29 @@ strDiff a b = snd . foldl toEdit (0, mempty) $ (getDiff `on` toList) a b
     toEdit (n, es) (Diff.Both _ _) = (succ n, es)
     toEdit (n, es) (Diff.First _ ) = (n, delete n <> es)
     toEdit (n, es) (Diff.Second c) = (succ n, insert n c <> es)
+
+-- | Generic breadth-first search
+bfs :: forall state transition. Ord state
+    => (Maybe state -> [(state, transition)]) -- ^ Find outgoing edges
+    -> ([(state, transition)] {- ^ Reverse path -} -> Maybe Bool {- ^ Continue search, finish successfully, or abort search on this branch -}) -- ^ Search predicate
+    -> Maybe [(state, transition)] -- ^ Reverse path
+bfs outgoing predicate
+  | Just True  <- emptyRes = Just []
+  | Just False <- emptyRes = Nothing
+  | otherwise = bfs' Set.empty . Seq.fromList . map pure $ outgoing Nothing
+  where
+    emptyRes = predicate []
+    
+    bfs' :: Set state -- ^ Visited states, not to be checked again
+         -> Seq [(state, transition)] -- ^ Search queue of paths to continue
+         -> Maybe [(state, transition)]
+    bfs' _ Seq.Empty = Nothing
+    bfs' visited (c@((lastSt, _) : _) :< cs) = case predicate c of
+      Just True  -> Just c
+      Just False -> bfs' visited cs
+      Nothing -> bfs' visited' $ cs <> Seq.fromList (map (: c) . filter (\(st, _) -> not $ Set.member st visited) . outgoing $ Just lastSt)
+      where
+        visited' = Set.insert lastSt visited
 \end{code}
 \end{comment}
 
@@ -457,5 +422,15 @@ affected (StringEdits es) = Just . toInterval $ go es Map.empty
         myOffset
           | Insert _ _ <- e = pred
           | Delete _   <- e = succ
+
+trace :: String -> a -> a
+{-# NOINLINE trace #-}
+trace str y = flip seq y . unsafePerformIO . withFile "lens.log" AppendMode $ \h ->
+  hPutStrLn h str
+
+traceShowId :: Show a => a -> a
+traceShowId x = trace (show x) x
+  
+  
 \end{code}
 \end{comment}
diff --git a/edit-lens/src/Control/FST.lhs b/edit-lens/src/Control/FST.lhs
index 9aa5341..9357da7 100644
--- a/edit-lens/src/Control/FST.lhs
+++ b/edit-lens/src/Control/FST.lhs
@@ -15,7 +15,7 @@ module Control.FST
   -- * Operations on FSTs
   , productFST, restrictOutput, restrictFST
   -- * Debugging Utilities
-  , liveFST
+  , liveFST, dotFST
   ) where
 
 import Data.Map.Lazy (Map, (!?), (!))
@@ -38,6 +38,11 @@ import Control.Monad.State.Strict
 import Text.PrettyPrint.Leijen (Pretty(..))
 import qualified Text.PrettyPrint.Leijen as PP
 
+import Data.Bool (bool)
+import Data.Monoid ((<>))
+
+import Text.Dot
+
 \end{code}
 \end{comment}
 
@@ -50,7 +55,7 @@ In Haskell lockern wir die Anforderung, dass die Ein- und Ausgabe-Alphabete endl
 Zudem speichern wir die Transitionsrelation als multimap um effiziente lookups von Zustand-Eingabe-Paaren zu ermöglichen.
 
 \begin{code}
-dFSeata FST state input output = FST
+data FST state input output = FST
   { stInitial :: Set state
   , stTransition :: Map (state, Maybe input) (Set (state, Maybe output))
   , stAccept :: Set state
@@ -58,13 +63,56 @@ dFSeata FST state input output = FST
 \end{code}
 \end{defn}
 
+\begin{eg} \label{eg:linebreak}
+  Als wiederkehrendes Beispiel betrachten wir einen Transducer $L_{80} = (\Sigma, \Delta, Q, I, F, E)$, der für ein beliebiges Alphabet $\Sigma \supseteq \{ \text{\tt ' '}, \text{\tt \textbackslash n} \}$ durch Umwandlung zwischen Leerzeichen und Zeilenumbrüchen sicherstellt, dass jede Zeile des Ausgabetextes mindestens 80 Zeichen enthält, jedoch nur an Wortgrenzen umbricht:
+
+  \begin{align*}
+    \Delta & = \Sigma \\
+    Q & = \{ 0, 1, \ldots, 80 \} \\
+    I & = \{ 0 \} \\
+    F & = Q \\
+    E & = \{ (q, \sigma, \sigma, q + 1) \mid q \in Q \mysetminus \{ 80 \}, \sigma \in \Sigma \mysetminus \{ \text{\tt \textbackslash n} \} \} \\
+      & \cup \{ (q, \text{\tt \textbackslash n}, \text{\tt ' '}, q + 1) \mid q \in Q \mysetminus \{ 80 \}, \sigma \in \Sigma \} \\
+      & \cup \{ (80, \text{\tt ' '}, \text{\tt \textbackslash n}, 0), (80, \text{\tt \textbackslash n}, \text{\tt \textbackslash n}, 0) \} \\
+      & \cup \{ (80, \sigma, \sigma, 80) \mid \sigma \in \Sigma \mysetminus \{ \text{\tt ' '}, \text{\tt \textbackslash n} \} \}
+  \end{align*}
+
+  \begin{figure}[p]
+    \centering
+    \begin{tikzpicture}[->,auto,node distance=5cm]
+      \node[initial,state,accepting] (0) {$0$};
+      \node[state,accepting] (1) [right of=0] {$1$};
+      \node[] (rest) [below of=1] {$\ldots$};
+      \node[state,accepting] (i) [right of=rest,xshift=-2cm] {$i$};
+      \node[state,accepting] (si) [below of=rest,yshift=2cm] {$i + 1$};
+      \node[state,accepting] (80) [left of=rest] {$80$};
+
+      \path (0) edge node {$\{ (\sigma, \sigma) \mid \sigma \in \Sigma, \sigma \neq \text{\tt \textbackslash n} \}$} (1)
+            (1) edge [bend left=20] node {$\{ (\sigma, \sigma) \mid \sigma \in \Sigma, \sigma \neq \text{\tt \textbackslash n} \}$} (rest)
+                edge [bend right=20] node [left] {$(\text{\tt \textbackslash n}, \text{\tt ' '})$} (rest)
+            (rest) edge node [below] {$\{ (\sigma, \sigma) \mid \sigma \in \Sigma, \sigma \neq \text{\tt \textbackslash n} \}$} (80)
+                   edge [bend right=20] node [above] {$(\text{\tt \textbackslash n}, \text{\tt ' '})$} (80)
+            (i) edge [bend left=45] node {$\{ (\sigma, \sigma) \mid \sigma \in \Sigma, \sigma \neq \text{\tt \textbackslash n} \}$} (si)
+                edge [bend left=10] node [left] {$(\text{\tt \textbackslash n}, \text{\tt ' '})$} (si)
+            (80) edge [loop below] node [below] {$\{ (\sigma, \sigma) \mid \sigma \in \Sigma, \sigma \neq \text{\tt \textbackslash n}, \sigma \neq \text{\tt ' '} \}$} (80)
+                 edge [bend left=20] node {$(\text{\tt \textbackslash n}, \text{\tt \textbackslash n})$} (0)
+                 edge [bend right=20] node [right] {$(\text{\tt ' '}, \text{\tt \textbackslash n})$} (0);
+
+      \draw[-] (rest)--(i.north);
+      \draw[-] (rest)--(si.west);
+    \end{tikzpicture}
+    \caption{Beispiel \ref{eg:linebreak} dargestellt als Graph}
+  \end{figure}
+\end{eg}
+
 \begin{comment}
 \begin{code}
-instance (Show state, Show input, Show output) => Pretty (FST state input output) where
-  pretty FST{..} = PP.vsep
+instance (Show state, Show input, Show output, Ord state, Ord input, Ord output) => Pretty (FST state input output) where
+  pretty fst@FST{..} = PP.vsep
     [ PP.text "Initial states:" PP.</> PP.hang 2 (list . map (PP.text . show) $ Set.toAscList stInitial)
     , PP.text "State transitions:" PP.<$> PP.indent 2 (PP.vsep
-        [        PP.text (show st)
+        [        PP.text (bool " " "#" $ Set.member st live)
+          PP.<+> PP.text (show st)
           PP.<+> (PP.text "-" PP.<> PP.tupled [label inS, label outS] PP.<> PP.text "→")
           PP.<+> PP.text (show st')
         | ((st, inS), to) <- Map.toList stTransition
@@ -77,9 +125,11 @@ instance (Show state, Show input, Show output) => Pretty (FST state input output
       label = PP.text . maybe "ɛ" show
       list :: [PP.Doc] -> PP.Doc
       list = PP.encloseSep (PP.lbracket PP.<> PP.space) (PP.space PP.<> PP.rbracket) (PP.comma PP.<> PP.space)
+      live = liveFST fst
 \end{code}
 \end{comment}
 
+\begin{defn}[Auswertung von FSTs]
 Wir definieren die Auswertung von finite state transducers induktiv indem wir zunächst angeben wie ein einzelner Auswertungs-Schritt erfolgt.
 
 Hierzu kommentieren wir die Haskell-Implementierung eines Auswertungs-Schritts.
@@ -145,6 +195,7 @@ akzeptierenden Endzustände liegt.
           go (initial, nPath) ncs
 \end{code}
 \end{comment}
+\end{defn}
 
 Es ist gelegentlich nützlich nur die möglichen Ausgaben eines FST auf gegebener
 Eingabe zu bestimmen, wir führen eine Hilfsfunktion auf Basis von
@@ -163,7 +214,7 @@ runFST = fmap (map $ catMaybes . fmap (view _2) . view _2) . runFST'
 \end{comment}
 
 Wir können das Produkt zweier FSTs definieren.
-Intuitiv wollen wir beide FSTs gleichzeitig ausführen und dabei sicherstellen, dass Ein- und Ausgabe der FSTs übereinstimmen\footnote{Da wir $\epsilon$-Transitionen in FSTs erlauben müssen wir uns festlegen wann eine $\epsilon$-Transition übereinstimmt mit einer anderen Transition. Wir definieren, dass $\epsilon$ als Eingabe mit jeder anderen Eingabe (inkl. einem weiteren $\epsilon$) übereinstimmt.}.
+Intuitiv wollen wir beide FSTs gleichzeitig ausführen und dabei sicherstellen, dass Ein- und Ausgabe der FSTs übereinstimmen\footnote{Da wir $\epsilon$-Transitionen in FSTs erlauben müssen wir uns festlegen wann eine $\epsilon$-Transition übereinstimmt mit einer anderen Transition. Wir definieren, dass $\epsilon$ als Eingabe ausschließlich mit $\epsilon$ übereinstimmt.}.
 
 Hierfür berechnen wir das Graphen-Produkt der FSTs:
 
@@ -221,7 +272,7 @@ Hierzu nehmen wir das FST-Produkt mit einem FST, der, ungeachtet der Eingabe, im
 Da die Ausgaben der beiden FSTs übereinstimmen müssen produziert das Produkt mit einem derartigen FST (solange dessen Ausgabe in keinem Sinne von der Eingabe abhängt) die gewünschte Ausgabe.
 
 Zur Konstruktion eines derartigen \emph{Wort-FST}s nehmen wir Indizes im Ausgabe-Wort (natürliche Zahlen) als Zustände.
-Übergänge sind immer entweder der Form $n \rightarrow \text{succ}(n)$, konsumieren keine Eingabe ($\epsilon$) und produzieren als Ausgabe das Zeichen am Index $n$ im Ausgabe-Wort, oder der Form $n \overset{(i, \epsilon)}{\rightarrow} n$, für jedes Eingabesymbol $i$ (um die Unabhängigkeit von der Eingabe sicherzustellen).
+Übergänge sind immer entweder der Form $n \rightarrow \text{succ}(n)$, konsumieren keine Eingabe ($\epsilon$) und produzieren als Ausgabe das Zeichen am Index $n$ im Ausgabe-Wort, oder der Form $n \overset{(\sigma, \epsilon)}{\rightarrow} n$, für jedes Eingabesymbol $\sigma$ (um die Unabhängigkeit von der Eingabe sicherzustellen).
 Weiter ist $0$ initial und $\text{length}(\text{Ausgabe})$ der einzige akzeptierende Endzustand.
 
 \begin{code}
@@ -251,6 +302,35 @@ wordFST inps outs = FST
 \end{code}
 \end{comment}
 
+\begin{eg} \label{eg:w100}
+  Der zum Wort $w = 1\, 2\, \ldots\, 80\, \text{\tt \textbackslash n}\, 81\, \ldots\, 98$ gehörige Wort-FST $W_w = ( \Sigma, \Delta, Q, I, F, E)$ für ein beliebiges Eingabe-Alphabet $\Sigma$ ist:
+
+  \begin{align*}
+    \Delta & = \{ 1, 2, \ldots, 98, \text{\tt \textbackslash n} \} \\
+    Q & = \{ 0, 1, \ldots, 99 \} \\
+    I & = \{ 0 \} \\
+    F & = \{ 99 \} \\
+    E & = \{ (i, \sigma, w_i, i + 1) \mid \sigma \in \Sigma \cup \{ \epsilon \}, i \in Q \mysetminus \{ 99 \} \} \\
+      & \cup \{ (i, \sigma, \epsilon, i) \mid \sigma \in \Sigma \cup \{ \epsilon \}, i \in Q \mysetminus \{ 99 \} \}
+  \end{align*}
+
+  \begin{figure}[p]
+    \centering
+    \begin{tikzpicture}[->,auto,node distance=5cm]
+      \node[initial,state] (0) {$0$};
+      \node[] (rest) [right of=0] {$\ldots$};
+      \node[state,accepting] (99) [right of=rest] {$99$};
+
+      \path (0) edge [loop above] node {$\{(\sigma, \epsilon) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (0)
+                edge node {$\{ (\sigma, 1) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (rest)
+            (rest) edge node {$\{ \sigma, 100 \} \mid \sigma \in \Sigma \cup \{ \epsilon \}$} (99)
+            (99) edge [loop above] node {$\{(\sigma, \epsilon) \mid \sigma \in \Sigma \}$} (99);
+    \end{tikzpicture}
+
+    \caption{Beispiel \ref{eg:w100} dargestellt als Graph}
+  \end{figure}
+\end{eg}
+
 Da \texttt{wordFST} zur Konstruktion eine komprehensive Menge aller Eingabesymbole benötigt verwenden wir im folgenden eine optimierte Variante des Produkts mit einem Wort-FST.
 
 \begin{code}
@@ -258,6 +338,46 @@ restrictOutput :: forall state input output. (Ord state, Ord input, Ord output)
 -- ^ @restrictOutput out@ is equivalent to @productFST (wordFST inps out)@ where @inps@ is a comprehensive set of all input symbols @inp :: input@
 \end{code}
 
+\begin{eg} \label{eg:l80timesw100}
+  Der FST $L_{80}$ aus Beispiel \autoref{eg:linebreak} eingeschränkt auf das Wort $w$ aus Beispiel \autoref{eg:w100} (also $W_w \times L_{80}$) ist:
+
+  \begin{align*}
+    \Sigma^\times & = \{1, 2, \ldots, 99, \text{\tt \textbackslash n}, \text{\tt ' '} \} \\
+    \Delta^\times & = \{1, 2, \ldots, 99, \text{\tt \textbackslash n} \} \\
+    Q^\times & = \{ (\sigma, p) \mid \sigma \in \{ 0_{W_w}, \ldots, 99_{W_w} \}, p \in \{ 0_{L_{80}}, \ldots, 80_{L_{80}} \} \} \\
+    I^\times & = \{ (0_{W_w}, 0_{L_{80}}) \} \\
+    F^\times & = \{ (99_{W_w}, p) \mid p \in \{ 0_{L_{80}}, \ldots, 80_{L_{80}} \} \} \\
+    E^\times & = \{ ((i, q), w_i, w_i, (i + 1, q + 1)) \mid q \in Q \mysetminus \{ 80 \}, i \in Q \mysetminus \{ 99 \} \} \\
+             & \cup \{ ((80, 80), \text{\tt \textbackslash n}, \text{\tt \textbackslash n}, (81, 0)) \}
+  \end{align*}
+
+  \begin{figure}[p]
+    \centering
+    \begin{tikzpicture}[->,auto,node distance=5cm]
+      \node[initial,state] (0) {$0_{W_w}\, 0_{L_{80}}$};
+      \node[] (rest1) [right of=0] {$\ldots$};
+      \node[state] (80) [right of=rest1] {$80_{W_w}\, 80_{L_{80}}$};
+      \node[state] (81) [below of=0] {$81_{W_w}\, 0_{L_{80}}$};
+      \node[] (rest2) [right of=81] {$\ldots$};
+      \node[state,accepting] (99) [right of=rest2] {$99_{W_w}\, 19_{L_{80}}$};
+
+      \path (0) edge node {$(1, 1)$} (rest1)
+            (rest1) edge node {$(80, 80)$} (80)
+            (80) edge node {$(\text{\tt \textbackslash n}, \text{\tt \textbackslash n})$} (81)
+            (81) edge node {$(81, 81)$} (rest2)
+            (rest2) edge node {$(98, 98)$} (99);
+    \end{tikzpicture}
+
+    \caption{Beispiel \ref{eg:l80timesw100} dargestellt als Graph}
+  \end{figure}
+\end{eg}
+
+\begin{rem}
+  Es ist bemerkenswert, dass in Beispiel \ref{eg:l80timesw100} die Zirkuläre Struktur von $L_80$ durch Produkt mit einem Wort verloren geht.
+
+  I.\@A.\@ ist das Produkt eines beliebigen FST mit einem Wort-FST zwar nicht azyklisch, erbt jedoch die lineare Struktur des Wort-FST in dem Sinne, dass Fortschritt in Richtung der akzeptierenden Zustände nur möglich ist indem der $(i, \sigma, w_i, i + 1)$-Klasse von Transitionen des Wort-FSTs gefolgt wird.
+\end{rem}
+  
 \begin{comment}
 \begin{code}
 restrictOutput out FST{..} = FST
@@ -302,18 +422,35 @@ liveFST :: forall state input output. (Ord state, Ord input, Ord output, Show st
 -- ^ Compute the set of "live" states (with no particular complexity)
 --
 -- A state is "live" iff there is a path from it to an accepting state and a path from an initial state to it
-liveFST fst@FST{..} = flip execState Set.empty $ mapM_ (depthSearch Set.empty) stInitial
+liveFST fst@FST{..} = flip execState (Set.empty) . depthSearch Set.empty $ Set.toList stInitial
   where
     stTransition' :: Map state (Set state)
     stTransition' = Map.map (Set.map (\(st, _) -> st)) $ Map.mapKeysWith Set.union (\(st, _) -> st) stTransition
-    depthSearch :: Set state -> state -> State (Set state) ()
-    depthSearch acc curr = do
+    depthSearch :: Set state -> [state] -> State (Set state) ()
+    depthSearch acc [] = return ()
+    depthSearch acc (curr : queue) = do
       let acc' = Set.insert curr acc
           next = fromMaybe Set.empty $ stTransition' !? curr
       alreadyLive <- get
       when (curr `Set.member` Set.union stAccept alreadyLive) $
         modify $ Set.union acc'
-      alreadyLive <- get
-      mapM_ (depthSearch acc') $ next `Set.difference` alreadyLive
+      depthSearch acc' $ filter (not . flip Set.member next) queue ++ Set.toList (next `Set.difference` acc')
+
+dotFST :: forall state input output. (Ord state, Ord input, Ord output, Show state, Show input, Show output) => FST state input output -> Dot ()
+dotFST FST{..} = do
+  let
+    stTransition' = concatMap (\(f, ts) -> (f,) <$> Set.toList ts) $ Map.toList stTransition
+    states = stInitial <> stAccept <> foldMap (Set.singleton . fst . fst) stTransition' <> foldMap (Set.singleton . fst . snd) stTransition'
+  stateIds <- sequence . (flip Map.fromSet) states $ \st -> node
+    [ ("label", show st)
+    , ("peripheries", bool "1" "2" $ st `Set.member` stAccept)
+    ]
+  forM_ stInitial $ \st -> do
+    init <- node [ ("label", ""), ("shape", "none") ]
+    init .->. (stateIds ! st)
+  forM_ stTransition' $ \((f, inS), (t, outS)) -> do
+    edge (stateIds ! f) (stateIds ! t)
+      [ ("label", show (inS, outS))
+      ]
 \end{code}
 \end{comment}
diff --git a/edit-lens/src/Control/FST/Lens.tex b/edit-lens/src/Control/FST/Lens.tex
new file mode 100644
index 0000000..dc44e10
--- /dev/null
+++ b/edit-lens/src/Control/FST/Lens.tex
@@ -0,0 +1,29 @@
+Es stellt sich die Frage, ob das obig beschriebene Verfahren zur Konstruktion einer edit-lens sich auch auf nondeterminische finite state transducers anwenden lässt.
+
+Eine natürlich Erweiterung von \texttt{DFSTAction} wäre:
+\begin{lstlisting}[language=Haskell]
+data FSTAction state input output = FSTAction
+  { runFSTAction :: state -> Map state [Seq output]
+  , fstaConsumes :: Seq input
+  }
+\end{lstlisting}
+wobei die Liste aller möglichen output-Strings in der rechten Seite von \texttt{runFSTAction} in aller Regel unendlich ist.
+
+$\Rrightarrow$ würde sich notwendigerweise arbiträr auf einen der möglichen output-Strings festlegen aber ansonsten wohl identisch zum DFST-Fall implementieren lassen.
+
+$\Lleftarrow$ basiert fundamental darauf im Komplement anhand der erzeugten output-Strings zu suchen (um das betroffene Intervall im output-String auf das Komplement zu übertragen).
+Um sicher zu stellen, dass jene Suche immer terminiert, müsste die Aufzählung der i.A. unendlich vielen zulässigen output-Strings in \texttt{FSTAction} geschickt gewählt sein.
+Quellen von Serien unendlich vieler output-Strings sind notwendigerweise Zykel im betrachteten FST.
+Wir könnten nun für jeden Zykel im betrachteten FST eine Kante arbiträr wählen und dem Folgen jener Kante Kosten zuweisen.
+Wenn wir nun sicherstellen, dass output-Strings in Reihenfolge aufsteigender Kosten aufgezählt werden, lässt sich jeder endliche output-String in endlicher Zeit finden.
+
+Das obig beschriebene Verfahren weißt eine Asymmetrie auf, die im unterliegenden FST nicht vorhanden ist (sowohl Eingabe- als auch Ausgabe-Symbole sind Annotationen vom gleichen Typ an die Transitionen des FST).
+Diese Asymmetrie ergibt sich ausschließlich aus der Wahl des Komplements.
+
+Wählen wir stattdessen ein Komplement, dass Eingabe und Ausgabe symmetrisch behandelt:
+\begin{lstlisting}[language=Haskell]
+newtype FSTAction' state input output = FSTAction'
+  { runFSTAction' :: state -> Map state [Seq input, Seq output]
+  }
+\end{lstlisting}
+So lassen sich $\Rrightarrow^\prime$ und $\Lleftarrow^\prime$ ebenfalls symmetrisch, analog zu $\Lleftarrow$, konstruieren.
diff --git a/edit-lens/src/Control/Lens/Edit.lhs b/edit-lens/src/Control/Lens/Edit.lhs
index 5a106c8..96b2114 100644
--- a/edit-lens/src/Control/Lens/Edit.lhs
+++ b/edit-lens/src/Control/Lens/Edit.lhs
@@ -71,7 +71,7 @@ instance (Module m, Module n) => HasEditLens (EditLens c m n) m n where
 
 Das einschlägige bestehende lens framework \cite{lens} konstruiert seine Linsen alá \citeauthor{laarhoven} wie folgt:
 
-\begin{defn}[lenses alá \citeauthor{laarhoven}]
+\begin{defn}[lenses alá laarhoven]
 Für Typen $n$ und $m$ ist eine \emph{lens} $\ell$ von $n$ in $m$ eine Abbildung\footnote{Gdw. die betrachtete Linse einen Isomorphismus kodiert wird auch über den verwendeten Profunktor anstatt $\to$ quantifiziert} folgender Struktur:
 
 $$ \forall f \, \text{Funktor} \colon \left ( \ell \colon \left ( m \to f(m) \right ) \to \left ( n \to f(n) \right ) \right )$$