mirror of
https://git.cs.ou.nl/joshua.moerman/mealy-decompose.git
synced 2025-06-01 16:37:46 +02:00
Added simultaneous bfs algorithm, not yet tested on a bigger model
This commit is contained in:
parent
a4d97a9d04
commit
ec8a4f0689
5 changed files with 117 additions and 3 deletions
|
@ -11,7 +11,7 @@ build-type: Simple
|
||||||
common stuff
|
common stuff
|
||||||
build-depends:
|
build-depends:
|
||||||
base >= 4.15,
|
base >= 4.15,
|
||||||
containers,
|
containers >= 0.6.8,
|
||||||
unordered-containers,
|
unordered-containers,
|
||||||
data-ordlist,
|
data-ordlist,
|
||||||
megaparsec,
|
megaparsec,
|
||||||
|
@ -37,6 +37,7 @@ library
|
||||||
Merger,
|
Merger,
|
||||||
SplittingTree,
|
SplittingTree,
|
||||||
StateCover.StateCover,
|
StateCover.StateCover,
|
||||||
|
StateCover.Simultaneous,
|
||||||
StateIdentifiers
|
StateIdentifiers
|
||||||
|
|
||||||
executable mealy-decompose-main
|
executable mealy-decompose-main
|
||||||
|
@ -67,4 +68,12 @@ test-suite mealy-decompose-test
|
||||||
main-is: Main.hs
|
main-is: Main.hs
|
||||||
type: exitcode-stdio-1.0
|
type: exitcode-stdio-1.0
|
||||||
build-depends:
|
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
|
||||||
|
|
49
hs/src/StateCover/Simultaneous.hs
Normal file
49
hs/src/StateCover/Simultaneous.hs
Normal file
|
@ -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
|
|
@ -1,3 +1,5 @@
|
||||||
|
-- | Copyright: (c) 2025 Joshua Moerman, Open Universiteit
|
||||||
|
-- SPDX-License-Identifier: EUPL-1.2
|
||||||
module StateCover.StateCover where
|
module StateCover.StateCover where
|
||||||
|
|
||||||
import Data.Functor.Identity (runIdentity)
|
import Data.Functor.Identity (runIdentity)
|
||||||
|
|
|
@ -1,4 +1,7 @@
|
||||||
module Main (main) where
|
module Main (main) where
|
||||||
|
|
||||||
|
import StateCoverTests
|
||||||
|
import Test.Tasty
|
||||||
|
|
||||||
main :: IO ()
|
main :: IO ()
|
||||||
main = putStrLn "Test suite not yet implemented."
|
main = defaultMain (testGroup "" [stateCoverTests])
|
||||||
|
|
51
hs/test/StateCoverTests.hs
Normal file
51
hs/test/StateCoverTests.hs
Normal file
|
@ -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")]]
|
||||||
|
]
|
Loading…
Add table
Reference in a new issue