haal (empty) → 0.1.0.0

raw patch · 24 files changed

+2643/−0 lines, 24 filesdep +QuickCheckdep +basedep +containerssetup-changed

Dependencies added: QuickCheck, base, containers, haal, hspec, mtl, process, random, vector

Files

• CHANGELOG.md +21/−0
• LICENSE +26/−0
• README.md +167/−0
• Setup.hs +2/−0
• examples/demo.hs +35/−0
• examples/div.hs +101/−0
• examples/io.hs +106/−0
• examples/website.hs +109/−0
• haal.cabal +139/−0
• src/Haal/Automaton/DFA.hs +20/−0
• src/Haal/Automaton/MealyAutomaton.hs +132/−0
• src/Haal/Automaton/MooreAutomaton.hs +98/−0
• src/Haal/BlackBox.hs +212/−0
• src/Haal/EquivalenceOracle/CombinedOracle.hs +23/−0
• src/Haal/EquivalenceOracle/RandomWalk.hs +56/−0
• src/Haal/EquivalenceOracle/RandomWords.hs +56/−0
• src/Haal/EquivalenceOracle/WMethod.hs +124/−0
• src/Haal/EquivalenceOracle/WpMethod.hs +175/−0
• src/Haal/Experiment.hs +208/−0
• src/Haal/Learning/LMstar.hs +329/−0
• test/AutomatonSpec.hs +120/−0
• test/EquivalenceOracleSpec.hs +82/−0
• test/Spec.hs +1/−0
• test/Utils.hs +301/−0

@@ -0,0 +1,21 @@+# Changelog for `haal`++All notable changes to this project will be documented in this file.++The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),+and this project adheres to the+[Haskell Package Versioning Policy](https://pvp.haskell.org/).++## Unreleased++## 0.1.0.0 - 2025-12-02++- Initial release of `haal`.+    - Support for Mealy Automata and DFAs.+    - One learner for Mealy Automata and DFAs with 2 configurations. +        - LStar.+        - LPlus.+    - Basic equivalence oracles. +    - Examples that showcase usage of the library.++

@@ -0,0 +1,26 @@+Copyright 2025 Stefanos Anagnostou++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++1.  Redistributions of source code must retain the above copyright notice, this+    list of conditions and the following disclaimer.++2.  Redistributions in binary form must reproduce the above copyright notice,+    this list of conditions and the following disclaimer in the documentation+    and/or other materials provided with the distribution.++3.  Neither the name of the copyright holder nor the names of its contributors+    may be used to endorse or promote products derived from this software+    without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,167 @@+```text+++                        _       _           _                   _                   _     +                       / /\    / /\        / /\                / /\                _\ \   +                      / / /   / / /       / /  \              / /  \              /\__ \  +                     / /_/   / / /       / / /\ \            / / /\ \            / /_ \_\ +                    / /\ \__/ / /       / / /\ \ \          / / /\ \ \          / / /\/_/ +                   / /\ \___\/ /       / / /  \ \ \        / / /  \ \ \        / / /      +                  / / /\/___/ /       / / /___/ /\ \      / / /___/ /\ \      / / /       +                 / / /   / / /       / / /_____/ /\ \    / / /_____/ /\ \    / / / ____   +                / / /   / / /       / /_________/\ \ \  / /_________/\ \ \  / /_/_/ ___/\ +               / / /   / / /       / / /_       __\ \_\/ / /_       __\ \_\/_______/\__\/ +               \/_/    \/_/        \_\___\     /____/_/\_\___\     /____/_/\_______\/     ++                                                                           ++```+## A Haskell library for Active Automata Learning++**Haal** is an [Active Automata Learning](https://wcventure.github.io/Active-Automata-Learning/) library aimed at making it easy to construct learning experiments and explore different configurations of learning algorithms and equivalence oracles. The library is still in its early stages, so nothing is set in stone yet. Most probably, the more features are added the more will the structure of the library change. For the time being, a summary of the current architecture can be found below. Of course, the best documentation is the source code itself.++## 🔧 Features (constantly updated)++| Automaton Type     | Learning Algorithms         | Equivalence Oracles    |+|--------------------|-----------------------------|------------------------|+| Mealy Machines     | ✅ LM\*                     | ✅ W-method Oracle     |+|                    | ✅ LM\+                     | ✅ Wp-method Oracle    |+|                    |                             | ✅ Random Words Oracle |+|                    |                             | ✅ Random Walk Oracle  |+|                    |                             | ✅ Random W-method Oracle |+|                    |                             | ✅ Random Wp-method Oracle  |+++## Table of Contents++- [Architecture](#architecture)+  - [Systems under learning](#systems-under-learning)+  - [Automata](#automata)+  - [Learning algorithms](#learning-algorithms)+  - [Equivalence oracles](#equivalence-oracles)+  - [Experiment](#experiment)+- [Installing](#installing)+- [Example](#example)++## Architecture++The library consists of the following main components:+- Systems under learning+- Automata+- Learning algorithms+- Equivalence oracles+- Experiment++### Systems under learning++Systems under learning are defined by the `SUL` typeclass, parameterized by the types of their inputs and outputs. They must implement functions that allow them to be queried by learning algorithms and equivalence oracles. They are also parameterized by a monad which they operate in. For example, a SUL that is an external program performs IO actions, whereas a SUL that is a pure function operates in the Identity monad.++### Automata++Automata are a subclass of systems under learning that also expose information about their internal states. In addition to being queryable, they must implement functions that expose useful structural information, particularly for use by equivalence oracles.++### Learning algorithms++Learning algorithms are used to construct hypotheses based on a `SUL`. They must support initialization, hypothesis construction, and refinement via counterexamples. Not all learning algorithms learn the same type of automaton; the type of automaton to be learned is determined by the algorithm itself. At the moment, all learning algorithms are represented by a typeclass and each specific learning algorithm is meant to be its own data type. The values of the data type are the different configurations of the algorithm.++### Equivalence oracles++Equivalence oracles are algorithms that generate a test suite of queries, which are sent to both the current hypothesis and the `SUL`, in order to discover counterexamples. They must implement functions to report the size of the test suite, generate the suite, and test the hypothesis for counterexamples. As in the case of learning algorithm, equivalence oracles as a whole are represented by a typeclass and a specific equivalence oracle algorithm is meant to be represented by a data type, with the possible values of it being the different configurations of the algorithm.++### Experiment++An experiment ties all the components above together. In this library, experiments are represented as values and can be built with various configurations. An experiment is a function that takes a learning algorithm and an oracle, and returns an environment that awaits a `SUL` to execute the experiment. This is implemented using a `Reader` monad, where the environment provides access to the `SUL`.++## Installing++The project is still in its early stages and has not yet been published. For now, you can clone the repository, build, and install it locally using:++```bash+stack install+```++Moreover, I try to add haddock comments as much as possible. Therefore, documentation can be built using:++```bash+stack haddock+```++## Example++Here's a quick GHCi session putting it all together, showing how to define a simple Mealy machine, configure an experiment, and run a learning algorithm using `haal`. This session is also available as a program `examples/demo.hs` which can be run with `stack runghc examples/demo.hs`, or `stack run demo` and can also be loaded interactively with `stack ghci haal:exe:demo`.++```haskell+ghci> :set +m+ghci> import qualified Data.Set as Set++-- Define input, output, and state types+ghci> data Input = A | B deriving (Show, Eq, Ord, Enum, Bounded)+ghci> data Output = X | Y deriving (Show, Eq, Ord, Enum, Bounded)+ghci> data State = S0 | S1 | S2 deriving (Show, Eq, Ord, Enum, Bounded)++-- Define the transition function for the system under learning+ghci> let sulTransitions S0 _ = (S1, X)+ghci|     sulTransitions S1 _ = (S2, Y)+ghci|     sulTransitions S2 A = (S0, X)+ghci|     sulTransitions S2 B = (S0, Y)++-- Set up the experiment.+ghci> myexperiment = experiment (mkLMstar Star) (mkWMethod 2)++-- Define the Mealy system under learning. Remember that automata can act as suls.+ghci> mysul = mkMealyAutomaton2 sulTransitions (Set.fromList [S0, S1, S2]) S0++-- Run the experiment+ghci> (learnedmodel, stats) = runExperiment myexperiment mysul++-- View the learned model+ghci> learnedmodel+{+    Current State: 0,+    Initial State: 0,+    Transitions: fromList [+        ((0,A),(1,X)),+        ((0,B),(1,X)),+        ((1,A),(2,Y)),+        ((1,B),(2,Y)),+        ((2,A),(0,X)),+        ((2,B),(0,Y))+    ]+}+```++This shows how a simple Mealy machine can be learned using the `LM*` algorithm and a `W`-method equivalence oracle.++This also showcases some strong points of using a functional programming language like haskell for the task of active automata learning:++### 1. Type-safe alphabets++In Haal, the input and output alphabets are represented as plain Haskell data types. This means the compiler can catch errors early — for example, if a symbol not defined in the alphabet accidentally appears in a transition, the type checker will reject the code. This eliminates entire classes of bugs that are easy to make in more loosely typed implementations.++```haskell+data Input = A | B deriving (Show, Eq, Ord, Enum, Bounded)+data Output = X | Y deriving (Show, Eq, Ord, Enum, Bounded)+```++### 2. Automata as functions++Instead of defining transitions via tables or external formats like `dot`, Haskell allows transitions to be encoded as pure functions:++```haskell+sulTransitions :: State -> Input -> (State, Output)+sulTransitions S0 _ = (S1, X)+sulTransitions S1 _ = (S2, Y)+sulTransitions S2 A = (S0, X)+sulTransitions S2 B = (S0, Y)+```++Combined with exhaustive pattern matching and totality checking, this ensures that:+- All input cases are handled for each state+- No states or transitions are forgotten+- The definition is both human-readable and machine-checkable++In essence, **Haskell itself is the language for defining automata**, without needing external DSLs or formats like DOT.++---++

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,35 @@+{-# OPTIONS_GHC -Wno-missing-signatures #-}++import qualified Data.Set as Set+import Haal.Automaton.MealyAutomaton+import Haal.EquivalenceOracle.WMethod+import Haal.Experiment+import Haal.Learning.LMstar++-- Define input, output, and state types+data Input = A | B deriving (Show, Eq, Ord, Enum, Bounded)+data Output = X | Y deriving (Show, Eq, Ord, Enum, Bounded)+data State = S0 | S1 | S2 deriving (Show, Eq, Ord, Enum, Bounded)++-- Define the transition function for the system under learning+sulTransitions S0 _ = (S1, X)+sulTransitions S1 _ = (S2, Y)+sulTransitions S2 A = (S0, X)+sulTransitions S2 B = (S0, Y)++-- Set up the experiment.+myexperiment = experiment (mkLMstar Star) (mkWMethod 2)++-- Define the Mealy system under learning. Remember that automata can act as suls.+mysul = mkMealyAutomaton2 sulTransitions (Set.fromList [S0, S1, S2]) S0++-- Run the experiment+(learnedmodel, stats) = runExperiment myexperiment mysul++main :: IO ()+main = do+    putStrLn "Learning Experiment"+    putStrLn "==================="+    putStrLn $ "System Under Learning: " ++ show mysul+    putStrLn $ "Learned Model: " ++ show learnedmodel+    putStrLn $ "Experiment Statistics: " ++ show stats

@@ -0,0 +1,101 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}++import Haal.Automaton.MealyAutomaton+import Haal.BlackBox (SUL (..), StateID)+import Haal.EquivalenceOracle.WpMethod (WpMethod, mkWpMethod)+import Haal.Experiment+import Haal.Learning.LMstar (LMstar, LMstarConfig (Star), mkLMstar)+import Control.Monad.Identity (Identity)++-- main logic+divisible :: Integer -> Bool+divisible n = n `mod` (3 :: Integer) == 0++-- suppose we want to construct an automaton representation of this program using model learning+-- first of all, we choose a representation for the inputs of the program.+-- one option is to use decimal digits, another is to use binary digits.+-- the reason why we use a representation is because we cannot use the existing integers+-- as they are infinite. we cannot use an infinite input alphabet for our model, because+-- we can't possibly define its behaviours for all symbols of the alphabet, that is all the+-- integers. we have to code the integers.++data Binary = B0 | B1 deriving (Show, Eq, Ord, Enum, Bounded)++-- now we are in the position to use binary digits to construct integers.+-- we need a mapper that maps from binary digits to integers that the program can actually use++convert :: (Num a) => [Binary] -> a+convert [] = 0+convert [B0] = 0+convert [B1] = 1+convert (b : bs) = convert [b] + 2 * convert bs++-- >>> convert [B1, B0, B0, B0]+-- 1++-- >>> convert [B0, B0, B0, B1]+-- 8++-- >>> convert [B1, B1, B1, B1]+-- 15++-- now, remember that the only notion of SUL that is defined in the library is+-- a typeclass that states what functions must be implemented, like a java interface.+-- in order to create our system, we have to define it as a type and construct a value++data Program i o = Program+    { theStep :: i -> (Program i o, o)+    , theReset :: Program i o+    , buffer :: [i]+    }++instance SUL Program Identity i o where+    step s i = return (theStep s i)+    reset = return . theReset++wrapped :: [Binary] -> Bool+wrapped = divisible . convert++-- our program logic isn't really stateful. it computes the result at once.+-- this is why we make it stateful by providing a buffer that retains previous inputs.+-- each input is added to the buffer and the whole buffer is used for the computation.+-- so the input sequence+-- [B0, B0, B1] will produce outputs+-- [wrapped [B0], wrapped [B0,B0], wrapped [B1, B0, B0]]+-- until the program is reset and the buffer emptied.++mkProg :: [Binary] -> Program Binary Bool+mkProg buf =+    Program+        { theStep = \x ->+            let newBuf = x : buf+             in (mkProg newBuf, wrapped newBuf)+        , theReset = mkProg []+        , buffer = buf+        }++-- construct a sul with an empty buffer+sul :: Program Binary Bool+sul = mkProg []++learner :: LMstar Binary Bool+learner = mkLMstar Star++oracle :: WpMethod+oracle = mkWpMethod 3++exper :: Experiment (Program Binary Bool) (MealyAutomaton StateID Binary Bool, Statistics MealyAutomaton StateID Binary Bool)+exper = experiment learner oracle++theModel :: MealyAutomaton StateID Binary Bool+theStats :: Statistics MealyAutomaton StateID Binary Bool+(theModel, theStats) = runExperiment exper sul++main :: IO ()+main = do+    putStrLn "Learning Experiment"+    putStrLn "==================="+    putStrLn "System Under Learning: \\x -> x `mod` 3 == 0"+    putStrLn $ "Learned Model: " ++ show theModel+    putStrLn $ "Experiment Statistics: " ++ show theStats

