Tool can now output mealy machines as well

app/Main.hs

@@ -1,6 +1,7 @@
 module Main where
 
 import DotParser
+import DotWriter
 import Mealy
 import MealyRefine
 import Merger
@@ -8,13 +9,19 @@ import Partition
 
 import Control.Monad (forM_, when)
 import Control.Monad.Trans.State.Strict
-import Data.List (sort)
+import Data.Bifunctor
+import Data.List (sort, sortOn, intercalate)
+import Data.List.Ordered (nubSort)
 import Data.Map.Strict qualified as Map
 import Data.Maybe (mapMaybe)
 import Data.Set qualified as Set
+import Data.Tuple (swap)
 import System.Environment
 import Text.Megaparsec
 
+converseRelation :: (Ord a, Ord b) => Map.Map a b -> Map.Map b [a]
+converseRelation m = Map.fromListWith (++) . fmap (second pure . swap) . Map.assocs $ m
+
 {-
   Hacked together, you can view the result with:
 
@@ -60,7 +67,7 @@ main = do
   -- I did some manual preprocessing, these are the only interesting bits
   let -- outs = ["10", "10-O9", "2.2", "3.0", "3.1", "3.10", "3.12", "3.13", "3.14", "3.16", "3.17", "3.18", "3.19", "3.2", "3.20", "3.21", "3.3", "3.4", "3.6", "3.7", "3.8", "3.9", "5.0", "5.1", "5.12", "5.13", "5.17", "5.2", "5.21", "5.23", "5.6", "5.7", "5.8", "5.9", "quiescence"]
       outs = outputs machine
-      projections0 = allProjections machine outs
+      (projections0, state2idx) = allProjections machine outs
       projections = zip outs $ fmap refineMealy projections0
 
   -- Print number of states of each projection
@@ -144,6 +151,42 @@ main = do
 
   projmap <- heuristicMerger topMods strategy
 
-  print . fmap fst $ projmap
+  let equivInv = converseRelation equiv
+      relMap = Map.fromListWith (++) . fmap (second pure) $ rel
+      projmapN = zip projmap [1..]
+
+  forM_ projmapN (\((os, p), i) -> do
+    let name = intercalate "x" os
+        filename = "component" <> show i <> ".dot"
+
+        osWithRel = concat $ os:[Map.findWithDefault [] o relMap | o <- os]
+        osWithRelAndEquiv = concat $ osWithRel:[Map.findWithDefault [] o equivInv | o <- osWithRel]
+        componentOutputs = Set.fromList osWithRelAndEquiv
+        proj = projectToComponent (flip Set.member componentOutputs) machine
+        -- Sanity check: compute partition again
+        partition = refineMealy . mealyMachineToEncoding $ proj
+
+    putStrLn $ ""
+    putStrLn $ "Component " <> show os
+    putStrLn $ "Correct? " <> show (comparePartitions p partition)
+    putStrLn $ "Size = " <> show (numBlocks p)
+    putStrLn $ "Output in file " <> filename
+
+    let MealyMachine{..} = proj
+        -- We enumerate all transitions in the full automaton
+        transitions = [(s, i, o, t) | s <- states, i <- inputs, let (o, t) = behaviour s i]
+        -- This is the quotient map, from state to block
+        state2block = blockOfState p . (state2idx Map.!)
+        -- We apply this to each transition, and then nubSort the duplicates away
+        transitionsBlocks = nubSort [(state2block s, i, o, state2block t) | (s, i, o, t) <- transitions]
+        -- The initial state should be first
+        initialBlock = state2block initialState
+        -- Sorting on "/= initialBlock" puts the initialBlock in front
+        initialFirst = sortOn (\(s,_,_,_) -> s /= initialBlock) transitionsBlocks
+        -- Convert to a file
+        content = toString . mealyToDot name $ initialFirst
+
+    writeFile filename content
+    )
 
   return ()

mealy-decompose.cabal

@@ -26,6 +26,7 @@ library
   hs-source-dirs: src
   exposed-modules:
     DotParser,
+    DotWriter,
     Mealy,
     MealyRefine,
     Merger,

src/DotParser.hs

@@ -54,6 +54,8 @@ convertToMealy l = MealyMachine
   , inputs = ins
   , outputs = outs
   , behaviour = \s i -> base Map.! (s, i)
+  , initialState = (\(a,_,_,_) -> a) . head $ l
+  -- ^ Assumption: first transition in the file belongs to the initial state
   }
   where
     froms = OrdList.nubSort . fmap (\(a,_,_,_) -> a) $ l

src/DotWriter.hs

