Counterexample handling

app/LStar.hs

@@ -6,38 +6,23 @@
 
 module Main where
 
-import Nominal hiding (product)
+import OnsAutomata
-import Support (Rat(..), Support(..), intersect)
+import OnsQuotient
+
 import OrbitList
 import qualified OrbitList as List
 import EquivariantMap (EquivariantMap(..), lookup, (!))
 import qualified EquivariantMap as Map
-import EquivariantSet (EquivariantSet(..))
 import qualified EquivariantSet as Set
 
+import Data.List (tails)
 import Control.Monad.State
-import Prelude hiding (filter, null, elem, lookup, product, Word, map, take, partition)
+import Prelude hiding (filter, null, elem, lookup, product, Word, map, take)
 
-type Word a    = [a]
 type Rows a    = OrbitList (Word a)
 type Columns a = OrbitList (Word a)
 type Table a   = EquivariantMap (Word a) Bool
 
--- states, initial state, acceptance, transition
-data Automaton q a = Automaton
-  { states :: OrbitList q
-  , initialState :: q
-  , acceptance :: EquivariantMap q Bool
-  , transition :: EquivariantMap (q, a) q
-  }
-
-instance (Nominal q, Nominal a, Show q, Show a) => Show (Automaton q a) where
-  show Automaton{..} = 
-       "{ states = " ++ show (toList states) ++
-       ", initialState = " ++ show initialState ++
-       ", acceptance = " ++ show (Map.toList acceptance) ++
-       ", transition = " ++ show (Map.toList transition) ++
-       "}"
 
 
 -- Utility functions
@@ -45,19 +30,19 @@ exists f = not . null . filter f
 forAll f = null . filter (not . f)
 ext p a = p <> [a]
 
-equalRows :: (Nominal a, Ord (Orbit a)) => Word a -> Word a -> Columns a -> Table a -> Bool
+equalRows :: _ => Word a -> Word a -> Columns a -> Table a -> Bool
 equalRows s0 t0 suffs table =
   forAll (\((s, t), e) -> lookup (s ++ e) table == lookup (t ++ e) table) $ product (singleOrbit (s0, t0)) suffs
 
-closed :: (Nominal a, Ord (Orbit a)) => Word a -> Rows a -> Columns a -> Table a -> Bool
+closed :: _ => Word a -> Rows a -> Columns a -> Table a -> Bool
 closed t prefs suffs table =
   exists (\(t, s) -> equalRows t s suffs table) (product (singleOrbit t) prefs)
 
-nonClosedness :: (Nominal a, Ord (Orbit a)) => Rows a -> Rows a -> Columns a -> Table a -> Rows a
+nonClosedness :: _ => Rows a -> Rows a -> Columns a -> Table a -> Rows a
 nonClosedness prefs prefsExt suffs table =
   filter (\t -> not $ closed t prefs suffs table) prefsExt
 
-inconsistencies :: (Nominal a, Ord a, Ord (Orbit a)) => Rows a -> Columns a -> Table a -> OrbitList a -> OrbitList ((Word a, Word a), (a, Word a))
+inconsistencies :: _ => Rows a -> Columns a -> Table a -> OrbitList a -> OrbitList ((Word a, Word a), (a, Word a))
 inconsistencies prefs suffs table alph =
   filter (\((s, t), (a, e)) -> lookup (s ++ (a:e)) table /= lookup (t ++ (a:e)) table) candidatesExt
   where
@@ -70,19 +55,6 @@ ask mq table (p, s) =
                         Just b -> return (w, b)
                         Nothing -> (w,) <$> mq w
 
--- Non trivial, should be made more efficient
-quotient :: _ => EquivariantSet (a, a) -> OrbitList a -> (EquivariantMap a (Int, Support), OrbitList (Int, Support))
-quotient equiv ls = go 0 Map.empty OrbitList.empty (toList ls)
-  where
-    go n phi acc []     = (phi, acc)
-    go n phi acc (a:as) = 
-      let (y0, r0) = partition (\p -> p `Set.member` equiv) (product (singleOrbit a) (fromList as))
-          y1 = filter (\p -> p `Set.member` equiv)  (product (singleOrbit a) (singleOrbit a))
-          y2 = map (\(a1, a2) -> (a2, (n, support a1 `intersect` support a2))) (y1 <> y0)
-          m0 = Map.fromListWith (\(n1, s1) (n2, s2) -> (n1, s1 `intersect` s2)) . OrbitList.toList $ y2
-          l0 = take 1 . fromList . fmap snd $ Map.toList m0
-      in go (n+1) (phi <> m0) (acc <> l0) (Set.toList . Set.fromOrbitList . map snd $ r0)
-
 
 -- invariants: * prefs and prefsExt disjoint, without dups
 --             * prefsExt ordered
