mirror of
https://github.com/Jaxan/nominal-lstar.git
synced 2025-04-27 14:47:45 +02:00
Updates it to use the new nlambda (with better support for generics).
This commit is contained in:
parent
2d1d5d7bfd
commit
b05d958666
8 changed files with 32 additions and 45 deletions
|
@ -20,11 +20,13 @@ executable NominalAngluin
|
||||||
Examples.Stack,
|
Examples.Stack,
|
||||||
NLStar,
|
NLStar,
|
||||||
ObservationTable,
|
ObservationTable,
|
||||||
Teacher
|
Teacher,
|
||||||
|
Teachers.Teacher,
|
||||||
|
Teachers.Terminal,
|
||||||
|
Teachers.Whitebox
|
||||||
build-depends:
|
build-depends:
|
||||||
base >= 4.8 && < 5,
|
base >= 4.8 && < 5,
|
||||||
containers,
|
containers,
|
||||||
deepseq,
|
|
||||||
haskeline,
|
haskeline,
|
||||||
mtl,
|
mtl,
|
||||||
NLambda >= 1.1
|
NLambda >= 1.1
|
||||||
|
|
|
@ -4,7 +4,6 @@ module AbstractLStar where
|
||||||
import ObservationTable
|
import ObservationTable
|
||||||
import Teacher
|
import Teacher
|
||||||
|
|
||||||
import Control.DeepSeq (deepseq)
|
|
||||||
import Debug.Trace
|
import Debug.Trace
|
||||||
import NLambda
|
import NLambda
|
||||||
|
|
||||||
|
@ -48,7 +47,6 @@ learn :: LearnableAlphabet i
|
||||||
-> State i
|
-> State i
|
||||||
-> Automaton (BRow i) i
|
-> Automaton (BRow i) i
|
||||||
learn makeComplete handleCounterExample constructHypothesis teacher s =
|
learn makeComplete handleCounterExample constructHypothesis teacher s =
|
||||||
deepseq s $ -- This helps ordering the traces somewhat.
|
|
||||||
trace "##################" $
|
trace "##################" $
|
||||||
trace "1. Making it complete and consistent" $
|
trace "1. Making it complete and consistent" $
|
||||||
let s2 = makeComplete teacher s in
|
let s2 = makeComplete teacher s in
|
||||||
|
|
|
@ -1,4 +1,4 @@
|
||||||
{-# LANGUAGE DeriveGeneric #-}
|
{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
|
||||||
module Examples.Contrived where
|
module Examples.Contrived where
|
||||||
|
|
||||||
import NLambda
|
import NLambda
|
||||||
|
@ -12,8 +12,8 @@ import GHC.Generics (Generic)
|
||||||
-- Example automaton from the whiteboard. Three orbits with 0, 1 and 2
|
-- Example automaton from the whiteboard. Three orbits with 0, 1 and 2
|
||||||
-- registers. The third orbit has a local symmetry (S2).
|
-- registers. The third orbit has a local symmetry (S2).
|
||||||
data Example1 = Initial | S1 Atom | S2 (Atom, Atom)
|
data Example1 = Initial | S1 Atom | S2 (Atom, Atom)
|
||||||
deriving (Show, Eq, Ord, Generic)
|
deriving (Show, Eq, Ord, Generic, NominalType, Contextual)
|
||||||
instance BareNominalType Example1
|
|
||||||
example1 :: Automaton Example1 Atom
|
example1 :: Automaton Example1 Atom
|
||||||
example1 = automaton
|
example1 = automaton
|
||||||
-- states, 4 orbits (of which one unreachable)
|
-- states, 4 orbits (of which one unreachable)
|
||||||
|
@ -36,8 +36,9 @@ example1 = automaton
|
||||||
|
|
||||||
-- Accepts all even words (ignores the alphabet). Two orbits, with a
|
-- Accepts all even words (ignores the alphabet). Two orbits, with a
|
||||||
-- trivial action. No registers.
|
-- trivial action. No registers.
|
||||||
data Aut2 = Even | Odd deriving (Eq, Ord, Show, Generic)
|
data Aut2 = Even | Odd
|
||||||
instance BareNominalType Aut2
|
deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
|
||||||
|
|
||||||
example2 :: Automaton Aut2 Atom
|
example2 :: Automaton Aut2 Atom
|
||||||
example2 = automaton
|
example2 = automaton
|
||||||
-- states, two orbits
|
-- states, two orbits
|
||||||
|
@ -55,8 +56,9 @@ example2 = automaton
|
||||||
|
|
||||||
-- Accepts all non-empty words with the same symbol. Three orbits: the initial
|
-- Accepts all non-empty words with the same symbol. Three orbits: the initial
|
||||||
-- state, a state with a register and a sink state.
|
-- state, a state with a register and a sink state.
|
||||||
data Aut3 = Empty | Stored Atom | Sink deriving (Eq, Ord, Show, Generic)
|
data Aut3 = Empty | Stored Atom | Sink
|
||||||
instance BareNominalType Aut3
|
deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
|
||||||
|
|
||||||
example3 :: Automaton Aut3 Atom
|
example3 :: Automaton Aut3 Atom
|
||||||
example3 = automaton
|
example3 = automaton
|
||||||
-- states, three orbits
|
-- states, three orbits
|
||||||
|
@ -84,8 +86,8 @@ data Aut4 = Aut4Init -- Initial state
|
||||||
| Second Atom Atom -- After reading two different symbols
|
| Second Atom Atom -- After reading two different symbols
|
||||||
| Symm Atom Atom Atom -- Accepting state with C3 symmetry
|
| Symm Atom Atom Atom -- Accepting state with C3 symmetry
|
||||||
| Sorted Atom Atom Atom -- State without symmetry
|
| Sorted Atom Atom Atom -- State without symmetry
|
||||||
deriving (Eq, Ord, Show, Generic)
|
deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
|
||||||
instance BareNominalType Aut4
|
|
||||||
example4 :: Automaton Aut4 Atom
|
example4 :: Automaton Aut4 Atom
|
||||||
example4 = automaton
|
example4 = automaton
|
||||||
-- states
|
-- states
|
||||||
|
@ -123,8 +125,8 @@ example4 = automaton
|
||||||
|
|
||||||
-- Accepts all two-symbols words with different atoms
|
-- Accepts all two-symbols words with different atoms
|
||||||
data Aut5 = Aut5Init | Aut5Store Atom | Aut5T | Aut5F
|
data Aut5 = Aut5Init | Aut5Store Atom | Aut5T | Aut5F
|
||||||
deriving (Eq, Ord, Show, Generic)
|
deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
|
||||||
instance BareNominalType Aut5
|
|
||||||
example5 :: Automaton Aut5 Atom
|
example5 :: Automaton Aut5 Atom
|
||||||
example5 = automaton
|
example5 = automaton
|
||||||
-- states
|
-- states
|
||||||
|
|
|
@ -1,4 +1,4 @@
|
||||||
{-# LANGUAGE DeriveGeneric #-}
|
{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
|
||||||
{-# LANGUAGE TupleSections #-}
|
{-# LANGUAGE TupleSections #-}
|
||||||
module Examples.ContrivedNFAs where
|
module Examples.ContrivedNFAs where
|
||||||
|
|
||||||
|
@ -14,8 +14,8 @@ import GHC.Generics (Generic)
|
||||||
-- The complement of 'all distinct atoms'
|
-- The complement of 'all distinct atoms'
|
||||||
-- Not determinizable
|
-- Not determinizable
|
||||||
data NFA1 = Initial1 | Guessed1 Atom | Final1
|
data NFA1 = Initial1 | Guessed1 Atom | Final1
|
||||||
deriving (Show, Eq, Ord, Generic)
|
deriving (Show, Eq, Ord, Generic, NominalType, Contextual)
|
||||||
instance BareNominalType NFA1
|
|
||||||
exampleNFA1 :: Automaton NFA1 Atom
|
exampleNFA1 :: Automaton NFA1 Atom
|
||||||
exampleNFA1 = automaton
|
exampleNFA1 = automaton
|
||||||
-- states, 4 orbits (of which one unreachable)
|
-- states, 4 orbits (of which one unreachable)
|
||||||
|
@ -43,8 +43,8 @@ exampleNFA1 = automaton
|
||||||
-- So this one *is* determinizable.
|
-- So this one *is* determinizable.
|
||||||
-- Also used in the Bollig et al paper.
|
-- Also used in the Bollig et al paper.
|
||||||
data NFA2 = Initial2 | Distinguished Atom | Count Int
|
data NFA2 = Initial2 | Distinguished Atom | Count Int
|
||||||
deriving (Show, Eq, Ord, Generic)
|
deriving (Show, Eq, Ord, Generic, NominalType, Contextual)
|
||||||
instance BareNominalType NFA2
|
|
||||||
exampleNFA2 n = automaton
|
exampleNFA2 n = automaton
|
||||||
(singleton Initial2
|
(singleton Initial2
|
||||||
`union` map Distinguished atoms
|
`union` map Distinguished atoms
|
||||||
|
|
|
@ -1,7 +1,6 @@
|
||||||
{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
|
{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
|
||||||
module Examples.Fifo (DataInput(..), fifoExample) where
|
module Examples.Fifo (DataInput(..), fifoExample) where
|
||||||
|
|
||||||
import Control.DeepSeq (NFData)
|
|
||||||
import GHC.Generics (Generic)
|
import GHC.Generics (Generic)
|
||||||
import NLambda
|
import NLambda
|
||||||
import Prelude (Eq, Int, Maybe (..), Ord, Show, Read, length, reverse,
|
import Prelude (Eq, Int, Maybe (..), Ord, Show, Read, length, reverse,
|
||||||
|
@ -12,7 +11,8 @@ import qualified Prelude ()
|
||||||
-- Functional queue data type. First list is for push stuff onto, the
|
-- Functional queue data type. First list is for push stuff onto, the
|
||||||
-- second list is to pop. If the second list is empty, it will reverse
|
-- second list is to pop. If the second list is empty, it will reverse
|
||||||
-- the first.
|
-- the first.
|
||||||
data Fifo a = Fifo [a] [a] deriving (Eq, Ord, Show, Generic)
|
data Fifo a = Fifo [a] [a]
|
||||||
|
deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
|
||||||
|
|
||||||
push :: a -> Fifo a -> Fifo a
|
push :: a -> Fifo a -> Fifo a
|
||||||
push x (Fifo l1 l2) = Fifo (x:l1) l2
|
push x (Fifo l1 l2) = Fifo (x:l1) l2
|
||||||
|
@ -35,16 +35,12 @@ sizeFifo (Fifo l1 l2) = length l1 + length l2
|
||||||
-- nominal automaton.
|
-- nominal automaton.
|
||||||
|
|
||||||
-- The alphabet:
|
-- The alphabet:
|
||||||
data DataInput = Put Atom | Get Atom deriving (Eq, Ord, Show, Read, Generic, NFData)
|
data DataInput = Put Atom | Get Atom
|
||||||
instance BareNominalType DataInput
|
deriving (Eq, Ord, Show, Read, Generic, NominalType, Contextual)
|
||||||
instance Contextual DataInput where
|
|
||||||
when f (Put a) = Put (when f a)
|
|
||||||
when f (Get a) = Get (when f a)
|
|
||||||
|
|
||||||
-- The automaton: States consist of fifo queues and a sink state.
|
-- The automaton: States consist of fifo queues and a sink state.
|
||||||
-- This representation is not minimal at all, but that's OK, since the
|
-- This representation is not minimal at all, but that's OK, since the
|
||||||
-- learner will learn a minimal anyways. The parameter n is the bound.
|
-- learner will learn a minimal anyways. The parameter n is the bound.
|
||||||
instance BareNominalType a => BareNominalType (Fifo a)
|
|
||||||
fifoExample :: Int -> Automaton (Maybe (Fifo Atom)) DataInput
|
fifoExample :: Int -> Automaton (Maybe (Fifo Atom)) DataInput
|
||||||
fifoExample n = automaton
|
fifoExample n = automaton
|
||||||
-- states
|
-- states
|
||||||
|
|
|
@ -19,7 +19,7 @@ import GHC.Generics (Generic)
|
||||||
|
|
||||||
-- Parametric in the alphabet, because why not?
|
-- Parametric in the alphabet, because why not?
|
||||||
data RunningExample a = Store [a] | Check [a] | Accept | Reject
|
data RunningExample a = Store [a] | Check [a] | Accept | Reject
|
||||||
deriving (Eq, Ord, Show, Generic, BareNominalType)
|
deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
|
||||||
|
|
||||||
runningExample alphabet 0 = automaton
|
runningExample alphabet 0 = automaton
|
||||||
(fromList [Accept, Reject])
|
(fromList [Accept, Reject])
|
||||||
|
|
|
@ -1,4 +1,4 @@
|
||||||
{-# LANGUAGE DeriveGeneric #-}
|
{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
|
||||||
module Examples.Stack (DataInput(..), stackExample) where
|
module Examples.Stack (DataInput(..), stackExample) where
|
||||||
|
|
||||||
import Examples.Fifo (DataInput (..))
|
import Examples.Fifo (DataInput (..))
|
||||||
|
@ -10,7 +10,8 @@ import qualified Prelude ()
|
||||||
|
|
||||||
|
|
||||||
-- Functional stack data type is simply a list.
|
-- Functional stack data type is simply a list.
|
||||||
data Stack a = Stack [a] deriving (Eq, Ord, Show, Generic)
|
data Stack a = Stack [a]
|
||||||
|
deriving (Eq, Ord, Show, Generic, NominalType, Contextual)
|
||||||
|
|
||||||
push :: a -> Stack a -> Stack a
|
push :: a -> Stack a -> Stack a
|
||||||
push x (Stack l1) = Stack (x:l1)
|
push x (Stack l1) = Stack (x:l1)
|
||||||
|
@ -35,7 +36,6 @@ sizeStack (Stack l1) = length l1
|
||||||
|
|
||||||
-- The automaton: States consist of stacks and a sink state.
|
-- The automaton: States consist of stacks and a sink state.
|
||||||
-- The parameter n is the bound.
|
-- The parameter n is the bound.
|
||||||
instance BareNominalType a => BareNominalType (Stack a)
|
|
||||||
stackExample :: Int -> Automaton (Maybe (Stack Atom)) DataInput
|
stackExample :: Int -> Automaton (Maybe (Stack Atom)) DataInput
|
||||||
stackExample n = automaton
|
stackExample n = automaton
|
||||||
-- states
|
-- states
|
||||||
|
|
|
@ -10,7 +10,6 @@ module ObservationTable where
|
||||||
import NLambda hiding (fromJust)
|
import NLambda hiding (fromJust)
|
||||||
import Teacher
|
import Teacher
|
||||||
|
|
||||||
import Control.DeepSeq (NFData, force)
|
|
||||||
import Data.Maybe (fromJust)
|
import Data.Maybe (fromJust)
|
||||||
import Debug.Trace (trace)
|
import Debug.Trace (trace)
|
||||||
import GHC.Generics (Generic)
|
import GHC.Generics (Generic)
|
||||||
|
@ -43,7 +42,7 @@ type Row i o = Fun [i] o
|
||||||
|
|
||||||
-- This is a rather arbitrary set of constraints
|
-- This is a rather arbitrary set of constraints
|
||||||
-- But I use them *everywhere*, so let's define them once and for all.
|
-- But I use them *everywhere*, so let's define them once and for all.
|
||||||
type LearnableAlphabet i = (NFData i, Contextual i, NominalType i, Show i)
|
type LearnableAlphabet i = (Contextual i, NominalType i, Show i)
|
||||||
|
|
||||||
-- `row is` denotes the data of a single row
|
-- `row is` denotes the data of a single row
|
||||||
-- that is, the function E -> O
|
-- that is, the function E -> O
|
||||||
|
@ -83,17 +82,7 @@ data State i = State
|
||||||
, ee :: Set [i] -- suffixes
|
, ee :: Set [i] -- suffixes
|
||||||
, aa :: Set i -- alphabet (remains constant)
|
, aa :: Set i -- alphabet (remains constant)
|
||||||
}
|
}
|
||||||
deriving (Show, Ord, Eq, Generic, NFData, BareNominalType)
|
deriving (Show, Ord, Eq, Generic, NominalType, Conditional, Contextual)
|
||||||
|
|
||||||
instance NominalType i => Conditional (State i) where
|
|
||||||
cond f s1 s2 = fromTup (cond f (toTup s1) (toTup s2)) where
|
|
||||||
toTup State{..} = (t,ss,ssa,ee,aa)
|
|
||||||
fromTup (t,ss,ssa,ee,aa) = State{..}
|
|
||||||
|
|
||||||
instance (Ord i, Contextual i) => Contextual (State i) where
|
|
||||||
when f s = fromTup (when f (toTup s)) where
|
|
||||||
toTup State{..} = (t,ss,ssa,ee,aa)
|
|
||||||
fromTup (t,ss,ssa,ee,aa) = State{..}
|
|
||||||
|
|
||||||
-- Precondition: the set together with the current rows is prefix closed
|
-- Precondition: the set together with the current rows is prefix closed
|
||||||
addRows :: LearnableAlphabet i => Teacher i -> Set [i] -> State i -> State i
|
addRows :: LearnableAlphabet i => Teacher i -> Set [i] -> State i -> State i
|
||||||
|
|
Loading…
Add table
Reference in a new issue