Put together a prototype to decompose a mealy machine and get show equivalent components and subcomponents

app/Main.hs

@@ -1,8 +1,124 @@
 module Main where
 
-import qualified MyLib (someFunc)
+import DotParser
+import Mealy
+import MyLib
 
+import Control.Monad.IO.Class (liftIO)
+import Control.Monad.Trans.State.Strict
+import Control.Monad (forM_, when)
+import Control.Monad.ST (runST)
+import Copar.Algorithm (refine)
+import Copar.Functors.Polynomial (Polynomial)
+import Data.Map.Strict qualified as Map
+import Data.Maybe (mapMaybe)
+import Data.Partition (isRefinementOf, numBlocks)
+import Data.Proxy (Proxy(..))
+import Data.Semigroup (Arg(..))
+import Data.Set qualified as Set
+import Data.List.Ordered (nubSort)
+import System.Environment
+import Text.Megaparsec
+
+{-
+  Hacked together, you can view the result with:
+
+    tred relation.dot | dot -Tpng -G"rankdir=BT" > relation.png
+
+  tred is the graphviz tool to remove transitive edges. And the rankdir
+  attribute flips the graph upside down.
+-}
 main :: IO ()
 main = do
-  putStrLn "Hello, Haskell!"
-  MyLib.someFunc
+  -- Read dot file
+  [dotFile] <- getArgs
+  print dotFile
+  transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile
+
+  -- convert to mealy
+  let machine = convertToMealy transitions
+
+  -- print some basic info
+  putStrLn $ (show . length $ states machine) <> " states, " <> (show . length $ inputs machine) <> " inputs and " <> (show . length $ outputs machine) <> " outputs"
+  putStrLn "Small sample:"
+  print . take 4 . states $ machine
+  print . take 4 . inputs $ machine
+  print . take 4 . outputs $ machine
+  putStrLn ""
+
+  -- DEBUG OUTPUT
+  -- forM_ (states machine) (\s -> do
+  --   print s
+  --   forM_ (inputs machine) (\i -> do
+  --     putStr "  "
+  --     let (o, t) = behaviour machine s i
+  --     putStrLn $ "--" <> (show i) <> "/" <> (show o) <> "->" <> (show t)
+  --     )
+  --   )
+
+  let printPartition p = putStrLn $ "  number of states = " <> show (numBlocks p)
+
+  -- Minimise input, so we know the actual number of states
+  printPartition (runST $ refine (Proxy @Polynomial) (mealyMachineToEncoding machine) True)
+  putStrLn ""
+
+  -- Then compute each projection
+  let minimiseProjection o = runST $ refine (Proxy @Polynomial) (mealyMachineToEncoding (project machine o)) True
+      outs = outputs machine
+      projections = Map.fromSet minimiseProjection (Set.fromList outs)
+
+  -- Print number of states of each projection
+  forM_ (Map.assocs projections) (\(o, partition) -> do
+    print o
+    printPartition partition
+    putStrLn ""
+    )
+
+  -- Consider all pairs
+  let keys = Map.argSet projections
+      pairs = Set.cartesianProduct keys keys
+      distinctPairs = Set.filter (\(Arg o1 _, Arg o2 _) -> o1 < o2) pairs -- bit inefficient
+
+  -- Check refinement relations for all pairs
+  (equiv, rel) <- flip execStateT (Map.empty, []) $ do
+    forM_ (Map.assocs projections) (\(o1, b1) -> do
+      (repr, _) <- get
+      if o1 `Map.member` repr
+        then do
+          liftIO . putStrLn $ "skip " <> (show o1) <> " |-> " <> (show (repr Map.! o1))
+        else do
+          liftIO $ print o1
+          forM_ (Map.assocs projections) (\(o2, b2) -> do
+            (repr0, _) <- get
+            when (o1 < o2 && o2 `Map.notMember` repr0) $ do
+              case (isRefinementOf b1 b2, isRefinementOf b2 b1) of
+                (True, True) -> do
+                  (repr, ls) <- get
+                  put (Map.insert o2 o1 repr, ls)
+                (True, False) -> do
+                  (repr, ls) <- get
+                  put (repr, (o1, o2):ls)
+                (False, True) -> do
+                  (repr, ls) <- get
+                  put (repr, (o2, o1):ls)
+                (False, False) -> return ()
+
+              -- liftIO $ putStr " vs. "
+              -- liftIO $ print o2
+            )
+      )
+
+  putStrLn ""
+  putStrLn "Equivalences"
+  forM_ (Map.assocs equiv) (\(o2, o1) -> do
+    putStrLn $ "  " <> (show o2) <> " == " <> (show o1)
+    )
+
+  let cleanRel = [(Map.findWithDefault o1 o1 equiv, Map.findWithDefault o2 o2 equiv) | (o1, o2) <- rel]
+  putStrLn ""
+  putStrLn "Relation (smaller points to bigger)"
+  forM_ (nubSort cleanRel) (\(o1, o2) -> do
+    putStrLn $ "  " <> (show o2) <> " -> " <> (show o1)
+    )
+
+  return ()

