diff --git a/app/Main.hs b/app/Main.hs index f893dd5..7581412 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,6 +1,7 @@ module Main where import DotParser +import DotWriter import Mealy import MealyRefine import Merger @@ -8,13 +9,19 @@ import Partition import Control.Monad (forM_, when) import Control.Monad.Trans.State.Strict -import Data.List (sort) +import Data.Bifunctor +import Data.List (sort, sortOn, intercalate) +import Data.List.Ordered (nubSort) import Data.Map.Strict qualified as Map import Data.Maybe (mapMaybe) import Data.Set qualified as Set +import Data.Tuple (swap) import System.Environment import Text.Megaparsec +converseRelation :: (Ord a, Ord b) => Map.Map a b -> Map.Map b [a] +converseRelation m = Map.fromListWith (++) . fmap (second pure . swap) . Map.assocs $ m + {- Hacked together, you can view the result with: @@ -60,7 +67,7 @@ main = do -- I did some manual preprocessing, these are the only interesting bits let -- outs = ["10", "10-O9", "2.2", "3.0", "3.1", "3.10", "3.12", "3.13", "3.14", "3.16", "3.17", "3.18", "3.19", "3.2", "3.20", "3.21", "3.3", "3.4", "3.6", "3.7", "3.8", "3.9", "5.0", "5.1", "5.12", "5.13", "5.17", "5.2", "5.21", "5.23", "5.6", "5.7", "5.8", "5.9", "quiescence"] outs = outputs machine - projections0 = allProjections machine outs + (projections0, state2idx) = allProjections machine outs projections = zip outs $ fmap refineMealy projections0 -- Print number of states of each projection @@ -144,6 +151,42 @@ main = do projmap <- heuristicMerger topMods strategy - print . fmap fst $ projmap + let equivInv = converseRelation equiv + relMap = Map.fromListWith (++) . fmap (second pure) $ rel + projmapN = zip projmap [1..] + + forM_ projmapN (\((os, p), i) -> do + let name = intercalate "x" os + filename = "component" <> show i <> ".dot" + + osWithRel = concat $ os:[Map.findWithDefault [] o relMap | o <- os] + osWithRelAndEquiv = concat $ osWithRel:[Map.findWithDefault [] o equivInv | o <- osWithRel] + componentOutputs = Set.fromList osWithRelAndEquiv + proj = projectToComponent (flip Set.member componentOutputs) machine + -- Sanity check: compute partition again + partition = refineMealy . mealyMachineToEncoding $ proj + + putStrLn $ "" + putStrLn $ "Component " <> show os + putStrLn $ "Correct? " <> show (comparePartitions p partition) + putStrLn $ "Size = " <> show (numBlocks p) + putStrLn $ "Output in file " <> filename + + let MealyMachine{..} = proj + -- We enumerate all transitions in the full automaton + transitions = [(s, i, o, t) | s <- states, i <- inputs, let (o, t) = behaviour s i] + -- This is the quotient map, from state to block + state2block = blockOfState p . (state2idx Map.!) + -- We apply this to each transition, and then nubSort the duplicates away + transitionsBlocks = nubSort [(state2block s, i, o, state2block t) | (s, i, o, t) <- transitions] + -- The initial state should be first + initialBlock = state2block initialState + -- Sorting on "/= initialBlock" puts the initialBlock in front + initialFirst = sortOn (\(s,_,_,_) -> s /= initialBlock) transitionsBlocks + -- Convert to a file + content = toString . mealyToDot name $ initialFirst + + writeFile filename content + ) return () diff --git a/mealy-decompose.cabal b/mealy-decompose.cabal index 1446b22..8ca3c13 100644 --- a/mealy-decompose.cabal +++ b/mealy-decompose.cabal @@ -26,6 +26,7 @@ library hs-source-dirs: src exposed-modules: DotParser, + DotWriter, Mealy, MealyRefine, Merger, diff --git a/src/DotParser.hs b/src/DotParser.hs index 04548bb..2e17064 100644 --- a/src/DotParser.hs +++ b/src/DotParser.hs @@ -54,6 +54,8 @@ convertToMealy l = MealyMachine , inputs = ins , outputs = outs , behaviour = \s i -> base Map.! (s, i) + , initialState = (\(a,_,_,_) -> a) . head $ l + -- ^ Assumption: first transition in the file belongs to the initial state } where froms = OrdList.nubSort . fmap (\(a,_,_,_) -> a) $ l diff --git a/src/DotWriter.hs b/src/DotWriter.hs new file mode 100644 index 0000000..4d9140b --- /dev/null +++ b/src/DotWriter.hs @@ -0,0 +1,40 @@ +module DotWriter where + +import Data.Monoid (Endo(..)) +import Data.Partition.Common (Block(..)) + +type StringBuilder = Endo String + +string :: String -> StringBuilder +string = Endo . (++) + +toString :: StringBuilder -> String +toString = flip appEndo [] + +class ToDot s where + toDot :: s -> StringBuilder + +instance ToDot String where + toDot = string + +instance ToDot a => ToDot (Maybe a) where + -- should be chosen not to conflict with possible outputs + toDot Nothing = string "nil" + toDot (Just a) = toDot a + +instance ToDot Block where + -- only works nicely when non-negative + toDot (Block n) = string "s" <> string (show n) + +transitionToDot :: (ToDot s, ToDot i, ToDot o) => (s, i, o, s) -> StringBuilder +transitionToDot (s, i, o, t) = + toDot s <> string " -> " <> toDot t + <> string " [label=\"" <> toDot i <> string " / " <> toDot o <> string "\"]" + +mealyToDot :: (ToDot s, ToDot i, ToDot o) => String -> [(s, i, o, s)] -> StringBuilder +mealyToDot name transitions = + string "digraph " <> string name <> string " {\n" + <> foldMap transitionToDotSep transitions + <> string "}\n" + where + transitionToDotSep t = string " " <> transitionToDot t <> string "\n" diff --git a/src/Mealy.hs b/src/Mealy.hs index 0f6a59d..50cdd1a 100644 --- a/src/Mealy.hs +++ b/src/Mealy.hs @@ -5,6 +5,7 @@ data MealyMachine s i o = MealyMachine , inputs :: [i] , outputs :: [o] , behaviour :: s -> i -> (o, s) + , initialState :: s } exampleMM :: MealyMachine String Char String @@ -20,4 +21,5 @@ exampleMM = behaviour "q2" 'b' = ("twee", "q0") behaviour "q1" 'b' = ("vier", "q3") behaviour "q3" 'b' = ("twee", "q1") + initialState = "q0" in MealyMachine {..} diff --git a/src/MealyRefine.hs b/src/MealyRefine.hs index 01f2142..6e7a20f 100644 --- a/src/MealyRefine.hs +++ b/src/MealyRefine.hs @@ -9,25 +9,35 @@ import Copar.Functors.Polynomial (Polynomial, PolyF1(..)) import Copar.RefinementInterface (Label, F1) import Data.Bool (bool) import Data.CoalgebraEncoding (Encoding(..)) +import Data.List.Ordered (nubSort) import Data.Map.Strict qualified as Map import Data.Proxy (Proxy(..)) import Data.Vector qualified import Data.Vector.Unboxed qualified -project :: Eq o => MealyMachine s i o -> o -> MealyMachine s i Bool -project MealyMachine{..} o = MealyMachine - { outputs = [False, True] +project :: Ord u => (o -> u) -> MealyMachine s i o -> MealyMachine s i u +project f MealyMachine{..} = MealyMachine + { outputs = nubSort $ fmap f outputs -- inefficient , behaviour = \s i -> case behaviour s i of - (out, s2) -> (out == o, s2) + (out, s2) -> (f out, s2) , .. } +projectToBit :: Ord o => o -> MealyMachine s i o -> MealyMachine s i Bool +projectToBit o = project (o ==) + +projectToComponent :: Ord o => (o -> Bool) -> MealyMachine s i o -> MealyMachine s i (Maybe o) +projectToComponent oPred = project oMaybe + where oMaybe o + | oPred o = Just o + | otherwise = Nothing + -- We will project to all (relevant) outputs. Since a lot of data is shared -- among those mealy machines, I do this in one function. The static parts -- are converted only once. Only "eStructure" (the state-labels) are different -- for each projection. -allProjections :: (Ord s, Ord i, Eq o) => MealyMachine s i o -> [o] -> [Encoding (Label Polynomial) (F1 Polynomial)] -allProjections MealyMachine{..} outs = fmap mkEncoding outs +allProjections :: (Ord s, Ord i, Eq o) => MealyMachine s i o -> [o] -> ([Encoding (Label Polynomial) (F1 Polynomial)], Map.Map s Int) +allProjections MealyMachine{..} outs = (fmap mkEncoding outs, state2idx) where numStates = length states numInputs = length inputs @@ -49,7 +59,7 @@ allProjections MealyMachine{..} outs = fmap mkEncoding outs ) mkEncoding o = Encoding { eStructure = structure o - , eInitState = Nothing + , eInitState = Nothing -- not needed , eEdgesFrom = edgesFrom , eEdgesLabel = edgesLabel , eEdgesTo = edgesTo diff --git a/src/Partition.hs b/src/Partition.hs index fb1a47b..b528427 100644 --- a/src/Partition.hs +++ b/src/Partition.hs @@ -4,9 +4,9 @@ module Partition ) where import Control.Monad.Trans.State.Strict (runState, get, put) -import Data.Partition (Partition(..), numStates) -import Data.Vector qualified as V import Data.Map.Strict qualified as Map +import Data.Partition (Partition(..), numStates, blockOfState) +import Data.Vector qualified as V import Unsafe.Coerce (unsafeCoerce) -- Returns the coarsest partition which is finer than either input