hs/app/HsiMethod.hs

@@ -1,27 +1,19 @@
 -- | 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
 
-data Mode = HSI | W
+newtype HsiMethodOptions = HsiMethodOptions
-  deriving (Eq, Ord, Show, Read)
-
-data HsiMethodOptions = HsiMethodOptions
   { filename :: FilePath
-  , mode :: Mode
   }
   deriving Show
 
@@ -29,38 +21,33 @@ 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 -> CommonOptions -> IO ()
+mainHsiMethod :: HsiMethodOptions -> IO ()
-mainHsiMethod HsiMethodOptions{..} CommonOptions{..} = do
+mainHsiMethod HsiMethodOptions{..} = do
-  let
+  let dotFile = filename
-    logging st x = when verbose (hPutStrLn stderr st >> hPrint stderr x >> hPutStrLn stderr "")
+  print dotFile
-
+  machine <- readDotFile dotFile
-  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 (const (pure ())) outputFuns reverseFuns) (initialPRState states)
+  (partition, splittingTree) <- evalStateT (refine print outputFuns reverseFuns) (initialPRState states)
 
-  logging "PARTITION" partition
+  putStrLn "\nPARTITION"
-  logging "TREE" splittingTree
+  print partition
+
+  putStrLn "\nTREE"
+  print 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]
 
-  logging "HARMONISED STATE IDENTIFIERS" [(s, Trie.toList (siFor s)) | s <- states]
+  putStrLn "\nHARMONISED STATE IDENTIFIERS"
-  logging "W-SET" wset
+  sis <- mapM (\s -> let si = siFor s in print (Trie.toList si) >> return si) states
-  logging "STATE COVER" prefixes
 
-  mapM_ print testSuite
+  putStrLn "\nW-SET"
+  print (Trie.toList . foldr Trie.union Trie.empty $ sis)

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 commonOptions
+    HsiMethod options -> mainHsiMethod options
     LStar options -> mainLStar options
     RandomGen options -> mainRandomGen options
 

hs/mealy-decompose.cabal

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

hs/src/Data/Trie.hs

@@ -46,7 +46,3 @@ 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

@@ -1,49 +0,0 @@
-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