1 files changed, 149 insertions, 12 deletions

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}