Addded state cover to hsi method

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

hs/mealy-decompose.cabal

@@ -36,6 +36,7 @@ library
     MealyRefine,
     Merger,
     SplittingTree,
+    StateCover.StateCover,
     StateIdentifiers
 
 executable mealy-decompose-main

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

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