diff --git a/app/Main.hs b/app/Main.hs index 35e5eac..fa11877 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -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 ()