@@ -0,0 +1,106 @@+-- we will attempt to reproduce the `div.hs` learning experiment,+-- but this time, instead of using a haskell function as a SUL,+-- we will use an actual program that performs IO, whose input and+-- output alphabet we know.+-- the output alphabet is just bool+-- the input alphabet is binary+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}++import Data.Functor ((<&>))+import Haal.Automaton.MealyAutomaton+import Haal.BlackBox+import Haal.EquivalenceOracle.WpMethod+import Haal.Experiment+import Haal.Learning.LMstar+import System.Process (readProcess)++-- Note that this is relative to the project root. Otherwise+-- the executable will not be found+source :: String+source = "./examples/divisible3"++inputMap :: Int -> String+inputMap num = show num ++ "\n"++innerQuery :: String -> IO String+innerQuery = readProcess source []++outputMap :: String -> Bool+outputMap = read++query :: Int -> IO Bool+query = (<&> outputMap) . innerQuery . inputMap++data Binary = B0 | B1 deriving (Show, Eq, Ord, Enum, Bounded)++-- now we are in the position to use binary digits to construct integers.+-- we need a mapper that maps from binary digits to integers that the program can actually use++convert :: (Num a) => [Binary] -> a+convert [] = 0+convert [B0] = 0+convert [B1] = 1+convert (b : bs) = convert [b] + 2 * convert bs++-- this time, in contrast to div.hs, a Program performs IO actions,+-- instead of purely returning the computes values+data Program i o = Program+    { theStep :: i -> IO (Program i o, o)+    , theReset :: IO (Program i o)+    , buffer :: [i]+    }++instance SUL Program IO Binary Bool where+    step = theStep+    reset = theReset++wrapped :: [Binary] -> IO Bool+wrapped = query . convert++mkProg :: [Binary] -> Program Binary Bool+mkProg buf =+    Program+        { theStep = \x -> do+            let newBuf = x : buf+            o <- wrapped newBuf+            return (mkProg newBuf, o)+        , theReset = return (mkProg [])+        , buffer = buf+        }++-- construct a sul with an empty buffer+sul :: Program Binary Bool+sul = mkProg []++learner :: LMstar Binary Bool+learner = mkLMstar Star++oracle :: WpMethod+oracle = mkWpMethod 3++exper ::+    ExperimentT+        (Program Binary Bool)+        IO+        ( MealyAutomaton+            StateID+            Binary+            Bool+        , Statistics+            MealyAutomaton+            StateID+            Binary+            Bool+        )+exper = experiment learner oracle+++main :: IO ()+main = do+    (theModel, theStats) <- runExperimentT exper sul+    putStrLn "Learning Experiment"+    putStrLn "==================="+    putStrLn "System Under Learning: \\x -> x `mod` 3 == 0"+    putStrLn $ "Learned Model: " ++ show theModel+    putStrLn $ "Experiment Statistics: " ++ show theStats

