From ec8a4f0689ac73898ae078ec918d58e093a3dba7 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Wed, 7 May 2025 15:12:12 +0200 Subject: [PATCH] Added simultaneous bfs algorithm, not yet tested on a bigger model --- hs/mealy-decompose.cabal | 13 ++++++-- hs/src/StateCover/Simultaneous.hs | 49 +++++++++++++++++++++++++++++ hs/src/StateCover/StateCover.hs | 2 ++ hs/test/Main.hs | 5 ++- hs/test/StateCoverTests.hs | 51 +++++++++++++++++++++++++++++++ 5 files changed, 117 insertions(+), 3 deletions(-) create mode 100644 hs/src/StateCover/Simultaneous.hs create mode 100644 hs/test/StateCoverTests.hs diff --git a/hs/mealy-decompose.cabal b/hs/mealy-decompose.cabal index b4ca461..a69ffe8 100644 --- a/hs/mealy-decompose.cabal +++ b/hs/mealy-decompose.cabal @@ -11,7 +11,7 @@ build-type: Simple common stuff build-depends: base >= 4.15, - containers, + containers >= 0.6.8, unordered-containers, data-ordlist, megaparsec, @@ -37,6 +37,7 @@ library Merger, SplittingTree, StateCover.StateCover, + StateCover.Simultaneous, StateIdentifiers executable mealy-decompose-main @@ -67,4 +68,12 @@ test-suite mealy-decompose-test main-is: Main.hs type: exitcode-stdio-1.0 build-depends: - mealy-decompose + 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 diff --git a/hs/src/StateCover/Simultaneous.hs b/hs/src/StateCover/Simultaneous.hs new file mode 100644 index 0000000..b24380e --- /dev/null +++ b/hs/src/StateCover/Simultaneous.hs @@ -0,0 +1,49 @@ +{-# 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 diff --git a/hs/src/StateCover/StateCover.hs b/hs/src/StateCover/StateCover.hs index cd033fc..b31c320 100644 --- a/hs/src/StateCover/StateCover.hs +++ b/hs/src/StateCover/StateCover.hs @@ -1,3 +1,5 @@ +-- | Copyright: (c) 2025 Joshua Moerman, Open Universiteit +-- SPDX-License-Identifier: EUPL-1.2 module StateCover.StateCover where import Data.Functor.Identity (runIdentity) diff --git a/hs/test/Main.hs b/hs/test/Main.hs index 3e2059e..ddc1d2a 100644 --- a/hs/test/Main.hs +++ b/hs/test/Main.hs @@ -1,4 +1,7 @@ module Main (main) where +import StateCoverTests +import Test.Tasty + main :: IO () -main = putStrLn "Test suite not yet implemented." +main = defaultMain (testGroup "" [stateCoverTests]) diff --git a/hs/test/StateCoverTests.hs b/hs/test/StateCoverTests.hs new file mode 100644 index 0000000..780ba45 --- /dev/null +++ b/hs/test/StateCoverTests.hs @@ -0,0 +1,51 @@ +{-# 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")]] + ]