From 7a8591f002741e3cd33ba1a393879ac129f0f43f Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Fri, 18 Jan 2019 15:12:03 +0100 Subject: [PATCH] Optimised minimisation to work on leaves separately --- app/Main.hs | 2 +- app/Minimise.hs | 30 ++++++++++++++++++------------ app/OnsQuotient.hs | 16 +++++++++------- src/OrbitList.hs | 14 +++++++++++++- 4 files changed, 41 insertions(+), 21 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index b36feaf..7e431db 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -2,7 +2,7 @@ module Main where -import OrbitList +import OrbitList hiding (head) import Support (Rat) import Prelude (Show, Ord, Eq, Int, IO, print, otherwise, (.), ($), (!!), (+), (-), Bool, head, tail) diff --git a/app/Minimise.hs b/app/Minimise.hs index 7ba3025..4cb8138 100644 --- a/app/Minimise.hs +++ b/app/Minimise.hs @@ -17,7 +17,7 @@ import qualified EquivariantSet as Set import Data.Foldable (fold) import qualified GHC.Generics as GHC -import Prelude as P hiding (map, product, words, filter) +import Prelude as P hiding (map, product, words, filter, foldr) -- Version A: works on equivalence relations @@ -50,7 +50,7 @@ minimiseA Automaton{..} alph = Automaton -- Version B: works on quotient maps minimiseB :: _ => Automaton q a -> OrbitList a -> Automaton _ a minimiseB Automaton{..} alph = Automaton - { states = stInf + { states = map fst stInf , initialState = phiInf ! initialState , acceptance = Map.fromList . fmap (\(s, b) -> (phiInf ! s, b)) . Map.toList $ acceptance , transition = Map.fromList . fmap (\((s, a), t) -> ((phiInf ! s, a), phiInf ! t)) . Map.toList $ transition @@ -59,25 +59,25 @@ minimiseB Automaton{..} alph = Automaton -- Are all successors of s0 t0 related? nextAreEquiv phi s0 t0 = OrbitList.null . filter (\(s2, t2) -> s2 /= t2 && phi ! s2 /= phi ! t2) - $ productWith (\(s, t) a -> (transition ! (s, a), transition ! (t, a))) (singleOrbit (s0, t0)) alph + $ productWith (\a (s, t) -> (transition ! (s, a), transition ! (t, a))) alph (singleOrbit (s0, t0)) -- Are s0 t0 equivalent with current information? equiv phi s0 t0 = s0 == t0 || (phi ! s0 == phi ! t0 && nextAreEquiv phi s0 t0) - -- Given a quotientmap, refine it - go phi st = let (phi2, st2) = quotientf (equiv phi) states - in if size st == size st2 + addMid p a (f, b, k) = (p <> f, b <> a, k) + -- Given a quotientmap, refine it, per "leaf" + go phi st = let (phi2, st2, _) = foldr (\(_, clas) (phix, acc, k) -> addMid phix acc . quotientf k (equiv phi) . Set.toOrbitList $ clas) (mempty, empty, 0) st + in if size st == size st2 -- fixpoint then (phi, st) else go phi2 st2 -- Start with acceptance as quotient map - (phi0, st0) = quotientf (\a b -> a == b || acceptance ! a == acceptance ! b) states + (phi0, st0, _) = quotientf 0 (\a b -> a == b || acceptance ! a == acceptance ! b) states -- Compute fixpoint (phiInf, stInf) = go phi0 st0 main :: IO () main = do - -- putStrLn . toStr . toList . map (\x -> (x, True)) $ words 2 - -- putStrLn . toStr $ (fifoAut 3) - putStrLn . toStr $ (minimiseB (fifoAut 2) fifoAlph) + -- putStrLn . toStr $ (doubleWordAut 4) + putStrLn . toStr $ (minimiseB (doubleWordAut 4) rationals) -- All example automata follow below @@ -94,6 +94,12 @@ data DoubleWord = Store [Rat] | Check [Rat] | Accept | Reject deriving (Eq, Ord, GHC.Generic) deriving Nominal via Generic DoubleWord +instance ToStr DoubleWord where + toStr (Store w) = "S " ++ toStr w + toStr (Check w) = "C " ++ toStr w + toStr Accept = "A" + toStr Reject = "R" + doubleWordAut 0 = Automaton {..} where states = fromList [Accept, Reject] initialState = Accept @@ -106,8 +112,8 @@ doubleWordAut n = Automaton {..} where trans Accept _ = Reject trans Reject _ = Reject trans (Store l) a - | length l < n = Store (a:l) - | otherwise = Check (reverse (a:l)) + | length l + 1 < n = Store (a:l) + | otherwise = Check (reverse (a:l)) trans (Check (a:as)) b | a == b = if (P.null as) then Accept else Check as | otherwise = Reject diff --git a/app/OnsQuotient.hs b/app/OnsQuotient.hs index 9c47443..7a9d9a2 100644 --- a/app/OnsQuotient.hs +++ b/app/OnsQuotient.hs @@ -9,26 +9,28 @@ import qualified EquivariantMap as Map import EquivariantSet (EquivariantSet(..)) import qualified EquivariantSet as Set -import Prelude (Bool, Int, Ord, (.), (<>), (+), ($), snd, fmap, uncurry) +import Prelude (Bool, Int, Ord, (.), (<>), (+), ($), fst, snd, fmap, uncurry) type QuotientType = (Int, Support) type QuotientMap a = EquivariantMap a QuotientType -- Computes a quotient map given an equivalence relation quotient :: (Nominal a, Ord (Orbit a)) => EquivariantSet (a, a) -> OrbitList a -> (QuotientMap a, OrbitList QuotientType) -quotient equiv = quotientf (\a b -> (a, b) `Set.member` equiv) +quotient equiv = post . quotientf 0 (\a b -> (a, b) `Set.member` equiv) + where post (a, b, _) = (a, map fst b) -- f should be equivariant and an equivalence relation -quotientf :: (Nominal a, Ord (Orbit a)) => (a -> a -> Bool) -> OrbitList a -> (QuotientMap a, OrbitList QuotientType) -quotientf f ls = go 0 Map.empty empty (toList ls) +quotientf :: (Nominal a, Ord (Orbit a)) => Int -> (a -> a -> Bool) -> OrbitList a -> (QuotientMap a, OrbitList (QuotientType, EquivariantSet a), Int) +quotientf k f ls = go k Map.empty empty (toList ls) where - go _ phi acc [] = (phi, acc) + go n phi acc [] = (phi, acc, n) go n phi acc (a:as) = let y0 = filter (uncurry f) (product (singleOrbit a) (fromList as)) y1 = filter (uncurry f) (product (singleOrbit a) (singleOrbit a)) y2 = map (\(a1, a2) -> (a2, (n, support a1 `intersect` support a2))) (y1 <> y0) m0 = Map.fromListWith (\(n1, s1) (n2, s2) -> (n1, s1 `intersect` s2)) . toList $ y2 - l0 = take 1 . fromList . fmap snd $ Map.toList m0 + clas = Map.keysSet m0 + l0 = head . fromList . fmap snd $ Map.toList m0 in if a `Set.member` (Map.keysSet phi) then go n phi acc as - else go (n+1) (phi <> m0) (acc <> l0) as + else go (n+1) (phi <> m0) ((l0, clas) `cons` acc) as diff --git a/src/OrbitList.hs b/src/OrbitList.hs index 466c581..1ebc35d 100644 --- a/src/OrbitList.hs +++ b/src/OrbitList.hs @@ -41,6 +41,9 @@ elem x = L.elem (toOrbit x) . unOrbitList size :: forall a. Nominal a => OrbitList a -> [Int] size = LO.sortOn negate . fmap (index (Proxy :: Proxy a)) . unOrbitList +-- May fail when empty +head :: Nominal a => OrbitList a -> a +head (OrbitList l) = getElementE (L.head l) -- Construction @@ -53,6 +56,9 @@ singleOrbit a = OrbitList [toOrbit a] rationals :: OrbitList Rat rationals = singleOrbit (Rat 0) +cons :: Nominal a => a -> OrbitList a -> OrbitList a +cons a (OrbitList l) = OrbitList (toOrbit a : l) + repeatRationals :: Int -> OrbitList [Rat] repeatRationals 0 = singleOrbit [] repeatRationals n = productWith (:) rationals (repeatRationals (n-1)) @@ -75,7 +81,13 @@ take :: Int -> OrbitList a -> OrbitList a take n = OrbitList . L.take n . unOrbitList -- TODO: drop, span, takeWhile, ... --- TODO: folds + +-- TODO: Think about preconditions and postconditions of folds +foldr :: Nominal a => (a -> b -> b) -> b -> OrbitList a -> b +foldr f b = L.foldr (f . getElementE) b . unOrbitList + +foldl :: Nominal a => (b -> a -> b) -> b -> OrbitList a -> b +foldl f b = L.foldl (\acc -> f acc . getElementE) b . unOrbitList -- Combinations