diff --git a/README.md b/README.md index 3803165..6c8c53e 100644 --- a/README.md +++ b/README.md @@ -16,9 +16,9 @@ machines (FSMs). Notable entry points are: ## How to run -The the haskell tools (tested with ghc 9.2.8 and ghc 9.10.1): +The the haskell tools (tested with ghc 9.2.8, ghc 9.4.8, and ghc 9.10.1): ``` -cabal run mealy-decompose-main -- +cabal run mealy-decompose-main -- -h ``` For the python tools (tested with python 3.12): diff --git a/hs/LICENSE b/hs/LICENSE new file mode 100644 index 0000000..f413340 --- /dev/null +++ b/hs/LICENSE @@ -0,0 +1,287 @@ +EUROPEAN UNION PUBLIC LICENCE v. 1.2 +EUPL © the European Union 2007, 2016 + +This European Union Public Licence (the ‘EUPL’) applies to the Work (as defined +below) which is provided under the terms of this Licence. Any use of the Work, +other than as authorised under this Licence is prohibited (to the extent such +use is covered by a right of the copyright holder of the Work). + +The Work is provided under the terms of this Licence when the Licensor (as +defined below) has placed the following notice immediately following the +copyright notice for the Work: + +Licensed under the EUPL + +or has expressed by any other means his willingness to license under the EUPL. + +1. Definitions + +In this Licence, the following terms have the following meaning: + +- ‘The Licence’: this Licence. + +- ‘The Original Work’: the work or software distributed or communicated by the +Licensor under this Licence, available as Source Code and also as Executable +Code as the case may be. + +- ‘Derivative Works’: the works or software that could be created by the +Licensee, based upon the Original Work or modifications thereof. This Licence +does not define the extent of modification or dependence on the Original Work +required in order to classify a work as a Derivative Work; this extent is +determined by copyright law applicable in the country mentioned in Article 15. + +- ‘The Work’: the Original Work or its Derivative Works. + +- ‘The Source Code’: the human-readable form of the Work which is the most +convenient for people to study and modify. + +- ‘The Executable Code’: any code which has generally been compiled and which is +meant to be interpreted by a computer as a program. + +- ‘The Licensor’: the natural or legal person that distributes or communicates +the Work under the Licence. + +- ‘Contributor(s)’: any natural or legal person who modifies the Work under the +Licence, or otherwise contributes to the creation of a Derivative Work. + +- ‘The Licensee’ or ‘You’: any natural or legal person who makes any usage of +the Work under the terms of the Licence. + +- ‘Distribution’ or ‘Communication’: any act of selling, giving, lending, +renting, distributing, communicating, transmitting, or otherwise making +available, online or offline, copies of the Work or providing access to its +essential functionalities at the disposal of any other natural or legal +person. + +2. Scope of the rights granted by the Licence + +The Licensor hereby grants You a worldwide, royalty-free, non-exclusive, +sublicensable licence to do the following, for the duration of copyright vested +in the Original Work: + +- use the Work in any circumstance and for all usage, +- reproduce the Work, +- modify the Work, and make Derivative Works based upon the Work, +- communicate to the public, including the right to make available or display +the Work or copies thereof to the public and perform publicly, as the case may +be, the Work, +- distribute the Work or copies thereof, +- lend and rent the Work or copies thereof, +- sublicense rights in the Work or copies thereof. + +Those rights can be exercised on any media, supports and formats, whether now +known or later invented, as far as the applicable law permits so. + +In the countries where moral rights apply, the Licensor waives his right to +exercise his moral right to the extent allowed by law in order to make effective +the licence of the economic rights here above listed. + +The Licensor grants to the Licensee royalty-free, non-exclusive usage rights to +any patents held by the Licensor, to the extent necessary to make use of the +rights granted on the Work under this Licence. + +3. Communication of the Source Code + +The Licensor may provide the Work either in its Source Code form, or as +Executable Code. If the Work is provided as Executable Code, the Licensor +provides in addition a machine-readable copy of the Source Code of the Work +along with each copy of the Work that the Licensor distributes or indicates, in +a notice following the copyright notice attached to the Work, a repository where +the Source Code is easily and freely accessible for as long as the Licensor +continues to distribute or communicate the Work. + +4. Limitations on copyright + +Nothing in this Licence is intended to deprive the Licensee of the benefits from +any exception or limitation to the exclusive rights of the rights owners in the +Work, of the exhaustion of those rights or of other applicable limitations +thereto. + +5. Obligations of the Licensee + +The grant of the rights mentioned above is subject to some restrictions and +obligations imposed on the Licensee. Those obligations are the following: + +Attribution right: The Licensee shall keep intact all copyright, patent or +trademarks notices and all notices that refer to the Licence and to the +disclaimer of warranties. The Licensee must include a copy of such notices and a +copy of the Licence with every copy of the Work he/she distributes or +communicates. The Licensee must cause any Derivative Work to carry prominent +notices stating that the Work has been modified and the date of modification. + +Copyleft clause: If the Licensee distributes or communicates copies of the +Original Works or Derivative Works, this Distribution or Communication will be +done under the terms of this Licence or of a later version of this Licence +unless the Original Work is expressly distributed only under this version of the +Licence — for example by communicating ‘EUPL v. 1.2 only’. The Licensee +(becoming Licensor) cannot offer or impose any additional terms or conditions on +the Work or Derivative Work that alter or restrict the terms of the Licence. + +Compatibility clause: If the Licensee Distributes or Communicates Derivative +Works or copies thereof based upon both the Work and another work licensed under +a Compatible Licence, this Distribution or Communication can be done under the +terms of this Compatible Licence. For the sake of this clause, ‘Compatible +Licence’ refers to the licences listed in the appendix attached to this Licence. +Should the Licensee's obligations under the Compatible Licence conflict with +his/her obligations under this Licence, the obligations of the Compatible +Licence shall prevail. + +Provision of Source Code: When distributing or communicating copies of the Work, +the Licensee will provide a machine-readable copy of the Source Code or indicate +a repository where this Source will be easily and freely available for as long +as the Licensee continues to distribute or communicate the Work. + +Legal Protection: This Licence does not grant permission to use the trade names, +trademarks, service marks, or names of the Licensor, except as required for +reasonable and customary use in describing the origin of the Work and +reproducing the content of the copyright notice. + +6. Chain of Authorship + +The original Licensor warrants that the copyright in the Original Work granted +hereunder is owned by him/her or licensed to him/her and that he/she has the +power and authority to grant the Licence. + +Each Contributor warrants that the copyright in the modifications he/she brings +to the Work are owned by him/her or licensed to him/her and that he/she has the +power and authority to grant the Licence. + +Each time You accept the Licence, the original Licensor and subsequent +Contributors grant You a licence to their contributions to the Work, under the +terms of this Licence. + +7. Disclaimer of Warranty + +The Work is a work in progress, which is continuously improved by numerous +Contributors. It is not a finished work and may therefore contain defects or +‘bugs’ inherent to this type of development. + +For the above reason, the Work is provided under the Licence on an ‘as is’ basis +and without warranties of any kind concerning the Work, including without +limitation merchantability, fitness for a particular purpose, absence of defects +or errors, accuracy, non-infringement of intellectual property rights other than +copyright as stated in Article 6 of this Licence. + +This disclaimer of warranty is an essential part of the Licence and a condition +for the grant of any rights to the Work. + +8. Disclaimer of Liability + +Except in the cases of wilful misconduct or damages directly caused to natural +persons, the Licensor will in no event be liable for any direct or indirect, +material or moral, damages of any kind, arising out of the Licence or of the use +of the Work, including without limitation, damages for loss of goodwill, work +stoppage, computer failure or malfunction, loss of data or any commercial +damage, even if the Licensor has been advised of the possibility of such damage. +However, the Licensor will be liable under statutory product liability laws as +far such laws apply to the Work. + +9. Additional agreements + +While distributing the Work, You may choose to conclude an additional agreement, +defining obligations or services consistent with this Licence. However, if +accepting obligations, You may act only on your own behalf and on your sole +responsibility, not on behalf of the original Licensor or any other Contributor, +and only if You agree to indemnify, defend, and hold each Contributor harmless +for any liability incurred by, or claims asserted against such Contributor by +the fact You have accepted any warranty or additional liability. + +10. Acceptance of the Licence + +The provisions of this Licence can be accepted by clicking on an icon ‘I agree’ +placed under the bottom of a window displaying the text of this Licence or by +affirming consent in any other similar way, in accordance with the rules of +applicable law. Clicking on that icon indicates your clear and irrevocable +acceptance of this Licence and all of its terms and conditions. + +Similarly, you irrevocably accept this Licence and all of its terms and +conditions by exercising any rights granted to You by Article 2 of this Licence, +such as the use of the Work, the creation by You of a Derivative Work or the +Distribution or Communication by You of the Work or copies thereof. + +11. Information to the public + +In case of any Distribution or Communication of the Work by means of electronic +communication by You (for example, by offering to download the Work from a +remote location) the distribution channel or media (for example, a website) must +at least provide to the public the information requested by the applicable law +regarding the Licensor, the Licence and the way it may be accessible, concluded, +stored and reproduced by the Licensee. + +12. Termination of the Licence + +The Licence and the rights granted hereunder will terminate automatically upon +any breach by the Licensee of the terms of the Licence. + +Such a termination will not terminate the licences of any person who has +received the Work from the Licensee under the Licence, provided such persons +remain in full compliance with the Licence. + +13. Miscellaneous + +Without prejudice of Article 9 above, the Licence represents the complete +agreement between the Parties as to the Work. + +If any provision of the Licence is invalid or unenforceable under applicable +law, this will not affect the validity or enforceability of the Licence as a +whole. Such provision will be construed or reformed so as necessary to make it +valid and enforceable. + +The European Commission may publish other linguistic versions or new versions of +this Licence or updated versions of the Appendix, so far this is required and +reasonable, without reducing the scope of the rights granted by the Licence. New +versions of the Licence will be published with a unique version number. + +All linguistic versions of this Licence, approved by the European Commission, +have identical value. Parties can take advantage of the linguistic version of +their choice. + +14. Jurisdiction + +Without prejudice to specific agreement between parties, + +- any litigation resulting from the interpretation of this License, arising +between the European Union institutions, bodies, offices or agencies, as a +Licensor, and any Licensee, will be subject to the jurisdiction of the Court +of Justice of the European Union, as laid down in article 272 of the Treaty on +the Functioning of the European Union, + +- any litigation arising between other parties and resulting from the +interpretation of this License, will be subject to the exclusive jurisdiction +of the competent court where the Licensor resides or conducts its primary +business. + +15. Applicable Law + +Without prejudice to specific agreement between parties, + +- this Licence shall be governed by the law of the European Union Member State +where the Licensor has his seat, resides or has his registered office, + +- this licence shall be governed by Belgian law if the Licensor has no seat, +residence or registered office inside a European Union Member State. + +Appendix + +‘Compatible Licences’ according to Article 5 EUPL are: + +- GNU General Public License (GPL) v. 2, v. 3 +- GNU Affero General Public License (AGPL) v. 3 +- Open Software License (OSL) v. 2.1, v. 3.0 +- Eclipse Public License (EPL) v. 1.0 +- CeCILL v. 2.0, v. 2.1 +- Mozilla Public Licence (MPL) v. 2 +- GNU Lesser General Public Licence (LGPL) v. 2.1, v. 3 +- Creative Commons Attribution-ShareAlike v. 3.0 Unported (CC BY-SA 3.0) for +works other than software +- European Union Public Licence (EUPL) v. 1.1, v. 1.2 +- Québec Free and Open-Source Licence — Reciprocity (LiLiQ-R) or Strong +Reciprocity (LiLiQ-R+). + +The European Commission may update this Appendix to later versions of the above +licences without producing a new version of the EUPL, as long as they provide +the rights granted in Article 2 of this Licence and protect the covered Source +Code from exclusive appropriation. + +All other changes or additions to this Appendix require the production of a new +EUPL version. diff --git a/hs/app/CommonOptions.hs b/hs/app/CommonOptions.hs new file mode 100644 index 0000000..c6abbaf --- /dev/null +++ b/hs/app/CommonOptions.hs @@ -0,0 +1,17 @@ +module CommonOptions where + +import Options.Applicative + +data CommonOptions = CommonOptions + { extraChecks :: Bool + , logDirectory :: FilePath + , resultsDirectory :: FilePath + } + deriving Show + +commonOptionsParser :: Parser CommonOptions +commonOptionsParser = + CommonOptions + <$> switch (long "extra-checks" <> help "Enable extra validation checks") + <*> option str (long "log-directory" <> help "Directory for logging" <> showDefault <> value "log") + <*> option str (long "results-directory" <> help "Directory for outputs" <> showDefault <> value "results") diff --git a/hs/app/DecomposeInput.hs b/hs/app/DecomposeInput.hs new file mode 100644 index 0000000..989a795 --- /dev/null +++ b/hs/app/DecomposeInput.hs @@ -0,0 +1,153 @@ +module DecomposeInput where + +import Bisimulation (bisimulation2) +import Data.Partition (Block (..), numBlocks) +import Data.UnionFind (empty, equate, equivalent) +import DotParser (readDotFile) +import Mealy (MealyMachine (..), outputFunction, transitionFunction) +import MealyRefine (refineMealy) + +import Control.Monad (mapAndUnzipM) +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 Options.Applicative +import System.Exit (exitFailure, exitSuccess) + +newtype DecomposeInputOptions = DecomposeInputOptions + { filename :: FilePath + } + deriving Show + +decomposeInputOptionsParser :: Parser DecomposeInputOptions +decomposeInputOptionsParser = + DecomposeInputOptions + <$> argument str (help "Filename to read (dot format)" <> metavar "FILE") + <**> helper + +-- Interleaving composition of restriction to subalphabets +-- precondition: alph1 and alph2 have no common elements +interleavingComposition :: Ord i => [[i]] -> MealyMachine s i o -> MealyMachine [s] i o +interleavingComposition alphs m = + MealyMachine + { states = error "states should not be necessary" + , inputs = concat alphs + , outputs = outputs m -- or some subset? + , behaviour = \ss i -> + case Map.lookup i alphLookup of + Just idx -> + let (o, t) = behaviour m (ss !! idx) i + (p, _ : s) = splitAt idx ss + in (o, p ++ [t] ++ s) + Nothing -> error "symbol not in either alphabet" + , initialState = replicate (length alphs) (initialState m) + } + where + alphLookup = Map.fromList [(i, idx) | (alph, idx) <- zip alphs [0 ..], i <- alph] + +-- mainInputDecomp :: [String] -> IO () +-- mainInputDecomp args = case args of +-- [dotFile] -> putStrLn ("reading " <> dotFile) >> run dotFile +-- _ -> putStrLn "Please provide a dot file" +-- where +mainDecomposeInput :: DecomposeInputOptions -> IO () +mainDecomposeInput DecomposeInputOptions{..} = do + let + dotFile = filename + report s = appendFile "results/log.txt" (dotFile <> "\t" <> s <> "\n") + witness s = appendFile "results/witnesses.txt" (dotFile <> "\n" <> s <> "\n\n") + + report "START-INPUT-DECOMP" + model <- readDotFile dotFile + 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 + bisim i j = + let compo = composition i j + in bisimulation2 + [i, j] + (outputFunction model) + (transitionFunction model) + (initialState model) + (outputFunction compo) + (transitionFunction compo) + (initialState compo) + dependent i j = isJust $ bisim i j + dependentPairs = [(i, j) | i <- inputs model, j <- inputs model, j > i, dependent i j] + + -- The relation dependentPairs is typically not transitive. + let closure = foldr (uncurry equate) Data.UnionFind.empty dependentPairs + step _ [] = Nothing + step clos ls@(i : _) = Just (List.partition (\j -> equivalent i j clos) ls) + classes = List.unfoldr (step closure) (inputs model) + + case length classes of + 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 + let + bigCompo = interleavingComposition currentClasses model + result = bisimulation2 (inputs model) (outputFunction model) (transitionFunction model) (initialState model) (outputFunction bigCompo) (transitionFunction bigCompo) (initialState bigCompo) + + -- print currentClasses + print result + + case result of + Nothing -> return currentClasses + Just cex -> do + let + -- The counterexample is always the shortest. I am not completely + -- confident that all pairs should be then consideren dependent. + newDependentPairs = zip cex (tail cex) + newClosure = foldr (uncurry equate) currentClosure newDependentPairs + newClasses = List.unfoldr (step newClosure) (inputs model) + loop newClosure newClasses + + finalClasses <- loop closure classes + + let + reachability initial next = go [initial] Set.empty + where + go [] visited = visited + go (s : todo) visited + | Set.member s visited = go todo visited + | otherwise = go (todo ++ next s) (Set.insert s visited) + minimiseComponent cls = + let + reachableStates = reachability (initialState model) (\s -> [snd (behaviour model s i) | i <- cls]) + machine = MealyMachine{states = Set.toList reachableStates, inputs = cls, outputs = outputs model, behaviour = behaviour model, initialState = initialState model} + partition = refineMealy machine + in + partition + processClass cls = do + let (Block p) = numBlocks . minimiseComponent $ cls + putStr (show cls) >> putStr " of size " >> print p + return (p, p * length cls) + + putStrLn $ "Final classes " <> show (length finalClasses) + (sizes, transitions) <- mapAndUnzipM processClass 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 diff --git a/hs/app/DecomposeOutput.hs b/hs/app/DecomposeOutput.hs new file mode 100644 index 0000000..06318af --- /dev/null +++ b/hs/app/DecomposeOutput.hs @@ -0,0 +1,202 @@ +{-# LANGUAGE PartialTypeSignatures #-} +{-# OPTIONS_GHC -Wno-partial-type-signatures #-} + +module DecomposeOutput where + +import CommonOptions +import Data.Partition +import Data.Preorder +import DotParser (readDotFile) +import DotWriter +import Mealy +import MealyRefine +import Merger + +import Control.Monad (when) +import Data.Bifunctor +import Data.List (sortOn) +import Data.List.Ordered (nubSort) +import Data.Map.Strict qualified as Map +import Data.Maybe (isNothing) +import Data.Set qualified as Set +import Data.Text qualified as T +import Data.Text.IO qualified as T +import Data.Text.Lazy.IO qualified as TL +import Data.Tuple (swap) +import Options.Applicative + +data DecomposeOutputOptions = DecomposeOutputOptions + { filename :: FilePath + , numComponents :: Int + } + deriving Show + +decomposeOutputOptionsParser :: _ +decomposeOutputOptionsParser = + DecomposeOutputOptions + <$> argument str (help "Filename to read (dot format)" <> metavar "FILE") + <*> option auto (long "components" <> short 'c' <> help "Number of components" <> metavar "NUM" <> showDefault <> value 2) + <**> helper + +mainDecomposeOutput :: DecomposeOutputOptions -> CommonOptions -> IO () +mainDecomposeOutput DecomposeOutputOptions{..} CommonOptions{..} = do + let + report s = appendFile "results/log.txt" (filename <> "\t" <> s <> "\n") + + -- READING INPUT + ---------------- + putStrLn $ "reading " <> filename + machine <- readDotFile filename + + -- PREPROCESSING + ---------------- + let (outputFuns, reverseFuns) = preprocess machine + printBasics outputFuns reverseFuns machine extraChecks + + -- MINIMISING EACH COMPONENT + ---------------------------- + let mappedOutputFuns o = [(i, (o ==) . f) | (i, f) <- outputFuns] + projections = [(o, refineFuns (mappedOutputFuns o) reverseFuns (states machine)) | o <- outputs machine] + + putStrLn $ "\nComponents " <> show (length (outputs machine)) + mapM_ (\(o, p) -> putStr " " >> T.putStr o >> putStr " has size " >> print (numBlocks p)) projections + + -- REDUCING NUMBER OF COMPONENTS + -- by checking which partitions are equivalent + ---------------------------------------------- + let (equiv, uniqPartitions) = equivalenceClasses comparePartitions projections + + putStrLn $ "\nRepresentatives " <> show (length uniqPartitions) + print . fmap fst $ uniqPartitions + + -- putStrLn "\nEquivalences" + -- mapM_ (\(o2, o1) -> putStrLn $ " " <> show o2 <> " == " <> show o1) (Map.assocs equiv) + + -- COMPUTING THE LATTICE OF COMPONENTS + -- 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 comparePartitions uniqPartitions + foo (a, b) = (numBlocks b, a) + sortedTopMods = sortOn (negate . fst) . fmap foo $ topMods + + putStrLn $ "\nTop modules " <> show (length topMods) + mapM_ (\(b, o) -> putStr " " >> T.putStr o >> putStr " has size " >> print b) sortedTopMods + + -- HEURISTIC MERGING + -- 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 + numStrategy current + | numberOfComponents current <= numComponents = StopWith (componentPartitions current) + | otherwise = Continue + prevStrategy current = case previous current of + Just prev -> if totalSize prev < totalSize current then StopWith (componentPartitions prev) else Continue + _ -> Continue + strategy c = case prevStrategy c of + StopWith x -> StopWith x + Continue -> numStrategy c + + putStrLn "\nHeuristic merging" + projmap <- heuristicMerger topMods strategy + + putStrLn "\nDone" + putStrLn $ " components: " <> show (length projmap) + 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 + equivInv = converseRelation equiv + projmapN = zip projmap [1 :: Int ..] + processComponent ((os, p), componentIdx) = do + let + name = T.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 (`Set.member` componentOutputs) machine + -- Sanity check: compute partition again + partition = refineMealy proj + + putStrLn $ "\nComponent " <> show os + when extraChecks (putStrLn $ " Correct? " <> show (comparePartitions p partition)) + putStrLn $ " Size = " <> show (numBlocks p) + + do + let + filename' = "partition_" <> show componentIdx <> ".dot" + content = T.unlines . fmap T.unwords . toBlocks $ p + + putStrLn $ " Output (partition) in file " <> filename' + T.writeFile ("results/" <> filename') content + + 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 + state2block = (Map.!) (getPartition p) + -- We apply this to each transition, and then nubSort the duplicates away + transitionsBlocks = nubSort [(state2block s, i, o, state2block t) | (s, i, o, t) <- transitions] + -- The initial state should be first + initialBlock = state2block initialState + -- Sorting on "/= initialBlock" puts the initialBlock in front + initialFirst = sortOn (\(s, _, _, _) -> s /= initialBlock) transitionsBlocks + + -- Convert to a file + 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 && isNothing o)) $ deadInputs0 + result = filter (\(_, i, _, _) -> i `Set.notMember` deadInputs) initialFirst + + -- Convert to a file + filename2 = "component_reduced_" <> show componentIdx <> ".dot" + content2 = toString . mealyToDot name $ result + + putStrLn $ " Output (reduced machine) in file " <> filename1 + TL.writeFile ("results/" <> filename1) content1 + + putStrLn $ " Dead inputs = " <> show (Set.size deadInputs) + + putStrLn $ " Output (reduced machine) in file " <> filename2 + TL.writeFile ("results/" <> filename2) content2 + + mapM_ processComponent projmapN + +-- * Helper functions + +-- | Computes the predecessors of each state. +preprocess :: _ => MealyMachine _ _ _ -> _ +preprocess MealyMachine{..} = (outputFuns, reverseFuns) + where + outputFuns = [(i, fun) | i <- inputs, let fun s = fst (behaviour s i)] + reverseTransitionMaps i = Map.fromListWith (++) [(t, [s]) | s <- states, let t = snd (behaviour s i)] + reverseFuns = [(i, fun) | i <- inputs, let mm = reverseTransitionMaps i, let fun s = Map.findWithDefault [] s mm] + +-- | Prints basic info. +printBasics :: _ => _ -> _ -> MealyMachine _ _ _ -> Bool -> IO _ +printBasics outputFuns reverseFuns MealyMachine{..} extraChecksEnabled = do + putStrLn $ (show . length $ states) <> " states, " <> (show . length $ inputs) <> " inputs and " <> (show . length $ outputs) <> " outputs" + when extraChecksEnabled $ do + printPartition (refineFuns outputFuns reverseFuns states) + putStrLn "" + +-- | This functions inverts a map. In the new map the values are lists. +converseRelation :: Ord b => Map.Map a b -> Map.Map b [a] +converseRelation = Map.fromListWith (++) . fmap (second pure . swap) . Map.assocs + +-- | Prints the number of blocks. +printPartition :: Partition s -> IO () +printPartition p = putStrLn $ "number of states = " <> show (numBlocks p) diff --git a/hs/app/Main.hs b/hs/app/Main.hs index fc34379..999aadb 100644 --- a/hs/app/Main.hs +++ b/hs/app/Main.hs @@ -1,205 +1,47 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PartialTypeSignatures #-} -{-# OPTIONS_GHC -Wno-partial-type-signatures #-} +{-# OPTIONS_GHC -Wno-missing-signatures #-} module Main where -import Data.Partition -import Data.Preorder -import DotParser (readDotFile) -import DotWriter -import Mealy -import MealyRefine -import Merger +import CommonOptions +import DecomposeInput +import DecomposeOutput -import Control.Monad (when) -import Data.Bifunctor -import Data.List (sortOn) -import Data.List.Ordered (nubSort) -import Data.Map.Strict qualified as Map -import Data.Maybe (isNothing) -import Data.Set qualified as Set -import Data.Text qualified as T -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) +import Options.Applicative +import System.Directory -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 + -- parse command and options + let opts = info optionsParser (fullDesc <> header "Tool(s) to decompose a finite state machine into separate components.") + Options{..} <- execParser opts -mainFun :: String -> Int -> IO () -mainFun dotFile numComponents = do - let - report str = appendFile "results/log.txt" (dotFile <> "\t" <> str <> "\n") + -- setup some logging facilities + createDirectoryIfMissing True "log" + createDirectoryIfMissing True "results" - -- READING INPUT - ---------------- - putStrLn $ "reading " <> dotFile - machine <- readDotFile dotFile + -- dispatch to actual functionality, based on the command provided + case optCommand of + DecomposeOutput options -> mainDecomposeOutput options commonOptions + DecomposeInput options -> mainDecomposeInput options - -- PREPROCESSING - ---------------- - let (outputFuns, reverseFuns) = preprocess machine - printBasics outputFuns reverseFuns machine +data Options = Options + { optCommand :: Command + , commonOptions :: CommonOptions + } + deriving Show - -- MINIMISING EACH COMPONENT - ---------------------------- - let mappedOutputFuns o = [(i, (o ==) . f) | (i, f) <- outputFuns] - projections = [(o, refineFuns (mappedOutputFuns o) reverseFuns (states machine)) | o <- (outputs machine)] +optionsParser = + Options + <$> commandParser + <*> commonOptionsParser + <**> helper - putStrLn $ "\nComponents " <> show (length (outputs machine)) - mapM_ (\(o, p) -> putStr " " >> T.putStr o >> putStr " has size " >> print (numBlocks p)) projections +data Command + = DecomposeOutput DecomposeOutputOptions + | DecomposeInput DecomposeInputOptions + deriving Show - -- REDUCING NUMBER OF COMPONENTS - -- by checking which partitions are equivalent - ---------------------------------------------- - let (equiv, uniqPartitions) = equivalenceClasses comparePartitions projections - - putStrLn $ "\nRepresentatives " <> show (length uniqPartitions) - print . fmap fst $ uniqPartitions - - -- putStrLn "\nEquivalences" - -- mapM_ (\(o2, o1) -> putStrLn $ " " <> show o2 <> " == " <> show o1) (Map.assocs equiv) - - -- COMPUTING THE LATTICE OF COMPONENTS - -- 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 comparePartitions uniqPartitions - foo (a, b) = (numBlocks b, a) - sortedTopMods = (sortOn (negate . fst) . fmap foo $ topMods) - - putStrLn $ "\nTop modules " <> show (length topMods) - mapM_ (\(b, o) -> putStr " " >> T.putStr o >> putStr " has size " >> print b) sortedTopMods - - -- HEURISTIC MERGING - -- 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 - 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 - - putStrLn $ "\nDone" - putStrLn $ " components: " <> show (length projmap) - 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 - equivInv = converseRelation equiv - projmapN = zip projmap [1 :: Int ..] - action ((os, p), componentIdx) = do - let - name = T.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 (`Set.member` componentOutputs) machine - -- Sanity check: compute partition again - partition = refineMealy proj - - putStrLn $ "\nComponent " <> show os - when extraChecks (putStrLn $ " Correct? " <> show (comparePartitions p partition)) - putStrLn $ " Size = " <> show (numBlocks p) - - do - let - filename = "partition_" <> show componentIdx <> ".dot" - content = T.unlines . fmap T.unwords . toBlocks $ p - - putStrLn $ " Output (partition) in file " <> filename - T.writeFile ("results/" <> filename) content - - 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 - state2block = (Map.!) (getPartition p) - -- We apply this to each transition, and then nubSort the duplicates away - transitionsBlocks = nubSort [(state2block s, i, o, state2block t) | (s, i, o, t) <- transitions] - -- The initial state should be first - initialBlock = state2block initialState - -- Sorting on "/= initialBlock" puts the initialBlock in front - initialFirst = sortOn (\(s, _, _, _) -> s /= initialBlock) transitionsBlocks - - -- Convert to a file - 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 && isNothing o)) $ deadInputs0 - result = filter (\(_, i, _, _) -> i `Set.notMember` deadInputs) initialFirst - - -- Convert to a file - filename2 = "component_reduced_" <> show componentIdx <> ".dot" - content2 = toString . mealyToDot name $ result - - putStrLn $ " Output (reduced machine) in file " <> filename1 - TL.writeFile ("results/" <> filename1) content1 - - putStrLn $ " Dead inputs = " <> show (Set.size deadInputs) - - putStrLn $ " Output (reduced machine) in file " <> filename2 - TL.writeFile ("results/" <> filename2) content2 - - mapM_ action projmapN - --- * Helper functions - --- | Computes the predecessors of each state. -preprocess :: _ => MealyMachine _ _ _ -> _ -preprocess MealyMachine{..} = (outputFuns, reverseFuns) - where - outputFuns = [(i, fun) | i <- inputs, let fun s = fst (behaviour s i)] - reverseTransitionMaps i = Map.fromListWith (++) [(t, [s]) | s <- states, let t = snd (behaviour s i)] - reverseFuns = [(i, fun) | i <- inputs, let mm = reverseTransitionMaps i, let fun s = Map.findWithDefault [] s mm] - --- | Prints basic info. -printBasics :: _ => _ -> _ -> MealyMachine _ _ _ -> IO _ -printBasics outputFuns reverseFuns MealyMachine{..} = do - putStrLn $ (show . length $ states) <> " states, " <> (show . length $ inputs) <> " inputs and " <> (show . length $ outputs) <> " outputs" - when extraChecks $ do - printPartition (refineFuns outputFuns reverseFuns states) - putStrLn "" - --- | This functions inverts a map. In the new map the values are lists. -converseRelation :: Ord b => Map.Map a b -> Map.Map b [a] -converseRelation = Map.fromListWith (++) . fmap (second pure . swap) . Map.assocs - --- | Prints the number of blocks. -printPartition :: Partition s -> IO () -printPartition p = putStrLn $ "number of states = " <> show (numBlocks p) +commandParser = + subparser + ( command "decompose-output" (info (DecomposeOutput <$> decomposeOutputOptionsParser) (progDesc "decompose based on output")) + <> command "decompose-input" (info (DecomposeInput <$> decomposeInputOptionsParser) (progDesc "decompose based on independent inputs")) + ) diff --git a/hs/app/Playground.hs b/hs/app/Playground.hs index 4f3f623..c7bff9e 100644 --- a/hs/app/Playground.hs +++ b/hs/app/Playground.hs @@ -1,30 +1,20 @@ module Main where -import Bisimulation (bisimulation2) -import Data.Partition (Block (..), numBlocks) import Data.Trie qualified as Trie -import Data.UnionFind (empty, equate, equivalent) import DotParser (readDotFile) -import Mealy (MealyMachine (..), outputFunction, transitionFunction) -import MealyRefine (refineMealy) +import Mealy (MealyMachine (..)) import SplittingTree (initialPRState, refine) import StateIdentifiers (stateIdentifierFor) import Control.Monad.Trans.State (evalStateT) -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) main :: IO () main = do args <- getArgs case args of ("HSI" : ls) -> mainHSI ls - ("InputDecomp" : ls) -> mainInputDecomp ls _ -> putStrLn "Please provide one of [HSI, InputDecomp]" mainHSI :: [String] -> IO () @@ -59,126 +49,3 @@ mainHSI args = case args of putStrLn "\nW-SET" print (Trie.toList . foldr Trie.union Trie.empty $ sis) - --- Interleaving composition of restriction to subalphabets --- precondigiotn: alph1 and alph2 have no common elements -interleavingComposition :: Ord i => [[i]] -> MealyMachine s i o -> MealyMachine [s] i o -interleavingComposition alphs m = - MealyMachine - { states = error "states should not be necessary" - , inputs = concat alphs - , outputs = outputs m -- or some subset? - , behaviour = \ss i -> - case Map.lookup i alphLookup of - Just idx -> - let (o, t) = behaviour m (ss !! idx) i - (p, _ : s) = splitAt idx ss - in (o, p ++ [t] ++ s) - Nothing -> error "symbol not in either alphabet" - , initialState = replicate (length alphs) (initialState m) - } - where - alphLookup = Map.fromList [(i, idx) | (alph, idx) <- zip alphs [0 ..], i <- alph] - -mainInputDecomp :: [String] -> IO () -mainInputDecomp args = case args of - [dotFile] -> putStrLn ("reading " <> dotFile) >> run dotFile - _ -> 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 - 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 - bisim i j = - let compo = composition i j - in bisimulation2 - [i, j] - (outputFunction model) - (transitionFunction model) - (initialState model) - (outputFunction compo) - (transitionFunction compo) - (initialState compo) - dependent i j = isJust $ bisim i j - dependentPairs = [(i, j) | i <- inputs model, j <- inputs model, j > i, dependent i j] - - -- The relation dependentPairs is typically not transitive. - let closure = foldr (uncurry equate) empty dependentPairs - step _ [] = Nothing - step clos ls@(i : _) = Just (List.partition (\j -> equivalent i j clos) ls) - classes = List.unfoldr (step closure) (inputs model) - - case length classes of - 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 - let - bigCompo = interleavingComposition currentClasses model - result = bisimulation2 (inputs model) (outputFunction model) (transitionFunction model) (initialState model) (outputFunction bigCompo) (transitionFunction bigCompo) (initialState bigCompo) - - -- print currentClasses - print result - - case result of - Nothing -> return currentClasses - Just cex -> do - let - -- The counterexample is always the shortest. I am not completely - -- confident that all pairs should be then consideren dependent. - newDependentPairs = zip cex (tail cex) - newClosure = foldr (uncurry equate) currentClosure newDependentPairs - newClasses = List.unfoldr (step newClosure) (inputs model) - loop newClosure newClasses - - finalClasses <- loop closure classes - - let - reachability initial next = go [initial] Set.empty - where - go [] visited = visited - go (s : todo) visited - | Set.member s visited = go todo visited - | otherwise = go (todo ++ next s) (Set.insert s visited) - minimiseComponent cls = - let - reachableStates = reachability (initialState model) (\s -> [snd (behaviour model s i) | i <- cls]) - machine = MealyMachine{states = Set.toList reachableStates, inputs = cls, outputs = outputs model, behaviour = behaviour model, initialState = initialState model} - partition = refineMealy machine - in - partition - action cls = do - let (Block p) = numBlocks . minimiseComponent $ cls - putStr (show cls) >> putStr " of size " >> putStrLn (show p) - return (p, p * length cls) - - putStrLn $ "Final classes " <> show (length finalClasses) - (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 diff --git a/hs/mealy-decompose.cabal b/hs/mealy-decompose.cabal index b959e83..27416fa 100644 --- a/hs/mealy-decompose.cabal +++ b/hs/mealy-decompose.cabal @@ -2,7 +2,7 @@ cabal-version: 2.2 name: mealy-decompose version: 0.3.0.0 license: EUPL-1.2 -license-file: ../LICENSE +license-file: LICENSE author: Joshua Moerman maintainer: joshua.moerman@ou.nl copyright: (c) 2024-2025 Joshua Moerman, Open Universiteit @@ -43,7 +43,15 @@ executable mealy-decompose-main hs-source-dirs: app main-is: Main.hs build-depends: - mealy-decompose + directory, + mealy-decompose, + optparse-applicative + other-modules: + CommonOptions, + DecomposeInput, + DecomposeOutput + default-extensions: + OverloadedStrings executable mealy-decompose-lstar import: stuff diff --git a/hs/src/Merger.hs b/hs/src/Merger.hs index 814ba42..596d553 100644 --- a/hs/src/Merger.hs +++ b/hs/src/Merger.hs @@ -15,7 +15,7 @@ data MergerStats o s = MergerStats { numberOfComponents :: Int , maximalComponent :: Block , totalSize :: Block - , value :: [([o], Partition s)] + , componentPartitions :: [([o], Partition s)] , previous :: Maybe (MergerStats o s) } deriving (Show) @@ -32,9 +32,7 @@ data MergerAction o s = StopWith [([o], Partition s)] | Continue 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 Nothing 2) (Map.fromList (fmap (first pure) components)) - return $ projmap +heuristicMerger components strategy = evalStateT (loop Nothing 2) (Map.fromList (fmap (first pure) components)) where score ps p3 = numBlocks p3 - sum (fmap numBlocks ps) combine ops = @@ -46,7 +44,7 @@ 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 = StopWith value + | numberOfComponents <= 1 = StopWith componentPartitions | otherwise = strategy ms loop prevMS n = do @@ -56,7 +54,7 @@ heuristicMerger components strategy = do maximalComponent = maximum componentSizes totalSize = sum componentSizes previous = prevMS - value = Map.assocs projmap + componentPartitions = Map.assocs projmap ms = MergerStats{..} liftIO . printStats $ ms case safeStrategy ms of