From ef2ab8a2a2f31955524bffcb3e13448e5fd488b7 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Mon, 23 Sep 2024 16:52:47 +0200 Subject: [PATCH] Some small changes --- app/Main.hs | 32 ++++++++++++++++++-------- src/DotWriter.hs | 55 +++++++++++++++----------------------------- src/SplittingTree.hs | 14 +++++------ 3 files changed, 47 insertions(+), 54 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index 6e0a23d..e44db9d 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -18,17 +18,15 @@ import Data.Maybe (isNothing) import Data.Set qualified as Set import Data.Text qualified as T import Data.Text.IO qualified as T +import Data.Text.Lazy.IO qualified as TL import Data.Tuple (swap) +import Debug.Trace (traceMarkerIO) import System.Environment -- | This functions inverts a map. In the new map the values are lists. converseRelation :: Ord b => Map.Map a b -> Map.Map b [a] converseRelation = Map.fromListWith (++) . fmap (second pure . swap) . Map.assocs --- TODO: use Data.Text here -myWriteFile :: FilePath -> String -> IO () -myWriteFile filename = writeFile ("results/" ++ filename) - main :: IO () main = do -- Read dot file @@ -37,12 +35,16 @@ main = do [x] -> x _ -> error "Please provide exactly one argument (filepath of dot file)" + traceMarkerIO "read input" + putStr "reading " >> putStrLn dotFile machine <- readDotFile dotFile -- print some basic info putStrLn $ (show . length $ states machine) <> " states, " <> (show . length $ inputs machine) <> " inputs and " <> (show . length $ outputs machine) <> " outputs" + traceMarkerIO "start minimisation" + let printPartition p = putStrLn $ "number of states = " <> show (numBlocks p) @@ -55,6 +57,8 @@ main = do printPartition (refineFuns outputFuns reverseFuns (states machine)) putStrLn "" + traceMarkerIO "start minimisation for each component" + -- Then compute each projection let outs = outputs machine @@ -70,6 +74,8 @@ main = do ) projections + traceMarkerIO "component equivalences" + -- First we check for equivalent partitions, so that we skip redundant work. let (equiv, uniqPartitions) = equivalenceClasses comparePartitions projections @@ -86,6 +92,8 @@ main = do ) (Map.assocs equiv) + traceMarkerIO "component lattice" + -- Then we compare each pair of partitions. We only keep the finest -- partitions, since the coarse ones don't provide value to us. let @@ -100,6 +108,8 @@ main = do ) (sortOn (negate . fst) . fmap foo $ topMods) + traceMarkerIO "heuristic merger" + -- Then we try to combine paritions, so that we don't end up with -- too many components. (Which would be too big to be useful.) let strategy MergerStats{..} @@ -110,6 +120,8 @@ main = do print projmap + traceMarkerIO "output" + -- Now we are going to output the components we found. let equivInv = converseRelation equiv @@ -132,10 +144,10 @@ main = do do let filename = "partition_" <> show componentIdx <> ".dot" - content = T.unpack . T.unlines . fmap T.unwords . toBlocks $ p + content = T.unlines . fmap T.unwords . toBlocks $ p putStrLn $ "Output (partition) in file " <> filename - myWriteFile filename content + T.writeFile ("results/" <> filename) content do let @@ -153,7 +165,7 @@ main = do -- Convert to a file filename1 = "component_" <> show componentIdx <> ".dot" - content1 = toString . mealyToDot (T.unpack name) $ initialFirst + content1 = toString . mealyToDot name $ initialFirst -- So far so good, `initialFirst` could serve as our output -- But we do one more optimisation on the machine @@ -164,14 +176,14 @@ main = do -- Convert to a file filename2 = "component_reduced_" <> show componentIdx <> ".dot" - content2 = toString . mealyToDot (T.unpack name) $ result + content2 = toString . mealyToDot name $ result putStrLn $ "Output (reduced machine) in file " <> filename1 - myWriteFile filename1 content1 + TL.writeFile ("results/" <> filename1) content1 putStrLn $ "Dead inputs = " <> show (Set.size deadInputs) putStrLn $ "Output (reduced machine) in file " <> filename2 - myWriteFile filename2 content2 + TL.writeFile ("results/" <> filename2) content2 mapM_ action projmapN diff --git a/src/DotWriter.hs b/src/DotWriter.hs index 8115bc0..8c046b8 100644 --- a/src/DotWriter.hs +++ b/src/DotWriter.hs @@ -1,54 +1,35 @@ +{-# LANGUAGE OverloadedStrings #-} + module DotWriter where -import Data.Monoid (Endo (..)) import Data.Partition (Block (..)) import Data.Text qualified as T +import Data.Text.Lazy qualified as TL +import Data.Text.Lazy.Builder qualified as TB --- TODO: use `Data.Text` here instead of strings - -type StringBuilder = Endo String - -string :: String -> StringBuilder -string = Endo . (++) - -toString :: StringBuilder -> String -toString = flip appEndo [] +toString :: TB.Builder -> TL.Text +toString = TB.toLazyText class ToDot s where - toDot :: s -> StringBuilder - -instance ToDot String where - toDot = string + toDot :: s -> TB.Builder instance ToDot T.Text where - toDot = string . T.unpack + toDot = TB.fromText +-- | Assumes "nil" is not a valid element of `a`. instance ToDot a => ToDot (Maybe a) where - -- should be chosen not to conflict with possible outputs - toDot Nothing = string "nil" + toDot Nothing = "nil" toDot (Just a) = toDot a +-- | Only works for non-negative numbers. instance ToDot Block where - -- only works nicely when non-negative - toDot b = string "s" <> string (show b) + toDot b = "s" <> TB.fromString (show b) -transitionToDot :: (ToDot s, ToDot i, ToDot o) => (s, i, o, s) -> StringBuilder -transitionToDot (s, i, o, t) = - toDot s - <> string " -> " - <> toDot t - <> string " [label=\"" - <> toDot i - <> string " / " - <> toDot o - <> string "\"]" - -mealyToDot :: (ToDot s, ToDot i, ToDot o) => String -> [(s, i, o, s)] -> StringBuilder +-- | Converts a list of transitions to a dot file. +mealyToDot :: (ToDot s, ToDot i, ToDot o) => T.Text -> [(s, i, o, s)] -> TB.Builder mealyToDot name transitions = - string "digraph " - <> string name - <> string " {\n" - <> foldMap transitionToDotSep transitions - <> string "}\n" + "digraph " <> TB.fromText name <> " {\n" <> foldMap transitionToDotSep transitions <> "}\n" where - transitionToDotSep t = string " " <> transitionToDot t <> string "\n" + transitionToDotSep t = " " <> transitionToDot t <> "\n" + transitionToDot (s, i, o, t) = + toDot s <> " -> " <> toDot t <> " [label=\"" <> toDot i <> " / " <> toDot o <> "\"]" diff --git a/src/SplittingTree.hs b/src/SplittingTree.hs index 33cfeb1..eb77571 100644 --- a/src/SplittingTree.hs +++ b/src/SplittingTree.hs @@ -52,36 +52,36 @@ data PRState s i o = PRState deriving (Show) updatePartition :: (Monad m, Ord s) => s -> Block -> StateT (PRState s i o) m () -updatePartition s b = modify foo +updatePartition s b = modify' foo where foo prs = prs{partition = coerce (Map.insert s b) (partition prs)} updateSize :: Monad m => Block -> Int -> StateT (PRState s i o) m Int updateSize b n = - modify (\prs -> prs{splittingTree = (splittingTree prs){size = Map.insert b n (size (splittingTree prs))}}) + modify' (\prs -> prs{splittingTree = (splittingTree prs){size = Map.insert b n (size (splittingTree prs))}}) >> return n genNextBlockId :: Monad m => StateT (PRState s i o) m Block genNextBlockId = do idx <- gets nextBlockId - modify (\prs -> prs{nextBlockId = succ (nextBlockId prs)}) + modify' (\prs -> prs{nextBlockId = succ (nextBlockId prs)}) return idx updateParent :: Monad m => Either Block InnerNode -> InnerNode -> o -> StateT (PRState s i o) m () -updateParent (Left block) target output = modify foo +updateParent (Left block) target output = modify' foo where foo prs = prs{splittingTree = (splittingTree prs){blockParent = Map.insert block (target, output) (blockParent (splittingTree prs))}} -updateParent (Right node) target output = modify foo +updateParent (Right node) target output = modify' foo where foo prs = prs{splittingTree = (splittingTree prs){innerParent = Map.insert node (target, output) (innerParent (splittingTree prs))}} updateLabel :: Monad m => InnerNode -> [i] -> StateT (PRState s i o) m () -updateLabel node witness = modify (\prs -> prs{splittingTree = (splittingTree prs){label = Map.insert node witness (label (splittingTree prs))}}) +updateLabel node witness = modify' (\prs -> prs{splittingTree = (splittingTree prs){label = Map.insert node witness (label (splittingTree prs))}}) genNextNodeId :: Monad m => StateT (PRState s i o) m InnerNode genNextNodeId = do idx <- gets nextNodeId - modify (\prs -> prs{nextNodeId = succ (nextNodeId prs)}) + modify' (\prs -> prs{nextNodeId = succ (nextNodeId prs)}) return idx refineWithSplitter :: (Monad m, Ord o, Ord s) => i -> (s -> [s]) -> Splitter s i o -> StateT (PRState s i o) m [Splitter s i o]