@@ -0,0 +1,40 @@
+module DotWriter where
+
+import Data.Monoid (Endo(..))
+import Data.Partition.Common (Block(..))
+
+type StringBuilder = Endo String
+
+string :: String -> StringBuilder
+string = Endo . (++)
+
+toString :: StringBuilder -> String
+toString = flip appEndo []
+
+class ToDot s where
+  toDot :: s -> StringBuilder
+
+instance ToDot String where
+  toDot = string
+
+instance ToDot a => ToDot (Maybe a) where
+  -- should be chosen not to conflict with possible outputs
+  toDot Nothing = string "nil"
+  toDot (Just a) = toDot a
+
+instance ToDot Block where
+  -- only works nicely when non-negative
+  toDot (Block n) = string "s" <> string (show n)
+
+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
+mealyToDot name transitions =
+  string "digraph " <> string name <> string " {\n"
+  <> foldMap transitionToDotSep transitions
+  <> string "}\n"
+  where
+    transitionToDotSep t = string "  " <> transitionToDot t <> string "\n"

src/Mealy.hs

@@ -5,6 +5,7 @@ data MealyMachine s i o = MealyMachine
   , inputs :: [i]
   , outputs :: [o]
   , behaviour :: s -> i -> (o, s)
+  , initialState :: s
   }
 
 exampleMM :: MealyMachine String Char String
@@ -20,4 +21,5 @@ exampleMM =
       behaviour "q2" 'b' = ("twee", "q0")
       behaviour "q1" 'b' = ("vier", "q3")
       behaviour "q3" 'b' = ("twee", "q1")
+      initialState = "q0"
   in MealyMachine {..}

src/MealyRefine.hs

@@ -9,25 +9,35 @@ import Copar.Functors.Polynomial (Polynomial, PolyF1(..))
 import Copar.RefinementInterface (Label, F1)
 import Data.Bool (bool)
 import Data.CoalgebraEncoding (Encoding(..))
+import Data.List.Ordered (nubSort)
 import Data.Map.Strict qualified as Map
 import Data.Proxy (Proxy(..))
 import Data.Vector qualified
 import Data.Vector.Unboxed qualified
 
-project :: Eq o => MealyMachine s i o -> o -> MealyMachine s i Bool
-project MealyMachine{..} o = MealyMachine
-  { outputs = [False, True]
+project :: Ord u => (o -> u) -> MealyMachine s i o -> MealyMachine s i u
+project f MealyMachine{..} = MealyMachine
+  { outputs = nubSort $ fmap f outputs -- inefficient
   , behaviour = \s i -> case behaviour s i of
-      (out, s2) -> (out == o, s2)
+      (out, s2) -> (f out, s2)
   , ..
   }
 
+projectToBit :: Ord o => o -> MealyMachine s i o -> MealyMachine s i Bool
+projectToBit o = project (o ==)
+
+projectToComponent :: Ord o => (o -> Bool) -> MealyMachine s i o -> MealyMachine s i (Maybe o)
+projectToComponent oPred = project oMaybe
+  where oMaybe o
+          | oPred o = Just o
+          | otherwise = Nothing
+
 -- We will project to all (relevant) outputs. Since a lot of data is shared
 -- among those mealy machines, I do this in one function. The static parts
 -- are converted only once. Only "eStructure" (the state-labels) are different
 -- for each projection.
-allProjections :: (Ord s, Ord i, Eq o) => MealyMachine s i o -> [o] -> [Encoding (Label Polynomial) (F1 Polynomial)]
-allProjections MealyMachine{..} outs = fmap mkEncoding outs
+allProjections :: (Ord s, Ord i, Eq o) => MealyMachine s i o -> [o] -> ([Encoding (Label Polynomial) (F1 Polynomial)], Map.Map s Int)
+allProjections MealyMachine{..} outs = (fmap mkEncoding outs, state2idx)
   where
     numStates = length states
     numInputs = length inputs
@@ -49,7 +59,7 @@ allProjections MealyMachine{..} outs = fmap mkEncoding outs
       )
     mkEncoding o = Encoding
       { eStructure = structure o
-      , eInitState = Nothing
+      , eInitState = Nothing -- not needed
       , eEdgesFrom = edgesFrom
       , eEdgesLabel = edgesLabel
       , eEdgesTo = edgesTo

src/Partition.hs

@@ -4,9 +4,9 @@ module Partition
   ) where
 
 import Control.Monad.Trans.State.Strict (runState, get, put)
-import Data.Partition (Partition(..), numStates)
-import Data.Vector qualified as V
 import Data.Map.Strict qualified as Map
+import Data.Partition (Partition(..), numStates, blockOfState)
+import Data.Vector qualified as V
 import Unsafe.Coerce (unsafeCoerce)
 
 -- Returns the coarsest partition which is finer than either input