Added proper commandline parsing, and moved the input-decompose into main

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 -- <path-to-fsm>
+cabal run mealy-decompose-main -- -h
 ```
 
 For the python tools (tested with python 3.12):

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.

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")

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

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)

hs/app/Main.hs

@@ -1,205 +1,47 @@
-{-# LANGUAGE OverloadedStrings #-}
+{-# OPTIONS_GHC -Wno-missing-signatures #-}
-{-# LANGUAGE PartialTypeSignatures #-}
-{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
 
 module Main where
 
-import Data.Partition
+import CommonOptions
-import Data.Preorder
+import DecomposeInput
-import DotParser (readDotFile)
+import DecomposeOutput
-import DotWriter
-import Mealy
-import MealyRefine
-import Merger
 
-import Control.Monad (when)
+import Options.Applicative
-import Data.Bifunctor
+import System.Directory
-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)
 
-extraChecks :: Bool
-extraChecks = False
-
-main :: IO ()
 main = do
-  -- COMMAND LINE
+  -- parse command and options
-  ---------------
+  let opts = info optionsParser (fullDesc <> header "Tool(s) to decompose a finite state machine into separate components.")
-  ls <- getArgs
+  Options{..} <- execParser opts
-  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 ()
+  -- setup some logging facilities
-mainFun dotFile numComponents = do
+  createDirectoryIfMissing True "log"
-  let
+  createDirectoryIfMissing True "results"
-    report str = appendFile "results/log.txt" (dotFile <> "\t" <> str <> "\n")
 
-  -- READING INPUT
+  -- dispatch to actual functionality, based on the command provided
-  ----------------
+  case optCommand of
-  putStrLn $ "reading " <> dotFile
+    DecomposeOutput options -> mainDecomposeOutput options commonOptions
-  machine <- readDotFile dotFile
+    DecomposeInput options -> mainDecomposeInput options
 
-  -- PREPROCESSING
+data Options = Options
-  ----------------
+  { optCommand :: Command
-  let (outputFuns, reverseFuns) = preprocess machine
+  , commonOptions :: CommonOptions
-  printBasics outputFuns reverseFuns machine
+  }
+  deriving Show
 
-  -- MINIMISING EACH COMPONENT
+optionsParser =
-  ----------------------------
+  Options
-  let mappedOutputFuns o = [(i, (o ==) . f) | (i, f) <- outputFuns]
+    <$> commandParser
-      projections = [(o, refineFuns (mappedOutputFuns o) reverseFuns (states machine)) | o <- (outputs machine)]
+    <*> commonOptionsParser
+      <**> helper
 
-  putStrLn $ "\nComponents " <> show (length (outputs machine))
+data Command
-  mapM_ (\(o, p) -> putStr "  " >> T.putStr o >> putStr " has size " >> print (numBlocks p)) projections
+  = DecomposeOutput DecomposeOutputOptions
+  | DecomposeInput DecomposeInputOptions
+  deriving Show
 
-  -- REDUCING NUMBER OF COMPONENTS
+commandParser =
-  -- by checking which partitions are equivalent
+  subparser
-  ----------------------------------------------
+    ( command "decompose-output" (info (DecomposeOutput <$> decomposeOutputOptionsParser) (progDesc "decompose based on output"))
-  let (equiv, uniqPartitions) = equivalenceClasses comparePartitions projections
+        <> command "decompose-input" (info (DecomposeInput <$> decomposeInputOptionsParser) (progDesc "decompose based on independent inputs"))
-
+    )
-  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)

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 Mealy (MealyMachine (..))
-import MealyRefine (refineMealy)
 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

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

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
+heuristicMerger components strategy = evalStateT (loop Nothing 2) (Map.fromList (fmap (first pure) components))
-  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 =
@@ -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