@@ -0,0 +1,109 @@+{-# LANGUAGE MultiParamTypeClasses #-}+{-# OPTIONS_GHC -Wno-missing-signatures #-}++import qualified Data.List as List+import Haal.BlackBox+import Haal.EquivalenceOracle.WMethod (mkWMethod)+import Haal.Experiment+import Haal.Learning.LMstar+import System.Process (readProcess)++--------------------------------------------------------------------------------+-- Types+--------------------------------------------------------------------------------++data Page = Home | About | CV | Links | Blogs | WrongUrl+    deriving (Eq, Show, Ord, Enum, Bounded)++data PageTag+    = LandingTag+    | AboutTag+    | CVTag+    | LinksTag+    | BlogsTag+    | NotFoundTag+    deriving (Eq, Show, Ord, Enum, Bounded)++data WebsiteSUL inp out = WebsiteSUL+    { baseUrl :: String+    , currentUrl :: String -- current path, e.g. "/about"+    }+    deriving (Eq, Show)++-- Fetch + HTML processing+--------------------------------------------------------------------------------++fetch :: String -> IO String+fetch url = readProcess "curl" ["-sL", url] ""++--------------------------------------------------------------------------------+-- Input and output abstraction+--------------------------------------------------------------------------------++inputMap :: Page -> String+inputMap Home = "/"+inputMap About = "/about"+inputMap CV = "/education-and-work"+inputMap Links = "/links"+inputMap Blogs = "/blogs"+inputMap WrongUrl = "/garbage"++outputMap :: String -> PageTag+outputMap html+    | "<title>About" `List.isInfixOf` html = AboutTag+    | "<title>Education" `List.isInfixOf` html = CVTag+    | "<title>Useful Links" `List.isInfixOf` html = LinksTag+    | "<title>My Blogs" `List.isInfixOf` html = BlogsTag+    | "<title>Stefanos" `List.isInfixOf` html = LandingTag+    | otherwise = NotFoundTag++-- >>> html <- fetch "http://www.anunknown.me/blogs"+-- >>> outputMap html+-- BlogsTag++--------------------------------------------------------------------------------+-- SUL instance+--------------------------------------------------------------------------------++instance SUL WebsiteSUL IO Page PageTag where+    reset sul = do+        pure sul{currentUrl = "/"}++    step sul input = do+        if currentUrl sul /= "/garbage"+            then do+                let suffix = inputMap input+                html <- fetch (baseUrl sul ++ suffix)+                let out = outputMap html+                    sul' = sul{currentUrl = suffix}+                pure (sul', out)+            else do+                pure (sul, NotFoundTag)++--------------------------------------------------------------------------------+-- Experiment setup+--------------------------------------------------------------------------------++learner = mkLMstar Star+teacher = mkWMethod 2+exper = experiment learner teacher++--------------------------------------------------------------------------------+-- Main+--------------------------------------------------------------------------------++main :: IO ()+main = do+    putStrLn "Learning Experiment"+    putStrLn "==================="+    putStrLn "System Under Learning: my personal website"+    let _baseUrl = "http://www.anunknown.me"+        _currentUrl = "/"+    let website =+            WebsiteSUL+                { baseUrl = _baseUrl -- this is constant+                , currentUrl = _currentUrl+                } ::+                WebsiteSUL Page PageTag+    (model, _) <- runExperimentT exper website+    putStrLn $ "Learned Model: " ++ show model

@@ -0,0 +1,139 @@+cabal-version: 2.2++-- This file has been generated from package.yaml by hpack version 0.37.0.+--+-- see: https://github.com/sol/hpack++name:           haal+version:        0.1.0.0+synopsis:       A Haskell library for Active Automata Learning.+description:    Please see the README on GitHub at <https://github.com/steve-anunknown/haal#readme>+category:       Model Learning+homepage:       https://github.com/steve-anunknown/haal#readme+bug-reports:    https://github.com/steve-anunknown/haal/issues+author:         Stefanos Anagnostou+maintainer:     steve.anunknown@gmail.com+copyright:      2025 Stefanos Anagnostou+license:        BSD-3-Clause+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+extra-doc-files:+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/steve-anunknown/haal++library+  exposed-modules:+      Haal.Automaton.DFA+      Haal.Automaton.MealyAutomaton+      Haal.Automaton.MooreAutomaton+      Haal.BlackBox+      Haal.EquivalenceOracle.CombinedOracle+      Haal.EquivalenceOracle.RandomWalk+      Haal.EquivalenceOracle.RandomWords+      Haal.EquivalenceOracle.WMethod+      Haal.EquivalenceOracle.WpMethod+      Haal.Experiment+      Haal.Learning.LMstar+  other-modules:+      Paths_haal+  autogen-modules:+      Paths_haal+  hs-source-dirs:+      src+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+  build-depends:+      base >=4.18.3 && <4.21+    , containers ==0.6.*+    , mtl >=2.3.1 && <2.4+    , random ==1.2.1.*+    , vector ==0.13.1.*+  default-language: Haskell2010++executable demo+  main-is: demo.hs+  other-modules:+      Paths_haal+  autogen-modules:+      Paths_haal+  hs-source-dirs:+      examples+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+  build-depends:+      base+    , containers ==0.6.*+    , haal+  default-language: Haskell2010++executable div+  main-is: div.hs+  other-modules:+      Paths_haal+  autogen-modules:+      Paths_haal+  hs-source-dirs:+      examples+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+  build-depends:+      base+    , haal+    , mtl >=2.3.1 && <2.4+  default-language: Haskell2010++executable io+  main-is: io.hs+  other-modules:+      Paths_haal+  autogen-modules:+      Paths_haal+  hs-source-dirs:+      examples+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+  build-depends:+      base+    , haal+    , mtl >=2.3.1 && <2.4+    , process >=1.6.19 && <1.6.25+  default-language: Haskell2010++executable website+  main-is: website.hs+  other-modules:+      Paths_haal+  autogen-modules:+      Paths_haal+  hs-source-dirs:+      examples+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints+  build-depends:+      base+    , haal+    , process >=1.6.19 && <1.6.25+  default-language: Haskell2010++test-suite haal-test+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  other-modules:+      AutomatonSpec+      EquivalenceOracleSpec+      Utils+      Paths_haal+  autogen-modules:+      Paths_haal+  hs-source-dirs:+      test+  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      QuickCheck+    , base >=4.18.3 && <4.21+    , containers ==0.6.*+    , haal+    , hspec+    , mtl >=2.3.1 && <2.4+    , random ==1.2.1.*+  default-language: Haskell2010

@@ -0,0 +1,20 @@+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wno-missing-export-lists #-}+{-# OPTIONS_GHC -Wno-unused-top-binds #-}++-- | This module implements a simple deterministic finite automaton (DFA).+module Haal.Automaton.DFA (+    DFA,+    mkDFA,+)+where++import qualified Data.Set as Set+import Haal.Automaton.MooreAutomaton++-- | 'DFA' is just a synonym for a 'MooreAutomaton' with 'Bool' type of output'.+type DFA state input = MooreAutomaton state input Bool++-- | Constructor for a 'DFA' value.+mkDFA :: (s -> i -> s) -> (s -> Bool) -> Set.Set s -> s -> DFA s i+mkDFA = mkMooreAutomaton

@@ -0,0 +1,132 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- | This module implements a Mealy automaton.+module Haal.Automaton.MealyAutomaton (+    MealyAutomaton (..),+    mkMealyAutomaton,+    mkMealyAutomaton2,+    mealyStep,+    mealyReset,+    mealyTransitions,+)+where++import qualified Data.Map as Map+import qualified Data.Set as Set+import Haal.BlackBox+import Control.Monad.Identity (Identity)++{- | The 'MealyAutomaton' data type is parameterised by the @input@, @output@ and @state@ types+ which play the role of the input alphabet, output alphabet and set of states respectively.+ The transitions of the automaton are defined by the 'mealyDelta' and 'mealyLambda' functions,+ which respectively return the new state after a transition and the produced output. Finally,+ the 'mealyInitialS' defines the initial state of the automaton and the 'mealyCurrentS' defines+ the current state which the automaton is in.+-}+data MealyAutomaton state input output = MealyAutomaton+    { mealyDelta :: state -> input -> state+    , mealyLambda :: state -> input -> output+    , mealyInitialS :: state+    , mealyCurrentS :: state+    , mealyStates :: Set.Set state+    }++{- | The 'mkMealyAutomaton' constructor returns a 'MealyAutomaton' by requiring the 'mealyDelta'+function, the 'mealyLambda' function and the initial state 'mealyInitialS'.+-}+mkMealyAutomaton :: (s -> i -> s) -> (s -> i -> o) -> Set.Set s -> s -> MealyAutomaton s i o+mkMealyAutomaton delta lambda sts initS =+    MealyAutomaton+        { mealyDelta = delta+        , mealyLambda = lambda+        , mealyInitialS = initS+        , mealyCurrentS = initS+        , mealyStates = sts+        }++{- | The 'mkMealyAutomaton2' constructor returns a 'MealyAutomaton' by requiring just one+function describing both the state transitions as well as the produced outputs, instead of two+separate functions, and the initial state 'mealyInitialS'.+-}+mkMealyAutomaton2 :: (s -> i -> (s, o)) -> Set.Set s -> s -> MealyAutomaton s i o+mkMealyAutomaton2 transs sts initS =+    MealyAutomaton+        { mealyDelta = \s i -> fst (transs s i)+        , mealyLambda = \s i -> snd (transs s i)+        , mealyInitialS = initS+        , mealyCurrentS = initS+        , mealyStates = sts+        }++{- | Performs a step in the automaton and returns a tuple containing the automaton with a modified+state as well as the output produced by the transition.+-}+mealyStep :: MealyAutomaton s i o -> i -> (MealyAutomaton s i o, o)+mealyStep m i = (m{mealyCurrentS = nextState}, output)+  where+    nextState = mealyDelta m (mealyCurrentS m) i+    output = mealyLambda m (mealyCurrentS m) i++-- | Resets the automaton to its initial state.+mealyReset :: MealyAutomaton s i o -> MealyAutomaton s i o+mealyReset m = m{mealyCurrentS = mealyInitialS m}++instance SUL (MealyAutomaton s) Identity i o where+    step sul i = return (mealyStep sul i)+    reset = return . mealyReset++{- | Returns a map describing the combined behaviour of the 'mealyDelta'+and 'mealyLambda' functions.+-}+mealyTransitions ::+    forall s i o.+    (Ord s, FiniteOrd i) =>+    MealyAutomaton s i o ->+    Map.Map (s, i) (s, o)+mealyTransitions m = Map.fromList [((s, i), (delta s i, lambda s i)) | s <- domainS, i <- domainI]+  where+    delta = mealyDelta m+    lambda = mealyLambda m+    domainS = Set.toList $ mealyStates m+    domainI = Set.toList $ inputs m++instance Automaton MealyAutomaton s i o where+    transitions = mealyTransitions+    states = mealyStates+    current = mealyCurrentS+    update m s = m{mealyCurrentS = s}++instance+    ( Show i+    , Show o+    , Show s+    , FiniteOrd s+    , FiniteOrd i+    ) =>+    Show (MealyAutomaton s i o)+    where+    show m =+        "{\n\tCurrent State: "+            ++ show currentS+            ++ ",\n\tInitial State: "+            ++ show initialS+            ++ ",\n\tTransitions: "+            ++ show transs+            ++ "\n}"+      where+        transs = mealyTransitions m+        initialS = initial m+        currentS = current m++instance+    ( FiniteOrd s+    , FiniteOrd i+    , Eq o+    ) =>+    Eq (MealyAutomaton s i o)+    where+    m1 == m2 =+        mealyTransitions m1 == mealyTransitions m2+            && mealyInitialS m1 == mealyInitialS m2

@@ -0,0 +1,98 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}++-- | This module implements a Moore automaton.+module Haal.Automaton.MooreAutomaton (+    MooreAutomaton,+    mkMooreAutomaton,+    mooreStep,+    mooreTransitions,+)+where++import qualified Data.Map as Map+import qualified Data.Set as Set+import Haal.BlackBox+import Control.Monad.Identity (Identity)++data MooreAutomaton state input output = MooreAutomaton+    { mooreDelta :: state -> input -> state+    , mooreLambda :: state -> output+    , mooreInitialS :: state+    , mooreCurrentS :: state+    , mooreStates :: Set.Set state+    }++{- | The 'mkMooreAutomaton' constructor returns a 'MooreAutomaton' by requiring the 'mooreDelta'+function, the 'mooreLambda' function and the initial state 'mooreInitialS'.+-}+mkMooreAutomaton :: (s -> i -> s) -> (s -> o) -> Set.Set s -> s -> MooreAutomaton s i o+mkMooreAutomaton delta lambda sts initS =+    MooreAutomaton+        { mooreDelta = delta+        , mooreLambda = lambda+        , mooreInitialS = initS+        , mooreCurrentS = initS+        , mooreStates = sts+        }++{- | Performs a step in the automaton and returns a tuple containing the automaton with a modified+state as well as the output produced by the transition.+-}+mooreStep :: MooreAutomaton s i o -> i -> (MooreAutomaton s i o, o)+mooreStep m i = (m{mooreCurrentS = nextState}, output)+  where+    nextState = mooreDelta m (mooreCurrentS m) i+    output = mooreLambda m (mooreCurrentS m)++-- | Resets the automaton to its initial state.+mooreReset :: MooreAutomaton s i o -> MooreAutomaton s i o+mooreReset m = m{mooreCurrentS = mooreInitialS m}++instance SUL (MooreAutomaton s) Identity i o where+    step sul i = return (mooreStep sul i)+    reset = return . mooreReset++{- | Returns a map describing the combined behaviour of the 'mooreDelta'+and 'mooreLambda' functions.+-}+mooreTransitions ::+    forall i o s.+    (FiniteOrd s, FiniteOrd i) =>+    MooreAutomaton s i o ->+    Map.Map (s, i) (s, o)+mooreTransitions m = Map.fromList [((s, i), (delta s i, lambda s)) | s <- domainS, i <- domainI]+  where+    delta = mooreDelta m+    lambda = mooreLambda m+    domainS = Set.toList $ mooreStates m+    domainI = Set.toList $ inputs m++instance Automaton MooreAutomaton s i o where+    transitions = mooreTransitions+    current = mooreCurrentS+    states = mooreStates+    update m s = m{mooreCurrentS = s}++instance+    ( Show i+    , Show o+    , Show s+    , FiniteOrd s+    , FiniteOrd i+    ) =>+    Show (MooreAutomaton s i o)+    where+    show m =+        "{\n\tCurrent State: "+            ++ show currentS+            ++ ",\n\tInitial State: "+            ++ show initialS+            ++ ",\n\tTransitions: "+            ++ show transs+            ++ "\n}"+      where+        transs = mooreTransitions m+        initialS = initial m+        currentS = current m

@@ -0,0 +1,212 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}++{- | This module defines the BlackBox type class as well as the Automaton and SUL+sub classes.+-}+module Haal.BlackBox (+    Automaton (..),+    SUL (..),+    StateID,+    Finite,+    FiniteEq,+    FiniteOrd,+    inputs,+    outputs,+    walk,+    initial,+    distinguish,+    accessSequences,+    localCharacterizingSet,+    globalCharacterizingSet,+    reachable,+)+where++import Control.Monad.Identity (Identity, runIdentity)+import qualified Data.Bifunctor as Bif+import qualified Data.List as List+import qualified Data.Map as Map+import qualified Data.Set as Set++{- | The 'StateID' type is an alias for an integer that represents the state of the automaton.+ - It is used as a default type for the state of learned automata.+-}+type StateID = Int++{- | The 'SUL' type class defines the basic interface for a black box automaton.+It provides methods to step through the automaton and retrieve the current state.+It also requires a monad m, that may be 'Identity' in case of a pure SUL, or 'IO'+in case of an external program that performs IO.+-}+class (Monad m) => SUL sul m i o where+    step :: sul i o -> i -> m (sul i o, o)+    reset :: sul i o -> m (sul i o)++-- | Finite is an alias for (Enum, Bounded).+type Finite i = (Enum i, Bounded i)+-- | FiniteEq is an alias for (Eq, Finite).+type FiniteEq i = (Eq i, Finite i)+-- | FiniteOrd is an alias for (Ord, Bounded).+type FiniteOrd i = (Ord i, Finite i)++-- | Generalization of 'step' that operates on a list of inputs.+walk :: (SUL sul m i o) => sul i o -> [i] -> m (sul i o, [o])+walk sul [] = pure (sul, [])+walk sul (x : xs) = do+    (sul', o) <- step sul x+    (sul'', os) <- walk sul' xs+    pure (sul'', o : os)++-- | Return a Set containing only the valid inputs of the SUL.+inputs :: (FiniteOrd i) => sul i o -> Set.Set i+inputs _ = Set.fromList [minBound .. maxBound]++-- | Return a Set containing only the valid outputs of the SUL.+outputs :: (FiniteOrd o) => sul i o -> Set.Set o+outputs _ = Set.fromList [minBound .. maxBound]++{- | The 'Automaton' type class extends the 'SUL' type class and adds+support for automata operations. Automatons are models, not programs,+so they are pure and operate in the Identity monad.+-}+class (SUL (aut s) Identity i o) => Automaton aut s i o where+    transitions ::+        (FiniteOrd i, FiniteOrd s) =>+        aut s i o ->+        Map.Map (s, i) (s, o)+    states :: (FiniteOrd s) => aut s i o -> Set.Set s+    current :: aut s i o -> s+    update :: aut s i o -> s -> aut s i o++-- | Pure instance of 'step'.+stepPure :: (SUL sul Identity i o) => sul i o -> i -> (sul i o, o)+stepPure sul i = runIdentity (step sul i)++-- | Pure instance of 'walk'.+walkPure :: (SUL sul Identity i o) => sul i o -> [i] -> (sul i o, [o])+walkPure sul i = runIdentity (walk sul i)++-- | Pure instance of 'reset'.+resetPure :: (SUL sul Identity i o) => sul i o -> sul i o+resetPure sul = runIdentity (reset sul)++-- | Return the initial state of an automaton.+initial :: (Automaton aut s i o) => aut s i o -> s+initial = current . resetPure++-- | Return the set of reachable states of an automaton.+reachable :: forall s i o aut. (Automaton aut s i o, Ord s, FiniteOrd i) => aut s i o -> Set.Set s+reachable aut = bfs [initial aut] $ Set.singleton (initial aut)+  where+    alphabet = inputs aut++    bfs :: [s] -> Set.Set s -> Set.Set s+    bfs [] visited = visited+    bfs (st : queue) visited = bfs queue' visited'+      where+        aut' = update aut st+        neighbours = Set.map (current . fst . stepPure aut') alphabet+        visited' = visited `Set.union` neighbours+        queue' = Set.toList (neighbours `Set.difference` visited) ++ queue++-- | Returns a map containing the shortest sequence to access each reachable state from the initial state.+accessSequences ::+    forall s i o aut.+    (Automaton aut s i o, FiniteOrd i, Ord s) =>+    aut s i o ->+    Map.Map s [i]+accessSequences aut = bfs [(initialSt, [])] (Set.singleton initialSt) (Map.singleton initialSt [])+  where+    alphabet = Set.toList (inputs aut)+    initialSt = initial aut++    bfs :: [(s, [i])] -> Set.Set s -> Map.Map s [i] -> Map.Map s [i]+    bfs [] _ acc = Map.map List.reverse acc+    bfs ((_, prefix) : rest) visited acc =+        bfs (rest ++ newQueue) newVisited newMap+      where+        mo = fst $ walkPure (resetPure aut) (reverse prefix)+        successors =+            [ (nextState, input : prefix)+            | input <- alphabet+            , let nextState = current . fst $ stepPure mo input+            , nextState `Set.notMember` visited+            ]++        newMap = foldr (uncurry Map.insert) acc successors+        newVisited = foldr (Set.insert . fst) visited successors+        newQueue = successors++{- | Returns an input sequence that distinguishes the given states in+the given automaton.+-}+distinguish ::+    ( Automaton aut s i o+    , FiniteOrd i+    , Ord s+    , Eq o+    ) =>+    aut s i o ->+    s ->+    s ->+    [i]+distinguish m s1 s2 = explore Map.empty [(s1, s2, [])]+  where+    alphabet = Set.toList (inputs m)++    explore _ [] = []+    explore visited ((q1, q2, prefix) : queue)+        | Just symbol <- discrepancy = reverse (symbol : prefix)+        | otherwise = explore newVisited (queue ++ newQueue)+      where+        newVisited = Map.insert (q1, q2) prefix visited+        mo1 = update m q1+        mo2 = update m q2++        (nextStates1, outputs1) = unzip $ map (stepAndCurrent mo1) alphabet+        (nextStates2, outputs2) = unzip $ map (stepAndCurrent mo2) alphabet++        discrepancy = snd <$> List.find fst (zip (zipWith (/=) outputs1 outputs2) alphabet)++        appended = map (: prefix) alphabet++        toBeVisited = Map.fromList $ zip (zip nextStates1 nextStates2) appended++        newQueue = [(s1', s2', p) | ((s1', s2'), p) <- Map.toList toBeVisited, (s1', s2') `Map.notMember` visited]++    stepAndCurrent mo i = Bif.first current (stepPure mo i)++{- | Returns a set of lists of inputs that can be used to distinguish between the given state and+ - any other state of the automaton.+-}+localCharacterizingSet ::+    ( Automaton aut s i o+    , FiniteOrd i+    , FiniteOrd s+    , Eq o+    ) =>+    aut s i o ->+    s ->+    Set.Set [i]+localCharacterizingSet m s = Set.fromList [d s sx | sx <- Set.toList $ states m, s /= sx]+  where+    d = distinguish m++{- | Returns a set of lists of inputs that can be used to distinguish between any two different states+of the automaton.+-}+globalCharacterizingSet ::+    ( Automaton aut s i o+    , FiniteOrd i+    , FiniteOrd s+    , Eq o+    ) =>+    aut s i o ->+    Set.Set [i]+globalCharacterizingSet m = Set.fromList [d s1 s2 | s1 <- sts, s2 <- sts, s1 < s2]+  where+    sts = Set.toList $ states m+    d = distinguish m