@@ -100,7 +72,7 @@ data Observations a = Observations
 type LStar i m a = StateT (Observations i) m a
 
 -- precondition: newPrefs is subset of prefExts
-addRows :: (Nominal a, Ord (Orbit a), Monad m) => Rows a -> (Word a -> m Bool) -> LStar a m ()
+addRows :: _ => Rows a -> (Word a -> m Bool) -> LStar a m ()
 addRows newPrefs mq = do
   Observations{..} <- get
   let newPrefsExt = productWith ext newPrefs alph
@@ -115,7 +87,7 @@ addRows newPrefs mq = do
   return ()
 
 -- precondition: newSuffs disjoint from suffs
-addCols :: (Nominal a, Ord (Orbit a), Monad m) => Columns a -> (Word a -> m Bool) -> LStar a m ()
+addCols :: _ => Columns a -> (Word a -> m Bool) -> LStar a m ()
 addCols newSuffs mq = do
   Observations{..} <- get
   let rect = product (prefs `union` prefsExt) newSuffs
@@ -127,7 +99,7 @@ addCols newSuffs mq = do
           }
   return ()
 
-fillTable :: (Nominal a, Ord (Orbit a), Monad m) => (Word a -> m Bool) -> LStar a m ()
+fillTable :: _ => (Word a -> m Bool) -> LStar a m ()
 fillTable mq = do
   Observations{..} <- get
   let rect = product (prefs `union` prefsExt) suffs
@@ -143,8 +115,6 @@ learn mq = do
   Observations{..} <- get
   let ncl = nonClosedness prefs prefsExt suffs table
       inc = inconsistencies prefs suffs table alph
-  lift (print (toList ncl))
-  lift (print (toList inc))
   case null ncl of
     False -> do
       addRows (take 1 ncl) mq
@@ -159,8 +129,7 @@ learn mq = do
               (f, s) = quotient equiv prefs
               trans = Map.fromList . toList . map (\(s, t) -> (s, f ! t)) . filter (\(s, t) -> equalRows s t suffs table) $ product prefsExt prefs
               trans2 pa = if pa `elem` prefsExt then trans ! pa else f ! pa
