Adds better support for counter membership queries

VERY EXPERIMENTAL AND SLOW

src/ObservationTable.hs

@@ -14,7 +14,7 @@ import           Control.DeepSeq (NFData, force)
 import           Data.Maybe   (fromJust)
 import           Debug.Trace  (trace)
 import           GHC.Generics (Generic)
-import           Prelude      (Bool (..), Eq, Ord, Show (..), ($), (++), (.), uncurry)
+import           Prelude      (Bool (..), Eq, Ord, Show (..), ($), (++), (.), uncurry, id)
 import qualified Prelude      ()
 
 
@@ -68,7 +68,10 @@ type BRow i = Row i Bool
 fillTable :: LearnableAlphabet i => Teacher i -> Set [i] -> Set [i] -> BTable i
 fillTable teacher sssa ee = Prelude.uncurry union . map2 (map slv) . map2 simplify . partition (\(_, _, f) -> f) $ base
     where
-        base = pairsWith (\s e -> (s, e, membership teacher (s++e))) sssa ee
+        base0 = pairsWith (\s e -> (s++e)) sssa ee
+        base1 = membership teacher base0
+        base1b s e = forAll id $ mapFilter (\(i,f) -> maybeIf (i `eq` (s++e)) f)  base1
+        base = pairsWith (\s e -> (s, e, base1b s e)) sssa ee
         map2 f (a, b) = (f a, f b)
         slv (a,b,f) = ((a,b), fromJust . solve $ f)
 

src/Teacher.hs

@@ -19,7 +19,6 @@ import Control.Monad.Identity (Identity(..))
 import Control.Monad (when)
 import Data.IORef (IORef, readIORef, newIORef, writeIORef)
 import System.IO.Unsafe (unsafePerformIO)
-import qualified Data.Set as Set
 
 -- Used in the IO teacher
 import           System.Console.Haskeline
@@ -31,7 +30,7 @@ import           Text.Read               (readMaybe)
 data Teacher i = Teacher
     -- Given a sequence, check whether it is in the language
     -- Assumed to be equivariant
-    { membership :: [i] -> Formula
+    { membership :: Set [i] -> Set ([i], Formula)
     -- Given a hypothesis, returns Nothing when equivalence or a (equivariant)
     -- set of counter examples. Needs to be quantified over q, because the
     -- learner may choose the type of the state space.
@@ -40,6 +39,13 @@ data Teacher i = Teacher
     , alphabet   :: Set i
     }
 
+-- In order to count membership queries, I had to have the set of inputs
+-- instead of just mere inputs... It's a bit annoying, since it doesn't
+-- look like Angluin like this... But this is the best I can do in NLambda
+-- Here is a function to make it element-wise again:
+foreachQuery :: NominalType i => ([i] -> Formula) -> Set[i] -> Set ([i], Formula)
+foreachQuery f qs = map (\q -> (q, f q)) qs
+
 -- We provide three ways to construct teachers:
 -- 1. Fully automatic
 -- 2. Fully interactive (via IO)
@@ -49,7 +55,7 @@ data Teacher i = Teacher
 -- Only works for DFAs for now, as those can be checked for equivalence
 teacherWithTarget :: (NominalType i, NominalType q) => Automaton q i -> Teacher i
 teacherWithTarget aut = Teacher
-    { membership = automaticMembership aut
+    { membership = foreachQuery $ automaticMembership aut
     , equivalent = automaticEquivalent bisim aut
     , alphabet   = automaticAlphabet aut
     }
@@ -58,7 +64,7 @@ teacherWithTarget aut = Teacher
 -- Might work for NFAs, not really tested
 teacherWithTargetNonDet :: (Show i, Show q, NominalType i, NominalType q) => Int -> Automaton q i -> Teacher i
 teacherWithTargetNonDet n aut = Teacher
-    { membership = automaticMembership aut
+    { membership = foreachQuery $ automaticMembership aut
     , equivalent = automaticEquivalent (bisimNonDet n) aut
     , alphabet   = automaticAlphabet aut
     }
@@ -70,7 +76,7 @@ teacherWithTargetNonDet n aut = Teacher
 -- consider the whole orbit generated by it.
 teacherWithIO :: Teacher Atom
 teacherWithIO = Teacher
-    { membership = ioMembership
+    { membership = foreachQuery ioMembership
     , equivalent = ioEquivalent
     , alphabet   = atoms
     }
@@ -79,7 +85,7 @@ teacherWithIO = Teacher
 -- Useful as long as you don't have an equivalence check, For example for G-NFAs
 teacherWithTargetAndIO :: NominalType q => Automaton q Atom -> Teacher Atom
 teacherWithTargetAndIO aut = Teacher
-    { membership = automaticMembership aut
+    { membership = foreachQuery $ automaticMembership aut
     , equivalent = ioEquivalent
     , alphabet   = atoms
     }
@@ -88,7 +94,7 @@ teacherWithTargetAndIO aut = Teacher
 -- Useful for debugging and so on, but *very very hacky*!
 countingTeacher :: (Show i, NominalType i) => Teacher i -> Teacher i
 countingTeacher delegate = Teacher
-    { membership = \q -> increaseMQ q `seq` membership delegate q
+    { membership = \qs -> increaseMQ qs `seq` membership delegate qs
     , equivalent = \a -> increaseEQ a `seq` equivalent delegate a
     , alphabet   = alphabet delegate
     }
@@ -101,32 +107,26 @@ countingTeacher delegate = Teacher
             return j
         {-# NOINLINE increaseMQ #-}
         increaseMQ q = unsafePerformIO $ do
-            -- new <- notInCache q
+            new <- newOrbitsInCache q
-            -- when new $ do
+            l <- readIORef mqCounter
-                l <- readIORef mqCounter
+            let l2 = fromVariant new : l
-                let len = length q
+            writeIORef mqCounter l2
-                let sup = length $ leastSupport q
+        {-# NOINLINE cache #-}
-                let l2 = (len, sup) : l
+        cache = unsafePerformIO $ newIORef empty
-                writeIORef mqCounter l2
+        {-# NOINLINE newOrbitsInCache #-}
-        -- {-# NOINLINE cache #-}
+        newOrbitsInCache qs = do
-        -- cache = unsafePerformIO $ newIORef Set.empty
+            oldCache <- readIORef cache
-        -- {-# NOINLINE notInCache #-}
+            let newQs = qs \\ oldCache
-        -- notInCache q = do
+            writeIORef cache (oldCache `union` qs)
-        --     oldCache <- readIORef cache
+            return $ setOrbitsNumber newQs
-        --     case q `Set.member` oldCache of
-        --         True -> return False
-        --         False -> do
-        --             let newCache = Set.insert q oldCache
-        --             writeIORef cache newCache
-        --             return True
 
 -- HACK: Counts number of equivalence queries
 eqCounter :: IORef Int
 {-# NOINLINE eqCounter #-}
 eqCounter = unsafePerformIO $ newIORef 0
 
--- HACK: Keeps track of membership queries with: length, size of support
+-- HACK: Keeps track of membership queries with: # orbits per 'query'
-mqCounter :: IORef [(Int, Int)]
+mqCounter :: IORef [Int]
 {-# NOINLINE mqCounter #-}
 mqCounter = unsafePerformIO $ newIORef []