1
Fork 0
mirror of https://git.cs.ou.nl/joshua.moerman/mealy-decompose.git synced 2025-04-29 17:57:44 +02:00

More output from Main

This commit is contained in:
Joshua Moerman 2024-03-11 13:21:41 +01:00
parent d19cd9f48f
commit 74f547ed38

View file

@ -22,6 +22,9 @@ 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
myWriteFile :: FilePath -> String -> IO ()
myWriteFile filename content = writeFile ("results/" ++ filename) content
{-
Hacked together, you can view the result with:
@ -115,8 +118,6 @@ main = do
forM_ projmapN (\((os, p), i) -> do
let name = intercalate "x" os
filename = "component" <> show i <> ".dot"
osWithRel = concat $ os:[Map.findWithDefault [] o downSets | o <- os]
osWithRelAndEquiv = concat $ osWithRel:[Map.findWithDefault [] o equivInv | o <- osWithRel]
componentOutputs = Set.fromList osWithRelAndEquiv
@ -128,33 +129,53 @@ main = do
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
(do
let filename = "partition_" <> show i <> ".dot"
idx2State = Map.map head . converseRelation $ state2idx
stateBlocks = fmap (fmap (idx2State Map.!)) . Partition.toBlocks $ partition
content = unlines . fmap (intercalate " ") $ stateBlocks
-- So far so good, `initialFirst` could serve as our output
-- But we do one more optimisation on the machine
-- We remove inputs, on which the machine does nothing
deadInputs0 = Map.fromListWith (++) . fmap (\(s,i,o,t) -> (i, [(s,o,t)])) $ initialFirst
deadInputs = Map.keysSet . Map.filter (all (\(s,o,t) -> s == t && o == Nothing)) $ deadInputs0
result = filter (\(_,i,_,_) -> i `Set.notMember` deadInputs) initialFirst
putStrLn $ "Output (partition) in file " <> filename
myWriteFile filename content
)
-- Convert to a file
content = toString . mealyToDot name $ result
(do
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
putStrLn $ "Dead inputs = " <> show (Set.size deadInputs)
-- Convert to a file
filename1 = "component_" <> show i <> ".dot"
content1 = toString . mealyToDot name $ initialFirst
writeFile filename content
-- So far so good, `initialFirst` could serve as our output
-- But we do one more optimisation on the machine
-- We remove inputs, on which the machine does nothing
deadInputs0 = Map.fromListWith (++) . fmap (\(s,i,o,t) -> (i, [(s,o,t)])) $ initialFirst
deadInputs = Map.keysSet . Map.filter (all (\(s,o,t) -> s == t && o == Nothing)) $ deadInputs0
result = filter (\(_,i,_,_) -> i `Set.notMember` deadInputs) initialFirst
-- Convert to a file
filename2 = "component_reduced_" <> show i <> ".dot"
content2 = toString . mealyToDot name $ result
putStrLn $ "Output (reduced machine) in file " <> filename1
myWriteFile filename1 content1
putStrLn $ "Dead inputs = " <> show (Set.size deadInputs)
putStrLn $ "Output (reduced machine) in file " <> filename2
myWriteFile filename2 content2
)
)
return ()