From 2b8b79a4318c0029dd8ff4d830700bfd05f6f7e6 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Wed, 26 Jun 2024 09:13:56 +0200 Subject: [PATCH] Refactored and cleaned up some things --- app/Main.hs | 11 ++--- app/Playground.hs | 49 ++++++++++++++++--- fourmolu.yaml | 5 ++ mealy-decompose.cabal | 11 +++-- other/decompose_fsm_optimise.py | 4 -- src/Bisimulation.hs | 30 +----------- src/Data/Partition.hs | 85 +++++++++++++++++++++++++++++++++ src/{ => Data}/Preorder.hs | 32 +++++++------ src/{ => Data}/Trie.hs | 16 +++++-- src/Data/UnionFind.hs | 50 +++++++++++++++++++ src/MealyRefine.hs | 2 +- src/Merger.hs | 2 +- src/Partition.hs | 74 ---------------------------- src/StateIdentifiers.hs | 2 +- 14 files changed, 227 insertions(+), 146 deletions(-) create mode 100644 fourmolu.yaml create mode 100644 src/Data/Partition.hs rename src/{ => Data}/Preorder.hs (88%) rename src/{ => Data}/Trie.hs (70%) create mode 100644 src/Data/UnionFind.hs delete mode 100644 src/Partition.hs diff --git a/app/Main.hs b/app/Main.hs index af47aa1..51f3020 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -8,8 +8,8 @@ import DotWriter import Mealy import MealyRefine import Merger -import Partition -import Preorder +import Data.Partition +import Data.Preorder import Control.Monad (forM_) import Data.Bifunctor @@ -84,8 +84,7 @@ main = do -- First we check for equivalent partitions, so that we skip redundant work. let - preord p1 p2 = toPreorder (comparePartitions p1 p2) - (equiv, uniqPartitions) = equivalenceClasses preord projections + (equiv, uniqPartitions) = equivalenceClasses comparePartitions projections putStrLn "" putStrLn "Representatives" @@ -102,7 +101,7 @@ main = do -- Then we compare each pair of partitions. We only keep the finest -- partitions, since the coarse ones don't provide value to us. let - (topMods, downSets) = maximalElements preord uniqPartitions + (topMods, downSets) = maximalElements comparePartitions uniqPartitions foo (a, b) = (numBlocks b, a) putStrLn "" @@ -144,7 +143,7 @@ main = do let filename = "partition_" <> show componentIdx <> ".dot" idx2State = Map.map head . converseRelation $ state2idx - stateBlocks = fmap (fmap (idx2State Map.!)) . Partition.toBlocks $ partition + stateBlocks = fmap (fmap (idx2State Map.!)) . toBlocks $ partition content = unlines . fmap unwords $ stateBlocks putStrLn $ "Output (partition) in file " <> filename diff --git a/app/Playground.hs b/app/Playground.hs index d19299a..a951428 100644 --- a/app/Playground.hs +++ b/app/Playground.hs @@ -1,17 +1,20 @@ module Main where -import Bisimulation (bisimulation2, empty, equate, equivalent) +import Bisimulation (bisimulation2) +import Data.UnionFind import DotParser (convertToMealy, parseTransFull) import Mealy (MealyMachine (..), outputFunction, transitionFunction) -import SplittingTree (PRState (..), initialPRState, refine) +import Data.Partition (numBlocks) +import SplittingTree (PRState (..), getPartition, initialPRState, refine) import StateIdentifiers (stateIdentifierFor) -import Trie qualified +import Data.Trie qualified as Trie import Control.Monad.Trans.State (execStateT) import Data.List qualified as List import Data.Map.Strict qualified as Map import Data.Maybe (isJust, mapMaybe) import Data.Set qualified as Set +import MealyRefine import System.Environment (getArgs) import Text.Megaparsec (parseMaybe) @@ -21,7 +24,8 @@ main = do case args of ("HSI" : ls) -> mainHSI ls ("InputDecomp" : ls) -> mainInputDecomp ls - _ -> putStrLn "Please provide one of [HSI, InputDecomp]" + ("Refine" : ls) -> mainRefine ls + _ -> putStrLn "Please provide one of [HSI, InputDecomp, Refine]" mainHSI :: [String] -> IO () mainHSI args = case args of @@ -87,9 +91,14 @@ mainInputDecomp args = case args of composition i j = interleavingComposition [i] [j] model bisim i j = let compo = composition i j - in bisimulation2 [i, j] - (outputFunction model) (transitionFunction model) (initialState model) - (outputFunction compo) (transitionFunction compo) (initialState compo) + in bisimulation2 + [i, j] + (outputFunction model) + (transitionFunction model) + (initialState model) + (outputFunction compo) + (transitionFunction compo) + (initialState compo) dependent i j = isJust $ bisim i j dependentPairs = [(i, j) | i <- inputs model, j <- inputs model, j > i, dependent i j] @@ -118,3 +127,29 @@ mainInputDecomp args = case args of 0 -> putStrLn "ERROR" 1 -> putStrLn "INDECOMPOSABLE" n -> putStrLn ("MAYBE DECOMPOSABLE: " ++ show n ++ " classes") + +-- Used to determine whether Copar is faster than SplittingTree (it is). +mainRefine :: [String] -> IO () +mainRefine args = case args of + [dotFile, copar] -> run dotFile (read copar) + _ -> putStrLn "Please provide a dot file and Boolean" + where + run dotFile copar = do + m <- convertToMealy . mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile + putStrLn $ "file parsed, initial state = " <> initialState m + if copar + then runCopar m + else runSplittingTree m + + runCopar m = + let printPartition p = putStrLn $ "Done " <> show (numBlocks p) + in printPartition (refineMealy (mealyMachineToEncoding m)) + + runSplittingTree MealyMachine{..} = do + let + outputFuns = [(i, fun) | i <- inputs, let fun s = fst (behaviour s i)] + reverseTransitionMaps i = Map.fromListWith (++) [(t, [s]) | s <- states, let t = snd (behaviour s i)] + reverseFuns = [(i, fun) | i <- inputs, let mm = reverseTransitionMaps i, let fun s = Map.findWithDefault [] s mm] + + PRState{..} <- execStateT (refine (\_ -> pure ()) outputFuns reverseFuns) (initialPRState states) + putStrLn $ "Done" <> show (Map.size (getPartition partition)) diff --git a/fourmolu.yaml b/fourmolu.yaml new file mode 100644 index 0000000..3a28a98 --- /dev/null +++ b/fourmolu.yaml @@ -0,0 +1,5 @@ +indentation: 2 +haddock-style: single-line +single-constraint-parens: auto +single-deriving-parens: auto +respectful: true diff --git a/mealy-decompose.cabal b/mealy-decompose.cabal index 4eb111e..c987e8c 100644 --- a/mealy-decompose.cabal +++ b/mealy-decompose.cabal @@ -12,7 +12,6 @@ common stuff build-depends: base ^>=4.19.0.0, containers, - copar, data-ordlist, megaparsec, transformers @@ -25,18 +24,20 @@ library hs-source-dirs: src exposed-modules: Bisimulation, + Data.Partition, + Data.Preorder, + Data.Trie, + Data.UnionFind, DotParser, DotWriter, LStar, Mealy, MealyRefine, Merger, - Partition, - Preorder, SplittingTree, - StateIdentifiers, - Trie + StateIdentifiers build-depends: + copar, vector executable mealy-decompose diff --git a/other/decompose_fsm_optimise.py b/other/decompose_fsm_optimise.py index 357083f..bc70dab 100644 --- a/other/decompose_fsm_optimise.py +++ b/other/decompose_fsm_optimise.py @@ -137,10 +137,6 @@ def print_table(cell, rs, cs): print('') -def print_eqrel(rel, xs): - print_table(lambda r, c: 'Y' if rel(r, c) else 'ยท', xs, xs) - - class Progress: def __init__(self, name: str, guess: int): self.reset(name, guess, show=False) diff --git a/src/Bisimulation.hs b/src/Bisimulation.hs index 75ada27..1317587 100644 --- a/src/Bisimulation.hs +++ b/src/Bisimulation.hs @@ -1,37 +1,9 @@ module Bisimulation where +import Data.UnionFind (empty, equivalent, equate) import Data.List (find) -import Data.Map.Strict qualified as Map import Data.Sequence qualified as Seq --- Dit is niet de echte union-find datastructuur (niet erg efficient), --- maar wel simpel en beter dan niks. -newtype UnionFind x = MkUnionFind {unUnionFind :: Map.Map x x} - --- Alle elementen zijn hun eigen klasse, dit geven we aan met Nothing. -empty :: UnionFind x -empty = MkUnionFind Map.empty - --- Omdat we een pure interface hebben, doen we hier geen path-compression. -equivalent :: Ord x => x -> x -> UnionFind x -> Bool -equivalent x y (MkUnionFind m) = root x == root y - where - root z = maybe z root (Map.lookup z m) - --- Hier kunnen we wel path-compression doen. We zouden ook nog een rank --- optimalisatie kunnen (moeten?) doen. Maar dan moeten we meer onthouden. -equate :: Ord x => x -> x -> UnionFind x -> UnionFind x -equate x y (MkUnionFind m1) = - let (rx, m2) = rootCP x m1 rx - (ry, m3) = rootCP y m2 ry - in if rx == ry - then MkUnionFind m3 - else MkUnionFind (Map.insert rx ry m3) - where - rootCP z m r = case Map.lookup z m of - Nothing -> (z, m) - Just w -> Map.insert z r <$> rootCP w m r - -- Bisimulatie in 1 machine bisimulation :: (Eq o, Ord s) => [i] -> (s -> i -> o) -> (s -> i -> s) -> s -> s -> Maybe [i] bisimulation alphabet output transition x y = go (Seq.singleton ([], x, y)) empty diff --git a/src/Data/Partition.hs b/src/Data/Partition.hs new file mode 100644 index 0000000..3b5bb00 --- /dev/null +++ b/src/Data/Partition.hs @@ -0,0 +1,85 @@ +{-# LANGUAGE PackageImports #-} + +module Data.Partition ( + -- $partitions + module Data.Partition, +) where + +import Data.Preorder + +import Control.Monad.Trans.State.Strict (get, put, runState) +import Data.Coerce (coerce) +import Data.Map.Strict qualified as Map +import Data.Partition.Common (Block (..)) +import Data.Vector qualified as V +import "copar" Data.Partition (Partition (..), blockOfState, numStates, toBlocks) + +-- $partitions +-- +-- This module re-exports the `Data.Partition` module from the `copar` library, +-- and adds some additional functions for working with partitions. A partition +-- on a set of type @a@ is represented as a map @a -> `Block`@, where a `Block` +-- is a unique identifier (integer) for a set of elements. +-- +-- In this module, we define +-- +-- * `commonRefinement` to compute the common refinement of two partitions. +-- * `isRefinementOf2` to check if one partition is a refinement of another. +-- * `isEquivalent` to check if two partitions are equal. +-- * `comparePartitions` to compare two partitions in the partition lattice. +-- +-- Partitions form a lattice (the so-called /partition lattice/), where the +-- partial order is given by the refinement relation. We put the finest +-- partition at the top, and the coarsest at the bottom. (This is the opposite +-- of the convection used on wikipedia.) + +-- | Returns the common refinement of two partitions. This is the coarsest +-- partition which is finer than either input, i.e., the lowest upper bound. +commonRefinement :: Partition -> Partition -> Partition +commonRefinement p1 p2 = + let n = numStates p1 + sa1 = (stateAssignment p1 V.!) + sa2 = (stateAssignment p2 V.!) + blockAtIdx i = do + (m, b) <- get + let key = (sa1 i, sa2 i) + case Map.lookup key m of + Just b0 -> return b0 + Nothing -> do + put (Map.insert key b m, succ b) + return b + (vect, (_, nextBlock)) = runState (V.generateM n blockAtIdx) (Map.empty, 0) + in Partition{numBlocks = coerce nextBlock, stateAssignment = vect} + +-- | This function checks whether one partition is a refinement of the other. +-- This function already appears in the `copar` library, but the one here is +-- faster. This function is the same as `>=` in the partition lattice. + +-- Could be made faster by doing what commonRefinement is doing but +-- stopping early. But it's fast enough for now, so I won't bother. +isRefinementOf2 :: Partition -> Partition -> Bool +isRefinementOf2 refined original = comparePartitions refined original == GT' + +-- | Checks whether two partitions are equal as partitions. Note that the `Eq` +-- instance on partitions checks for equality of the state assignments, not +-- whether the partitions are equal as partitions. +isEquivalent :: Partition -> Partition -> Bool +isEquivalent p1 p2 = comparePartitions p1 p2 == EQ' + +-- | Compares two partitions. Returns `EQ'` if the partitions are equal, `GT'` +-- if the first partition is a refinement of the second, `LT'` if the first +-- partition is a coarsening of the second, and `IC'` if the partitions are +-- incomparable. +comparePartitions :: Partition -> Partition -> PartialOrdering +comparePartitions p1 p2 + | p1 == p2 = EQ' + | otherwise = + let glb = commonRefinement p1 p2 + n1 = numBlocks p1 + n2 = numBlocks p2 + n3 = numBlocks glb + in case (n1 == n3, n2 == n3) of + (True, True) -> EQ' + (True, False) -> GT' + (False, True) -> LT' + (False, False) -> IC' diff --git a/src/Preorder.hs b/src/Data/Preorder.hs similarity index 88% rename from src/Preorder.hs rename to src/Data/Preorder.hs index 643dbd1..1dece95 100644 --- a/src/Preorder.hs +++ b/src/Data/Preorder.hs @@ -1,14 +1,6 @@ {-# LANGUAGE PatternSynonyms #-} -module Preorder where - --- \| --- This modules includes some algorithms to deal with preorders. For our use-case --- it could be done efficiently with a single function. But this makes it a bit --- unwieldy. So I have separated it into two functions: --- 1. One function takes a preorder and computes the equivalence classes. --- 2. The second function takes the order into account (now only on the --- representatives of the first function) and returns the "top" elements. +module Data.Preorder where import Control.Monad.Trans.Writer.Lazy (runWriter, tell) import Data.Bifunctor @@ -16,18 +8,30 @@ import Data.Foldable (find) import Data.Map.Strict qualified as Map import Data.Set qualified as Set +-- * Basic types + +-- $moduleDocs +-- This modules includes some algorithms to deal with preorders. For our +-- use-case it could be done efficiently with a single function. But this makes +-- it a bit unwieldy. So I have separated it into two functions: +-- +-- 1. One function takes a preorder and computes the equivalence classes. +-- 2. The second function takes the order into account (now only on the +-- representatives of the first function) and returns the "top" elements. + +-- | The partial order adds one constructor to the `Ordering` data type: the +-- possibility of elements being incomparable. type PartialOrdering = Maybe Ordering pattern EQ', LT', GT', IC' :: PartialOrdering pattern EQ' = Just EQ --- \^ Equivalent (or equal) +-- ^ Equivalent (or equal) pattern LT' = Just LT --- \^ Strictly less than +-- ^ Strictly less than pattern GT' = Just GT --- \^ Strictly greater than +-- ^ Strictly greater than pattern IC' = Nothing - --- \^ Incomparable +-- ^ Incomparable -- | A preorder should satisfy reflexivity and transitivity. It is not assumed -- to be anti-symmetric. diff --git a/src/Trie.hs b/src/Data/Trie.hs similarity index 70% rename from src/Trie.hs rename to src/Data/Trie.hs index 73a9507..3068787 100644 --- a/src/Trie.hs +++ b/src/Data/Trie.hs @@ -1,11 +1,12 @@ -module Trie where +module Data.Trie where import Data.Map.Lazy qualified as Map import Data.Map.Merge.Lazy qualified as Map --- | Trie data structure to store a set of words of type i. Not necessarily +-- | Trie data structure to store a set of words of type @i@. Not necessarily -- the most efficient implementation, but it's fine for our purposes. It can --- be used to remove common prefixes from a set of words. +-- be used to remove common prefixes from a list of words: +-- @`toList` . `fromList` $ ls@. data Trie i = Leaf [i] | Node (Map.Map i (Trie i)) @@ -15,9 +16,11 @@ data Trie i empty :: Trie i empty = Leaf [] +-- | Set with a single word. singleton :: [i] -> Trie i singleton = Leaf +-- | Insert a word into the trie. insert :: Ord i => [i] -> Trie i -> Trie i insert [] t = t insert w (Leaf []) = Leaf w @@ -28,13 +31,18 @@ insert (a : w1) (Leaf (b : w2)) | otherwise = Node (Map.fromList [(a, Leaf w1), (b, Leaf w2)]) insert (a : w1) (Node m) = Node (Map.insertWith union a (Leaf w1) m) +-- | Union of two tries. union :: Ord i => Trie i -> Trie i -> Trie i union (Leaf w) t = insert w t union t (Leaf w) = insert w t union (Node m1) (Node m2) = Node (Map.merge Map.preserveMissing Map.preserveMissing (Map.zipWithMatched (const union)) m1 m2) --- Without common prefixes +-- | Enumerates all words in the trie. Prefixes are not outputted. toList :: Trie i -> [[i]] toList (Leaf w) = [w] toList (Node m) = Map.foldMapWithKey (\a t -> fmap (a :) . toList $ t) m + +-- | Adds all words in the list to a trie. +fromList :: Ord i => [[i]] -> Trie i +fromList = foldr insert empty diff --git a/src/Data/UnionFind.hs b/src/Data/UnionFind.hs new file mode 100644 index 0000000..befb1bd --- /dev/null +++ b/src/Data/UnionFind.hs @@ -0,0 +1,50 @@ +module Data.UnionFind where + +import Data.Map.Strict qualified as Map + +-- | A simple implementation of the Union-Find data structure. It does not have +-- the optimal runtime bounds. Depending on the sequence of actions, the time +-- might take O(n^2). Very simple and purely functional. My design goals: +-- +-- * Pure interface, no state monad. +-- * Generic element type, not restricted to `Int`. +-- * No unnecessary optimisations. +-- * O(1) initialisation, as not all elements are known in advance. +newtype UnionFind x = MkUnionFind {unUnionFind :: Map.Map x x} + +-- The map data structure stores a 'parent' for each element. If an element +-- has no parent, it is the root. If two elements have the same root, they are +-- equivalent. The path-compression optimisation is used to make the tree +-- flatter. + +-- | Initialises the union-find data structure, i.e., all elements disjoint. +-- Runs in O(1). +empty :: UnionFind x +empty = MkUnionFind Map.empty + +-- | Checks whether two elements are equivalent. This functions does not use +-- path-compression, as the interface is pure. +equivalent :: Ord x => x -> x -> UnionFind x -> Bool +equivalent x y (MkUnionFind m) = root x == root y + where + root z = maybe z root (Map.lookup z m) + +-- | Equates two elements, that is make two elements equivalent. This function +-- does use path-compression, so that subsequent calls to `equivalent` are +-- faster. +equate :: Ord x => x -> x -> UnionFind x -> UnionFind x +equate x y (MkUnionFind m1) = + let (rx, m2) = rootCP x m1 rx + (ry, m3) = rootCP y m2 ry + in if rx == ry + then MkUnionFind m3 + else MkUnionFind (Map.insert rx ry m3) + where + rootCP z m r = case Map.lookup z m of + Nothing -> (z, m) + Just w -> Map.insert z r <$> rootCP w m r + +-- We zouden ook nog een rank optimalisatie kunnen (moeten?) doen. Maar dan +-- moeten we meer onthouden. Verder zou ik een functie kunnen maken die +-- een `equivalent` en `equate` combineert, dat kan namelijk wel met pad- +-- compressie. diff --git a/src/MealyRefine.hs b/src/MealyRefine.hs index eda8f95..9c51f96 100644 --- a/src/MealyRefine.hs +++ b/src/MealyRefine.hs @@ -1,7 +1,7 @@ module MealyRefine where import Mealy -import Partition (Partition) +import Data.Partition (Partition) import Control.Monad.ST (runST) import Copar.Algorithm (refine) diff --git a/src/Merger.hs b/src/Merger.hs index abcf058..6024a0b 100644 --- a/src/Merger.hs +++ b/src/Merger.hs @@ -1,6 +1,6 @@ module Merger where -import Partition +import Data.Partition import Control.Monad (replicateM) import Control.Monad.IO.Class (liftIO) diff --git a/src/Partition.hs b/src/Partition.hs deleted file mode 100644 index 15a6212..0000000 --- a/src/Partition.hs +++ /dev/null @@ -1,74 +0,0 @@ -module Partition ( - module Partition, - module Data.Partition, -) where - -import Preorder - -import Control.Monad.Trans.State.Strict (get, put, runState) -import Data.Coerce (coerce) -import Data.Map.Strict qualified as Map -import Data.Partition (Partition (..), blockOfState, numStates, toBlocks) -import Data.Partition.Common (Block (..)) -import Data.Vector qualified as V - --- | Returns the common refinement of two partitions. This is the coarsest --- partition which is finer than either input, i.e., the greatest lower bound. --- (If we put the finest partition on the top, and the coarsest on the bottom.) -commonRefinement :: Partition -> Partition -> Partition -commonRefinement p1 p2 = - let n = numStates p1 - sa1 = (stateAssignment p1 V.!) - sa2 = (stateAssignment p2 V.!) - blockAtIdx i = do - (m, b) <- get - let key = (sa1 i, sa2 i) - case Map.lookup key m of - Just b0 -> return b0 - Nothing -> do - put (Map.insert key b m, succ b) - return b - (vect, (_, nextBlock)) = runState (V.generateM n blockAtIdx) (Map.empty, 0) - in Partition{numBlocks = coerce nextBlock, stateAssignment = vect} - --- Could be made faster by doing what commonRefinement is doing but --- stopping early. This is already much faster than what is in --- the CoPaR library, so I won't bother. -isRefinementOf2 :: Partition -> Partition -> Bool -isRefinementOf2 refined original = comparePartitions refined original == Refinement - --- See comment at isRefinementOf2 -isEquivalent :: Partition -> Partition -> Bool -isEquivalent p1 p2 = comparePartitions p1 p2 == Equivalent - --- Instead of checking whether one partition is a refinement of another AND --- also checking vice versa. We can check the direction at once, computing the --- common refinement only once. It saves some time. -data Comparison - = Equivalent - | Refinement - | Coarsening - | Incomparable - deriving (Eq, Ord, Read, Show, Enum, Bounded) - --- We put the finer partitions above -toPreorder :: Comparison -> PartialOrdering -toPreorder Equivalent = EQ' -toPreorder Refinement = GT' -toPreorder Coarsening = LT' -toPreorder Incomparable = IC' - --- See comment at isRefinementOf2 -comparePartitions :: Partition -> Partition -> Comparison -comparePartitions p1 p2 - | p1 == p2 = Equivalent - | otherwise = - let glb = commonRefinement p1 p2 - n1 = numBlocks p1 - n2 = numBlocks p2 - n3 = numBlocks glb - in case (n1 == n3, n2 == n3) of - (True, True) -> Equivalent - (True, False) -> Refinement - (False, True) -> Coarsening - (False, False) -> Incomparable diff --git a/src/StateIdentifiers.hs b/src/StateIdentifiers.hs index 5c3b9b3..5ad9229 100644 --- a/src/StateIdentifiers.hs +++ b/src/StateIdentifiers.hs @@ -1,7 +1,7 @@ module StateIdentifiers where import SplittingTree -import Trie qualified +import Data.Trie qualified as Trie import Data.Map.Strict qualified as Map