Adds SplittingTree -> StateIdentifiers

app/Playground.hs

@@ -3,6 +3,8 @@ module Main where
 import DotParser ( convertToMealy, parseTransFull )
 import Mealy ( MealyMachine(..) )
 import SplittingTree ( PRState(..), refine, initialPRState )
+import StateIdentifiers ( stateIdentifierFor )
+import Trie qualified as Trie
 
 import Control.Monad.Trans.State ( execStateT )
 import Data.Map.Strict qualified as Map
@@ -23,8 +25,19 @@ main = do
     reverseTransitionMaps i = Map.fromListWith (++) [ (t, [s]) | s <- states, let t = snd (behaviour s i)]
     reverseFuns = [(i, fun) | i <- inputs, let m = reverseTransitionMaps i, let fun s = Map.findWithDefault [] s m]
 
-  tree <- execStateT (refine print outputFuns reverseFuns) (initialPRState states)
+  PRState{..} <- execStateT (refine print outputFuns reverseFuns) (initialPRState states)
 
-  print (partition tree)
+  putStrLn "\nPARTITION"
-  print (splittingTree tree)
+  print partition
 
+  putStrLn "\nTREE"
+  print splittingTree
+
+  let
+    siFor s = stateIdentifierFor s partition splittingTree
+
+  putStrLn "\nHARMONISED STATE IDENTIFIERS"
+  sis <- mapM (\s -> let si = siFor s in print (Trie.toList si) >> return si) states
+
+  putStrLn "\nW-SET"
+  print (Trie.toList . foldr Trie.union Trie.empty $ sis)

mealy-decompose.cabal

@@ -32,7 +32,9 @@ library
     Merger,
     Partition,
     Preorder,
-    SplittingTree
+    SplittingTree,
+    StateIdentifiers,
+    Trie
   build-depends:
     vector
 

src/StateIdentifiers.hs

@@ -0,0 +1,14 @@
+module StateIdentifiers where
+
+import SplittingTree
+import Trie qualified as Trie
+
+import Data.Map.Strict qualified as Map
+
+stateIdentifierFor :: (Ord i, Ord s) => s -> Partition s -> SplittingTree s i o -> Trie.Trie i
+stateIdentifierFor state Partition{..} SplittingTree{..} = go firstNode where
+  firstNode = fst <$> blockParent Map.!? (getPartition Map.! state)
+  getParent n = fst <$> innerParent Map.!? n
+  go Nothing = Trie.empty
+  go (Just n) = Trie.insert (label Map.! n) (go (getParent n))
+

src/Trie.hs

@@ -0,0 +1,40 @@
+module Trie where
+
+import Data.Map.Lazy qualified as Map
+import Data.Map.Merge.Lazy qualified as Map
+
+-- | Trie data structure to store a set of words of type i. Not necessarily
+-- the most efficient implementation, but it's fine for our purposes. It can
+-- be used to remove common prefixes from a set of words.
+data Trie i
+  = Leaf [i]
+  | Node (Map.Map i (Trie i))
+  deriving (Eq, Ord, Read, Show)
+
+-- | The empty word is always included.
+empty :: Trie i
+empty = Leaf []
+
+singleton :: [i] -> Trie i
+singleton = Leaf
+
+insert :: Ord i => [i] -> Trie i -> Trie i
+insert [] t = t
+insert w (Leaf []) = Leaf w
+insert (a:w1) (Leaf (b:w2))
+  | a == b = case insert w1 (Leaf w2) of
+    Leaf w3 -> Leaf (a:w3)
+    node -> Node (Map.singleton a node)
+  | otherwise = Node (Map.fromList [(a, Leaf w1), (b, Leaf w2)])
+insert (a:w1) (Node m) = Node (Map.insertWith union a (Leaf w1) m)
+
+union :: Ord i => Trie i -> Trie i -> Trie i
+union (Leaf w) t = insert w t
+union t (Leaf w) = insert w t
+union (Node m1) (Node m2) =
+  Node (Map.merge Map.preserveMissing Map.preserveMissing (Map.zipWithMatched (const union)) m1 m2)
+
+-- Without common prefixes
+toList :: Trie i -> [[i]]
+toList (Leaf w) = [w]
+toList (Node m) = Map.foldMapWithKey (\a t -> fmap (a:) . toList $ t) m