diff --git a/app/LStarMain.hs b/app/LStarMain.hs index 518685e..120f3c9 100644 --- a/app/LStarMain.hs +++ b/app/LStarMain.hs @@ -19,8 +19,7 @@ debugOutput = False semanticsForState :: MealyMachine s i o -> s -> [i] -> o semanticsForState _ _ [] = error "" semanticsForState MealyMachine{..} q [a] = fst (behaviour q a) -semanticsForState m@MealyMachine{..} q (a:w) = semanticsForState m (snd (behaviour q a)) w - +semanticsForState m@MealyMachine{..} q (a : w) = semanticsForState m (snd (behaviour q a)) w main :: IO () main = do @@ -28,38 +27,39 @@ main = do print dotFile transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile - let machine = convertToMealy transitions - alphabet = inputs machine - tInit = initialState machine - tOut s i = fst (behaviour machine s i) - tTrans s i = snd (behaviour machine s i) + let + machine = convertToMealy transitions + alphabet = inputs machine + tInit = initialState machine + tOut s i = fst (behaviour machine s i) + tTrans s i = snd (behaviour machine s i) - mq0 = semanticsForState machine (initialState machine) - mq = countingMQ (\w -> when debugOutput (print w) >> return (mq0 w)) + mq0 = semanticsForState machine (initialState machine) + mq = countingMQ (\w -> when debugOutput (print w) >> return (mq0 w)) - let loop table = do - lift $ putStrLn "Making the table closed and consistent" - (table2, b) <- makeClosedAndConsistentA mq table - let (hInit, size, hTransMap, hOutMap) = createHypothesis table2 - hTrans s i = hTransMap Map.! (s, i) - hOut s i = hOutMap Map.! (s, i) - res = bisimulation2 alphabet tOut tTrans tInit hOut hTrans hInit + loop table = do + lift $ putStrLn "Making the table closed and consistent" + (table2, b) <- makeClosedAndConsistentA mq table + let (hInit, size, hTransMap, hOutMap) = createHypothesis table2 + hTrans s i = hTransMap Map.! (s, i) + hOut s i = hOutMap Map.! (s, i) + res = bisimulation2 alphabet tOut tTrans tInit hOut hTrans hInit - lift $ putStrLn (if b then "Table changed" else "Table did not changed") - lift $ putStrLn (show size <> " states") + lift $ putStrLn (if b then "Table changed" else "Table did not changed") + lift $ putStrLn (show size <> " states") - case res of - Nothing -> do - lift $ putStrLn "Done learning!" - return size - Just cex -> do - lift $ putStrLn "CEX:" >> print cex - table3 <- processCounterexampleA cex mq table2 - loop table3 + case res of + Nothing -> do + lift $ putStrLn "Done learning!" + return size + Just cex -> do + lift $ putStrLn "CEX:" >> print cex + table3 <- processCounterexampleA cex mq table2 + loop table3 - learner = do - table <- initialiseA alphabet mq - loop table + learner = do + table <- initialiseA alphabet mq + loop table (a, b) <- runStateT learner 0 diff --git a/app/Main.hs b/app/Main.hs index b682df4..af47aa1 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,3 +1,6 @@ +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + +{-# HLINT ignore "Avoid reverse" #-} module Main where import DotParser @@ -10,21 +13,20 @@ import Preorder import Control.Monad (forM_) import Data.Bifunctor -import Data.List (sort, sortOn, intercalate) +import Data.List (intercalate, sort, sortOn) import Data.List.Ordered (nubSort) import Data.Map.Strict qualified as Map -import Data.Maybe (mapMaybe) +import Data.Maybe (isNothing, mapMaybe) import Data.Set qualified as Set import Data.Tuple (swap) import System.Environment import Text.Megaparsec - converseRelation :: Ord b => Map.Map a b -> Map.Map b [a] -converseRelation m = Map.fromListWith (++) . fmap (second pure . swap) . Map.assocs $ m +converseRelation = Map.fromListWith (++) . fmap (second pure . swap) . Map.assocs myWriteFile :: FilePath -> String -> IO () -myWriteFile filename content = writeFile ("results/" ++ filename) content +myWriteFile filename = writeFile ("results/" ++ filename) {- Hacked together, you can view the result with: @@ -39,10 +41,7 @@ main = do -- Read dot file [dotFile] <- getArgs print dotFile - transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile - - -- convert to mealy - let machine = convertToMealy transitions + machine <- convertToMealy . mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile -- print some basic info putStrLn $ (show . length $ states machine) <> " states, " <> (show . length $ inputs machine) <> " inputs and " <> (show . length $ outputs machine) <> " outputs" @@ -69,20 +68,24 @@ main = do -- Then compute each projection -- 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, state2idx) = allProjections machine outs - projections = zip outs $ fmap refineMealy projections0 + 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, state2idx) = allProjections machine outs + projections = zip outs $ fmap refineMealy projections0 -- Print number of states of each projection - forM_ projections (\(o, partition) -> do - putStr $ o <> " -> " - printPartition partition + forM_ + projections + ( \(o, partition) -> do + putStr $ o <> " -> " + printPartition partition ) -- 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 + let + preord p1 p2 = toPreorder (comparePartitions p1 p2) + (equiv, uniqPartitions) = equivalenceClasses preord projections putStrLn "" putStrLn "Representatives" @@ -90,19 +93,24 @@ main = do putStrLn "" putStrLn "Equivalences" - forM_ (Map.assocs equiv) (\(o2, o1) -> do - putStrLn $ " " <> (show o2) <> " == " <> (show o1) + forM_ + (Map.assocs equiv) + ( \(o2, o1) -> do + putStrLn $ " " <> show o2 <> " == " <> show o1 ) -- 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 - foo (a, b) = (numBlocks b, a) + let + (topMods, downSets) = maximalElements preord uniqPartitions + foo (a, b) = (numBlocks b, a) putStrLn "" putStrLn "Top modules" - forM_ (reverse . sort . fmap foo $ topMods) (\(b, o) -> do - putStrLn $ " " <> (show o) <> " has size " <> (show b) + forM_ + (reverse . sort . fmap foo $ topMods) + ( \(b, o) -> do + putStrLn $ " " <> show o <> " has size " <> show b ) -- Then we try to combine paritions, so that we don't end up with @@ -114,35 +122,37 @@ main = do projmap <- heuristicMerger topMods strategy -- Now we are going to output the components we found. - let equivInv = converseRelation equiv - projmapN = zip projmap [1 :: Int ..] - - forM_ projmapN (\((os, p), i) -> do - let name = intercalate "x" os - osWithRel = concat $ os:[Map.findWithDefault [] o downSets | o <- os] - osWithRelAndEquiv = concat $ osWithRel:[Map.findWithDefault [] o equivInv | o <- osWithRel] + let + equivInv = converseRelation equiv + projmapN = zip projmap [1 :: Int ..] + action ((os, p), componentIdx) = do + let + name = intercalate "x" os + osWithRel = concat $ os : [Map.findWithDefault [] o downSets | o <- os] + osWithRelAndEquiv = concat $ osWithRel : [Map.findWithDefault [] o equivInv | o <- osWithRel] componentOutputs = Set.fromList osWithRelAndEquiv - proj = projectToComponent (flip Set.member componentOutputs) machine + proj = projectToComponent (`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 "" + putStrLn $ "Component " <> show os + putStrLn $ "Correct? " <> show (comparePartitions p partition) + putStrLn $ "Size = " <> show (numBlocks p) - (do - let filename = "partition_" <> show i <> ".dot" + do + let + filename = "partition_" <> show componentIdx <> ".dot" idx2State = Map.map head . converseRelation $ state2idx stateBlocks = fmap (fmap (idx2State Map.!)) . Partition.toBlocks $ partition - content = unlines . fmap (intercalate " ") $ stateBlocks + content = unlines . fmap unwords $ stateBlocks - putStrLn $ "Output (partition) in file " <> filename - myWriteFile filename content - ) + putStrLn $ "Output (partition) in file " <> filename + myWriteFile filename content - (do - let MealyMachine{..} = proj + 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 @@ -152,31 +162,29 @@ main = do -- The initial state should be first initialBlock = state2block initialState -- Sorting on "/= initialBlock" puts the initialBlock in front - initialFirst = sortOn (\(s,_,_,_) -> s /= initialBlock) transitionsBlocks + initialFirst = sortOn (\(s, _, _, _) -> s /= initialBlock) transitionsBlocks -- Convert to a file - filename1 = "component_" <> show i <> ".dot" + filename1 = "component_" <> show componentIdx <> ".dot" content1 = toString . mealyToDot name $ initialFirst -- 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 + deadInputs0 = Map.fromListWith (++) . fmap (\(s, i, o, t) -> (i, [(s, o, t)])) $ initialFirst + deadInputs = Map.keysSet . Map.filter (all (\(s, o, t) -> s == t && isNothing o)) $ deadInputs0 + result = filter (\(_, i, _, _) -> i `Set.notMember` deadInputs) initialFirst -- Convert to a file - filename2 = "component_reduced_" <> show i <> ".dot" + filename2 = "component_reduced_" <> show componentIdx <> ".dot" content2 = toString . mealyToDot name $ result - putStrLn $ "Output (reduced machine) in file " <> filename1 - myWriteFile filename1 content1 + putStrLn $ "Output (reduced machine) in file " <> filename1 + myWriteFile filename1 content1 - putStrLn $ "Dead inputs = " <> show (Set.size deadInputs) + putStrLn $ "Dead inputs = " <> show (Set.size deadInputs) - putStrLn $ "Output (reduced machine) in file " <> filename2 - myWriteFile filename2 content2 - ) - ) + putStrLn $ "Output (reduced machine) in file " <> filename2 + myWriteFile filename2 content2 - return () + mapM_ action projmapN diff --git a/app/RandomGen.hs b/app/RandomGen.hs index 0d23660..9471a25 100644 --- a/app/RandomGen.hs +++ b/app/RandomGen.hs @@ -1,5 +1,6 @@ -{-# language PartialTypeSignatures #-} +{-# LANGUAGE PartialTypeSignatures #-} {-# OPTIONS_GHC -Wno-partial-type-signatures #-} + module Main where import SplittingTree @@ -16,28 +17,31 @@ import System.Random genTransitions :: _ => Int -> [Char] -> [Char] -> RandT _ _ _ genTransitions size inputs outputs = do let - states = [1..size] + states = [1 .. size] numOutputs = length outputs - randomOutput = (outputs !!) <$> liftRand (uniformR (0, numOutputs-1)) - randomTarget = (states !!) <$> liftRand (uniformR (0, size-1)) + randomOutput = (outputs !!) <$> liftRand (uniformR (0, numOutputs - 1)) + randomTarget = (states !!) <$> liftRand (uniformR (0, size - 1)) randomTransition s i = (\o t -> (s, i, o, t)) <$> randomOutput <*> randomTarget - t <- sequence $ (\s i -> randomTransition s i) <$> states <*> inputs + t <- sequence $ randomTransition <$> states <*> inputs return (states, t) -- numC <= 8 genComposition :: _ => Int -> Int -> [Char] -> RandT _ _ _ genComposition size numC inputs = do let - components = [1..numC] + components = [1 .. numC] outputSets = [[], "xy", "zw", "uv", "kl", "mn", "op", "qr", "st"] allTransitions <- traverse (\c -> genTransitions size inputs (outputSets !! c)) components let - productState = fmap (Map.fromList . zip components) (sequence (fmap fst allTransitions)) + productState = fmap (Map.fromList . zip components) (mapM fst allTransitions) allStates = (,) <$> components <*> productState - compMap = Map.fromList $ zip components (fmap (Map.fromList . fmap (\(s, i, o, t) -> ((s, i), (o, t)))) . fmap snd $ allTransitions) - norm c = if c <= 0 then c + numC else if c > numC then c - numC else c + compMap = Map.fromList $ zip components ((Map.fromList . fmap (\(s, i, o, t) -> ((s, i), (o, t)))) . snd <$> allTransitions) + norm c + | c <= 0 = c + numC + | c > numC = c - numC + | otherwise = c transition (c, cs) 'L' = (norm (c - 1), cs) transition (c, cs) 'R' = (norm (c + 1), cs) transition (c, cs) x = (c, Map.adjust (\s -> snd (compMap Map.! c Map.! (s, x))) c cs) @@ -46,16 +50,16 @@ genComposition size numC inputs = do output (c, cs) x = fst (compMap Map.! c Map.! (cs Map.! c, x)) -- initial states, inputs, transition function, outputs - return (head allStates, 'L':'R':inputs, transition, output) + return (head allStates, 'L' : 'R' : inputs, transition, output) reachability :: _ => s -> [i] -> (s -> i -> s) -> Map.Map s Int reachability initialState inputs transitions = go 0 Map.empty [initialState] - where - go _ visited [] = visited - go n visited (s:rest) = - let newVis = Map.insert s n visited - newStates = [t | i <- inputs, let t = transitions s i, t `Map.notMember` newVis] - in go (n+1) newVis (rest ++ newStates) + where + go _ visited [] = visited + go n visited (s : rest) = + let newVis = Map.insert s n visited + newStates = [t | i <- inputs, let t = transitions s i, t `Map.notMember` newVis] + in go (n + 1) newVis (rest ++ newStates) main :: IO () main = do @@ -75,12 +79,12 @@ main = do states = Map.elems reachableMap init = reachableMap Map.! init0 trans s i = reachableMap Map.! trans0 (inverseMap Map.! s) i - outpf s i = outpf0 (inverseMap Map.! s) i + outpf s = outpf0 (inverseMap Map.! s) -- minimize let outputFuns = [(i, fun) | i <- inputs, let fun s = outpf s i] - reverseTransitionMaps i = Map.fromListWith (++) [ (t, [s]) | s <- states, let t = trans s i] + reverseTransitionMaps i = Map.fromListWith (++) [(t, [s]) | s <- states, let t = trans s i] reverseFuns = [(i, fun) | i <- inputs, let m = reverseTransitionMaps i, let fun s = Map.findWithDefault [] s m] PRState{..} <- execStateT (refine (const (pure ())) outputFuns reverseFuns) (initialPRState states) @@ -89,7 +93,7 @@ main = do let toBlock s = getPartition partition Map.! s allTransitions = [(toBlock s, i, o, toBlock t) | s <- states, i <- inputs, let o = outpf s i, let t = trans s i] - uniqueTransitions = sortOn (\(s,_,_,_) -> s /= toBlock init) .Set.toList . Set.fromList $ allTransitions + uniqueTransitions = sortOn (\(s, _, _, _) -> s /= toBlock init) . Set.toList . Set.fromList $ allTransitions showLabel i o = "[label=\"" <> [i] <> "/" <> [o] <> "\"]" showTransition s i o t = "s" <> show (coerce s :: Int) <> " -> " <> "s" <> show (coerce t :: Int) <> " " <> showLabel i o diff --git a/other/decompose_fsm_optimise.py b/other/decompose_fsm_optimise.py index e63f860..36e4f3b 100644 --- a/other/decompose_fsm_optimise.py +++ b/other/decompose_fsm_optimise.py @@ -335,9 +335,7 @@ class Encoder: # Even omzetten in een makkelijkere data structuur m = self.solver.get_model() - model = {} - for l in m: - model[abs(l)] = l > 0 + model = {abs(l): l > 0 for l in m} if self.args.verbose: for rid in self.rids: diff --git a/src/Bisimulation.hs b/src/Bisimulation.hs index ad1a452..75ada27 100644 --- a/src/Bisimulation.hs +++ b/src/Bisimulation.hs @@ -4,10 +4,9 @@ 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 } +newtype UnionFind x = MkUnionFind {unUnionFind :: Map.Map x x} -- Alle elementen zijn hun eigen klasse, dit geven we aan met Nothing. empty :: UnionFind x @@ -15,10 +14,9 @@ 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 = case Map.lookup z m of - Nothing -> z - Just w -> root w +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. @@ -26,39 +24,37 @@ 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 - - + 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 - where - go Seq.Empty _ = Nothing - go ((rpath, a, b) Seq.:<| queue) !visited - -- Skip the equal nodes - | a == b = go queue visited - -- Skip nodes deemed equivalent - | equivalent a b visited = go queue visited - -- Of not visited, check output and add successors to queue - | otherwise = + where + go Seq.Empty _ = Nothing + go ((rpath, a, b) Seq.:<| queue) !visited + -- Skip the equal nodes + | a == b = go queue visited + -- Skip nodes deemed equivalent + | equivalent a b visited = go queue visited + -- Of not visited, check output and add successors to queue + | otherwise = case find (\i -> output a i /= output b i) alphabet of -- Found an input which leads to different outputs => return difference Just i -> Just (reverse (i : rpath)) -- Else, we continue the search Nothing -> - let succesors = Seq.fromList $ fmap (\i -> (i:rpath, transition a i, transition b i)) alphabet - in go (queue <> succesors) (equate a b visited) + let succesors = Seq.fromList $ fmap (\i -> (i : rpath, transition a i, transition b i)) alphabet + in go (queue <> succesors) (equate a b visited) -- Bisimulatie in verschillende machines bisimulation2 :: (Eq o, Ord s, Ord t) => [i] -> (s -> i -> o) -> (s -> i -> s) -> s -> (t -> i -> o) -> (t -> i -> t) -> t -> Maybe [i] bisimulation2 alphabet output1 transition1 x output2 transition2 y = bisimulation alphabet (either output1 output2) transition (Left x) (Right y) - where - transition (Left s) i = Left (transition1 s i) - transition (Right t) i = Right (transition2 t i) + where + transition (Left s) i = Left (transition1 s i) + transition (Right t) i = Right (transition2 t i) diff --git a/src/DotParser.hs b/src/DotParser.hs index 2e17064..f7f28a3 100644 --- a/src/DotParser.hs +++ b/src/DotParser.hs @@ -29,38 +29,40 @@ type Parser = Parsec Void String parseTrans :: Parser Trans parseTrans = assoc <$> identifierQ <* symbol "->" <*> identifierQ <*> brackets parseLabel <* optional (symbol ";") - where - -- defines whitespace and lexemes - sc = L.space space1 empty empty - lexeme = L.lexeme sc - symbol = L.symbol sc - -- state, input, output is any string of alphaNumChar's - isAlphaNumExtra c = isAlphaNum c || c == '_' || c == '+' || c == '.' || c == ',' || c == '-' || c == '(' || c == ')' - alphaNumCharExtra = satisfy isAlphaNumExtra "alphanumeric character or extra" - identifier = lexeme (some alphaNumCharExtra) - identifierQ = identifier <|> between (symbol "\"") (symbol "\"") identifier - -- The label has the shape [label="i/o"] - brackets = between (symbol "[") (symbol "]") - parseLabel = (,) <$> (symbol "label=\"" *> identifier <* symbol "/") <*> (identifier <* symbol "\"") - -- re-associate different parts of the parser - assoc from to (i, o) = (from, to, i, o) + where + -- defines whitespace and lexemes + sc = L.space space1 empty empty + lexeme = L.lexeme sc + symbol = L.symbol sc + -- state, input, output is any string of alphaNumChar's + isAlphaNumExtra c = isAlphaNum c || c == '_' || c == '+' || c == '.' || c == ',' || c == '-' || c == '(' || c == ')' + alphaNumCharExtra = satisfy isAlphaNumExtra "alphanumeric character or extra" + identifier = lexeme (some alphaNumCharExtra) + identifierQ = identifier <|> between (symbol "\"") (symbol "\"") identifier + -- The label has the shape [label="i/o"] + brackets = between (symbol "[") (symbol "]") + parseLabel = (,) <$> (symbol "label=\"" *> identifier <* symbol "/") <*> (identifier <* symbol "\"") + -- re-associate different parts of the parser + assoc from to (i, o) = (from, to, i, o) parseTransFull :: Parser Trans parseTransFull = space *> parseTrans <* eof convertToMealy :: [Trans] -> MealyMachine String String String -convertToMealy l = MealyMachine - { states = states - , 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 - tos = OrdList.nubSort . fmap (\(_,a,_,_) -> a) $ l - ins = OrdList.nubSort . fmap (\(_,_,i,_) -> i) $ l - outs = OrdList.nubSort . fmap (\(_,_,_,o) -> o) $ l - states = froms `OrdList.union` tos - base = Map.fromList . fmap (\(from, to, i, o) -> ((from, i), (o, to))) $ l +convertToMealy l = + MealyMachine + { states = states + , inputs = ins + , outputs = outs + , behaviour = curry (base Map.!) + , initialState = (\(a, _, _, _) -> a) . head $ l + } + where + -- \^ Assumption: first transition in the file belongs to the initial state + + froms = OrdList.nubSort . fmap (\(a, _, _, _) -> a) $ l + tos = OrdList.nubSort . fmap (\(_, a, _, _) -> a) $ l + ins = OrdList.nubSort . fmap (\(_, _, i, _) -> i) $ l + outs = OrdList.nubSort . fmap (\(_, _, _, o) -> o) $ l + states = froms `OrdList.union` tos + base = Map.fromList . fmap (\(from, to, i, o) -> ((from, i), (o, to))) $ l diff --git a/src/LStar.hs b/src/LStar.hs index b155fc7..411f172 100644 --- a/src/LStar.hs +++ b/src/LStar.hs @@ -73,7 +73,7 @@ inconsistencies table@LStarState{..} = defects equivalentPairs = [(r1, r2) | r1 <- Set.toList rowIndices, r2 <- Set.toList rowIndices, r1 < r2, row table r1 == row table r2] defects = [(a, s) | (r1, r2) <- equivalentPairs, a <- alphabet, let d = differenceOfRows r1 r2 a, s <- Map.keys d] differenceOfRows r1 r2 a = differenceOfMaps (row table (r1 `snoc` a)) (row table (r2 `snoc` a)) - differenceOfMaps m1 m2 = MapMerge.merge MapMerge.dropMissing MapMerge.dropMissing (MapMerge.zipWithMaybeMatched (\_ x y -> if x == y then Nothing else Just ())) m1 m2 + differenceOfMaps = MapMerge.merge MapMerge.dropMissing MapMerge.dropMissing (MapMerge.zipWithMaybeMatched (\_ x y -> if x == y then Nothing else Just ())) -- Preconditie: tabel is gesloten en consistent -- TODO: misschien checken of de automaat uniek is? De constructie van @@ -83,7 +83,7 @@ createHypothesis :: (Ord i, Ord o) => LStarState i o -> (Int, Int, Map.Map (Int, createHypothesis table@LStarState{..} = (initialState, Map.size row2IntMap, transitions, outputs) where rowIndicesLs = Set.toList rowIndices - upperRows = map (row table) $ rowIndicesLs + upperRows = map (row table) rowIndicesLs row2IntMap = Map.fromList $ zip upperRows [0..] row2Int = (Map.!) row2IntMap . row table transitions = Map.fromList [((row2Int r, a), row2Int (r `snoc` a)) | r <- rowIndicesLs, a <- alphabet] @@ -97,7 +97,7 @@ createHypothesis table@LStarState{..} = (initialState, Map.size row2IntMap, tran -- Een lege tabel heeft altijd een "epsilon-rij" en voor elk symbool een kolom. -- (Omdat het Mealy machines zijn.) initialiseA :: (Applicative f, Ord i) => [i] -> MQ f i o -> f (LStarState i o) -initialiseA alphabet mq = initialiseWithA alphabet [mempty] (map pure alphabet) mq +initialiseA alphabet = initialiseWithA alphabet [mempty] (map pure alphabet) -- We kunnen ook een tabel maken met voorgedefinieerde rijen en kolommen. initialiseWithA :: (Applicative f, Ord i) => [i] -> [Word i] -> [Word i] -> MQ f i o -> f (LStarState i o) @@ -106,7 +106,7 @@ initialiseWithA alphabet rowIdcs colIdcs mq = (\content -> LStarState{..}) <$> c rowIndices = Set.fromList rowIdcs colIndices = Set.fromList colIdcs queries = [p <> m <> s | p <- rowIdcs, m <- []:fmap pure alphabet, s <- colIdcs] - contentA = Map.traverseWithKey (\w _ -> mq w) . Map.fromList . zip queries $ repeat () + contentA = Map.traverseWithKey (\ w _ -> mq w) . Map.fromList . map (, ()) $ queries -- preconditie: newRowIndices is disjunct van de huidige rowIndices en de -- vereniging is prefix-gesloten. (Wordt niet gechecked.) @@ -116,7 +116,7 @@ addRowsA newRowIndices mq table@LStarState{..} = (\newContent -> table , rowIndices = rowIndices <> Set.fromList newRowIndices }) <$> contentA where queries = [w | p <- newRowIndices, m <- []:fmap pure alphabet, s <- Set.toList colIndices, let w = p <> m <> s, w `Map.notMember` content] - contentA = Map.traverseWithKey (\w _ -> mq w) . Map.fromList . zip queries $ repeat () + contentA = Map.traverseWithKey (\ w _ -> mq w) . Map.fromList . map (, ()) $ queries -- preconditie: zie addRows (?) addColumnsA :: (Applicative f, Ord i) => [Word i] -> MQ f i o -> LStarState i o -> f (LStarState i o) @@ -125,7 +125,7 @@ addColumnsA newColIndices mq table@LStarState{..} = (\newContent -> table , colIndices = colIndices <> Set.fromList newColIndices }) <$> contentA where queries = [w | p <- Set.toList rowIndices, m <- []:fmap pure alphabet, s <- newColIndices, let w = p <> m <> s, w `Map.notMember` content] - contentA = Map.traverseWithKey (\w _ -> mq w) . Map.fromList . zip queries $ repeat () + contentA = Map.traverseWithKey (\ w _ -> mq w) . Map.fromList . map (, ()) $ queries ------------------ diff --git a/src/Mealy.hs b/src/Mealy.hs index 0a42841..5cd7bf0 100644 --- a/src/Mealy.hs +++ b/src/Mealy.hs @@ -15,18 +15,18 @@ transitionFunction :: MealyMachine s i o -> s -> i -> s transitionFunction MealyMachine{..} s i = snd (behaviour s i) exampleMM :: MealyMachine String Char String -exampleMM = - let states = ["q0", "q1", "q2", "q3"] - inputs = ['a', 'b'] - outputs = ["een", "twee", "drie", "vier"] - behaviour "q0" 'a' = ("een", "q1") - behaviour "q1" 'a' = ("drie", "q0") - behaviour "q2" 'a' = ("een", "q3") - behaviour "q3" 'a' = ("drie", "q2") - behaviour "q0" 'b' = ("vier", "q2") - behaviour "q2" 'b' = ("twee", "q0") - behaviour "q1" 'b' = ("vier", "q3") - behaviour "q3" 'b' = ("twee", "q1") - behaviour _ _ = error "undefined behaviour of exampleMM" - initialState = "q0" - in MealyMachine{..} +exampleMM = MealyMachine{..} + where + states = ["q0", "q1", "q2", "q3"] + inputs = ['a', 'b'] + outputs = ["een", "twee", "drie", "vier"] + behaviour "q0" 'a' = ("een", "q1") + behaviour "q1" 'a' = ("drie", "q0") + behaviour "q2" 'a' = ("een", "q3") + behaviour "q3" 'a' = ("drie", "q2") + behaviour "q0" 'b' = ("vier", "q2") + behaviour "q2" 'b' = ("twee", "q0") + behaviour "q1" 'b' = ("vier", "q3") + behaviour "q3" 'b' = ("twee", "q1") + behaviour _ _ = error "undefined behaviour of exampleMM" + initialState = "q0" diff --git a/src/MealyRefine.hs b/src/MealyRefine.hs index 6e7a20f..eda8f95 100644 --- a/src/MealyRefine.hs +++ b/src/MealyRefine.hs @@ -5,32 +5,34 @@ import Partition (Partition) import Control.Monad.ST (runST) import Copar.Algorithm (refine) -import Copar.Functors.Polynomial (Polynomial, PolyF1(..)) -import Copar.RefinementInterface (Label, F1) +import Copar.Functors.Polynomial (PolyF1 (..), Polynomial) +import Copar.RefinementInterface (F1, Label) import Data.Bool (bool) -import Data.CoalgebraEncoding (Encoding(..)) +import Data.CoalgebraEncoding (Encoding (..)) import Data.List.Ordered (nubSort) import Data.Map.Strict qualified as Map -import Data.Proxy (Proxy(..)) +import Data.Proxy (Proxy (..)) import Data.Vector qualified import Data.Vector.Unboxed qualified 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) -> (f out, s2) - , .. - } +project f MealyMachine{..} = + MealyMachine + { outputs = nubSort $ fmap f outputs -- inefficient + , behaviour = \s i -> case behaviour s i of + (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 + 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 @@ -38,26 +40,32 @@ projectToComponent oPred = project oMaybe -- for each projection. 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 - idx2state = Map.fromList $ zip [0..] states - state2idx = Map.fromList $ zip states [0..] - idx2input = Map.fromList $ zip [0..] inputs - stateInputIndex n = n `divMod` numInputs -- inverse of \(s, i) -> s * numInputs + i - edgesFrom = Data.Vector.Unboxed.generate (numStates * numInputs) (fst . stateInputIndex) - edgesLabel = Data.Vector.generate (numStates * numInputs) (snd . stateInputIndex) - edgesTo = Data.Vector.Unboxed.generate (numStates * numInputs) ((state2idx Map.!) . snd . (\(s, i) -> behaviour (idx2state Map.! s) (idx2input Map.! i)) . stateInputIndex) - bool2Int = bool 0 1 - structure o = Data.Vector.generate numStates - (\s -> PolyF1 - { polyF1Summand = 0 -- There is only one summand - , polyF1Variables = numInputs -- This many transitions per state - , polyF1Constants = Data.Vector.Unboxed.generate numInputs - (\i -> bool2Int . (o==) . fst $ (behaviour (idx2state Map.! s) (idx2input Map.! i))) - } + where + numStates = length states + numInputs = length inputs + idx2state = Map.fromList $ zip [0 ..] states + state2idx = Map.fromList $ zip states [0 ..] + idx2input = Map.fromList $ zip [0 ..] inputs + stateInputIndex n = n `divMod` numInputs -- inverse of \(s, i) -> s * numInputs + i + edgesFrom = Data.Vector.Unboxed.generate (numStates * numInputs) (fst . stateInputIndex) + edgesLabel = Data.Vector.generate (numStates * numInputs) (snd . stateInputIndex) + edgesTo = Data.Vector.Unboxed.generate (numStates * numInputs) ((state2idx Map.!) . snd . (\(s, i) -> behaviour (idx2state Map.! s) (idx2input Map.! i)) . stateInputIndex) + bool2Int = bool 0 1 + structure o = + Data.Vector.generate + numStates + ( \s -> + PolyF1 + { polyF1Summand = 0 -- There is only one summand + , polyF1Variables = numInputs -- This many transitions per state + , polyF1Constants = + Data.Vector.Unboxed.generate + numInputs + (\i -> bool2Int . (o ==) . fst $ behaviour (idx2state Map.! s) (idx2input Map.! i)) + } ) - mkEncoding o = Encoding + mkEncoding o = + Encoding { eStructure = structure o , eInitState = Nothing -- not needed , eEdgesFrom = edgesFrom @@ -73,22 +81,27 @@ mealyMachineToEncoding :: (Ord s, Ord i, Ord o) => MealyMachine s i o -> Encodin mealyMachineToEncoding MealyMachine{..} = let numStates = length states numInputs = length inputs - idx2state = Map.fromList $ zip [0..] states - idx2input = Map.fromList $ zip [0..] inputs - out2idx = Map.fromList $ zip outputs [0..] - eStructure = Data.Vector.generate numStates - (\s -> PolyF1 - { polyF1Summand = 0 -- There is only one summand - , polyF1Variables = numInputs -- This many transitions per state - , polyF1Constants = Data.Vector.Unboxed.generate numInputs - (\i -> out2idx Map.! (fst (behaviour (idx2state Map.! s) (idx2input Map.! i)))) - } - ) + idx2state = Map.fromList $ zip [0 ..] states + idx2input = Map.fromList $ zip [0 ..] inputs + out2idx = Map.fromList $ zip outputs [0 ..] + eStructure = + Data.Vector.generate + numStates + ( \s -> + PolyF1 + { polyF1Summand = 0 -- There is only one summand + , polyF1Variables = numInputs -- This many transitions per state + , polyF1Constants = + Data.Vector.Unboxed.generate + numInputs + (\i -> out2idx Map.! fst (behaviour (idx2state Map.! s) (idx2input Map.! i))) + } + ) eInitState = Nothing - state2idx = Map.fromList $ zip states [0..] + state2idx = Map.fromList $ zip states [0 ..] stateInputIndex n = n `divMod` numInputs -- stateInputPair (s, i) = s * numInputs + i eEdgesFrom = Data.Vector.Unboxed.generate (numStates * numInputs) (fst . stateInputIndex) eEdgesLabel = Data.Vector.generate (numStates * numInputs) (snd . stateInputIndex) eEdgesTo = Data.Vector.Unboxed.generate (numStates * numInputs) ((state2idx Map.!) . snd . (\(s, i) -> behaviour (idx2state Map.! s) (idx2input Map.! i)) . stateInputIndex) - in Encoding { .. } + in Encoding{..} diff --git a/src/Merger.hs b/src/Merger.hs index 08eacb1..abcf058 100644 --- a/src/Merger.hs +++ b/src/Merger.hs @@ -27,34 +27,35 @@ heuristicMerger :: Ord o => [(o, Partition)] -> MergerStrategy -> IO [([o], Part heuristicMerger components strategy = do projmap <- evalStateT (loop 2) (Map.fromList (fmap (first pure) components)) return $ Map.assocs projmap - where - score ps p3 = numBlocks p3 - sum (fmap numBlocks ps) - combine ops = let os = fmap fst ops - ps = fmap snd ops - p3 = foldr1 commonRefinement ps - in ((os, p3), score ps p3) - isSortedOn f ls = and $ zipWith (\a b -> f a < f b) ls (drop 1 ls) - allCombs n projs = fmap combine . filter (isSortedOn fst) $ replicateM n projs - minComb n projs = minimumBy (comparing snd) (allCombs n projs) - safeStrategy ms@MergerStats{..} - | numberOfComponents <= 1 = Stop - | otherwise = strategy ms + where + score ps p3 = numBlocks p3 - sum (fmap numBlocks ps) + combine ops = + let os = fmap fst ops + ps = fmap snd ops + p3 = foldr1 commonRefinement ps + in ((os, p3), score ps p3) + isSortedOn f ls = and $ zipWith (\a b -> f a < f b) ls (drop 1 ls) + allCombs n projs = fmap combine . filter (isSortedOn fst) $ replicateM n projs + minComb n projs = minimumBy (comparing snd) (allCombs n projs) + safeStrategy ms@MergerStats{..} + | numberOfComponents <= 1 = Stop + | otherwise = strategy ms - loop n = do - projmap <- get - let numberOfComponents = Map.size projmap - componentSizes = fmap numBlocks . Map.elems $ projmap - maximalComponent = maximum componentSizes - totalSize = sum componentSizes - ms = MergerStats{..} - liftIO . print $ ms - case safeStrategy ms of - Stop -> return projmap - Continue -> do - let ((os, p3), _) = minComb n (Map.assocs projmap) - o3 = mconcat os - newProjmap = Map.insert o3 p3 . Map.withoutKeys projmap $ Set.fromList os - put newProjmap - if Map.size newProjmap < n - then loop (Map.size newProjmap) - else loop n \ No newline at end of file + loop n = do + projmap <- get + let numberOfComponents = Map.size projmap + componentSizes = fmap numBlocks . Map.elems $ projmap + maximalComponent = maximum componentSizes + totalSize = sum componentSizes + ms = MergerStats{..} + liftIO . print $ ms + case safeStrategy ms of + Stop -> return projmap + Continue -> do + let ((os, p3), _) = minComb n (Map.assocs projmap) + o3 = mconcat os + newProjmap = Map.insert o3 p3 . Map.withoutKeys projmap $ Set.fromList os + put newProjmap + if Map.size newProjmap < n + then loop (Map.size newProjmap) + else loop n \ No newline at end of file diff --git a/src/Partition.hs b/src/Partition.hs index 9a0aa1d..15a6212 100644 --- a/src/Partition.hs +++ b/src/Partition.hs @@ -1,15 +1,15 @@ -module Partition - ( module Partition - , module Data.Partition - ) where +module Partition ( + module Partition, + module Data.Partition, +) where import Preorder -import Control.Monad.Trans.State.Strict (runState, get, put) +import Control.Monad.Trans.State.Strict (get, put, runState) import Data.Coerce (coerce) import Data.Map.Strict qualified as Map -import Data.Partition (Partition(..), numStates, blockOfState, toBlocks) -import Data.Partition.Common (Block(..)) +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 @@ -29,7 +29,7 @@ commonRefinement p1 p2 = 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 } + 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 @@ -62,12 +62,13 @@ toPreorder Incomparable = IC' 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 + | 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/Preorder.hs b/src/Preorder.hs index db2fe53..643dbd1 100644 --- a/src/Preorder.hs +++ b/src/Preorder.hs @@ -1,14 +1,14 @@ -{-# language PatternSynonyms #-} +{-# 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. --} +-- \| +-- 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. import Control.Monad.Trans.Writer.Lazy (runWriter, tell) import Data.Bifunctor @@ -19,10 +19,15 @@ import Data.Set qualified as Set type PartialOrdering = Maybe Ordering pattern EQ', LT', GT', IC' :: PartialOrdering -pattern EQ' = Just EQ -- ^ Equivalent (or equal) -pattern LT' = Just LT -- ^ Strictly less than -pattern GT' = Just GT -- ^ Strictly greater than -pattern IC' = Nothing -- ^ Incomparable +pattern EQ' = Just EQ +-- \^ Equivalent (or equal) +pattern LT' = Just LT +-- \^ Strictly less than +pattern GT' = Just GT +-- \^ Strictly greater than +pattern IC' = Nothing + +-- \^ Incomparable -- | A preorder should satisfy reflexivity and transitivity. It is not assumed -- to be anti-symmetric. @@ -47,16 +52,16 @@ type Representatives a = [a] -- the representatives, they can be streamed. equivalenceClasses :: Ord l => Preorder x -> [(l, x)] -> (EquivalenceClasses l, Representatives (l, x)) equivalenceClasses comp ls = runWriter (go ls [] Map.empty) - where - -- end of list: return the classes - go [] _ classes = return classes - -- element x, we compare to all currently known representatives with 'find' - go (p@(l1, x):xs) repr classes = - case find (\(_, y) -> comp x y == EQ') repr of - -- If it is equivalent: insert in the map - Just (l2, _) -> go xs repr (Map.insert l1 l2 classes) - -- If not, add as representative, and output it - Nothing -> tell (pure p) >> go xs (p:repr) classes + where + -- end of list: return the classes + go [] _ classes = return classes + -- element x, we compare to all currently known representatives with 'find' + go (p@(l1, x) : xs) repr classes = + case find (\(_, y) -> comp x y == EQ') repr of + -- If it is equivalent: insert in the map + Just (l2, _) -> go xs repr (Map.insert l1 l2 classes) + -- If not, add as representative, and output it + Nothing -> tell (pure p) >> go xs (p : repr) classes -- * Order @@ -67,17 +72,17 @@ equivalenceClasses comp ls = runWriter (go ls [] Map.empty) -- algorithm, which requires fewer comparisons. But this one is simple. maximalElements :: Ord l => Preorder x -> [(l, x)] -> ([(l, x)], Map.Map l [l]) maximalElements comp ls = (maxs, downSets) - where - -- bigger first - ordPair p GT' = p - ordPair (l1, l2) LT' = (l2, l1) - ordPair _ _ = error "Cannot happen" - -- all elements in relation - rel = [ordPair (l1, l2) c | (l1, x1) <- ls, (l2, x2) <- ls, l1 < l2, let c = comp x1 x2, c /= IC'] - -- elements in second component are lower - lows = Set.fromList . fmap snd $ rel - -- keep everything which is not low - maxs = filter (\(l, _) -> l `Set.notMember` lows) ls - -- keep relations from the top elements, to form a map - maxRel = filter (\(l, _) -> l `Set.notMember` lows) rel - downSets = Map.fromListWith (++) . fmap (second pure) $ maxRel + where + -- bigger first + ordPair p GT' = p + ordPair (l1, l2) LT' = (l2, l1) + ordPair _ _ = error "Cannot happen" + -- all elements in relation + rel = [ordPair (l1, l2) c | (l1, x1) <- ls, (l2, x2) <- ls, l1 < l2, let c = comp x1 x2, c /= IC'] + -- elements in second component are lower + lows = Set.fromList . fmap snd $ rel + -- keep everything which is not low + maxs = filter (\(l, _) -> l `Set.notMember` lows) ls + -- keep relations from the top elements, to form a map + maxRel = filter (\(l, _) -> l `Set.notMember` lows) rel + downSets = Map.fromListWith (++) . fmap (second pure) $ maxRel diff --git a/src/SplittingTree.hs b/src/SplittingTree.hs index 63b8dbb..e0fa5f2 100644 --- a/src/SplittingTree.hs +++ b/src/SplittingTree.hs @@ -1,13 +1,14 @@ -{-# language PartialTypeSignatures #-} +{-# LANGUAGE PartialTypeSignatures #-} {-# OPTIONS_GHC -Wno-partial-type-signatures #-} module SplittingTree where import Control.Monad.Trans.Class import Control.Monad.Trans.State -import Data.Map.Strict qualified as Map import Data.Coerce (coerce) +import Data.Foldable (traverse_) import Data.List (sortOn) +import Data.Map.Strict qualified as Map newtype Block = Block Int deriving (Eq, Ord, Read, Show, Enum) @@ -16,7 +17,7 @@ newtype Block = Block Int -- same block are equivalent. Note that a permutation of the blocks will -- not change the partition, but it does change the underlying representation. -- (That is why I haven't given it an Eq instance yet.) -newtype Partition s = Partition { getPartition :: Map.Map s Block } +newtype Partition s = Partition {getPartition :: Map.Map s Block} deriving (Read, Show) -- Determines whether two elements are equivalent in the partition. @@ -63,33 +64,36 @@ data PRState s i o = PRState deriving (Show) updatePartition :: (Monad m, Ord s) => s -> Block -> StateT (PRState s i o) m () -updatePartition s b = modify foo where - foo prs = prs { partition = coerce (Map.insert s b) (partition prs) } +updatePartition s b = modify foo + where + foo prs = prs{partition = coerce (Map.insert s b) (partition prs)} updateSize :: Monad m => Block -> Int -> StateT (PRState s i o) m Int updateSize b n = - modify (\prs -> prs { splittingTree = (splittingTree prs) { size = Map.insert b n (size (splittingTree prs)) }}) - >> return n + modify (\prs -> prs{splittingTree = (splittingTree prs){size = Map.insert b n (size (splittingTree prs))}}) + >> return n genNextBlockId :: Monad m => StateT (PRState s i o) m Block genNextBlockId = do idx <- gets nextBlockId - modify (\prs -> prs { nextBlockId = succ (nextBlockId prs) }) + modify (\prs -> prs{nextBlockId = succ (nextBlockId prs)}) return idx updateParent :: Monad m => Either Block InnerNode -> InnerNode -> o -> StateT (PRState s i o) m () -updateParent (Left block) target output = modify foo where - foo prs = prs { splittingTree = (splittingTree prs) { blockParent = Map.insert block (target, output) (blockParent (splittingTree prs)) }} -updateParent (Right node) target output = modify foo where - foo prs = prs { splittingTree = (splittingTree prs) { innerParent = Map.insert node (target, output) (innerParent (splittingTree prs)) }} +updateParent (Left block) target output = modify foo + where + foo prs = prs{splittingTree = (splittingTree prs){blockParent = Map.insert block (target, output) (blockParent (splittingTree prs))}} +updateParent (Right node) target output = modify foo + where + foo prs = prs{splittingTree = (splittingTree prs){innerParent = Map.insert node (target, output) (innerParent (splittingTree prs))}} updateLabel :: Monad m => InnerNode -> [i] -> StateT (PRState s i o) m () -updateLabel node witness = modify (\prs -> prs { splittingTree = (splittingTree prs) { label = Map.insert node witness (label (splittingTree prs)) }}) +updateLabel node witness = modify (\prs -> prs{splittingTree = (splittingTree prs){label = Map.insert node witness (label (splittingTree prs))}}) genNextNodeId :: Monad m => StateT (PRState s i o) m InnerNode genNextNodeId = do idx <- gets nextNodeId - modify (\prs -> prs { nextNodeId = succ (nextNodeId prs) }) + modify (\prs -> prs{nextNodeId = succ (nextNodeId prs)}) return idx refineWithSplitter :: (Monad m, Ord o, Ord s) => i -> (s -> [s]) -> Splitter s i o -> StateT (PRState s i o) m [Splitter s i o] @@ -111,10 +115,10 @@ refineWithSplitter action rev Splitter{..} = do tempChildsMaps = Map.map (Map.fromListWith (++)) . Map.fromListWith (++) $ tempChildsList -- Now we need to check the 3-way split: - -- * Some blocks have no states which occured, these don't appear. - -- * Some blocks have all states move to a single subblock, this is not a + -- \* Some blocks have no states which occured, these don't appear. + -- \* Some blocks have all states move to a single subblock, this is not a -- proper split and should be removed. - -- * Some blocks have different outputs (a proper split) or states which + -- \* Some blocks have different outputs (a proper split) or states which -- moved and states which didn't. properSplit b os | Map.null os = error "Should not happen" @@ -130,7 +134,7 @@ refineWithSplitter action rev Splitter{..} = do -- Create a new sub-block nBIdx <- genNextBlockId -- Set all states to that id - mapM_ (\s -> updatePartition s nBIdx) ls + mapM_ (`updatePartition` nBIdx) ls -- And update the tree updateParent (Left nBIdx) nNIdx o n <- updateSize nBIdx (length ls) @@ -153,7 +157,7 @@ refineWithSplitter action rev Splitter{..} = do -- and nNIdx a child of the current parent of b. -- And we update the witness by prepending the action let (currentParent, op) = blockParent currentSplittingTree Map.! b - newWitness = action:witness + newWitness = action : witness updateParent (Right nNIdx) currentParent op updateParent (Left b) nNIdx leftOut updateLabel nNIdx newWitness @@ -163,21 +167,24 @@ refineWithSplitter action rev Splitter{..} = do -- sure it's worth the effort, so we only do it when we can remove a -- subblock. if missingSize == 0 - then let ls = Map.toList sizesAndSubblocks - -- TODO: sort(On) is unnecessarily expensive, we only need to - -- know the biggest... - ((o1, _) : smallerBlocks) = sortOn (\(_, (n, _)) -> -n) ls - in - return Splitter - { split = Map.fromList (fmap (\(o, (_, lss)) -> (o, lss)) smallerBlocks) - , leftOut = o1 - , witness = newWitness - } - else return Splitter - { split = Map.map snd sizesAndSubblocks - , leftOut = leftOut - , witness = newWitness - } + then + let ls = Map.toList sizesAndSubblocks + -- TODO: sort(On) is unnecessarily expensive, we only need to + -- know the biggest... + ((o1, _) : smallerBlocks) = sortOn (\(_, (n, _)) -> -n) ls + in return + Splitter + { split = Map.fromList (fmap (\(o, (_, lss)) -> (o, lss)) smallerBlocks) + , leftOut = o1 + , witness = newWitness + } + else + return + Splitter + { split = Map.map snd sizesAndSubblocks + , leftOut = leftOut + , witness = newWitness + } Map.elems <$> Map.traverseWithKey updateBlock tempChildsMaps2 @@ -197,14 +204,14 @@ refineWithOutput action out = do tempChildsMaps2 = Map.filter (\children -> Map.size children >= 2) tempChildsMaps updateStates nNIdx o ss = do - -- Create a new sub-block - nBIdx <- genNextBlockId - -- Set all states to that id - mapM_ (\s -> updatePartition s nBIdx) ss - -- And update the tree - updateParent (Left nBIdx) nNIdx o - _ <- updateSize nBIdx (length ss) - return () + -- Create a new sub-block + nBIdx <- genNextBlockId + -- Set all states to that id + mapM_ (`updatePartition` nBIdx) ss + -- And update the tree + updateParent (Left nBIdx) nNIdx o + _ <- updateSize nBIdx (length ss) + return () updateBlock b children = do -- We skip the biggest part, and don't update the blocks. @@ -213,7 +220,7 @@ refineWithOutput action out = do -- For the remaining blocks, we update the partition nNIdx <- genNextNodeId - _ <- traverse (\(o, ss) -> updateStates nNIdx o ss) smaller + traverse_ (uncurry (updateStates nNIdx)) smaller -- If we are doing the very first split, the nNIdx node does not have a -- parent. So we don't have to do updates. Now nNIdx will be the root. @@ -228,34 +235,37 @@ refineWithOutput action out = do _ <- updateSize b (length biggest) -- Return the splitter, not that we already skipped the larger part. - return Splitter - { split = Map.fromList smaller - , leftOut = o1 - , witness = witness - } + return + Splitter + { split = Map.fromList smaller + , leftOut = o1 + , witness = witness + } Map.elems <$> Map.traverseWithKey updateBlock tempChildsMaps2 initialPRState :: Ord s => [s] -> PRState s i o -initialPRState ls = PRState - { partition = Partition . Map.fromList $ [(s, Block 0) | s <- ls] - , nextBlockId = Block 1 - , splittingTree = SplittingTree - { label = Map.empty - , innerParent = Map.empty - , blockParent = Map.empty - , size = Map.singleton (Block 0) (length ls) +initialPRState ls = + PRState + { partition = Partition . Map.fromList $ [(s, Block 0) | s <- ls] + , nextBlockId = Block 1 + , splittingTree = + SplittingTree + { label = Map.empty + , innerParent = Map.empty + , blockParent = Map.empty + , size = Map.singleton (Block 0) (length ls) + } + , nextNodeId = Node 0 } - , nextNodeId = Node 0 - } -refineWithAllOutputs :: (Monad m, Ord o, Ord s) => [(i, (s -> o))] -> StateT (PRState s i o) m [Splitter s i o] +refineWithAllOutputs :: (Monad m, Ord o, Ord s) => [(i, s -> o)] -> StateT (PRState s i o) m [Splitter s i o] refineWithAllOutputs ls = concat <$> traverse (uncurry refineWithOutput) ls -refineWithSplitterAllInputs :: (Monad m, Ord o, Ord s) => [(i, (s -> [s]))] -> Splitter s i o -> StateT (PRState s i o) m [Splitter s i o] +refineWithSplitterAllInputs :: (Monad m, Ord o, Ord s) => [(i, s -> [s])] -> Splitter s i o -> StateT (PRState s i o) m [Splitter s i o] refineWithSplitterAllInputs ls splitter = concat <$> traverse (\(i, rev) -> refineWithSplitter i rev splitter) ls -refine :: (Monad m, Ord o, Ord s) => ([i] -> m ()) -> [(i, (s -> o))] -> [(i, (s -> [s]))] -> StateT (PRState s i o) m () +refine :: (Monad m, Ord o, Ord s) => ([i] -> m ()) -> [(i, s -> o)] -> [(i, s -> [s])] -> StateT (PRState s i o) m () refine ping outputs transitionsReverse = do initialQueue <- refineWithAllOutputs outputs diff --git a/src/StateIdentifiers.hs b/src/StateIdentifiers.hs index 85a7ca6..5c3b9b3 100644 --- a/src/StateIdentifiers.hs +++ b/src/StateIdentifiers.hs @@ -1,14 +1,14 @@ module StateIdentifiers where import SplittingTree -import Trie qualified as Trie +import Trie qualified import Data.Map.Strict qualified as Map stateIdentifierFor :: (Ord i, Ord s) => s -> Partition s -> SplittingTree s i o -> Trie.Trie i -stateIdentifierFor state Partition{..} SplittingTree{..} = go firstNode where +stateIdentifierFor state Partition{..} SplittingTree{..} = go firstNode + where firstNode = fst <$> blockParent Map.!? (getPartition Map.! state) getParent n = fst <$> innerParent Map.!? n go Nothing = Trie.empty go (Just n) = Trie.insert (label Map.! n) (go (getParent n)) - diff --git a/src/Trie.hs b/src/Trie.hs index 743499d..73a9507 100644 --- a/src/Trie.hs +++ b/src/Trie.hs @@ -21,12 +21,12 @@ singleton = Leaf insert :: Ord i => [i] -> Trie i -> Trie i insert [] t = t insert w (Leaf []) = Leaf w -insert (a:w1) (Leaf (b:w2)) +insert (a : w1) (Leaf (b : w2)) | a == b = case insert w1 (Leaf w2) of - Leaf w3 -> Leaf (a:w3) - node -> Node (Map.singleton a node) + Leaf w3 -> Leaf (a : w3) + node -> Node (Map.singleton a node) | otherwise = Node (Map.fromList [(a, Leaf w1), (b, Leaf w2)]) -insert (a:w1) (Node m) = Node (Map.insertWith union a (Leaf w1) m) +insert (a : w1) (Node m) = Node (Map.insertWith union a (Leaf w1) m) union :: Ord i => Trie i -> Trie i -> Trie i union (Leaf w) t = insert w t @@ -37,4 +37,4 @@ union (Node m1) (Node m2) = -- Without common prefixes toList :: Trie i -> [[i]] toList (Leaf w) = [w] -toList (Node m) = Map.foldMapWithKey (\a t -> fmap (a:) . toList $ t) m +toList (Node m) = Map.foldMapWithKey (\a t -> fmap (a :) . toList $ t) m