From c14d24a13cd16edf05bee9e378228537110bd078 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Tue, 22 Apr 2025 11:53:39 +0200 Subject: [PATCH] moved the other commands as well so that everything goes via main --- hs/app/DecomposeInput.hs | 1 - hs/app/DecomposeOutput.hs | 1 - hs/app/HsiMethod.hs | 51 +++++++++++++++++++++++++++++++++++++++ hs/app/LStarMain.hs | 33 ++++++++++++++++--------- hs/app/Main.hs | 11 ++++++++- hs/app/Playground.hs | 51 --------------------------------------- hs/app/RandomGen.hs | 1 - hs/mealy-decompose.cabal | 18 +++----------- 8 files changed, 86 insertions(+), 81 deletions(-) create mode 100644 hs/app/HsiMethod.hs delete mode 100644 hs/app/Playground.hs diff --git a/hs/app/DecomposeInput.hs b/hs/app/DecomposeInput.hs index 9e08c66..5f3b886 100644 --- a/hs/app/DecomposeInput.hs +++ b/hs/app/DecomposeInput.hs @@ -27,7 +27,6 @@ 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 diff --git a/hs/app/DecomposeOutput.hs b/hs/app/DecomposeOutput.hs index 514b039..339b02a 100644 --- a/hs/app/DecomposeOutput.hs +++ b/hs/app/DecomposeOutput.hs @@ -37,7 +37,6 @@ 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 diff --git a/hs/app/HsiMethod.hs b/hs/app/HsiMethod.hs new file mode 100644 index 0000000..fccdc8c --- /dev/null +++ b/hs/app/HsiMethod.hs @@ -0,0 +1,51 @@ +module HsiMethod where + +import Data.Trie qualified as Trie +import DotParser (readDotFile) +import Mealy (MealyMachine (..)) +import SplittingTree (initialPRState, refine) +import StateIdentifiers (stateIdentifierFor) + +import Control.Monad.Trans.State (evalStateT) +import Data.Map.Strict qualified as Map +import Options.Applicative + +newtype HsiMethodOptions = HsiMethodOptions + { filename :: FilePath + } + deriving Show + +hsiMethodOptionsParser :: Parser HsiMethodOptions +hsiMethodOptionsParser = + HsiMethodOptions + <$> argument str (help "Filename to read (dot format)" <> metavar "FILE") + +mainHsiMethod :: HsiMethodOptions -> IO () +mainHsiMethod HsiMethodOptions{..} = do + let dotFile = filename + print dotFile + machine <- readDotFile dotFile + + -- convert to mealy + let + MealyMachine{..} = machine + 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 m = reverseTransitionMaps i, let fun s = Map.findWithDefault [] s m] + + (partition, splittingTree) <- evalStateT (refine print outputFuns reverseFuns) (initialPRState states) + + putStrLn "\nPARTITION" + print partition + + putStrLn "\nTREE" + print splittingTree + + let + siFor s = stateIdentifierFor s partition splittingTree + + putStrLn "\nHARMONISED STATE IDENTIFIERS" + sis <- mapM (\s -> let si = siFor s in print (Trie.toList si) >> return si) states + + putStrLn "\nW-SET" + print (Trie.toList . foldr Trie.union Trie.empty $ sis) diff --git a/hs/app/LStarMain.hs b/hs/app/LStarMain.hs index cbed3ff..61407a8 100644 --- a/hs/app/LStarMain.hs +++ b/hs/app/LStarMain.hs @@ -1,4 +1,4 @@ -module Main where +module LStarMain where import Bisimulation (bisimulation2) import DotParser (readDotFile) @@ -9,19 +9,25 @@ import Control.Monad (when) import Control.Monad.Trans.Class import Control.Monad.Trans.State.Strict import Data.Map.Strict qualified as Map -import System.Environment +import Options.Applicative -debugOutput :: Bool -debugOutput = False +data LStarOptions = LStarOptions + { filename :: FilePath + , debugOutput :: Bool + } + deriving Show -semanticsForState :: MealyMachine s i o -> s -> [i] -> o -semanticsForState _ _ [] = error "" -semanticsForState MealyMachine{..} q [a] = fst (behaviour q a) -semanticsForState m@MealyMachine{..} q (a : w) = semanticsForState m (snd (behaviour q a)) w +lStarOptionsParser :: Parser LStarOptions +lStarOptionsParser = + LStarOptions + <$> argument str (help "Filename to read (dot format)" <> metavar "FILE") + <*> switch (long "verbose" <> short 'v' <> help "Enable extra debugging output") + +mainLStar :: LStarOptions -> IO () +mainLStar LStarOptions{..} = do + let + dotFile = filename -main :: IO () -main = do - [dotFile] <- getArgs print dotFile machine <- readDotFile dotFile @@ -62,3 +68,8 @@ main = do putStrLn $ "Size: " <> show a putStrLn $ "MQs: " <> show b + +semanticsForState :: MealyMachine s i o -> s -> [i] -> o +semanticsForState _ _ [] = error "" +semanticsForState MealyMachine{..} q [a] = fst (behaviour q a) +semanticsForState m@MealyMachine{..} q (a : w) = semanticsForState m (snd (behaviour q a)) w diff --git a/hs/app/Main.hs b/hs/app/Main.hs index 21c222b..182f5bd 100644 --- a/hs/app/Main.hs +++ b/hs/app/Main.hs @@ -5,6 +5,8 @@ module Main where import CommonOptions import DecomposeInput import DecomposeOutput +import HsiMethod +import LStarMain import RandomGen import Options.Applicative @@ -23,6 +25,8 @@ main = do case optCommand of DecomposeOutput options -> mainDecomposeOutput options commonOptions DecomposeInput options -> mainDecomposeInput options commonOptions + HsiMethod options -> mainHsiMethod options + LStar options -> mainLStar options RandomGen options -> mainRandomGen options data Options = Options @@ -36,16 +40,21 @@ optionsParser = <$> commandParser <*> commonOptionsParser <**> helper + <**> simpleVersioner "0.4.0.0" data Command = DecomposeOutput DecomposeOutputOptions | DecomposeInput DecomposeInputOptions + | HsiMethod HsiMethodOptions + | LStar LStarOptions | RandomGen RandomGenOptions deriving Show commandParser = - subparser + hsubparser ( command "decompose-output" (info (DecomposeOutput <$> decomposeOutputOptionsParser) (progDesc "decompose based on output")) <> command "decompose-input" (info (DecomposeInput <$> decomposeInputOptionsParser) (progDesc "decompose based on independent inputs")) + <> command "hsi-method" (info (HsiMethod <$> hsiMethodOptionsParser) (progDesc "construct HSI test suite from specification dot file")) + <> command "lstar" (info (LStar <$> lStarOptionsParser) (progDesc "little l* playground")) <> command "random-gen" (info (RandomGen <$> randomGenOptionsParser) (progDesc "generate random parallel compositions")) ) diff --git a/hs/app/Playground.hs b/hs/app/Playground.hs deleted file mode 100644 index c7bff9e..0000000 --- a/hs/app/Playground.hs +++ /dev/null @@ -1,51 +0,0 @@ -module Main where - -import Data.Trie qualified as Trie -import DotParser (readDotFile) -import Mealy (MealyMachine (..)) -import SplittingTree (initialPRState, refine) -import StateIdentifiers (stateIdentifierFor) - -import Control.Monad.Trans.State (evalStateT) -import Data.Map.Strict qualified as Map -import System.Environment (getArgs) - -main :: IO () -main = do - args <- getArgs - case args of - ("HSI" : ls) -> mainHSI ls - _ -> putStrLn "Please provide one of [HSI, InputDecomp]" - -mainHSI :: [String] -> IO () -mainHSI args = case args of - [dotFile] -> run dotFile - _ -> putStrLn "Please provide a dot file" - where - run dotFile = do - print dotFile - machine <- readDotFile dotFile - - -- convert to mealy - let - MealyMachine{..} = machine - 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 m = reverseTransitionMaps i, let fun s = Map.findWithDefault [] s m] - - (partition, splittingTree) <- evalStateT (refine print outputFuns reverseFuns) (initialPRState states) - - putStrLn "\nPARTITION" - print partition - - putStrLn "\nTREE" - print splittingTree - - let - siFor s = stateIdentifierFor s partition splittingTree - - putStrLn "\nHARMONISED STATE IDENTIFIERS" - sis <- mapM (\s -> let si = siFor s in print (Trie.toList si) >> return si) states - - putStrLn "\nW-SET" - print (Trie.toList . foldr Trie.union Trie.empty $ sis) diff --git a/hs/app/RandomGen.hs b/hs/app/RandomGen.hs index ed17c17..47c02cd 100644 --- a/hs/app/RandomGen.hs +++ b/hs/app/RandomGen.hs @@ -25,7 +25,6 @@ randomGenOptionsParser = RandomGenOptions <$> option auto (long "states" <> short 'n' <> help "Number of states per component (max)" <> metavar "NUM" <> showDefault <> value 10) <*> option auto (long "components" <> short 'c' <> help "Number of components" <> metavar "COMP" <> showDefault <> value 2) - <**> helper genTransitions :: _ => Int -> [Char] -> [Char] -> RandT _ _ _ genTransitions size inputs outputs = do diff --git a/hs/mealy-decompose.cabal b/hs/mealy-decompose.cabal index 1bf3f6b..1727fd7 100644 --- a/hs/mealy-decompose.cabal +++ b/hs/mealy-decompose.cabal @@ -1,6 +1,6 @@ cabal-version: 2.2 name: mealy-decompose -version: 0.3.0.0 +version: 0.4.0.0 license: EUPL-1.2 license-file: LICENSE author: Joshua Moerman @@ -53,24 +53,12 @@ executable mealy-decompose-main CommonOptions, DecomposeInput, DecomposeOutput, + HsiMethod, + LStarMain, RandomGen default-extensions: OverloadedStrings -executable mealy-decompose-lstar - import: stuff - hs-source-dirs: app - main-is: LStarMain.hs - build-depends: - mealy-decompose - -executable mealy-decompose-playground - import: stuff - hs-source-dirs: app - main-is: Playground.hs - build-depends: - mealy-decompose - test-suite mealy-decompose-test import: stuff hs-source-dirs: test