From 7205f298270299e9554141261a5abc6f3e00f053 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Tue, 12 Mar 2024 09:48:50 +0100 Subject: [PATCH] Adds SplittingTree -> StateIdentifiers --- app/Playground.hs | 19 ++++++++++++++++--- mealy-decompose.cabal | 4 +++- src/StateIdentifiers.hs | 14 ++++++++++++++ src/Trie.hs | 40 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 73 insertions(+), 4 deletions(-) create mode 100644 src/StateIdentifiers.hs create mode 100644 src/Trie.hs diff --git a/app/Playground.hs b/app/Playground.hs index 71080a6..ef1d12f 100644 --- a/app/Playground.hs +++ b/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) - print (splittingTree tree) + putStrLn "\nPARTITION" + 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) diff --git a/mealy-decompose.cabal b/mealy-decompose.cabal index a6d872b..2809f35 100644 --- a/mealy-decompose.cabal +++ b/mealy-decompose.cabal @@ -32,7 +32,9 @@ library Merger, Partition, Preorder, - SplittingTree + SplittingTree, + StateIdentifiers, + Trie build-depends: vector diff --git a/src/StateIdentifiers.hs b/src/StateIdentifiers.hs new file mode 100644 index 0000000..85a7ca6 --- /dev/null +++ b/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)) + diff --git a/src/Trie.hs b/src/Trie.hs new file mode 100644 index 0000000..743499d --- /dev/null +++ b/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