hs/app/HsiMethod.hs

@@ -1,5 +1,3 @@
-{-# LANGUAGE PartialTypeSignatures #-}
-{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 -- | Copyright: (c) 2024-2025 Joshua Moerman, Open Universiteit
 -- SPDX-License-Identifier: EUPL-1.2
 module HsiMethod where
@@ -10,22 +8,19 @@ import DotParser (readDotFile)
 import Mealy (MealyMachine (..))
 import SplittingTree (initialPRState, refine)
 import StateCover.StateCover (stateCover)
-import StateCover.Simultaneous (simultaneousStateCover)
 import StateIdentifiers (stateIdentifierFor)
 
-import Control.Monad (when, unless)
+import Control.Monad (when)
 import Control.Monad.Trans.State (evalStateT)
 import Data.Map.Strict qualified as Map
 import Options.Applicative
 import System.IO
-import System.Exit (exitSuccess)
-import Data.Functor.Identity (runIdentity)
 
 data Mode = HSI | W
   deriving (Eq, Ord, Show, Read)
 
 data HsiMethodOptions = HsiMethodOptions
-  { filenames :: [FilePath]
+  { filename :: FilePath
   , mode :: Mode
   }
   deriving Show
@@ -33,7 +28,7 @@ data HsiMethodOptions = HsiMethodOptions
 hsiMethodOptionsParser :: Parser HsiMethodOptions
 hsiMethodOptionsParser =
   HsiMethodOptions
-    <$> many (argument str (help "Filename(s) to read (dot format)" <> metavar "FILE"))
+    <$> 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 ()
@@ -41,21 +36,21 @@ mainHsiMethod HsiMethodOptions{..} CommonOptions{..} = do
   let
     logging st x = when verbose (hPutStrLn stderr st >> hPrint stderr x >> hPutStrLn stderr "")
 
-  logging "FILENAME" filenames
+  logging "FILENAME" filename
+  machine <- readDotFile filename
 
-  when (length filenames > 1) $ do
-    compositionalTesting filenames
-    exitSuccess
+  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]
 
-  machine <- readDotFile (head filenames)
-
-  let (partition, splittingTree) = mealyToHsi machine
+  (partition, splittingTree) <- evalStateT (refine (const (pure ())) outputFuns reverseFuns) (initialPRState states)
 
   logging "PARTITION" partition
   logging "TREE" splittingTree
 
   let
-    MealyMachine{..} = machine
     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
@@ -69,50 +64,3 @@ mainHsiMethod HsiMethodOptions{..} CommonOptions{..} = do
   logging "STATE COVER" prefixes
 
   mapM_ print testSuite
-
-  logging "STATS" (length testSuite, sum (fmap length testSuite))
-
-mealyToHsi :: _ -> _
-mealyToHsi MealyMachine{..} =
-  let
-    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]
-    ignore = const (pure ()) -- no debug info
-  in
-    runIdentity $ evalStateT (refine ignore outputFuns reverseFuns) (initialPRState states)
-
-
-
-compositionalTesting :: [FilePath] -> IO ()
-compositionalTesting filenames = do
-  machines <- mapM readDotFile filenames
-
-  unless (all (\m -> inputs m == inputs (head machines)) machines) $ do
-    putStrLn "Warning: different intput sets, currently poorly implemented"
-    return ()
-
-  let
-    inps = inputs (head machines)
-    separatePrefixes m = stateCover (\s -> [((i, o), t) | i <- inputs m, let (o, t) = behaviour m s i]) (initialState m)
-    hsi m = let (partition, splittingTree) = mealyToHsi m in \s -> stateIdentifierFor s partition splittingTree
-    separateTestSuite m =
-      let ps = separatePrefixes m
-          ws = hsi m
-       in Trie.reducePrefixes [px <> sx | s <- states m, let px = ps Map.! s, sx <- Trie.toList (ws s)]
-    testSuiteUnion = Trie.reducePrefixes (concatMap separateTestSuite machines)
-
-    simultaneousPrefixes = simultaneousStateCover [\s i -> Just (snd (behaviour m s i)) | m <- machines] inps (fmap initialState machines)
-    simultaneousTestSuite m ps =
-      let ws = hsi m
-       in Trie.reducePrefixes [px <> sx | s <- states m, let px = ps Map.! s, sx <- Trie.toList (ws s)]
-    testSuiteUnion2 = Trie.reducePrefixes . concat $ zipWith simultaneousTestSuite machines simultaneousPrefixes
-
-
-  -- middle part of test not yet implemented
-
-  putStrLn "\nStats"
-  putStrLn $ "Sep words: " <> show (length testSuiteUnion)
-  putStrLn $ "Sep symbols: " <> show (sum (fmap length testSuiteUnion))
-  putStrLn $ "Com words: " <> show (length testSuiteUnion2)
-  putStrLn $ "Com symbols: " <> show (sum (fmap length testSuiteUnion2))

hs/mealy-decompose.cabal

@@ -11,7 +11,7 @@ build-type:         Simple
 common stuff
   build-depends:
     base >= 4.15,
-    containers >= 0.6.8,
+    containers,
     unordered-containers,
     data-ordlist,
     megaparsec,
@@ -37,7 +37,6 @@ library
     Merger,
     SplittingTree,
     StateCover.StateCover,
-    StateCover.Simultaneous,
     StateIdentifiers
 
 executable mealy-decompose-main
@@ -68,12 +67,4 @@ test-suite mealy-decompose-test
   main-is: Main.hs
   type: exitcode-stdio-1.0
   build-depends:
-    mealy-decompose,
-    tasty,
-    tasty-hunit,
-    tasty-quickcheck
-  other-modules:
-    StateCoverTests
-  default-extensions:
-    PartialTypeSignatures
-  ghc-options: -Wno-incomplete-patterns -Wno-missing-signatures -Wno-orphans -Wno-partial-type-signatures
+    mealy-decompose

hs/src/StateCover/Simultaneous.hs

@@ -1,49 +0,0 @@
-{-# LANGUAGE PartialTypeSignatures #-}
--- | Copyright: (c) 2025 Joshua Moerman, Open Universiteit
--- SPDX-License-Identifier: EUPL-1.2
-module StateCover.Simultaneous where
-
-import Data.Bifunctor (first)
-import Data.Functor.Identity (runIdentity)
-import Data.IntMap.Strict qualified as IntMap
-import Data.IntSet qualified as IntSet
-import Data.List (sortOn)
-import Data.Map.Strict qualified as Map
-
--- | The simultaneous state cover has to "synchronise" on the input labels,
--- and must be deterministic. (It an be partial though.) This type seems
--- to capture that.
-type IGraph s i = s -> i -> Maybe s
-
--- | Just as in "StateCover.StateCover", the queue can be shuffled. Note that
--- the queue is partially ordered by something afterwards, so it is not
--- completely random afterwards.
-type SIReordering m s i = [([(Int, s)], [i])] -> m [([(Int, s)], [i])]
-
--- | Simultaneous BFS. This tries to aim for a great overlap in the
--- prefix-trees for the separate components.
-simultaneousStateCoverM :: (Monad m, Ord s) => SIReordering m s i -> [IGraph s i] -> [i] -> [s] -> m [Map.Map s [i]]
-simultaneousStateCoverM shuff graphs inputs sources = go (IntMap.fromSet (const Map.empty) (IntSet.fromRange (1, numC))) [] [(source, [])]
- where
-  numC = length graphs
-  source = zip [1 .. numC] sources
-  indexedGraphs = IntMap.fromList (zip [1 .. numC] graphs)
-  -- get rid of already visited nodes in the components
-  filtering visited = first (filter (\(i, s) -> s `Map.notMember` (visited IntMap.! i)))
-  -- filter, then shuffle (monadic), then sort on most components first
-  reordering visited ls = sortOn (negate . length . fst) <$> shuff (fmap (filtering visited) ls)
-  -- bfs
-  go visited [] [] = pure . fmap (Map.map reverse) . IntMap.elems $ visited
-  go visited queue2 [] = reordering visited queue2 >>= go visited []
-  go visited queue2 (sss : rest) =
-    case filtering visited sss of
-      ([], _) -> go visited queue2 rest
-      (tt, suffix) ->
-        let
-          newVisited = foldr (\(sidx, s) -> IntMap.adjust (Map.insert s suffix) sidx) visited tt
-          successors = [([(sidx, t) | (sidx, s) <- tt, let g = indexedGraphs IntMap.! sidx, Just t <- [g s l]], l : suffix) | l <- inputs]
-         in
-          go newVisited (successors ++ queue2) rest
-
-simultaneousStateCover :: Ord s => [IGraph s i] -> [i] -> [s] -> [Map.Map s [i]]
-simultaneousStateCover graphs inputs = runIdentity . simultaneousStateCoverM pure graphs inputs

hs/src/StateCover/StateCover.hs

@@ -1,5 +1,3 @@
--- | Copyright: (c) 2025 Joshua Moerman, Open Universiteit
--- SPDX-License-Identifier: EUPL-1.2
 module StateCover.StateCover where
 
 import Data.Functor.Identity (runIdentity)

hs/test/Main.hs

@@ -1,7 +1,4 @@
 module Main (main) where
 
-import StateCoverTests
-import Test.Tasty
-
 main :: IO ()
-main = defaultMain (testGroup "" [stateCoverTests])
+main = putStrLn "Test suite not yet implemented."

hs/test/StateCoverTests.hs

@@ -1,51 +0,0 @@
-{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
-{-# OPTIONS_GHC -Wno-missing-signatures #-}
-
-module StateCoverTests where
-
-import Data.Map.Strict qualified as Map
-import Data.Maybe (mapMaybe)
-import StateCover.Simultaneous
-import StateCover.StateCover
-import Test.Tasty
-import Test.Tasty.HUnit
-
-type PMealy s i o = s -> [((i, o), s)]
-
-g0 :: PMealy Int Char Int
-g0 0 = [(('a', 0), 1)]
-g0 1 = [(('b', 0), 2)]
-g0 2 = [(('c', 0), 0)]
-
-g1 :: PMealy Int Char Int
-g1 0 = [(('a', 0), 1), (('d', 0), 2)]
-g1 1 = [(('b', 0), 2)]
-g1 2 = [(('c', 0), 0)]
-
-c0 :: IGraph Int Char
-c0 0 'x' = Just 0
-c0 0 _ = Just 1
-c0 1 'x' = Just 2
-c0 _ _ = Just 0
-
-c1 :: IGraph Int Char
-c1 0 'y' = Just 0
-c1 0 _ = Just 1
-c1 1 'y' = Just 2
-c1 _ _ = Just 0
-
-conv :: [i] -> IGraph s i -> Graph s i
-conv inputs fun s = mapMaybe (\i -> (i,) <$> fun s i) inputs
-
-stateCoverTests =
-  testGroup
-    "state covers"
-    [ testCase "g0" $ stateCover g0 0 @?= Map.fromList [(0, ""), (1, "a"), (2, "ab")]
-    , testCase "g1" $ stateCover g1 0 @?= Map.fromList [(0, ""), (1, "a"), (2, "d")]
-    , testCase "c0" $ bfs (conv "xyz" c0) 0 @?= Map.fromList [(0, ""), (1, "y"), (2, "xy")]
-    , testCase "c1" $ bfs (conv "xyz" c1) 0 @?= Map.fromList [(0, ""), (1, "x"), (2, "yx")]
-    , testCase "c0" $ bfs (conv "zyx" c0) 0 @?= Map.fromList [(0, ""), (1, "z"), (2, "xz")]
-    , testCase "c1" $ bfs (conv "zyx" c1) 0 @?= Map.fromList [(0, ""), (1, "z"), (2, "yz")]
-    , testCase "simul c0 c1" $ simultaneousStateCover [c0, c1] "xyz" [0, 0] @?= [Map.fromList [(0, ""), (1, "z"), (2, "zx")], Map.fromList [(0, ""), (1, "z"), (2, "zy")]]
-    , testCase "simul c0 c1" $ simultaneousStateCover [c0, c1] "zyx" [0, 0] @?= [Map.fromList [(0, ""), (1, "z"), (2, "zx")], Map.fromList [(0, ""), (1, "z"), (2, "zy")]]
-    ]