@@ -0,0 +1,23 @@+-- | This module implements a combined equivalence oracle for two oracles.+module Haal.EquivalenceOracle.CombinedOracle (+    CombinedOracle (..),+) where++import Haal.Experiment++{- | The 'CombinedOracle' type is a data type for combining two equivalence oracles.+It is used to chain multiple oracles together by first exhausting the test suite+of the first oracle and then using the second oracle.+-}+data CombinedOracle a b = CombinedOracle a b deriving (Show, Eq)++instance+    ( EquivalenceOracle a+    , EquivalenceOracle b+    ) =>+    EquivalenceOracle (CombinedOracle a b)+    where+    testSuite (CombinedOracle or1 or2) aut =+        let (or1', testSuite1) = testSuite or1 aut+            (or2', testSuite2) = testSuite or2 aut+         in (CombinedOracle or1' or2', testSuite1 ++ testSuite2)

@@ -0,0 +1,56 @@+-- | This module implements the Random Walk equivalence oracle.+module Haal.EquivalenceOracle.RandomWalk (+    RandomWalk (..),+    RandomWalkConfig (..),+    mkRandomWalk,+)+where++import qualified Data.Set as Set+import qualified Data.Vector as V+import Haal.BlackBox+import Haal.Experiment+import System.Random (+    Random (randomR, randomRs),+    RandomGen (split),+    StdGen,+ )++-- | The 'RandomWalkConfig' data type represents the configuration for an instance of the 'RandomWalk' algorithm.+data RandomWalkConfig = RandomWalkConfig+    { rwlGen :: StdGen+    , rwlMaxSteps :: Int+    , rwlRestart :: Double+    }+    deriving (Eq, Show)++-- | The 'RandomWalk' data type is just a wrapper around the config.+newtype RandomWalk = RandomWalk RandomWalkConfig deriving (Show, Eq)++-- | Constructor for a 'RandomWalk' value.+mkRandomWalk :: RandomWalkConfig -> RandomWalk+mkRandomWalk = RandomWalk++-- | Generates a random walk for the automaton.+randomWalkSuite :: (FiniteOrd a) => RandomWalk -> sul a o -> (RandomWalk, [[a]])+randomWalkSuite (RandomWalk (RandomWalkConfig{rwlGen = g, rwlMaxSteps = maxS, rwlRestart = restartP})) aut =+    let (g1, g2) = split g+        alphabet = V.fromList . Set.toList $ inputs aut+        randomInputs = take maxS $ randomRs (0, V.length alphabet - 1) g1+        inputSequence = map (alphabet V.!) randomInputs+        (inputSequence', g3) = splitWithProbability g2 restartP inputSequence+        oracle' = mkRandomWalk (RandomWalkConfig g3 maxS restartP)+     in (oracle', inputSequence')++splitWithProbability :: StdGen -> Double -> [a] -> ([[a]], StdGen)+splitWithProbability generator p symbols = go generator symbols [] []+  where+    go g [] acc word = (word : acc, g)+    go g (x : xs) acc word =+        let (r, g') = randomR (0.0, 1.0) g+         in if r < p && not (null word)+                then go g' xs (word : acc) [x]+                else go g' xs acc (x : word)++instance EquivalenceOracle RandomWalk where+    testSuite = randomWalkSuite

@@ -0,0 +1,56 @@+-- | This module implements a simple random words equivalence oracle.+module Haal.EquivalenceOracle.RandomWords (+    RandomWords (..),+    RandomWordsConfig (..),+    mkRandomWords,+)+where++import Control.Monad (replicateM)+import Control.Monad.State (MonadState (state), runState)+import qualified Data.Set as Set+import qualified Data.Vector as V+import Haal.BlackBox+import Haal.Experiment+import System.Random (Random (randomR), StdGen)++-- | Data type that represents the configuration for an instance of the 'RandomWords' algorithm.+data RandomWordsConfig = RandomWordsConfig+    { rwGen :: StdGen+    , rwLimit :: Int+    , rwMinLength :: Int+    , rwMaxLength :: Int+    }+    deriving (Eq, Show)++-- | The 'RandomWords' type is just a wrapper around the respective config type.+newtype RandomWords = RandomWords RandomWordsConfig deriving (Show, Eq)++-- | Constructor for a 'RandomWords' data type.+mkRandomWords :: RandomWordsConfig -> RandomWords+mkRandomWords = RandomWords++-- | Return the test suite of the 'RandomWords' algorithm.+generateRandomWords :: (FiniteOrd a) => RandomWords -> sul a o -> (RandomWords, [[a]])+generateRandomWords+    ( RandomWords+            RandomWordsConfig+                { rwGen = generator+                , rwLimit = count+                , rwMinLength = minL+                , rwMaxLength = maxL+                }+        )+    aut =+        let (ranWords, finalGen) = runState (replicateM count genWord) generator+            oracle = mkRandomWords (RandomWordsConfig finalGen count minL maxL)+         in (oracle, ranWords)+      where+        alphaVec = V.fromList . Set.toList $ inputs aut+        alphaLen = V.length alphaVec - 1+        genWord = do+            len <- state $ randomR (minL, maxL)+            replicateM len (state $ \g -> let (ix, g') = randomR (0, alphaLen) g in (alphaVec V.! ix, g'))++instance EquivalenceOracle RandomWords where+    testSuite = generateRandomWords

@@ -0,0 +1,124 @@+{-# LANGUAGE ScopedTypeVariables #-}++-- | This module implements the W-method equivalence oracle.+module Haal.EquivalenceOracle.WMethod (+    WMethod (..),+    wmethodSuiteSize,+    RandomWMethod (..),+    RandomWMethodConfig (..),+    mkWMethod,+    mkRandomWMethod,+) where++import Control.Monad (replicateM)+import qualified Data.List as List+import qualified Data.Map as Map+import qualified Data.Set as Set+import qualified Data.Vector as Vec+import Haal.BlackBox+import Haal.EquivalenceOracle.RandomWords+import Haal.Experiment+import System.Random (Random (randomRs), RandomGen (split), StdGen)++{- | The 'WMethod' type represents the W-method equivalence oracle.+It is just a wrapper around an integer, which is used for configuring+the exploration depth of the method.+-}+newtype WMethod = WMethod Int deriving (Show, Eq)++-- | Constructor for a 'WMethod' value.+mkWMethod :: Int -> WMethod+mkWMethod = WMethod++-- | The 'wmethodSuiteSize' function computes the size of the test suite for the W-method.+wmethodSuiteSize ::+    ( Automaton aut s i o+    , FiniteOrd i+    , FiniteOrd s+    , Eq o+    ) =>+    WMethod ->+    aut s i o ->+    Int+wmethodSuiteSize (WMethod d) aut = size+  where+    alphabet = Set.size $ inputs aut+    accessSeqs = Map.size $ accessSequences aut+    characterizingSet = Set.size $ globalCharacterizingSet aut+    transitionCover = accessSeqs * alphabet+    size = sum [transitionCover * (alphabet ^ n) * characterizingSet | n <- [0 .. d]]++-- | The 'wmethodSuite' function generates the test suite for the W-method and a new oracle.+wmethodSuite ::+    ( Automaton aut s i o+    , FiniteOrd i+    , FiniteOrd s+    , Eq o+    ) =>+    WMethod ->+    aut s i o ->+    (WMethod, [[i]])+wmethodSuite wm@(WMethod d) aut = (wm, suite)+  where+    alphabet = Set.toList $ inputs aut+    accessSeqs = accessSequences aut+    characterizingSet = Set.toList $ globalCharacterizingSet aut+    transitionCover = [a ++ [inp] | a <- Map.elems accessSeqs, inp <- alphabet]+    middlesByDepth = [replicateM n alphabet | n <- [0 .. d]]+    suite =+        concat+            [ [acc ++ middle ++ char | acc <- transitionCover, char <- characterizingSet]+            | middles <- middlesByDepth+            , middle <- middles+            ]++instance EquivalenceOracle WMethod where+    testSuite = wmethodSuite++-- | The 'RandomWMethodConfig' type is used to configure the random W-method.+data RandomWMethodConfig = RandomWMethodConfig+    { rwmGen :: StdGen+    -- ^ The random number generator.+    , rwmLimit :: Int+    -- ^ The maximum number of random words to generate.+    , rwmLength :: Int+    -- ^ The maximum length of the random words.+    }+    deriving (Show, Eq)++-- | The 'RandomWMethod' type represents a random W-method equivalence oracle.+newtype RandomWMethod = RandomWMethod RandomWMethodConfig deriving (Show, Eq)++-- | Constructor for a 'RandomWMethod' value.+mkRandomWMethod :: StdGen -> Int -> Int -> RandomWMethod+mkRandomWMethod g l n = RandomWMethod (RandomWMethodConfig g n l)++-- | The 'randomWMethodSuite' function generates the test suite for the random W-method and a new oracle.+randomWMethodSuite ::+    forall i o s aut.+    ( Automaton aut s i o+    , FiniteOrd i+    , FiniteOrd s+    , Eq o+    ) =>+    RandomWMethod ->+    aut s i o ->+    (RandomWMethod, [[i]])+randomWMethodSuite (RandomWMethod (RandomWMethodConfig g wpr wl)) aut =+    let rorc = RandomWords (RandomWordsConfig{rwMaxLength = wl, rwMinLength = 1, rwLimit = wpr, rwGen = g})+        prefixes = Map.elems $ accessSequences aut+        vecSuffixes = Vec.fromList $ Set.toList $ globalCharacterizingSet aut++        (RandomWords roc', wordBatches) = List.mapAccumL testSuite rorc (replicate (length prefixes) (undefined :: aut s i o))+        flatWords = concat wordBatches++        (gen'', gen''') = split (rwGen roc')+        samples = length prefixes * wpr+        randomSuffixes = take samples $ randomRs (0, Vec.length vecSuffixes - 1) gen''+        suffixes = map (vecSuffixes Vec.!) randomSuffixes++        suite = [prefix ++ rand ++ suffix | prefix <- prefixes, rand <- flatWords, suffix <- suffixes]+     in (mkRandomWMethod gen''' wpr wl, suite)++instance EquivalenceOracle RandomWMethod where+    testSuite = randomWMethodSuite

@@ -0,0 +1,175 @@+{-# LANGUAGE ScopedTypeVariables #-}++-- | This module implements the WpMethod.+module Haal.EquivalenceOracle.WpMethod (+    WpMethod (..),+    RandomWpMethod (..),+    RandomWpMethodConfig (..),+    wpmethodSuiteSize,+    randomWpMethodSuite,+    mkWpMethod,+    mkRandomWpMethod,+) where++import Control.Monad (replicateM)+import Control.Monad.Identity (Identity (runIdentity))+import Control.Monad.State (MonadState (state), State, runState)+import qualified Data.Map as Map+import qualified Data.Set as Set+import Haal.BlackBox+import Haal.Experiment+import System.Random (Random (randomR), StdGen)++-- | Type for the WpMethod. It simply wraps the depth of the method.+newtype WpMethod = WpMethod Int deriving (Eq, Show)++-- | Constructor for a 'WpMethod' value.+mkWpMethod :: Int -> WpMethod+mkWpMethod = WpMethod++-- | The 'wpmethodSuiteSize' returns the nunmber of test cases in the test suite of WpMethod+wpmethodSuiteSize :: a+wpmethodSuiteSize = error "todo"++-- | Returns the test suite for the WpMethod.+wpmethodSuite ::+    forall aut i o s.+    ( Automaton aut s i o+    , FiniteOrd i+    , FiniteOrd s+    , Eq o+    ) =>+    WpMethod ->+    aut s i o ->+    (WpMethod, [[i]])+wpmethodSuite wpm@(WpMethod d) aut = (wpm, suite)+  where+    alphabet = inputs aut+    stateCover = accessSequences aut+    localSuf =+        Map.fromAscList+            [ (st, localCharacterizingSet aut st) | st <- Set.toAscList $ states aut+            ]+    globalSuf = globalCharacterizingSet aut++    transitionCover =+        [ acc ++ [a]+        | acc <- Map.elems stateCover+        , a <- Set.toList alphabet+        ]+    difference =+        Set.fromList (Map.elems stateCover)+            `Set.difference` Set.fromList transitionCover++    firstPhase =+        concat+            [ [ acc ++ middle ++ suf+              | acc <- Map.elems stateCover+              , suf <- Set.toList globalSuf+              ]+            | fixed <- [0 .. d]+            , middle <- replicateM fixed $ Set.toList alphabet+            ]++    secondPhase =+        concat+            [ [ acc ++ middle ++ suf+              | acc <- Set.toList difference+              , suf <- Set.toList $ localSuf Map.! current (fst (runIdentity (walk aut (acc ++ middle))))+              ]+            | fixed <- [0 .. d]+            , middle <- replicateM fixed $ Set.toList alphabet+            ]++    suite = firstPhase ++ secondPhase++{- | The 'RandomWpMethodConfig' is a record data type that represents the configuration for an instance+of the Random WpMethod algorithm.+-}+data RandomWpMethodConfig = RandomWpMethodConfig+    { rwpGen :: StdGen+    -- ^ Random generator.+    , rwpExpected :: Int+    -- ^ Expected depth of random walk.+    , rwpMin :: Int+    -- ^ Minimum depth of random walk.+    , rwpLimit :: Int+    -- ^ Maximum number of queries.+    }+    deriving (Show, Eq)++-- | The 'RandomWpMethod' type is just a wrapper around the config.+newtype RandomWpMethod = RandomWpMethod RandomWpMethodConfig deriving (Show, Eq)++-- | Constructor for a 'RandomWpMethod' value.+mkRandomWpMethod :: RandomWpMethodConfig -> RandomWpMethod+mkRandomWpMethod = RandomWpMethod++-- | Return the 'RandomWpMethod' test suite.+randomWpMethodSuite ::+    forall aut i o s.+    ( Automaton aut s i o+    , FiniteOrd i+    , FiniteOrd s+    , Eq o+    ) =>+    RandomWpMethod ->+    aut s i o ->+    (RandomWpMethod, [[i]])+randomWpMethodSuite+    ( RandomWpMethod+            conf@RandomWpMethodConfig+                { rwpGen = g+                , rwpExpected = e+                , rwpMin = mi+                , rwpLimit = lim+                }+        )+    aut = (RandomWpMethod (conf{rwpGen = genfinal}), suite)+      where+        alphabet = inputs aut+        prefixes = accessSequences aut+        localSuf =+            Map.fromAscList+                [ (st, localCharacterizingSet aut st) | st <- Set.toAscList $ states aut+                ]+        globalSuf = globalCharacterizingSet aut++        (suite, genfinal) = runState (replicateM lim genTestCase) g++        genTestCase :: State StdGen [i]+        genTestCase = do+            prefixIdx <- state $ randomR (0, Map.size prefixes - 1)+            let (_, prefix) = prefixIdx `Map.elemAt` prefixes+            middle <- genExpectedLength+            local <- state $ randomR (False, True)+            if local+                then do+                    let curr = current $ fst (runIdentity (walk aut (prefix ++ middle)))+                        suffixSet = localSuf Map.! curr+                    suffixIdx <- state $ randomR (0, Set.size suffixSet - 1)+                    let suffix = suffixIdx `Set.elemAt` suffixSet+                    return $ prefix ++ middle ++ suffix+                else do+                    globalIdx <- state $ randomR (0, Set.size globalSuf - 1)+                    let suffix = globalIdx `Set.elemAt` globalSuf+                    return $ prefix ++ middle ++ suffix++        genExpectedLength :: State StdGen [i]+        genExpectedLength = state $ go [] mi+          where+            go :: [i] -> Int -> StdGen -> ([i], StdGen)+            go acc minim gen =+                let (continue, gen') = randomR (0.0 :: Double, 1.0) gen+                 in if minim > 0 || continue > 1 / (fromIntegral e + 1)+                        then+                            let (idx, gen'') = randomR (0, Set.size alphabet - 1) gen'+                                nextChar = idx `Set.elemAt` alphabet+                             in go (nextChar : acc) (minim - 1) gen''+                        else (acc, gen)++instance EquivalenceOracle WpMethod where+    testSuite = wpmethodSuite++instance EquivalenceOracle RandomWpMethod where+    testSuite = randomWpMethodSuite

@@ -0,0 +1,208 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE UndecidableInstances #-}++{- | This module exports the basic types, classes and functions that are required to+easily construct and configure learning experiments.+-}+module Haal.Experiment (+    Experiment,+    ExperimentT,+    Learner (..),+    EquivalenceOracle (..),+    Statistics (..),+    experiment,+    runExperiment,+    pairwiseWalk,+    execute,+    findCex,+    runExperimentT,+) where++import Control.Monad.Reader (+    MonadReader (ask),+    MonadTrans (lift),+    Reader,+    ReaderT (runReaderT),+    runReader,+ )++import Control.Monad.Identity+import Haal.BlackBox++{- | The 'EquivalenceOracle' type class defines the interface for equivalence oracles.+Instances of this class should provide methods to generate a test suite+-}+class EquivalenceOracle or where+    testSuite ::+        ( Automaton aut s i o+        , FiniteOrd i+        , FiniteOrd s+        , Eq o+        ) =>+        or ->+        aut s i o ->+        (or, [[i]])++{- | The 'Learner' type class defines the interface for learning algorithms.+Instances of this class should provide methods to initialize the learner,+refine the learner with a counterexample, and learn an automaton. The type @l@+determines the type of automaton @aut@ that is learned.+-}+class Learner l aut s | l -> aut s where+    initialize ::+        ( SUL sul m i o+        , FiniteOrd i+        , Finite o+        ) =>+        l i o ->+        ExperimentT (sul i o) m (l i o)+    refine ::+        ( SUL sul m i o+        , FiniteOrd i+        , Finite o+        ) =>+        l i o ->+        [i] ->+        ExperimentT (sul i o) m (l i o)+    learn ::+        ( SUL sul m i o+        , Automaton aut s i o+        , FiniteOrd i+        , FiniteOrd s+        , FiniteEq o+        ) =>+        l i o ->+        ExperimentT (sul i o) m (l i o, aut s i o)++{- | The 'ExperimentT' type is a monad transformer that allows for+running experiments in a reader monad. This may prove useful for+learning real systems, which requires IO.+-}+type ExperimentT sul m result = ReaderT sul m result++{- | The 'Experiment' type is a type alias for the 'ExperimentT' type+with the 'Identity' monad. This allows for running pure experiments.+-}+type Experiment sul result = ExperimentT sul Identity result++{- | The 'runExperimentT' function runs an experiment in the 'ExperimentT' monad.+It is just an alias for 'runReaderT'.+-}+runExperimentT :: ReaderT r m a -> r -> m a+runExperimentT = runReaderT++{- | The 'runExperiment' function runs an experiment in the 'Experiment' monad.+It is just an alias for 'runReader'.+-}+runExperiment :: Reader r a -> r -> a+runExperiment = runReader++{- | The 'Statistics' data type is parameterized by the type of model being learned+and the state, input and output types of the model. Its purpose is to keep track of+different experimental stats. For the time being, only the number of rounds 'statsRounds',+the counterexamples 'statsCexs' and the intermediate hypotheses 'statsHyps' are being kept+track of.+-}+data Statistics aut s i o = Statistics+    { statsRounds :: Int+    , statsCexs :: [[i]]+    , statsHyps :: [aut s i o]+    }+    deriving (Show)++-- | Empty 'Statistics' value.+mkStats :: Statistics aut s i o+mkStats = Statistics 0 [] []++{- | The 'experiment' function returns an 'Experiment' that can be run with+the 'runExperiment' function. It takes a learner and an equivalence oracle+and then requires a system under learning (SUL) to run the experiment.+-}+experiment ::+    ( SUL sul m i o+    , Automaton aut s i o+    , Learner learner aut s+    , EquivalenceOracle oracle+    , FiniteOrd i+    , FiniteOrd s+    , FiniteEq o+    ) =>+    learner i o ->+    oracle ->+    ExperimentT (sul i o) m (aut s i o, Statistics aut s i o)+experiment learner oracle = do+    initializedLearner <- initialize learner+    let inner le orc stats = do+            (learner', aut) <- learn le+            (oracle', cex) <- findCex orc aut+            case cex of+                ([], []) -> return (aut, stats)+                (ce, _) -> do+                    refinedLearner <- refine learner' ce+                    let rounds = statsRounds stats+                        cexs = statsCexs stats+                        hyps = statsHyps stats+                        stats' = Statistics (rounds + 1) (ce : cexs) (aut : hyps)+                    inner refinedLearner oracle' stats'+    inner initializedLearner oracle mkStats++-- | The 'execute' function executes the test suite of an oracle, given a SUL and an automaton.+execute ::+    ( SUL sul m i o+    , Automaton aut s i o+    , Ord i+    , Eq o+    ) =>+    sul i o ->+    aut s i o ->+    [[i]] ->+    m ([i], [o])+execute _ _ [] = return ([], [])+execute theSul theAut (s : ss) = do+    continue <- pairwiseWalk theSul theAut s+    if continue+        then execute theSul theAut ss+        else do+            (_, out) <- walk theSul s+            return (s, out)++{- | The 'pairwiseWalk' function executes a test case on both the SUL and the automaton+simultaneously, checking if the outputs are the same.+-}+pairwiseWalk ::+    ( SUL sul m i o+    , Automaton aut s i o+    , Ord i+    , Eq o+    ) =>+    sul i o ->+    aut s i o ->+    [i] ->+    m Bool+pairwiseWalk _ _ [] = return True+pairwiseWalk theSul theAut (s : ss) = do+    (sul', out1) <- step theSul s+    let (aut', out2) = runIdentity (step theAut s)+    rest <- pairwiseWalk sul' aut' ss+    return $ out1 == out2 && rest++{- | The 'findCex' function executes the test suite of each oracle to the automaton+and SUL.+-}+findCex ::+    ( SUL sul m i o+    , Automaton aut s i o+    , EquivalenceOracle or+    , FiniteOrd i+    , FiniteOrd s+    , Eq o+    ) =>+    or ->+    aut s i o ->+    ExperimentT (sul i o) m (or, ([i], [o]))+findCex oracle aut = do+    sul <- ask+    let (oracle', theSuite) = testSuite oracle aut+    (cin, cout) <- lift $ execute sul aut theSuite+    return (oracle', (cin, cout))

@@ -0,0 +1,329 @@+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -Wno-redundant-constraints #-}++-- | This module implements the LM* algorithm for learning Mealy automata.+module Haal.Learning.LMstar (+    lmstar,+    LMstar (..),+    LMstarConfig (..),+    mkLMstar,+)+where++import Control.Monad (foldM, forM)+import Control.Monad.Reader (MonadReader (ask), MonadTrans (lift))+import qualified Data.List as List+import qualified Data.Map as Map+import qualified Data.Maybe as Maybe+import qualified Data.Set as Set+import Haal.Automaton.MealyAutomaton+import Haal.BlackBox+import Haal.Experiment++-- | The 'ObservationTable' type is a data type for storing the observation table of the LM* algorithm.+data ObservationTable i o = ObservationTable+    { prefixSetS :: Set.Set [i]+    , suffixSetE :: Set.Set [i]+    , mappingT :: Map.Map ([i], [i]) o+    , -- more fields to avoid recomputing+      prefixSetSI :: Set.Set [i]+    }+    deriving (Show)++{- | The 'LMstarConfig' type is a configuration type for the LM* algorithm.+It allows the user to choose between the original LM* algorithm and the LM+ algorithm.+-}+data LMstarConfig = Star | Plus++-- | The 'LMstar' type is a wrapper around the 'ObservationTable' type and represents the LM* algorithm.+data LMstar i o = LMstar (ObservationTable i o) | LMplus (ObservationTable i o)++{- | The 'mkLMstar' function creates a new instance of the 'LMstar' type. It holds a dummy value+so that the user does not have to provide an initial observation table.+-}+mkLMstar :: LMstarConfig -> LMstar i o+mkLMstar Star = LMstar (error "this is invisible")+mkLMstar Plus = LMplus (error "this is invisible")++-- | The 'equivalentRows' function checks if two rows in the observation table are equivalent.+equivalentRows :: forall i o. (Ord i, Eq o) => ObservationTable i o -> [i] -> [i] -> Bool+equivalentRows ot r1 r2 = and $ Set.map (\e -> mapping (r1, e) == mapping (r2, e)) em+  where+    mapping = flip Map.lookup (mappingT ot)+    em = suffixSetE ot++{- | The 'initializeOT' function initializes the observation table for the LM* algorithm.+It must be in the 'Experiment' monad to allow queries to the SUL.+-}+initializeOT ::+    forall i o sul m.+    (FiniteOrd i, SUL sul m i o) =>+    ExperimentT (sul i o) m (ObservationTable i o)+initializeOT = do+    sul <- ask+    let alph = List.map (: []) $ Set.toList $ inputs sul+        sm = Set.singleton []+        sm_I = Set.fromList alph+        em = Set.fromList alph+        domain = Set.toList $ (sm `Set.union` sm_I) `Set.cartesianProduct` em+    -- monadic mapping because walk is in m+    tmList <- forM domain $ \(in1, in2) -> do+        sul0 <- lift $ reset sul+        (_, outs) <- lift $ walk sul0 (in1 ++ in2)+        pure ((in1, in2), last outs)++    let tm = Map.fromList tmList++    return+        ( ObservationTable+            { prefixSetS = sm+            , suffixSetE = em+            , mappingT = tm+            , prefixSetSI = sm_I+            }+        )++-- | The 'equivalenceClasses' function computes the equivalence classes of the observation table.+equivalenceClasses ::+    forall i o.+    (FiniteOrd i, Eq o) =>+    ObservationTable i o ->+    Map.Map [i] [[i]]+equivalenceClasses ot = go Map.empty (sm `Set.union` sm_I)+  where+    sm = prefixSetS ot+    sm_I = prefixSetSI ot+    go acc s+        | Set.null s = acc+        | otherwise =+            let (x, rest) = Set.deleteFindMin s+                (equivClass, remainder) = Set.partition (equivalentRows ot x) rest+                classMembers = x : Set.toList equivClass+             in go (Map.insert x classMembers acc) remainder++-- | The 'lmstar' function implements one iteration of the LM* algorithm.+lmstar ::+    forall sul i o m.+    (SUL sul m i o, FiniteOrd i, Eq o, Monad m) =>+    LMstar i o ->+    ExperimentT (sul i o) m (LMstar i o, MealyAutomaton StateID i o)+lmstar (LMstar ot) = case otIsClosed ot of+    [] -> case otIsConsistent ot of+        ([], []) -> return (LMstar ot, makeHypothesis ot)+        inc' -> do+            ot' <- makeConsistent ot inc'+            lmstar (LMstar ot')+    inc -> do+        ot' <- makeClosed ot inc+        lmstar (LMstar ot')+lmstar (LMplus ot) = case otIsClosed ot of+    [] -> return (LMplus ot, makeHypothesis ot)+    inc -> do+        ot' <- makeClosed ot inc+        lmstar (LMplus ot')++-- | The 'otIsClosed' function checks if the observation table is closed.+otIsClosed :: forall i o. (FiniteOrd i, Eq o) => ObservationTable i o -> [i]+otIsClosed ot = Maybe.fromMaybe [] exists+  where+    sm = prefixSetS ot+    sm_I = prefixSetSI ot++    exists = List.find (\x -> not $ any (equivalentRows ot x) sm) sm_I++-- | The 'otIsConsistent' function checks if the observation table is consistent.+otIsConsistent :: forall i o. (FiniteOrd i, Eq o) => ObservationTable i o -> ([i], [i])+otIsConsistent ot = Maybe.fromMaybe ([], []) condition+  where+    alph = [minBound .. maxBound] :: [i]+    sm = Set.toList $ prefixSetS ot++    equivalentPairs = [(r1, r2) | r1 <- sm, r2 <- sm, r1 /= r2, equivalentRows ot r1 r2]++    condition =+        List.find+            ( \(a, b) ->+                any+                    (\x -> not (equivalentRows ot (a ++ [x]) (b ++ [x])))+                    alph+            )+            equivalentPairs++-- | The 'otRefineAngluin' function refines the observation table based on a counterexample, according to Angluin's algorithm.+otRefineAngluin ::+    forall sul i o m.+    (FiniteOrd i, SUL sul m i o) =>+    ObservationTable i o ->+    [i] ->+    ExperimentT (sul i o) m (ObservationTable i o)+otRefineAngluin ot [] = return ot+otRefineAngluin ot cex = do+    sul <- ask+    let+        sm = prefixSetS ot+        em = suffixSetE ot+        tm = mappingT ot+        -- insert all prefixes of the counterexample+        sm' = List.foldr Set.insert sm [take n cex | n <- [1 .. length cex]]+        sm_I' = Set.fromList [w ++ [a] | w <- Set.toList sm', a <- Set.toList $ inputs sul]+        missing = (sm' `Set.union` sm_I') `Set.cartesianProduct` em++    tm' <- lift $ updateMap tm missing sul+    let ot' = ObservationTable{prefixSetS = sm', suffixSetE = em, mappingT = tm', prefixSetSI = sm_I'}+    return ot'++{- | The 'makeHypothesis' function constructs a Mealy automaton from the observation table. It uses+the default 'StateID' type defined in the 'Experiment' module for representing the automaton states.+-}+makeHypothesis :: forall i o. (FiniteOrd i, Eq o) => ObservationTable i o -> MealyAutomaton StateID i o+makeHypothesis ot = mkMealyAutomaton delta' lambda' (Set.fromList [0 .. length repList - 1]) starting+  where+    -- Equivalence classes: Map from representative prefix to class members+    equivMap :: Map.Map [i] [[i]]+    equivMap = equivalenceClasses ot++    -- Assign an integer ID to each class representative+    repList :: [[i]]+    repList = Map.keys equivMap++    repToId :: Map.Map [i] StateID+    repToId = Map.fromList (zip repList [0 ..])++    -- Helper: get the ID for the class a string belongs to+    getStateId :: [i] -> StateID+    getStateId s =+        case List.find (equivalentRows ot s) repList of+            Just rep -> repToId Map.! rep+            Nothing -> error "No equivalent class found for string!"++    delta' :: StateID -> i -> StateID+    delta' sid i =+        let rep = repList !! sid+         in getStateId (rep ++ [i])++    lambda' :: StateID -> i -> o+    lambda' sid i =+        let rep = repList !! sid+         in mappingT ot Map.! (rep, [i])++    starting = getStateId []++-- | The 'makeConsistent' function makes the observation table consistent by adding missing prefixes.+makeConsistent ::+    forall i o sul m.+    (FiniteOrd i, SUL sul m i o) =>+    ObservationTable i o ->+    ([i], [i]) ->+    ExperimentT (sul i o) m (ObservationTable i o)+makeConsistent ot ([], []) = return ot+makeConsistent ot (column, symbol) = do+    sul <- ask+    let+        query = symbol ++ column+        -- prefices = [take n query | n <- [1 .. length query]]++        -- only the query itself must be inserted.+        -- the suffixes are already members.+        em = suffixSetE ot+        em' = query `Set.insert` em++        sm = prefixSetS ot+        sm_I = prefixSetSI ot++        tm = mappingT ot++        missing = (sm `Set.union` sm_I) `Set.cartesianProduct` em'+        missing' = map (uncurry (++)) $ Set.toList missing++    outs <- lift $ forM missing' (walk sul)++    let+        outs' = map (last . snd) outs+        tm' = foldr (\((a, b), o) -> Map.insert (a, b) o) tm (zip (Set.toList missing) outs')+    return (ObservationTable{prefixSetS = sm, suffixSetE = em', mappingT = tm', prefixSetSI = sm_I})++-- | The 'makeClosed' function makes the observation table closed by adding missing suffixes.+makeClosed ::+    forall sul i o m.+    (FiniteOrd i, SUL sul m i o) =>+    ObservationTable i o ->+    [i] ->+    ExperimentT (sul i o) m (ObservationTable i o)+makeClosed ot [] = return ot+makeClosed ot inc = do+    sul <- ask+    let+        alph = Set.toList $ inputs sul+        sm = prefixSetS ot+        em = suffixSetE ot+        tm = mappingT ot+        sm' = inc `Set.insert` sm+        sm_I' = Set.fromList [w ++ [a] | w <- Set.toList sm', a <- alph]+    outs <- lift $ forM (Set.toList em) (walk sul)+    let mappings = [((inc ++ [s], e), last (snd o)) | s <- alph, (e, o) <- zip (Set.toList em) outs]+        tm' = List.foldr (uncurry Map.insert) tm mappings+    return (ObservationTable{prefixSetS = sm', suffixSetE = em, mappingT = tm', prefixSetSI = sm_I'})++instance Learner LMstar MealyAutomaton StateID where+    initialize (LMstar _) = do+        LMstar <$> initializeOT+    initialize (LMplus _) = do+        LMplus <$> initializeOT++    refine (LMstar ot) cex = do+        ot' <- otRefineAngluin ot cex+        return (LMstar ot')+    refine (LMplus ot) cex = do+        ot' <- otRefinePlus ot cex+        return (LMplus ot')++    learn (LMstar ot) = lmstar (LMstar ot)+    learn (LMplus ot) = lmstar (LMplus ot)++{- | The 'otRefinePlus' function refines the observation table based on a counterexample, according to the LM+ algorithm,+which is an improvement over Angluin's algorithm.+-}+otRefinePlus ::+    forall sul i o m.+    (FiniteOrd i, SUL sul m i o) =>+    ObservationTable i o ->+    [i] ->+    ExperimentT (sul i o) m (ObservationTable i o)+otRefinePlus ot [] = return ot+otRefinePlus ot cex = do+    sul <- ask+    let sm = prefixSetS ot+        em = suffixSetE ot+        tm = mappingT ot+        sm_I = prefixSetSI ot+        -- look for the longest prefix of the counterexample+        -- that is in sm U sm_I+        prefixes = List.inits cex+        suffixes = List.tails cex+        pairs = List.reverse $ List.zip prefixes suffixes+        wrapped = List.find (\x -> Set.member (fst x) sm || Set.member (fst x) sm_I) pairs+        (_, suffix) = Maybe.fromMaybe (error "failed to update observation table") wrapped+        -- the suffix is the distinguishing suffix. insert all suffixes expect from the empty one+        newSuffixes = em `Set.difference` Set.fromList (init $ List.tails suffix)+        em' = List.foldr Set.insert em newSuffixes+        missing = (sm `Set.union` sm_I) `Set.cartesianProduct` newSuffixes+    tm' <- lift $ updateMap tm missing sul+    return (ObservationTable{prefixSetS = sm, suffixSetE = em', mappingT = tm', prefixSetSI = sm_I})++updateMap ::+    (Ord i, SUL sul m i o, Monad m) =>+    Map.Map ([i], [i]) o ->+    Set.Set ([i], [i]) ->+    sul i o ->+    m (Map.Map ([i], [i]) o)+updateMap themap thestuff thesul =+    foldM+        ( \acc (a, b) -> do+            (_, outs) <- walk thesul (a ++ b)+            let o = last outs+            pure (Map.insert (a, b) o acc)+        )+        themap+        thestuff

@@ -0,0 +1,120 @@+{-# LANGUAGE ScopedTypeVariables #-}++-- | This module tests the Mealy automaton implementation.+module AutomatonSpec (+    spec,+)+where++import qualified Data.List as List+import qualified Data.Map as Map+import qualified Data.Maybe as Maybe+import qualified Data.Set as Set+import Haal.Automaton.MealyAutomaton (+    MealyAutomaton (..),+    mealyDelta,+    mealyLambda,+ )+import Haal.BlackBox+import Test.Hspec (Spec, context, describe, it)+import Test.QuickCheck (Property, property, (==>))+import Utils (Input, Mealy (..), NonMinimalMealy (..), Output, State, statesAreEquivalent)+import Control.Monad.Identity (runIdentity)++-- The global characterizing set of a non minimal mealy automaton contains+-- the empty list. This will fail if the 'State' type has less than 6-7 constructors+-- because a lot of test cases will be discarded.+prop_emptyListInCharacterizingSet :: NonMinimalMealy -> State -> State -> Property+prop_emptyListInCharacterizingSet (NonMinimalMealy automaton) s1 s2 =+    statesAreEquivalent automaton s1 s2+        && s1+            /= s2+                ==> []+                `Set.member` globalCharacterizingSet automaton++-- Two states that are not equivalent can be distinguished.+prop_existsDistinguishingSequence :: Mealy State Input Output -> State -> State -> Property+prop_existsDistinguishingSequence (Mealy automaton) s1 s2 =+    not (statesAreEquivalent automaton s1 s2)+        ==> output1+        /= output2+        && output1 /= []+        && output2 /= []+  where+    dist = distinguish automaton s1 s2+    (_, output1) = runIdentity $ walk (update automaton s1) dist+    (_, output2) = runIdentity $ walk (update automaton s2) dist++-- The map returned by 'mealyTransitions' is equivalent to the 'mealyLambda'+-- and 'mealyDelta' functions of the automaton.+prop_mappingEquivalentToFunctions :: Mealy State Input Output -> Bool+prop_mappingEquivalentToFunctions (Mealy automaton) =+    let transs = transitions automaton+        alphabet = Set.toList $ inputs automaton+        sts = Set.toList $ states automaton+        -- Calculate outputs using mealyDelta and mealyLambda+        mapOutputs =+            [ Maybe.fromJust (Map.lookup (s, a) transs)+            | s <- sts+            , a <- alphabet+            ]+        funOutputs = [(mealyDelta automaton s a, mealyLambda automaton s a) | s <- sts, a <- alphabet]+     in mapOutputs == funOutputs++-- The access sequences returned by 'mealyAccessSequences' cover all reachable states.+prop_completeAccessSequences :: Mealy State Input Output -> Property+prop_completeAccessSequences (Mealy automaton) = sts == rsts ==> allin+  where+    seqs = accessSequences automaton+    sts = states automaton+    rsts = reachable automaton+    allin = all (`Map.member` seqs) rsts++-- The access sequences returned by 'mealyAccessSequences' are the shortest+prop_shortestAccessSequences :: Mealy State Input Output -> State -> State -> Property+prop_shortestAccessSequences (Mealy automaton) s1 s2 =+    s1 `Set.member` rsts+        && s2 `Set.member` rsts+        && existsS1toS2 ==> List.length seq2 <= List.length seq1 + 1+  where+    rsts = reachable automaton+    transs = transitions automaton+    accessSeqs = accessSequences automaton+    seq1 = accessSeqs Map.! s1+    seq2 = accessSeqs Map.! s2+    -- find transition in map (s, i) -> (s, o)+    -- that leads from s1 to s2+    listed = Map.toList transs+    filtering (s, i) = s == s1 && fst (transs Map.! (s, i)) == s2+    maybeTransition = List.find filtering $ List.map fst listed+    existsS1toS2 = case maybeTransition of+        Nothing -> False+        Just _ -> True++spec :: Spec+spec = do+    describe "Blackbox.distinguish for MealyAutomaton" $+        context "if 2 automatons states are not equivalent" $+            it "returns an input sequence that distinguishes them" $+                property+                    prop_existsDistinguishingSequence++    describe "BlackBox.globalCharacterizingSet for MealyAutomaton" $+        context "if the automaton contains at least 2 equivalent states" $+            it "returns a set that contains the empty list" $+                property+                    prop_emptyListInCharacterizingSet++    describe "MealyAutomaton.mealyTransitions" $+        it "returns a map equivalent to the transition and output functions of the model" $+            property+                prop_mappingEquivalentToFunctions++    describe "BlackBox.accessSequences for MealyAutomaton" $ do+        it "returns a map from states to list of inputs that covers all reachable states" $+            property+                prop_completeAccessSequences++        it "returns a map from reachable states to shortest list of inputs that access them" $+            property+                prop_shortestAccessSequences

@@ -0,0 +1,82 @@+module EquivalenceOracleSpec (+    spec,+) where++import Control.Monad.Reader+import Haal.EquivalenceOracle.WMethod (WMethod (..), wmethodSuiteSize)+import Haal.Experiment+import Test.Hspec (Spec, context, describe, it)+import Test.QuickCheck (Property, property, (==>))+import Utils++-- Generic identity and difference properties+prop_identity :: (OracleWrapper w oracle) => Mealy State Input Output -> w -> Bool+prop_identity (Mealy aut) w = ([], []) == snd (runReader (findCex (unwrap w) aut) aut)++prop_difference :: (OracleWrapper w oracle) => Mealy State Input Output -> Mealy State Input Output -> w -> Property+prop_difference (Mealy aut1) (Mealy aut2) w =+    aut1 /= aut2 ==> ([], []) /= snd (runReader (findCex (unwrap w) aut1) aut2)++-- WMethod-specific cardinality law+prop_WMethodCardinality :: ArbWMethod -> Mealy State Input Output -> Bool+prop_WMethodCardinality (ArbWMethod (WMethod d)) (Mealy aut) =+    length (snd (testSuite (WMethod d) aut)) == wmethodSuiteSize (WMethod d) aut++spec :: Spec+spec = do+    describe "WMethod Equivalence Oracle" $ do+        context "when two automatons differ" $+            it "WMethod returns Just" $+                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbWMethod -> Property)++        context "when two automatons are the same" $+            it "WMethod returns Nothing" $+                property (prop_identity :: Mealy State Input Output -> ArbWMethod -> Bool)++        it "computes the correct WMethod test suite size" $+            property prop_WMethodCardinality++    describe "WpMethod Equivalence Oracle" $ do+        context "when two automatons differ" $+            it "WpMethod returns Just" $+                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbWpMethod -> Property)++        context "when two automatons are the same" $+            it "WpMethod returns Nothing" $+                property (prop_identity :: Mealy State Input Output -> ArbWpMethod -> Bool)++    describe "RandomWords Equivalence Oracle" $ do+        context "when two automatons differ" $+            it "RandomWords returns Just" $+                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbRandomWords -> Property)++        context "when two automatons are the same" $+            it "RandomWords returns Nothing" $+                property (prop_identity :: Mealy State Input Output -> ArbRandomWords -> Bool)++    describe "RandomWalk Equivalence Oracle" $ do+        context "when two automatons differ" $+            it "RandomWalk returns Just" $+                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbRandomWalk -> Property)++        context "when two automatons are the same" $+            it "RandomWalk returns Nothing" $+                property (prop_identity :: Mealy State Input Output -> ArbRandomWalk -> Bool)++    describe "RandomWMethod Equivalence Oracle" $ do+        context "when two automatons differ" $+            it "RandomWMethod returns Just" $+                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbRandomWMethod -> Property)++        context "when two automatons are the same" $+            it "RandomWMethod returns Nothing" $+                property (prop_identity :: Mealy State Input Output -> ArbRandomWMethod -> Bool)++    describe "RandomWpMethod Equivalence Oracle" $ do+        context "when two automatons differ" $+            it "RandomWpMethod returns Just" $+                property (prop_difference :: Mealy State Input Output -> Mealy State Input Output -> ArbRandomWpMethod -> Property)++        context "when two automatons are the same" $+            it "RandomWpMethod returns Nothing" $+                property (prop_identity :: Mealy State Input Output -> ArbRandomWpMethod -> Bool)

