diff --git a/NominalAngluin.cabal b/NominalAngluin.cabal index a81a303..2263cf8 100644 --- a/NominalAngluin.cabal +++ b/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 diff --git a/src/AbstractLStar.hs b/src/AbstractLStar.hs index d72368b..39f3494 100644 --- a/src/AbstractLStar.hs +++ b/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 - traceShow eq $ - case eq of - Nothing -> h - Just ce -> do - let s3 = handleCounterExample teacher s2 ce - learn makeComplete handleCounterExample constructHypothesis teacher s3 + eqloop s2 h + where + eqloop s2 h = case equivalent teacher h of + Nothing -> trace "Yes" $ h + Just ces -> trace "No" $ + 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 diff --git a/src/Angluin.hs b/src/Angluin.hs index b9de749..e120eb2 100644 --- a/src/Angluin.hs +++ b/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 diff --git a/src/Teacher.hs b/src/Teacher.hs index 0c0c293..a932d78 100644 --- a/src/Teacher.hs +++ b/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 diff --git a/src/Teachers/Terminal.hs b/src/Teachers/Terminal.hs index 5b4f621..57b92ac 100644 --- a/src/Teachers/Terminal.hs +++ b/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)"