Adds more example on residual languages

NominalAngluin.cabal

@@ -16,6 +16,8 @@ executable NominalAngluin
     Examples.Contrived,
     Examples.ContrivedNFAs,
     Examples.Fifo,
+    Examples.NonResidual,
+    Examples.Residual,
     Examples.RunningExample,
     Examples.Stack,
     NLStar,
@@ -46,6 +48,8 @@ executable NominalAngluin2
     Examples.Contrived,
     Examples.ContrivedNFAs,
     Examples.Fifo,
+    Examples.NonResidual,
+    Examples.Residual,
     Examples.RunningExample,
     Examples.Stack,
     NLStar,

src/Examples.hs

@@ -3,6 +3,8 @@ module Examples
     , module Examples.Contrived
     , module Examples.ContrivedNFAs
     , module Examples.Fifo
+    , module Examples.NonResidual
+    , module Examples.Residual
     , module Examples.RunningExample
     , module Examples.Stack
     ) where
@@ -10,6 +12,8 @@ module Examples
 import           Examples.Contrived
 import           Examples.ContrivedNFAs
 import           Examples.Fifo
+import           Examples.NonResidual
+import           Examples.Residual
 import           Examples.RunningExample
 import           Examples.Stack
 import           NLambda            (Atom)

src/Examples/NonResidual.hs

@@ -0,0 +1,42 @@
+{-# language DeriveAnyClass #-}
+{-# language DeriveGeneric #-}
+module Examples.NonResidual where
+
+{- The language { u d e v d f | u,v words and d,e,f atoms such that e!=f }
+   This should be non-guessing and non-residual 5-state NFA.
+
+   This cannot be learned by NL*, because the poset of residual languages
+   is too complicated. (It is not generated by an orbit-finite set of
+   join-irreducible elements.)
+-}
+
+import NLambda
+
+import GHC.Generics (Generic)
+import Prelude (Eq, Ord, Show)
+import qualified Prelude ()
+
+-- Parametric in the alphabet, because why not?
+data NonResidual a = Q1 | Q2 a | Q3 a a | Q4 a | Q5
+  deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
+
+exampleNonResidual :: Automaton (NonResidual Atom) Atom
+exampleNonResidual = automaton
+    -- state space
+    (fromList [Q1, Q5]
+        `union` map Q2 atoms
+        `union` map Q4 atoms
+        `union` pairsWith Q3 atoms atoms)
+    -- alphabet
+    atoms
+    -- transition relation
+    (map (\d -> (Q1, d, Q1)) atoms
+        `union` map (\d -> (Q1, d, Q2 d)) atoms
+        `union` pairsWith (\d e -> (Q2 d, e, Q3 d e)) atoms atoms
+        `union` triplesWith (\d e f -> (Q3 d e, f, Q3 d e)) atoms atoms atoms
+        `union` pairsWith (\d e -> (Q3 d e, d, Q4 e)) atoms atoms
+        `union` pairsWithFilter (\e f -> maybeIf (e `neq` f) (Q4 e, f, Q5)) atoms atoms)
+    -- initial states
+    (singleton Q1)
+    -- final states
+    (singleton Q5)

src/Examples/Residual.hs

@@ -0,0 +1,63 @@
+{-# language DeriveAnyClass #-}
+{-# language DeriveGeneric #-}
+module Examples.Residual
+  ( exampleResidual1
+  , exampleResidual2
+  ) where
+
+import Examples.Fifo (DataInput (..))
+import NLambda
+
+import GHC.Generics (Generic)
+import Prelude (Eq, Ord, Read, Show)
+import qualified Prelude ()
+
+data Res1 a = QR1 a | QR2 | QAncStar
+  deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
+
+exampleResidual1 :: Automaton (Res1 Atom) DataInput
+exampleResidual1 = automaton
+    -- state space
+    (fromList [QR2, QAncStar]
+        `union` map QR1 atoms)
+    -- alphabet
+    (map Put atoms `union` map Get atoms)
+    -- transition relation
+    (map (\a -> (QR1 a, Get a, QR1 a)) atoms
+        `union` pairsWithFilter (\a b -> maybeIf (a `neq` b) (QR1 a, Put b, QR1 a)) atoms atoms
+        `union` map (\a -> (QR1 a, Put a, QR2)) atoms
+        `union` map (\a -> (QAncStar, Put a, QAncStar)) atoms)
+    -- initial states
+    (map QR1 atoms `union` singleton QAncStar)
+    -- final states
+    (fromList [QR2, QAncStar])
+
+
+-- Example when learning breaks
+data Res2 a = Guess a | GuessConfused a | Accept
+  deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
+
+data AlphabetR a = A a | Anc a
+  deriving (Eq, Ord, Show, Read, Generic, NominalType, Contextual)
+
+exampleResidual2 :: Automaton (Res2 Atom) (AlphabetR Atom)
+exampleResidual2 = automaton
+    -- state space
+    (singleton Accept
+        `union` map Guess atoms
+        `union` map GuessConfused atoms)
+    -- alphabet
+    (map Anc atoms `union` map A atoms)
+    -- transition relation
+    (map (\a -> (Guess a, A a, Accept)) atoms
+        `union` map (\a -> (GuessConfused a, A a, Accept)) atoms
+        `union` map (\a -> (Guess a, Anc a, Accept)) atoms
+        `union` map (\a -> (GuessConfused a, Anc a, Accept)) atoms
+        `union` pairsWithFilter (\a b -> maybeIf (a `neq` b) (Guess a, A b, Guess a)) atoms atoms
+        `union` pairsWithFilter (\a b -> maybeIf (a `neq` b) (GuessConfused a, A b, GuessConfused a)) atoms atoms
+        `union` pairsWithFilter (\a b -> maybeIf (a `neq` b) (Guess a, Anc b, GuessConfused a)) atoms atoms
+        `union` map (\a -> (GuessConfused a, A a, Guess a)) atoms)
+    -- initial states
+    (map Guess atoms)
+    -- final states
+    (fromList [Accept])

src/Main.hs

@@ -12,13 +12,16 @@ import           NLambda
 
 import           Prelude hiding (map)
 
-data Learner = NomLStar | NomLStarCol | NomNLStar
+data Learner
+  = NomLStar -- nominal L* for nominal automata
+  | NomLStarCol -- nominal L* with counterexamples as columns (suffix closed)
+  | NomNLStar -- NL* for nominal automata, counterexamples as columns (suffix closed)
   deriving (Show, Read)
 
 data Teacher = EqDFA | EqNFA Int
   deriving (Show, Read)
 
-data Aut = Fifo Int | Stack Int | Running Int | NFA1 | Bollig Int
+data Aut = Fifo Int | Stack Int | Running Int | NFA1 | Bollig Int | NonResidual | Residual1 | Residual2
   deriving (Show, Read)
 
 -- existential wrapper
@@ -32,6 +35,9 @@ mainExample learnerName teacherName autName = do
             Running n -> A $ Examples.runningExample atoms n
             NFA1      -> A $ Examples.exampleNFA1
             Bollig n  -> A $ Examples.exampleNFA2 n
+            NonResidual -> A $ Examples.exampleNonResidual
+            Residual1 -> A $ Examples.exampleResidual1
+            Residual2 -> A $ Examples.exampleResidual2
     let teacher = case read teacherName of
             EqDFA   -> teacherWithTarget automaton
             EqNFA k -> teacherWithTargetNonDet k automaton