@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}

@@ -0,0 +1,301 @@+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Utils (+    statesAreEquivalent,+    NonMinimalMealy (..),+    Mealy (..),+    Input (..),+    Output (..),+    State (..),+    ArbWMethod (..),+    ArbWpMethod (..),+    ArbRandomWords (..),+    ArbRandomWalk (..),+    ArbRandomWMethod (..),+    ArbRandomWpMethod (..),+    OracleWrapper (..),+)+where++import qualified Data.Bifunctor as Bif+import qualified Data.List as List+import qualified Data.Map as Map+import qualified Data.Maybe+import qualified Data.Set as Set+import Haal.Automaton.MealyAutomaton (+    MealyAutomaton (..),+    mealyDelta,+    mealyLambda,+ )+import Haal.BlackBox+import Haal.EquivalenceOracle.RandomWalk (+    RandomWalk (RandomWalk),+    RandomWalkConfig (RandomWalkConfig),+ )+import Haal.EquivalenceOracle.RandomWords (+    RandomWords (RandomWords),+    RandomWordsConfig (RandomWordsConfig),+ )+import Haal.EquivalenceOracle.WMethod (+    RandomWMethod (RandomWMethod),+    RandomWMethodConfig (RandomWMethodConfig),+    WMethod (WMethod),+    mkWMethod,+ )+import Haal.EquivalenceOracle.WpMethod (+    RandomWpMethod (RandomWpMethod),+    RandomWpMethodConfig (RandomWpMethodConfig),+    WpMethod (WpMethod),+    mkWpMethod,+ )+import Haal.Experiment (EquivalenceOracle)+import System.Random+import Test.QuickCheck (Arbitrary (..), Gen, choose, elements, vectorOf)++newtype ArbWMethodConfig = ArbWMethodConfig Int deriving (Show, Eq)+newtype ArbWMethod = ArbWMethod WMethod deriving (Show, Eq)++newtype ArbWpMethodConfig = ArbWpMethodConfig Int deriving (Show, Eq)+newtype ArbWpMethod = ArbWpMethod WpMethod deriving (Show, Eq)++newtype ArbRandomWordsConfig = ArbRandomWordsConfig RandomWordsConfig deriving (Show, Eq)+newtype ArbRandomWords = ArbRandomWords RandomWords deriving (Show, Eq)++newtype ArbRandomWalkConfig = ArbRandomWalkConfig RandomWalkConfig deriving (Show, Eq)+newtype ArbRandomWalk = ArbRandomWalk RandomWalk deriving (Show, Eq)++newtype ArbRandomWMethodConfig = ArbRandomWMethodConfig RandomWMethodConfig deriving (Show, Eq)+newtype ArbRandomWMethod = ArbRandomWMethod RandomWMethod deriving (Show, Eq)++newtype ArbRandomWpMethodConfig = ArbRandomWpMethodConfig RandomWpMethodConfig deriving (Show, Eq)+newtype ArbRandomWpMethod = ArbRandomWpMethod RandomWpMethod deriving (Show, Eq)++instance Arbitrary ArbWMethodConfig where+    arbitrary = do+        d <- choose (1, 5)+        return (ArbWMethodConfig d)+instance Arbitrary ArbWMethod where+    arbitrary = do+        (ArbWMethodConfig config) <- arbitrary :: Gen ArbWMethodConfig+        return (ArbWMethod (mkWMethod config))++instance Arbitrary ArbWpMethodConfig where+    arbitrary = do+        d <- choose (1, 5)+        return (ArbWpMethodConfig d)+instance Arbitrary ArbWpMethod where+    arbitrary = do+        (ArbWpMethodConfig config) <- arbitrary :: Gen ArbWpMethodConfig+        return (ArbWpMethod (mkWpMethod config))++instance Arbitrary ArbRandomWordsConfig where+    arbitrary = do+        lim <- choose (100, 10000)+        minL <- choose (1, 10)+        maxL <- choose (minL, 11)+        seed <- choose (17, 69)+        let randGen = mkStdGen seed+        return (ArbRandomWordsConfig (RandomWordsConfig randGen lim minL maxL))+instance Arbitrary ArbRandomWords where+    arbitrary = do+        (ArbRandomWordsConfig config) <- arbitrary :: Gen ArbRandomWordsConfig+        return (ArbRandomWords (RandomWords config))++instance Arbitrary ArbRandomWalkConfig where+    arbitrary = do+        lim <- choose (100, 10000)+        restart <- choose (0.0, 1.0)+        seed <- choose (17, 69)+        let randGen = mkStdGen seed+        return (ArbRandomWalkConfig (RandomWalkConfig randGen lim restart))+instance Arbitrary ArbRandomWalk where+    arbitrary = do+        (ArbRandomWalkConfig config) <- arbitrary :: Gen ArbRandomWalkConfig+        return (ArbRandomWalk (RandomWalk config))++instance Arbitrary ArbRandomWMethodConfig where+    arbitrary = do+        seed <- choose (17, 69)+        let randGen = mkStdGen seed+        wpr <- choose (10, 20)+        wl <- choose (1, 5)+        return (ArbRandomWMethodConfig (RandomWMethodConfig randGen wpr wl))+instance Arbitrary ArbRandomWMethod where+    arbitrary = do+        (ArbRandomWMethodConfig config) <- arbitrary :: Gen ArbRandomWMethodConfig+        return (ArbRandomWMethod (RandomWMethod config))++instance Arbitrary ArbRandomWpMethodConfig where+    arbitrary = do+        seed <- choose (17, 69)+        let randGen = mkStdGen seed+        e <- choose (1, 10)+        m <- choose (1, e)+        l <- choose (1, 10000)+        return (ArbRandomWpMethodConfig (RandomWpMethodConfig randGen e m l))++instance Arbitrary ArbRandomWpMethod where+    arbitrary = do+        (ArbRandomWpMethodConfig config) <- arbitrary :: Gen ArbRandomWpMethodConfig+        return (ArbRandomWpMethod (RandomWpMethod config))++class (EquivalenceOracle oracle) => OracleWrapper w oracle | w -> oracle where+    unwrap :: w -> oracle++instance OracleWrapper ArbWMethod WMethod where+    unwrap (ArbWMethod o) = o++instance OracleWrapper ArbWpMethod WpMethod where+    unwrap (ArbWpMethod o) = o++instance OracleWrapper ArbRandomWords RandomWords where+    unwrap (ArbRandomWords o) = o++instance OracleWrapper ArbRandomWalk RandomWalk where+    unwrap (ArbRandomWalk o) = o++instance OracleWrapper ArbRandomWMethod RandomWMethod where+    unwrap (ArbRandomWMethod o) = o++instance OracleWrapper ArbRandomWpMethod RandomWpMethod where+    unwrap (ArbRandomWpMethod o) = o++newtype Mealy s i o = Mealy (MealyAutomaton s i o) deriving (Show)++instance+    ( Arbitrary i+    , Arbitrary o+    , Arbitrary s+    , FiniteOrd i+    , FiniteOrd o+    , FiniteOrd s+    ) =>+    Arbitrary (Mealy s i o)+    where+    arbitrary = do+        let sts = [minBound .. maxBound]+        delta <- generateDelta sts+        lambda <- generateLambda sts++        initialState <- arbitrary+        currentState <- arbitrary++        return+            ( Mealy+                ( MealyAutomaton+                    { mealyDelta = delta+                    , mealyLambda = lambda+                    , mealyInitialS = initialState+                    , mealyCurrentS = currentState+                    , mealyStates = Set.fromList sts+                    }+                )+            )+      where+        generateDelta :: [s] -> Gen (s -> i -> s)+        generateDelta sts = do+            let+                ins = Set.toList $ inputs (undefined :: MealyAutomaton s i o)+                complete = [(st, inp) | st <- sts, inp <- ins]+                (numS, numI) = Bif.bimap List.length List.length (sts, ins)+            matching <- vectorOf (numS * numI) (choose (0, numS - 1))+            let stateOutputs = [sts !! index | index <- matching]+                stateMappings = Map.fromList $ List.zip complete stateOutputs+            fallbackState <- arbitrary :: Gen s+            return $ \s i -> Data.Maybe.fromMaybe fallbackState (Map.lookup (s, i) stateMappings)++        generateLambda :: [s] -> Gen (s -> i -> o)+        generateLambda sts = do+            let+                ins = Set.toList $ inputs (undefined :: MealyAutomaton s i o)+                outs = Set.toList $ outputs (undefined :: MealyAutomaton s i o)+                complete = [(st, inp) | st <- sts, inp <- ins]+                (numS, numI) = Bif.bimap List.length List.length (sts, ins)+                numO = List.length outs+            matching <- vectorOf (numS * numI) (choose (0, numO - 1))+            let outputOutputs = [outs !! index | index <- matching]+                outputMappings = Map.fromList $ List.zip complete outputOutputs+            fallbackOutput <- arbitrary :: Gen o+            return $ \s i -> Data.Maybe.fromMaybe fallbackOutput (Map.lookup (s, i) outputMappings)++data Input = A | B | C | D deriving (Show, Eq, Ord, Enum, Bounded)+data Output = X | Y | Z | W deriving (Show, Eq, Ord, Enum, Bounded)+data State = S0 | S1 | S2 | S3 | S4 | S5 | S6 | S7 deriving (Show, Eq, Ord, Enum, Bounded)++-- Arbitrary instances for Input, Output, and State+instance Arbitrary Input where+    arbitrary = elements [A, B, C, D]++instance Arbitrary Output where+    arbitrary = elements [X, Y, Z, W]++instance Arbitrary State where+    arbitrary = elements [S0, S1, S2, S3, S4, S5, S6, S7]++newtype NonMinimalMealy = NonMinimalMealy (MealyAutomaton State Input Output) deriving (Show)++instance Arbitrary NonMinimalMealy where+    arbitrary = do+        let sts = [minBound .. maxBound]+        delta <- generateDelta sts+        lambda <- generateLambda sts++        initialState <- arbitrary :: Gen State+        currentState <- arbitrary :: Gen State++        return+            ( NonMinimalMealy+                ( MealyAutomaton+                    { mealyDelta = delta+                    , mealyLambda = lambda+                    , mealyInitialS = initialState+                    , mealyCurrentS = currentState+                    , mealyStates = Set.fromList sts+                    }+                )+            )+      where+        generateDelta :: [State] -> Gen (State -> Input -> State)+        generateDelta sts = do+            let+                ins = Set.toList $ inputs (undefined :: MealyAutomaton State Input Output)+                (numS, numI) = Bif.bimap List.length List.length (sts, ins)+                same = numS `div` 2+                nonMinimal = [(st, inp) | st <- take same sts, inp <- ins]+                rest = [(st, inp) | st <- drop same sts, inp <- ins]+            nonMinimalMatching1 <- vectorOf numI (choose (0, numS - 1))+            nonMinimalMatching2 <- vectorOf ((numS - same) * numI) (choose (0, numS - 1))+            let stateOutputs1 = [sts !! index | index <- concat (replicate same nonMinimalMatching1)]+                stateOutputs2 = [sts !! index | index <- nonMinimalMatching2]+                nonMinimalMappings = Map.fromList $ List.zip (nonMinimal ++ rest) (stateOutputs1 ++ stateOutputs2)+            fallbackState <- arbitrary :: Gen State+            return $ \s i -> Data.Maybe.fromMaybe fallbackState (Map.lookup (s, i) nonMinimalMappings)++        generateLambda :: [State] -> Gen (State -> Input -> Output)+        generateLambda sts = do+            let+                ins = Set.toList $ inputs (undefined :: MealyAutomaton State Input Output)+                outs = Set.toList $ outputs (undefined :: MealyAutomaton State Input Output)+                same = numS `div` 2+                nonMinimal = [(st, inp) | st <- take same sts, inp <- ins]+                rest = [(st, inp) | st <- drop same sts, inp <- ins]+                (numS, numI) = Bif.bimap List.length List.length (sts, ins)+                numO = List.length outs+            nonMinimalMatching1 <- vectorOf numI (choose (0, numO - 1))+            nonMinimalMatching2 <- vectorOf ((numS - same) * numI) (choose (0, numO - 1))+            let outputOutputs1 = [outs !! index | index <- concat (replicate same nonMinimalMatching1)]+                outputOutputs2 = [outs !! index | index <- nonMinimalMatching2]+                outputMappings = Map.fromList $ List.zip (nonMinimal ++ rest) (outputOutputs1 ++ outputOutputs2)+            fallbackOutput <- arbitrary :: Gen Output+            return $ \s i -> Data.Maybe.fromMaybe fallbackOutput (Map.lookup (s, i) outputMappings)++-- Two states are equivalent if their delta and lambda functions are equivalent.+statesAreEquivalent :: MealyAutomaton State Input Output -> State -> State -> Bool+statesAreEquivalent _ s1 s2 | s1 == s2 = True+statesAreEquivalent automaton s1 s2 =+    all (\i -> (delta s1 i, lambda s1 i) == (delta s2 i, lambda s2 i)) alphabet+  where+    delta = mealyDelta automaton+    lambda = mealyLambda automaton+    alphabet = inputs automaton