Two things: Optimisations (now only adds one row to fix closedness, and one column to fix inconsistencies) and IO (now also speaks the protocol used in the new paper)

NominalAngluin.cabal

@@ -32,3 +32,32 @@ executable NominalAngluin
     NLambda >= 1.1
   hs-source-dirs:      src
   default-language:    Haskell2010
+
+executable NominalAngluin2
+  ghc-options:
+    -O2
+  main-is:             Main2.hs
+  other-modules:
+    AbstractLStar,
+    Angluin,
+    Bollig,
+    Examples,
+    Examples.Contrived,
+    Examples.ContrivedNFAs,
+    Examples.Fifo,
+    Examples.RunningExample,
+    Examples.Stack,
+    NLStar,
+    ObservationTable,
+    Teacher,
+    Teachers.Teacher,
+    Teachers.Terminal,
+    Teachers.Whitebox
+  build-depends:
+    base >= 4.8 && < 5,
+    containers,
+    haskeline,
+    mtl,
+    NLambda >= 1.1
+  hs-source-dirs:      src
+  default-language:    Haskell2010

src/AbstractLStar.hs

@@ -54,13 +54,17 @@ learn makeComplete handleCounterExample constructHypothesis teacher s =
     let h = constructHypothesis s2 in
     traceShow h $
     trace "3. Equivalent? " $
-    let eq = equivalent teacher h in
+    eqloop s2 h
-    traceShow eq $
+    where
-    case eq of
+        eqloop s2 h = case equivalent teacher h of
-        Nothing -> h
+                          Nothing -> trace "Yes" $ h
-        Just ce -> do
+                          Just ces -> trace "No" $
-            let s3 = handleCounterExample teacher s2 ce
+                              case isTrue . isEmpty $ realces h ces of
+                                  True -> eqloop s2 h
+                                  False ->
+                                      let s3 = handleCounterExample teacher s2 ces in
                                       learn makeComplete handleCounterExample constructHypothesis teacher s3
+        realces h ces = NLambda.filter (\(ce, a) -> a `neq` accepts h ce) $ membership teacher ces
 
 -- Initial state is always the same in our case
 constructEmptyState :: LearnableAlphabet i => Teacher i -> State i

src/Angluin.hs

@@ -11,22 +11,25 @@ import NLambda
 import qualified Prelude hiding ()
 import Prelude (Bool(..), Maybe(..), id, ($), (.), (++), fst, show)
 
+justOne :: (Contextual a, NominalType a) => Set a -> Set a
+justOne s = mapFilter id . orbit [] . element $ s
+
 -- We can determine its completeness with the following
 -- It returns all witnesses (of the form sa) for incompleteness
-closednessTest :: NominalType i => State i -> TestResult i
+closednessTest :: LearnableAlphabet i => State i -> TestResult i
 closednessTest State{..} = case solve (isEmpty defect) of
     Just True  -> Succes
-    Just False -> trace "Not closed" $ Failed defect empty
+    Just False -> trace "Not closed" $ Failed (justOne defect) empty
     where
         sss = map (row t) ss                 -- all the rows
         hasEqRow = contains sss . row t      -- has equivalent upper row
         defect = filter (not . hasEqRow) ssa -- all rows without equivalent guy
 
 -- We look for inconsistencies and return columns witnessing it
-consistencyTestDirect :: NominalType i => State i -> TestResult i
+consistencyTestDirect :: LearnableAlphabet i => State i -> TestResult i
 consistencyTestDirect State{..} = case solve (isEmpty defect) of
     Just True  -> Succes
-    Just False -> trace "Not consistent" $ Failed empty defect
+    Just False -> trace "Not consistent" $ Failed empty (justOne defect)
     where
         ssRows = map (\u -> (u, row t u)) ss
         candidates = pairsWithFilter (\(u1,r1) (u2,r2) -> maybeIf (u1 `neq` u2 /\ r1 `eq` r2) (u1, u2)) ssRows ssRows

src/Teacher.hs

@@ -6,6 +6,7 @@ module Teacher
     , teacherWithTarget
     , teacherWithTargetNonDet
     , teacherWithIO
+    , teacherWithIO2
     , teacherWithTargetAndIO
     ) where
 