mealy-decompose.cabal

@@ -11,7 +11,10 @@ build-type:         Simple
 common stuff
   build-depends:
     base ^>=4.19.0.0,
-    containers
+    containers,
+    copar,
+    data-ordlist,
+    megaparsec
   default-language: GHC2021
   default-extensions:
     RecordWildCards
@@ -20,10 +23,12 @@ common stuff
 library
   import: stuff
   hs-source-dirs: src
-  exposed-modules: MyLib
+  exposed-modules:
+    MyLib,
+    Mealy,
+    DotParser
   -- other-modules:
   build-depends:
-    copar,
     vector
 
 executable mealy-decompose
@@ -31,7 +36,8 @@ executable mealy-decompose
   hs-source-dirs: app
   main-is: Main.hs
   build-depends:
-    mealy-decompose
+    mealy-decompose,
+    transformers
 
 test-suite mealy-decompose-test
   import: stuff

src/DotParser.hs

@@ -0,0 +1,63 @@
+module DotParser where
+
+import Data.Char (isAlphaNum)
+import Data.List.Ordered qualified as OrdList
+import Data.Map.Strict qualified as Map
+import Data.Void (Void)
+import Mealy
+import Text.Megaparsec
+import Text.Megaparsec.Char
+import Text.Megaparsec.Char.Lexer qualified as L
+
+{-
+   Parser for Dot files generated by the RERS LearnLib learner. This is not
+   a fully fledged parser. It is specific to our models.
+
+   Really only parses a single transition. We just collect all succesfull
+   transitions. This gives all transitions.
+
+   Usage:
+     transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile
+-}
+
+type Stat = String
+type Input = String
+type Output = String
+type Trans = (Stat, Stat, Input, Output)
+
+type Parser = Parsec Void String
+
+parseTrans :: Parser Trans
+parseTrans = assoc <$> identifier <* symbol "->" <*> identifier <*> brackets parseLabel <* optional (symbol ";")
+  where
+    -- defines whitespace and lexemes
+    sc = L.space space1 empty empty
+    lexeme = L.lexeme sc
+    symbol = L.symbol sc
+    -- state, input, output is any string of alphaNumChar's
+    isAlphaNumExtra c = isAlphaNum c || c == '.' || c == '-'
+    alphaNumCharExtra = satisfy isAlphaNumExtra <?> "alphanumeric character or extra"
+    identifier = lexeme (some alphaNumCharExtra)
+    -- The label has the shape [label="i/o"]
+    brackets = between (symbol "[") (symbol "]")
+    parseLabel = (,) <$> (symbol "label=\"" *> identifier <* symbol "/") <*> (identifier <* symbol "\"")
+    -- re-associate different parts of the parser
+    assoc from to (i, o) = (from, to, i, o)
+
+parseTransFull :: Parser Trans
+parseTransFull = space *> parseTrans <* eof
+
+convertToMealy :: [Trans] -> MealyMachine String String String
+convertToMealy l = MealyMachine
+  { states = states
+  , inputs = ins
+  , outputs = outs
+  , behaviour = \s i -> base Map.! (s, i)
+  }
+  where
+    froms = OrdList.nubSort . fmap (\(a,_,_,_) -> a) $ l
+    tos   = OrdList.nubSort . fmap (\(_,a,_,_) -> a) $ l
+    ins   = OrdList.nubSort . fmap (\(_,_,i,_) -> i) $ l
+    outs  = OrdList.nubSort . fmap (\(_,_,_,o) -> o) $ l
+    states = froms `OrdList.union` tos
+    base = Map.fromList . fmap (\(from, to, i, o) -> ((from, i), (o, to))) $ l

src/Mealy.hs

@@ -0,0 +1,23 @@
+module Mealy where
+
+data MealyMachine s i o = MealyMachine
+  { states :: [s]
+  , inputs :: [i]
+  , outputs :: [o]
+  , behaviour :: s -> i -> (o, s)
+  }
+
+exampleMM :: MealyMachine String Char String
+exampleMM =
+  let states = ["q0", "q1", "q2", "q3"]
+      inputs = ['a', 'b']
+      outputs = ["een", "twee", "drie", "vier"]
+      behaviour "q0" 'a' = ("een", "q1")
+      behaviour "q1" 'a' = ("drie", "q0")
+      behaviour "q2" 'a' = ("een", "q3")
+      behaviour "q3" 'a' = ("drie", "q2")
+      behaviour "q0" 'b' = ("vier", "q2")
+      behaviour "q2" 'b' = ("twee", "q0")
+      behaviour "q1" 'b' = ("vier", "q3")
+      behaviour "q3" 'b' = ("twee", "q1")
+  in MealyMachine {..}

