hsi and w method (almost)

hs/app/HsiMethod.hs

@@ -1,19 +1,27 @@
 -- | Copyright: (c) 2024-2025 Joshua Moerman, Open Universiteit
--- SPDX-License-Identifier: EUPL-1.2]
+-- SPDX-License-Identifier: EUPL-1.2
 module HsiMethod where
 
+import CommonOptions
 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
+import System.IO
 
-newtype HsiMethodOptions = HsiMethodOptions
+data Mode = HSI | W
+  deriving (Eq, Ord, Show, Read)
+
+data HsiMethodOptions = HsiMethodOptions
   { filename :: FilePath
+  , mode :: Mode
   }
   deriving Show
 
@@ -21,33 +29,38 @@ hsiMethodOptionsParser :: Parser HsiMethodOptions
 hsiMethodOptionsParser =
   HsiMethodOptions
     <$> argument str (help "Filename to read (dot format)" <> metavar "FILE")
+    <*> option auto (long "mode" <> help "Mode (HSI, W)" <> metavar "MODE" <> showDefault <> value HSI)
 
-mainHsiMethod :: HsiMethodOptions -> IO ()
-mainHsiMethod HsiMethodOptions{..} = do
-  let dotFile = filename
-  print dotFile
-  machine <- readDotFile dotFile
+mainHsiMethod :: HsiMethodOptions -> CommonOptions -> IO ()
+mainHsiMethod HsiMethodOptions{..} CommonOptions{..} = do
+  let
+    logging st x = when verbose (hPutStrLn stderr st >> hPrint stderr x >> hPutStrLn stderr "")
+
+  logging "FILENAME" 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
-
-  putStrLn "\nTREE"
-  print splittingTree
+  logging "PARTITION" partition
+  logging "TREE" splittingTree
 
   let
     siFor s = stateIdentifierFor s partition splittingTree
+    wset = Trie.toList . foldr (Trie.union . siFor) Trie.empty $ states
+    prefixes = stateCover (\s -> [((i, o), t) | i <- inputs, let (o, t) = behaviour s i]) initialState
+    -- TODO: add middle transition(s)
+    testSuite = case mode of
+      HSI -> Trie.reducePrefixes [px <> sx | s <- states, let px = prefixes Map.! s, sx <- Trie.toList (siFor s)]
+      W -> Trie.reducePrefixes [prefixes Map.! s <> sx | s <- states, sx <- wset]
 
-  putStrLn "\nHARMONISED STATE IDENTIFIERS"
-  sis <- mapM (\s -> let si = siFor s in print (Trie.toList si) >> return si) states
+  logging "HARMONISED STATE IDENTIFIERS" [(s, Trie.toList (siFor s)) | s <- states]
+  logging "W-SET" wset
+  logging "STATE COVER" prefixes
 
-  putStrLn "\nW-SET"
-  print (Trie.toList . foldr Trie.union Trie.empty $ sis)
+  mapM_ print testSuite

hs/app/Main.hs

@@ -29,7 +29,7 @@ main = do
     DecomposeOutput options -> mainDecomposeOutput options commonOptions
     DecomposeInput options -> mainDecomposeInput options commonOptions
     DecomposeTemp options -> mainDecomposeTemp options
-    HsiMethod options -> mainHsiMethod options
+    HsiMethod options -> mainHsiMethod options commonOptions
     LStar options -> mainLStar options
     RandomGen options -> mainRandomGen options
 

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