@@ -53,6 +54,14 @@ teacherWithIO alph = Teacher
     , alphabet   = alph
     }
 
+-- 2b. Same as above. But with machine readable queries (except for EQs maybe)
+teacherWithIO2 :: (Show i, Read i, NominalType i, Contextual i) => Set i -> Teacher i
+teacherWithIO2 alph = Teacher
+    { membership = ioMembership2
+    , equivalent = ioEquivalent2
+    , alphabet   = alph
+    }
+
 -- 3. A teacher uses a target for the mebership queries, but you for equivalence
 -- Useful as long as you don't have an equivalence check
 -- used for NFAs when there was no bounded bisimulation yet

src/Teachers/Terminal.hs

@@ -4,6 +4,7 @@ import NLambda
 
 import Control.Monad
 import Data.IORef
+import Data.List (intersperse, concat)
 import Prelude hiding (filter, map, and, sum)
 import System.Console.Haskeline
 import System.IO.Unsafe (unsafePerformIO)
@@ -41,6 +42,34 @@ ioMembership queries = unsafePerformIO $ do
         mqCache = unsafePerformIO $ newIORef empty
 
 
+-- Same as above, but with a machine-readable format
+ioMembership2 :: (Show i, NominalType i, Contextual i) => Set [i] -> Set ([i], Formula)
+ioMembership2 queries = unsafePerformIO $ do
+    cache <- readIORef mqCache
+    let cachedAnswers = filter (\(a, f) -> a `member` queries) cache
+    let newQueries = simplify $ queries \\ map fst cache
+    let representedInputs = toList . mapFilter id . setOrbitsRepresentatives $ newQueries
+    answers <- forM representedInputs $ \input -> do
+        let str = Data.List.concat . intersperse " " . fmap show $ input
+        putStrLn $ "MQ \"" ++ str ++ "\""
+        let askit = do
+                x <- getInputLine ""
+                case x of
+                    Just "Y" -> return True
+                    Just "N" -> return False
+                    _ -> error "Unable to parse, or quit. Bye!"
+        answer <- runInputT defaultSettings askit
+        return $ orbit [] (input, fromBool answer)
+    let answersAsSet = simplify . sum . fromList $ answers
+    writeIORef mqCache (simplify $ cache `union` answersAsSet)
+    return (simplify $ cachedAnswers `union` answersAsSet)
+    where
+        -- We use a cache, so that questions will not be repeated.
+        -- It is a bit hacky, as the Teacher interface does not allow state...
+        {-# NOINLINE mqCache #-}
+        mqCache = unsafePerformIO $ newIORef empty
+
+
 -- Poses a query to the terminal, waiting for the user to provide a counter example
 -- TODO: extend to any alphabet type (hard because of parsing)
 ioEquivalent :: (Show q, NominalType q, Show i, Read i, NominalType i) => Automaton q i -> Maybe (Set [i])
@@ -56,8 +85,29 @@ ioEquivalent hypothesis = unsafePerformIO $ do
                     outputStrLn $ "Ok, we're done"
                     return Nothing
                 Just Nothing -> do
-                    outputStrLn $ "Unable to parse, try again"
+                    outputStrLn $ "Unable to parse (88), try again"
                     loop
                 Just (Just f) -> return (Just f)
     answer <- runInputT defaultSettings loop
     return (orbit [] <$> answer)
+
+-- Same as above but in different format.
+ioEquivalent2 :: (Show q, NominalType q, Show i, Read i, NominalType i) => Automaton q i -> Maybe (Set [i])
+ioEquivalent2 hypothesis = unsafePerformIO $ do
+    putStrLn "EQ\n\"Is the following automaton correct?"
+    print hypothesis
+    putStrLn "\""
+    let loop = do
+            x <- getInputLine ""
+            case x of
+                Just "Y" -> return Nothing
+                Just ('N' : ' ' : ce) -> return (Just (readCE ce))
+                _ -> error "Unable to parse (104), or quit. Bye!"
+    answer <- runInputT defaultSettings loop
+    return (orbit [] <$> answer)
+    where
+        readCE [] = []
+        readCE (' ' : xs) = readCE xs
+        readCE xs = case reads xs of
+            [(a, str)] -> a : readCE str
+            _ -> error "Unable to parse (113)"