From 91d4c6d5392cd938aed8b62c733b2627b4a21388 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Fri, 18 Oct 2024 16:07:21 +0200 Subject: [PATCH] Removed gauge and added tasty and some tests (working towards mealy machines) --- .stylish-haskell.yaml | 141 ------------------------------------------ bench/Bench.hs | 14 +---- fourmolu.yaml | 5 ++ nominal-lstar.cabal | 11 ++-- test/Spec.hs | 80 +++++++++++++++++++----- 5 files changed, 77 insertions(+), 174 deletions(-) delete mode 100644 .stylish-haskell.yaml create mode 100644 fourmolu.yaml diff --git a/.stylish-haskell.yaml b/.stylish-haskell.yaml deleted file mode 100644 index 73243a4..0000000 --- a/.stylish-haskell.yaml +++ /dev/null @@ -1,141 +0,0 @@ -# stylish-haskell configuration file -# ================================== - -# The stylish-haskell tool is mainly configured by specifying steps. These steps -# are a list, so they have an order, and one specific step may appear more than -# once (if needed). Each file is processed by these steps in the given order. -steps: - # Convert some ASCII sequences to their Unicode equivalents. This is disabled - # by default. - # - unicode_syntax: - # # In order to make this work, we also need to insert the UnicodeSyntax - # # language pragma. If this flag is set to true, we insert it when it's - # # not already present. You may want to disable it if you configure - # # language extensions using some other method than pragmas. Default: - # # true. - # add_language_pragma: true - - # Format record definitions - # Disabled: don't like it for simple sum types - # - records: {} - - # Align the right hand side of some elements. This is quite conservative - # and only applies to statements where each element occupies a single - # line. All default to true. - - simple_align: - cases: true - top_level_patterns: true - records: true - - # Import cleanup - - imports: - # There are different ways we can align names and lists. - # - # - global: Align the import names and import list throughout the entire - # file. - # - # - file: Like global, but don't add padding when there are no qualified - # imports in the file. - # - # - group: Only align the imports per group (a group is formed by adjacent - # import lines). - # - # - none: Do not perform any alignment. - # - # Default: global. - align: none - - # The following options affect only import list alignment. - # - # List align has following options: - # - # - after_alias: Import list is aligned with end of import including - # 'as' and 'hiding' keywords. - # - # > import qualified Data.List as List (concat, foldl, foldr, head, - # > init, last, length) - # - # - with_alias: Import list is aligned with start of alias or hiding. - # - # > import qualified Data.List as List (concat, foldl, foldr, head, - # > init, last, length) - # - # - with_module_name: Import list is aligned `list_padding` spaces after - # the module name. - # - # > import qualified Data.List as List (concat, foldl, foldr, head, - # init, last, length) - # - # This is mainly intended for use with `pad_module_names: false`. - # - # > import qualified Data.List as List (concat, foldl, foldr, head, - # init, last, length, scanl, scanr, take, drop, - # sort, nub) - # - # - new_line: Import list starts always on new line. - # - # > import qualified Data.List as List - # > (concat, foldl, foldr, head, init, last, length) - # - # Default: after_alias - list_align: after_alias - - # Right-pad the module names to align imports in a group: - # - # - true: a little more readable - # - # > import qualified Data.List as List (concat, foldl, foldr, - # > init, last, length) - # > import qualified Data.List.Extra as List (concat, foldl, foldr, - # > init, last, length) - # - # - false: diff-safe - # - # > import qualified Data.List as List (concat, foldl, foldr, init, - # > last, length) - # > import qualified Data.List.Extra as List (concat, foldl, foldr, - # > init, last, length) - # - # Default: true - pad_module_names: false - - - # Language pragmas - - language_pragmas: - # We can generate different styles of language pragma lists. - # - # - vertical: Vertical-spaced language pragmas, one per line. - # - # - compact: A more compact style. - # - # - compact_line: Similar to compact, but wrap each line with - # `{-#LANGUAGE #-}'. - # - # Default: vertical. - style: vertical - - # Align affects alignment of closing pragma brackets. - # - # - true: Brackets are aligned in same column. - # - # - false: Brackets are not aligned together. There is only one space - # between actual import and closing bracket. - # - # Default: true - align: false - - # Language prefix to be used for pragma declaration, this allows you to - # use other options non case-sensitive like "language" or "Language". - # If a non correct String is provided, it will default to: LANGUAGE. - language_prefix: language - - # Remove trailing whitespace - - trailing_whitespace: {} - - # Squash multiple spaces between the left and right hand sides of some - # elements into single spaces. Basically, this undoes the effect of - # simple_align but is a bit less conservative. - # - squash: {} - -# A common indentation setting. Different steps take this into account. -indent: 4 diff --git a/bench/Bench.hs b/bench/Bench.hs index 51e29ed..6f46c56 100644 --- a/bench/Bench.hs +++ b/bench/Bench.hs @@ -5,11 +5,10 @@ import Bollig (learnBollig) import Examples import Teacher -import Gauge.Main -import Gauge.Main.Options +import Test.Tasty.Bench import NLambda -{- Benchmarks can be run with `stack bench`. If you would like to run a +{- Benchmarks can be run with `cabal bench`. If you would like to run a subset of benchmarks, you can do this with `stack bench --ba NomNLStar` for example. May take a long time (so we only run once). @@ -24,13 +23,6 @@ import NLambda Examples.example4 is not used, because it takes a bit too long. -} -myConfig :: Config -myConfig = defaultConfig - { quickMode = True - , includeFirstIter = True - , csvFile = Just "bench.csv" - } - -- Some bounds on the size of automata fifoBound = 4 stackBound = 4 @@ -38,7 +30,7 @@ doublewordBound = 3 nlastpositionBound = 4 main :: IO () -main = defaultMainWith myConfig +main = defaultMain [ bgroup "NomLStarR" [ bgroup "Fifo" $ fmap (\n -> bench (show n) $ whnf lstar (target (fifoExample n))) [0..fifoBound] diff --git a/fourmolu.yaml b/fourmolu.yaml new file mode 100644 index 0000000..ede47ab --- /dev/null +++ b/fourmolu.yaml @@ -0,0 +1,5 @@ +indentation: 4 +haddock-style: single-line +single-constraint-parens: auto +single-deriving-parens: auto +respectful: true diff --git a/nominal-lstar.cabal b/nominal-lstar.cabal index c6da77e..390eca5 100644 --- a/nominal-lstar.cabal +++ b/nominal-lstar.cabal @@ -1,8 +1,8 @@ cabal-version: 2.2 name: nominal-lstar -version: 0.1.0.0 +version: 0.1.1.0 author: Joshua Moerman -copyright: (c) 2016 - 2023, Joshua Moerman +copyright: (c) 2016 - 2024, Joshua Moerman build-type: Simple extra-source-files: README.md @@ -12,7 +12,7 @@ common stuff build-depends: base >= 4.8 && < 5, haskeline, - NLambda >= 1.1.1 + NLambda >= 1.1.3 library import: stuff @@ -57,7 +57,7 @@ benchmark bench type: exitcode-stdio-1.0 main-is: Bench.hs build-depends: - gauge, + tasty-bench, nominal-lstar test-suite test @@ -66,5 +66,6 @@ test-suite test type: exitcode-stdio-1.0 main-is: Spec.hs build-depends: - gauge, + tasty, + tasty-hunit, nominal-lstar diff --git a/test/Spec.hs b/test/Spec.hs index 46ae0e4..6121ad8 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -1,27 +1,73 @@ -{-# language PartialTypeSignatures #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE PartialTypeSignatures #-} {-# OPTIONS_GHC -Wno-missing-signatures -Wno-partial-type-signatures #-} -import Angluin (learnAngluin) + +import Angluin import Examples import Teacher +import Teachers.Whitebox -import Gauge.Main -import Gauge.Main.Options +import GHC.Generics (Generic) import NLambda +import Test.Tasty +import Test.Tasty.HUnit -{- TODO: choose test framework -} +main :: IO () +main = defaultMain (testGroup "Unit tests" unitTests) + where + unitTests = + [ testCase "Learning DFA DW1" $ learnAndCompare (runningExample atoms 1) @?= True + , testCase "Learning DFA DW2" $ learnAndCompare (runningExample atoms 2) @?= True + , testCase "Mealy deterministic echo" $ isTrue (mealyIsDeterministic echoMachine) @?= True + , testCase "Mealy deterministic memory True" $ isTrue (mealyIsDeterministic (memoryMachine True)) @?= True + , testCase "Mealy deterministic memory False" $ isTrue (mealyIsDeterministic (memoryMachine False)) @?= True + , testCase "Mealy enabled echo" $ isTrue (mealyIsEnabled echoMachine) @?= True + , testCase "Mealy enabled memory True" $ isTrue (mealyIsEnabled (memoryMachine True)) @?= True + , testCase "Mealy enabled memory False" $ isTrue (mealyIsEnabled (memoryMachine False)) @?= True + ] -myConfig = defaultConfig - { quickMode = True - , includeFirstIter = True - , csvFile = Just "test.csv" - } +learnAndCompare :: (Contextual i, Show i, Nominal i, Nominal q1) => Automaton q1 i -> Bool +learnAndCompare target = equivalenceCheck target learnedModel + where + learnedModel = learnAngluin (teacherWithTarget target) + equivalenceCheck m1 m2 = isTrue . isEmpty $ bisim m1 m2 -main = defaultMainWith myConfig - [ bench "DW2" $ whnf lstarCol (target (runningExample atoms 2)) ] +data MealyMachine s i o = MealyMachine + { mealyInitialState :: s + , mealyStates :: Set s + , mealyInputs :: Set i + , mealyTransitions :: Set (s, i, o, s) + } + deriving (Eq, Ord, Show, Generic, Nominal, Contextual) --- Some (polymorphic) abbreviations -lstarCol :: _ => Teacher i -> Automaton _ i -lstarCol = learnAngluin +mealyIsDeterministic :: _ => MealyMachine s i o -> Formula +mealyIsDeterministic m = forAll (\s -> forAll (\i -> let ot = mapFilter ((\(s2, i2, o, t) -> maybeIf ((s, i) `eq` (s2, i2)) (o, t))) (mealyTransitions m) in forAll (\(x, y) -> x `eq` y) (pairs ot ot)) (mealyInputs m)) (mealyStates m) -target :: _ => Automaton q i -> Teacher i -target = teacherWithTarget +mealyIsEnabled :: _ => MealyMachine s i o -> Formula +mealyIsEnabled m = forAll (\s -> forAll (\i -> let ot = mapFilter ((\(s2, i2, o, t) -> maybeIf ((s, i) `eq` (s2, i2)) (o, t))) (mealyTransitions m) in isNotEmpty ot) (mealyInputs m)) (mealyStates m) + +echoMachine :: MealyMachine () Atom Atom +echoMachine = MealyMachine + { mealyInitialState = () + , mealyStates = singleton () + , mealyInputs = atoms + , mealyTransitions = NLambda.map (\a -> ((), a, a, ())) atoms + } + +data MIn a = MPut a | MGet + deriving (Eq, Ord, Show, Generic, Nominal, Contextual) + +data MOut a = MNok | MOk | MVal a + deriving (Eq, Ord, Show, Generic, Nominal, Contextual) + +memoryMachine :: Bool -> MealyMachine (Maybe Atom) (MIn Atom) (MOut Atom) +memoryMachine forget = MealyMachine + { mealyInitialState = Nothing + , mealyStates = allStates + , mealyInputs = singleton MGet `union` NLambda.map MPut atoms + , mealyTransitions = NLambda.pairsWith (\q a -> (q, MPut a, MOk, Just a)) allStates atoms `union` + NLambda.map (\a -> (Just a, MGet, MVal a, if forget then Nothing else Just a)) atoms `union` + NLambda.singleton (Nothing, MGet, MNok, Nothing) + } + where allStates = singleton Nothing `union` (NLambda.map Just atoms)