mirror of
https://github.com/Jaxan/nominal-lstar.git
synced 2025-04-27 14:47:45 +02:00
Made code anonymous
Also removed some vague comments
This commit is contained in:
parent
3de97f93c6
commit
2ebd8b9774
6 changed files with 26 additions and 17 deletions
|
@ -7,8 +7,8 @@ version: 0.1.0.0
|
||||||
-- description:
|
-- description:
|
||||||
-- license:
|
-- license:
|
||||||
license-file: LICENSE
|
license-file: LICENSE
|
||||||
author: Joshua Moerman
|
author: Anonymous
|
||||||
maintainer: lakseru@gmail.com
|
-- maintainer:
|
||||||
-- copyright:
|
-- copyright:
|
||||||
-- category:
|
-- category:
|
||||||
build-type: Simple
|
build-type: Simple
|
||||||
|
|
|
@ -54,7 +54,6 @@ useCounterExampleAngluin teacher state@State{..} ces =
|
||||||
addRows teacher ds state
|
addRows teacher ds state
|
||||||
|
|
||||||
-- This is the variant by Maler and Pnueli
|
-- This is the variant by Maler and Pnueli
|
||||||
-- I used to think it waw Rivest and Schapire, but they add less columns
|
|
||||||
useCounterExampleMP :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i
|
useCounterExampleMP :: LearnableAlphabet i => Teacher i -> State i -> Set [i] -> State i
|
||||||
useCounterExampleMP teacher state@State{..} ces =
|
useCounterExampleMP teacher state@State{..} ces =
|
||||||
trace ("Using ce: " ++ show ces) $
|
trace ("Using ce: " ++ show ces) $
|
||||||
|
@ -79,9 +78,9 @@ learnAngluinRows teacher = learn makeCompleteAngluin useCounterExampleAngluin co
|
||||||
-- Below are some variations of the above functions with different
|
-- Below are some variations of the above functions with different
|
||||||
-- performance characteristics.
|
-- performance characteristics.
|
||||||
|
|
||||||
-- Joshua's slower version
|
-- Some coauthor's slower version
|
||||||
consistencyTestJ :: NominalType i => State i -> TestResult i
|
consistencyTest2 :: NominalType i => State i -> TestResult i
|
||||||
consistencyTestJ State{..} = case solve (isEmpty defect) of
|
consistencyTest2 State{..} = case solve (isEmpty defect) of
|
||||||
Just True -> Succes
|
Just True -> Succes
|
||||||
Just False -> trace "Not consistent" $ Failed empty columns
|
Just False -> trace "Not consistent" $ Failed empty columns
|
||||||
where
|
where
|
||||||
|
@ -95,9 +94,9 @@ consistencyTestJ State{..} = case solve (isEmpty defect) of
|
||||||
) ss ss aa
|
) ss ss aa
|
||||||
columns = sum $ map (\((s1,s2,a),es) -> map (a:) es) defect
|
columns = sum $ map (\((s1,s2,a),es) -> map (a:) es) defect
|
||||||
|
|
||||||
-- Bartek's faster version
|
-- Some coauthor's faster version
|
||||||
consistencyTestB :: NominalType i => State i -> TestResult i
|
consistencyTest3 :: NominalType i => State i -> TestResult i
|
||||||
consistencyTestB State{..} = case solve (isEmpty defect) of
|
consistencyTest3 State{..} = case solve (isEmpty defect) of
|
||||||
Just True -> Succes
|
Just True -> Succes
|
||||||
Just False -> trace "Not consistent" $ Failed empty columns
|
Just False -> trace "Not consistent" $ Failed empty columns
|
||||||
where
|
where
|
||||||
|
|
|
@ -30,7 +30,6 @@ sublang r1 r2 = forAll fromBool $ pairsWithFilter (\(i1, f1) (i2, f2) -> maybeIf
|
||||||
sublangs :: NominalType i => BRow i -> Set (BRow i) -> Set (BRow i)
|
sublangs :: NominalType i => BRow i -> Set (BRow i) -> Set (BRow i)
|
||||||
sublangs r set = filter (\r2 -> r2 `sublang` r) set
|
sublangs r set = filter (\r2 -> r2 `sublang` r) set
|
||||||
|
|
||||||
-- Infinitary version ?
|
|
||||||
rfsaClosednessTest2 :: LearnableAlphabet i => State i -> TestResult i
|
rfsaClosednessTest2 :: LearnableAlphabet i => State i -> TestResult i
|
||||||
rfsaClosednessTest2 State{..} = case solve (isEmpty defect) of
|
rfsaClosednessTest2 State{..} = case solve (isEmpty defect) of
|
||||||
Just True -> Succes
|
Just True -> Succes
|
||||||
|
|
|
@ -25,7 +25,10 @@ import Prelude hiding (and, curry, filter, lookup, map, not,
|
||||||
Sounds a bit crazy, but the teacher kind of takes care of that. Of course
|
Sounds a bit crazy, but the teacher kind of takes care of that. Of course
|
||||||
I do not know whether this will terminate. But it's nice to experiment with.
|
I do not know whether this will terminate. But it's nice to experiment with.
|
||||||
Also I do not 'minimize' the NFA by taking only prime rows. Saves a lot of
|
Also I do not 'minimize' the NFA by taking only prime rows. Saves a lot of
|
||||||
checking but makes the result not minimal (whatever that would mean).
|
checking but makes the result not minimal (whatever that would mean). It
|
||||||
|
is quite fast, however ;-).
|
||||||
|
|
||||||
|
THIS IS NOT USED IN THE PAPER.
|
||||||
-}
|
-}
|
||||||
|
|
||||||
-- We can determine its completeness with the following
|
-- We can determine its completeness with the following
|
||||||
|
|
|
@ -29,7 +29,6 @@ apply f a1 = mapFilter (\(a2, b) -> maybeIf (eq a1 a2) b) f
|
||||||
|
|
||||||
-- Returns the subset (of the domain) which exhibits
|
-- Returns the subset (of the domain) which exhibits
|
||||||
-- different return values for the two functions
|
-- different return values for the two functions
|
||||||
-- I am not sure about its correctness...
|
|
||||||
discrepancy :: (NominalType a, NominalType b) => Fun a b -> Fun a b -> Set a
|
discrepancy :: (NominalType a, NominalType b) => Fun a b -> Fun a b -> Set a
|
||||||
discrepancy f1 f2 =
|
discrepancy f1 f2 =
|
||||||
pairsWithFilter (
|
pairsWithFilter (
|
||||||
|
|
|
@ -27,9 +27,12 @@ import Text.Read (readMaybe)
|
||||||
|
|
||||||
-- Abstract teacher type (inside the NLambda library, ideally one would like
|
-- Abstract teacher type (inside the NLambda library, ideally one would like
|
||||||
-- an external interface, with Bool as output instead of Formula for instance)
|
-- an external interface, with Bool as output instead of Formula for instance)
|
||||||
|
-- For now we do actually implement an external teacher, but it is rather hacky.
|
||||||
data Teacher i = Teacher
|
data Teacher i = Teacher
|
||||||
-- Given a sequence, check whether it is in the language
|
-- Given a sequence, check whether it is in the language
|
||||||
-- Assumed to be equivariant
|
-- Assumed to be equivariant.
|
||||||
|
-- We slightly change the type to support counting the number of orbits.
|
||||||
|
-- All teacher (except the counting one) implement membership :: [i] -> Formula
|
||||||
{ membership :: Set [i] -> Set ([i], Formula)
|
{ membership :: Set [i] -> Set ([i], Formula)
|
||||||
-- Given a hypothesis, returns Nothing when equivalence or a (equivariant)
|
-- Given a hypothesis, returns Nothing when equivalence or a (equivariant)
|
||||||
-- set of counter examples. Needs to be quantified over q, because the
|
-- set of counter examples. Needs to be quantified over q, because the
|
||||||
|
@ -50,6 +53,8 @@ foreachQuery f qs = map (\q -> (q, f q)) qs
|
||||||
-- 1. Fully automatic
|
-- 1. Fully automatic
|
||||||
-- 2. Fully interactive (via IO)
|
-- 2. Fully interactive (via IO)
|
||||||
-- 3. Automatic membership, but interactive equivalence tests
|
-- 3. Automatic membership, but interactive equivalence tests
|
||||||
|
-- Furthermore we provide a teacher which counts and then passes the query
|
||||||
|
-- to a delegate.
|
||||||
|
|
||||||
-- 1. This is a fully automatic teacher, which has an internal automaton
|
-- 1. This is a fully automatic teacher, which has an internal automaton
|
||||||
-- Only works for DFAs for now, as those can be checked for equivalence
|
-- Only works for DFAs for now, as those can be checked for equivalence
|
||||||
|
@ -61,7 +66,7 @@ teacherWithTarget aut = Teacher
|
||||||
}
|
}
|
||||||
|
|
||||||
-- 1b. This is a fully automatic teacher, which has an internal automaton
|
-- 1b. This is a fully automatic teacher, which has an internal automaton
|
||||||
-- Might work for NFAs, not really tested
|
-- NFA have undecidable equivalence, n is a bound on deoth of bisimulation.
|
||||||
teacherWithTargetNonDet :: (Show i, Show q, NominalType i, NominalType q) => Int -> Automaton q i -> Teacher i
|
teacherWithTargetNonDet :: (Show i, Show q, NominalType i, NominalType q) => Int -> Automaton q i -> Teacher i
|
||||||
teacherWithTargetNonDet n aut = Teacher
|
teacherWithTargetNonDet n aut = Teacher
|
||||||
{ membership = foreachQuery $ automaticMembership aut
|
{ membership = foreachQuery $ automaticMembership aut
|
||||||
|
@ -82,7 +87,8 @@ teacherWithIO = Teacher
|
||||||
}
|
}
|
||||||
|
|
||||||
-- 3. A teacher uses a target for the mebership queries, but you for equivalence
|
-- 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, For example for G-NFAs
|
-- Useful as long as you don't have an equivalence check
|
||||||
|
-- used for NFAs when there was no bounded bisimulation yet
|
||||||
teacherWithTargetAndIO :: NominalType q => Automaton q Atom -> Teacher Atom
|
teacherWithTargetAndIO :: NominalType q => Automaton q Atom -> Teacher Atom
|
||||||
teacherWithTargetAndIO aut = Teacher
|
teacherWithTargetAndIO aut = Teacher
|
||||||
{ membership = foreachQuery $ automaticMembership aut
|
{ membership = foreachQuery $ automaticMembership aut
|
||||||
|
@ -131,7 +137,9 @@ mqCounter :: IORef [Int]
|
||||||
{-# NOINLINE mqCounter #-}
|
{-# NOINLINE mqCounter #-}
|
||||||
mqCounter = unsafePerformIO $ newIORef []
|
mqCounter = unsafePerformIO $ newIORef []
|
||||||
|
|
||||||
|
|
||||||
-- Implementations of above functions
|
-- Implementations of above functions
|
||||||
|
--
|
||||||
automaticMembership aut input = accepts aut input
|
automaticMembership aut input = accepts aut input
|
||||||
automaticEquivalent bisimlator aut hypo = case solve isEq of
|
automaticEquivalent bisimlator aut hypo = case solve isEq of
|
||||||
Nothing -> error "should be solved"
|
Nothing -> error "should be solved"
|
||||||
|
@ -146,8 +154,7 @@ automaticAlphabet aut = NLambda.alphabet aut
|
||||||
instance Conditional a => Conditional (Identity a) where
|
instance Conditional a => Conditional (Identity a) where
|
||||||
cond f x y = return (cond f (runIdentity x) (runIdentity y))
|
cond f x y = return (cond f (runIdentity x) (runIdentity y))
|
||||||
|
|
||||||
-- Checks bisimulation of initial states
|
-- Checks bisimulation of initial states (only for DFAs)
|
||||||
-- I am not sure whether it does the right thing for non-det automata
|
|
||||||
-- returns some counter examples if not bisimilar
|
-- returns some counter examples if not bisimilar
|
||||||
-- returns empty set iff bisimilar
|
-- returns empty set iff bisimilar
|
||||||
bisim :: (NominalType i, NominalType q1, NominalType q2) => Automaton q1 i -> Automaton q2 i -> Set [i]
|
bisim :: (NominalType i, NominalType q1, NominalType q2) => Automaton q1 i -> Automaton q2 i -> Set [i]
|
||||||
|
@ -219,6 +226,7 @@ bisimNonDet n aut1 aut2 = runIdentity $ go empty (singleton ([], initialStates a
|
||||||
addEmptyWord x y = ([], x, y)
|
addEmptyWord x y = ([], x, y)
|
||||||
sumMap f = sum . (map f)
|
sumMap f = sum . (map f)
|
||||||
|
|
||||||
|
-- Posing a membership query to the terminal and waits for used to input a formula
|
||||||
ioMembership :: (Show i, NominalType i) => [i] -> Formula
|
ioMembership :: (Show i, NominalType i) => [i] -> Formula
|
||||||
ioMembership input = unsafePerformIO $ do
|
ioMembership input = unsafePerformIO $ do
|
||||||
let supp = leastSupport input
|
let supp = leastSupport input
|
||||||
|
@ -243,6 +251,7 @@ ioMembership input = unsafePerformIO $ do
|
||||||
loop
|
loop
|
||||||
Just f -> return f
|
Just f -> return f
|
||||||
|
|
||||||
|
-- Poses a query to the terminal, waiting for the user to provide a counter example
|
||||||
ioEquivalent :: (Show q, NominalType q) => Automaton q Atom -> Maybe (Set [Atom])
|
ioEquivalent :: (Show q, NominalType q) => Automaton q Atom -> Maybe (Set [Atom])
|
||||||
ioEquivalent hypothesis = unsafePerformIO $ do
|
ioEquivalent hypothesis = unsafePerformIO $ do
|
||||||
Prelude.putStrLn "\n# Is the following automaton correct?"
|
Prelude.putStrLn "\n# Is the following automaton correct?"
|
||||||
|
|
Loading…
Add table
Reference in a new issue