mirror of
https://git.cs.ou.nl/joshua.moerman/mealy-decompose.git
synced 2025-04-29 17:57:44 +02:00
Added command line option
This commit is contained in:
parent
7deb8e8e1c
commit
3ea28601db
5 changed files with 84 additions and 33 deletions
36
app/Main.hs
36
app/Main.hs
|
@ -24,19 +24,30 @@ import Data.Text.IO qualified as T
|
|||
import Data.Text.Lazy.IO qualified as TL
|
||||
import Data.Tuple (swap)
|
||||
import System.Environment
|
||||
import System.Exit (exitFailure)
|
||||
|
||||
extraChecks :: Bool
|
||||
extraChecks = False
|
||||
|
||||
main :: IO ()
|
||||
main = do
|
||||
-- COMMAND LINE
|
||||
---------------
|
||||
ls <- getArgs
|
||||
case ls of
|
||||
[dotFile] -> mainFun dotFile 2
|
||||
[dotFile, cs] -> mainFun dotFile (read cs)
|
||||
_ -> do
|
||||
putStrLn "Please provide a dot file as argument"
|
||||
exitFailure
|
||||
|
||||
mainFun :: String -> Int -> IO ()
|
||||
mainFun dotFile numComponents = do
|
||||
let
|
||||
report str = appendFile "results/log.txt" (dotFile <> "\t" <> str <> "\n")
|
||||
|
||||
-- READING INPUT
|
||||
----------------
|
||||
ls <- getArgs
|
||||
let dotFile = case ls of
|
||||
[x] -> x
|
||||
_ -> error "Please provide exactly one argument (filepath of dot file)"
|
||||
|
||||
putStrLn $ "reading " <> dotFile
|
||||
machine <- readDotFile dotFile
|
||||
|
||||
|
@ -80,9 +91,16 @@ main = do
|
|||
-- Then we try to combine paritions, so that we don't end up with
|
||||
-- too many components. (Which would be too big to be useful.)
|
||||
-----------------------------------------------------------------
|
||||
let strategy MergerStats{..}
|
||||
| numberOfComponents <= 4 = Stop
|
||||
| otherwise = Continue
|
||||
let
|
||||
numStrategy current
|
||||
| numberOfComponents current <= numComponents = StopWith (value current)
|
||||
| otherwise = Continue
|
||||
prevStrategy current = case previous current of
|
||||
Just prev -> if (totalSize prev < totalSize current) then StopWith (value prev) else Continue
|
||||
_ -> Continue
|
||||
strategy c = case prevStrategy c of
|
||||
StopWith x -> StopWith x
|
||||
Continue -> numStrategy c
|
||||
|
||||
putStrLn $ "\nHeuristic merging"
|
||||
projmap <- heuristicMerger topMods strategy
|
||||
|
@ -92,6 +110,8 @@ main = do
|
|||
putStrLn $ " sizes: " <> show (fmap (numBlocks . snd) projmap)
|
||||
putStrLn "Start writing output files"
|
||||
|
||||
report $ "PAR-BIT-DECOMP" <> "\t" <> (show (length (states machine))) <> "\t" <> (show (length (inputs machine))) <> "\t" <> (show (length (outputs machine))) <> "\t" <> show (length projmap) <> "\t" <> show (sum (fmap (numBlocks . snd) projmap)) <> "\t" <> show (fmap (numBlocks . snd) projmap)
|
||||
|
||||
-- OUTPUT
|
||||
---------
|
||||
let
|
||||
|
|
|
@ -15,6 +15,7 @@ import Data.List qualified as List
|
|||
import Data.Map.Strict qualified as Map
|
||||
import Data.Maybe (isJust)
|
||||
import Data.Set qualified as Set
|
||||
import Data.Text qualified as T
|
||||
import System.Environment (getArgs)
|
||||
import System.Exit (exitFailure, exitSuccess)
|
||||
|
||||
|
@ -85,10 +86,17 @@ mainInputDecomp args = case args of
|
|||
_ -> putStrLn "Please provide a dot file"
|
||||
where
|
||||
run dotFile = do
|
||||
let
|
||||
report str = appendFile "results/log.txt" (dotFile <> "\t" <> str <> "\n")
|
||||
witness str = appendFile "results/witnesses.txt" (dotFile <> "\n" <> str <> "\n\n")
|
||||
|
||||
report "START-INPUT-DECOMP"
|
||||
model <- readDotFile dotFile
|
||||
putStr $ "states: " <> show (length (states model)) <> "; "
|
||||
putStr $ "inputs: " <> show (length (inputs model)) <> "; "
|
||||
putStr $ " outputs: " <> show (length (outputs model)) <> "\n"
|
||||
let
|
||||
inputSizes = [length (f model) | f <- [states, inputs, outputs]]
|
||||
|
||||
report $ "INPUT" <> "\t" <> show inputSizes
|
||||
putStrLn $ "[states, inputs, outputs] = " <> show inputSizes
|
||||
|
||||
let
|
||||
composition i j = interleavingComposition [[i], [j]] model
|
||||
|
@ -112,9 +120,16 @@ mainInputDecomp args = case args of
|
|||
classes = List.unfoldr (step closure) (inputs model)
|
||||
|
||||
case length classes of
|
||||
0 -> putStrLn "ERROR" >> exitFailure
|
||||
1 -> putStrLn "INDECOMPOSABLE" >> exitSuccess
|
||||
n -> putStrLn ("MAYBE DECOMPOSABLE: " ++ show n ++ " classes")
|
||||
0 -> do
|
||||
report "ERROR"
|
||||
exitFailure
|
||||
1 -> do
|
||||
report "INDECOMPOSABLE"
|
||||
putStrLn "INDECOMPOSABLE"
|
||||
exitSuccess
|
||||
n -> do
|
||||
report $ "MAYBE DECOMPOSABLE" <> "\t" <> show n
|
||||
putStrLn ("MAYBE DECOMPOSABLE: " ++ show n ++ " classes")
|
||||
|
||||
let
|
||||
loop currentClosure currentClasses = do
|
||||
|
@ -158,6 +173,12 @@ mainInputDecomp args = case args of
|
|||
return (p, p * length cls)
|
||||
|
||||
putStrLn $ "Final classes " <> show (length finalClasses)
|
||||
(stateSizes, transitionSizes) <- unzip <$> mapM action finalClasses
|
||||
putStrLn $ "Total size = " <> show (sum stateSizes)
|
||||
putStrLn $ "Total transitions = " <> show (sum transitionSizes)
|
||||
(sizes, transitions) <- unzip <$> mapM action finalClasses
|
||||
|
||||
witness $ T.unpack . T.unlines . fmap T.unwords $ classes
|
||||
report $ "DECOMPOSABLE" <> "\t" <> show sizes <> "\t" <> show transitions
|
||||
|
||||
putStrLn "DECOMPOSABLE"
|
||||
putStrLn $ "Total size = " <> show (sum sizes)
|
||||
putStrLn $ "Total transitions = " <> show (sum transitions)
|
||||
exitSuccess
|
||||
|
|
|
@ -92,7 +92,7 @@ def parse_dot_file(lines):
|
|||
(l, _, _) = r.partition('"]')
|
||||
(i, _, o) = l.partition('/')
|
||||
|
||||
return (s, i, o, t)
|
||||
return (s.strip(), i.strip(), o.strip(), t.strip())
|
||||
|
||||
initial_state = None
|
||||
states, inputs, outputs = set(), set(), set()
|
||||
|
|
|
@ -55,7 +55,7 @@ parseTrans = assoc <$> identifierQ <* symbol "->" <*> identifierQ <*> brackets p
|
|||
lexeme = L.lexeme sc
|
||||
symbol = L.symbol sc
|
||||
-- state, input, output is any string of alphaNumChar's (and some additional characters)
|
||||
isAlphaNumExtra c = isAlphaNum c || ('(' <= c && c <= '.') || c == '_'
|
||||
isAlphaNumExtra c = isAlphaNum c || ('(' <= c && c <= '.') || c == '_' || c == '|' || c==':' || c == ';'
|
||||
alphaNumCharExtra = takeWhile1P (Just "alphanumeric character or extra") isAlphaNumExtra
|
||||
identifier = lexeme alphaNumCharExtra
|
||||
identifierQ = identifier <|> between (symbol "\"") (symbol "\"") identifier
|
||||
|
|
|
@ -11,22 +11,30 @@ import Data.Map.Strict qualified as Map
|
|||
import Data.Ord (comparing)
|
||||
import Data.Set qualified as Set
|
||||
|
||||
data MergerStats = MergerStats
|
||||
data MergerStats o s = MergerStats
|
||||
{ numberOfComponents :: Int
|
||||
, maximalComponent :: Block
|
||||
, totalSize :: Block
|
||||
, value :: [([o], Partition s)]
|
||||
, previous :: Maybe (MergerStats o s)
|
||||
}
|
||||
deriving (Eq, Ord, Show)
|
||||
deriving (Show)
|
||||
|
||||
data MergerAction = Stop | Continue
|
||||
deriving (Eq, Ord, Show)
|
||||
printStats :: MergerStats o s -> IO ()
|
||||
printStats MergerStats{..} = do
|
||||
putStr $ "MergerStats = Number of components: " <> show numberOfComponents
|
||||
putStr $ ", Maximal component: " <> show maximalComponent
|
||||
putStrLn $ ", Total size: " <> show totalSize
|
||||
|
||||
type MergerStrategy = MergerStats -> MergerAction
|
||||
data MergerAction o s = StopWith [([o], Partition s)] | Continue
|
||||
deriving (Show)
|
||||
|
||||
heuristicMerger :: (Ord o, Ord s) => [(o, Partition s)] -> MergerStrategy -> IO [([o], Partition s)]
|
||||
type MergerStrategy o s = MergerStats o s -> MergerAction o s
|
||||
|
||||
heuristicMerger :: (Ord o, Ord s) => [(o, Partition s)] -> MergerStrategy o s -> IO [([o], Partition s)]
|
||||
heuristicMerger components strategy = do
|
||||
projmap <- evalStateT (loop 2) (Map.fromList (fmap (first pure) components))
|
||||
return $ Map.assocs projmap
|
||||
projmap <- evalStateT (loop Nothing 2) (Map.fromList (fmap (first pure) components))
|
||||
return $ projmap
|
||||
where
|
||||
score ps p3 = numBlocks p3 - sum (fmap numBlocks ps)
|
||||
combine ops =
|
||||
|
@ -38,24 +46,26 @@ heuristicMerger components strategy = do
|
|||
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
|
||||
| numberOfComponents <= 1 = StopWith value
|
||||
| otherwise = strategy ms
|
||||
|
||||
loop n = do
|
||||
loop prevMS n = do
|
||||
projmap <- get
|
||||
let numberOfComponents = Map.size projmap
|
||||
componentSizes = fmap numBlocks . Map.elems $ projmap
|
||||
maximalComponent = maximum componentSizes
|
||||
totalSize = sum componentSizes
|
||||
previous = prevMS
|
||||
value = Map.assocs projmap
|
||||
ms = MergerStats{..}
|
||||
liftIO . print $ ms
|
||||
liftIO . printStats $ ms
|
||||
case safeStrategy ms of
|
||||
Stop -> return projmap
|
||||
StopWith pm -> return pm
|
||||
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
|
||||
then loop (Just ms) (Map.size newProjmap)
|
||||
else loop (Just ms) n
|
||||
|
|
Loading…
Add table
Reference in a new issue