src/MyLib.hs

@@ -1,46 +1,17 @@
 module MyLib where
 
-import Control.Monad (forM)
-import Control.Monad.ST (runST)
-import Copar.Algorithm (refine)
+import Mealy
+
 import Copar.Functors.Polynomial
 import Copar.RefinementInterface (Label, F1)
 import Data.CoalgebraEncoding (Encoding(..))
-import Data.Proxy (Proxy(..))
+import Data.Map.Strict qualified as Map
 import Data.Vector qualified
 import Data.Vector.Unboxed qualified
 
-import Data.Map.Strict qualified as Map
--- import Data.Map.Strict (Map)
-
-import Data.Set qualified as Set
-import Data.Set (Set)
-
-data MealyMachine s i o = MealyMachine
-  { states :: Set s
-  , inputs :: Set i
-  , outputs :: Set o
-  , behaviour :: s -> i -> (o, s)
-  }
-
-exampleMM :: MealyMachine String Char String
-exampleMM =
-  let states = Set.fromList ["q0", "q1", "q2", "q3"]
-      inputs = Set.fromList ['a', 'b']
-      outputs = Set.fromList ["xx", "xy", "yx", "yy"]
-      behaviour "q0" 'a' = ("xx", "q1")
-      behaviour "q1" 'a' = ("yx", "q0")
-      behaviour "q2" 'a' = ("xx", "q3")
-      behaviour "q3" 'a' = ("yx", "q2")
-      behaviour "q0" 'b' = ("xx", "q2")
-      behaviour "q2" 'b' = ("xy", "q0")
-      behaviour "q1" 'b' = ("xx", "q3")
-      behaviour "q3" 'b' = ("xy", "q1")
-  in MealyMachine {..}
-
 project :: Eq o => MealyMachine s i o -> o -> MealyMachine s i Bool
 project MealyMachine{..} o = MealyMachine
-  { outputs = Set.fromList [False, True]
+  { outputs = [False, True]
   , behaviour = \s i -> case behaviour s i of
       (out, s2) -> (out == o, s2)
   , ..
@@ -48,11 +19,11 @@ project MealyMachine{..} o = MealyMachine
 
 mealyMachineToEncoding :: (Ord s, Ord i, Ord o) => MealyMachine s i o -> Encoding (Label Polynomial) (F1 Polynomial)
 mealyMachineToEncoding MealyMachine{..} =
-  let numStates = Set.size states
-      numInputs = Set.size inputs
-      idx2state = Map.fromList $ zip [0..] (Set.toList states)
-      idx2input = Map.fromList $ zip [0..] (Set.toList inputs)
-      out2idx = Map.fromList $ zip (Set.toList outputs) [0..]
+  let numStates = length states
+      numInputs = length inputs
+      idx2state = Map.fromList $ zip [0..] states
+      idx2input = Map.fromList $ zip [0..] inputs
+      out2idx = Map.fromList $ zip outputs [0..]
       eStructure = Data.Vector.generate numStates
         (\s -> PolyF1
           { polyF1Summand = 0 -- There is only one summand
@@ -62,24 +33,10 @@ mealyMachineToEncoding MealyMachine{..} =
           }
         )
       eInitState = Nothing
-      state2idx = Map.fromList $ zip (Set.toList states) [0..]
+      state2idx = Map.fromList $ zip states [0..]
       stateInputIndex n = n `divMod` numInputs
       -- stateInputPair (s, i) = s * numInputs + i
       eEdgesFrom = Data.Vector.Unboxed.generate (numStates * numInputs) (fst . stateInputIndex)
       eEdgesLabel = Data.Vector.generate (numStates * numInputs) (snd . stateInputIndex)
       eEdgesTo = Data.Vector.Unboxed.generate (numStates * numInputs) ((state2idx Map.!) . snd . (\(s, i) -> behaviour (idx2state Map.! s) (idx2input Map.! i)) . stateInputIndex)
   in Encoding { .. }
-
-someFunc :: IO ()
-someFunc = do
-  let blocks = runST $ refine (Proxy @Polynomial) (mealyMachineToEncoding exampleMM) True
-  print blocks
-
-  forM ["xx", "xy", "yx", "yy"] (\o -> do
-    print o
-    let blocks = runST $ refine (Proxy @Polynomial) (mealyMachineToEncoding (project exampleMM o)) True
-    print blocks
-    )
-
-  print "Bye"
-