diff --git a/hs/app/HsiMethod.hs b/hs/app/HsiMethod.hs index 9f8b4ac..7a1f849 100644 --- a/hs/app/HsiMethod.hs +++ b/hs/app/HsiMethod.hs @@ -6,12 +6,18 @@ import Data.Trie qualified as Trie import DotParser (readDotFile) import Mealy (MealyMachine (..)) import SplittingTree (initialPRState, refine) +import StateCover.StateCover (stateCover) import StateIdentifiers (stateIdentifierFor) +import Control.Monad (when) import Control.Monad.Trans.State (evalStateT) import Data.Map.Strict qualified as Map import Options.Applicative +-- TODO: use common options +verbose :: Bool +verbose = False + newtype HsiMethodOptions = HsiMethodOptions { filename :: FilePath } @@ -24,30 +30,41 @@ hsiMethodOptionsParser = mainHsiMethod :: HsiMethodOptions -> IO () mainHsiMethod HsiMethodOptions{..} = do - let dotFile = filename - print dotFile - machine <- readDotFile dotFile + when verbose (print filename) + + machine <- readDotFile filename - -- convert to mealy let MealyMachine{..} = machine outputFuns = [(i, fun) | i <- inputs, let fun s = fst (behaviour s i)] 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] - (partition, splittingTree) <- evalStateT (refine print outputFuns reverseFuns) (initialPRState states) + (partition, splittingTree) <- evalStateT (refine (const (pure ())) outputFuns reverseFuns) (initialPRState states) - putStrLn "\nPARTITION" - print partition + when verbose $ do + putStrLn "\nPARTITION" + print partition - putStrLn "\nTREE" - print splittingTree + putStrLn "\nTREE" + print splittingTree let siFor s = stateIdentifierFor s partition splittingTree + prefixes = stateCover (\s -> [((i, o), t) | i <- inputs, let (o, t) = behaviour s i]) initialState + -- TODO: add middle transition(s) + testSuite = Trie.reducePrefixes [px <> sx | s <- states, let px = prefixes Map.! s, sx <- Trie.toList (siFor s)] - putStrLn "\nHARMONISED STATE IDENTIFIERS" - sis <- mapM (\s -> let si = siFor s in print (Trie.toList si) >> return si) states + when verbose $ do + 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) + putStrLn "\nW-SET" + print (Trie.toList . foldr Trie.union Trie.empty $ sis) + + putStrLn "\nSTATE COVER" + print prefixes + + putStrLn "\nTEST SUITE" + + mapM_ print testSuite diff --git a/hs/mealy-decompose.cabal b/hs/mealy-decompose.cabal index 57002a4..b4ca461 100644 --- a/hs/mealy-decompose.cabal +++ b/hs/mealy-decompose.cabal @@ -36,6 +36,7 @@ library MealyRefine, Merger, SplittingTree, + StateCover.StateCover, StateIdentifiers executable mealy-decompose-main diff --git a/hs/src/Data/Trie.hs b/hs/src/Data/Trie.hs index 3068787..f17ef54 100644 --- a/hs/src/Data/Trie.hs +++ b/hs/src/Data/Trie.hs @@ -46,3 +46,7 @@ toList (Node m) = Map.foldMapWithKey (\a t -> fmap (a :) . toList $ t) m -- | Adds all words in the list to a trie. fromList :: Ord i => [[i]] -> Trie i fromList = foldr insert empty + +-- | Removes all common prefixes in a set of words. +reducePrefixes :: Ord i => [[i]] -> [[i]] +reducePrefixes = toList . fromList diff --git a/hs/src/StateCover/StateCover.hs b/hs/src/StateCover/StateCover.hs new file mode 100644 index 0000000..cd033fc --- /dev/null +++ b/hs/src/StateCover/StateCover.hs @@ -0,0 +1,49 @@ +module StateCover.StateCover where + +import Data.Functor.Identity (runIdentity) +import Data.Map.Strict qualified as Map + +-- | A graph is represented by the neighbours of each node. In principle this +-- can also be used for infinite graphs, but the `bfsM` algorithm cannot +-- handle those. +type Graph s l = s -> [(l, s)] + +-- | The `bfsM` algorithm allows the queue of next elements to be re-ordered, +-- so that e.g. randomisation can be added. The re-ordering happens per level. +-- This means that paths are still minimal (in terms of length). +type ReorderQueue m x = [x] -> m [x] + +-- | Runs a breadth-first search through a graph from a single source. +-- Returns a map of reverse-paths to each node. The paths are reversed by +-- construction. This way the paths can share suffixes and reduce memory. +-- It maintains two queues: +-- +-- * A current queue +-- * And the next queue, of nodes with distance one more +-- +-- The additional function allows the second queue to be sorted or shuffled +-- when the algorithms starts with the next distance. +bfsM :: (Monad m, Ord s) => ReorderQueue m (s, [l]) -> Graph s l -> s -> m (Map.Map s [l]) +bfsM reorder graph source = go Map.empty [] [(source, [])] + where + go visited [] [] = pure visited + go visited queue2 [] = reorder queue2 >>= go visited [] + go visited queue2 ((s, suffix) : rest) + | s `Map.member` visited = go visited queue2 rest + | otherwise = + let + newVisited = Map.insert s suffix visited + successors = [(t, l : suffix) | (l, t) <- graph s, t `Map.notMember` newVisited] + in + -- TODO: do we want this order? Does it matter performance-wise? + go newVisited (successors ++ queue2) rest + +-- | Specialised to not re-ordering the queue. So this performs a very +-- standard breadth-first-search. Note that the resulting paths are reversed. +bfs :: Ord s => Graph s l -> s -> Map.Map s [l] +bfs g = runIdentity . bfsM pure g + +-- | State cover for a Mealy machine. The labels in a Mealy machine are input- +-- output pairs, and for the state cover we only care about the input. +stateCover :: Ord s => Graph s (i, o) -> s -> Map.Map s [i] +stateCover g = Map.map (reverse . fmap fst) . bfs g