-          lift (print (Map.toList trans))
+              hypothesis = Automaton
-          let hypothesis = Automaton
                 { states = s
                 , initialState = f ! []
                 , acceptance = Map.fromList . toList . map (\p -> (f ! p, table ! p)) $ prefs
@@ -169,13 +138,18 @@ learn mq = do
           eq <- lift (askEquiv hypothesis)
           case eq of
             Nothing -> return hypothesis
-            Just w -> error "No counterexample handling yet"
+            Just w -> do
+              lift (print w)
+              let allSuffs = Set.fromList $ tails w
+                  newSuffs = allSuffs `Set.difference` Set.fromOrbitList suffs
+              addCols (Set.toOrbitList newSuffs) mq
+              learn mq
 
 
-accept :: Show a => Word a -> IO Bool
+accept :: _ => Word a -> IO Bool
 accept w = do
   putStr "MQ \""
-  putStr (show w)
+  putStr (toStr w)
   putStrLn "\""
   a <- getLine
   case a of
@@ -186,10 +160,13 @@ accept w = do
 askEquiv :: _ => Automaton q a -> IO (Maybe (Word a))
 askEquiv aut = do
   putStr "EQ \""
-  putStr (show aut)
+  putStr (toStr aut)
   putStrLn "\""
   a <- getLine
-  return Nothing
+  case a of
+    "Y"       -> return Nothing
+    'N':' ':w -> return $ Just (fst $ fromStr w)
+    _         -> askEquiv aut
 
 main :: IO ()
 main = do
@@ -200,6 +177,6 @@ main = do
       table = Map.empty
       init = Observations{..}
   aut <- evalStateT (fillTable accept >> learn accept) init
-  print aut
+  putStrLn "Done learning :D"
   return ()
 

app/OnsAutomata.hs

@@ -0,0 +1,67 @@
+{-# language RecordWildCards #-}
+module OnsAutomata where
+
+import Data.Char (isSpace)
+import Data.Ratio
+import Data.List (intersperse)
+
+import Nominal
+import Support (Rat(..), Support(..))
+import OrbitList as L (OrbitList, toList)
+import EquivariantMap as M (EquivariantMap, toList)
+
+import Prelude hiding (print)
+
+
+type Word a    = [a]
+
+-- states, initial state, acceptance, transition
+data Automaton q a = Automaton
+  { states :: OrbitList q
+  , initialState :: q
+  , acceptance :: EquivariantMap q Bool
+  , transition :: EquivariantMap (q, a) q
+  }
+
+
+
+-- I do not want to give weird Show instances for basic types, so I create my
+-- own. This is not meant to be generic, but just enough for the queries of L*.
+class ToStr a where toStr :: a -> String
+class FromStr a where fromStr :: String -> (a, String)
+
+-- Should always print integers, this is not a problem for the things we build
+-- from getElementE (since it returns elements with support from 1 to n).
+instance ToStr Rat where
+  toStr (Rat r) = case denominator r of
+    1 -> show (numerator r)
+    _ -> error "Can only show integers"
+
+instance ToStr Support where
+  toStr (Support s) = "{" ++ toStr s ++ "}"
+
+instance ToStr Bool where toStr b = show b
+instance ToStr Int where toStr i = show i
+instance ToStr a => ToStr [a] where
+  toStr = concat . intersperse " " . fmap toStr
+instance (ToStr a, ToStr b) => ToStr (a, b) where
+  toStr (a, b) = "(" ++ toStr a ++ ", " ++ toStr b ++ ")" 
+
+instance (Nominal q, Nominal a, ToStr q, ToStr a) => ToStr (Automaton q a) where
+  toStr Automaton{..} =
+       "{ states = " ++ toStr (L.toList states) ++
+       ", initialState = " ++ toStr initialState ++
+       ", acceptance = " ++ toStr (M.toList acceptance) ++
+       ", transition = " ++ toStr (M.toList transition) ++ " }"
+
+instance FromStr Rat where
+  fromStr str = (Rat (read l % 1), r)
+    where (l, r) = break isSpace str
+
+instance FromStr a => FromStr [a] where
+  fromStr "" = ([], "")
+  fromStr str = (a : l, emptyStr)
+    where
+      (a, str2) = fromStr str
+      (l, emptyStr)    = fromStr (dropWhile isSpace str2)
+

app/OnsQuotient.hs

@@ -0,0 +1,28 @@
+{-# language FlexibleContexts #-}
+module OnsQuotient where
+
+import Nominal (Nominal(..))
+import Support (Support, intersect)
+import OrbitList
+import EquivariantMap (EquivariantMap(..))
+import qualified EquivariantMap as Map
+import EquivariantSet (EquivariantSet(..))
+import qualified EquivariantSet as Set
+
+import Prelude (Int, Ord, (.), (<>), (+), ($), snd, fmap)
+
+type QuotientType = (Int, Support)
+type QuotientMap a = EquivariantMap a QuotientType
+
+-- Non trivial, should be made more efficient
+quotient :: (Nominal a, Ord (Orbit a)) => EquivariantSet (a, a) -> OrbitList a -> (QuotientMap a, OrbitList QuotientType)
+quotient equiv ls = go 0 Map.empty empty (toList ls)
+  where
+    go _ phi acc []     = (phi, acc)
+    go n phi acc (a:as) = 
+      let (y0, r0) = partition (\p -> p `Set.member` equiv) (product (singleOrbit a) (fromList as))
+          y1 = filter (\p -> p `Set.member` equiv)  (product (singleOrbit a) (singleOrbit a))
+          y2 = map (\(a1, a2) -> (a2, (n, support a1 `intersect` support a2))) (y1 <> y0)
+          m0 = Map.fromListWith (\(n1, s1) (n2, s2) -> (n1, s1 `intersect` s2)) . toList $ y2
+          l0 = take 1 . fromList . fmap snd $ Map.toList m0
+      in go (n+1) (phi <> m0) (acc <> l0) (Set.toList . Set.fromOrbitList . map snd $ r0)

ons-hs.cabal

@@ -47,6 +47,8 @@ executable ons-hs-lstar
   build-depends:       base
                      , mtl
                      , ons-hs
+  other-modules:       OnsAutomata
+                     , OnsQuotient
   ghc-options:         -threaded -rtsopts -with-rtsopts=-N -O2
   default-language:    Haskell2010