From 6b89d2dc5f33f6bf2137daf5fb5f6096408126b0 Mon Sep 17 00:00:00 2001 From: Joshua Moerman Date: Thu, 10 Jan 2019 15:55:43 +0100 Subject: [PATCH] Counterexample handling --- app/LStar.hs | 77 ++++++++++++++++------------------------------ app/OnsAutomata.hs | 67 ++++++++++++++++++++++++++++++++++++++++ app/OnsQuotient.hs | 28 +++++++++++++++++ ons-hs.cabal | 2 ++ 4 files changed, 124 insertions(+), 50 deletions(-) create mode 100644 app/OnsAutomata.hs create mode 100644 app/OnsQuotient.hs diff --git a/app/LStar.hs b/app/LStar.hs index fa5c70c..c3e4c47 100644 --- a/app/LStar.hs +++ b/app/LStar.hs @@ -6,38 +6,23 @@ module Main where -import Nominal hiding (product) -import Support (Rat(..), Support(..), intersect) +import OnsAutomata +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)) - let hypothesis = Automaton + 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 () diff --git a/app/OnsAutomata.hs b/app/OnsAutomata.hs new file mode 100644 index 0000000..f77cb3a --- /dev/null +++ b/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) + diff --git a/app/OnsQuotient.hs b/app/OnsQuotient.hs new file mode 100644 index 0000000..66cbb92 --- /dev/null +++ b/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) diff --git a/ons-hs.cabal b/ons-hs.cabal index 3aa498e..87b3efa 100644 --- a/ons-hs.cabal +++ b/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