mirror of
https://git.cs.ou.nl/joshua.moerman/mealy-decompose.git
synced 2025-04-30 02:07:44 +02:00
more formatting
This commit is contained in:
Joshua Moerman
parent
8223ff9d59
commit
646b915d36
15 changed files with 425 additions and 387 deletions
|
|
@ -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,7 +27,8 @@ main = do
|
|||
print dotFile
|
||||
transitions <- mapMaybe (parseMaybe parseTransFull) . lines <$> readFile dotFile
|
||||
|
||||
let machine = convertToMealy transitions
|
||||
let
|
||||
machine = convertToMealy transitions
|
||||
alphabet = inputs machine
|
||||
tInit = initialState machine
|
||||
tOut s i = fst (behaviour machine s i)
|
||||
|
|
@ -37,7 +37,7 @@ main = do
|
|||
mq0 = semanticsForState machine (initialState machine)
|
||||
mq = countingMQ (\w -> when debugOutput (print w) >> return (mq0 w))
|
||||
|
||||
let loop table = do
|
||||
loop table = do
|
||||
lift $ putStrLn "Making the table closed and consistent"
|
||||
(table2, b) <- makeClosedAndConsistentA mq table
|
||||
let (hInit, size, hTransMap, hOutMap) = createHypothesis table2
|
||||
|
|
|
|||
88
app/Main.hs
88
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,19 +68,23 @@ 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"]
|
||||
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
|
||||
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)
|
||||
let
|
||||
preord p1 p2 = toPreorder (comparePartitions p1 p2)
|
||||
(equiv, uniqPartitions) = equivalenceClasses preord projections
|
||||
|
||||
putStrLn ""
|
||||
|
|
@ -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
|
||||
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
|
||||
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]
|
||||
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 ""
|
||||
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
|
||||
)
|
||||
|
||||
(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,21 +162,21 @@ 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
|
||||
|
|
@ -176,7 +186,5 @@ main = do
|
|||
|
||||
putStrLn $ "Output (reduced machine) in file " <> filename2
|
||||
myWriteFile filename2 content2
|
||||
)
|
||||
)
|
||||
|
||||
return ()
|
||||
mapM_ action projmapN
|
||||
|
|
|
|||
|
|
@ -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) =
|
||||
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)
|
||||
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
|
||||
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
@ -34,8 +32,6 @@ equate x y (MkUnionFind m1) =
|
|||
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
|
||||
|
|
@ -53,7 +49,7 @@ bisimulation alphabet output transition x y = go (Seq.singleton ([], x, y)) empt
|
|||
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
|
||||
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
|
||||
|
|
|
|||
|
|
@ -49,18 +49,20 @@ parseTransFull :: Parser Trans
|
|||
parseTransFull = space *> parseTrans <* eof
|
||||
|
||||
convertToMealy :: [Trans] -> MealyMachine String String String
|
||||
convertToMealy l = MealyMachine
|
||||
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
|
||||
, behaviour = curry (base Map.!)
|
||||
, initialState = (\(a, _, _, _) -> a) . head $ l
|
||||
}
|
||||
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
|
||||
-- \^ 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
|
||||
|
|
|
|||
12
src/LStar.hs
12
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
|
||||
|
||||
|
||||
------------------
|
||||
|
|
|
|||
|
|
@ -15,8 +15,9 @@ 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"]
|
||||
exampleMM = MealyMachine{..}
|
||||
where
|
||||
states = ["q0", "q1", "q2", "q3"]
|
||||
inputs = ['a', 'b']
|
||||
outputs = ["een", "twee", "drie", "vier"]
|
||||
behaviour "q0" 'a' = ("een", "q1")
|
||||
|
|
@ -29,4 +30,3 @@ exampleMM =
|
|||
behaviour "q3" 'b' = ("twee", "q1")
|
||||
behaviour _ _ = error "undefined behaviour of exampleMM"
|
||||
initialState = "q0"
|
||||
in MealyMachine{..}
|
||||
|
|
|
|||
|
|
@ -5,18 +5,19 @@ 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
|
||||
project f MealyMachine{..} =
|
||||
MealyMachine
|
||||
{ outputs = nubSort $ fmap f outputs -- inefficient
|
||||
, behaviour = \s i -> case behaviour s i of
|
||||
(out, s2) -> (f out, s2)
|
||||
|
|
@ -28,7 +29,8 @@ 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
|
||||
where
|
||||
oMaybe o
|
||||
| oPred o = Just o
|
||||
| otherwise = Nothing
|
||||
|
||||
|
|
@ -41,23 +43,29 @@ 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
|
||||
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
|
||||
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)))
|
||||
, 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
|
||||
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))))
|
||||
, 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{..}
|
||||
|
|
|
|||
|
|
@ -29,7 +29,8 @@ heuristicMerger components strategy = do
|
|||
return $ Map.assocs projmap
|
||||
where
|
||||
score ps p3 = numBlocks p3 - sum (fmap numBlocks ps)
|
||||
combine ops = let os = fmap fst ops
|
||||
combine ops =
|
||||
let os = fmap fst ops
|
||||
ps = fmap snd ops
|
||||
p3 = foldr1 commonRefinement ps
|
||||
in ((os, p3), score ps p3)
|
||||
|
|
|
|||
|
|
@ -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,7 +62,8 @@ toPreorder Incomparable = IC'
|
|||
comparePartitions :: Partition -> Partition -> Comparison
|
||||
comparePartitions p1 p2
|
||||
| p1 == p2 = Equivalent
|
||||
| otherwise = let glb = commonRefinement p1 p2
|
||||
| otherwise =
|
||||
let glb = commonRefinement p1 p2
|
||||
n1 = numBlocks p1
|
||||
n2 = numBlocks p2
|
||||
n3 = numBlocks glb
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
@ -51,12 +56,12 @@ equivalenceClasses comp ls = runWriter (go ls [] Map.empty)
|
|||
-- 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 =
|
||||
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
|
||||
Nothing -> tell (pure p) >> go xs (p : repr) classes
|
||||
|
||||
-- * Order
|
||||
|
||||
|
|
|
|||
|
|
@ -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)) }})
|
||||
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,17 +167,20 @@ 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
|
||||
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
|
||||
in return
|
||||
Splitter
|
||||
{ split = Map.fromList (fmap (\(o, (_, lss)) -> (o, lss)) smallerBlocks)
|
||||
, leftOut = o1
|
||||
, witness = newWitness
|
||||
}
|
||||
else return Splitter
|
||||
else
|
||||
return
|
||||
Splitter
|
||||
{ split = Map.map snd sizesAndSubblocks
|
||||
, leftOut = leftOut
|
||||
, witness = newWitness
|
||||
|
|
@ -200,7 +207,7 @@ refineWithOutput action out = do
|
|||
-- Create a new sub-block
|
||||
nBIdx <- genNextBlockId
|
||||
-- Set all states to that id
|
||||
mapM_ (\s -> updatePartition s nBIdx) ss
|
||||
mapM_ (`updatePartition` nBIdx) ss
|
||||
-- And update the tree
|
||||
updateParent (Left nBIdx) nNIdx o
|
||||
_ <- updateSize nBIdx (length ss)
|
||||
|
|
@ -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,7 +235,8 @@ refineWithOutput action out = do
|
|||
_ <- updateSize b (length biggest)
|
||||
|
||||
-- Return the splitter, not that we already skipped the larger part.
|
||||
return Splitter
|
||||
return
|
||||
Splitter
|
||||
{ split = Map.fromList smaller
|
||||
, leftOut = o1
|
||||
, witness = witness
|
||||
|
|
@ -237,10 +245,12 @@ refineWithOutput action out = do
|
|||
Map.elems <$> Map.traverseWithKey updateBlock tempChildsMaps2
|
||||
|
||||
initialPRState :: Ord s => [s] -> PRState s i o
|
||||
initialPRState ls = PRState
|
||||
initialPRState ls =
|
||||
PRState
|
||||
{ partition = Partition . Map.fromList $ [(s, Block 0) | s <- ls]
|
||||
, nextBlockId = Block 1
|
||||
, splittingTree = SplittingTree
|
||||
, splittingTree =
|
||||
SplittingTree
|
||||
{ label = Map.empty
|
||||
, innerParent = Map.empty
|
||||
, blockParent = Map.empty
|
||||
|
|
@ -249,13 +259,13 @@ initialPRState ls = PRState
|
|||
, 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
|
||||
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue