From a4d97a9d0427e329ebee75a29018b40537bcabcc Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Tue, 29 Apr 2025 11:36:40 +0200 Subject: [PATCH] hsi and w method (almost) --- hs/app/HsiMethod.hs | 48 +++++++++++++++++++++------------------------ hs/app/Main.hs | 2 +- 2 files changed, 23 insertions(+), 27 deletions(-) diff --git a/hs/app/HsiMethod.hs b/hs/app/HsiMethod.hs index 7a1f849..3816527 100644 --- a/hs/app/HsiMethod.hs +++ b/hs/app/HsiMethod.hs @@ -1,7 +1,8 @@ -- | Copyright: (c) 2024-2025 Joshua Moerman, Open Universiteit --- SPDX-License-Identifier: EUPL-1.2] +-- SPDX-License-Identifier: EUPL-1.2 module HsiMethod where +import CommonOptions import Data.Trie qualified as Trie import DotParser (readDotFile) import Mealy (MealyMachine (..)) @@ -13,13 +14,14 @@ import Control.Monad (when) import Control.Monad.Trans.State (evalStateT) import Data.Map.Strict qualified as Map import Options.Applicative +import System.IO --- TODO: use common options -verbose :: Bool -verbose = False +data Mode = HSI | W + deriving (Eq, Ord, Show, Read) -newtype HsiMethodOptions = HsiMethodOptions +data HsiMethodOptions = HsiMethodOptions { filename :: FilePath + , mode :: Mode } deriving Show @@ -27,11 +29,14 @@ hsiMethodOptionsParser :: Parser HsiMethodOptions hsiMethodOptionsParser = HsiMethodOptions <$> argument str (help "Filename to read (dot format)" <> metavar "FILE") + <*> option auto (long "mode" <> help "Mode (HSI, W)" <> metavar "MODE" <> showDefault <> value HSI) -mainHsiMethod :: HsiMethodOptions -> IO () -mainHsiMethod HsiMethodOptions{..} = do - when verbose (print filename) +mainHsiMethod :: HsiMethodOptions -> CommonOptions -> IO () +mainHsiMethod HsiMethodOptions{..} CommonOptions{..} = do + let + logging st x = when verbose (hPutStrLn stderr st >> hPrint stderr x >> hPutStrLn stderr "") + logging "FILENAME" filename machine <- readDotFile filename let @@ -42,29 +47,20 @@ mainHsiMethod HsiMethodOptions{..} = do (partition, splittingTree) <- evalStateT (refine (const (pure ())) outputFuns reverseFuns) (initialPRState states) - when verbose $ do - putStrLn "\nPARTITION" - print partition - - putStrLn "\nTREE" - print splittingTree + logging "PARTITION" partition + logging "TREE" splittingTree let siFor s = stateIdentifierFor s partition splittingTree + wset = Trie.toList . foldr (Trie.union . siFor) Trie.empty $ states prefixes = stateCover (\s -> [((i, o), t) | i <- inputs, let (o, t) = behaviour s i]) initialState -- TODO: add middle transition(s) - testSuite = Trie.reducePrefixes [px <> sx | s <- states, let px = prefixes Map.! s, sx <- Trie.toList (siFor s)] + testSuite = case mode of + HSI -> Trie.reducePrefixes [px <> sx | s <- states, let px = prefixes Map.! s, sx <- Trie.toList (siFor s)] + W -> Trie.reducePrefixes [prefixes Map.! s <> sx | s <- states, sx <- wset] - when verbose $ do - 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) - - putStrLn "\nSTATE COVER" - print prefixes - - putStrLn "\nTEST SUITE" + logging "HARMONISED STATE IDENTIFIERS" [(s, Trie.toList (siFor s)) | s <- states] + logging "W-SET" wset + logging "STATE COVER" prefixes mapM_ print testSuite diff --git a/hs/app/Main.hs b/hs/app/Main.hs index 3a95dfe..9f5d8b5 100644 --- a/hs/app/Main.hs +++ b/hs/app/Main.hs @@ -29,7 +29,7 @@ main = do DecomposeOutput options -> mainDecomposeOutput options commonOptions DecomposeInput options -> mainDecomposeInput options commonOptions DecomposeTemp options -> mainDecomposeTemp options - HsiMethod options -> mainHsiMethod options + HsiMethod options -> mainHsiMethod options commonOptions LStar options -> mainLStar options RandomGen options -> mainRandomGen options